soundness for sets

Signed-off-by: John Kastner <jkastner@amazon.com>

cedar-lean/Cedar/Thm/Validation/Levels.lean

@@ -30,6 +30,7 @@ import Cedar.Thm.Validation.Levels.BinaryApp
 import Cedar.Thm.Validation.Levels.And
 import Cedar.Thm.Validation.Levels.Or
 import Cedar.Thm.Validation.Levels.Record
+import Cedar.Thm.Validation.Levels.Set
 
 namespace Cedar.Thm
 
@@ -76,13 +77,14 @@ theorem level_based_slicing_is_sound_expr {e : Expr} {n nmax : Nat} {tx : TypedE
     have ihe := @level_based_slicing_is_sound_expr e
     exact level_based_slicing_is_sound_has_attr hn hs hc hr ht hl ihe
   case set xs =>
-    replace ⟨ hc, txs, ty,  htx, ht ⟩  := type_of_set_inversion ht
-    subst tx
-    cases hl ; rename_i hl
-    -- TODO: I need a slightly stronger inversion lemma that gives me something like
-    --       ∀ x ∈ xs, ∃ tx c', typeOf x c env = .ok (tx, c') ∧ (tx.typeOf ⊔ ty) = some ty ∧ tx ∈ txs
-    --       Notably, `tx ∈ txs` is required to concluded `TypedAtLevel tx n` by `hl`
-    sorry
+    have ih : ∀ x ∈ xs, TypedAtLevelIsSound x := by
+      intro x hx
+      have _ : sizeOf x < sizeOf (Expr.set xs) := by
+        have h₁ := List.sizeOf_lt_of_mem hx
+        simp only [Expr.set.sizeOf_spec]
+        omega
+      exact @level_based_slicing_is_sound_expr x
+    exact level_based_slicing_is_sound_set hn hs hc hr ht hl ih
   case call => sorry -- should be the same as set
   case record rxs =>
     have ih : ∀ x ∈ rxs, TypedAtLevelIsSound x.snd := by

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

