Use explicit tree structure to represent policy tree

1 files changed, 33 insertions, 25 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 5a2f536..3452e0e 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -127,9 +127,6 @@ structure Bag where
   contents: List Primitive
 deriving Repr
 
-def List.count [BEq α] (xs : List α) (x : α) : Int :=
-  (xs.filter (fun y => y == x)).length
-
 def Bag.beq (b₁ b₂ : Bag) : Bool :=
   b₁.contents.all (fun x => b₂.contents.count x == b₁.contents.count x)
 
@@ -646,13 +643,11 @@ end Rule
 structure Policy where
   combinator  : RuleCombinatorAlgorithm
   target      : Target
-  rules       : List Rule
   obligations : List ObligationExpression
   advice      : List AdviceExpression
 
 namespace Policy
-  def eval (policy : Policy) (context : Request) : Decision' :=
-    let results := policy.rules.map (fun rule => rule.eval context)
+  def eval (policy : Policy) (child_results : List Decision') (context : Request) : Decision' :=
     let combinator :=
       match policy.combinator with
         | RuleCombinatorAlgorithm.deny_overrides                  => RuleCombinatorAlgorithm.eval_deny_overrides
@@ -666,7 +661,7 @@ namespace Policy
         | RuleCombinatorAlgorithm.legacy_ordered_deny_overrides   => RuleCombinatorAlgorithm.eval_legacy_ordered_deny_overrides
         | RuleCombinatorAlgorithm.legacy_permit_overrides         => RuleCombinatorAlgorithm.eval_legacy_permit_overrides
         | RuleCombinatorAlgorithm.legacy_ordered_permit_overrides => RuleCombinatorAlgorithm.eval_legacy_ordered_permit_overrides
-    let decision := combinator results
+    let decision := combinator child_results
     match policy.target.eval context with
       | MatchResult.is_match => decision
       | MatchResult.no_match => Decision'.not_applicable
@@ -681,29 +676,16 @@ namespace Policy
           | Decision'.indeterminate_d  => Decision'.indeterminate_d
 end Policy
 
-structure PolicySetMetadata where
+structure PolicySet 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') := []
+  def eval (policyset : PolicySet) (child_results : List Decision') (context : Request) : Decision' :=
     let combinator :=
-      match policyset.fst.combinator with
+      match policyset.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
@@ -716,8 +698,8 @@ namespace PolicySet
         | 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
+    let decision := combinator child_results
+    match policyset.target.eval context with
       | MatchResult.is_match => decision
       | MatchResult.no_match => Decision'.not_applicable
       | MatchResult.indeterminate =>
@@ -731,6 +713,32 @@ namespace PolicySet
           | Decision'.indeterminate_d  => Decision'.indeterminate_d
 end PolicySet
 
+inductive PolicyElement where
+  | PolicySet (ps : PolicySet)
+  | Policy    (p : Policy)
+  | Rule      (r : Rule)
+
+def PolicyElement.eval (context : Request) : PolicyElement -> List Decision' -> Decision'
+  | PolicySet ps, results => ps.eval results context
+  | Policy p, results => p.eval results context
+  | Rule r, _ => r.eval context
+
+inductive ElementTree where
+  | Node (e : PolicyElement) (xs : List ElementTree)
+
+def ElementTree.eval' (context : Request) : ElementTree -> List Decision' -> Decision'
+  | ElementTree.Node e [], results => PolicyElement.eval context e results
+  | ElementTree.Node e (x :: xs), results =>
+      ElementTree.eval'
+        context
+        (ElementTree.Node e xs)
+        ((ElementTree.eval' context x []) :: results)
+
+def ElementTree.eval (context : Request) (et : ElementTree) : Decision' :=
+  ElementTree.eval' context et []
+
+-- let results := policy.rules.map (fun rule => rule.eval context)
+
 structure ResultAuxiliary where
   status      : Option (List StatusCode)
   obligations : List Obligation