Initial implementation of evaluation functions

1 files changed, 71 insertions, 4 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 7b8697c..2153abe 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -41,7 +41,7 @@ inductive MatchResult where
   | is_match      : MatchResult
   | no_match      : MatchResult
   | indeterminate : MatchResult
-deriving Repr
+deriving BEq, Repr
 
 inductive Decision where
   | permit           : Decision
@@ -399,6 +399,7 @@ def example_4_2_policy :=
 ---
 
 def Choice : Type := List Decision
+deriving BEq
 
 -- TODO
 def evaluate_expression (expression : Expression) : XacmlValue :=
@@ -410,12 +411,51 @@ def evaluate_expression (expression : Expression) : XacmlValue :=
     | Expression.attribute_value inner => inner
     | Expression.function _ => XacmlValue.mk XacmlType.string "True"
 
-def evaluate_target (target : Target) : MatchResult :=
-  MatchResult.no_match
+-- TODO
+def evaluate_designator (designator : AttributeDesignator) (context : Request) : XacmlValue :=
+  XacmlValue.mk XacmlType.string "True"
+  -- match designator with
+    -- | AttributeDesignator.mk category identifier type issuer must_be_present
+    --   match issuer with
+    --     | Option.some x =>
+
+def evaluate_match (m : Match) (context : Request) : XacmlValue :=
+  match m with
+    | Match.mk fn designator value =>
+      evaluate_expression (Expression.apply fn (([evaluate_designator designator context].append value).map (fun x => Expression.attribute_value x)))
+
+def evaluate_all_of (all_of : AllOf) (context : Request) : MatchResult :=
+  let result := all_of.map (fun x => evaluate_match x context)
+  if result.all (fun x => x == (XacmlType.boolean, "True")) then MatchResult.is_match
+  else if result.all (fun x => x != (XacmlType.boolean, "False")) ∧
+          result.elem (XacmlType.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_rule (rule : Rule) (context : Request) : Choice :=
   if rule.target == [] then [rule.effect]
-  else match evaluate_target rule.target with
+  else match evaluate_target rule.target context with
     | MatchResult.is_match =>
       match evaluate_expression rule.condition with
         -- TODO: coe to some strongly typed result?
@@ -428,9 +468,36 @@ def evaluate_rule (rule : Rule) (context : Request) : Choice :=
     | MatchResult.no_match      => [Decision.not_applicable]
     | MatchResult.indeterminate => [Decision.not_applicable]
 
+theorem test :
+  ∀ r: Rule,
+  ∀ c: Request,
+    evaluate_target r.target c = MatchResult.is_match
+  ∧ evaluate_expression r.condition = XacmlValue.mk XacmlType.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 = (XacmlType.string, "True") := And.right h
+      simp [h_target_eval]
+      simp [h_condition_eval] }
+    { simp }
+
 def evaluate_policy (policy : Policy) (context : Request) : Choice :=
   match policy.rules with
     | [rule₁] => evaluate_rule rule₁ context
     | _ => []
 
+def evaluate_deny_overrides (results : List Decision) : Decision :=
+  if results.elem Decision.deny then Decision.deny else
+  if results.elem  Decision.indeterminate_dp then Decision.indeterminate_dp else
+  if results.elem Decision.indeterminate_d ∧ results.elem Decision.indeterminate_p then Decision.indeterminate_dp else
+  if results.elem  Decision.indeterminate_d then Decision.indeterminate_d else
+  if results.elem Decision.permit then Decision.permit else
+  if results.elem Decision.indeterminate_p then Decision.indeterminate_p else
+  Decision.not_applicable
+
 #eval evaluate_policy example_4_1_policy example_4_1_request