Entity Attribute Maps Lean Model

cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean

@@ -54,7 +54,8 @@ theorem type_of_eq_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Env
     rename_i h₄ <;> simp [h₄]
   case h_2 h₄ =>
     split at h₁
-    case h_1 h₅ =>
+    case h_1 => contradiction
+    case h_2 h₅ =>
       simp at h₁ ; simp [h₁]
       split
       case h_1 p₁ p₂ _ =>
@@ -67,7 +68,7 @@ theorem type_of_eq_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Env
           constructor
           · exists tc₂.snd
           · simp [h₅]
-    case h_2 h₅ =>
+    case h_3 h₅ =>
       split at h₁ <;> simp at h₁ ; simp [h₁]
       split
       case h_1 p₁ p₂ _ =>
@@ -288,7 +289,7 @@ theorem type_of_contains_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env
   simp [ifLubThenBool, err, ok] at h₁
   split at h₁ <;> simp only [Except.ok.injEq, Prod.mk.injEq] at h₁
   simp [h₁]
-  rename_i tc₁ tc₂ _ ty₁ ty₂ ty₃ _ h₄ _ _ h₅
+  rename_i tc₁ tc₂ _ ty₁ ty₂ ty₃ _ h₄ _ _ _ h₅
   exists ty₃, tc₂.fst
   rw [lub_comm] at h₅
   simp [h₅, ←h₄]
