Check-in 2023-12-07

1 files changed, 330 insertions, 44 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 10fe136..2a8b8a4 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -9,8 +9,12 @@
 ------------------------------------------------------------------------
 
 import Aesop
+import Mathlib.Data.Prod.Basic
+import Mathlib.Tactic.LibrarySearch
 import Std.Data.List.Basic
 
+macro "rw_local " t:term p:term : tactic => `(tactic| have hint : $t := $p <;> simp [hint] <;> clear hint)
+
 inductive MatchResult where
   | is_match      : MatchResult
   | no_match      : MatchResult
@@ -102,9 +106,47 @@ inductive XmlType
   | dnsName           : XmlType
 deriving BEq, Repr
 
+instance : LawfulBEq XmlType 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
+
 def Primitive : Type := XmlType × String
 deriving BEq, Repr
 
+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
+  apply Iff.intro
+  { simp_all only [beq_iff_eq]
+    intro _
+    trivial }
+  { intro h
+    simp_all only [beq_iff_eq, Prod.eq_iff_fst_eq_snd_eq] }
+
+instance : LawfulBEq Primitive where
+  eq_of_beq := by
+    intros a b h
+    rw [Prod.eq_iff_fst_eq_snd_eq]
+    rw [Prod.beq_iff_fst_eq_snd_eq] at h
+    simp [beq_iff_eq] at h
+    assumption
+  rfl := by
+    intro a
+    rw [Prod.beq_iff_fst_eq_snd_eq]
+    apply And.intro
+    all_goals simp 
+
 def Primitive.mk (type : XmlType) (inner : String) : Primitive := (type, inner)
 
 notation:65 "#<" lhs:65 "," rhs:66 ">" => Primitive.mk lhs rhs
@@ -142,6 +184,10 @@ inductive Value where
   | bag (b : Bag)             : Value
 deriving BEq, Repr
 
+instance : LawfulBEq Value where
+  eq_of_beq := by sorry
+  rfl := by sorry
+
 instance : Coe (Option Value) Value where
   coe b :=
     match b with
@@ -373,6 +419,38 @@ namespace AttributeDesignator
         else Sum.inl $ Value.bag (Bag.mk found)
 end AttributeDesignator
 
+theorem designator_always_returns_bag
+  (designator : AttributeDesignator) (context : List Attribute) (p : Primitive) :
+  designator.eval context ≠ Sum.inl (Value.primitive p) := by
+  simp [AttributeDesignator.eval]
+  match designator with
+  | { must_be_present := true, category, identifier, type, issuer .. } =>
+    simp
+    let check :=
+      List.map (fun x => x.value)
+        (List.filter
+          (fun attr =>
+            decide
+              ((attr.category == category) = true ∧
+                (attr.identifier == identifier) = true ∧
+                  (attr.value.1 == type) = true ∧ ((attr.issuer == none) = true ∨ (attr.issuer == issuer) = true)))
+          context)
+    rw_local
+      List.map (fun x => x.value)
+        (List.filter
+          (fun attr =>
+            decide
+              ((attr.category == category) = true ∧
+                (attr.identifier == identifier) = true ∧
+                  (attr.value.1 == type) = true ∧ ((attr.issuer == none) = true ∨ (attr.issuer == issuer) = true)))
+          context) = check
+      by rfl
+    match check with
+    | List.nil => simp
+    | List.cons a b => simp
+  | { must_be_present := false, .. } =>
+    simp
+
 def matches? (designator : AttributeDesignator) (attr : Attribute) : Prop :=
   designator.category == attr.category ∧
   designator.identifier == attr.identifier ∧
@@ -951,21 +1029,61 @@ def compiled_sturecieveextgrades_element := ((ElementTree.Node compiled_sturecie
 def compiled_stu100_element := ((ElementTree.Node compiled_stu100_metadata [compiled_sturecieveextgrades_element]))
 def compiled_college100_element := ((ElementTree.Node compiled_college100_metadata [compiled_fac100_element, compiled_stu100_element]))
 
-theorem filter_attr (req : Request) (attr : Attribute):
-  req.contains attr →
-  AttributeDesignator.eval
-        { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none,
-          must_be_present := true }
-        req = Sum.inl (Value.bag (Bag.mk [attr.value])) := by sorry
+#eval Expression.eval (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal" [Value.primitive (XmlType.string, "test"), Value.primitive (XmlType.string, "test")]) []
 
-theorem self_eq_self (s : String) (req : Request) :
+theorem string_equal_self (s : String) (req : Request) :
   Expression.eval
     (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal"
       [Value.primitive (XmlType.string, s), Value.primitive (XmlType.string, s)])
     req = some (Value.primitive (XmlType.boolean, "True")) := by
-  sorry
+  simp [Expression.eval, Expression.apply_eval, Primitive.mk]
 
-macro "rw_local " t:term p:term : tactic => `(tactic| have hint : $t := $p <;> simp [hint] <;> clear hint)
+-- #check List.contains_cons
+-- theorem ssdf' {α β : Type} [BEq α] [BEq β] (x y : α) (xs : List α) (f : α → β) : x = y → (x == y) = true := by
+--   intro h
+--   apply?
+
+theorem contains_implies_map_contains {α β : Type} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] (x : α) (xs : List α) (f : α → β) :
+  xs.contains x → (List.map f xs).contains (f x) := by
+  induction xs with
+  | nil =>
+    intro h
+    contradiction
+  | cons x₁ xs₁ ih =>
+    intro h
+    simp [ih] at *
+    cases h with
+    | inl h' => 
+      apply Or.intro_left
+      apply congrArg f
+      assumption
+    | inr h' => 
+      apply Or.intro_right
+      apply ih h'
+
+theorem match_eval_lemma₀ (s : String) (attrs : List Primitive) (req : Request) : 
+  attrs.contains (XmlType.string, s) →
+  List.contains
+    (List.map
+      (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)
+      attrs)
+    (Value.primitive (XmlType.boolean, "True")) := by
+  rw_local
+    (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 
+      rw [eq_comm]
+      simp
+      apply string_equal_self
+  apply contains_implies_map_contains
 
 theorem match_eval (attr : Attribute) (s : String) (req : Request) :
   attr.value = (XmlType.string, s) →
@@ -981,21 +1099,20 @@ 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
-    AttributeDesignator.eval
+  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 = Sum.inl (Value.bag (Bag.mk [attr.value]))
-    by apply filter_attr _ _ h₂
-
-  rw [h₁]
-  rw_local
-    Expression.eval
-      (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal"
-        [Value.primitive (XmlType.string, s), Value.primitive (XmlType.string, s)])
-      req = some (Value.primitive (XmlType.boolean, "True"))
-    by apply self_eq_self _ _
-  rfl
+        req with
+  | Sum.inl (Value.primitive p) => 
+    simp
+    sorry -- contradiction by designator_always_returns_bag
+  | Sum.inl (Value.bag b) => sorry
+  | Sum.inr _ => sorry
+  -- wts: eval results in a list with the attribute in it
+  -- wts: streq map containing attribute contains true
 
 -- Pr2: All members of Faculty can Assign both InternalGrades and ExternalGrades.
 
@@ -1405,31 +1522,31 @@ def compiled_RPSlist100_element := ((ElementTree.Node compiled_RPSlist100_metada
 def compiled_gradeAsgnAssigngrades_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_Assignp100_metadata' := ((PolicyElement.Policy (Policy.mk RuleCombinatorAlgorithm.legacy_permit_overrides [] [] [])))
 def compiled_PPSFaculty100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] [])))
