Check-in 2023-12-15

1 files changed, 326 insertions, 60 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 448f287..42c5150 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -9,6 +9,8 @@
 ------------------------------------------------------------------------
 
 import Aesop
+import Mathlib.Data.Bool.AllAny
+import Mathlib.Data.Multiset.Basic
 import Mathlib.Data.Prod.Basic
 import Mathlib.Tactic.LibrarySearch
 import Std.Data.List.Basic
@@ -19,14 +21,28 @@ inductive MatchResult where
   | is_match      : MatchResult
   | no_match      : MatchResult
   | indeterminate : MatchResult
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
+
+instance : LawfulBEq MatchResult where
+  eq_of_beq := by
+    intros a b h
+    induction a
+    all_goals induction b
+    all_goals
+      first
+      | rfl
+      | contradiction
+  rfl := by
+    intro a
+    induction a
+    all_goals rfl
 
 inductive Decision where
   | permit           : Decision
   | deny             : Decision
   | indeterminate    : Decision
   | not_applicable   : Decision
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 -- This type is used to implement the semantics described in § 7.10 (Extended
 -- Indeterminate). It is only relevant to combining algorithms.
@@ -38,11 +54,21 @@ inductive Decision' where
   | indeterminate_p  : Decision'
   | indeterminate_dp : Decision'
   | not_applicable   : Decision'
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 instance : LawfulBEq Decision' where
-  eq_of_beq := by sorry
-  rfl := by sorry
+  eq_of_beq := by
+    intros a b h
+    induction a
+    all_goals induction b
+    all_goals
+      first
+      | rfl
+      | contradiction
+  rfl := by
+    intro a
+    induction a
+    all_goals rfl
 
 def Decision'.downcast : Decision' → Decision
   | Decision'.permit           => Decision.permit
@@ -59,7 +85,7 @@ instance : Coe Decision' Decision where
 inductive EffectType where
   | permit : EffectType
   | deny   : EffectType
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 namespace EffectType
   def to_decision (e : EffectType) : Decision :=
@@ -108,14 +134,14 @@ inductive XmlType
   | rfc822Name        : XmlType
   | ipAddress         : XmlType
   | dnsName           : XmlType
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 instance : LawfulBEq XmlType where
   eq_of_beq := by
     intros a b h
     induction a
     all_goals induction b
-    all_goals 
+    all_goals
       first
       | rfl
       | contradiction
@@ -125,9 +151,9 @@ instance : LawfulBEq XmlType where
     all_goals rfl
 
 def Primitive : Type := XmlType × String
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
-theorem Prod.beq_iff_fst_eq_snd_eq 
+theorem Prod.beq_iff_fst_eq_snd_eq
   {α β : Type} [BEq α] [BEq β] [LawfulBEq α] [LawfulBEq β]
   (a b : α × β) :
   a == b  ↔ a.fst == b.fst ∧ a.snd == b.snd := by
@@ -149,7 +175,7 @@ instance : LawfulBEq Primitive where
     intro a
     rw [Prod.beq_iff_fst_eq_snd_eq]
     apply And.intro
-    all_goals simp 
+    all_goals simp
 
 def Primitive.mk (type : XmlType) (inner : String) : Primitive := (type, inner)
 
@@ -175,21 +201,44 @@ instance : Coe (Option Primitive) Primitive where
 
 structure Bag where
   contents: List Primitive
-deriving Repr
+deriving BEq, DecidableEq, Repr
+
+-- def Bag.beq (b₁ b₂ : Bag) : Bool :=
+--   b₁.contents.all (fun x => b₂.contents.count x == b₁.contents.count x)
 
-def Bag.beq (b₁ b₂ : Bag) : Bool :=
-  b₁.contents.all (fun x => b₂.contents.count x == b₁.contents.count x)
+#check {1, 2, 3}
 
 instance : BEq Bag where
   beq := Bag.beq
 
+-- instance : LawfulBEq Bag where
+--   eq_of_beq := by
+--     intros a b h
+    
+--   rfl := by sorry
+
 inductive Value where
   | primitive (p : Primitive) : Value
   | bag (b : Bag)             : Value
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 instance : LawfulBEq Value where
-  eq_of_beq := by sorry
+  eq_of_beq := by
+    intros a b h
+    cases a with
+    | primitive pa =>
+      cases b with
+      | primitive pb => 
+        simp
+        exact (beq_iff_eq pa pb).mp h
+      | bag bb => contradiction
+    | bag ba =>
+      cases b with
+      | primitive pb => contradiction
+      | bag bb => 
+        simp
+        sorry
+        -- exact (beq_iff_eq ba bb).mp h
   rfl := by sorry
 
 instance : Coe (Option Value) Value where
