Troll through syntax once more

2 files changed, 216 insertions, 51 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 2801567..387b9a2 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -18,12 +18,47 @@ inductive Decision where
   | permit           : Decision
   | deny             : Decision
   | indeterminate    : Decision
-  | indeterminate_d  : Decision
-  | indeterminate_p  : Decision
-  | indeterminate_dp : Decision
   | not_applicable   : Decision
 deriving BEq, Repr
 
+inductive Decision' where
+  | permit           : Decision'
+  | deny             : Decision'
+  | indeterminate    : Decision'
+  | indeterminate_d  : Decision'
+  | indeterminate_p  : Decision'
+  | indeterminate_dp : Decision'
+  | not_applicable   : Decision'
+deriving BEq, Repr
+
+instance : Coe Decision' Decision where
+  coe b :=
+    match b with
+      | Decision'.permit           => Decision.permit
+      | Decision'.deny             => Decision.deny
+      | Decision'.indeterminate    => Decision.indeterminate
+      | Decision'.indeterminate_d  => Decision.indeterminate
+      | Decision'.indeterminate_p  => Decision.indeterminate
+      | Decision'.indeterminate_dp => Decision.indeterminate
+      | Decision'.not_applicable   => Decision.not_applicable
+
+inductive EffectType where
+  | permit : EffectType
+  | deny   : EffectType
+deriving BEq, Repr
+
+namespace EffectType
+  def to_decision (e : EffectType) : Decision :=
+    match e with
+    | EffectType.permit => Decision.permit
+    | EffectType.deny   => Decision.deny
+
+  def to_decision' (e : EffectType) : Decision' :=
+    match e with
+    | EffectType.permit => Decision'.permit
+    | EffectType.deny   => Decision'.deny
+end EffectType
+
 ------------------------------------------------------------------------
 ---- Values ------------------------------------------------------------
 ------------------------------------------------------------------------
@@ -128,6 +163,12 @@ deriving BEq, Repr
 def FunctionID : Type := String
 deriving BEq, Repr
 
+
+-- "The <Expression> element is not used directly in a policy. The <Expression>
+-- element signifies that an element that extends the ExpressionType and is a
+-- member of the <Expression> element substitution group SHALL appear in its
+-- place."
+
 inductive Expression where
   | apply                (function : FunctionID) (args: List Expression) : Expression
   | attribute_designator (inner : AttributeDesignator)                   : Expression
@@ -147,40 +188,46 @@ deriving BEq, Repr
 def Target : Type := List AnyOf
 deriving BEq, Repr
 
-structure AttributeAssignmentExpression where
+structure AttributeAssignment where
   category        : String
   identifier      : String
   issuer          : Option String
-  expression      : Expression
 deriving BEq, Repr
 
-structure ObligationExpression where
-  assignments : List AttributeAssignmentExpression
+structure Obligation where
+  assignments : List AttributeAssignment
   identifier : String
-  fulfill_on : Decision
 deriving BEq, Repr
 
-structure Obligation where
-  assignments : List AttributeAssignmentExpression
+structure Advice where
+  assignments : List AttributeAssignment
   identifier : String
 deriving BEq, Repr
 
-structure AdviceExpression where
+structure AttributeAssignmentExpression where
+  category        : String
+  identifier      : String
+  issuer          : Option String
+  expression      : Expression
+deriving BEq, Repr
+
+structure ObligationExpression where
   assignments : List AttributeAssignmentExpression
   identifier : String
-  applies_to : Decision
+  fulfill_on : Decision
 deriving BEq, Repr
 
-structure Advice where
+structure AdviceExpression where
   assignments : List AttributeAssignmentExpression
   identifier : String
+  applies_to : Decision
 deriving BEq, Repr
 
 -- n.b. "The <Condition> contains one <Expression> element"
 structure Rule where
   target      : Target
   condition   : Expression