-def compiled_gradeAsgnAssigngrades_element' := ((ElementTree.Node compiled_gradeAsgnAssigngrades_metadata []))
-def compiled_Assignp100_element' := ((ElementTree.Node compiled_Assignp100_metadata [compiled_gradeAsgnAssigngrades_element]))
-def compiled_PPSFaculty100_element' := ((ElementTree.Node compiled_PPSFaculty100_metadata [compiled_Assignp100_element]))
--- root element: compiled_PPSFaculty100_element
+def compiled_gradeAsgnAssigngrades_element' := ((ElementTree.Node compiled_gradeAsgnAssigngrades_metadata' []))
+def compiled_Assignp100_element' := ((ElementTree.Node compiled_Assignp100_metadata' [compiled_gradeAsgnAssigngrades_element']))
+def compiled_PPSFaculty100_element' := ((ElementTree.Node compiled_PPSFaculty100_metadata' [compiled_Assignp100_element']))
+-- root element: compiled_PPSFaculty100_element'
 def compiled_gradedViewgrades_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, "Receive")))]]] none EffectType.permit [] [])))
 def compiled_gradedp100_metadata' := ((PolicyElement.Policy (Policy.mk RuleCombinatorAlgorithm.legacy_permit_overrides [] [] [])))
 def compiled_PPSStudent100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] [])))
