Beginnings of encoding bags into semantics

1 files changed, 134 insertions, 103 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 195b412..80b1436 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -99,14 +99,14 @@ inductive XmlType
   | xpathExpression   : XmlType
 deriving BEq, Repr
 
-def Value : Type := XmlType × String
+def Primitive : Type := XmlType × String
 deriving BEq, Repr
 
-def Value.mk (type : XmlType) (inner : String) : Value := (type, inner)
+def Primitive.mk (type : XmlType) (inner : String) : Primitive := (type, inner)
 
-notation:65 "#<" lhs:65 "," rhs:66 ">" => Value.mk lhs rhs
+notation:65 "#<" lhs:65 "," rhs:66 ">" => Primitive.mk lhs rhs
 
-instance : Coe Bool Value where
+instance : Coe Bool Primitive where
   coe b :=
     match b with
       | true  => #<XmlType.boolean, "True">
@@ -118,12 +118,36 @@ instance : Coe Bool Value where
 -- to be the result of an invalid expression, or an operational error
 -- occurring during the evaluation of the expression."
 
-instance : Coe (Option Value) Value where
+instance : Coe (Option Primitive) Primitive where
   coe b :=
     match b with
       | Option.none   => #<XmlType.boolean, "Indeterminate">
       | Option.some a => a
 
