More cleanup

1 files changed, 140 insertions, 99 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index a9b03b4..ff4e78d 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -1,41 +1,12 @@
-inductive XMLType
-  | string            : XMLType
-  | boolean           : XMLType
-  | integer           : XMLType
-  | double            : XMLType
-  | time              : XMLType
-  | date              : XMLType
-  | dateTime          : XMLType
-  | anyURI            : XMLType
-  | hexBinary         : XMLType
-  | base64Binary      : XMLType
-  | dayTimeDuration   : XMLType
-  | yearMonthDuration : XMLType
-  | x500Name          : XMLType
-  | rfc822Name        : XMLType
-  | ipAddress         : XMLType
-  | dnsName           : XMLType
-  | xpathExpression   : XMLType
-deriving BEq, Repr
-
-def Value : Type := XMLType × String
-deriving BEq, Repr
-
-def Value.mk (type : XMLType) (inner : String) : Value := (type, inner)
-
----
-
-structure Attribute where
-  category : String
-  identifier: String
-  issuer : Option String
-  value : List Value
-deriving Repr
-
-def Request : Type := List Attribute
-deriving Repr
-
----
+------------------------------------------------------------------------
+---- Atoms -------------------------------------------------------------
+------------------------------------------------------------------------
+--
+-- # References
+--
+-- - 7.6 Match evaluation
+--
+------------------------------------------------------------------------
 
 inductive MatchResult where
   | is_match      : MatchResult
@@ -56,6 +27,76 @@ deriving BEq, Repr
 def Response : Type := Decision
 deriving Repr
 
+------------------------------------------------------------------------
+---- Values ------------------------------------------------------------
+------------------------------------------------------------------------
+--
+-- From A.2 Data-types: "Although XML instances represent all data-types
+-- as strings, an XACML PDP must operate on types of data that, while
+-- they have string representations, are not just strings. Types such as
+-- Boolean, integer, and double MUST be converted from their XML string
+-- representations to values that can be compared with values in their
+-- domain of discourse, such as numbers."
+--
+-- The standard enumerates the types that must be supported by any
+-- conforming implementaiton. This is represented in `XmlType`, and
+-- `Value` is the representation of a value payload with its associated
+-- type.
+--
+------------------------------------------------------------------------
+
+inductive XmlType
+  | string            : XmlType
+  | boolean           : XmlType
+  | integer           : XmlType
+  | double            : XmlType
+  | time              : XmlType
+  | date              : XmlType
+  | dateTime          : XmlType
+  | anyURI            : XmlType
+  | hexBinary         : XmlType
+  | base64Binary      : XmlType
+  | dayTimeDuration   : XmlType
+  | yearMonthDuration : XmlType
+  | x500Name          : XmlType
+  | rfc822Name        : XmlType
+  | ipAddress         : XmlType
+  | dnsName           : XmlType
+  | xpathExpression   : XmlType
+deriving BEq, Repr
+
+def Value : Type := XmlType × String
+deriving BEq, Repr
+
+def Value.mk (type : XmlType) (inner : String) : Value := (type, inner)
+
+notation:65 "#<" lhs:65 "," rhs:66 ">" => Value.mk lhs rhs
+
+------------------------------------------------------------------------
+---- Attributes---------------------------------------------------------
+------------------------------------------------------------------------
+--
+-- # References
+--
+-- - 5.46 Element <Attribute>
+-- - 5.42 Element <Request>
+--
+-- Attributes are categories into <Attributes> elements. In this
+-- implementation, categories are rolled up - every attribute carries
+-- the category of its enclosing <Attributes> element.
+--
+------------------------------------------------------------------------
+
+structure Attribute where
+  category : String
+  identifier: String
+  issuer : Option String
+  value : List Value
+deriving Repr
+
+def Request : Type := List Attribute
+deriving Repr
+
 ---
 
 def Identifier : Type := String
@@ -78,7 +119,7 @@ inductive CombinatorAlgorithm where
 structure AttributeDesignator where
   category        : String
   identifier      : String
-  type            : XMLType
+  type            : XmlType
   issuer          : Option String
   must_be_present : Bool
 deriving BEq
@@ -88,7 +129,7 @@ def FunctionID : Type := String
 inductive Expression where
   | apply                (function : FunctionID) (args: List Expression) : Expression
   | attribute_designator (inner : AttributeDesignator)                   : Expression
-  | attribute_value      (inner : Value)                            : Expression
+  | attribute_value      (inner : Value)                                 : Expression
   | function             (function : FunctionID)                         : Expression
 
 structure Match where
@@ -96,9 +137,9 @@ structure Match where
   designator: AttributeDesignator
   value: List Value
 deriving BEq
-def AllOf : Type  := List Match -- TODO: Should restrict nonempty.
+def AllOf  : Type := List Match -- TODO: Should restrict nonempty.
 deriving BEq
