Intro Obligations and Expressions to the type definitions

1 files changed, 74 insertions, 36 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 060a2c2..723fece 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -24,9 +24,6 @@ inductive Decision where
   | not_applicable   : Decision
 deriving BEq, Repr
 
-def Response : Type := Decision
-deriving Repr
-
 ------------------------------------------------------------------------
 ---- Values ------------------------------------------------------------
 ------------------------------------------------------------------------
@@ -104,7 +101,7 @@ deriving Repr
 ---
 
 def Identifier : Type := String
-deriving BEq
+deriving BEq, Repr
 
 inductive CombinatorAlgorithm where
   | deny_overrides                  : CombinatorAlgorithm
@@ -126,58 +123,89 @@ structure AttributeDesignator where
   type            : XmlType
   issuer          : Option String
   must_be_present : Bool
-deriving BEq
+deriving BEq, Repr
 
 def FunctionID : Type := String
-deriving BEq
+deriving BEq, Repr
 
 inductive Expression where
   | apply                (function : FunctionID) (args: List Expression) : Expression
   | attribute_designator (inner : AttributeDesignator)                   : Expression
   | attribute_value      (inner : Value)                                 : Expression
   | function             (function : FunctionID)                         : Expression
-deriving BEq
+deriving BEq, Repr
 
 structure Match where
   function   : Identifier
   designator : AttributeDesignator
   value      : Value
-deriving BEq
-def AllOf  : Type := List Match -- TODO: Should restrict nonempty.
-deriving BEq
-def AnyOf  : Type := List AllOf -- TODO: Should restrict nonempty.
-deriving BEq
+deriving BEq, Repr
+def AllOf  : Type := List Match
+deriving BEq, Repr
+def AnyOf  : Type := List AllOf
+deriving BEq, Repr
 def Target : Type := List AnyOf
-deriving BEq
+deriving BEq, Repr
+
+structure AttributeAssignmentExpression where
+  category        : String
+  identifier      : String
+  issuer          : Option String
+  expression      : Expression
+deriving BEq, Repr
+
+structure ObligationExpression where
+  assignments : List AttributeAssignmentExpression
+  identifier : String
+  fullfill_on : Decision
+deriving BEq, Repr
+
+structure AdviceExpression where
+  assignments : List AttributeAssignmentExpression
+  identifier : String
+  applies_to : Decision
+deriving BEq, Repr
 
+-- n.b. "The <Condition> contains one <Expression> element"
 structure Rule where
-  target : Target
-  -- "The <Condition> contains one <Expression> element"
-  condition : Expression
-  effect : Decision
-  -- TODO: ObligationExpressions
-  -- TODO: AdviceExpressions
+  target      : Target
+  condition   : Expression
+  effect      : Decision
+  obligations : List ObligationExpression
+  advice      : List AdviceExpression
 
 structure PolicySet where
-  combinator : CombinatorAlgorithm
-  target : Target
-  children : List PolicySetChild
-  -- TODO: ObligationExpressions
-  -- TODO: AdviceExpressions
+  combinator  : CombinatorAlgorithm
+  target      : Target
+  children    : List PolicySetChild
+  obligations : List ObligationExpression
+  advice      : List AdviceExpression
 
 inductive PolicySetChild where
   | policy_set (inner : PolicySet) : PolicySetChild
   | policy     (inner : Policy)    : PolicySetChild
 
 structure Policy where
-  combinator : CombinatorAlgorithm
-  target : Target
-  rules : List Rule
-  -- TODO: ObligationExpressions
-  -- TODO: AdviceExpressions
+  combinator  : CombinatorAlgorithm
+  target      : Target
+  rules       : List Rule
+  obligations : List ObligationExpression
+  advice      : List AdviceExpression
+
+def Obligation : Type := String
+deriving BEq, Repr
+def Advice     : Type := String
+deriving BEq, Repr
+
+structure Response where
+  decision    : Decision
+  status      : Option String
+  obligations : List Obligation
+  advice      : List Advice
+deriving BEq, Repr
 
 def Choice : Type := List Decision
-deriving BEq
+deriving BEq, Repr
 
 ---
 
@@ -202,7 +230,9 @@ def example_4_1_policy :=
         ] -- </AnyOf>
       ]
       (Expression.attribute_value (#<XmlType.boolean, "True">))
-      Decision.permit]
+      Decision.permit
+      [] []]
+      [] []
 
 def example_4_1_request :=
   [Attribute.mk "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
@@ -274,7 +304,9 @@ def example_4_2_policy_rule_1 :=
               XmlType.string
               Option.none
               false)]])
-      Decision.permit]
+      Decision.permit
+      [] []]
+    [] []
 
 def example_4_2_policy_rule_2 :=
   Policy.mk
@@ -330,7 +362,9 @@ def example_4_2_policy_rule_2 :=
                 XmlType.string
                 Option.none
                 false)]])
-      Decision.permit]
+      Decision.permit
+      [] []]
+    [] []
 
 def example_4_2_policy_rule_3 :=
   Policy.mk
@@ -392,7 +426,9 @@ def example_4_2_policy_rule_3 :=
               XmlType.string
               Option.none
               false)]])
-      Decision.permit]
+      Decision.permit
+      [] []]
+    [] []
 
 def example_4_2_policy_rule_4 :=
   Policy.mk
@@ -436,8 +472,9 @@ def example_4_2_policy_rule_4 :=
           false)
         (#<XmlType.string, "read">)]]]
       (Expression.attribute_value (#<XmlType.boolean, "True">))
-      Decision.deny]
-
+      Decision.deny
+      [] []]
+    [] []
 
 def example_4_2_policy :=
   PolicySet.mk
@@ -451,6 +488,7 @@ def example_4_2_policy :=
           Option.none
           false)
         (#<XmlType.string, "urn:example:med:schema:records">)]]]
+    [] []
 
 ---