Check-in 2023-12-06

1 files changed, 545 insertions, 21 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index a210c47..10fe136 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -8,6 +8,9 @@
 --
 ------------------------------------------------------------------------
 
+import Aesop
+import Std.Data.List.Basic
+
 inductive MatchResult where
   | is_match      : MatchResult
   | no_match      : MatchResult
@@ -33,16 +36,17 @@ inductive Decision' where
   | not_applicable   : Decision'
 deriving BEq, Repr
 
+def Decision'.downcast : Decision' → Decision
+  | 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
+
 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
+  coe := Decision'.downcast
 
 inductive EffectType where
   | permit : EffectType
@@ -412,6 +416,12 @@ namespace Expression
            Value.primitive (XmlType.rfc822Name, rhs)] =>
            Value.primitive (lhs == rhs)
         | _ => Value.primitive (#<XmlType.boolean, "Indeterminate">)
+    else if name == "urn:oasis:names:tc:xacml:1.0:function:string-equal" then
+      match args with
+        | [Value.primitive (XmlType.string, lhs),
+           Value.primitive (XmlType.string, rhs)] =>
+           Value.primitive (lhs == rhs)
+        | _ => Value.primitive (#<XmlType.boolean, "Indeterminate">)
     else Option.none
 
   def eval (expression : Expression) (context : Request) : Option Value :=
@@ -528,16 +538,21 @@ namespace AllOf
 
 namespace AnyOf
   def eval (disj : AnyOf) (context : Request) : MatchResult :=
-  match disj with
-    | [] => MatchResult.is_match
-    | List.cons x xs => match x.eval context with
-      | MatchResult.is_match => MatchResult.is_match
-      | MatchResult.no_match =>
-        let rest := AnyOf.eval xs context
-        if rest == MatchResult.is_match then MatchResult.no_match else rest
-      | MatchResult.indeterminate =>
-        let rest := AnyOf.eval xs context
-        if rest == MatchResult.no_match then MatchResult.indeterminate else rest
+  -- match disj with
+  --   | [] => MatchResult.is_match
+  --   | List.cons x xs => match x.eval context with
+  --     | MatchResult.is_match => MatchResult.is_match
+  --     | MatchResult.no_match =>
+  --       let rest := AnyOf.eval xs context
+  --       if rest == MatchResult.no_match then MatchResult.no_match else rest
+  --     | MatchResult.indeterminate =>
+  --       let rest := AnyOf.eval xs context
+  --       if rest == MatchResult.no_match then MatchResult.indeterminate else rest
+    if disj.isEmpty then MatchResult.is_match else
+      let result := disj.map (fun x => x.eval context)
+      if result.any (fun x => x == MatchResult.is_match) then MatchResult.is_match
+      else if result.elem MatchResult.indeterminate then MatchResult.indeterminate
+      else MatchResult.no_match
 end AnyOf
 
 namespace Target
@@ -925,5 +940,514 @@ def combine_response_aux (x y : ResultAuxiliary) : ResultAuxiliary :=
 def Choice : Type := List (Decision × ResultAuxiliary)
 deriving BEq, Repr
 
-def 2asdf := 2
-#check 1-2
+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")))]]] [] [])))
+def compiled_sturecieveextgrades_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_stu100_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, "Student")))]]] [] [])))
+def compiled_college100_metadata := ((PolicyElement.PolicySet (PolicySet.mk PolicyCombinatorAlgorithm.legacy_permit_overrides [] [] [])))
+def compiled_facassignviewgrades_element := ((ElementTree.Node compiled_facassignviewgrades_metadata []))
+def compiled_fac100_element := ((ElementTree.Node compiled_fac100_metadata [compiled_facassignviewgrades_element]))
+def compiled_sturecieveextgrades_element := ((ElementTree.Node compiled_sturecieveextgrades_metadata []))
+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
+
+theorem self_eq_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
+
+macro "rw_local " t:term p:term : tactic => `(tactic| have hint : $t := $p <;> simp [hint] <;> clear hint)
+
+theorem match_eval (attr : Attribute) (s : String) (req : Request) :
+  attr.value = (XmlType.string, s) →
+  req.contains attr →
+  Match.eval { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
+               designator :=
+                 { category := attr.category,
+                   identifier := attr.identifier,
+                   type := XmlType.string,
+                   issuer := none,
+                   must_be_present := true },
+               value := Value.primitive attr.value }
+             req = some (Value.primitive (XmlType.boolean, "True")) := by
+  intros h₁ h₂
+  simp [Match.eval]
+  rw_local
+    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
+
+-- Pr2: All members of Faculty can Assign both InternalGrades and ExternalGrades.
+
+theorem pr₂_lemma₀ (req : Request) :
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign"))
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades"))
+  → AllOf.eval
+      [{ 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, "InternalGrades") },
+        { 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, "Assign") }]
+      req = MatchResult.is_match := by
+  intros h₁ h₂
+  simp [AllOf.eval]
+  rw_local
+    Match.eval
+      { 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, "InternalGrades") }
+      req = some (Value.primitive (XmlType.boolean, "True"))
+    by
+      let attr := (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades"))
+      have hint : attr.value = (XmlType.string, "InternalGrades") := by rfl
+      have h₂' : req.contains attr := by apply h₂
+      apply match_eval attr "InternalGrades" req hint h₂'
+  rw_local
+    Match.eval
+      { 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, "Assign") }
+      req = some (Value.primitive (XmlType.boolean, "True"))
+    by
+      let attr := ({ category := "urn:oasis:names:tc:xacml:3.0:attribute-category:action", identifier := "command", issuer := none, value := (XmlType.string, "Assign") } : Attribute)
+      have hint : attr.value = (XmlType.string, "Assign") := by rfl
+      have h₁' : req.contains attr := by apply h₁
+      apply match_eval attr "Assign" req hint h₁'
+
+theorem pr₂_lemma₁ (req : Request) :
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign"))
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades"))
+  → Target.eval
+      [[[{ 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, "Assign") }],
+       [{ 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, "InternalGrades") },
+         { 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, "Assign") }],
+       [{ 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, "View") }],
+       [{ 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, "InternalGrades") },
+         { 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, "View") }]]]
+       req = MatchResult.is_match := by
+    intros h₂ h₃
+    simp [Target.eval, AnyOf.eval]
+    cases (AllOf.eval
+                [{ 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, "Assign") }]
+                req)
+    with
+    | is_match => simp
+    | _ =>
+      simp
+      rw_local
+        AllOf.eval
+          [{ 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, "InternalGrades") },
+            { 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, "Assign") }]
+          req = MatchResult.is_match
+        by apply pr₂_lemma₀ req h₂ h₃
+
+theorem pr₂_lemma₂ (req : Request) :
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign"))
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades"))
+  → (ElementTree.eval' req compiled_facassignviewgrades_element []).fst = Decision'.permit := by
+  intros h₂ h₃
+  simp [compiled_facassignviewgrades_element, compiled_facassignviewgrades_metadata]
+  simp [ElementTree.eval,
+        ElementTree.eval',
+        PolicyElement.eval,
+        Rule.eval]
+  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: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, "Assign") }],
+       [{ 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, "InternalGrades") },
+         { 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, "Assign") }],
+       [{ 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, "View") }],
+       [{ 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, "InternalGrades") },
+         { 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, "View") }]]]
+       req = MatchResult.is_match
+    by apply pr₂_lemma₁ req h₂ h₃
+  simp [Primitive.mk]
+
+theorem pr₂_lemma₃ (req : Request) :
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Faculty"))
+  → AllOf.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, "Faculty") }]
+      req = MatchResult.is_match := by
+  intro h₁
+  simp [AllOf.eval]
+  rw_local
+    Match.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, "Faculty") }
+      req = some (Value.primitive (XmlType.boolean, "True"))
+    by
+      let attr := (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Faculty"))
+      have hint : attr.value = (XmlType.string, "Faculty") := by rfl
+      have h₂' : req.contains attr := by apply h₁
+      apply match_eval attr "Faculty" req hint h₂'
+
+theorem pr₂_lemma₄ (req : Request) :
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Faculty"))
+  → 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, "Faculty") }]]]
+        req = MatchResult.is_match := by
+  intros h₁
+  simp [Target.eval, AnyOf.eval]
+  rw_local
+    (AllOf.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, "Faculty") }]
+      req = MatchResult.is_match)
+    by apply pr₂_lemma₃ req h₁
+
+theorem pr₂_lemma₅ (req : Request) :
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Faculty"))
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign"))
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades"))
+  → (ElementTree.eval' req compiled_fac100_element []).fst = Decision'.permit := by
+  intros h₁ h₂ h₃
+  simp [compiled_fac100_element, compiled_fac100_metadata]
+  simp [ElementTree.eval,
+        ElementTree.eval',
+        PolicyElement.eval]
+
+  simp [Policy.eval]
+  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, "Faculty") }]]]
+        req = MatchResult.is_match
+    by apply pr₂_lemma₄ req h₁
+
+  simp [RuleCombinatorAlgorithm.eval_legacy_permit_overrides]
+  rw_local
+    (ElementTree.eval' req compiled_facassignviewgrades_element []).fst = Decision'.permit
+    by apply pr₂_lemma₂ req h₂ h₃
+
+theorem pr₂ (req : Request) :
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Faculty"))
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign"))
+  → req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "InternalGrades"))
+  → (ElementTree.eval req compiled_college100_element).fst == Decision'.permit := by
+  intros h₁ h₂ h₃
+  simp [compiled_college100_element,
+        compiled_college100_metadata,
+        ElementTree.eval,
+        ElementTree.eval',
+        PolicyElement.eval,
+        PolicySet.eval,
+        Target.eval,
+        PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
+  rw_local
+    (ElementTree.eval' req compiled_fac100_element []).fst = Decision'.permit
+    by apply pr₂_lemma₅ req h₁ h₂ h₃
+
+-- Pr1: There do not exist members of Student who can Assign ExternalGrades. (This is violated, so we show a counterexample.)
+
+def bad_req :=
+  [Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Student"),
+   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Receive"),
+   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign"),
+   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")]
+
+theorem pr₁ :
+  ∃ (req : Request),
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Student"))
+  ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign"))
+  ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades"))
+  ∧ (ElementTree.eval req compiled_college100_element).fst == Decision'.permit := by
+  have h₁ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Student")) := by
+    { simp }
+  have h₂ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign")) := by
+    { simp }
+  have h₃ : bad_req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by
+    { simp }
+
+  apply Exists.intro bad_req
+  apply And.intro
+  { apply h₁ }
+  apply And.intro
+  { apply h₂ }
+  apply And.intro
+  { apply h₃ }
+  rfl
+
+-- Pr3: No combination of roles exists such that a user with those roles can both Receive and Assign the resource ExternalGrades.
+
+def roles (req : Request) :=
+  req.filter
+    (fun attr =>
+      match attr with
+      | { category, identifier, .. } => identifier = "role" && category = "urn:oasis:names:tc:xacml:3.0:attribute-category:subject")
+
+def bad_req₀ :=
+  [Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Student"),
+   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Faculty"),
+   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Receive"),
+   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")]
+
+def bad_req₁ :=
+  [Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Student"),
+   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Faculty"),
+   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign"),
+   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")]
+
+theorem pr₃ :
+  ∃ (user_roles : List Attribute),
+     ((∃ (req : Request),
+         user_roles ⊆ roles req
+       ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Receive"))
+       ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades"))
+       ∧ (ElementTree.eval req compiled_college100_element).fst == Decision'.permit)
+    ∧ (∃ (req : Request),
+         user_roles ⊆ roles req
+       ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign"))
+       ∧ req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades"))
+       ∧ (ElementTree.eval req compiled_college100_element).fst == Decision'.permit))
+ := by
+   let bad_roles :=
+     ([Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role" none (XmlType.string, "Student"),
+       Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role" none (XmlType.string, "Faculty")])
+
+   apply Exists.intro bad_roles
+   apply And.intro
+   { apply Exists.intro bad_req₀
+
+     have h₁ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Student")) := by
+       { simp }
+     have h₂ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Receive")) := by
+       { simp }
+     have h₃ : bad_req₀.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by
+       { simp }
+
+     apply And.intro
+     { rw_local
+       roles bad_req₀ = bad_roles
+       by rfl }
+     apply And.intro
+     { apply h₁ }
+     apply And.intro
+     { apply h₂ }
+     rfl}
+   { apply Exists.intro bad_req₁
+
+     have h₁ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject"  "role"           none (XmlType.string, "Student")) := by
+       { simp }
+     have h₂ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"   "command"        none (XmlType.string, "Assign")) := by
+       { simp }
+     have h₃ : bad_req₁.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource" "resource-class" none (XmlType.string, "ExternalGrades")) := by
+       { simp }
+
+     apply And.intro
+     { rw_local
+       roles bad_req₁ = bad_roles
+       by rfl }
+     apply And.intro
+     { apply h₁ }
+     apply And.intro
+     { apply h₂ }
+     rfl}
+
+--- Property: Adding TAs should not affect ExternalGrades in any way.
+
+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_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_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_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_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]))
+-- root element: compiled_RPSlist100_element
+
+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_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_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_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_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_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
+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']))
+-- root element: compiled_RPSlist100_element
+
+def separation_of_duty (req : Request) :=
+  ∀ (role : String),
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role))
+  → ∀ (role' : String),
+    req.contains (Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:subject" "role" none (XmlType.string, role'))
+    ↔ role = role'
+
+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