-def AnyOf : Type  := List AllOf -- TODO: Should restrict nonempty.
+def AnyOf  : Type := List AllOf -- TODO: Should restrict nonempty.
 deriving BEq
 def Target : Type := List AnyOf
 deriving BEq
@@ -129,6 +170,9 @@ structure Policy where
   -- TODO: ObligationExpressions
   -- TODO: AdviceExpressions
 
+def Choice : Type := List Decision
+deriving BEq
+
 ---
 
 def example_4_1_policy :=
@@ -141,26 +185,26 @@ def example_4_1_policy :=
           (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
+            XmlType.rfc822Name
             Option.none
             false)
-          [Value.mk XMLType.string "med.example.com"]]]]
-      (Expression.attribute_value (Value.mk XMLType.boolean "True"))
+          [#<XmlType.string, "med.example.com">]]]]
+      (Expression.attribute_value (#<XmlType.boolean, "True">))
       Decision.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
-                [Value.mk XMLType.rfc822Name "bs@simpsons.com"],
+                [#<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
-                [Value.mk XMLType.anyURI "file://example/med/record/patient/BartSimpson"],
+                [#<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
-                [Value.mk XMLType.string "read"]]
+                [#<XmlType.string, "read">]]
 
 def example_4_1_response := Decision.not_applicable
 
@@ -176,28 +220,28 @@ def example_4_2_policy_rule_1 :=
           (AttributeDesignator.mk
             "urn:oasis:names:tc:xacml:3.0:subject-category:resource"
             "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
-            XMLType.rfc822Name
+            XmlType.rfc822Name
             Option.none
             false)
-          [Value.mk XMLType.anyURI "urn:example:med:schemas:record"],
+          [#<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
+            XmlType.xpathExpression
             Option.none
             false)
-          [Value.mk XMLType.xpathExpression "md:record"]],
+          [#<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
+            XmlType.string
             Option.none
             false)
-          [Value.mk XMLType.string "read"]]]]
+          [#<XmlType.string, "read">]]]]
       (Expression.apply
         "urn:oasis:names:tc:xacml:1.0:function:string-equal"
         [Expression.apply
@@ -206,7 +250,7 @@ def example_4_2_policy_rule_1 :=
             (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
+              XmlType.string
               Option.none
               false)],
           Expression.apply
@@ -215,7 +259,7 @@ def example_4_2_policy_rule_1 :=
             (AttributeDesignator.mk
               "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
               "md:record/md:patient/md:patient-number/text()"
-              XMLType.string
+              XmlType.string
               Option.none
               false)]])
       Decision.permit]
@@ -230,28 +274,28 @@ def example_4_2_policy_rule_2 :=
           (AttributeDesignator.mk
             "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
             "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
-            XMLType.anyURI
+            XmlType.anyURI
             Option.none
             false)
-          [Value.mk XMLType.anyURI "urn:example:med:schemas:record"],
+          [#<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
+            XmlType.xpathExpression
             Option.none
             false)
-           [Value.mk XMLType.xpathExpression "md:record"]]],
+           [#<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
+            XmlType.string
             Option.none
             false)
-          [Value.mk XMLType.string "read"]]]]
+          [#<XmlType.string, "read">]]]]
       (Expression.apply
         "urn:oasis:names:tc:xacml:1.0:function:and"
         [Expression.apply
@@ -262,7 +306,7 @@ def example_4_2_policy_rule_2 :=
               (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
+                XmlType.string
                 Option.none
                 false)]],
           Expression.apply
@@ -271,7 +315,7 @@ def example_4_2_policy_rule_2 :=
               (AttributeDesignator.mk
                 "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
                 "#anonymous-selector-0"
-                XMLType.string
+                XmlType.string
                 Option.none
                 false)]])
       Decision.permit]
@@ -284,38 +328,38 @@ def example_4_2_policy_rule_3 :=
         (AttributeDesignator.mk
           "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
           "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
-          XMLType.anyURI
+          XmlType.anyURI
           Option.none
           false)
-        [Value.mk XMLType.anyURI "urn:example:med:schemas:record"]]]]
+        [#<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
+            XmlType.string
             Option.none
             false)
-          [Value.mk XMLType.string "physician"]]],
+          [#<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
+            XmlType.xpathExpression
             Option.none
             false)
-           [Value.mk XMLType.xpathExpression "md:record"]]],
+           [#<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
+            XmlType.string
             Option.none
             false)
-          [Value.mk XMLType.string "write"]]]]
+          [#<XmlType.string, "write">]]]]
       (Expression.apply
         "urn:oasis:names:tc:xacml:1.0:function:string-equal"
         [Expression.apply
@@ -324,7 +368,7 @@ def example_4_2_policy_rule_3 :=
             (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
+              XmlType.string
               Option.none
               false)],
         Expression.apply
@@ -333,7 +377,7 @@ def example_4_2_policy_rule_3 :=
             (AttributeDesignator.mk
               "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
               "#anonymous-selector-1"
-              XMLType.string
+              XmlType.string
               Option.none
               false)]])
       Decision.permit]
