From 8dd155cd4a87b9831e967444634723fdb633aefa Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Tue, 7 Oct 2025 10:15:21 -0700
Subject: [PATCH 1/3] complete CallElimCorrect proof

---
 Strata/DL/Util/ListUtils.lean                 |  31 +-
 Strata/DL/Util/Map.lean                       |   6 +
 Strata/Languages/Boogie/OldExpressions.lean   |  12 +
 .../Boogie/StatementSemanticsProps.lean       |   2 +-
 Strata/Transform/CallElimCorrect.lean         | 265 ++++++++++++------
 5 files changed, 233 insertions(+), 83 deletions(-)

diff --git a/Strata/DL/Util/ListUtils.lean b/Strata/DL/Util/ListUtils.lean
index 59047888..8b055336 100644
--- a/Strata/DL/Util/ListUtils.lean
+++ b/Strata/DL/Util/ListUtils.lean
@@ -191,13 +191,22 @@ theorem List.Disjoint.symm_app (d : Disjoint l (l₁ ++ l₂))
   : Disjoint l (l₂ ++ l₁) := fun _ Hin1 Hin2 => d Hin1
         (mem_append.mpr $ Or.symm (mem_append.mp Hin2))
 
-theorem List.Disjoint_Subset : Disjoint vs ks → ks'.Subset ks → vs.Disjoint ks' := by
+theorem List.Disjoint_Subset_right : Disjoint vs ks → ks'.Subset ks → vs.Disjoint ks' := by
   intros Hdis Hsub
   simp [Disjoint, List.Subset] at *
   intros a Hin1 Hin2
   specialize Hdis Hin1
   simp_all
 