@@ -345,7 +346,7 @@ theorem type_of_containsA_inversion {op₂ : BinaryOp} {x₁ x₂ : Expr} {c c'
     simp [ifLubThenBool, err, ok] at h₂
     split at h₂ <;> simp only [Except.ok.injEq, Prod.mk.injEq] at h₂
     simp [h₂]
-    rename_i tc₁ tc₂ _ _ _ ty₁ ty₂ _ h₅ h₆ _ _ h₇
+    rename_i tc₁ tc₂ _ _ _ ty₁ ty₂ _ h₅ h₆ _ _ _ h₇
     exists ty₁, ty₂
     simp [h₇]
     constructor

cedar-lean/Cedar/Thm/Validation/Typechecker/GetAttr.lean

@@ -37,12 +37,22 @@ theorem getAttrInRecord_has_empty_capabilities {x₁ : Expr} {a : Attr} {c₁ c
   split at h₁ <;> simp at h₁
   simp [h₁]
 
+theorem getAttrInEAMap_has_empty_capabilities {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {aty ty ty₁ : CedarType} :
+  getAttrInEAMap ty aty x₁ a c₁ = Except.ok (ty₁, c₂) →
+  c₂ = ∅
+:= by
+  intro h₁
+  simp [getAttrInEAMap] at h₁
+  split at h₁ <;> simp [ok, err] at h₁
+  simp [h₁]
+
 theorem type_of_getAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType}
   (h₁ : typeOf (Expr.getAttr x₁ a) c₁ env = Except.ok (ty, c₂)) :
   c₂ = ∅ ∧
   ∃ c₁',
     (∃ ety, typeOf x₁ c₁ env = Except.ok (.entity ety, c₁')) ∨
-    (∃ rty, typeOf x₁ c₁ env = Except.ok (.record rty, c₁'))
+    (∃ rty, typeOf x₁ c₁ env = Except.ok (.record rty, c₁')) ∨
+    (∃ aty, typeOf x₁ c₁ env = Except.ok (.attribute_map aty, c₁'))
 := by
   simp [typeOf] at h₁
   cases h₂ : typeOf x₁ c₁ env <;> simp [h₂] at h₁
@@ -51,12 +61,15 @@ theorem type_of_getAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabili
     simp [typeOfGetAttr] at h₁
     split at h₁ <;> try contradiction
     · simp only [List.empty_eq, Except.ok.injEq, Prod.mk.injEq, false_and, exists_const,
-        CedarType.record.injEq, exists_and_right, exists_eq', true_and, false_or, and_true]
+        CedarType.record.injEq, exists_and_right, exists_eq', true_and, false_or, or_false, and_true]
       apply getAttrInRecord_has_empty_capabilities h₁
     · simp only [List.empty_eq, Except.ok.injEq, Prod.mk.injEq, CedarType.entity.injEq,
         exists_and_right, exists_eq', true_and, false_and, exists_const, or_false, and_true]
       split at h₁ <;> try simp [err] at h₁
       apply getAttrInRecord_has_empty_capabilities h₁
+    · simp only [List.empty_eq, Except.ok.injEq, Prod.mk.injEq, CedarType.attribute_map.injEq,
+        exists_and_right, exists_eq', true_and, false_and, exists_const, false_or, or_false, and_true]
+      apply getAttrInEAMap_has_empty_capabilities h₁
 
 theorem type_of_getAttr_is_sound_for_records {x₁ : Expr} {a : Attr} {c₁ c₁' : Capabilities} {env : Environment} {rty : RecordType} {request : Request} {entities : Entities} {v₁ : Value}
   (h₁ : CapabilitiesInvariant c₁ request entities)
@@ -155,6 +168,35 @@ theorem type_of_getAttr_is_sound_for_entities {x₁ : Expr} {a : Attr} {c₁ c
         apply instance_of_attribute_type _ h₁₁ (by simp [Qualified.getType]) h₉
         apply well_typed_entity_attributes h₂ h₈ h₁₀
 
+theorem type_of_getAttr_is_sound_for_ea_maps {x₁ : Expr} {a : Attr} {c₁ c₁' : Capabilities} {env : Environment} {aty : CedarType} {request : Request} {entities : Entities} {v₁ : Value}
+  (h₁ : CapabilitiesInvariant c₁ request entities)
+  (h₂ : typeOf (Expr.getAttr x₁ a) c₁ env = Except.ok (ty, ∅))
+  (h₃ : typeOf x₁ c₁ env = Except.ok (CedarType.attribute_map aty, c₁'))
+  (h₄ : evaluate x₁ request entities = Except.ok v₁)
+  (h₅ : InstanceOfType v₁ (CedarType.attribute_map aty)) :
+  ∃ v,
+  (getAttr v₁ a entities = Except.error Error.entityDoesNotExist ∨
+   getAttr v₁ a entities = Except.error Error.extensionError ∨
+   getAttr v₁ a entities = Except.error Error.arithBoundsError ∨
+   getAttr v₁ a entities = Except.ok v) ∧
+   InstanceOfType v ty
+:= by
+  have ⟨ r, h₆ ⟩ := instance_of_ea_map_type_is_record h₅
+  subst h₆
+  simp only [typeOf, h₃, typeOfGetAttr, getAttrInEAMap, List.empty_eq, Except.bind_ok] at h₂
+  split at h₂ <;> try contradiction
+  cases h₈ : r.find? a
+  case none =>
+    rename_i h₇
+    have ⟨_, h₁₁⟩ := capability_implies_record_attribute h₁ h₄ h₇
+    rw [h₁₁] at h₈
+    contradiction
+  case some =>
+    simp only [h₈, getAttr, attrsOf, Map.findOrErr, Except.bind_ok, Except.ok.injEq, false_or, exists_eq_left']
+    injections _ h₂
+    rw [←h₂]
+    exact instance_of_ea_map_attribute_type h₅ h₈
+
 theorem type_of_getAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} {request : Request} {entities : Entities}
   (h₁ : CapabilitiesInvariant c₁ request entities)
   (h₂ : RequestAndEntitiesMatchEnvironment env request entities)
@@ -166,14 +208,15 @@ theorem type_of_getAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilit
   have ⟨h₅, c₁', h₄⟩ := type_of_getAttr_inversion h₃
   subst h₅
   apply And.intro empty_guarded_capabilities_invariant
-  rcases h₄ with ⟨ety, h₄⟩ | ⟨rty, h₄⟩ <;>
+  rcases h₄ with ⟨ety, h₄⟩ | ⟨rty, h₄⟩ | ⟨ aty, h₄ ⟩ <;>
   have ⟨_, v₁, h₆, h₇⟩ := ih h₁ h₂ h₄ <;>
   simp [EvaluatesTo] at h₆ <;>
   simp [EvaluatesTo, evaluate] <;>
   rcases h₆ with h₆ | h₆ | h₆ | h₆ <;> simp [h₆]
   <;> try exact type_is_inhabited ty
   · exact type_of_getAttr_is_sound_for_entities h₁ h₂ h₃ h₄ h₆ h₇
   · exact type_of_getAttr_is_sound_for_records h₁ h₃ h₄ h₆ h₇
+  · exact type_of_getAttr_is_sound_for_ea_maps h₁ h₃ h₄ h₆ h₇
 
 
 end Cedar.Thm

cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean

@@ -31,7 +31,8 @@ theorem type_of_hasAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabili
   (c₂ = ∅ ∨ c₂ = Capabilities.singleton x₁ a) ∧
   ∃ c₁',
     (∃ ety, typeOf x₁ c₁ env = Except.ok (.entity ety, c₁')) ∨
-    (∃ rty, typeOf x₁ c₁ env = Except.ok (.record rty, c₁'))
+    (∃ rty, typeOf x₁ c₁ env = Except.ok (.record rty, c₁')) ∨
+    (∃ aty, typeOf x₁ c₁ env = Except.ok (.attribute_map aty, c₁'))
 := by
   simp [typeOf, typeOfHasAttr] at h₁
   cases h₂ : typeOf x₁ c₁ env <;> simp [h₂] at h₁
@@ -40,11 +41,11 @@ theorem type_of_hasAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabili
     simp at h₁
     split at h₁
     <;> simp [err, ok, hasAttrInRecord] at h₁
-    <;> split at h₁
+    <;> try split at h₁
     <;> try split at h₁
     <;> try split at h₁
     all_goals {
-      simp [ok] at h₁
+      try simp [ok] at h₁
       try simp [h₁]
     }
 
@@ -158,6 +159,22 @@ theorem type_of_hasAttr_is_sound_for_entities {x₁ : Expr} {a : Attr} {c₁ c
     rw [h₇] at h₈
     contradiction
 
+theorem type_of_hasAttr_is_sound_for_ea_maps {x₁ : Expr} {a : Attr} {c₁ c₁' : Capabilities} {env : Environment} {aty : CedarType} {entities : Entities} {v₁ : Value}
+  (h₁ : typeOf (Expr.hasAttr x₁ a) c₁ env = Except.ok (ty, c₂))
+  (h₂ : typeOf x₁ c₁ env = Except.ok (CedarType.attribute_map aty, c₁'))
+  (h₃ : InstanceOfType v₁ (CedarType.attribute_map aty)) :
+  ∃ v,
+  (hasAttr v₁ a entities = Except.error Error.entityDoesNotExist ∨
+   hasAttr v₁ a entities = Except.error Error.extensionError ∨
+   hasAttr v₁ a entities = Except.error Error.arithBoundsError ∨
+   hasAttr v₁ a entities = Except.ok v) ∧
+  InstanceOfType v ty
+:= by
+  simp only [typeOf, h₂, typeOfHasAttr, List.empty_eq, Except.bind_ok] at h₁
+  injections _ h₁ₗ
+  have ⟨ _, h₃ ⟩ := instance_of_ea_map_type_is_record h₃
+  rw [←h₁ₗ, h₃]
+  simp [hasAttr, attrsOf, InstanceOfType.instance_of_bool, InstanceOfBoolType]
 
 theorem type_of_hasAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} {request : Request} {entities : Entities}
   (h₁ : CapabilitiesInvariant c₁ request entities)
@@ -177,14 +194,14 @@ theorem type_of_hasAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilit
     subst h₇; subst h₈
     simp [EvaluatesTo, h₆]
   case right =>
-    rcases h₄ with ⟨ety, h₄⟩ | ⟨rty, h₄⟩ <;>
+    rcases h₄ with ⟨ety, h₄⟩ | ⟨rty, h₄⟩ | ⟨ aty, h₄ ⟩ <;>
     have ⟨_, v₁, h₆, h₇⟩ := ih h₁ h₂ h₄ <;>
     simp [EvaluatesTo] at h₆ <;>
     simp [EvaluatesTo, evaluate] <;>
     rcases h₆ with h₆ | h₆ | h₆ | h₆ <;> simp [h₆]
     <;> try exact type_is_inhabited ty
     · exact type_of_hasAttr_is_sound_for_entities h₁ h₂ h₃ h₄ h₆ h₇
     · exact type_of_hasAttr_is_sound_for_records h₁ h₃ h₄ h₆ h₇
-
+    · exact type_of_hasAttr_is_sound_for_ea_maps h₃ h₄ h₇
 
 end Cedar.Thm

cedar-lean/Cedar/Thm/Validation/Typechecker/IfThenElse.lean

@@ -61,7 +61,7 @@ theorem type_of_ite_inversion {x₁ x₂ x₃ : Expr} {c c' : Capabilities} {env
     cases h₃ : typeOf x₂ (c ∪ res₁.snd) env <;> simp [h₃] at h₁
     cases h₄ : typeOf x₃ c env <;> simp [h₄] at h₁
     split at h₁ <;> simp [ok, err] at h₁
-    rename_i ty' res₂ res₃ _ ty' hty
+    rename_i ty' res₂ res₃ _ ty' hty _
     have ⟨ht, hc⟩ := h₁
     subst ht hc hc₁
     exists res₂.fst, res₂.snd

cedar-lean/Cedar/Thm/Validation/Typechecker/LUB.lean

@@ -621,7 +621,7 @@ theorem lub_assoc_some_some {ty₁ ty₂ ty₃ ty₄ ty₅ : CedarType}
   case int | string =>
     subst h₁ h₂
     simp [lub?]
-  case entity | ext =>
+  case entity | ext | attribute_map =>
     have ⟨hl₁, hr₁⟩ := h₁
     have ⟨hl₂, hr₂⟩ := h₂
     subst hl₁ hr₁ hl₂ hr₂

cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean

@@ -58,10 +58,11 @@ theorem type_of_record_inversion_forall {axs : List (Attr × Expr)} {c : Capabil
         simp [pure, Except.pure] at h₁
         have ⟨hl₁, hr₁⟩ := h₁
         rw [eq_comm] at hl₁ hr₁ ; subst hl₁ hr₁
-        simp [requiredAttr, Except.map] at h₂
+        simp [requiredAttr, Except.bind] at h₂
+        split at h₂ <;> try contradiction
         split at h₂ <;> simp at h₂
         subst h₂
-        rename_i _ r _
+        rename_i _ r _ _ _
         simp [AttrExprHasAttrType]
         exists r.snd
       }

cedar-lean/Cedar/Thm/Validation/Typechecker/Set.lean

@@ -71,8 +71,10 @@ theorem type_of_set_tail
   (h₁ : (List.mapM₁ (xhd :: xtl) fun x => justType (typeOf x.val c env)) = Except.ok (hd :: tl))
   (h₂ : List.foldlM lub? hd tl = some ty)
   (h₃ : List.Mem x xtl) :
-  ∃ ty', typeOf (Expr.set xtl) c env = Except.ok (.set ty', []) ∧
-  (ty' ⊔ ty) = some ty
+  ∃ ty',
+    (typeOf (Expr.set xtl) c env = Except.ok (.set ty', []) ∨
+     typeOf (Expr.set xtl) c env = Except.error (.unexpectedType ty')) ∧
+    (ty' ⊔ ty) = some ty
 := by
   cases xtl
   case nil =>
@@ -110,7 +112,26 @@ theorem type_of_set_tail
         simp only [subty] at h₆
         split at h₆ <;> simp at h₆
         subst h₆
-        assumption
+        cases ty' <;> rename_i h₆ <;> simp [h₆]
+
+theorem type_of_set_unexpected_type_inversion {xs : List Expr} {c : Capabilities} {env: Environment} {ty : CedarType} {tys : List CedarType}
+  (h₁ : typeOf (Expr.set xs) c env = Except.error (.unexpectedType ty))
+  (h₂ : List.mapM (fun x => justType (typeOf x c env)) xs = Except.ok tys) :
+  ∃ aty, ty = (.attribute_map aty)
+:= by
+  have h₃ := List.mapM₁_eq_mapM (fun x : Expr => justType (typeOf x c env)) xs
+  simp only [h₂, h₃, typeOf, typeOfSet, List.empty_eq, Except.bind_ok] at h₁
+  cases tys <;> simp only at h₁
+  case nil => simp [err] at h₁
+  case cons tyₕ tysₜ =>
+    split at h₁ <;> try contradiction
+    case h_1 =>
+      rename_i aty _
+      exists aty
+      simp only [err, Except.error.injEq, TypeError.unexpectedType.injEq] at h₁
+      simp [h₁]
+    case h_3 =>
+      simp [err] at h₁
 
 theorem type_of_set_inversion {xs : List Expr} {c c' : Capabilities} {env : Environment} {sty : CedarType}
   (h₁ : typeOf (Expr.set xs) c env = Except.ok (sty, c')) :
@@ -155,15 +176,24 @@ theorem type_of_set_inversion {xs : List Expr} {c c' : Capabilities} {env : Envi
   case tail xhd xtl h₄ =>
     have ⟨ty', h₅, h₆⟩ := type_of_set_tail h₂ h₃ h₄
     have h₇ := @type_of_set_inversion xtl c ∅ env (.set ty')
-    simp only [h₅, List.empty_eq, CedarType.set.injEq, exists_and_right, exists_eq_left', true_and,
-      true_implies] at h₇
-    specialize h₇ x h₄
-    have ⟨tyᵢ, h₇, h₈⟩ := h₇
-    exists tyᵢ
-    have ⟨cᵢ, h₇⟩ := h₇
-    apply And.intro
-    · exists cᵢ
-    . exact lub_lub_fixed h₈ h₆
+    cases h₅
+    case inr h₅ =>
+      have h₈ := List.mapM_head_tail h₂
+      rw [List.mapM_pmap_subtype (fun x : Expr => justType (typeOf x c env))] at h₈
+      have ⟨ _, h₁₀ ⟩ := type_of_set_unexpected_type_inversion h₅ h₈
+      simp only [h₁₀, lub?, ite_some_none_eq_some, and_self] at h₆
+      simp [←h₆] at ty
+
+    case inl h₅ =>
+      simp only [h₅, List.empty_eq, CedarType.set.injEq, exists_and_right, exists_eq_left', true_and,
+        true_implies] at h₇
+      specialize h₇ x h₄
+      have ⟨tyᵢ, h₇, h₈⟩ := h₇
+      exists tyᵢ
+      have ⟨cᵢ, h₇⟩ := h₇
+      apply And.intro
+      · exists cᵢ
+      . exact lub_lub_fixed h₈ h₆
 
 theorem list_is_sound_implies_tail_is_sound {hd : Expr} {tl : List Expr}
   (h₁ : ∀ (xᵢ : Expr), xᵢ ∈ hd :: tl → TypeOfIsSound xᵢ) :

cedar-lean/Cedar/Thm/Validation/Typechecker/Types.lean

@@ -72,6 +72,9 @@ inductive InstanceOfType : Value → CedarType → Prop :=
   | instance_of_ext (x : Ext) (xty : ExtType)
       (h₁ : InstanceOfExtType x xty) :
       InstanceOfType (.ext x) (.ext xty)
+  | instance_of_ea_map (r : Map Attr Value) (aty : CedarType)
+      (h₂ : ∀ (k : Attr) (v : Value), r.find? k = some v → InstanceOfType v aty) :
+      InstanceOfType (.record r) (.attribute_map aty)
 
 def InstanceOfRequestType (request : Request) (reqty : RequestType) : Prop :=
   InstanceOfEntityType request.principal reqty.principal ∧
@@ -225,6 +228,24 @@ theorem instance_of_set_type_is_set {v : Value} {ty : CedarType} :
   rename_i s h₁
   exists s
 
+theorem instance_of_ea_map_type_is_record {v : Value} {aty : CedarType} :
+  InstanceOfType v (.attribute_map aty) →
+  ∃ r, v = .record r
+:= by
+  intro h₁
+  cases h₁
+  rename_i r _
+  exists r
+
+theorem instance_of_ea_map_attribute_type {r : Map Attr Value} {v : Value} {aty : CedarType} {a : Attr}
+  (h₁ : InstanceOfType (.record r) (.attribute_map aty))
+  (h₂ : r.find? a = .some v) :
+  InstanceOfType v aty
+:= by
+  cases h₁
+  rename_i h₃
+  exact h₃ a v h₂
+
 theorem instance_of_record_type_is_record {v : Value} {rty : RecordType} :
   InstanceOfType v (.record rty) →
   ∃ r, v = .record r
@@ -323,6 +344,12 @@ theorem instance_of_record_nil :
   apply InstanceOfType.instance_of_record <;>
   simp [Map.contains, Map.find?, Map.kvs, List.find?]
 
+theorem instance_of_attribute_map_nil (ty : CedarType) :
+  InstanceOfType (Value.record (Map.mk [])) (CedarType.attribute_map ty)
+:= by
+  apply InstanceOfType.instance_of_ea_map <;>
+  simp [Map.find?, List.find?]
+
 theorem instance_of_record_cons {hd : Attr × Qualified CedarType} {tl : List (Attr × Qualified CedarType)} {rhd : Value} {rtl : List (Attr × Value)}
   (h₁ : InstanceOfType rhd (Qualified.getType hd.snd))
   (h₂ : InstanceOfType (Value.record (Map.mk rtl)) (CedarType.record (Map.mk tl))) :
@@ -423,6 +450,9 @@ theorem type_is_inhabited (ty : CedarType) :
       subst h₄ ; cases mtl ; rename_i rtl
       exists (.record (Map.mk ((hd.fst, rhd) :: rtl)))
       exact instance_of_record_cons h₂ h₃
+  | .attribute_map aty =>
+      exists (.record (Map.mk []))
+      exact (instance_of_attribute_map_nil aty)
 
 theorem instance_of_lubBool_left {v : Value} {bty₁ bty₂ : BoolType} :
   InstanceOfType v (CedarType.bool bty₁) →

cedar-lean/Cedar/Validation/RequestEntityValidator.lean

@@ -65,6 +65,8 @@ def instanceOfType (v : Value) (ty : CedarType) : Bool :=
         | .some qty => instanceOfType v qty.getType
         | _ => true))) &&
     rty.keys.all (requiredAttributePresent r rty)
+  | .record r, .attribute_map aty =>
+    (r.kvs.attach₂.all (λ ⟨(_, v), _⟩ => instanceOfType v aty))
   | .ext x, .ext xty => instanceOfExtType x xty
   | _, _ => false
     termination_by v
@@ -73,7 +75,7 @@ def instanceOfType (v : Value) (ty : CedarType) : Bool :=
       case _ h₁ =>
         have := Set.sizeOf_lt_of_mem h₁
         omega
-      case _ h₁ =>
+      case _ h₁ | _ h₁ =>
         cases r
         simp only [Map.kvs] at h₁
         simp only [Map.mk.sizeOf_spec]