From 7bd1a920de9ee34139bf40b75f2c812e16b2de45 Mon Sep 17 00:00:00 2001
From: Jakob L. Kreuze
Date: Wed, 20 Sep 2023 18:16:10 -0400
Subject: Rule evaluation

---
 xacml-proofs/lean/Xacml.lean | 54 +++++++++++++++++++++++++++++---------------
 1 file changed, 36 insertions(+), 18 deletions(-)

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 8aadefd..9950b1a 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -453,7 +453,6 @@ structure AdviceExpression where
   applies_to : Decision
 deriving BEq, Repr
 
--- n.b. "The <Condition> contains one <Expression> element"
 structure Rule where
   target      : Target
   condition   : Option Expression
@@ -462,23 +461,42 @@ structure Rule where
   advice      : List AdviceExpression
 
 namespace Rule
-  def eval (rule : Rule) (context : Request) : MatchResult :=
-    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">)
-    sorry
+  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
 end Rule
 
 structure PolicySet where
-- 
cgit v1.3