@@ -225,7 +274,7 @@ structure Attribute where
   identifier : String
   issuer     : Option String
   value      : Primitive
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 instance : LawfulBEq Attribute where
   eq_of_beq := by sorry
@@ -241,7 +290,7 @@ deriving Repr
 ---
 
 def Identifier : Type := String
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 inductive RuleCombinatorAlgorithm where
   | deny_overrides                  : RuleCombinatorAlgorithm
@@ -382,7 +431,7 @@ inductive StatusCode
   | missing_attribute : StatusCode
   | syntax_error      : StatusCode
   | processing_error  : StatusCode
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 structure AttributeDesignator where
   category        : String
@@ -390,7 +439,7 @@ structure AttributeDesignator where
   type            : XmlType
   issuer          : Option String
   must_be_present : Bool
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 namespace AttributeDesignator
   -- A named attribute SHALL match an attribute if the values of their
@@ -467,7 +516,7 @@ def matches? (designator : AttributeDesignator) (attr : Attribute) : Prop :=
   | _ => False
 
 def FunctionID : Type := String
-deriving BEq, Repr
+deriving DecidableEq, 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
@@ -490,7 +539,7 @@ inductive Expression where
   | attribute_designator (inner : AttributeDesignator)                   : Expression
   | attribute_value      (inner : Value)                                 : Expression
   | function             (function : FunctionID)                         : Expression
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 namespace Expression
   def apply_eval (name : FunctionID) (args : List Value) : Option Value :=
@@ -537,13 +586,29 @@ structure Match where
   function   : Identifier
   designator : AttributeDesignator
   value      : Value
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 def AllOf  : Type := List Match
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 def AnyOf  : Type := List AllOf
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 def Target : Type := List AnyOf
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
+
+instance : Membership AllOf AnyOf where
+  mem := fun x y => y.contains x
+
+instance : LawfulBEq Match where
+  eq_of_beq := by sorry
+  rfl := by sorry
+instance : LawfulBEq AllOf where
+  eq_of_beq := by sorry
+  rfl := by sorry
+instance : LawfulBEq AnyOf where
+  eq_of_beq := by sorry
+  rfl := by sorry
+instance : LawfulBEq Target where
+  eq_of_beq := by sorry
+  rfl := by sorry
 
 namespace Match
   -- The evaluation semantics for a matching element is as follows.
@@ -618,7 +683,7 @@ namespace AllOf
             result.elem (Value.primitive (XmlType.boolean, "Indeterminate"))
          then MatchResult.indeterminate
     else MatchResult.no_match
-  end AllOf
+end AllOf
 
 namespace AnyOf
   def eval (disj : AnyOf) (context : Request) : MatchResult :=
@@ -639,6 +704,113 @@ namespace AnyOf
       else MatchResult.no_match
 end AnyOf
 
