Implement advice/obligation combining

1 files changed, 198 insertions, 80 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 3452e0e..f904da7 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -171,7 +171,7 @@ structure Attribute where
   identifier : String
   issuer     : Option String
   value      : Primitive
-deriving Repr
+deriving BEq, Repr
 
 -- More than one attribute with a particular (category, identifier, issuer) can
 -- exist in a `Request`. Indeed, this is how poly-valued attributes are
@@ -559,19 +559,13 @@ namespace Target
         else MatchResult.indeterminate
 end Target
 
-structure AttributeAssignment where
-  category        : String
-  identifier      : String
-  issuer          : Option String
-deriving BEq, Repr
-
 structure Obligation where
-  assignments : List AttributeAssignment
+  assignments : List Attribute
   identifier : String
 deriving BEq, Repr
 
 structure Advice where
-  assignments : List AttributeAssignment
+  assignments : List Attribute
   identifier : String
 deriving BEq, Repr
 
@@ -582,18 +576,92 @@ structure AttributeAssignmentExpression where
   expression      : Expression
 deriving BEq, Repr
 
+namespace AttributeAssignmentExpression
+  def eval (assignment : AttributeAssignmentExpression) (context : Request) : Option Attribute :=
+    match assignment.expression.eval context with
+      | some (Value.primitive inner) =>
+          Attribute.mk
+            assignment.category
+            assignment.identifier
+            assignment.issuer
+            inner
+      | _ => none
+end AttributeAssignmentExpression
+
 structure ObligationExpression where
   assignments : List AttributeAssignmentExpression
   identifier : String
   fulfill_on : Decision
 deriving BEq, Repr
 
+namespace ObligationExpression
+  def eval (obligation : ObligationExpression) (context : Request) : Option Obligation :=
+    let assignments := obligation.assignments.map (fun x => AttributeAssignmentExpression.eval x context)
+    if assignments.all Option.isSome then
+      Obligation.mk
+        (List.filterMap id assignments)
+        obligation.identifier
+    else none
+end ObligationExpression
+
 structure AdviceExpression where
   assignments : List AttributeAssignmentExpression
   identifier : String
   applies_to : Decision
 deriving BEq, Repr
 
