Drop examples to make exprimenting easier

1 files changed, 0 insertions, 283 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 387b9a2..285285d 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -326,289 +326,6 @@ deriving BEq, Repr
 
 ---
 
-def example_4_1_policy :=
-  Policy.mk
-    CombinatorAlgorithm.deny_overrides
-    []
-    [Rule.mk
-      [
-        [ -- <AnyOf>
-          [ -- <AllOf>
-            Match.mk
-              "urn:oasis:names:tc:xacml:1.0:function:rfc822Name-match"
-              (AttributeDesignator.mk
-                "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
-                "urn:oasis:names:tc:xacml:1.0:subject:subject-id"
-                XmlType.rfc822Name
-                Option.none
-                false)
-              (#<XmlType.string, "med.example.com">)
-          ] -- </AllOf>
-        ] -- </AnyOf>
-      ]
-      (Expression.attribute_value (#<XmlType.boolean, "True">))
-      EffectType.permit
-      [] []]
-    [] []
-
-def example_4_1_request :=
-  [Attribute.mk "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
-                "urn:oasis:names:tc:xacml:1.0:subject:subject-id"
-                Option.none
-                (#<XmlType.rfc822Name, "bs@simpsons.com">),
-   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-                "urn:oasis:names:tc:xacml:1.0:resource:resource-id"
-                Option.none
-                (#<XmlType.anyURI, "file://example/med/record/patient/BartSimpson">),
-   Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"
-                "urn:oasis:names:tc:xacml:1.0:action:action-id"
-                Option.none
-                (#<XmlType.string, "read">)]
-
-def example_4_1_response := Decision.not_applicable
-
----
-
-def example_4_2_policy_rule_1 :=
-  Policy.mk
-    CombinatorAlgorithm.deny_overrides
-    []
-    [Rule.mk
-      [[[Match.mk
-          "anyURI_equal"
-          (AttributeDesignator.mk
-            "urn:oasis:names:tc:xacml:3.0:subject-category:resource"
-            "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
-            XmlType.rfc822Name
-            Option.none
-            false)
-          (#<XmlType.anyURI, "urn:example:med:schemas:record">),
-        Match.mk
-          "xpath_node_match"
-          (AttributeDesignator.mk
-            "urn:oasis:names:tc:xacml:3.0:subject-category:resource"
-            "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
-            XmlType.xpathExpression
-            Option.none
-            false)
-          (#<XmlType.xpathExpression, "md:record">)],
-        [Match.mk
-          "string_equal"
-          (AttributeDesignator.mk
-            "urn:oasis:names:tc:xacml:3.0:subject-category:action"
-            "urn:oasis:names:tc:xacml:1.0:action:action-id"
-            XmlType.string
-            Option.none
-            false)
-          (#<XmlType.string, "read">)]]]
-      (Expression.apply
-        "urn:oasis:names:tc:xacml:1.0:function:string-equal"
-        [Expression.apply
-          "urn:oasis:names:tc:xacml:1.0:function:string-one-and-only"
-          [Expression.attribute_designator
-            (AttributeDesignator.mk
-              "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
-              "urn:oasis:names:tc:xacml:3.0:example:attribute:patient-number"
-              XmlType.string
-              Option.none
-              false)],
-          Expression.apply
-          "urn:oasis:names:tc:xacml:1.0:function:string-one-and-only"
-          [Expression.attribute_designator
-            (AttributeDesignator.mk
-              "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-              "md:record/md:patient/md:patient-number/text()"
-              XmlType.string
-              Option.none
-              false)]])
-      EffectType.permit
-      [] []]
-    [] []
-
-def example_4_2_policy_rule_2 :=
-  Policy.mk
-    CombinatorAlgorithm.deny_overrides
-    []
-    [Rule.mk
-      [[[Match.mk
-          "anyURI-equal"
-          (AttributeDesignator.mk
-            "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-            "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
-            XmlType.anyURI
-            Option.none
-            false)
-          (#<XmlType.anyURI, "urn:example:med:schemas:record">),
-         Match.mk
-           "xpath-node-match"
-           (AttributeDesignator.mk
-            "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-            "urn:oasis:names:tc:xacml:3.0:content-selector"
-            XmlType.xpathExpression
-            Option.none
-            false)
-          (#<XmlType.xpathExpression, "md:record">)]],
-        [[Match.mk
-          "string-equal"
-          (AttributeDesignator.mk
-            "urn:oasis:names:tc:xacml:3.0:attribute-category:action"
-            "urn:oasis:names:tc:xacml:1.0:action:action-id"
-            XmlType.string
-            Option.none
-            false)
-          (#<XmlType.string, "read">)]]]
-      (Expression.apply
-        "urn:oasis:names:tc:xacml:1.0:function:and"
-        [Expression.apply
-          "urn:oasis:names:tc:xacml:1.0:function:string-equal"
-          [Expression.apply
-            "urn:oasis:names:tc:xacml:1.0:function:string-one-and-only"
-            [Expression.attribute_designator
-              (AttributeDesignator.mk
-                "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
-                "urn:oasis:names:tc:xacml:3.0:example:attribute:parent-guardian-id"
-                XmlType.string
-                Option.none
-                false)]],
-          Expression.apply
-            "urn:oasis:names:tc:xacml:1.0:function:string-one-and-only"
-            [Expression.attribute_designator
-              (AttributeDesignator.mk
-                "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-                "#anonymous-selector-0"
-                XmlType.string
-                Option.none
-                false)]])
-      EffectType.permit
-      [] []]
-    [] []
-
-def example_4_2_policy_rule_3 :=
-  Policy.mk
-    CombinatorAlgorithm.deny_overrides
-    [[[Match.mk
-        "anyURI-equal"
-        (AttributeDesignator.mk
-          "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-          "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
-          XmlType.anyURI
-          Option.none
-          false)
-        (#<XmlType.anyURI, "urn:example:med:schemas:record">)]]]
-    [Rule.mk
-      [[[Match.mk
-          "string-equal"
-          (AttributeDesignator.mk
-            "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
-            "urn:oasis:names:tc:xacml:3.0:example:attribute:role"
-            XmlType.string
-            Option.none
-            false)
-          (#<XmlType.string, "physician">)]],
-       [[Match.mk
-           "xpath-node-match"
-           (AttributeDesignator.mk
-            "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-            "urn:oasis:names:tc:xacml:3.0:content-selector"
-            XmlType.xpathExpression
-            Option.none
-            false)
-          (#<XmlType.xpathExpression, "md:record">)]],
-        [[Match.mk
-          "string-equal"
-          (AttributeDesignator.mk
-            "urn:oasis:names:tc:xacml:3.0:attribute-category:action"
-            "urn:oasis:names:tc:xacml:1.0:action:action-id"
-            XmlType.string
-            Option.none
-            false)
-          (#<XmlType.string, "write">)]]]
-      (Expression.apply
-        "urn:oasis:names:tc:xacml:1.0:function:string-equal"
-        [Expression.apply
-          "urn:oasis:names:tc:xacml:1.0:function:string-one-and-only"
-          [Expression.attribute_designator
-            (AttributeDesignator.mk
-              "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
-              "urn:oasis:names:tc:xacml:3.0:example:attribute:physician-id"
-              XmlType.string
-              Option.none
-              false)],
-        Expression.apply
-          "urn:oasis:names:tc:xacml:1.0:function:string-one-and-only"
-          [Expression.attribute_designator
-            (AttributeDesignator.mk
-              "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-              "#anonymous-selector-1"
-              XmlType.string
-              Option.none
-              false)]])
-      EffectType.permit
-      [] []]
-    [] []
-
-def example_4_2_policy_rule_4 :=
-  Policy.mk
-    CombinatorAlgorithm.deny_overrides
-    []
-    [Rule.mk
-      [[[Match.mk
-        "string-equal"
-        (AttributeDesignator.mk
-          "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
-          "urn:oasis:names:tc:xacml:3.0:example:attribute:role"
-          XmlType.string
-          Option.none
-          false)
-        (#<XmlType.string, "administrator">)]],
-      [[Match.mk
-        "anyURI-equal"
-        (AttributeDesignator.mk
-          "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-          "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
-          XmlType.anyURI
-          Option.none
-          false)
-        (#<XmlType.anyURI, "urn:example:med:schemas:record">),
-        Match.mk
-        "xpath-node-match"
-        (AttributeDesignator.mk
-          "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-          "urn:oasis:names:tc:xacml:3.0:content-selector"
-          XmlType.xpathExpression
-          Option.none
-          false)
-        (#<XmlType.xpathExpression, "md:record/md:medical">)]],
-      [[Match.mk
-        "string-equal"
-        (AttributeDesignator.mk
-          "urn:oasis:names:tc:xacml:3.0:attribute-category:action"
-          "urn:oasis:names:tc:xacml:1.0:action:action-id"
-          XmlType.string
-          Option.none
-          false)
-        (#<XmlType.string, "read">)]]]
-      (Expression.attribute_value (#<XmlType.boolean, "True">))
-      EffectType.deny
-      [] []]
-    [] []
-
-def example_4_2_policy :=
-  PolicySet.mk
-    CombinatorAlgorithm.deny_overrides
-    [[[Match.mk
-        "string-equal"
-        (AttributeDesignator.mk
-          "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
-          "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
-          XmlType.string
-          Option.none
-          false)
-        (#<XmlType.string, "urn:example:med:schema:records">)]]]
-    [] []
-
----
-
 -- Per 7.4 Expression evaluation,
 --
 -- "XACML defines an evaluation result of "Indeterminate", which is said