+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)
+
+instance : BEq Bag where
+  beq := Bag.beq
+
+inductive Value where
+  | primitive (p : Primitive) : Value
+  | bag (b : Bag)             : Value
+deriving BEq, Repr
+
+instance : Coe (Option Value) Value where
+  coe b :=
+    match b with
+      | Option.none   => Value.primitive (#<XmlType.boolean, "Indeterminate">)
+      | Option.some a => a
+
 ------------------------------------------------------------------------
 ---- Attributes---------------------------------------------------------
 ------------------------------------------------------------------------
@@ -143,7 +167,7 @@ structure Attribute where
   category   : String
   identifier : String
   issuer     : Option String
-  value      : Value
+  value      : Primitive
 deriving Repr
 
 -- More than one attribute with a particular (category, identifier, issuer) can
@@ -181,7 +205,7 @@ structure AttributeDesignator where
 deriving BEq, Repr
 
 namespace AttributeDesignator
-  def eval (designator : AttributeDesignator) (context : List Attribute) : Option (List Value) :=
+  def eval (designator : AttributeDesignator) (context : List Attribute) : Option Value :=
     match designator with
       | AttributeDesignator.mk category identifier type issuer must_be_present =>
         let found :=
@@ -211,8 +235,8 @@ namespace AttributeDesignator
         if must_be_present then
           match found with
             | [] => Option.none
-            | _ => found
-        else found
+            | _ => Value.bag (Bag.mk found)
+        else Value.bag (Bag.mk found)
 end AttributeDesignator
 
 def matches? (designator : AttributeDesignator) (attr : Attribute) : Prop :=
@@ -254,8 +278,8 @@ namespace Expression
   def apply_eval (name : FunctionID) (args : List Value) : Option Value :=
     if name == "urn:oasis:names:tc:xacml:1.0:function:rfc822Name-match" then
       match args with
-        | [lhs, rhs] => lhs == rhs
-        | _          => #<XmlType.boolean, "Indeterminate">
+        | [Value.primitive lhs, Value.primitive rhs] => Value.primitive (lhs == rhs)
+        | _          => Value.primitive (#<XmlType.boolean, "Indeterminate">)
     else Option.none
 
   def eval (expression : Expression) (context : Request) : Option Value :=
@@ -284,16 +308,23 @@ namespace Match
     match m with
       | Match.mk fn designator value =>
         do
-          let attrs <- designator.eval context
-          let results :=
+          let result <- designator.eval context
+          let results := match result with
+          | (Value.bag (Bag.mk attrs)) => 
             attrs.map
-              (fun attr =>
-                let args := [value, attr]
-                (Expression.apply fn args).eval context)
+            fun attr =>
+              let args := [value, Value.primitive attr]
+              (Expression.apply fn args).eval context
+          | (Value.primitive attr) =>
+            let args := [value, Value.primitive attr]
+            [(Expression.apply fn args).eval context]
+      
           let results := results.map (fun (x : Option Value) => (x : Value))
-          if results.elem (#<XmlType.boolean, "True">) then (#<XmlType.boolean, "True">)
-          else if results.elem (#<XmlType.boolean, "Indeterminate">) then (#<XmlType.boolean, "Indeterminate">)
-          else (#<XmlType.boolean, "False">)
+          if results.elem (Value.primitive (#<XmlType.boolean, "True">)) then 
+            (Value.primitive (#<XmlType.boolean, "True">))
+          else if results.elem (Value.primitive (#<XmlType.boolean, "Indeterminate">)) then 
+            (Value.primitive (#<XmlType.boolean, "Indeterminate">))
+          else Value.primitive (#<XmlType.boolean, "False">)
 end Match
 
 structure AttributeAssignment where
@@ -382,7 +413,7 @@ def Result : Type := Decision × (Option ResultAuxiliary)
 
 def is_indeterminate (x : Expression) : Bool :=
   match x with
-  | Expression.attribute_value (XmlType.boolean, "Indeterminate") => true
+  | Expression.attribute_value (Value.primitive (XmlType.boolean, "Indeterminate")) => true
   | _ => false
 
 def make_response
@@ -454,69 +485,69 @@ deriving BEq, Repr
 --    c. Finally, if all function applications evaluate to "False", then
 --       the result of the entire expression SHALL be "False".
 
-def evaluate_all_of (all_of : AllOf) (context : Request) : MatchResult :=
-  let result := all_of.map (fun x => x.eval context)
-  let result := result.map (fun (x : Option Value) => (x : Value))
-  if result.all (fun x => x == (XmlType.boolean, "True")) then MatchResult.is_match
-  else if result.all (fun x => x != (XmlType.boolean, "False")) ∧
-          result.elem (XmlType.boolean, "Indeterminate") then MatchResult.indeterminate
-  else MatchResult.no_match
+-- def evaluate_all_of (all_of : AllOf) (context : Request) : MatchResult :=
+--   let result := all_of.map (fun x => x.eval context)
+--   let result := result.map (fun (x : Option Value) => (x : Value))
+--   if result.all (fun x => x == (XmlType.boolean, "True")) then MatchResult.is_match
+--   else if result.all (fun x => x != (XmlType.boolean, "False")) ∧
+--           result.elem (XmlType.boolean, "Indeterminate") then MatchResult.indeterminate
+--   else MatchResult.no_match
 
-def evaluate_any_of (any_of : AnyOf) (context : Request) : MatchResult :=
-  match any_of with
-    | [] => MatchResult.is_match
-    | List.cons x xs => match evaluate_all_of x context with
-      | MatchResult.is_match => MatchResult.is_match
-      | MatchResult.no_match =>
-        let rest := evaluate_any_of xs context
-        if rest == MatchResult.is_match then MatchResult.no_match else rest
-      | MatchResult.indeterminate =>
-        let rest := evaluate_any_of xs context
-        if rest == MatchResult.no_match then MatchResult.indeterminate else rest
+-- def evaluate_any_of (any_of : AnyOf) (context : Request) : MatchResult :=
+--   match any_of with
+--     | [] => MatchResult.is_match
+--     | List.cons x xs => match evaluate_all_of x context with
+--       | MatchResult.is_match => MatchResult.is_match
+--       | MatchResult.no_match =>
+--         let rest := evaluate_any_of xs context
+--         if rest == MatchResult.is_match then MatchResult.no_match else rest
+--       | MatchResult.indeterminate =>
+--         let rest := evaluate_any_of xs context
+--         if rest == MatchResult.no_match then MatchResult.indeterminate else rest
 
-def evaluate_target (target : Target) (context : Request) : MatchResult :=
-  match target with
-    | [] => MatchResult.is_match
-    | List.cons x xs => match evaluate_any_of x context with
-      | MatchResult.is_match => evaluate_target xs context
-      | MatchResult.no_match => MatchResult.no_match
-      | MatchResult.indeterminate =>
-        let rest := evaluate_target xs context
-        if rest == MatchResult.no_match then rest else MatchResult.indeterminate
+-- def evaluate_target (target : Target) (context : Request) : MatchResult :=
+--   match target with
+--     | [] => MatchResult.is_match
+--     | List.cons x xs => match evaluate_any_of x context with
+--       | MatchResult.is_match => evaluate_target xs context
+--       | MatchResult.no_match => MatchResult.no_match
+--       | MatchResult.indeterminate =>
+--         let rest := evaluate_target xs context
+--         if rest == MatchResult.no_match then rest else MatchResult.indeterminate
 
-def evaluate_assignments (assignments : List AttributeAssignmentExpression) : List AttributeAssignment :=
-  assignments.map (fun assignment =>
-                       match assignment with
-                       | AttributeAssignmentExpression.mk category identifier issuer _ =>
-                         AttributeAssignment.mk category identifier issuer)
+-- def evaluate_assignments (assignments : List AttributeAssignmentExpression) : List AttributeAssignment :=
+--   assignments.map (fun assignment =>
+--                        match assignment with
+--                        | AttributeAssignmentExpression.mk category identifier issuer _ =>
+--                          AttributeAssignment.mk category identifier issuer)
 
 
-def evaluate_rule (rule : Rule) (context : Request) : Decision' × ResultAuxiliary :=
-  let decision :=
-    if rule.target == [] then (rule.effect).to_decision'
-    else match evaluate_target rule.target context with
-      | MatchResult.is_match =>
-        match ((rule.condition).eval context : Value) with
-          | (XmlType.string, "True") => (rule.effect).to_decision'
-          | (XmlType.string, "False") => Decision'.not_applicable
-          | (_, _) =>
-            if (rule.effect).to_decision' == 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 : Decision))
-  let advice      := rule.advice.filter      (fun obl => obl.applies_to == (decision : Decision))
-  (
-    decision,
-    ResultAuxiliary.mk
-      Option.none
-      (obligations.map (fun expr => Obligation.mk
-                                      (evaluate_assignments expr.assignments)
-                                      expr.identifier))
-      (advice.map      (fun expr => Advice.mk
-                                      (evaluate_assignments expr.assignments)
-                                      expr.identifier)))
+-- def evaluate_rule (rule : Rule) (context : Request) : Decision' × ResultAuxiliary :=
+--   let decision :=
+--     if rule.target == [] then (rule.effect).to_decision'
+--     else match evaluate_target rule.target context with
+--       | MatchResult.is_match =>
+--         match ((rule.condition).eval context : Value) with
+--           | (XmlType.string, "True") => (rule.effect).to_decision'
+--           | (XmlType.string, "False") => Decision'.not_applicable
+--           | (_, _) =>
+--             if (rule.effect).to_decision' == 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 : Decision))
+--   let advice      := rule.advice.filter      (fun obl => obl.applies_to == (decision : Decision))
+--   (
+--     decision,
+--     ResultAuxiliary.mk
+--       Option.none
+--       (obligations.map (fun expr => Obligation.mk
+--                                       (evaluate_assignments expr.assignments)
+--                                       expr.identifier))
+--       (advice.map      (fun expr => Advice.mk
+--                                       (evaluate_assignments expr.assignments)
+--                                       expr.identifier)))
 
 -- theorem test :
 --   ∀ (r : Rule) (c : Request),
@@ -535,29 +566,29 @@ def evaluate_rule (rule : Rule) (context : Request) : Decision' × ResultAuxilia
 --       simp [h_condition_eval] }
 --     { simp }
 
-def evaluate_deny_overrides (results : List Decision') : Decision' :=
-  if results.elem Decision'.deny then Decision'.deny else
-  if results.elem Decision'.indeterminate_dp then Decision'.indeterminate_dp else
-  if results.elem Decision'.indeterminate_d ∧ results.elem Decision'.indeterminate_p then Decision'.indeterminate_dp else
-  if results.elem Decision'.indeterminate_d then Decision'.indeterminate_d else
-  if results.elem Decision'.permit then Decision'.permit else
-  if results.elem Decision'.indeterminate_p then Decision'.indeterminate_p else
-  Decision'.not_applicable
+-- def evaluate_deny_overrides (results : List Decision') : Decision' :=
+--   if results.elem Decision'.deny then Decision'.deny else
+--   if results.elem Decision'.indeterminate_dp then Decision'.indeterminate_dp else
+--   if results.elem Decision'.indeterminate_d ∧ results.elem Decision'.indeterminate_p then Decision'.indeterminate_dp else
+--   if results.elem Decision'.indeterminate_d then Decision'.indeterminate_d else
+--   if results.elem Decision'.permit then Decision'.permit else
+--   if results.elem Decision'.indeterminate_p then Decision'.indeterminate_p else
+--   Decision'.not_applicable
 
-def evaluate_policy (policy : Policy) (context : Request) : Choice :=
-  let results     := policy.rules.map (fun x => evaluate_rule x context)
-  let decision    := evaluate_deny_overrides (results.map Prod.fst)
-  let obligations := policy.obligations.filter (fun obl => obl.fulfill_on == (decision : Decision))
-  let advice      := policy.advice.filter      (fun obl => obl.applies_to == (decision : Decision))
-  -- TODO: How do we combine advice/obligations?
-  [(
-    decision,
-    ResultAuxiliary.mk
-      Option.none
-      (obligations.map (fun expr => Obligation.mk
-                                      (evaluate_assignments expr.assignments)
-                                      expr.identifier))
-      (advice.map      (fun expr => Advice.mk
-                                      (evaluate_assignments expr.assignments)
-                                      expr.identifier))
-  )]
+-- def evaluate_policy (policy : Policy) (context : Request) : Choice :=
+--   let results     := policy.rules.map (fun x => evaluate_rule x context)
+--   let decision    := evaluate_deny_overrides (results.map Prod.fst)
+--   let obligations := policy.obligations.filter (fun obl => obl.fulfill_on == (decision : Decision))
+--   let advice      := policy.advice.filter      (fun obl => obl.applies_to == (decision : Decision))
+--   -- TODO: How do we combine advice/obligations?
+--   [(
+--     decision,
+--     ResultAuxiliary.mk
+--       Option.none
+--       (obligations.map (fun expr => Obligation.mk
+--                                       (evaluate_assignments expr.assignments)
+--                                       expr.identifier))
+--       (advice.map      (fun expr => Advice.mk
+--                                       (evaluate_assignments expr.assignments)
+--                                       expr.identifier))
+--   )]