Target/Match semantics

1 files changed, 80 insertions, 3 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 8464aa0..8a7a40e 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -14,6 +14,19 @@ 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
@@ -147,6 +160,13 @@ instance : Coe (Option Value) Value where
       | Option.none   => Value.primitive (#<XmlType.boolean, "Indeterminate">)
       | Option.some a => a
 
+instance : Coe (Option Value) MatchResult where
+  coe b :=
+    match b with
+      | Option.some (Value.primitive (XmlType.boolean, "True"))          => MatchResult.is_match
+      | Option.some (Value.primitive (XmlType.boolean, "False"))         => MatchResult.no_match
+      | _                                                                => MatchResult.indeterminate
+
 ------------------------------------------------------------------------
 ---- Attributes---------------------------------------------------------
 ------------------------------------------------------------------------
@@ -324,23 +344,80 @@ namespace Match
         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 =>
+            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]
 
           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">))
-          else Value.primitive (#<XmlType.boolean, "False">)
+          -- 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.
 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
+
+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
+end AnyOf
+
+namespace Target
+  def eval (target : Target) (context : Request) : MatchResult :=
+    match target with
+      -- An empty target matches any request.
+      | [] => MatchResult.is_match
+      | xs =>
+        let results := xs.map (fun disj => disj.eval context)
+        -- Otherwise the target value SHALL be "Match" if all the AnyOf
+        -- specified in the target match values in the request context.
+        if results.all (fun result => result == MatchResult.is_match) then
+          MatchResult.is_match
+        -- Otherwise, if any one of the AnyOf specified in the target is “No
+        -- Match”, then the target SHALL be “No Match”.
+        else if results.any (fun result => result == MatchResult.no_match) then
+          MatchResult.no_match
+        -- Otherwise, the target SHALL be “Indeterminate”.
+        else MatchResult.indeterminate
+end Target
+
 structure AttributeAssignment where
   category        : String
   identifier      : String