-def compiled_gradedViewgrades_element' := ((ElementTree.Node compiled_gradedViewgrades_metadata []))
-def compiled_gradedp100_element' := ((ElementTree.Node compiled_gradedp100_metadata [compiled_gradedViewgrades_element]))
-def compiled_PPSStudent100_element' := ((ElementTree.Node compiled_PPSStudent100_metadata [compiled_gradedp100_element]))
--- root element: compiled_PPSStudent100_element
+def compiled_gradedViewgrades_element' := ((ElementTree.Node compiled_gradedViewgrades_metadata' []))
+def compiled_gradedp100_element' := ((ElementTree.Node compiled_gradedp100_metadata' [compiled_gradedViewgrades_element']))
+def compiled_PPSStudent100_element' := ((ElementTree.Node compiled_PPSStudent100_metadata' [compiled_gradedp100_element']))
+-- root element: compiled_PPSStudent100_element'
 def compiled_PPSTA100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] [])))
-def compiled_PPSTA100_element' := ((ElementTree.Node compiled_PPSTA100_metadata' [compiled_Assignp100_element]))
--- root element: compiled_PPSTA100_element
+def compiled_PPSTA100_element' := ((ElementTree.Node compiled_PPSTA100_metadata' [compiled_Assignp100_element']))
+-- root element: compiled_PPSTA100_element'
 def compiled_RPSFaculty100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.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")))]]] [] [])))
-def compiled_RPSFaculty100_element' := ((ElementTree.Node compiled_RPSFaculty100_metadata [compiled_PPSFaculty100_element]))
--- root element: compiled_RPSFaculty100_element
+def compiled_RPSFaculty100_element' := ((ElementTree.Node compiled_RPSFaculty100_metadata' [compiled_PPSFaculty100_element']))
+-- root element: compiled_RPSFaculty100_element'
 def compiled_RPSStudent100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.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, "Student")))]]] [] [])))
