Distinguish between rule/policy combinators

1 files changed, 83 insertions, 41 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index c35499a..601887f 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -188,21 +188,20 @@ deriving Repr
 def Identifier : Type := String
 deriving BEq, Repr
 
-inductive CombinatorAlgorithm where
-  | deny_overrides                  : CombinatorAlgorithm
-  | ordered_deny_overrides          : CombinatorAlgorithm
-  | permit_overrides                : CombinatorAlgorithm
-  | ordered_permit_overrides        : CombinatorAlgorithm
-  | deny_unless_permit              : CombinatorAlgorithm
-  | permit_unless_deny              : CombinatorAlgorithm
-  | first_applicable                : CombinatorAlgorithm
-  | only_one_applicable             : CombinatorAlgorithm
-  | legacy_deny_overrides           : CombinatorAlgorithm
-  | legacy_ordered_deny_overrides   : CombinatorAlgorithm
-  | legacy_permit_overrides         : CombinatorAlgorithm
-  | legacy_ordered_permit_overrides : CombinatorAlgorithm
+inductive RuleCombinatorAlgorithm where
+  | deny_overrides                  : RuleCombinatorAlgorithm
+  | ordered_deny_overrides          : RuleCombinatorAlgorithm
+  | permit_overrides                : RuleCombinatorAlgorithm
+  | ordered_permit_overrides        : RuleCombinatorAlgorithm
+  | deny_unless_permit              : RuleCombinatorAlgorithm
+  | permit_unless_deny              : RuleCombinatorAlgorithm
+  | first_applicable                : RuleCombinatorAlgorithm
+  | legacy_deny_overrides           : RuleCombinatorAlgorithm
+  | legacy_ordered_deny_overrides   : RuleCombinatorAlgorithm
+  | legacy_permit_overrides         : RuleCombinatorAlgorithm
+  | legacy_ordered_permit_overrides : RuleCombinatorAlgorithm
 
-namespace CombinatorAlgorithm
+namespace RuleCombinatorAlgorithm
   -- The output of a combining algorithm which does not track the extended set
   -- of “Indeterminate” values MUST be treated as “Indeterminate{DP}” for the
   -- value “Indeterminate” by a combining algorithm which tracks the extended
@@ -245,19 +244,12 @@ namespace CombinatorAlgorithm
   --
   -- This behavior isn't spelled out in the normative part, because errors are
   -- represented as an Indeterminate.
