Initial attempt at PolicySet evaluation; hitting a wall with nontermination

1 files changed, 53 insertions, 12 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 601887f..2690134 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -290,7 +290,8 @@ namespace PolicyCombinatorAlgorithm
   def eval_permit_overrides := RuleCombinatorAlgorithm.eval_permit_overrides
   def eval_ordered_permit_overrides := RuleCombinatorAlgorithm.eval_ordered_permit_overrides
   def eval_deny_unless_permit := RuleCombinatorAlgorithm.eval_deny_unless_permit
-  def eval_permit_unless_deniy := RuleCombinatorAlgorithm.eval_permit_unless_deny
+  def eval_permit_unless_deny := RuleCombinatorAlgorithm.eval_permit_unless_deny
+  def eval_first_applicable := RuleCombinatorAlgorithm.eval_first_applicable
 
   -- The non-normative part of the specification asserts that "If an error
   -- occurs while evaluating the target or condition of a rule, then the
@@ -634,17 +635,6 @@ namespace Rule
           Decision'.indeterminate_d
 end Rule
 
-structure PolicySet where
-  combinator  : PolicyCombinatorAlgorithm
-  target      : Target
-  children    : List PolicySetChild
-  obligations : List ObligationExpression
-  advice      : List AdviceExpression
-
-inductive PolicySetChild where
-  | policy_set (inner : PolicySet) : PolicySetChild
-  | policy     (inner : Policy)    : PolicySetChild
-
 structure Policy where
   combinator  : RuleCombinatorAlgorithm
   target      : Target
@@ -683,6 +673,57 @@ namespace Policy
           | Decision'.indeterminate_d  => Decision'.indeterminate_d
 end Policy
 
+structure PolicySetMetadata where
+  combinator  : PolicyCombinatorAlgorithm
+  target      : Target
+  -- children    : List PolicySetChild
+  obligations : List ObligationExpression
+  advice      : List AdviceExpression
+
+inductive PolicySetChild where
+  | policy_set (metadata : PolicySetMetadata) (xs : List PolicySetChild) : PolicySetChild
+  | policy     (inner : Policy)    : PolicySetChild
+
+def PolicySet : Type := PolicySetMetadata × (List PolicySetChild)
+
+namespace PolicySet
+  def eval (policyset : PolicySet) (context : Request) : Decision' :=
+    let results := policyset.snd.map
+      (fun child =>
+        match child with
+          | PolicySetChild.policy_set ps xs => PolicySet.eval (ps, xs) context
+          | PolicySetChild.policy     p  => Policy.eval    p  context)
+    let (results : List Decision') := []
+    let combinator :=
+      match policyset.fst.combinator with
+        | PolicyCombinatorAlgorithm.deny_overrides                  => PolicyCombinatorAlgorithm.eval_deny_overrides
+        | PolicyCombinatorAlgorithm.ordered_deny_overrides          => PolicyCombinatorAlgorithm.eval_ordered_deny_overrides
+        | PolicyCombinatorAlgorithm.permit_overrides                => PolicyCombinatorAlgorithm.eval_permit_overrides
+        | PolicyCombinatorAlgorithm.ordered_permit_overrides        => PolicyCombinatorAlgorithm.eval_ordered_permit_overrides
+        | PolicyCombinatorAlgorithm.deny_unless_permit              => PolicyCombinatorAlgorithm.eval_deny_unless_permit
+        | PolicyCombinatorAlgorithm.permit_unless_deny              => PolicyCombinatorAlgorithm.eval_permit_unless_deny
+        | PolicyCombinatorAlgorithm.first_applicable                => PolicyCombinatorAlgorithm.eval_first_applicable
+        | PolicyCombinatorAlgorithm.only_one_applicable             => PolicyCombinatorAlgorithm.eval_only_one_applicable
+        | PolicyCombinatorAlgorithm.legacy_deny_overrides           => PolicyCombinatorAlgorithm.eval_legacy_deny_overrides
+        | PolicyCombinatorAlgorithm.legacy_ordered_deny_overrides   => PolicyCombinatorAlgorithm.eval_legacy_ordered_deny_overrides
+        | PolicyCombinatorAlgorithm.legacy_permit_overrides         => PolicyCombinatorAlgorithm.eval_legacy_permit_overrides
+        | PolicyCombinatorAlgorithm.legacy_ordered_permit_overrides => PolicyCombinatorAlgorithm.eval_legacy_ordered_permit_overrides
+    let decision := combinator results
+    match policyset.fst.target.eval context with
+      | MatchResult.is_match => decision
+      | MatchResult.no_match => Decision'.not_applicable
+      | MatchResult.indeterminate =>
+        match decision with
+          | Decision'.not_applicable   => Decision'.not_applicable
+          | Decision'.permit           => Decision'.indeterminate_p
+          | Decision'.deny             => Decision'.indeterminate_d
+          | Decision'.indeterminate    => Decision'.indeterminate_dp
+          | Decision'.indeterminate_dp => Decision'.indeterminate_dp
+          | Decision'.indeterminate_p  => Decision'.indeterminate_p
+          | Decision'.indeterminate_d  => Decision'.indeterminate_d
+end PolicySet
+
+
 inductive StatusCode
   | ok                : StatusCode
   | missing_attribute : StatusCode