+theorem elem_imp_nonempty 
+  {α : Type}
+  (x : α) (xs : List α) :
+  x ∈ xs → xs.isEmpty = false := by
+  induction xs with
+  | nil => simp
+  | cons _ _ _ => simp [List.isEmpty]
+
+theorem elem_map 
+  {α β : Type}
+  [BEq α] [LawfulBEq α]
+  [BEq β] [LawfulBEq β]
+  (x : α) (xs : List α) (f : α → β) :
+  List.elem x xs → List.elem (f x) (List.map f xs) := by
+  induction xs with
+  | nil => simp
+  | cons hd tl ih =>
+    intro h
+    simp [List.elem_cons] at *
+    cases h with
+    | inl h =>
+      apply Or.intro_left
+      exact congrArg f h
+    | inr h =>
+      apply Or.intro_right
+      simp [List.contains] at *
+      apply ih h
+
+theorem elem_imp_forall_not 
+  {α β : Type}
+  [BEq α] [LawfulBEq α] 
+  [BEq β] [LawfulBEq β]
+  (y : β) (xs : List α) (f : α → β) :
+  (∀ (x : α), x ∈ xs → f x ≠ y) →
+  List.elem y (List.map f xs) = false := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp
+    intros hy h_no_y
+    apply And.intro
+    { rw [eq_comm]
+      exact hy }
+    { apply ih h_no_y }
+
+theorem table_1_target_match_table₁ (disj : List AllOf) (context : Request) :
+  (∃ (conj : AllOf), conj ∈ disj ∧ conj.eval context = MatchResult.is_match)
+  → AnyOf.eval disj context = MatchResult.is_match := by
+  intro h
+  unfold AnyOf.eval
+  simp
+  intro _ h₂
+  apply False.elim
+  let ⟨x, hx⟩ := h
+  have hc₁ : ¬AllOf.eval x context = MatchResult.is_match := by
+    apply h₂
+    exact hx.left
+  have hc₂ : AllOf.eval x context = MatchResult.is_match := by
+    exact hx.right
+  contradiction
+
+theorem table_1_target_match_table₂ (disj : List AllOf) (context : Request) :
+    (∀ (conj : AllOf), conj ∈ disj → conj.eval context ≠ MatchResult.is_match)
+  → (∃ (conj : AllOf), conj ∈ disj ∧ conj.eval context = MatchResult.indeterminate)
+  → AnyOf.eval disj context = MatchResult.indeterminate := by
+    intros h_no_match h_indet
+    simp [AnyOf.eval]
+
+    let ⟨x, hx⟩ := h_indet
+
+    have hbranch : 
+      List.elem MatchResult.indeterminate
+                (List.map (fun x => AllOf.eval x context) disj)
+              = true := by
+      have hx' : AllOf.eval x context = MatchResult.indeterminate := by
+        exact hx.right
+      rw [←hx']
+      apply elem_map x disj (fun y => y.eval context)
+      apply List.elem_eq_true_of_mem hx.left
+    have hnonempty : List.isEmpty disj = false := by
+      apply elem_imp_nonempty _ _ hx.left
+    simp [hnonempty, hbranch]
+    intros x hx
+    apply h_no_match
+    exact hx
+
+theorem table_1_target_match_table₃ (disj : List AllOf) (context : Request) :
+    (∀ (conj : AllOf), conj ∈ disj → conj.eval context ≠ MatchResult.is_match)
+  → (∀ (conj : AllOf), conj ∈ disj → conj.eval context ≠ MatchResult.indeterminate)
+  → disj.isEmpty = false
+  → AnyOf.eval disj context = MatchResult.no_match := by
+    intros h_no_match h_no_indet h_nonempty
+    simp [AnyOf.eval]
+
+    simp [h_nonempty]
+    have h_no_match : 
+      ¬ ∃ a, a ∈ disj ∧ AllOf.eval a context = MatchResult.is_match := by
+      simp
+      apply h_no_match
+    have h_no_indet : 
+      List.elem MatchResult.indeterminate
+                (List.map (fun x => AllOf.eval x context) disj)
+        = false := by
+      apply elem_imp_forall_not
+      apply h_no_indet
+    simp [h_no_match, h_no_indet]
+
 namespace Target
   def eval (target : Target) (context : Request) : MatchResult :=
     match target with
@@ -661,19 +833,19 @@ end Target
 structure Obligation where
   assignments : List Attribute
   identifier : String
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 structure Advice where
   assignments : List Attribute
   identifier : String
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 structure AttributeAssignmentExpression where
   category        : String
   identifier      : String
   issuer          : Option String
   expression      : Expression
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 namespace AttributeAssignmentExpression
   def eval (assignment : AttributeAssignmentExpression) (context : Request) : Option Attribute :=
@@ -691,7 +863,7 @@ structure ObligationExpression where
   assignments : List AttributeAssignmentExpression
   identifier : String
   fulfill_on : Decision
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 namespace ObligationExpression
   def eval (obligation : ObligationExpression) (context : Request) : Option Obligation :=
@@ -707,7 +879,7 @@ structure AdviceExpression where
   assignments : List AttributeAssignmentExpression
   identifier : String
   applies_to : Decision
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 namespace AdviceExpression
   def eval (advice : AdviceExpression) (context : Request) : Option Advice :=
@@ -723,13 +895,13 @@ structure ResultAuxiliary where
   status      : Option (List StatusCode)
   obligations : List Obligation
   advice      : List Advice
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 structure ResultAuxiliary' where
   status      : Option (List StatusCode)
   obligations : List ObligationExpression
   advice      : List AdviceExpression
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 structure MissingAttributeDetail where
   category   : String
@@ -737,7 +909,7 @@ structure MissingAttributeDetail where
   issuer     : Option String
   value      : Option Value
   type       : XmlType
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 def Result : Type := Decision' × (Option ResultAuxiliary)
 def Result' : Type := Decision' × (Option ResultAuxiliary')
@@ -1022,7 +1194,7 @@ def combine_response_aux (x y : ResultAuxiliary) : ResultAuxiliary :=
         (advice₁ ++ advice₂)
 
 def Choice : Type := List (Decision × ResultAuxiliary)
-deriving BEq, Repr
+deriving DecidableEq, BEq, Repr
 
 def compiled_facassignviewgrades_metadata := ((PolicyElement.Rule (Rule.mk [[[(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "ExternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "Assign")))], [(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "InternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "Assign")))], [(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "ExternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "View")))], [(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "InternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "View")))]]] none EffectType.permit [] [])))
 def compiled_fac100_metadata := ((PolicyElement.Policy (Policy.mk RuleCombinatorAlgorithm.legacy_permit_overrides [[[(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" XmlType.string none True) (Value.primitive (XmlType.string, "Faculty")))]]] [] [])))
@@ -1059,15 +1231,15 @@ theorem contains_implies_map_contains {α β : Type} [BEq α] [LawfulBEq α] [BE
     intro h
     simp [ih] at *
     cases h with
-    | inl h' => 
+    | inl h' =>
       apply Or.intro_left
       apply congrArg f
       assumption
-    | inr h' => 
+    | inr h' =>
       apply Or.intro_right
       apply ih h'
 
-theorem match_eval_lemma₀ (s : String) (attrs : List Primitive) (req : Request) : 
+theorem match_eval_lemma₀ (s : String) (attrs : List Primitive) (req : Request) :
   attrs.contains (XmlType.string, s) →
   List.contains
     (List.map
@@ -1079,13 +1251,13 @@ theorem match_eval_lemma₀ (s : String) (attrs : List Primitive) (req : Request
       attrs)
     (Value.primitive (XmlType.boolean, "True")) := by
   rw_local
-    (some (Value.primitive (XmlType.boolean, "True"))) = 
+    (some (Value.primitive (XmlType.boolean, "True"))) =
     ((fun attr_1 =>
        Expression.eval
          (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal"
            [Value.primitive (XmlType.string, s), Value.primitive attr_1])
          req) (XmlType.string, s))
-    by 
+    by
       rw [eq_comm]
       simp
       apply string_equal_self
@@ -1105,14 +1277,14 @@ theorem match_eval (attr : Attribute) (s : String) (req : Request) :
              req = some (Value.primitive (XmlType.boolean, "True")) := by
   intros h₁ h₂
   simp [Match.eval]
-  rw_local 
+  rw_local
     attr.value = (XmlType.string, s)
     by apply h₁
   match AttributeDesignator.eval
         { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none,
           must_be_present := true }
         req with
-  | Sum.inl (Value.primitive p) => 
+  | Sum.inl (Value.primitive p) =>
     simp
     sorry -- contradiction by designator_always_returns_bag
   | Sum.inl (Value.bag b) => sorry
@@ -1658,7 +1830,7 @@ theorem separation_of_duty_imp_other_role_not_in_req' (req : Request) (s₁ s₂
   → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, s₂))
   → s₁ = s₂
  := by
-   intros hsod hs₁ hs₂ 
+   intros hsod hs₁ hs₂
    have hint₁ :
      ∀ (role' : String),
       req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role'))
@@ -1709,7 +1881,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') :
                                     value := Value.primitive (XmlType.string, "Receive") }]]],
                           condition := none, effect := EffectType.permit, obligations := [], advice := [] })
                       [] with
-  | (Decision'.permit, _) => 
+  | (Decision'.permit, _) =>
     simp [PolicyElement.eval, PolicySet.eval]
     match Target.eval
           [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
@@ -1718,7 +1890,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') :
                       type := XmlType.string, issuer := none, must_be_present := true },
                   value := Value.primitive (XmlType.string, "Student") }]]]
           req with