-  effect      : Decision
+  effect      : EffectType
   obligations : List ObligationExpression
   advice      : List AdviceExpression
 
@@ -202,13 +249,79 @@ structure Policy where
   obligations : List ObligationExpression
   advice      : List AdviceExpression
 
-structure ResponseAuxiliary where
-  status      : Option String
+inductive StatusCode
+  | ok                : StatusCode
+  | missing_attribute : StatusCode
+  | syntax_error      : StatusCode
+  | processing_error  : StatusCode
+deriving BEq, Repr
+
+structure ResultAuxiliary where
+  status      : Option (List StatusCode)
   obligations : List Obligation
   advice      : List Advice
 deriving BEq, Repr
 
-def Choice : Type := List (Decision × ResponseAuxiliary)
+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 (XmlType.boolean, "Indeterminate") => true
+  | _ => false
+
+def make_response
+  (decision    : Decision)
+  (status      : Option (List StatusCode))
+  (obligations : List Obligation)
+  (advice      : List Advice)
+: Decision × ResultAuxiliary :=
+  let obligations := obligations.map (fun expr => Obligation.mk expr.assignments expr.identifier)
+  let advice      := advice.map      (fun expr => Advice.mk     expr.assignments expr.identifier)
+  -- If any of the attribute assignment expressions in an obligation or
+  -- advice expression with a matching FulfillOn or AppliesTo attribute
+  -- evaluates to “Indeterminate”, then the whole rule, policy, or
+  -- policy set SHALL be “Indeterminate”. If the FulfillOn or AppliesTo
+  -- attribute does not match the result of the combining algorithm or
+  -- the rule evaluation, then any indeterminate in an obligation or
+  -- advice expression has no effect.
+  -- if obligations.
+  let decision :=
+    -- if obligations.any
+    --      (fun obligation => obligation.assignments.any
+    --        (fun assignment => is_indeterminate assignment.expression)) ∨
+    --    advice.any
+    --      (fun advice => advice.assignments.any
+    --        (fun assignment => is_indeterminate assignment.expression))
+    -- then
+    --   Decision.indeterminate
+    -- else
+      decision
+  (
+    decision,
+    ResultAuxiliary.mk
+      status
+      (obligations.map (fun expr => Obligation.mk expr.assignments expr.identifier))
+      (advice.map      (fun expr => Advice.mk     expr.assignments expr.identifier))
+  )
+
+def combine_response_aux (x y : ResultAuxiliary) : ResultAuxiliary :=
+  match (x, y) with
+    | (ResultAuxiliary.mk status₁ obligations₁ advice₁,
+       ResultAuxiliary.mk status₂ obligations₂ advice₂) =>
+      ResultAuxiliary.mk
+        status₁
+        (obligations₁ ++ obligations₂)
+        (advice₁ ++ advice₂)
+
+def Choice : Type := List (Decision × ResultAuxiliary)
 deriving BEq, Repr
 
 ---
@@ -234,7 +347,7 @@ def example_4_1_policy :=
         ] -- </AnyOf>
       ]
       (Expression.attribute_value (#<XmlType.boolean, "True">))
-      Decision.permit
+      EffectType.permit
       [] []]
     [] []
 
@@ -308,7 +421,7 @@ def example_4_2_policy_rule_1 :=
               XmlType.string
               Option.none
               false)]])
-      Decision.permit
+      EffectType.permit
       [] []]
     [] []
 
@@ -366,7 +479,7 @@ def example_4_2_policy_rule_2 :=
                 XmlType.string
                 Option.none
                 false)]])
-      Decision.permit
+      EffectType.permit
       [] []]
     [] []
 
@@ -430,7 +543,7 @@ def example_4_2_policy_rule_3 :=
               XmlType.string
               Option.none
               false)]])
-      Decision.permit
+      EffectType.permit
       [] []]
     [] []
 