@@ -0,0 +1,70 @@
+/-
+ Copyright Cedar Contributors
+
+ Licensed under the Apache License, Version 2.0 (the "License");
+ you may not use this file except in compliance with the License.
+ You may obtain a copy of the License at
+
+      https://www.apache.org/licenses/LICENSE-2.0
+
+ Unless required by applicable law or agreed to in writing, software
+ distributed under the License is distributed on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ See the License for the specific language governing permissions and
+ limitations under the License.
+-/
+
+import Cedar.Spec
+import Cedar.Data
+import Cedar.Validation
+import Cedar.Thm.Validation.Typechecker
+import Cedar.Thm.Validation.Typechecker.Types
+import Cedar.Thm.Validation.Levels.Basic
+
+namespace Cedar.Thm
+
+open Cedar.Data
+open Cedar.Spec
+open Cedar.Validation
+
+theorem mapm_eval_congr_entities {xs : List Expr} {request : Request} {entities slice : Entities}
+  (he : ∀ (x : Expr), x ∈ xs → evaluate x request entities = evaluate x request slice) :
+  List.mapM (fun x => evaluate x request entities) xs = List.mapM (fun x => evaluate x request slice) xs
+:= by
+  cases xs
+  case nil => simp
+  case cons x xs =>
+    simp only [List.mapM_cons, bind_pure_comp]
+    rw [he x (by simp)]
+    have he' : ∀ (x : Expr), x ∈ xs → evaluate x request entities = evaluate x request slice := by
+      intros x' hx'
+      replace hx' : x' ∈ x :: xs := by simp [hx']
+      exact he x' hx'
+    cases evaluate x request slice <;> simp only [Except.bind_err, Except.bind_ok]
+    have ih := mapm_eval_congr_entities he'
+    rw [ih]
+
+theorem level_based_slicing_is_sound_set {xs : List Expr} {n : Nat} {c₀ c₁: Capabilities} {env : Environment} {request : Request} {entities slice : Entities}
+  (hn : nmax ≥ n)
+  (hs : slice = entities.sliceAtLevel request nmax)
+  (hc : CapabilitiesInvariant c₀ request entities)
+  (hr : RequestAndEntitiesMatchEnvironment env request entities)
+  (ht : typeOf (.set xs) c₀ env = Except.ok (tx, c₁))
+  (hl : TypedExpr.AtLevel tx n nmax)
+  (ih : ∀ x ∈ xs, TypedAtLevelIsSound x) :
+  evaluate (.set xs) request entities = evaluate (.set xs) request slice
+:= by
+  replace ⟨ _, txs, ty,  htx, ht ⟩ := type_of_set_inversion ht
+  subst tx
+  cases hl ; rename_i hl
+
+  have he : ∀ x ∈ xs, evaluate x request entities = evaluate x request slice := by
+    intros x hx
+    replace ⟨ tx, c', htxs, htx, _ ⟩ := ht x hx
+    specialize hl tx htxs
+    exact ih x hx hn hs hc hr htx hl
+
+  simp only [evaluate, List.mapM₁, List.attach, List.attachWith]
+  simp only [List.mapM_pmap_subtype (λ x : Expr => evaluate x request entities) xs]
+  simp only [List.mapM_pmap_subtype (λ x : Expr => evaluate x request slice) xs]
+  rw [mapm_eval_congr_entities he]

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

@@ -119,9 +119,10 @@ theorem type_of_set_inversion {xs : List Expr} {c c' : Capabilities} {env : Envi
   ∃ txs ty,
     tx = (.set txs (.set ty)) ∧
     ∀ xᵢ ∈ xs,
-      ∃ tyᵢ cᵢ,
-        (typeOf xᵢ c env).typeOf = Except.ok (tyᵢ, cᵢ) ∧
-        (tyᵢ ⊔ ty) = .some ty
+      ∃ txᵢ cᵢ,
+        txᵢ ∈ txs ∧
+        typeOf xᵢ c env = Except.ok (txᵢ, cᵢ) ∧
+        (txᵢ.typeOf ⊔ ty) = .some ty
 := by
   simp [typeOf] at h₁
   cases h₂ : List.mapM₁ xs fun x => justType (typeOf x.val c env) <;>
@@ -150,8 +151,9 @@ theorem type_of_set_inversion {xs : List Expr} {c c' : Capabilities} {env : Envi
     simp only [justType, Except.map] at h₅
     split at h₅ <;> simp at h₅
     rename_i res h₇
-    exists hdty.typeOf, res.snd
-    apply And.intro
+    exists hdty, res.snd
+    and_intros
+    · simp
     · simp [←h₅, h₇, ResultType.typeOf, Except.map]
     · exact foldlM_of_lub_is_LUB h₃
   case tail xhd xtl h₄ =>
@@ -163,10 +165,12 @@ theorem type_of_set_inversion {xs : List Expr} {c c' : Capabilities} {env : Envi
     replace ⟨ h₇, h₉ ⟩ := h₇
     subst h₇ h₉
     specialize h₈ x h₄
-    replace ⟨tyᵢ, ⟨c₁, h₈⟩, h₉⟩ := h₈
-    exists tyᵢ, c₁
-    simp only [h₈, true_and]
-    exact lub_trans h₉ h₆
+    replace ⟨txᵢ, c₁, htl, htxᵢ, hlub ⟩ := h₈
+    exists txᵢ, c₁
+    and_intros
+    · exact List.Mem.tail _ htl
+    · exact htxᵢ
+    · exact lub_trans hlub h₆
 
 theorem list_is_sound_implies_tail_is_sound {hd : Expr} {tl : List Expr}
   (h₁ : ∀ (xᵢ : Expr), xᵢ ∈ hd :: tl → TypeOfIsSound xᵢ) :
@@ -177,8 +181,8 @@ theorem list_is_sound_implies_tail_is_sound {hd : Expr} {tl : List Expr}
   simp [h₂]
 
 theorem list_is_typed_implies_tail_is_typed {hd : Expr} {tl : List Expr} {c₁ : Capabilities} {env : Environment} {ty : CedarType}
-  (h₁ : ∀ (xᵢ : Expr), xᵢ ∈ hd :: tl → ∃ tyᵢ cᵢ, (typeOf xᵢ c₁ env).typeOf = Except.ok (tyᵢ, cᵢ) ∧ (tyᵢ ⊔ ty) = some ty) :
-  ∀ (xᵢ : Expr), xᵢ ∈ tl → ∃ tyᵢ cᵢ, (typeOf xᵢ c₁ env).typeOf = Except.ok (tyᵢ, cᵢ) ∧ (tyᵢ ⊔ ty) = some ty
+  (h₁ : ∀ (xᵢ : Expr), xᵢ ∈ hd :: tl → ∃ txᵢ cᵢ, (typeOf xᵢ c₁ env) = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty) :
+  ∀ (xᵢ : Expr), xᵢ ∈ tl → ∃ txᵢ cᵢ, typeOf xᵢ c₁ env = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty
 := by
   intro xᵢ h₂
   apply h₁
@@ -188,7 +192,7 @@ theorem type_of_set_is_sound_err {xs : List Expr} {c₁ : Capabilities} {env : E
   (ih : ∀ (xᵢ : Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
   (h₁ : CapabilitiesInvariant c₁ request entities)
   (h₂ : RequestAndEntitiesMatchEnvironment env request entities)
-  (h₄ : ∀ (xᵢ : Expr), xᵢ ∈ xs → ∃ tyᵢ cᵢ, (typeOf xᵢ c₁ env).typeOf = Except.ok (tyᵢ, cᵢ) ∧ (tyᵢ ⊔ ty) = some ty)
+  (h₄ : ∀ (xᵢ : Expr), xᵢ ∈ xs → ∃ txᵢ cᵢ, (typeOf xᵢ c₁ env) = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty)
   (h₅ : (xs.mapM fun x => evaluate x request entities) = Except.error err) :
   err = Error.entityDoesNotExist ∨
   err = Error.extensionError ∨
@@ -203,7 +207,6 @@ theorem type_of_set_is_sound_err {xs : List Expr} {c₁ : Capabilities} {env : E
     have h₄ := h₄ hd
     simp only [h₆, List.mem_cons, true_or, forall_const] at h₄
     have ⟨tyᵢ, cᵢ, h₇, _⟩ := h₄
-    split_type_of h₇ ; rename_i h₇ hl₇ _
     have h₉ := ih hd ; simp [h₆, TypeOfIsSound] at h₉
     specialize (h₉ h₁ h₂ h₇) ; have ⟨_, v, h₉⟩ := h₉
     simp [EvaluatesTo] at h₉
@@ -226,7 +229,7 @@ theorem type_of_set_is_sound_ok { xs : List Expr } { c₁ : Capabilities } { env
   (ih : ∀ (xᵢ : Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
   (h₁ : CapabilitiesInvariant c₁ request entities)
   (h₂ : RequestAndEntitiesMatchEnvironment env request entities)
-  (h₃ : ∀ (xᵢ : Expr), xᵢ ∈ xs → ∃ tyᵢ cᵢ, (typeOf xᵢ c₁ env).typeOf = Except.ok (tyᵢ, cᵢ) ∧ (tyᵢ ⊔ ty) = some ty)
+  (h₃ : ∀ (xᵢ : Expr), xᵢ ∈ xs → ∃ txᵢ cᵢ, (typeOf xᵢ c₁ env) = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty)
   (h₄ : (xs.mapM fun x => evaluate x request entities) = Except.ok vs)
   (h₅ : v ∈ vs):
   InstanceOfType v ty
@@ -252,14 +255,12 @@ theorem type_of_set_is_sound_ok { xs : List Expr } { c₁ : Capabilities } { env
       have ⟨tyᵢ, cᵢ, h₃, h₆⟩ := h₃
       specialize ih hd
       simp [TypeOfIsSound] at ih
-      split_type_of h₃ ; rename_i h₃ hl₃ _
       specialize ih h₁ h₂ h₃
       have ⟨_, v', ihl, ihr⟩ := ih
       simp [EvaluatesTo] at ihl
       rcases ihl with ihl | ihl | ihl | ihl <;>
       simp [ihl] at h₇
       subst h₇
-      rw [hl₃] at ihr
       exact instance_of_lub_left h₆ ihr
     case tail h₉ =>
       apply @type_of_set_is_sound_ok
@@ -283,6 +284,10 @@ theorem type_of_set_is_sound {xs : List Expr} {c₁ c₂ : Capabilities} {env :
   apply And.intro empty_guarded_capabilities_invariant
   simp only [EvaluatesTo, evaluate, List.mapM₁, List.attach_def,
     List.mapM_pmap_subtype (evaluate · request entities)]
+  replace h₅ : ∀ xᵢ ∈ xs, ∃ tx c', typeOf xᵢ c₁ env = .ok (tx, c') ∧ (tx.typeOf ⊔ ty) = some ty := by
+    intros x h₁
+    replace ⟨txᵢ, cᵢ, h₅⟩ := h₅ x h₁
+    simp [h₅]
   cases h₆ : xs.mapM fun x => evaluate x request entities <;>
   simp [h₆]
   case error err =>