-  def eval_first_applicable_rule (results : List Decision') : Decision' :=
+  def eval_first_applicable (results : List Decision') : Decision' :=
     match (results.filter (fun d => d != Decision'.not_applicable)).get? 0 with
       | some a => a
       | none => Decision'.not_applicable
 
-  -- See the comment for `eval_first_applicable_rule`.
-  def eval_only_one_applicable (results : List Decision') : Decision' :=
-    match results.filter (fun d => d != Decision'.not_applicable) with
-      | []  => Decision'.not_applicable
-      | [a] => a
-      | _   => Decision'.indeterminate
-
-  def eval_legacy_deny_overrides_rule (results : List Decision') : Decision' :=
+  def eval_legacy_deny_overrides (results : List Decision') : Decision' :=
     -- Note that "any rule having Effect=Deny evaluates to Indeterminate"
     -- corresponds to indeterminate_d, and "any rule having Effect=Permit
     -- evaluates to Indeterminate" corresponds to indeterminate_p.
@@ -266,17 +258,68 @@ namespace CombinatorAlgorithm
     if results.elem Decision'.permit then Decision'.permit else
     if results.elem Decision'.indeterminate_p then Decision'.indeterminate else
     Decision'.not_applicable
-  def eval_legacy_ordered_deny_overrides_rule : List Decision' -> Decision' := eval_legacy_deny_overrides_rule
+  def eval_legacy_ordered_deny_overrides : List Decision' -> Decision' := eval_legacy_deny_overrides
 
   -- See the comment for `eval_legacy_deny_overrides_rule`.
-  def eval_legacy_permit_overrides_rule (results : List Decision') : Decision' :=
+  def eval_legacy_permit_overrides (results : List Decision') : Decision' :=
     if results.elem Decision'.permit then Decision'.permit else
     if results.elem Decision'.indeterminate_p then Decision'.indeterminate else
     if results.elem Decision'.deny then Decision'.deny else
     if results.elem Decision'.indeterminate_d then Decision'.indeterminate else
     Decision'.not_applicable
-  def eval_legacy_ordered_permit_overrides_rule : List Decision' -> Decision' := eval_legacy_permit_overrides_rule
-end CombinatorAlgorithm
+  def eval_legacy_ordered_permit_overrides : List Decision' -> Decision' := eval_legacy_permit_overrides
+end RuleCombinatorAlgorithm
+
+inductive PolicyCombinatorAlgorithm where
+  | deny_overrides                  : PolicyCombinatorAlgorithm
+  | ordered_deny_overrides          : PolicyCombinatorAlgorithm
+  | permit_overrides                : PolicyCombinatorAlgorithm
+  | ordered_permit_overrides        : PolicyCombinatorAlgorithm
+  | deny_unless_permit              : PolicyCombinatorAlgorithm
+  | permit_unless_deny              : PolicyCombinatorAlgorithm
+  | first_applicable                : PolicyCombinatorAlgorithm
+  | only_one_applicable             : PolicyCombinatorAlgorithm
+  | legacy_deny_overrides           : PolicyCombinatorAlgorithm
+  | legacy_ordered_deny_overrides   : PolicyCombinatorAlgorithm
+  | legacy_permit_overrides         : PolicyCombinatorAlgorithm
+  | legacy_ordered_permit_overrides : PolicyCombinatorAlgorithm
+
+namespace PolicyCombinatorAlgorithm
+  def eval_deny_overrides := RuleCombinatorAlgorithm.eval_deny_overrides
+  def eval_ordered_deny_overrides := RuleCombinatorAlgorithm.eval_ordered_deny_overrides
+  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
+
+  -- The non-normative part of the specification asserts that "If an error
+  -- occurs while evaluating the target or condition of a rule, then the
+  -- evaluation SHALL halt, and the policy shall evaluate to "Indeterminate",
+  -- with the appropriate error status."
+  --
+  -- This behavior isn't spelled out in the normative part, because errors are
+  -- represented as an Indeterminate.
+  def eval_only_one_applicable (results : List Decision') : Decision' :=
+    match results.filter (fun d => d != Decision'.not_applicable) with
+      | []  => Decision'.not_applicable
+      | [a] => a
+      | _   => Decision'.indeterminate
+
+  def eval_legacy_deny_overrides (results : List Decision') : Decision' :=
+    if results.elem Decision'.deny then Decision'.deny else
+    if results.elem Decision'.indeterminate then Decision'.deny else
+    if results.elem Decision'.permit then Decision'.permit else
+    Decision'.not_applicable
+  def eval_legacy_ordered_deny_overrides : List Decision' -> Decision' := eval_legacy_deny_overrides
+
+  -- See the comment for `eval_legacy_deny_overrides`.
+  def eval_legacy_permit_overrides (results : List Decision') : Decision' :=
+    if results.elem Decision'.permit then Decision'.permit else
+    if results.elem Decision'.deny then Decision'.deny else
+    if results.elem Decision'.indeterminate then Decision'.indeterminate else
+    Decision'.not_applicable
+  def eval_legacy_ordered_permit_overrides : List Decision' -> Decision' := eval_legacy_permit_overrides
+end PolicyCombinatorAlgorithm
 
 structure AttributeDesignator where
   category        : String
@@ -592,7 +635,7 @@ namespace Rule
 end Rule
 
 structure PolicySet where
-  combinator  : CombinatorAlgorithm
+  combinator  : PolicyCombinatorAlgorithm
   target      : Target
   children    : List PolicySetChild
   obligations : List ObligationExpression
@@ -603,7 +646,7 @@ inductive PolicySetChild where
   | policy     (inner : Policy)    : PolicySetChild
 
 structure Policy where
-  combinator  : CombinatorAlgorithm
+  combinator  : RuleCombinatorAlgorithm
   target      : Target
   rules       : List Rule
   obligations : List ObligationExpression
@@ -614,18 +657,17 @@ namespace Policy
     let results := policy.rules.map (fun rule => rule.eval context)
     let combinator :=
       match policy.combinator with
-        | CombinatorAlgorithm.deny_overrides                  => CombinatorAlgorithm.eval_deny_overrides
-        | CombinatorAlgorithm.ordered_deny_overrides          => CombinatorAlgorithm.eval_ordered_deny_overrides
-        | CombinatorAlgorithm.permit_overrides                => CombinatorAlgorithm.eval_permit_overrides
-        | CombinatorAlgorithm.ordered_permit_overrides        => CombinatorAlgorithm.eval_ordered_permit_overrides
-        | CombinatorAlgorithm.deny_unless_permit              => CombinatorAlgorithm.eval_deny_unless_permit
-        | CombinatorAlgorithm.permit_unless_deny              => CombinatorAlgorithm.eval_permit_unless_deny
-        | CombinatorAlgorithm.first_applicable                => CombinatorAlgorithm.eval_first_applicable_rule
-        | CombinatorAlgorithm.only_one_applicable             => CombinatorAlgorithm.eval_only_one_applicable
-        | CombinatorAlgorithm.legacy_deny_overrides           => CombinatorAlgorithm.eval_legacy_deny_overrides_rule
-        | CombinatorAlgorithm.legacy_ordered_deny_overrides   => CombinatorAlgorithm.eval_legacy_ordered_deny_overrides_rule
-        | CombinatorAlgorithm.legacy_permit_overrides         => CombinatorAlgorithm.eval_legacy_permit_overrides_rule
-        | CombinatorAlgorithm.legacy_ordered_permit_overrides => CombinatorAlgorithm.eval_legacy_ordered_permit_overrides_rule
+        | RuleCombinatorAlgorithm.deny_overrides                  => RuleCombinatorAlgorithm.eval_deny_overrides
+        | RuleCombinatorAlgorithm.ordered_deny_overrides          => RuleCombinatorAlgorithm.eval_ordered_deny_overrides
+        | RuleCombinatorAlgorithm.permit_overrides                => RuleCombinatorAlgorithm.eval_permit_overrides
+        | RuleCombinatorAlgorithm.ordered_permit_overrides        => RuleCombinatorAlgorithm.eval_ordered_permit_overrides
+        | RuleCombinatorAlgorithm.deny_unless_permit              => RuleCombinatorAlgorithm.eval_deny_unless_permit
+        | RuleCombinatorAlgorithm.permit_unless_deny              => RuleCombinatorAlgorithm.eval_permit_unless_deny
+        | RuleCombinatorAlgorithm.first_applicable                => RuleCombinatorAlgorithm.eval_first_applicable
+        | RuleCombinatorAlgorithm.legacy_deny_overrides           => RuleCombinatorAlgorithm.eval_legacy_deny_overrides
+        | 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
     match policy.target.eval context with
       | MatchResult.is_match => decision