Check-in 2023-12-11

1 files changed, 280 insertions, 136 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 2a8b8a4..448f287 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -40,6 +40,10 @@ inductive Decision' where
   | not_applicable   : Decision'
 deriving BEq, Repr
 
+instance : LawfulBEq Decision' where
+  eq_of_beq := by sorry
+  rfl := by sorry
+
 def Decision'.downcast : Decision' → Decision
   | Decision'.permit           => Decision.permit
   | Decision'.deny             => Decision.deny
@@ -223,6 +227,10 @@ structure Attribute where
   value      : Primitive
 deriving BEq, Repr
 
+instance : LawfulBEq Attribute where
+  eq_of_beq := by sorry
+  rfl := by sorry
+
 -- More than one attribute with a particular (category, identifier, issuer) can
 -- exist in a `Request`. Indeed, this is how poly-valued attributes are
 -- represented.
@@ -385,71 +393,69 @@ structure AttributeDesignator where
 deriving BEq, Repr
 
 namespace AttributeDesignator
+  -- A named attribute SHALL match an attribute if the values of their
+  -- respective Category, AttributeId, DataType and Issuer attributes
+  -- match. The attribute designator’s Category MUST match, by
+  -- identifier equality, the Category of the <Attributes> element in
+  -- which the attribute is present. The attribute designator’s
+  -- AttributeId MUST match, by identifier equality, the AttributeId of
+  -- the attribute. The attribute designator’s DataType MUST match, by
+  -- identifier equality, the DataType of the same attribute.
+  --
+  -- If the Issuer attribute is present in the attribute designator,
+  -- then it MUST match, using the
+  -- “urn:oasis:names:tc:xacml:1.0:function:string-equal” function, the
+  -- Issuer of the same attribute. If the Issuer is not present in the
+  -- attribute designator, then the matching of the attribute to the
+  -- named attribute SHALL be governed by AttributeId and DataType
+  -- attributes alone.
+  def matches? (designator : AttributeDesignator) (attr : Attribute) : Bool :=
+       attr.category == designator.category
+    && attr.identifier == designator.identifier
+    && attr.value.fst == designator.type
+    && (attr.issuer == Option.none ∨ attr.issuer == designator.issuer)
+
   def eval (designator : AttributeDesignator) (context : List Attribute) : Sum Value (List StatusCode) :=
-    match designator with
-      | AttributeDesignator.mk category identifier type issuer must_be_present =>
-        let found :=
-          -- A named attribute SHALL match an attribute if the values of
-          -- their respective Category, AttributeId, DataType and Issuer
-          -- attributes match. The attribute designator’s Category MUST
-          -- match, by identifier equality, the Category of the
-          -- <Attributes> element in which the attribute is present. The
-          -- attribute designator’s AttributeId MUST match, by identifier
-          -- equality, the AttributeId of the attribute. The attribute
-          -- designator’s DataType MUST match, by identifier equality, the
-          -- DataType of the same attribute.
-          --
-          -- If the Issuer attribute is present in the attribute
-          -- designator, then it MUST match, using the
-          -- “urn:oasis:names:tc:xacml:1.0:function:string-equal”
-          -- function, the Issuer of the same attribute. If the Issuer is
-          -- not present in the attribute designator, then the matching of
-          -- the attribute to the named attribute SHALL be governed by
-          -- AttributeId and DataType attributes alone.
-          context.filter (fun (attr : Attribute) =>
-                            attr.category == category
-                          ∧ attr.identifier == identifier
-                          ∧ attr.value.fst == type
-                          ∧ (attr.issuer == Option.none ∨ attr.issuer == issuer))
-        let found := found.map (fun x => x.value)
-        if must_be_present then
-          match found with
-            | [] => Sum.inr $ [StatusCode.missing_attribute]
-            | _ => Sum.inl $ Value.bag (Bag.mk found)
-        else Sum.inl $ Value.bag (Bag.mk found)
+    let found := context.filter designator.matches?
+    let found := found.map (fun x => x.value)
+    if designator.must_be_present then
+      match found with
+        | [] => Sum.inr $ [StatusCode.missing_attribute]
+        | _ => Sum.inl $ Value.bag (Bag.mk found)
+    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
+-- 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 ∧
@@ -1556,43 +1562,39 @@ 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.
+def well_formed (req : Request) :=
+  ∃ (role res : String),
+      req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, res))
+    ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role))
 
 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 designator_eval_distrib (req_head : Attribute) (req_tail : Request) (d : AttributeDesignator) :