-    | MatchResult.is_match => 
+    | MatchResult.is_match =>
       simp [Target.eval]
       simp [Policy.eval, Target.eval]
       simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
@@ -1742,7 +1914,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') :
                       type := XmlType.string, issuer := none, must_be_present := true },
                   value := Value.primitive (XmlType.string, "Student") }]]]
           req with
-    | MatchResult.is_match => 
+    | MatchResult.is_match =>
       simp [Target.eval]
       simp [Policy.eval, Target.eval]
       simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
@@ -1757,7 +1929,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') :
       all_goals { intro hbad
                   simp [hbad] at h }
     | MatchResult.indeterminate => sorry
-  | (Decision'.not_applicable, _) => 
+  | (Decision'.not_applicable, _) =>
     simp [PolicyElement.eval, PolicySet.eval]
     match Target.eval
           [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
@@ -1766,7 +1938,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') :
                       type := XmlType.string, issuer := none, must_be_present := true },
                   value := Value.primitive (XmlType.string, "Student") }]]]
           req with
-    | MatchResult.is_match => 
+    | MatchResult.is_match =>
       simp [Target.eval]
       simp [Policy.eval, Target.eval]
       simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
@@ -1790,7 +1962,7 @@ theorem student_not_indeterminate (req : Request) (result : Decision') :
 theorem not_applicable_no_effect (xs : List Decision') :
   PolicyCombinatorAlgorithm.eval_legacy_permit_overrides xs =
   PolicyCombinatorAlgorithm.eval_legacy_permit_overrides (xs ++ [Decision'.not_applicable]) := by
-  have append_no_effect (x : Decision') (xs : List Decision') : 
+  have append_no_effect (x : Decision') (xs : List Decision') :
     (x == Decision'.not_applicable) = false
   → List.contains (xs ++ [Decision'.not_applicable]) x
   = List.contains xs x := by
@@ -1799,10 +1971,14 @@ theorem not_applicable_no_effect (xs : List Decision') :
       | nil => simp [h]
       | cons head tail ih =>
         simp [List.contains_cons]
+        -- match (x == head) with
+        -- | true => simp
+        -- | false => simp
+
         cases Classical.em (x == head) with
-        | inl h' => 
+        | inl h' =>
           simp [h']
-        | inr h => 
+        | inr h =>
           simp [h]
           apply ih
   simp [PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
@@ -1832,10 +2008,10 @@ theorem pr' :
        (ElementTree.eval' req compiled_RPSStudent100_element []).1,
        (ElementTree.eval' req compiled_RPSFaculty100_element []).1] := by
   intros req hsod hwf hres
-  cases Classical.em 
+  cases Classical.em
     (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "TA")))
   with
-  | inl h => 
+  | inl h =>
     rw_local
       (ElementTree.eval' req compiled_RPSStudent100_element []).1 = Decision'.not_applicable
       by apply student_not_applicable req (separation_of_duty_imp_other_role_not_in_req req "TA" "Student" hsod (by simp) h)
@@ -1861,7 +2037,7 @@ theorem pr :
   → (ElementTree.eval req compiled_RPSlist100_element).fst == (ElementTree.eval req compiled_RPSlist100_element').fst := by
   intros req hsod hwf h
   simp [compiled_RPSlist100_element, compiled_RPSlist100_element']
-  
+
   rw_local
     compiled_RPSlist100_metadata' = compiled_RPSlist100_metadata
     by rfl
@@ -1871,13 +2047,103 @@ theorem pr :
   rw_local
     compiled_RPSStudent100_element' = compiled_RPSStudent100_element
     by rfl
-  
+
   simp [ElementTree.eval, ElementTree.eval', PolicyElement.eval]
   simp [compiled_RPSlist100_metadata]
   simp [PolicySet.eval, Target.eval]
   apply pr' req hsod hwf h
 
-#check ElementTree.Node
-         (PolicyElement.Rule (Rule.mk [[[(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "ExternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "Receive")))]]] none EffectType.permit [] []))
-         [ElementTree.Node
-           (PolicyElement.Rule (Rule.mk [[[(Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" XmlType.string none True) (Value.primitive (XmlType.string, "ExternalGrades"))), (Match.mk "urn:oasis:names:tc:xacml:1.0:function:string-equal" (AttributeDesignator.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" XmlType.string none True) (Value.primitive (XmlType.string, "Receive")))]]] none EffectType.permit [] [])) []]
+def xml_of_decision (decision : Decision) :=
+  match decision with
+  | Decision.permit           => "<Decision>Permit</Decision>"
+  | Decision.deny             => "<Decision>Deny</Decision>"
+  | Decision.indeterminate    => "<Decision>Indeterminate</Decision>"
+  | Decision.not_applicable   => "<Decision>NotApplicable</Decision>"
+
+def string_of_status_code (code : StatusCode) :=
+  match code with
+  | StatusCode.ok                => "urn:oasis:names:tc:xacml:1.0:status:ok"
+  | StatusCode.missing_attribute => "urn:oasis:names:tc:xacml:1.0:status:missing-attribute"
+  | StatusCode.syntax_error      => "urn:oasis:names:tc:xacml:1.0:status:syntax-error"
+  | StatusCode.processing_error  => "urn:oasis:names:tc:xacml:1.0:status:processing-error"
+
+def xml_of_status (status : List StatusCode) :=
+  match status with
+  | primary :: rest => String.join ["<Status Value=\"", string_of_status_code primary, "\">", xml_of_status rest, "</Status>"]
+  | _ => ""
+
+def xml_of_xmltype : XmlType -> String
+  | XmlType.string            => "http://www.w3.org/2001/XMLSchema#string"
+  | XmlType.boolean           => "http://www.w3.org/2001/XMLSchema#boolean"
+  | XmlType.integer           => "http://www.w3.org/2001/XMLSchema#integer"
+  | XmlType.double            => "http://www.w3.org/2001/XMLSchema#double"
+  | XmlType.time              => "http://www.w3.org/2001/XMLSchema#time"
+  | XmlType.date              => "http://www.w3.org/2001/XMLSchema#date"
+  | XmlType.dateTime          => "http://www.w3.org/2001/XMLSchema#dateTime"
+  | XmlType.dayTimeDuration   => "http://www.w3.org/2001/XMLSchema#dayTimeDuration"
+  | XmlType.yearMonthDuration => "http://www.w3.org/2001/XMLSchema#yearMonthDuration"
+  | XmlType.anyURI            => "http://www.w3.org/2001/XMLSchema#anyURI"
+  | XmlType.hexBinary         => "http://www.w3.org/2001/XMLSchema#hexBinary"
+  | XmlType.base64Binary      => "http://www.w3.org/2001/XMLSchema#base64Binary"
+  | XmlType.rfc822Name        => "urn:oasis:names:tc:xacml:1.0:data-type:rfc822Name"
+  | XmlType.x500Name          => "urn:oasis:names:tc:xacml:1.0:data-type:x500Name"
+  | XmlType.ipAddress         => "urn:oasis:names:tc:xacml:2.0:data-type:ipAddress"
+  | XmlType.dnsName           => "urn:oasis:names:tc:xacml:2.0:data-type:dnsName"
+
+def xml_of_attribute_assignment (assignment : Attribute) :=
+  String.join [
+    "<AttributeAssignment  AttributeId=\"",
+    assignment.identifier,
+    "\" DataType=\"",
+    xml_of_xmltype assignment.value.fst,
+    "\" Category=\"",
+    assignment.category,
+    (match assignment.issuer with
+    | some issuer => String.join ["\" Category=\"", assignment.category]
+    | none => ""),
+    "\">", 
+    "</AttributeAssignment>"
+  ]
+
+def xml_of_obligation (obligation : Obligation) :=
+  String.join [
+    "<Obligation ObligationId=\"",
+    obligation.identifier,
+    "\">",
+    String.join (List.map xml_of_attribute_assignment obligation.assignments),
+    "</Obligation>"
+  ]
+
+def xml_of_obligations (obligations : List Obligation) :=
+  String.join ["<Obligations>", String.join (List.map xml_of_obligation obligations), "</Obligations>"]
+
+def xml_of_advice (advice : Advice) :=
+  String.join [
+    "<Advice AdviceId=\"",
+    advice.identifier,
+    "\">",
+    String.join (List.map xml_of_attribute_assignment advice.assignments),
+    "</Advice>"
+  ]
+
+def xml_of_advices (advices : List Advice) :=
+  String.join ["<AssociatedAdvice>", String.join (List.map xml_of_advice advices), "</AssociatedAdvices>"]
+
+def xml_of_response (response : Result) :=
+  String.join [
+    "<Response>",
+    xml_of_decision response.fst,
+    (match response.snd with
+     | some {status, obligations, advice} =>
+       String.join [
+         (match status with
+          | some status => xml_of_status status
+          | none => ""),
+         xml_of_obligations obligations,
+         xml_of_advices advice
+       ]
+     | none => ""),
+ "</Response>"]
+
+def request := ([(Attribute.mk "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject" "urn:oasis:names:tc:xacml:1.0:subject:subject-id" none (XmlType.rfc822Name, "bs@simpsons.com")), (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "urn:oasis:names:tc:xacml:1.0:resource:resource-id" none (XmlType.anyURI, "file://example/med/record/patient/BartSimpson")), (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "urn:oasis:names:tc:xacml:1.0:action:action-id" none (XmlType.string, "read"))])
+#eval xml_of_response (Decision'.not_applicable, none)