+theorem List.Disjoint_Subset_left : Disjoint vs ks → List.Subset vs' vs → vs'.Disjoint ks := by
+  intros Hdis Hsub
+  apply List.Disjoint.symm
+  apply Disjoint_Subset_right (Disjoint.symm Hdis) Hsub
+
+theorem List.Disjoint_Subsets : Disjoint vs ks → List.Subset vs' vs → List.Subset ks' ks → vs'.Disjoint ks' := by
+  intros Hdis Hsub1 Hsub2
+  exact List.Disjoint_Subset_left (Disjoint_Subset_right Hdis Hsub2) Hsub1
+
 theorem List.DisjointAppLeft' :
   Disjoint vs (ks ++ ks') → Disjoint vs ks' := by
   intros Hdist h
@@ -212,6 +221,26 @@ theorem List.DisjointAppRight' :
   have Hdist' := List.Disjoint.symm_app Hdist
   exact List.DisjointAppLeft' Hdist'
 
+theorem List.Subset.subset_app_of_or_2 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 → l ⊆ l1 ++ l2  := by
+  simp [Subset, List.Subset]
+  intro H a Ha
+  cases H <;> simp_all
+
+theorem List.Subset.subset_app_of_or_3 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 ∨ l ⊆ l3 → l ⊆ l1 ++ l2 ++ l3  := by
+  simp [Subset, List.Subset]
+  intro H a Ha
+  cases H <;> try (rename_i H; cases H)
+  any_goals simp_all
+
+theorem List.Subset.subset_app_of_or_4 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 ∨ l ⊆ l3 ∨ l ⊆ l4 → l ⊆ l1 ++ l2 ++ l3 ++ l4 := by
+  simp [Subset, List.Subset]
+  intro H a Ha
+  cases H <;> try (rename_i H; cases H <;> try (rename_i H; cases H))
+  any_goals simp_all
+
+theorem List.Subset.assoc {l: List α}: l ⊆ l1 ++ l2 ++ l3 ↔ l ⊆ l1 ++ (l2 ++ l3) := by
+  simp [Subset, List.Subset]
+
 theorem List.replaceAll_app {α : Type} [DecidableEq α] {h h' : α} {as bs : List α}:
   List.replaceAll as h h' ++ List.replaceAll bs h h' = List.replaceAll (as ++ bs) h h' := by
   induction as generalizing bs
diff --git a/Strata/DL/Util/Map.lean b/Strata/DL/Util/Map.lean
index fc090955..2e4f6512 100644
--- a/Strata/DL/Util/Map.lean
+++ b/Strata/DL/Util/Map.lean
@@ -202,4 +202,10 @@ theorem Map.insert_values [DecidableEq α] (m : Map α β) :
       grind
   done
 
+theorem Map.findNone_eq_notmem_mapfst {m: Map α β} [DecidableEq α]: ¬ a ∈ List.map Prod.fst m ↔ Map.find? m a = none := by
+  induction m <;> simp [Map.find?]
+  constructor <;> intro H
+  split <;> simp_all
+  split at H <;> simp_all
+  rw [Eq.comm]; assumption
 -------------------------------------------------------------------------------
diff --git a/Strata/Languages/Boogie/OldExpressions.lean b/Strata/Languages/Boogie/OldExpressions.lean
index e195e5c8..9c56833e 100644
--- a/Strata/Languages/Boogie/OldExpressions.lean
+++ b/Strata/Languages/Boogie/OldExpressions.lean
@@ -255,6 +255,18 @@ with `val`.
 def substsOldExprs (sm : Map Expression.Ident Expression.Expr) (es : List Expression.Expr) :=
   es.map $ substsOldExpr sm
 
+theorem substsOldExpr_singleton: substsOldExpr [(var,s)] e = substOld var s e := by
+  induction e <;> simp [substsOldExpr, substOld, Map.isEmpty, *]
+  split <;> simp_all;
+  simp [Map.find?]
+  split <;> simp_all
+  intro h; rw [Eq.comm] at h
+  contradiction
+
+theorem substOldExpr_nil: OldExpressions.substsOldExpr [] e = e := by
+  unfold OldExpressions.substsOldExpr
+  simp [Map.isEmpty]
+  
 /--
 For each `(var, expr)` pair in `sm`, substitute `old(var)` with `expr` in
 `conds`.
diff --git a/Strata/Languages/Boogie/StatementSemanticsProps.lean b/Strata/Languages/Boogie/StatementSemanticsProps.lean
index df786e60..3dec9f56 100644
--- a/Strata/Languages/Boogie/StatementSemanticsProps.lean
+++ b/Strata/Languages/Boogie/StatementSemanticsProps.lean
@@ -1954,7 +1954,7 @@ theorem InvStoresExceptUpdatedMem :
   simp [invStoresExcept] at *
   intros Hsub vs Hdisj
   refine InvStoresUpdatedStatesDisjLeftMono ?_ ?_ Hlen
-  exact List.Disjoint_Subset Hdisj Hsub
+  exact List.Disjoint_Subset_right Hdisj Hsub
   exact Hinv _ Hdisj
 
 theorem InvStoresExceptUpdateStates :
diff --git a/Strata/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean
index 2938e456..daff39d6 100644
--- a/Strata/Transform/CallElimCorrect.lean
+++ b/Strata/Transform/CallElimCorrect.lean
@@ -1483,6 +1483,13 @@ intros Hsubst k1 k2 Hin
 apply Hsubst
 exact List.mem_cons_of_mem h Hin
 
+theorem substNodup_tail :
+Imperative.substNodup (h :: t) →
+Imperative.substNodup t := by
+intros Hsubst
+simp [Imperative.substNodup] at *
+exact (List.nodup_cons.mp (nodup_middle Hsubst.right)).right
+
 theorem substDefined_updatedState :
 Imperative.substDefined σ σ' ls →
 Imperative.substDefined (updatedState σ k v) σ' ls := by
@@ -1750,6 +1757,7 @@ theorem SubstPostsMem :
     substPost = OldExpressions.substsOldExpr (createOldVarsSubst oldTrips) (OldExpressions.normalizeOldExpr post)
   := by
   intros Hin
+
   generalize Heq : OldExpressions.substsOldExprs
                     (createOldVarsSubst oldTrips)
                     (OldExpressions.normalizeOldExprs vs) = l at *
@@ -1760,13 +1768,11 @@ theorem SubstPostsMem :
     simp [← Heq] at *
     cases Hin with
     | inl Hin =>
-      left; sorry -- assumption
+      left; assumption
     | inr Hin =>
       right
       cases Hin with
-      | intro id HH =>
-        sorry
-        -- exact ⟨id, HH.1, Eq.symm HH.2⟩
+      | intro id HH => exact ⟨id, HH.1, Eq.symm HH.2⟩
 
 /--
 Generate the substitution pairs needed for the body of the procedure
@@ -2232,6 +2238,67 @@ NormalizedOldExpr e →
     rw [trih, eih]
     simp [List.app_removeAll]
 
+theorem substOldExpr_cons:
+  Imperative.substNodup (createOldStoreSubst (h::t)) →
+  OldExpressions.substsOldExpr (createOldVarsSubst (h :: t)) e
+          = OldExpressions.substsOldExpr (createOldVarsSubst t) (OldExpressions.substOld h.snd (createFvar h.1.fst) e) :=by
+  intro Hnd
+  induction e
+  case app Hfn He =>
+    simp [OldExpressions.substsOldExpr, createOldVarsSubst, Map.isEmpty, OldExpressions.substOld, createFvar]
+    split; split; split
+    simp [OldExpressions.substOld, createFvar,Map.find? , *, createOldVarsSubst.go] at *
+    rename_i H; simp [← H, OldExpressions.substsOldExpr]
+    simp_all [OldExpressions.substOld, createFvar,Map.find?, createOldVarsSubst.go]
+    rename_i H _; split at H <;> simp_all [OldExpressions.substsOldExpr]
+    intro; simp_all [Map.isEmpty]; rename_i H; split at H <;> simp_all [Map.find?]
+    split <;> (rename_i H _; simp [*, createOldVarsSubst.go, Map.find?] at H)
+    split at H; contradiction
+    unfold OldExpressions.substsOldExpr
+    split <;> simp [*]
+    simp_all [createOldVarsSubst, createFvar]
+    rename_i fn e _ _ H
+    generalize H1: (OldExpressions.substOld h.snd (Lambda.LExpr.fvar h.fst.fst none) fn) = fn'
+    generalize H2: (OldExpressions.substOld h.snd (Lambda.LExpr.fvar h.fst.fst none) e) = e'
+    rw (occs := [3]) [Boogie.OldExpressions.substsOldExpr.eq_def]
+    simp; split
+    simp_all [Map.isEmpty]; rename_i H; split at H <;> simp_all
+    rw[OldExpressions.substOldExpr_nil, OldExpressions.substOldExpr_nil]; simp
+    split; split
+    unfold OldExpressions.substOld at H1
+    split at H1 <;> simp_all
+    unfold OldExpressions.substOld at H2
+    split at H2 <;> simp_all
+    split at H2; split at H2
+    any_goals simp_all
+    simp [← H2.left] at *
+    have : Map.find? (List.map createOldVarsSubst.go t) h.fst.fst = none :=by
+      simp [Imperative.substNodup, createOldStoreSubst, createOldStoreSubst.go] at Hnd
+      have Hnd := Hnd.right
+      have : List.map (Prod.fst ∘ createOldStoreSubst.go) t = List.map (Prod.fst ∘ createOldVarsSubst.go) t := by
+        simp [createOldStoreSubst.go, createOldVarsSubst.go]
+      have : ¬ h.fst.fst ∈ List.map (Prod.fst ∘ createOldVarsSubst.go) t := by
+       rw[← this]
+       rw [List.nodup_append] at Hnd
+       false_or_by_contra
+       have Hnd := Hnd.right.right h.fst.fst (by assumption) h.fst.fst (by simp)
+       contradiction
+      apply Map.findNone_eq_notmem_mapfst.mp
+      simp only [List.map_map]
+      assumption
+    simp_all
+    split at H1 <;> try simp_all
+    split at H1 <;> try simp_all
+    simp [OldExpressions.substsOldExpr]
+  any_goals simp [OldExpressions.substsOldExpr, OldExpressions.substOld, createOldVarsSubst, Map.isEmpty]
+  any_goals (split <;> rename_i H; split at H)
+  any_goals (simp_all [createOldVarsSubst];  rw [OldExpressions.substOldExpr_nil])
+  any_goals simp_all
+  any_goals (split at H <;> try contradiction)
+  any_goals simp_all [createOldVarsSubst]
+  any_goals rw [OldExpressions.substOldExpr_nil]
+  simp [createFvar]; rw [OldExpressions.substOldExpr_nil]
+
 theorem substsOldCorrect :
   Imperative.WellFormedSemanticEvalVar δ →
   Imperative.WellFormedSemanticEvalVal δ →
@@ -2244,71 +2311,43 @@ theorem substsOldCorrect :
   oldTrips.unzip.1.unzip.1.Disjoint (OldExpressions.extractOldExprVars e) →
   δ σ₀ σ e = δ σ₀' σ (OldExpressions.substsOldExpr (createOldVarsSubst oldTrips) e) := by
   intros Hwfvr Hwfvl Hwfc Hwf2 Hnorm Hsubst Hdef Hnd Hdisj
-  induction oldTrips generalizing e σ₀
-  repeat sorry
-  /-
+  induction oldTrips generalizing e
   case nil =>
-    simp [createOldVarsSubst, OldExpressions.substsOldExpr] at *
+    simp [createOldVarsSubst] at *; rw[OldExpressions.substOldExpr_nil]
     cases Hwf2 with
     | intro vs Hwf2 =>
       apply Lambda.LExpr.substFvarsCorrectZero Hwfc Hwfvr Hwfvl
       intros k1 k2 Hin
       simp [zip_self_eq Hin]
   case cons h t ih =>
-    simp [createOldVarsSubst, OldExpressions.substsOldExpr, OldExpressions.substsOldExpr] at *
-    simp [createOldVarsSubst.go]
-    simp [createOldStoreSubst, createOldStoreSubst.go] at Hsubst
-    have Hsubst1 := substStoresCons' Hnd Hdef Hsubst
-    cases Hsubst1 with
-    | intro σ₁ Hsubst1 =>
-    cases Hsubst1 with
-    | intro v₁ Hsubst1 =>
-    cases Hsubst1 with
-    | intro Hsome Hsubst1 =>
-    cases Hsubst1 with
-    | intro Hstore Hsubst1 =>
-    cases Hsubst1 with
-    | intro Hsubst' Hsubst1 =>
-    rw [← ih (σ₀ := σ₁)] <;> try simp_all
-    rw [← substOldCorrect (e := e) Hwfvr Hwfvl Hwfc Hwf2 Hnorm] <;> try simp_all
-    . apply invStoresSubstHead Hsubst'
-      simp [List.Disjoint] at Hdisj
-      simp_all
-    . -- substDefined
-      simp [createOldStoreSubst, createOldStoreSubst.go] at Hdef
-      intros k1 k2 Hin
-      apply Hdef <;> simp_all
-    . -- substStores
-      intros k1 k2 Hin
-      apply Hsubst <;> simp_all
-    . -- wfTwoState
-      refine updatedStateOldWellFormedBoogieEvalTwoState ?_ Hwf2
-      rw [← Hsubst]
-      exact Hsome
-      simp_all
-    . -- normalized expr
-      apply OldExpressions.substOldNormalizedMono
-      . simp [createFvar]
-        intros Hold
-        cases Hold
-      . simp_all
-      . simp [createFvar]
-        constructor
-    . simp [Imperative.substNodup, createOldStoreSubst] at Hnd ⊢
-      have Hnd2 := nodup_middle Hnd.2
-      simp_all
-    . -- substDefined
-      refine substDefined_updatedState ?_
-      exact substDefined_tail Hdef
-    . simp [Imperative.substNodup, createOldStoreSubst] at Hnd ⊢
-      have Hnd2 := nodup_middle Hnd.2
-      simp_all
-    . -- Disjoint
-      rw [substOld_create_replace] <;> try assumption
-      apply List.Disjoint.mono ?_ ?_ Hdisj
-      . simp
-      . simp [List.removeAll]
-  -/
+  have : OldExpressions.substsOldExpr (createOldVarsSubst (h :: t)) e
+          = OldExpressions.substsOldExpr (createOldVarsSubst t) (OldExpressions.substOld h.snd (createFvar h.1.fst) e) :=by
+    apply substOldExpr_cons Hnd
+  rw[this, ← ih]
+  apply substOldCorrect <;> try simp_all
+  intro k1 k2 Hin
+  simp [zip_self_eq Hin]
+  intro k1 k2 Hin
+  simp [Imperative.substDefined] at Hdef
+  apply Hdef; simp_all [createOldStoreSubst, createOldStoreSubst.go]
+  intro k1 k2 Hin
+  simp [Imperative.substStores] at Hsubst
+  apply Hsubst; simp_all [createOldStoreSubst, createOldStoreSubst.go]
+  apply OldExpressions.substOldNormalizedMono
+  intro H; cases H; assumption;
+  constructor
+  intro k1 k2 Hin
+  simp [Imperative.substStores] at Hsubst
+  apply Hsubst; simp_all [createOldStoreSubst, createOldStoreSubst.go]
+  exact substDefined_tail Hdef
+  simp [createOldStoreSubst] at *
+  exact substNodup_tail Hnd
+  simp at Hdisj
+  rw [substOld_create_replace] <;> try assumption
+  have H:= List.Disjoint.removeAll (zs:=[h.snd]) Hdisj
+  rw[← List.Disjoint_app] at H;
+  simp
+  exact List.Disjoint_cons_tail H.right
 
 theorem genArgExprIdent_len' : (List.mapM genArgExprIdent t s).fst.length = t.length := by
   induction t generalizing s <;> simp_all
@@ -3285,6 +3324,69 @@ theorem substOldPostSubset:
       intros x Hin
       simp_all
 
+theorem substOldExprPostSubset':
+  (Imperative.HasVarsPure.getVars (P:=Expression)
+    (OldExpressions.substsOldExpr [(h2, (Lambda.LExpr.fvar h1 ty))] post)).Subset
+    (Imperative.HasVarsPure.getVars (P:=Expression) post ++ [h1]) := by
+  rw [OldExpressions.substsOldExpr_singleton]
+  apply substOldPostSubset
+
+theorem substOldExprPostSubset'':
+  (Imperative.HasVarsPure.getVars (P:=Expression) post ++ [h1]) ⊆ S →
+  (Imperative.HasVarsPure.getVars (P:=Expression)
+    (OldExpressions.substsOldExpr [(h2, (Lambda.LExpr.fvar h1 ty))] post)) ⊆ S := by
+  have : (Imperative.HasVarsPure.getVars (P:=Expression)
+    (OldExpressions.substsOldExpr [(h2, (Lambda.LExpr.fvar h1 ty))] post)).Subset
+    (Imperative.HasVarsPure.getVars (P:=Expression) post ++ [h1]) := substOldExprPostSubset'
+  apply List.Subset.trans this
+
+open OldExpressions in
+theorem substOldExprPostSubset:
+  (Imperative.HasVarsPure.getVars (P:=Expression)
+    (substsOldExpr ((h2, (Lambda.LExpr.fvar h1 ty))::t) post)).Subset
+    (Imperative.HasVarsPure.getVars (P:=Expression) (substsOldExpr t post) ++ [h1]) := by
+  induction post
+  any_goals (simp only [Imperative.HasVarsPure.getVars, substsOldExpr, Map.isEmpty, Bool.false_eq_true, ↓reduceIte, ite_self] at *; try apply List.subset_append_left)
+  any_goals (by_cases Hnil: t = [] <;> (simp only [Hnil]; simp only [Bool.false_eq_true, ↓reduceIte, Lambda.LExpr.LExpr.getVars]); try apply substOldExprPostSubset'; try assumption)
+  any_goals (try simp only [Hnil, List.append_assoc] at *; try rw [OldExpressions.substOldExpr_nil] at *)
+  any_goals (apply List.append_subset.mpr; constructor <;> try apply List.Subset.trans (by assumption); try apply List.append_subset.mpr; constructor)
+  any_goals (apply List.append_subset.mpr; constructor)
+  any_goals apply List.Subset.assoc.mp
+  any_goals (apply List.Subset.subset_app_of_or_3; simp)
+  split <;> try split
+  any_goals (split <;> try split)
+  any_goals split
+  any_goals (simp [Map.find?] at *)
+  any_goals simp [Lambda.LExpr.LExpr.getVars]
+  any_goals (apply substOldExprPostSubset'')
+  any_goals (try apply List.Subset.trans (by assumption))
+  any_goals (apply List.append_subset.mpr; constructor)
+  any_goals (repeat apply List.Subset.assoc.mp)
+  any_goals apply List.Subset.subset_app_of_or_4
+  any_goals simp [Imperative.HasVarsPure.getVars]
+  rename_i H; simp [← H.right, Lambda.LExpr.LExpr.getVars]
+  constructor <;> (apply substOldExprPostSubset''; apply List.Subset.assoc.mp; apply List.append_subset.mpr; constructor <;> (apply List.Subset.subset_app_of_or_3; simp[Imperative.HasVarsPure.getVars]))
+  rename_i H _ _ _
+  split at H <;> try contradiction
+  apply List.Subset.subset_app_of_or_2
+  simp at H
+  simp [← H, Lambda.LExpr.LExpr.getVars]
+  simp_all
+  apply List.Subset.subset_app_of_or_2; simp
+  rename_i H _ _
+  split at H <;> try contradiction
+  simp at H
+  simp [← H, Lambda.LExpr.LExpr.getVars, List.Subset]
+  simp_all
+  rename_i H _ _ _
+  split at H <;> try contradiction
+  simp_all
+  unfold substsOldExpr; simp [Map.isEmpty, Lambda.LExpr.LExpr.getVars]
+  apply List.Subset.trans (by assumption)
+  any_goals (try apply List.Subset.trans (by assumption); apply List.append_subset.mpr <;> constructor)
+  apply List.append_subset.mpr; constructor
+  any_goals (try apply List.Subset.assoc.mp; apply List.Subset.subset_app_of_or_3; simp)
+
 open OldExpressions in
 theorem substsOldPostSubset:
   oldTrips.unzip.1.unzip.1.Disjoint oldTrips.unzip.2 →
@@ -3295,25 +3397,26 @@ theorem substsOldPostSubset:
     simp [createFvar, createOldVarsSubst, createOldVarsSubst.go] at *
   case nil =>
     intros x Hin
-    -- exact Hin
-    sorry
+    unfold substsOldExpr at Hin
+    simp [Map.isEmpty] at Hin
+    exact Hin
   case cons h t ih =>
-    apply List.Subset.trans
-      (b:=(Imperative.HasVarsPure.getVars
-            (P:=Expression) (substOld h.snd (Lambda.LExpr.fvar h.1.fst none) post)) ++
-            List.map (Prod.fst ∘ Prod.fst) t)
-    . -- apply ih
-      -- intros x Hin1 Hin2
-      -- apply @Hdisj x <;> simp_all
-      sorry
-    . apply List.Subset.app
-      apply List.Subset.trans
-      apply substOldPostSubset
-      . intros x Hin
-        simp at Hin
-        cases Hin <;> simp_all
-      . intros x Hin
-        simp_all
+    have Hdisj: (List.map (Prod.fst ∘ Prod.fst) t).Disjoint (List.map Prod.snd t) := by
+      apply List.Disjoint_Subsets Hdisj <;> apply List.subset_cons_self
+
+    have ih := @ih post Hdisj
+    have : (Imperative.HasVarsPure.getVars
+      (substsOldExpr ((h.snd, Lambda.LExpr.fvar h.1.fst none) :: List.map createOldVarsSubst.go t) post)).Subset
+          ((Imperative.HasVarsPure.getVars (substsOldExpr (List.map createOldVarsSubst.go t) post)) ++ [h.1.fst]) := by
+      apply substOldExprPostSubset
+    apply List.Subset.trans this
+    apply List.Subset.app _ (by simp [List.Subset])
+    apply List.Subset.trans ih
+    apply List.Subset.app
+    apply List.subset_append_left
+    apply List.subset_append_of_subset_right
+    apply List.subset_cons_self
+
 
 set_option maxHeartbeats 500000
 -- Second, the program/statement returned by callElim has the same semantics as the pre-transformation program/statement
@@ -4459,7 +4562,7 @@ theorem callElimStatementCorrect :
                                 exact BoogieIdent.Disjoint_isTemp_isGlobOrLocl
                                 exact BoogieIdent.isGlob_isGlobOrLocl
                           . simp [Holdtriplen]
-                        . apply List.Disjoint_Subset (ks:=(Imperative.HasVarsPure.getVars post))
+                        . apply List.Disjoint_Subset_right (ks:=(Imperative.HasVarsPure.getVars post))
                           . apply List.PredDisjoint_Disjoint
                                 (P:=(BoogieIdent.isTemp ·))
                                 (Q:=(BoogieIdent.isGlobOrLocl ·))

From 20ccaf49e636bbfd1ed33a6897735d216e23acb5 Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Tue, 7 Oct 2025 13:02:53 -0700
Subject: [PATCH 2/3] remove empty line

---
 Strata/Transform/CallElimCorrect.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Strata/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean
index daff39d6..508c60d8 100644
--- a/Strata/Transform/CallElimCorrect.lean
+++ b/Strata/Transform/CallElimCorrect.lean
@@ -1757,7 +1757,6 @@ theorem SubstPostsMem :
     substPost = OldExpressions.substsOldExpr (createOldVarsSubst oldTrips) (OldExpressions.normalizeOldExpr post)
   := by
   intros Hin
-
   generalize Heq : OldExpressions.substsOldExprs
                     (createOldVarsSubst oldTrips)
                     (OldExpressions.normalizeOldExprs vs) = l at *

From 7f034be614733ea1ac0d35a2ce75f6d3fca561e0 Mon Sep 17 00:00:00 2001
From: thanhnguyen-aws <ntson@amazon.com>
Date: Wed, 8 Oct 2025 15:24:36 -0700
Subject: [PATCH 3/3] delete white space

---
 Strata/Languages/Boogie/OldExpressions.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Strata/Languages/Boogie/OldExpressions.lean b/Strata/Languages/Boogie/OldExpressions.lean
index 9c56833e..f5556487 100644
--- a/Strata/Languages/Boogie/OldExpressions.lean
+++ b/Strata/Languages/Boogie/OldExpressions.lean
@@ -266,7 +266,7 @@ theorem substsOldExpr_singleton: substsOldExpr [(var,s)] e = substOld var s e :=
 theorem substOldExpr_nil: OldExpressions.substsOldExpr [] e = e := by
   unfold OldExpressions.substsOldExpr
   simp [Map.isEmpty]
-  
+
 /--
 For each `(var, expr)` pair in `sm`, substitute `old(var)` with `expr` in
 `conds`.