+  d.matches? req_head = false →
+  AttributeDesignator.eval d (req_head :: req_tail) = AttributeDesignator.eval d req_tail := by
+  intro h
+  simp [AttributeDesignator.eval]
+  cases d.must_be_present with
+  | false => simp_all [not_false_eq_true, List.filter_cons_of_neg]
+  | true  => simp_all [not_false_eq_true, List.filter_cons_of_neg]
+
+theorem match_eval_distrib (req_head : Attribute) (req_tail : Request) (m : Match) :
+  m.designator.matches? req_head = false →
+  Match.eval m (req_head :: req_tail) = Match.eval m req_tail := by
+  intro h
+  simp [Match.eval]
+  rw_local
+      AttributeDesignator.eval m.designator (req_head :: req_tail)
+    = AttributeDesignator.eval m.designator req_tail
+    by apply designator_eval_distrib req_head req_tail m.designator h
+  rfl
 
 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
+  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
@@ -1604,6 +1606,31 @@ theorem student_not_applicable (req : Request) :
   --     req = MatchResult.no_match
   --   by sorry
 
+theorem target_no_match (req : Request) (role : String) :
+  separation_of_duty req
+  → well_formed req
+  → ¬ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role))
+  → 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, role) }]]]
+      req = MatchResult.no_match := by
+  intros hsod hwf h_not_role
+  induction req with
+  | nil => sorry
+  | cons _ _ _ => sorry
+
+theorem student_not_applicable' (req : Request) :
+  separation_of_duty req
+  → well_formed req
+  → ¬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
+  intros hsod hwf hnot_student
+  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]
+  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
@@ -1611,15 +1638,154 @@ theorem faculty_not_applicable (req : Request) :
 
 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