@@ -476,7 +589,7 @@ def example_4_2_policy_rule_4 :=
           false)
         (#<XmlType.string, "read">)]]]
       (Expression.attribute_value (#<XmlType.boolean, "True">))
-      Decision.deny
+      EffectType.deny
       [] []]
     [] []
 
@@ -624,29 +737,39 @@ 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) : Decision × ResponseAuxiliary :=
+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
+    if rule.target == [] then (rule.effect).to_decision'
     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
+          | (XmlType.string, "True") => (rule.effect).to_decision'
+          | (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)
+            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,
-    ResponseAuxiliary.mk
+    ResultAuxiliary.mk
       Option.none
-      (obligations.map (fun expr => Obligation.mk expr.assignments expr.identifier))
-      (advice.map      (fun expr => Advice.mk     expr.assignments expr.identifier))
-  )
+      (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),
@@ -665,18 +788,32 @@ def evaluate_rule (rule : Rule) (context : Request) : Decision × ResponseAuxili
 --       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_policy (policy : Policy) (context : Request) : Choice :=
-  match policy.rules with
-    | [rule₁] => [evaluate_rule rule₁ context]
-    | _ => []
+  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_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
 
 #eval evaluate_policy example_4_1_policy example_4_1_request
diff --git a/xacml-proofs/modeling-choices.org b/xacml-proofs/modeling-choices.org
index 80c2968..8d88c61 100644
--- a/xacml-proofs/modeling-choices.org
+++ b/xacml-proofs/modeling-choices.org
@@ -1,4 +1,17 @@
-* Not Relevant
+XACML makes use of URIs and strings as identifiers. When such identifiers are compared for equality, the comparison MUST be done so that the identifiers are equal if they have the same length and the characters in the two identifiers are equal codepoint by codepoint.
+
+(This is equivalent to string equality in Lean.)
+
+* Modeling Exceptions
+
+7.19 Exception handling specifies that an indeterminate decision is returned and a statuscode is set.
+  StatusCode is, however, optional.
+
+* In Scope vs Out of Scope
+
+"We would like to be as complete as possible, so as to ensure that this can be leveraged to prove a refinement of a policy down to the status codes, obligations, and advice it returns."
+
+** Not Relevant
 
 - [ ] Element <Description> (no semantic meaning)
 - [ ] Element <PolicyIssuer> (XMLAdmin)
@@ -26,7 +39,7 @@
 - [ ] Element <VariableReference> (dissolved by compiler translation)
 - [ ] Element <Content> (dissolved by compiler translation)
   
-* Modeled
+** Modeled
 
 - [X] Element <PolicySet>
 - [X] Element <Target>
@@ -65,7 +78,7 @@
 - [ ] Element <StatusCode>
 - [ ] Element <MissingAttributeDetail>
 
-* Doesn't Line Up with ACES
+** Doesn't Line Up with ACES
 
 - Does use PolicySetDefaults and XPathVersion but it's just XPath 1.0. Probably safe to ignore and have our XPath implementation follow 1.0.
 
@@ -88,3 +101,18 @@ Same assumption about PolicySelector as logic paper.
 
 - Assume Attribute->Issuer has no effect on access control decision
 - TODO What about Attribute->IncludeInResult?
+
+* 7.3.3 Multivalued attributes
+
+If a single <Attribute> element in a request context contains multiple <AttributeValue> child elements, then the bag of values resulting from evaluation of the <Attribute> element MUST be identical to the bag of values that results from evaluating a context in which each <AttributeValue> element appears in a separate <Attribute> element, each carrying identical meta-data.
+
+This is handled by the compiler.
+
+* Variable Substitution
+
+Functions SHALL NOT have side effects, as evaluation order cannot be guaranteed in a standard way.
+
+* Compiler Versus Embedding Decisions
+
+Example: =<AllOf>= and =<AnyOf>= are specified to be nonempty.
+We could encode this in Lean's type system but it's more convenient to assume that an empty =AllOf= or =AnyOf= will never be constructed by the trusted compiler base.