Evaluate AllOf/AnyOf according to § 7.7

1 files changed, 38 insertions, 143 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 15a5d4b..c35499a 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -14,19 +14,6 @@ inductive MatchResult where
   | indeterminate : MatchResult
 deriving BEq, Repr
 
-def MatchResult.or : MatchResult -> MatchResult -> MatchResult
-  | MatchResult.indeterminate , _                         => MatchResult.indeterminate
-  | _                         , MatchResult.indeterminate => MatchResult.indeterminate
-  | MatchResult.is_match      , _                         => MatchResult.is_match
-  | _                         , MatchResult.is_match      => MatchResult.is_match
-  | MatchResult.no_match      , MatchResult.no_match      => MatchResult.no_match
-
-def MatchResult.and : MatchResult -> MatchResult -> MatchResult
-  | MatchResult.indeterminate , _                         => MatchResult.indeterminate
-  | _                         , MatchResult.indeterminate => MatchResult.indeterminate
-  | MatchResult.is_match      , MatchResult.is_match      => MatchResult.is_match
-  | _                         , _                         => MatchResult.no_match
-
 inductive Decision where
   | permit           : Decision
   | deny             : Decision
@@ -414,6 +401,26 @@ def Target : Type := List AnyOf
 deriving BEq, Repr
 
 namespace Match
+  -- The evaluation semantics for a matching element is as follows.
+  --
+  -- 1. If an operational error were to occur while evaluating the
+  --    <AttributeDesignator> or <AttributeSelector> element, then the
+  --    result of the entire expression SHALL be "Indeterminate".
+  --
+  -- 2. If the <AttributeDesignator> or <AttributeSelector> element were
+  --    to evaluate to an empty bag, then the result of the expression
+  --    SHALL be "False".
+  --
+  -- 3. Otherwise, the MatchId function SHALL be applied between the
+  --    <AttributeValue> and each element of the bag returned from the
+  --    <AttributeDesignator> or <AttributeSelector> element.
+  --    a. If at least one of those function applications were to evaluate
+  --       to "True", then the result of the entire expression SHALL be
+  --       "True".
+  --    b. Otherwise, if at least one of the function applications results
+  --       in "Indeterminate", then the result SHALL be "Indeterminate".
+  --    c. Finally, if all function applications evaluate to "False", then
+  --       the result of the entire expression SHALL be "False".
   def eval (m : Match) (context : Request) : Option Value :=
     match m with
       | Match.mk fn designator value =>
@@ -460,19 +467,28 @@ namespace Match
 end Match
 
 namespace AllOf
-  -- There is no section specifying the semantics of `AllOf`.
   def eval (conj : AllOf) (context : Request) : MatchResult :=
-    (conj.map (fun m => m.eval context)).foldl
-      MatchResult.and
-      MatchResult.no_match
-end AllOf
+    let result := conj.map (fun x => x.eval context)
+    let result := result.map (fun (x : Option Value) => (x : Value))
+    if result.all (fun x => x == Value.primitive (XmlType.boolean, "True")) then MatchResult.is_match
+    else if result.all (fun x => x != Value.primitive (XmlType.boolean, "False")) ∧
+            result.elem (Value.primitive (XmlType.boolean, "Indeterminate"))
+         then MatchResult.indeterminate
+    else MatchResult.no_match
+  end AllOf
 
 namespace AnyOf
-  -- There is no section specifying the semantics of `AnyOf`.
   def eval (disj : AnyOf) (context : Request) : MatchResult :=
-    (disj.map (fun conj => conj.eval context)).foldl
-      MatchResult.or
-      MatchResult.is_match
+  match disj with
+    | [] => MatchResult.is_match
+    | List.cons x xs => match x.eval context with
+      | MatchResult.is_match => MatchResult.is_match
+      | MatchResult.no_match =>
+        let rest := AnyOf.eval xs context
+        if rest == MatchResult.is_match then MatchResult.no_match else rest
+      | MatchResult.indeterminate =>
+        let rest := AnyOf.eval xs context
+        if rest == MatchResult.no_match then MatchResult.indeterminate else rest
 end AnyOf
 
 namespace Target
@@ -699,124 +715,3 @@ def combine_response_aux (x y : ResultAuxiliary) : ResultAuxiliary :=
 
 def Choice : Type := List (Decision × ResultAuxiliary)
 deriving BEq, Repr