@@ -348,38 +392,38 @@ def example_4_2_policy_rule_4 :=
         (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
+          XmlType.string
           Option.none
           false)
-        [Value.mk XMLType.string "administrator"]]],
+        [#<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
+          XmlType.anyURI
           Option.none
           false)
-        [Value.mk XMLType.anyURI "urn:example:med:schemas:record"],
+        [#<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
+          XmlType.xpathExpression
           Option.none
           false)
-        [Value.mk XMLType.xpathExpression "md:record/md:medical"]]],
+        [#<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
+          XmlType.string
           Option.none
           false)
-        [Value.mk XMLType.string "read"]]]]
-      (Expression.attribute_value (Value.mk XMLType.boolean "True"))
+        [#<XmlType.string, "read">]]]]
+      (Expression.attribute_value (#<XmlType.boolean, "True">))
       Decision.deny]
 
 
@@ -391,29 +435,26 @@ def example_4_2_policy :=
         (AttributeDesignator.mk
           "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
           "urn:oasis:names:tc:xacml:2.0:resource:target-namespace"
-          XMLType.string
+          XmlType.string
           Option.none
           false)
-        [Value.mk XMLType.string "urn:example:med:schema:records"]]]]
+        [#<XmlType.string, "urn:example:med:schema:records">]]]]
 
 ---
 
-def Choice : Type := List Decision
-deriving BEq
-
 -- TODO
 def evaluate_expression (expression : Expression) : Value :=
   match expression with
-    | Expression.apply fn args => Value.mk XMLType.string "True"
+    | Expression.apply fn args => #<XmlType.string, "True">
     | Expression.attribute_designator
         (AttributeDesignator.mk category identifier type issuer must_be_present)
-      => Value.mk XMLType.string "True"
+      => #<XmlType.string, "True">
     | Expression.attribute_value inner => inner
-    | Expression.function _ => Value.mk XMLType.string "True"
+    | Expression.function _ => #<XmlType.string, "True">
 
 -- TODO
 def evaluate_designator (designator : AttributeDesignator) (context : Request) : Value :=
-  Value.mk XMLType.string "True"
+  #<XmlType.string, "True">
   -- match designator with
     -- | AttributeDesignator.mk category identifier type issuer must_be_present
     --   match issuer with
@@ -426,9 +467,9 @@ def evaluate_match (m : Match) (context : Request) : Value :=
 
 def evaluate_all_of (all_of : AllOf) (context : Request) : MatchResult :=
   let result := all_of.map (fun x => evaluate_match x context)
-  if result.all (fun x => x == (XMLType.boolean, "True")) then MatchResult.is_match
-  else if result.all (fun x => x != (XMLType.boolean, "False")) ∧
-          result.elem (XMLType.boolean, "Indeterminate") then MatchResult.indeterminate
+  if result.all (fun x => x == (XmlType.boolean, "True")) then MatchResult.is_match
+  else if result.all (fun x => x != (XmlType.boolean, "False")) ∧
+          result.elem (XmlType.boolean, "Indeterminate") then MatchResult.indeterminate
   else MatchResult.no_match
 
 def evaluate_any_of (any_of : AnyOf) (context : Request) : MatchResult :=
@@ -459,8 +500,8 @@ def evaluate_rule (rule : Rule) (context : Request) : Choice :=
     | MatchResult.is_match =>
       match evaluate_expression rule.condition with
         -- TODO: coe to some strongly typed result?
-        | (XMLType.string, "True") => [rule.effect]
-        | (XMLType.string, "False") => [Decision.not_applicable]
+        | (XmlType.string, "True") => [rule.effect]
+        | (XmlType.string, "False") => [Decision.not_applicable]
         | (_, _) =>
           if rule.effect == Decision.permit then
             [Decision.indeterminate_p] else
@@ -472,7 +513,7 @@ theorem test :
   ∀ r: Rule,
   ∀ c: Request,
     evaluate_target r.target c = MatchResult.is_match
-  ∧ evaluate_expression r.condition = Value.mk XMLType.string "True"
+  ∧ evaluate_expression r.condition = #<XmlType.string, "True">
   → evaluate_rule r c = [r.effect] :=
   by
     intros r c
@@ -481,7 +522,7 @@ theorem test :
     cases (r.target == [])
     { simp
       have h_target_eval : evaluate_target r.target c = MatchResult.is_match := And.left h
-      have h_condition_eval : evaluate_expression r.condition = (XMLType.string, "True") := And.right h
+      have h_condition_eval : evaluate_expression r.condition = (XmlType.string, "True") := And.right h
       simp [h_target_eval]
       simp [h_condition_eval] }
     { simp }