+  → (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
+  → (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 (Decision'.not_applicable :: xs) := by
+  simp [PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
+
+theorem separation_of_duty_imp_other_role_not_in_req' (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 separation_of_duty_imp_other_role_not_in_req (req : Request) (role₁ role₂ : String) :
+  separation_of_duty req
+  →  role₁ ≠ role₂
+  →  req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role₁))
+  → ¬req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role₂)) := by
+  intros hsod hneq hr₁
+  intro hbad
+  have hcont : role₁ = role₂ := by
+    apply separation_of_duty_imp_other_role_not_in_req' req role₁ role₂ hsod
+    all_goals assumption
+  contradiction
+
+theorem student_not_indeterminate (req : Request) (result : Decision') :
+    well_formed req
+  → (ElementTree.eval' req compiled_RPSStudent100_element []).1 = result →
+      result ≠ Decision'.indeterminate
+    ∧ result ≠ Decision'.indeterminate_d
+    ∧ result ≠ Decision'.indeterminate_p
+    ∧ result ≠ Decision'.indeterminate_dp := by
+  unfold well_formed
+  intro hwf
+  simp [ElementTree.eval',
+        compiled_RPSStudent100_element,    compiled_RPSStudent100_metadata,
+        compiled_PPSStudent100_element,    compiled_PPSStudent100_metadata,
+        compiled_gradedp100_element,       compiled_gradedp100_metadata,
+        compiled_gradedViewgrades_element, compiled_gradedViewgrades_metadata]
+  match PolicyElement.eval req
+                      (PolicyElement.Rule
+                        {
+                          target :=
+                            [[[{ function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+                                    designator :=
+                                      { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:resource",
+                                        identifier := "resource-class", type := XmlType.string, issuer := none,
+                                        must_be_present := true },
+                                    value := Value.primitive (XmlType.string, "ExternalGrades") },
+                                  { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+                                    designator :=
+                                      { category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action",
+                                        identifier := "command", type := XmlType.string, issuer := none,
+                                        must_be_present := true },
+                                    value := Value.primitive (XmlType.string, "Receive") }]]],
+                          condition := none, effect := EffectType.permit, obligations := [], advice := [] })
+                      [] with
+  | (Decision'.permit, _) => 
+    simp [PolicyElement.eval, PolicySet.eval]
+    match 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 with
+    | MatchResult.is_match => 
+      simp [Target.eval]
+      simp [Policy.eval, Target.eval]
+      simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
+      intro h
+      repeat' apply And.intro
+      all_goals { intro hbad
+                  simp [hbad] at h }
+    | MatchResult.no_match =>
+      simp [Target.eval]
+      intro h
+      repeat' apply And.intro
+      all_goals { intro hbad
+                  simp [hbad] at h }
+    | MatchResult.indeterminate => sorry
+  | (Decision'.deny, _) =>
+    simp [PolicyElement.eval, PolicySet.eval]
+    match 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 with
+    | MatchResult.is_match => 
+      simp [Target.eval]
+      simp [Policy.eval, Target.eval]
+      simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
+      intro h
+      repeat' apply And.intro
+      all_goals { intro hbad
+                  simp [hbad] at h }
+    | MatchResult.no_match =>
+      simp [Target.eval]
+      intro h
+      repeat' apply And.intro
+      all_goals { intro hbad
+                  simp [hbad] at h }
+    | MatchResult.indeterminate => sorry
+  | (Decision'.not_applicable, _) => 
+    simp [PolicyElement.eval, PolicySet.eval]
+    match 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 with
+    | MatchResult.is_match => 
+      simp [Target.eval]
+      simp [Policy.eval, Target.eval]
+      simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides, PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
+      intro h
+      repeat' apply And.intro
+      all_goals { intro hbad
+                  simp [hbad] at h }
+    | MatchResult.no_match =>
+      simp [Target.eval]
+      intro h
+      repeat' apply And.intro
+      all_goals { intro hbad
+                  simp [hbad] at h }
+    | MatchResult.indeterminate => sorry
+  | (Decision'.indeterminate, _) => sorry
+  | (Decision'.indeterminate_d, _) => sorry
+  | (Decision'.indeterminate_p, _) => sorry
+  | (Decision'.indeterminate_dp, _) => sorry
+
 
 theorem not_applicable_no_effect (xs : List Decision') :
   PolicyCombinatorAlgorithm.eval_legacy_permit_overrides xs =
@@ -1652,69 +1818,48 @@ theorem not_applicable_no_effect (xs : List Decision') :
     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
+  → well_formed 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
+      [(ElementTree.eval' req compiled_RPSTA100_element' []).1,
+       (ElementTree.eval' req compiled_RPSStudent100_element []).1,
+       (ElementTree.eval' req compiled_RPSFaculty100_element []).1] := by
+  intros req hsod hwf 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
+      by apply student_not_applicable req (separation_of_duty_imp_other_role_not_in_req req "TA" "Student" hsod (by simp) h)
     rw_local
       (ElementTree.eval' req compiled_RPSFaculty100_element []).1 = Decision'.not_applicable
-      by apply faculty_not_applicable req hint_faculty
-
+      by apply faculty_not_applicable req (separation_of_duty_imp_other_role_not_in_req req "TA" "Faculty" hsod (by simp) h)
     rw_local
-      (ElementTree.eval' req compiled_RPSTA100_element []).1 = Decision'.not_applicable
+      (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
+      (ElementTree.eval' req compiled_RPSTA100_element' []).1 = Decision'.not_applicable
+      by apply ta_not_applicable req h
+    rw [not_applicable_no_effect']
 
 theorem pr :
   ∀ (req : Request),
     separation_of_duty req
+  → well_formed 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
+  intros req hsod hwf h
   simp [compiled_RPSlist100_element, compiled_RPSlist100_element']
   
   rw_local
@@ -1729,11 +1874,10 @@ theorem pr :
   
   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
+  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 [] [])) []]