First propagation of missing attribute errors

1 files changed, 51 insertions, 51 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 2690134..5a2f536 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -322,6 +322,13 @@ namespace PolicyCombinatorAlgorithm
   def eval_legacy_ordered_permit_overrides : List Decision' -> Decision' := eval_legacy_permit_overrides
 end PolicyCombinatorAlgorithm
 
+inductive StatusCode
+  | ok                : StatusCode
+  | missing_attribute : StatusCode
+  | syntax_error      : StatusCode
+  | processing_error  : StatusCode
+deriving BEq, Repr
+
 structure AttributeDesignator where
   category        : String
   identifier      : String
@@ -331,7 +338,7 @@ structure AttributeDesignator where
 deriving BEq, Repr
 
 namespace AttributeDesignator
-  def eval (designator : AttributeDesignator) (context : List Attribute) : Option Value :=
+  def eval (designator : AttributeDesignator) (context : List Attribute) : Sum Value (List StatusCode) :=
     match designator with
       | AttributeDesignator.mk category identifier type issuer must_be_present =>
         let found :=
@@ -360,9 +367,9 @@ namespace AttributeDesignator
         let found := found.map (fun x => x.value)
         if must_be_present then
           match found with
-            | [] => Option.none
-            | _ => Value.bag (Bag.mk found)
-        else Value.bag (Bag.mk found)
+            | [] => Sum.inr $ [StatusCode.missing_attribute]
+            | _ => Sum.inl $ Value.bag (Bag.mk found)
+        else Sum.inl $ Value.bag (Bag.mk found)
 end AttributeDesignator
 
 def matches? (designator : AttributeDesignator) (attr : Attribute) : Prop :=
@@ -427,7 +434,10 @@ namespace Expression
     -- - <xacml:VariableReference>
     match expression with
       | Expression.apply name args            => apply_eval name args
-      | Expression.attribute_designator inner => inner.eval context
+      | Expression.attribute_designator inner =>
+        match inner.eval context with
+        | Sum.inl res => res
+        | Sum.inr status => Option.none
       | Expression.attribute_value inner      => some inner
       | _                                     => Option.none
 end Expression
@@ -468,46 +478,44 @@ namespace Match
   def eval (m : Match) (context : Request) : Option Value :=
     match m with
       | Match.mk fn designator value =>
-        do
-          let result <- designator.eval context
-          let results := match result with
-          -- Otherwise, the MatchId function SHALL be applied between the
-          -- <AttributeValue> and each element of the bag returned from the
-          -- <AttributeDesignator> or <AttributeSelector> element.
-          | (Value.bag (Bag.mk attrs)) =>
-            attrs.map fun attr =>
+        match designator.eval context with
+          | Sum.inl result =>
+            let results := match result with
+            -- Otherwise, the MatchId function SHALL be applied between the
+            -- <AttributeValue> and each element of the bag returned from the
+            -- <AttributeDesignator> or <AttributeSelector> element.
+            | (Value.bag (Bag.mk attrs)) =>
+              attrs.map fun attr =>
+                let args := [value, Value.primitive attr]
+                (Expression.apply fn args).eval context
+            | (Value.primitive attr) =>
+              -- TODO: Prove that this case is impossible.
               let args := [value, Value.primitive attr]
-              (Expression.apply fn args).eval context
-          | (Value.primitive attr) =>
-            -- TODO: Prove that this case is impossible.
-            let args := [value, Value.primitive attr]
-            [(Expression.apply fn args).eval context]
+              [(Expression.apply fn args).eval context]
 
-          let results := results.map (fun (x : Option Value) => (x : Value))
-          -- If at least one of those function applications were to evaluate to
-          -- "True", then the result of the entire expression SHALL be "True".
-          if results.elem (Value.primitive (#<XmlType.boolean, "True">)) then
-            (Value.primitive (#<XmlType.boolean, "True">))
-          -- Otherwise, if at least one of the function applications results in
-          -- "Indeterminate", then the result SHALL be "Indeterminate".
-          else if results.elem (Value.primitive (#<XmlType.boolean, "Indeterminate">)) then
-            (Value.primitive (#<XmlType.boolean, "Indeterminate">))
-          -- The `else` arm handles the following cases:
-          --
-          -- If the <AttributeDesignator> or <AttributeSelector> element were to
-          -- evaluate to an empty bag, then the result of the expression SHALL
-          -- be "False".
-          --
-          -- Finally, if all function applications evaluate to "False", then the
-          -- result of the entire expression SHALL be "False".
-          else
-            Value.primitive (#<XmlType.boolean, "False">)
-      -- If an operational error were to occur while evaluating the
-      -- <AttributeDesignator> or <AttributeSelector> element, then the result
-      -- of the entire expression SHALL be "Indeterminate".
-      --
-      -- In our case, this is handled by the Option monad, since the assignment
-      -- to `result` would fail.
+            let results := results.map (fun (x : Option Value) => (x : Value))
+            -- If at least one of those function applications were to evaluate to
+            -- "True", then the result of the entire expression SHALL be "True".
+            if results.elem (Value.primitive (#<XmlType.boolean, "True">)) then
+              (Value.primitive (#<XmlType.boolean, "True">))
+            -- Otherwise, if at least one of the function applications results in
+            -- "Indeterminate", then the result SHALL be "Indeterminate".
+            else if results.elem (Value.primitive (#<XmlType.boolean, "Indeterminate">)) then
+              (Value.primitive (#<XmlType.boolean, "Indeterminate">))
+            -- The `else` arm handles the following cases:
+            --
+            -- If the <AttributeDesignator> or <AttributeSelector> element were to
+            -- evaluate to an empty bag, then the result of the expression SHALL
+            -- be "False".
+            --
+            -- Finally, if all function applications evaluate to "False", then the
+            -- result of the entire expression SHALL be "False".
+            else
+              Value.primitive (#<XmlType.boolean, "False">)
+          -- If an operational error were to occur while evaluating the
+          -- <AttributeDesignator> or <AttributeSelector> element, then the result
+          -- of the entire expression SHALL be "Indeterminate".
+          | Sum.inr status => Option.none
 end Match
 
 namespace AllOf
@@ -723,14 +731,6 @@ namespace PolicySet
           | Decision'.indeterminate_d  => Decision'.indeterminate_d
 end PolicySet
 
-
-inductive StatusCode
-  | ok                : StatusCode
-  | missing_attribute : StatusCode
-  | syntax_error      : StatusCode
-  | processing_error  : StatusCode
-deriving BEq, Repr
-
 structure ResultAuxiliary where
   status      : Option (List StatusCode)
   obligations : List Obligation