Initial evaluation for obligation/advice

1 files changed, 38 insertions, 25 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 723fece..2801567 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -157,7 +157,12 @@ deriving BEq, Repr
 structure ObligationExpression where
   assignments : List AttributeAssignmentExpression
   identifier : String
-  fullfill_on : Decision
+  fulfill_on : Decision
+deriving BEq, Repr
+
+structure Obligation where
+  assignments : List AttributeAssignmentExpression
+  identifier : String
 deriving BEq, Repr
 
 structure AdviceExpression where
@@ -166,6 +171,11 @@ structure AdviceExpression where
   applies_to : Decision
 deriving BEq, Repr
 
+structure Advice where
+  assignments : List AttributeAssignmentExpression
+  identifier : String
+deriving BEq, Repr
+
 -- n.b. "The <Condition> contains one <Expression> element"
 structure Rule where
   target      : Target
@@ -192,19 +202,13 @@ structure Policy where
   obligations : List ObligationExpression
   advice      : List AdviceExpression
 
-def Obligation : Type := String
-deriving BEq, Repr
-def Advice     : Type := String
-deriving BEq, Repr
-
-structure Response where
-  decision    : Decision
+structure ResponseAuxiliary where
   status      : Option String
   obligations : List Obligation
   advice      : List Advice
 deriving BEq, Repr
 
-def Choice : Type := List Decision
+def Choice : Type := List (Decision × ResponseAuxiliary)
 deriving BEq, Repr
 
 ---
@@ -232,7 +236,7 @@ def example_4_1_policy :=
       (Expression.attribute_value (#<XmlType.boolean, "True">))
       Decision.permit
       [] []]
-      [] []
+    [] []
 
 def example_4_1_request :=
   [Attribute.mk "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
@@ -620,20 +624,29 @@ def evaluate_target (target : Target) (context : Request) : MatchResult :=
         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 context with
-    | MatchResult.is_match =>
-      match (evaluate_expression rule.condition : Value) with
-        -- TODO: coe to some strongly typed result?
-        | (XmlType.string, "True") => [rule.effect]
-        | (XmlType.string, "False") => [Decision.not_applicable]
-        | (_, _) =>
-          if rule.effect == Decision.permit then
-            [Decision.indeterminate_p] else
-            [Decision.indeterminate_d]
-    | MatchResult.no_match      => [Decision.not_applicable]
-    | MatchResult.indeterminate => [Decision.not_applicable]
+def evaluate_rule (rule : Rule) (context : Request) : Decision × ResponseAuxiliary :=
+  let decision :=
+    if rule.target == [] then rule.effect
+    else match evaluate_target rule.target context with
+      | MatchResult.is_match =>
+        match (evaluate_expression rule.condition : Value) with
+          | (XmlType.string, "True") => rule.effect
+          | (XmlType.string, "False") => Decision.not_applicable
+          | (_, _) =>
+            if rule.effect == Decision.permit then
+              Decision.indeterminate_p else
+              Decision.indeterminate_d
+      | MatchResult.no_match      => Decision.not_applicable
+      | MatchResult.indeterminate => Decision.not_applicable
+  let obligations := rule.obligations.filter (fun obl => obl.fulfill_on == decision)
+  let advice      := rule.advice.filter      (fun obl => obl.applies_to == decision)
+  (
+    decision,
+    ResponseAuxiliary.mk
+      Option.none
+      (obligations.map (fun expr => Obligation.mk expr.assignments expr.identifier))
+      (advice.map      (fun expr => Advice.mk     expr.assignments expr.identifier))
+  )
 
 -- theorem test :
 --   ∀ (r : Rule) (c : Request),
@@ -654,7 +667,7 @@ def evaluate_rule (rule : Rule) (context : Request) : Choice :=
 
 def evaluate_policy (policy : Policy) (context : Request) : Choice :=
   match policy.rules with
-    | [rule₁] => evaluate_rule rule₁ context
+    | [rule₁] => [evaluate_rule rule₁ context]
     | _ => []
 
 def evaluate_deny_overrides (results : List Decision) : Decision :=