Prove ta_external_grades_not_applicable

1 files changed, 299 insertions, 5 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index efe86d2..3e7b1eb 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -1943,9 +1943,11 @@ def compiled_RPSlist100_element := ((ElementTree.Node compiled_RPSlist100_metada
 -- 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_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, "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, "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_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'
@@ -1957,7 +1959,7 @@ def compiled_gradedp100_element' := ((ElementTree.Node compiled_gradedp100_metad
 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']))
+def compiled_PPSTA100_element' := ((ElementTree.Node compiled_PPSTA100_metadata' [compiled_gradeAsgnAssigngrades_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']))
@@ -2097,6 +2099,83 @@ theorem target_no_match (req : Request) (role : String) :
       apply anyof_no_match req role h_not_role
   simp [hint]
 
+theorem allof_match(req : Request) (role : String) :
+    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, role) }
+      req = some (Value.primitive (XmlType.boolean, "True"))
+  → 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, role) }]
+      req = MatchResult.is_match := by
+  intro h_not_role
+  unfold AllOf.eval
+  simp [h_not_role]
+
+theorem anyof_match (req : Request) (role : String) :
+    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, role) }
+      req = some (Value.primitive (XmlType.boolean, "True"))
+  → AnyOf.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.is_match := by
+  intro h_role
+  unfold AnyOf.eval
+  simp [List.isEmpty]
+  have hint :
+    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, role) }]
+      req = MatchResult.is_match := by
+      apply allof_match req role h_role
+  simp [hint]
+
+theorem target_match (req : Request) (role : String) :
+    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, role) }
+      req = some (Value.primitive (XmlType.boolean, "True"))
+  → 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.is_match := by
+  intro h_role
+  unfold Target.eval
+  simp
+  have hint :
+    AnyOf.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.is_match := by
+      apply anyof_match req role h_role
+  simp [hint]
+
 theorem student_not_applicable (req : Request) :
     Match.eval
       { function := "urn:oasis:names:tc:xacml:1.0:function:string-equal",
@@ -2169,12 +2248,227 @@ theorem ta_not_applicable (req : Request) :
       apply target_no_match req "TA" h_not_role
   simp [hint]
 
+theorem internal_grades_no_match₁ (req : Request) (command : String) :
+    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, "False"))
+  → 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, command) }]
+      req = MatchResult.no_match := by
+  intro hno_internal_grades
+  simp [AllOf.eval, hno_internal_grades]
+  intro hcont
+  contradiction
+
+theorem internal_grades_no_match₂ (req : Request) :
+    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, "False"))
+  → AnyOf.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") }],
+      [{ 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.no_match := by
+  intro hno_internal_grades
+  simp [AnyOf.eval]
+  have hint :
+    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.no_match :=
+    by apply internal_grades_no_match₁ req "Assign" hno_internal_grades
+  simp [hint]
+  have hint :
+    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, "View") }]
+      req = MatchResult.no_match :=
+    by apply internal_grades_no_match₁ req "View" hno_internal_grades
+  simp [hint]
+  rfl
+
+theorem internal_grades_no_match (req : Request) :
+    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, "False"))
+  → 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, "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, "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.no_match := by
+  intro hno_internal_grades
+  simp [Target.eval]
+  have hint :
+    AnyOf.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") }],
+      [{ 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.no_match := by
+    apply internal_grades_no_match₂ req hno_internal_grades
+  simp [hint]
+
 theorem ta_external_grades_not_applicable (req : Request) :
-    well_formed req
-  → 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"))
+    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, "TA") }
+      req = some (Value.primitive (XmlType.boolean, "True"))
+  → 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, "False"))
   → (ElementTree.eval' req compiled_RPSTA100_element' []).1 = Decision'.not_applicable := by
-  sorry
+  intros hta hno_internal_grades
+  simp [ElementTree.eval', PolicyElement.eval, PolicySet.eval,
+        compiled_RPSTA100_element', compiled_RPSTA100_metadata']
+  have hint :
+    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, "TA") }]]]
+      req = MatchResult.is_match :=
+    (by apply target_match req "TA" hta)
+  simp [hint]
+
+  have hint : Target.eval [] req = MatchResult.is_match := by simp [Target.eval]
+
+  simp [ElementTree.eval', PolicyElement.eval, PolicySet.eval, hint,
+        Rule.eval, Policy.eval,
+        compiled_PPSTA100_element', compiled_PPSTA100_metadata',
+        compiled_gradeAsgnAssigngrades_element'', compiled_gradeAsgnAssigngrades_metadata'']
+  have hint :
+    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, "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, "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.no_match := by
+    apply internal_grades_no_match req hno_internal_grades
+  simp [hint]
+
+  simp [PolicyCombinatorAlgorithm.eval_legacy_permit_overrides]
 
 theorem not_applicable_no_effect' (xs : List Decision') :
   PolicyCombinatorAlgorithm.eval_legacy_permit_overrides xs =