Prove that well-formed Environment compiles to well-formed SymEnv (cedar-policy#661)

Signed-off-by: Zhengyao Lin <zyal@amazon.com>

Author: zhengyao-lin

cedar-lean/Cedar/Thm/Data/List/Lemmas.lean

@@ -383,6 +383,14 @@ theorem mapM₂_eq_mapM [Monad m] [LawfulMonad m] [SizeOf α] [SizeOf β]
 := by
   simp only [mapM₂, attach₂, mapM_pmap_subtype]
 
+theorem mapM₃_eq_mapM [Monad m] [LawfulMonad m] [SizeOf α] [SizeOf β]
+  (f : (α × β) → m γ)
+  (as : List (α × β)) :
+  List.mapM₃ as (λ x : { x // sizeOf x.snd < 1 + (1 + sizeOf as) } => f x.val) =
+  List.mapM f as
+:= by
+  simp only [mapM₃, attach₃, mapM_pmap_subtype]
+
 theorem mapM_implies_nil {f : α → Except β γ} {as : List α}
   (h₁ : List.mapM f as = Except.ok []) :
   as = []
@@ -1430,4 +1438,62 @@ theorem find?_compose {α β} (f : α → β) (p₁ : β → Bool) (p₂ : α 
       specialize hₐ head
       simp only [Function.comp_apply, heq₁, heq₂, Bool.false_eq_true] at hₐ
     case _ => exact h hₐ
+
+theorem mem_implies_mem_eraseDups
+  [BEq α] [LawfulBEq α]
+  {xs : List α} {x : α}
+  (hmem : x ∈ xs) :
+  x ∈ xs.eraseDups
+:= by
+  cases xs with
+  | nil => contradiction
+  | cons hd tl =>
+    simp only [List.eraseDups_cons, List.mem_cons]
+    simp only [List.mem_cons] at hmem
+    cases hx : x == hd
+    · simp only [beq_eq_false_iff_ne, ne_eq] at hx
+      apply Or.inr
+      simp only [hx, false_or] at hmem
+      apply mem_implies_mem_eraseDups
+      apply List.mem_filter.mpr
+      simp only [hmem, true_and]
+      simp only [Bool.not_eq_eq_eq_not, Bool.not_true, beq_eq_false_iff_ne, ne_eq]
+      exact hx
+    · apply Or.inl
+      simp only [beq_iff_eq] at hx
+      exact hx
+termination_by xs.length
+decreasing_by
+  calc
+    (List.filter (fun b => !b == hd) tl).length <= tl.length := by
+      apply List.length_filter_le
+    _ < xs.length := by
+      simp [*]
+
+theorem mem_eraseDups_implies_mem
+  [BEq α] [LawfulBEq α]
+  {xs : List α} {x : α}
+  (hmem : x ∈ xs.eraseDups) :
+  x ∈ xs
+:= by
+  cases xs with
+  | nil => contradiction
+  | cons hd tl =>
+    simp only [eraseDups_cons, mem_cons] at hmem
+    simp only [mem_cons]
+    cases hmem with
+    | inl h => exact Or.inl h
+    | inr h =>
+      apply Or.inr
+      have := mem_eraseDups_implies_mem h
+      have := List.mem_filter.mp this
+      exact this.1
+termination_by xs.length
+decreasing_by
+  calc
+    (List.filter (fun b => !b == hd) tl).length <= tl.length := by
+      apply List.length_filter_le
+    _ < xs.length := by
+      simp [*]
+
 end List

cedar-lean/Cedar/Thm/Data/Map.lean

@@ -201,6 +201,13 @@ theorem contains_iff_some_find? {α β} [BEq α] {m : Map α β} {k : α} :
   m.contains k ↔ ∃ v, m.find? k = .some v
 := by simp [contains, Option.isSome_iff_exists]
 
+theorem find?_some_implies_contains {α β} [BEq α] {m : Map α β} {k : α} {v : β} :
+  m.find? k = .some v → m.contains k
+:= by
+  intros h
+  apply contains_iff_some_find?.mpr
+  simp [h]
+
 theorem not_contains_of_empty {α β} [BEq α] (k : α) :
   ¬ (Map.empty : Map α β).contains k
 := by simp [contains, empty, find?, List.find?]
@@ -427,7 +434,7 @@ theorem find?_implies_make_find?
   {l : List (α × β)}
   {k : α} {v : β}
   (h : List.find? (λ x => x.fst == k) l = some (k, v)) :
-  (Data.Map.make l).find? k = some v
+  (make l).find? k = some v
 := by
   apply (in_list_iff_find?_some (Data.Map.make_wf l)).mp
   simp only [make, Data.Map.kvs]
@@ -1116,4 +1123,54 @@ theorem wellFormed_correct {α β} [LT α] [StrictLT α] [DecidableLT α] {m : M
     apply wf_iff_sorted.mp
     exact h
 
+/--
+If a key exists in `l₂` but not in `l₁`,
+then `Map.make (l₁ ++ l₂)` contains that key.
+-/
+theorem map_make_append_find_disjoint
+  [LT α] [StrictLT α] [DecidableEq α] [DecidableLT α]
+  [SizeOf α] [SizeOf β]
+  {l₁ : List (α × β)} {l₂ : List (α × β)} {k : α}
+  (hfind₁ : l₁.find? (λ ⟨k', _⟩ => k' == k) = none)
+  (hfind₂ : (l₂.find? (λ ⟨k', _⟩ => k' == k)).isSome) :
+  ∃ v,
+    (Map.make (l₁ ++ l₂)).find? k = some v ∧
+    (k, v) ∈ l₂
+:= by
+  have hwf : (Map.make (l₁ ++ l₂)).WellFormed := by
+    exact Map.make_wf _
+  have hsub :
+    (Map.make (l₁ ++ l₂)).kvs ⊆ l₁ ++ l₂
+  := by
+    apply List.canonicalize_subseteq
+  simp [Subset, List.Subset] at hsub
+  have ⟨v, hv⟩ :
+    ∃ v, (Map.make (l₁ ++ l₂)).find? k = some v
+  := by
+    simp only [Option.isSome] at hfind₂
+    split at hfind₂
+    rotate_left
+    contradiction
+    rename_i kv hkv
+    exists kv.snd
+    apply Map.find?_implies_make_find?
+    simp [List.find?_append]
+    apply Or.inr
+    constructor
+    · simp only [List.find?_eq_none, beq_iff_eq, Prod.forall] at hfind₁
+      exact hfind₁
+    have := List.find?_some hkv
+    simp only [beq_iff_eq] at this
+    simp only [hkv]
+    simp [←this]
+  simp only [hv, Option.some.injEq, exists_eq_left']
+  have := Map.find?_mem_toList hv
+  have := hsub k v this
+  cases this with
+  | inl hmem₁ =>
+    have := List.find?_eq_none.mp hfind₁
+    specialize this (k, v) hmem₁
+    simp at this
+  | inr h => exact h
+
 end Cedar.Data.Map

cedar-lean/Cedar/Thm/SymCC/Compiler/WellTyped.lean

@@ -1527,9 +1527,10 @@ theorem compile_well_typed_call
       simp [hty_comp_x1, hty_comp_x2, hty_x1, hty_x2, TermType.ofType]
 
 /--
-Compiling a well-typed expression should produce a term of the corresponding `TermType`.
+Compiling a well-typed expression should produce a term of the corresponding `TermType`,
+assuming that the expression is well-formed in the symbolic environment.
 -/
-theorem compile_well_typed {Γ : Environment} {εnv : SymEnv} {tx : TypedExpr} :
+theorem compile_well_typed_on_wf_expr {Γ : Environment} {εnv : SymEnv} {tx : TypedExpr} :
   CompileWellTypedCondition tx Γ εnv →
   CompileWellTyped tx εnv
 := by
@@ -1541,52 +1542,52 @@ theorem compile_well_typed {Γ : Environment} {εnv : SymEnv} {tx : TypedExpr} :
     have ⟨h1, h2, h3⟩ := h.eliminate_ite
     apply compile_well_typed_ite
     any_goals apply CompileWellTyped.add_wf
-    any_goals apply compile_well_typed
+    any_goals apply compile_well_typed_on_wf_expr
     any_goals assumption
   case and =>
     have ⟨ha, hb⟩ := h.eliminate_or_and ?_
     apply (compile_well_typed_or_and ?_ ?_).right
     any_goals apply CompileWellTyped.add_wf
-    any_goals apply compile_well_typed
+    any_goals apply compile_well_typed_on_wf_expr
     any_goals assumption
     any_goals simp
   case or =>
     have ⟨ha, hb⟩ := h.eliminate_or_and ?_
     apply (compile_well_typed_or_and ?_ ?_).left
     any_goals apply CompileWellTyped.add_wf
-    any_goals apply compile_well_typed
+    any_goals apply compile_well_typed_on_wf_expr
     any_goals assumption
     any_goals simp
   case unaryApp =>
     have hcond := h.eliminate_unaryApp
     apply compile_well_typed_unaryApp
     any_goals apply CompileWellTyped.add_wf
-    any_goals apply compile_well_typed
+    any_goals apply compile_well_typed_on_wf_expr
     all_goals assumption
   case binaryApp =>
     have ⟨ha, hb⟩ := h.eliminate_binaryApp
     apply compile_well_typed_binaryApp
     any_goals apply CompileWellTyped.add_wf
-    any_goals apply compile_well_typed
+    any_goals apply compile_well_typed_on_wf_expr
     any_goals assumption
   case getAttr =>
     have hcond := h.eliminate_getAttr
     apply compile_well_typed_getAttr
     any_goals apply CompileWellTyped.add_wf
-    any_goals apply compile_well_typed
+    any_goals apply compile_well_typed_on_wf_expr
     all_goals assumption
   case hasAttr =>
     have hcond := h.eliminate_hasAttr
     apply compile_well_typed_hasAttr
     any_goals apply CompileWellTyped.add_wf
-    any_goals apply compile_well_typed
+    any_goals apply compile_well_typed_on_wf_expr
     all_goals assumption
   case set =>
     have hcond := h.eliminate_set
     apply compile_well_typed_set
     · intros x hx
       apply CompileWellTyped.add_wf
-      apply compile_well_typed (hcond x hx)
+      apply compile_well_typed_on_wf_expr (hcond x hx)
       apply hcond
       assumption
     assumption
@@ -1595,7 +1596,7 @@ theorem compile_well_typed {Γ : Environment} {εnv : SymEnv} {tx : TypedExpr} :
     apply compile_well_typed_record
     · intros a x hx
       apply CompileWellTyped.add_wf
-      apply compile_well_typed (hcond a x hx)
+      apply compile_well_typed_on_wf_expr (hcond a x hx)
       apply hcond
       assumption
     assumption
@@ -1604,7 +1605,7 @@ theorem compile_well_typed {Γ : Environment} {εnv : SymEnv} {tx : TypedExpr} :
     apply compile_well_typed_call
     · intros x hx
       apply CompileWellTyped.add_wf
-      apply compile_well_typed (hcond x hx)
+      apply compile_well_typed_on_wf_expr (hcond x hx)
       apply hcond
       assumption
     assumption