+namespace AdviceExpression
+  def eval (advice : AdviceExpression) (context : Request) : Option Advice :=
+    let assignments := advice.assignments.map (fun x => AttributeAssignmentExpression.eval x context)
+    if assignments.all Option.isSome then
+      Advice.mk
+        (List.filterMap id assignments)
+        advice.identifier
+    else none
+end AdviceExpression
+
+structure ResultAuxiliary where
+  status      : Option (List StatusCode)
+  obligations : List Obligation
+  advice      : List Advice
+deriving BEq, Repr
+
+structure ResultAuxiliary' where
+  status      : Option (List StatusCode)
+  obligations : List ObligationExpression
+  advice      : List AdviceExpression
+deriving BEq, Repr
+
+structure MissingAttributeDetail where
+  category   : String
+  identifier : String
+  issuer     : Option String
+  value      : Option Value
+  type       : XmlType
+deriving BEq, Repr
+
+def Result : Type := Decision' × (Option ResultAuxiliary)
+def Result' : Type := Decision' × (Option ResultAuxiliary')
+
+namespace Result'
+  def eval (result : Result') (context : Request) : Result :=
+    match result.snd with
+    | some aux =>
+      let advices := aux.advice.map (fun advice => AdviceExpression.eval advice context)
+      let obligations := aux.obligations.map (fun x => ObligationExpression.eval x context)
+      if advices.any Option.isNone || obligations.any Option.isNone then
+         (Decision'.indeterminate, none)
+      else
+        (
+          result.fst,
+          ResultAuxiliary.mk
+            aux.status
+            (List.filterMap id obligations)
+            (List.filterMap id advices)
+        )
+    | none => (result.fst, none)
+end Result'
+
 structure Rule where
   target      : Target
   condition   : Option Expression
@@ -602,42 +670,56 @@ structure Rule where
   advice      : List AdviceExpression
 
 namespace Rule
-  def eval (rule : Rule) (context : Request) : Decision' :=
-    -- The "no target" case is handled within `Target.eval`, returning
-    -- `MatchResult.is_match` when the target is empty.
-    match rule.target.eval context with
-      | MatchResult.is_match =>
-        let condition :=
-          match rule.condition with
-            | some condition =>
-              -- The condition value SHALL be "True" if the <Condition> element
-              -- evaluates to "True".
-              let result := condition.eval context
-              if result == some (Value.primitive (#<XmlType.boolean, "True">)) then result
-              -- Its value SHALL be "False" if the <Condition> element evaluates to
-              -- "False".
-              else if result == some (Value.primitive (#<XmlType.boolean, "False">)) then result
-              -- The condition value SHALL be "Indeterminate", if the expression
-              -- contained in the <Condition> element evaluates to "Indeterminate."
-              else Value.primitive (#<XmlType.boolean, "Indeterminate">)
-            -- The condition value SHALL be "True" if the <Condition> element is absent.
-            | none => Value.primitive (#<XmlType.boolean, "True">)
-        match condition with
-          | some (Value.primitive (XmlType.boolean, "False")) => Decision'.not_applicable
-          | some (Value.primitive (XmlType.boolean, "True")) =>
-            match rule.effect with
-              | EffectType.permit => Decision'.permit
-              | EffectType.deny   => Decision'.deny
-          -- | (#<XmlType.boolean, "Indeterminate">) =>
-          | _ =>
-            if rule.effect == EffectType.permit then
-              Decision'.indeterminate_p else
-              Decision'.indeterminate_d
-      | MatchResult.no_match => Decision'.not_applicable
-      | MatchResult.indeterminate =>
-        if rule.effect == EffectType.permit then
-          Decision'.indeterminate_p else
-          Decision'.indeterminate_d
+  def eval (rule : Rule) (context : Request) : Result' :=
+    let (decision : Decision') :=
+      -- The "no target" case is handled within `Target.eval`, returning
+      -- `MatchResult.is_match` when the target is empty.
+      match rule.target.eval context with
+        | MatchResult.is_match =>
+          let condition :=
+            match rule.condition with
+              | some condition =>
+                -- The condition value SHALL be "True" if the <Condition> element
+                -- evaluates to "True".
+                let result := condition.eval context
+                if result == some (Value.primitive (#<XmlType.boolean, "True">)) then result
+                -- Its value SHALL be "False" if the <Condition> element evaluates to
+                -- "False".
+                else if result == some (Value.primitive (#<XmlType.boolean, "False">)) then result
+                -- The condition value SHALL be "Indeterminate", if the expression
+                -- contained in the <Condition> element evaluates to "Indeterminate."
+                else Value.primitive (#<XmlType.boolean, "Indeterminate">)
+              -- The condition value SHALL be "True" if the <Condition> element is absent.
+              | none => Value.primitive (#<XmlType.boolean, "True">)
+          match condition with
+            | some (Value.primitive (XmlType.boolean, "False")) => Decision'.not_applicable
+            | some (Value.primitive (XmlType.boolean, "True")) =>
+              match rule.effect with
+                | EffectType.permit => Decision'.permit
+                | EffectType.deny   => Decision'.deny
+            -- | (#<XmlType.boolean, "Indeterminate">) =>
+            | _ =>
+              if rule.effect == EffectType.permit then
+                Decision'.indeterminate_p else
+                Decision'.indeterminate_d
+        | MatchResult.no_match => Decision'.not_applicable
+        | MatchResult.indeterminate =>
+          if rule.effect == EffectType.permit then
+            Decision'.indeterminate_p else
+            Decision'.indeterminate_d
+    let advices :=
+      rule.advice.filter
+        (fun advice => advice.applies_to == (decision : Decision))
+    let obligations :=
+      rule.obligations.filter
+        (fun obligation => obligation.fulfill_on == (decision : Decision))
+    (
+      decision,
+      ResultAuxiliary'.mk
+        none
+        obligations
+        advices
+    )
 end Rule
 
 structure Policy where
@@ -647,7 +729,7 @@ structure Policy where
   advice      : List AdviceExpression
 
 namespace Policy
-  def eval (policy : Policy) (child_results : List Decision') (context : Request) : Decision' :=
+  def eval (policy : Policy) (child_results : List Result') (context : Request) : Result' :=
     let combinator :=
       match policy.combinator with
         | RuleCombinatorAlgorithm.deny_overrides                  => RuleCombinatorAlgorithm.eval_deny_overrides
@@ -661,19 +743,45 @@ 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 child_results
-    match policy.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
+    let (decision : Decision') := combinator (List.map Prod.fst child_results)
+    let (decision : Decision') :=
+      match policy.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
+    let advices :=
+      policy.advice.filter
+        (fun advice => advice.applies_to == (decision : Decision))
+      ++
+      List.join
+        (child_results.filterMap
+          (fun x => match x.snd with
+                      | some y => y.advice
+                      | none => none))
+    let obligations :=
+      policy.obligations.filter
+        (fun obligation => obligation.fulfill_on == (decision : Decision))
+      ++
+      List.join
+        (child_results.filterMap
+          (fun x => match x.snd with
+                      | some y => y.obligations
+                      | none => none))
+    (
+      decision,
+      ResultAuxiliary'.mk
+        none
+        obligations
+        advices
+    )
 end Policy
 
 structure PolicySet where
@@ -683,7 +791,7 @@ structure PolicySet where
   advice      : List AdviceExpression
 
 namespace PolicySet
-  def eval (policyset : PolicySet) (child_results : List Decision') (context : Request) : Decision' :=
+  def eval (policyset : PolicySet) (child_results : List Result') (context : Request) : Result' :=
     let combinator :=
       match policyset.combinator with
         | PolicyCombinatorAlgorithm.deny_overrides                  => PolicyCombinatorAlgorithm.eval_deny_overrides
@@ -698,7 +806,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 child_results
+    let (decision : Decision') := combinator (List.map Prod.fst child_results)
+    let (decision : Decision') :=
     match policyset.target.eval context with
       | MatchResult.is_match => decision
       | MatchResult.no_match => Decision'.not_applicable
@@ -711,6 +820,31 @@ namespace PolicySet
           | Decision'.indeterminate_dp => Decision'.indeterminate_dp
           | Decision'.indeterminate_p  => Decision'.indeterminate_p
           | Decision'.indeterminate_d  => Decision'.indeterminate_d
+    let advices :=
+      policyset.advice.filter
+        (fun advice => advice.applies_to == (decision : Decision))
+      ++
+      List.join
+        (child_results.filterMap
+          (fun x => match x.snd with
+                      | some y => y.advice
+                      | none => none))
+    let obligations :=
+      policyset.obligations.filter
+        (fun obligation => obligation.fulfill_on == (decision : Decision))
+      ++
+      List.join
+        (child_results.filterMap
+          (fun x => match x.snd with
+                      | some y => y.obligations
+                      | none => none))
+    (
+      decision,
+      ResultAuxiliary'.mk
+        none
+        obligations
+        advices
+    )
 end PolicySet
 
 inductive PolicyElement where
@@ -718,7 +852,7 @@ inductive PolicyElement where
   | Policy    (p : Policy)
   | Rule      (r : Rule)
 
-def PolicyElement.eval (context : Request) : PolicyElement -> List Decision' -> Decision'
+def PolicyElement.eval (context : Request) : PolicyElement -> List Result' -> Result'
   | PolicySet ps, results => ps.eval results context
   | Policy p, results => p.eval results context
   | Rule r, _ => r.eval context
@@ -726,7 +860,7 @@ def PolicyElement.eval (context : Request) : PolicyElement -> List Decision' ->
 inductive ElementTree where
   | Node (e : PolicyElement) (xs : List ElementTree)
 
-def ElementTree.eval' (context : Request) : ElementTree -> List Decision' -> Decision'
+def ElementTree.eval' (context : Request) : ElementTree -> List Result' -> Result'
   | ElementTree.Node e [], results => PolicyElement.eval context e results
   | ElementTree.Node e (x :: xs), results =>
       ElementTree.eval'
@@ -734,27 +868,11 @@ def ElementTree.eval' (context : Request) : ElementTree -> List Decision' -> Dec
         (ElementTree.Node e xs)
         ((ElementTree.eval' context x []) :: results)
 
-def ElementTree.eval (context : Request) (et : ElementTree) : Decision' :=
+def ElementTree.eval (context : Request) (et : ElementTree) : Result' :=
   ElementTree.eval' context et []
 
 -- let results := policy.rules.map (fun rule => rule.eval context)
 
-structure ResultAuxiliary where
-  status      : Option (List StatusCode)
-  obligations : List Obligation
-  advice      : List Advice
-deriving BEq, Repr
-
-structure MissingAttributeDetail where
-  category   : String
-  identifier : String
-  issuer     : Option String
-  value      : Option Value
-  type       : XmlType
-deriving BEq, Repr
-
-def Result : Type := Decision × (Option ResultAuxiliary)
-
 def is_indeterminate (x : Expression) : Bool :=
   match x with
   | Expression.attribute_value (Value.primitive (XmlType.boolean, "Indeterminate")) => true