-
----
--- The evaluation semantics for a matching element is as follows.
---
--- 1. If an operational error were to occur while evaluating the
---    <AttributeDesignator> or <AttributeSelector> element, then the
---    result of the entire expression SHALL be "Indeterminate".
---
--- 2. If the <AttributeDesignator> or <AttributeSelector> element were
---    to evaluate to an empty bag, then the result of the expression
---    SHALL be "False".
---
--- 3. Otherwise, the MatchId function SHALL be applied between the
---    <AttributeValue> and each element of the bag returned from the
---    <AttributeDesignator> or <AttributeSelector> element.
---    a. If at least one of those function applications were to evaluate
---       to "True", then the result of the entire expression SHALL be
---       "True".
---    b. Otherwise, if at least one of the function applications results
---       in "Indeterminate", then the result SHALL be "Indeterminate".
---    c. Finally, if all function applications evaluate to "False", then
---       the result of the entire expression SHALL be "False".
-
--- def evaluate_all_of (all_of : AllOf) (context : Request) : MatchResult :=
---   let result := all_of.map (fun x => x.eval context)
---   let result := result.map (fun (x : Option Value) => (x : Value))
---   if result.all (fun x => x == (XmlType.boolean, "True")) then MatchResult.is_match
---   else if result.all (fun x => x != (XmlType.boolean, "False")) ∧
---           result.elem (XmlType.boolean, "Indeterminate") then MatchResult.indeterminate
---   else MatchResult.no_match
-
--- def evaluate_any_of (any_of : AnyOf) (context : Request) : MatchResult :=
---   match any_of with
---     | [] => MatchResult.is_match
---     | List.cons x xs => match evaluate_all_of x context with
---       | MatchResult.is_match => MatchResult.is_match
---       | MatchResult.no_match =>
---         let rest := evaluate_any_of xs context
---         if rest == MatchResult.is_match then MatchResult.no_match else rest
---       | MatchResult.indeterminate =>
---         let rest := evaluate_any_of xs context
---         if rest == MatchResult.no_match then MatchResult.indeterminate else rest
-
--- def evaluate_target (target : Target) (context : Request) : MatchResult :=
---   match target with
---     | [] => MatchResult.is_match
---     | List.cons x xs => match evaluate_any_of x context with
---       | MatchResult.is_match => evaluate_target xs context
---       | MatchResult.no_match => MatchResult.no_match
---       | MatchResult.indeterminate =>
---         let rest := evaluate_target xs context
---         if rest == MatchResult.no_match then rest else MatchResult.indeterminate
-
--- def evaluate_assignments (assignments : List AttributeAssignmentExpression) : List AttributeAssignment :=
---   assignments.map (fun assignment =>
---                        match assignment with
---                        | AttributeAssignmentExpression.mk category identifier issuer _ =>
---                          AttributeAssignment.mk category identifier issuer)
-
-
--- def evaluate_rule (rule : Rule) (context : Request) : Decision' × ResultAuxiliary :=
---   let decision :=
---     if rule.target == [] then (rule.effect).to_decision'
---     else match evaluate_target rule.target context with
---       | MatchResult.is_match =>
---         match ((rule.condition).eval context : Value) with
---           | (XmlType.string, "True") => (rule.effect).to_decision'
---           | (XmlType.string, "False") => Decision'.not_applicable
---           | (_, _) =>
---             if (rule.effect).to_decision' == Decision'.permit then
---               Decision'.indeterminate_p else
---               Decision'.indeterminate_d
---       | MatchResult.no_match      => Decision'.not_applicable
---       | MatchResult.indeterminate => Decision'.not_applicable
---   let obligations := rule.obligations.filter (fun obl => obl.fulfill_on == (decision : Decision))
---   let advice      := rule.advice.filter      (fun obl => obl.applies_to == (decision : Decision))
---   (
---     decision,
---     ResultAuxiliary.mk
---       Option.none
---       (obligations.map (fun expr => Obligation.mk
---                                       (evaluate_assignments expr.assignments)
---                                       expr.identifier))
---       (advice.map      (fun expr => Advice.mk
---                                       (evaluate_assignments expr.assignments)
---                                       expr.identifier)))
-
--- theorem test :
---   ∀ (r : Rule) (c : Request),
---     evaluate_target r.target c = MatchResult.is_match
---   ∧ evaluate_expression r.condition = #<XmlType.string, "True">
---   → evaluate_rule r c = [r.effect] :=
---   by
---     intros r c
---     intro h
---     rw [evaluate_rule]
---     cases (r.target == [])
---     { simp
---       have h_target_eval : evaluate_target r.target c = MatchResult.is_match := And.left h
---       have h_condition_eval : (evaluate_expression r.condition : Value) = (XmlType.string, "True") := And.right h
---       simp [h_target_eval]
---       simp [h_condition_eval] }
---     { simp }
-
--- def evaluate_policy (policy : Policy) (context : Request) : Choice :=
---   let results     := policy.rules.map (fun x => evaluate_rule x context)
---   let decision    := evaluate_deny_overrides (results.map Prod.fst)
---   let obligations := policy.obligations.filter (fun obl => obl.fulfill_on == (decision : Decision))
---   let advice      := policy.advice.filter      (fun obl => obl.applies_to == (decision : Decision))
---   -- TODO: How do we combine advice/obligations?
---   [(
---     decision,
---     ResultAuxiliary.mk
---       Option.none
---       (obligations.map (fun expr => Obligation.mk
---                                       (evaluate_assignments expr.assignments)
---                                       expr.identifier))
---       (advice.map      (fun expr => Advice.mk
---                                       (evaluate_assignments expr.assignments)
---                                       expr.identifier))
---   )]