Check-in 2023-12-21

2 files changed, 234 insertions, 95 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 42c5150..d4c34da 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -206,21 +206,49 @@ deriving BEq, DecidableEq, Repr
 -- def Bag.beq (b₁ b₂ : Bag) : Bool :=
 --   b₁.contents.all (fun x => b₂.contents.count x == b₁.contents.count x)
 
-#check {1, 2, 3}
+-- instance : BEq Bag where
+--   beq := Bag.beq
 
-instance : BEq Bag where
-  beq := Bag.beq
-
--- instance : LawfulBEq Bag where
---   eq_of_beq := by
---     intros a b h
-    
---   rfl := by sorry
+instance : LawfulBEq Bag where
+  eq_of_beq := by
+    intros a b h
+    match a with
+    | { contents := contents_a } =>
+      match b with
+      | { contents := contents_b } =>
+        simp
+        rw [←beq_iff_eq]
+        apply h
+  rfl := by
+    intro a
+    match a with
+    | { contents := contents_a } =>
+      unfold_projs
+      reduce
+      induction contents_a with
+      | nil => rfl
+      | cons hd tl ih =>
+        unfold List.beq
+        simp [ih]
 
 inductive Value where
   | primitive (p : Primitive) : Value
   | bag (b : Bag)             : Value
-deriving DecidableEq, BEq, Repr
+deriving DecidableEq, Repr
+
+def Value.beq (v₁ v₂ : Value) : Bool :=
+  match v₁ with
+  | Value.primitive p₁ =>
+    match v₂ with
+    | Value.primitive p₂ => p₁ == p₂
+    | Value.bag _ => false
+  | Value.bag b₁ =>
+    match v₂ with
+    | Value.primitive _ => false
+    | Value.bag b₂ => b₁ == b₂
+
+instance : BEq Value where
+  beq := Value.beq
 
 instance : LawfulBEq Value where
   eq_of_beq := by
@@ -228,18 +256,25 @@ instance : LawfulBEq Value where
     cases a with
     | primitive pa =>
       cases b with
-      | primitive pb => 
+      | primitive pb =>
         simp
         exact (beq_iff_eq pa pb).mp h
       | bag bb => contradiction
     | bag ba =>
       cases b with
       | primitive pb => contradiction
-      | bag bb => 
+      | bag bb =>
         simp
-        sorry
-        -- exact (beq_iff_eq ba bb).mp h
-  rfl := by sorry
+        exact (beq_iff_eq ba bb).mp h
+  rfl := by
+    intro a
+    cases a with
+    | primitive pa =>
+      unfold_projs
+      simp [Value.beq]
+    | bag ba =>
+      unfold_projs
+      simp [Value.beq]
 
 instance : Coe (Option Value) Value where
   coe b :=
@@ -274,11 +309,47 @@ structure Attribute where
   identifier : String
   issuer     : Option String
   value      : Primitive
-deriving DecidableEq, BEq, Repr
+deriving DecidableEq, Repr
+
+def Attribute.beq (a₁ a₂ : Attribute) : Bool :=
+  match a₁ with
+  | { category := category₁,
+      identifier := identifier₁,
+      issuer := issuer₁,
+      value := value₁ } =>
+    match a₂ with
+    | { category := category₂,
+        identifier := identifier₂,
+        issuer := issuer₂,
+        value := value₂ } =>
+       category₁   == category₂
+    && identifier₁ == identifier₂
+    && issuer₁     == issuer₂
+    && value₁      == value₂
+
+instance : BEq Attribute where
+  beq := Attribute.beq
 
 instance : LawfulBEq Attribute where
-  eq_of_beq := by sorry
-  rfl := by sorry
+  eq_of_beq := by
+    intros a b h
+    match a with
+    | { category := category_a,
+        identifier := identifier_a,
+        issuer := issuer_a,
+        value := value_a } =>
+      match b with
+      | { category := category_b,
+          identifier := identifier_b,
+          issuer := issuer_b,
+          value := value_b } =>
+        unfold_projs at h
+        simp [Attribute.beq] at *
+        simp_all only [and_self]
+  rfl := by
+    intro a
+    unfold_projs
+    simp [Attribute.beq]
 
 -- More than one attribute with a particular (category, identifier, issuer) can
 -- exist in a `Request`. Indeed, this is how poly-valued attributes are
@@ -543,16 +614,16 @@ deriving DecidableEq, BEq, Repr
 
 namespace Expression
   def apply_eval (name : FunctionID) (args : List Value) : Option Value :=