-def compiled_RPSStudent100_element' := ((ElementTree.Node compiled_RPSStudent100_metadata [compiled_PPSStudent100_element]))
--- root element: compiled_RPSStudent100_element
+def compiled_RPSStudent100_element' := ((ElementTree.Node compiled_RPSStudent100_metadata' [compiled_PPSStudent100_element']))
+-- root element: compiled_RPSStudent100_element'
 def compiled_RPSTA100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.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, "TA")))]]] [] [])))
 def compiled_RPSTA100_element' := ((ElementTree.Node compiled_RPSTA100_metadata' [compiled_PPSTA100_element']))
--- root element: compiled_RPSTA100_element
+-- root element: compiled_RPSTA100_element'
 def compiled_RPSlist100_metadata' := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] [])))
-def compiled_RPSlist100_element' := ((ElementTree.Node compiled_RPSlist100_metadata [compiled_RPSFaculty100_element, compiled_RPSStudent100_element, compiled_RPSTA100_element']))
+def compiled_RPSlist100_element' := ((ElementTree.Node compiled_RPSlist100_metadata' [compiled_RPSFaculty100_element', compiled_RPSStudent100_element', compiled_RPSTA100_element']))
 -- root element: compiled_RPSlist100_element
 
 def separation_of_duty (req : Request) :=
@@ -1439,15 +1556,184 @@ def separation_of_duty (req : Request) :=
     req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role'))
     ↔ role = role'
 
+-- 2a3
+-- > -- root element: compiled_PPSTA100_element
+-- 4a6
+-- > -- root element: compiled_RPSTA100_element
+-- 11a14,15
+-- > def compiled_PPSTA100_element := ((ElementTree.Node compiled_PPSTA100_metadata' [compiled_Assignp100_element]))
+-- > def compiled_PPSTA100_metadata := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] [])))
+-- 16c20,22
+-- < def compiled_RPSlist100_element := ((ElementTree.Node compiled_RPSlist100_metadata [compiled_RPSFaculty100_element, compiled_RPSStudent100_element]))
+-- ---
+-- > def compiled_RPSTA100_element := ((ElementTree.Node compiled_RPSTA100_metadata' [compiled_PPSTA100_element']))
+-- > def compiled_RPSTA100_metadata := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.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, "TA")))]]] [] [])))
+-- > def compiled_RPSlist100_element := ((ElementTree.Node compiled_RPSlist100_metadata [compiled_RPSFaculty100_element, compiled_RPSStudent100_element, compiled_RPSTA100_element']))
+
+-- Difference lies solely in compiled_RPSlist100_element.
+
+theorem compiled_RPSFaculty100_element_unchanged :
+  compiled_RPSFaculty100_element = compiled_RPSFaculty100_element' := by rfl
+
+theorem asdf (req : Request) (s₁ s₂ : String) :
+  separation_of_duty req
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, 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₂ 
+   have hint₁ :
+     ∀ (role' : String),
+      req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role'))
+      ↔ s₁ = role' := by apply hsod s₁ hs₁
+   apply (Iff.mp (hint₁ s₂)) hs₂
+
+theorem student_not_applicable (req : Request) :
+  ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"))
+  → (ElementTree.eval' req compiled_RPSStudent100_element []).1 = Decision'.not_applicable := by
+  sorry
+  -- simp [ElementTree.eval', compiled_RPSStudent100_element, compiled_RPSStudent100_metadata, compiled_PPSStudent100_element, compiled_PPSStudent100_metadata, compiled_gradedp100_element, compiled_gradedp100_metadata, PolicyElement.eval, compiled_gradedViewgrades_element, compiled_gradedViewgrades_metadata, PolicySet.eval]
+  -- intro h
+  -- rw_local
+  --   Target.eval
+  --     [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+  --             designator :=
+  --               { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:subject", identifier := "role",
+  --                 type := XmlType.string, issuer := none, must_be_present := true },
+  --             value := Value.primitive (XmlType.string, "Student") }]]]
+  --     req = MatchResult.no_match
+  --   by sorry
+
+theorem faculty_not_applicable (req : Request) :
+  ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty"))
+  → (ElementTree.eval' req compiled_RPSFaculty100_element []).1 = Decision'.not_applicable := by
+  sorry
+
+theorem ta_not_applicable (req : Request) :
+  ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "TA"))
+  → (ElementTree.eval' req compiled_RPSTA100_element []).1 = Decision'.not_applicable := by
+  sorry
+
+theorem ta_external_grades_not_applicable (req : Request) :
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "TA"))
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades"))
+  → (ElementTree.eval' req compiled_RPSTA100_element []).1 = Decision'.not_applicable := by
+  sorry
+
+
+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') : 
+    (x == Decision'.not_applicable) = false
+  → List.contains (xs ++ [Decision'.not_applicable]) x
+  = List.contains xs x := by
+    intro h
+    induction xs with
+      | nil => simp [h]
+      | cons head tail ih =>
+        simp [List.contains_cons]
+        cases Classical.em (x == head) with
+        | inl h' => 
+          simp [h']
+        | inr h => 
+          simp [h]
+          apply ih
+  simp [PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
+  rw_local
+    List.contains (xs ++ [Decision'.not_applicable]) Decision'.permit
+      = List.contains xs Decision'.permit
+    by apply append_no_effect Decision'.permit xs (by rfl)
+  rw_local
+    List.contains (xs ++ [Decision'.not_applicable]) Decision'.deny
+      = List.contains xs Decision'.deny
+    by apply append_no_effect Decision'.deny xs (by rfl)
+  rw_local
+    List.contains (xs ++ [Decision'.not_applicable]) Decision'.indeterminate
+      = List.contains xs Decision'.indeterminate
+    by apply append_no_effect Decision'.indeterminate xs (by rfl)
+  
+theorem pr' :
+  ∀ (req : Request),
+    separation_of_duty req
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades"))
+  → PolicyCombinatorAlgorithm.eval_legacy_permit_overrides
+      [(ElementTree.eval' req compiled_RPSStudent100_element []).1,
+       (ElementTree.eval' req compiled_RPSFaculty100_element []).1]
+  = PolicyCombinatorAlgorithm.eval_legacy_permit_overrides
+      [(ElementTree.eval' req compiled_RPSStudent100_element []).1,
+       (ElementTree.eval' req compiled_RPSFaculty100_element []).1,
+       (ElementTree.eval' req compiled_RPSTA100_element []).1] := by
+  intros req hsod hres
+  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 => 
+    have hint_student :
+      ¬ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student")) := by
+      apply by_contradiction
+      intro hcont'
+      simp at hcont'
+      have hcont : "TA" = "Student" := by
+        apply asdf req "TA" "Student" hsod
+        all_goals assumption
+      contradiction
+    rw_local
+      (ElementTree.eval' req compiled_RPSStudent100_element []).1 = Decision'.not_applicable
+      by apply student_not_applicable req hint_student
+    
+    have hint_faculty :
+      ¬ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Faculty")) := by
+      apply by_contradiction
+      intro hcont'
+      simp at hcont'
+      have hcont : "TA" = "Faculty" := by
+        apply asdf req "TA" "Faculty" hsod
+        all_goals assumption
+      contradiction
+    rw_local
+      (ElementTree.eval' req compiled_RPSFaculty100_element []).1 = Decision'.not_applicable
+      by apply faculty_not_applicable req hint_faculty
+
+    rw_local
+      (ElementTree.eval' req compiled_RPSTA100_element []).1 = Decision'.not_applicable
+      by apply ta_external_grades_not_applicable req h hres
+    rw [not_applicable_no_effect]
+    simp
+  | inr h =>
+    rw_local
+      (ElementTree.eval' req compiled_RPSTA100_element []).1 = Decision'.not_applicable
+      by sorry
+    
+
+  -- cases (ElementTree.eval' req compiled_RPSStudent100_element []).1
+  -- all_goals cases (ElementTree.eval' req compiled_RPSFaculty100_element []).1
+
 theorem pr :
   ∀ (req : Request),
     separation_of_duty req
   → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades"))
   → (ElementTree.eval req compiled_RPSlist100_element).fst == (ElementTree.eval req compiled_RPSlist100_element').fst := by
   intros req hsod h
-  cases Classical.em (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"))) with
-  | inl h' =>
-    cases Classical.em (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Receive"))) with
-    | inl h'' => sorry
-    | inr h'' => sorry
-  | inr h' => sorry
+  simp [compiled_RPSlist100_element, compiled_RPSlist100_element']
+  
+  rw_local
+    compiled_RPSlist100_metadata' = compiled_RPSlist100_metadata
+    by rfl
+  rw_local
+    compiled_RPSFaculty100_element' = compiled_RPSFaculty100_element
+    by rfl
+  rw_local
+    compiled_RPSStudent100_element' = compiled_RPSStudent100_element
+    by rfl
+  
+  simp [ElementTree.eval, ElementTree.eval', PolicyElement.eval]
+  simp [compiled_RPSlist100_metadata]
+  simp [PolicySet.eval]
+  
+  -- cases Classical.em (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, "Student"))) with
+  -- | inl h' =>
+  --   cases Classical.em (req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action" "command" none (XmlType.string, "Receive"))) with
+  --   | inl h'' => sorry
+  --   | inr h'' => sorry
+  -- | inr h' => sorry