-    if name == "urn:oasis:names:tc:xacml:1.0:function:rfc822Name-match" then
+    if name == "urn:oasis:names:tc:xacml:1.0:function:string-equal" then
       match args with
-        | [Value.primitive (XmlType.string,     lhs),
-           Value.primitive (XmlType.rfc822Name, rhs)] =>
+        | [Value.primitive (XmlType.string, lhs),
+           Value.primitive (XmlType.string, rhs)] =>
            Value.primitive (lhs == rhs)
         | _ => Value.primitive (#<XmlType.boolean, "Indeterminate">)
-    else if name == "urn:oasis:names:tc:xacml:1.0:function:string-equal" then
+    else if name == "urn:oasis:names:tc:xacml:1.0:function:anyURI-equal" then
       match args with
-        | [Value.primitive (XmlType.string, lhs),
-           Value.primitive (XmlType.string, rhs)] =>
+        | [Value.primitive (XmlType.anyURI, lhs),
+           Value.primitive (XmlType.anyURI, rhs)] =>
            Value.primitive (lhs == rhs)
         | _ => Value.primitive (#<XmlType.boolean, "Indeterminate">)
     else Option.none
@@ -704,7 +775,7 @@ namespace AnyOf
       else MatchResult.no_match
 end AnyOf
 
-theorem elem_imp_nonempty 
+theorem elem_imp_nonempty
   {α : Type}
   (x : α) (xs : List α) :
   x ∈ xs → xs.isEmpty = false := by
@@ -712,7 +783,7 @@ theorem elem_imp_nonempty
   | nil => simp
   | cons _ _ _ => simp [List.isEmpty]
 
-theorem elem_map 
+theorem elem_map
   {α β : Type}
   [BEq α] [LawfulBEq α]
   [BEq β] [LawfulBEq β]
@@ -732,9 +803,9 @@ theorem elem_map
       simp [List.contains] at *
       apply ih h
 
-theorem elem_imp_forall_not 
+theorem elem_imp_forall_not
   {α β : Type}
-  [BEq α] [LawfulBEq α] 
+  [BEq α] [LawfulBEq α]
   [BEq β] [LawfulBEq β]
   (y : β) (xs : List α) (f : α → β) :
   (∀ (x : α), x ∈ xs → f x ≠ y) →
@@ -774,7 +845,7 @@ theorem table_1_target_match_table₂ (disj : List AllOf) (context : Request) :
 
     let ⟨x, hx⟩ := h_indet
 
-    have hbranch : 
+    have hbranch :
       List.elem MatchResult.indeterminate
                 (List.map (fun x => AllOf.eval x context) disj)
               = true := by
@@ -799,11 +870,11 @@ theorem table_1_target_match_table₃ (disj : List AllOf) (context : Request) :
     simp [AnyOf.eval]
 
     simp [h_nonempty]
-    have h_no_match : 
+    have h_no_match :
       ¬ ∃ a, a ∈ disj ∧ AllOf.eval a context = MatchResult.is_match := by
       simp
       apply h_no_match
-    have h_no_indet : 
+    have h_no_indet :
       List.elem MatchResult.indeterminate
                 (List.map (fun x => AllOf.eval x context) disj)
         = false := by
@@ -903,6 +974,27 @@ structure ResultAuxiliary' where
   advice      : List AdviceExpression
 deriving DecidableEq, BEq, Repr
 
+def collect_option {α : Type} (xs : List (Option α)) : Option (List α) :=
+  match xs with
+  | [] => some []
+  | some x :: xs' =>
+    match collect_option xs' with
+    | some xs' => some (x :: xs')
+    | none => none
+  | none :: _ => none
+
+namespace ResultAuxiliary'
+  def eval (result : ResultAuxiliary') (context : Request) : Option ResultAuxiliary :=
+    let advice :=
+      collect_option (List.map (fun x => AdviceExpression.eval x context) result.advice)
+    let obligations :=
+      collect_option (List.map (fun x => ObligationExpression.eval x context) result.obligations)
+    match (obligations, advice) with
+    | (some obligations, some advice) =>
+      some { status := result.status, obligations, advice }
+    | _ => none
+end ResultAuxiliary'
+
 structure MissingAttributeDetail where
   category   : String
   identifier : String
@@ -1239,29 +1331,67 @@ theorem contains_implies_map_contains {α β : Type} [BEq α] [LawfulBEq α] [BE
       apply Or.intro_right
       apply ih h'
 
-theorem match_eval_lemma₀ (s : String) (attrs : List Primitive) (req : Request) :
-  attrs.contains (XmlType.string, s) →
-  List.contains
-    (List.map
-      (fun attr_1 =>
-        Expression.eval
-          (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal"
-            [Value.primitive (XmlType.string, s), Value.primitive attr_1])
-          req)
-      attrs)
-    (Value.primitive (XmlType.boolean, "True")) := by
+theorem attribute_designator_matches (attr : Attribute) (s : String) :
+  attr.value = (XmlType.string, s) →
+  attr.issuer = none →
+  AttributeDesignator.matches?
+    { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none, must_be_present := true }
+    attr = true := by
+  intro h
+  unfold AttributeDesignator.matches?
+  simp [h]
+
+theorem filter_elem {α : Type} (x : α) (xs : List α) (f : α → Bool) :
+  x ∈ xs → f x = true → (x ∈ (List.filter f xs)) := by
+  induction xs with
+  | nil => simp
+  | cons hd tl ih =>
+    intros h₁ h₂
+    unfold List.filter
+    simp_all only [forall_true_left, List.mem_cons]
+    cases h₁ with
+    | inl h =>
+      subst h
+      simp_all only [List.mem_cons, true_or]
+    | inr h =>
+      simp_all only [forall_true_left]
+      split
+      { simp_all only [List.mem_cons, or_true] }
+      { simp_all only }
+
+theorem attribute_designator_eval (attr : Attribute) (s : String) (req : Request) :
+  attr.value = (XmlType.string, s) →
+  req.elem attr →
+  AttributeDesignator.eval
+    { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none, must_be_present := true }
+    req = Sum.inl (Value.primitive (XmlType.boolean, "True")) := by
+  intros h₁ h₂
+  unfold AttributeDesignator.eval
+  simp
+
+  let filter :=
+    (List.filter
+      (AttributeDesignator.matches?
+        { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none,
+          must_be_present := true })
+      req)
+  let filtermap := List.map (fun x => x.value) filter
   rw_local
-    (some (Value.primitive (XmlType.boolean, "True"))) =
-    ((fun attr_1 =>
-       Expression.eval
-         (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal"
-           [Value.primitive (XmlType.string, s), Value.primitive attr_1])
-         req) (XmlType.string, s))
-    by
-      rw [eq_comm]
-      simp
-      apply string_equal_self
-  apply contains_implies_map_contains
+    List.map (fun x => x.value)
+      (List.filter
+        (AttributeDesignator.matches?
+          { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none,
+            must_be_present := true })
+        req) = filtermap
+    by rfl
+
+  have h : attr ∈ filter := by
+    apply filter_elem
+    apply h₁
+
+  -- have h : attr.value ∈ filtermap := by
+
+
 
 theorem match_eval (attr : Attribute) (s : String) (req : Request) :
   attr.value = (XmlType.string, s) →
@@ -1280,6 +1410,7 @@ theorem match_eval (attr : Attribute) (s : String) (req : Request) :
   rw_local
     attr.value = (XmlType.string, s)
     by apply h₁
+
   match AttributeDesignator.eval
         { category := attr.category, identifier := attr.identifier, type := XmlType.string, issuer := none,
           must_be_present := true }
@@ -1287,7 +1418,26 @@ theorem match_eval (attr : Attribute) (s : String) (req : Request) :
   | Sum.inl (Value.primitive p) =>
     simp
     sorry -- contradiction by designator_always_returns_bag
-  | Sum.inl (Value.bag b) => sorry
+  | Sum.inl (Value.bag b) =>
+    simp
+    let f := ((fun x =>
+                  match x with
+                  | none => Value.primitive (#<XmlType.boolean,"Indeterminate">)
+                  | some a => a) ∘
+                fun attr =>
+                Expression.eval
+                  (Expression.apply "urn:oasis:names:tc:xacml:1.0:function:string-equal"
+                    [Value.primitive (XmlType.string, s), Value.primitive attr])
+                  req)
+    have h_branch :
+      List.elem (Value.primitive (#<XmlType.boolean,"True">))
+            (List.map f b.contents) =
+          true := by
+
+
+
+    simp [h_branch]
+    simp [Primitive.mk]
   | Sum.inr _ => sorry
   -- wts: eval results in a list with the attribute in it
   -- wts: streq map containing attribute contains true
@@ -2067,11 +2217,24 @@ def string_of_status_code (code : StatusCode) :=
   | StatusCode.syntax_error      => "urn:oasis:names:tc:xacml:1.0:status:syntax-error"
   | StatusCode.processing_error  => "urn:oasis:names:tc:xacml:1.0:status:processing-error"
 
-def xml_of_status (status : List StatusCode) :=
+def xml_of_status_code (status : List StatusCode) :=
   match status with
-  | primary :: rest => String.join ["<Status Value=\"", string_of_status_code primary, "\">", xml_of_status rest, "</Status>"]
+  | primary :: [] => String.join [
+    "<StatusCode Value=\"",
+    string_of_status_code primary,
+    "\"/>"]
+  | primary :: rest => String.join [
+    "<StatusCode Value=\"",
+    string_of_status_code primary,
+    "\">",
+    xml_of_status_code rest, "</StatusCode>"]
   | _ => ""
 
+def xml_of_status (status : List StatusCode) :=
+  match status with
+  | [] => ""
+  | codes => String.join ["<Status>", xml_of_status_code codes, "</Status>"]
+
 def xml_of_xmltype : XmlType -> String
   | XmlType.string            => "http://www.w3.org/2001/XMLSchema#string"
   | XmlType.boolean           => "http://www.w3.org/2001/XMLSchema#boolean"
@@ -2099,10 +2262,9 @@ def xml_of_attribute_assignment (assignment : Attribute) :=
     "\" Category=\"",
     assignment.category,
     (match assignment.issuer with
-    | some issuer => String.join ["\" Category=\"", assignment.category]
+    | some issuer => String.join ["\" Issuer=\"", issuer]
     | none => ""),
-    "\">", 
-    "</AttributeAssignment>"
+    "\"/>"
   ]
 
 def xml_of_obligation (obligation : Obligation) :=
@@ -2127,23 +2289,27 @@ def xml_of_advice (advice : Advice) :=
   ]
 
 def xml_of_advices (advices : List Advice) :=
-  String.join ["<AssociatedAdvice>", String.join (List.map xml_of_advice advices), "</AssociatedAdvices>"]
+  String.join ["<AssociatedAdvice>", String.join (List.map xml_of_advice advices), "</AssociatedAdvice>"]
 
 def xml_of_response (response : Result) :=
   String.join [
-    "<Response>",
+    "<Response xmlns=\"urn:oasis:names:tc:xacml:3.0:core:schema:wd-17\" xmlns:xsi=\"http://www.w3.org/2001/XMLSchema-instance\">",
+    "<Result>",
     xml_of_decision response.fst,
     (match response.snd with
      | some {status, obligations, advice} =>
        String.join [
          (match status with
           | some status => xml_of_status status
-          | none => ""),
-         xml_of_obligations obligations,
-         xml_of_advices advice
+          | none => "<Status><StatusCode Value=\"urn:oasis:names:tc:xacml:1.0:status:ok\"/></Status>"),
+          (match obligations with
+          | [] => ""
+          | _ => xml_of_obligations obligations),
+          (match advice with
+          | [] => ""
+          | _ => xml_of_advices advice)
        ]
      | none => ""),
- "</Response>"]
-
-def request := ([(Attribute.mk "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject" "urn:oasis:names:tc:xacml:1.0:subject:subject-id" 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" 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" none (XmlType.string, "read"))])
-#eval xml_of_response (Decision'.not_applicable, none)
+    "</Result>",
+    "</Response>"
+  ]
diff --git a/xacml-proofs/lean/Xacml.lean.bak b/xacml-proofs/lean/Xacml.lean.bak
deleted file mode 100644
index bec63e6..0000000
--- a/xacml-proofs/lean/Xacml.lean.bak
+++ /dev/null
@@ -1,27 +0,0 @@
-inductive V₃ where
-  | true          : V₃
-  | false         : V₃
-  | indeterminate : V₃
-
-inductive V₆ where
-  | true_deny : V₆
-  | true_permit : V₆
-  | indeterminate_deny : V₆
-  | indeterminate_permit : V₆
-  | indeterminate : V₆
-  | false : V₆
-
-inductive Decision where
-  | permit : Decision
-  | deny   : Decision
-deriving Repr
-
--- structure Result where
---   decision    : Decision
---   obligations : Option (List String)
---   advice      : Option (List String)
--- deriving Repr
-
-def Result (α : Type) : Type := Decision × α
-
-#check ((Decision.permit, "Hi!") : Result String)