CallElimCorrect: rewrite using small-step semantics

Strata/DL/Imperative.lean

@@ -12,6 +12,7 @@ public import Strata.DL.Imperative.MetaData
 public import Strata.DL.Imperative.CmdEval
 public import Strata.DL.Imperative.CmdType
 public import Strata.DL.Imperative.CmdSemantics
+public import Strata.DL.Imperative.CmdSemanticsProps
 public import Strata.DL.Imperative.StmtSemantics
 
 public import Strata.DL.Imperative.KleeneStmt

Strata/DL/Imperative/CmdSemantics.lean

@@ -44,7 +44,7 @@ when the command signals a failure.
 @[expose] def isDefined {P : PureExpr} (σ : SemanticStore P) (vs : List P.Ident) : Prop :=
   ∀ v, v ∈ vs → (σ v).isSome = true
 
-def isNotDefined {P : PureExpr} (σ : SemanticStore P) (vs : List P.Ident) : Prop :=
+@[expose] def isNotDefined {P : PureExpr} (σ : SemanticStore P) (vs : List P.Ident) : Prop :=
   ∀ v, v ∈ vs → σ v = none
 
 -- Can make this more generic by supplying a predicate function
@@ -59,26 +59,26 @@ def isDefinedOver {P : PureExpr}
 /-! ### Store Substitution -/
 
 /-- Substitution relation between stores.  -/
-def substStores {P : PureExpr} (σ₁ σ₂ : SemanticStore P) (substs : List (P.Ident × P.Ident))
+@[expose] def substStores {P : PureExpr} (σ₁ σ₂ : SemanticStore P) (substs : List (P.Ident × P.Ident))
   : Prop :=
   ∀ k1 k2, (k1, k2) ∈ substs → σ₁ k1 = σ₂ k2
 
-def substDefined {P : PureExpr} (σ₁ σ₂ : SemanticStore P) (substs : List (P.Ident × P.Ident))
+@[expose] def substDefined {P : PureExpr} (σ₁ σ₂ : SemanticStore P) (substs : List (P.Ident × P.Ident))
   : Prop :=
   ∀ k1 k2, (k1, k2) ∈ substs → (σ₁ k1).isSome = true ∧ (σ₂ k2).isSome = true
 
-def substNodup {P : PureExpr} (substs : List (P.Ident × P.Ident))
+@[expose] def substNodup {P : PureExpr} (substs : List (P.Ident × P.Ident))
   : Prop := (substs.unzip.1 ++ substs.unzip.2).Nodup
 
 /-- a specialization of substitution, where the keys are the same -/
-def invStores {P : PureExpr} (σ₁ σ₂ : SemanticStore P) (vs : List P.Ident)
+@[expose] def invStores {P : PureExpr} (σ₁ σ₂ : SemanticStore P) (vs : List P.Ident)
   : Prop :=
   substStores σ₁ σ₂ $ vs.zip vs
 
 def invStoresExcept {P : PureExpr} (σ₁ σ₂ : SemanticStore P) (vs : List P.Ident)
   : Prop := ∀ (vs' : List P.Ident), vs'.Disjoint vs → invStores σ₁ σ₂ vs'
 
-def substSwap {P : PureExpr} (substs : List (P.Ident × P.Ident))
+@[expose] def substSwap {P : PureExpr} (substs : List (P.Ident × P.Ident))
   : List (P.Ident × P.Ident) := substs.map Prod.swap
 
 /-! ### Well-Formedness of `SemanticEval`s -/
@@ -94,7 +94,7 @@ def WellFormedSemanticEvalBool {P : PureExpr} [HasBool P] [HasNot P]
       (δ σ e = some Imperative.HasBool.tt ↔ δ σ (Imperative.HasNot.not e) = (some HasBool.ff)) ∧
       (δ σ e = some Imperative.HasBool.ff ↔ δ σ (Imperative.HasNot.not e) = (some HasBool.tt))
 
-def WellFormedSemanticEvalVal {P : PureExpr} [HasVal P]
+@[expose] def WellFormedSemanticEvalVal {P : PureExpr} [HasVal P]
     (δ : SemanticEval P) : Prop :=
   -- evaluator only evaluates to values
     (∀ v v' σ, δ σ v = some v' → HasVal.value v') ∧

Strata/DL/Imperative/CmdSemanticsProps.lean

@@ -9,7 +9,10 @@ public import Strata.DL.Imperative.CmdSemantics
 import all Strata.DL.Imperative.CmdSemantics
 import all Strata.DL.Imperative.Cmd
 public import Strata.DL.Imperative.Stmt
+public import Strata.DL.Util.ListUtils
+public import Strata.DL.Util.Nodup
 import all Strata.DL.Util.ListUtils
+import all Strata.DL.Util.Nodup
 
 ---------------------------------------------------------------------
 
@@ -371,4 +374,34 @@ theorem eval_cmd_set_comm
   have Heval1:= semantic_eval_eq_of_eval_cmd_set_unrelated_var Hwf Hnin2 Hs3
   exact eval_cmd_set_comm' Hneq Heval1 Heval2 Hs1 Hs2 Hs3 Hs4
 
+/-! ## `substDefined` / `substNodup` tail lemmas
+
+  Pure-Imperative property lemmas about `substDefined` / `substNodup`
+  that do not depend on any specific `PureExpr` instantiation (e.g.,
+  Core).  Live here rather than in `Strata.Transform.SubstProps`
+  because they are reusable across any transform that introduces fresh
+  variables and substitutes them. -/
+
+/-- The tail of a `substDefined` cons-list still satisfies `substDefined`. -/
+theorem subst_defined_tail
+    {P : PureExpr} {σ σ' : SemanticStore P}
+    {h : P.Ident × P.Ident}
+    {t : List (P.Ident × P.Ident)} :
+    Imperative.substDefined σ σ' (h :: t) →
+    Imperative.substDefined σ σ' t := by
+  intros Hsubst k1 k2 Hin
+  apply Hsubst
+  exact List.mem_cons_of_mem h Hin
+
+/-- The tail of a `substNodup` cons-list still satisfies `substNodup`. -/
+theorem subst_nodup_tail
+    {P : PureExpr}
+    {h : P.Ident × P.Ident}
+    {t : List (P.Ident × P.Ident)} :
+    Imperative.substNodup (h :: t) →
+    Imperative.substNodup t := by
+  intros Hsubst
+  simp [Imperative.substNodup] at *
+  exact (List.nodup_cons.mp (nodup_middle Hsubst.right)).right
+
 end -- public section

Strata/DL/Lambda/LExprWF.lean

@@ -327,7 +327,7 @@ Substitute `(.fvar x _)` in `e` with `to`. Does NOT lift de Bruijn indices in `t
 when going under binders - safe when `to` contains no bvars (e.g., substituting
 fvar→fvar). Use `substFvarLifting` when `to` contains bvars.
 -/
-def substFvar [BEq T.IDMeta] (e : LExpr ⟨T, GenericTy⟩) (fr : T.Identifier) (to : LExpr ⟨T, GenericTy⟩)
+@[expose] def substFvar [BEq T.IDMeta] (e : LExpr ⟨T, GenericTy⟩) (fr : T.Identifier) (to : LExpr ⟨T, GenericTy⟩)
   : (LExpr ⟨T, GenericTy⟩) :=
   match e with
   | .const _ _ => e | .bvar _ _ => e | .op _ _ _ => e
@@ -368,7 +368,7 @@ in a single pass, avoiding variable capture between substitutions.
 Does NOT lift de Bruijn indices when going under binders. Safe only when all
 replacement expressions contain no bvars.
 -/
-def substFvars [BEq T.IDMeta] (e : LExpr ⟨T, GenericTy⟩) (sm : Map T.Identifier (LExpr ⟨T, GenericTy⟩))
+@[expose] def substFvars [BEq T.IDMeta] (e : LExpr ⟨T, GenericTy⟩) (sm : Map T.Identifier (LExpr ⟨T, GenericTy⟩))
   : LExpr ⟨T, GenericTy⟩ :=
   if sm.isEmpty then e else substFvarsAux e sm
 where

Strata/DL/Util/ListUtils.lean

@@ -91,7 +91,7 @@ theorem List.Forall_append : Forall P (a ++ b) ↔ Forall P a ∧ Forall P b :=
 * `replace [1, 4, 2, 3, 3, 7] 5 6 = [1, 4, 2, 3, 3, 7]`
 Adapted from List.replace
 -/
-def List.replaceAll [BEq α] : List α → α → α → List α
+@[expose] def List.replaceAll [BEq α] : List α → α → α → List α
   | [],    _, _ => []
   | a::as, b, c => match b == a with
     | true  => c :: replaceAll as b c
@@ -260,7 +260,7 @@ theorem List.Subset.subset_app_of_or_4 {l: List α}: l ⊆ l1 ∨ l ⊆ l2 ∨ l
 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 α}:
+public 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
   case nil => simp [List.replaceAll]
@@ -278,7 +278,7 @@ theorem cons_removeAll [BEq α] {x : α} {xs ys : List α} :
         xs.removeAll ys := by
   simp [List.removeAll, List.filter_cons]
 
-theorem List.app_removeAll {α : Type} [BEq α] {xs₁ xs₂ ys : List α}:
+public theorem List.app_removeAll {α : Type} [BEq α] {xs₁ xs₂ ys : List α}:
   (xs₁ ++ xs₂).removeAll ys =
   (xs₁.removeAll ys) ++ (xs₂.removeAll ys) := by
   induction xs₁ <;> simp_all
@@ -325,13 +325,13 @@ theorem List.removeAll_comm {α : Type} [BEq α] {xs₁ xs₂ ys : List α}:
 
 /-- From Mathlib4 https://github.com/leanprover-community/mathlib4/blob/e70dc4ede17dd5fcda9926c84268e0f270147cba/Mathlib/Data/List/Zip.lean#L32-L37 -/
 @[simp]
-theorem zip_swap : ∀ (l₁ : List α) (l₂ : List β), (List.zip l₁ l₂).map Prod.swap = List.zip l₂ l₁
+public theorem zip_swap : ∀ (l₁ : List α) (l₂ : List β), (List.zip l₁ l₂).map Prod.swap = List.zip l₂ l₁
   | [], _ => List.zip_nil_right.symm
   | l₁, [] => by rw [List.zip_nil_right]; rfl
   | a :: l₁, b :: l₂ => by
     simp only [List.zip_cons_cons, List.map_cons, zip_swap l₁ l₂, Prod.swap_prod_mk]
 
-theorem replaceAll_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' k : α} {t: List α}:
+public theorem replaceAll_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' k : α} {t: List α}:
   k ∈ (t.replaceAll h h') → k ∈ t ∨ k = h' := by
   intros Hr
   induction t generalizing k h h' <;> simp [List.replaceAll] at *
@@ -348,21 +348,21 @@ theorem replaceAll_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' k : α} {t: L
       specialize ih hin
       cases ih <;> simp_all
 
-theorem zip_self_eq :
+public theorem zip_self_eq :
 (k1, k2) ∈ List.zip ks ks → k1 = k2 := by
   intros Hin
   induction ks <;> simp_all
   case cons h t ih =>
   cases Hin <;> simp_all
 
-theorem zip_self_eq' :
+public theorem zip_self_eq' :
 k ∈ ks → (k, k) ∈ List.zip ks ks := by
   intros Hin
   induction ks <;> simp_all
   case cons h t ih =>
   cases Hin <;> simp_all
 
-theorem in_replaceAll_removeAll {α : Type u} [BEq α] [LawfulBEq α] {h h' k2 : α} {vs t: List α}:
+public theorem in_replaceAll_removeAll {α : Type u} [BEq α] [LawfulBEq α] {h h' k2 : α} {vs t: List α}:
   k2 ∈ (vs.replaceAll h h').removeAll t → k2 = h' ∨ k2 ∈ vs.removeAll t := by
   intros H
   induction vs generalizing k2 <;> simp [List.removeAll, List.replaceAll] at *
@@ -380,7 +380,7 @@ theorem in_replaceAll_removeAll {α : Type u} [BEq α] [LawfulBEq α] {h h' k2 :
       have Hor := replaceAll_mem Hin
       cases Hor <;> simp_all
 
-theorem removeAll_cons {α : Type u} [BEq α] [LawfulBEq α] {k h : α} {vs t : List α} :
+public theorem removeAll_cons {α : Type u} [BEq α] [LawfulBEq α] {k h : α} {vs t : List α} :
   k ≠ h →
   k ∈ List.removeAll vs t →
   k ∈ List.removeAll vs (h :: t) := by
@@ -389,11 +389,11 @@ theorem removeAll_cons {α : Type u} [BEq α] [LawfulBEq α] {k h : α} {vs t :
   case cons h' t' ih =>
     simp_all
 
-theorem removeAll_sublist {α : Type u} [BEq α] [LawfulBEq α] (as bs : List α):
+public theorem removeAll_sublist {α : Type u} [BEq α] [LawfulBEq α] (as bs : List α):
   (List.removeAll as bs).Sublist as := by
   induction as <;> simp [List.removeAll]
 
-theorem replaceAll_not_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' : α} {vs : List α}:
+public theorem replaceAll_not_mem {α : Type u} [BEq α] [LawfulBEq α] {h h' : α} {vs : List α}:
   h ≠ h' →
   ¬ h ∈ (vs.replaceAll h h') := by
   intros Hne Hin
@@ -507,3 +507,131 @@ theorem List.Forall_flatMap :
     intros Hfa
     have Hfa := List.Forall_append.mp Hfa
     exact ⟨Hfa.1, ih Hfa.2⟩
+
+/-- Decompose a non-membership fact over a balanced 4-way append
+    `a ∉ (l₁ ++ l₂) ++ (l₃ ++ l₄)` into four leaf-level non-membership
+    facts.  Used at the L4 (preVars) and L6 (postVars) `Hinv` sites in
+    `callElimStatementCorrect` to flatten the per-`removeAll` decomposition
+    cascades. -/
+public theorem List.notin_append4
+    {α} {a : α} {l₁ l₂ l₃ l₄ : List α}
+    (Hnin : a ∉ (l₁ ++ l₂) ++ (l₃ ++ l₄)) :
+    a ∉ l₁ ∧ a ∉ l₂ ∧ a ∉ l₃ ∧ a ∉ l₄ :=
+  ⟨fun h => Hnin (List.mem_append.mpr (Or.inl (List.mem_append.mpr (Or.inl h)))),
+   fun h => Hnin (List.mem_append.mpr (Or.inl (List.mem_append.mpr (Or.inr h)))),
+   fun h => Hnin (List.mem_append.mpr (Or.inr (List.mem_append.mpr (Or.inl h)))),
+   fun h => Hnin (List.mem_append.mpr (Or.inr (List.mem_append.mpr (Or.inr h))))⟩
+
+/-- The length of `trips.unzip.snd` matches `trips.length`.  Convenient
+    one-liner used to bridge `genXxxExprIdentsTrip_snd` shape facts to a
+    `triplen` length equation, instead of inlining the `simp
+    [List.unzip_eq_map]` rewrite at every length proof. -/
+public theorem List.unzip_snd_length {α β : Type _} (trips : List (α × β)) :
+    trips.unzip.snd.length = trips.length := by
+  simp [List.unzip_eq_map]
+
+/-- Pairwise disjointness between three concatenated lists, extracted
+    from `(a ++ b ++ c).Nodup`.  Convenience re-packaging used downstream
+    to peel `cs'.generated`'s Nodup into per-segment disjointness. -/
+public theorem List.disjoint_of_nodup_append_three
+    {α} {a b c : List α}
+    (Hnd : (a ++ b ++ c).Nodup) :
+    a.Disjoint b ∧ a.Disjoint c ∧ b.Disjoint c := by
+  rw [List.append_assoc] at Hnd
+  have Hnd' := List.nodup_append.mp Hnd
+  have Hbc := List.nodup_append.mp Hnd'.2.1
+  refine ⟨?_, ?_, ?_⟩
+  · intro x hxa hxb
+    exact Hnd'.2.2 x hxa x (List.mem_append_left c hxb) rfl
+  · intro x hxa hxc
+    exact Hnd'.2.2 x hxa x (List.mem_append_right b hxc) rfl
+  · intro x hxb hxc
+    exact Hbc.2.2 x hxb x hxc rfl
+
+/-- If `(h, x) ∉ List.zip t t'` for every `x : β` and `t.length = t'.length`,
+    then `h ∉ t`.  Pure list lemma with no Imperative or Core dependencies. -/
+public theorem List.zip_notin_fst_pair {α β : Type _}
+    {h : α} {t : List α} {t' : List β} :
+    t.length = t'.length →
+    (∀ x, ¬(h, x) ∈ List.zip t t') →
+    ¬ h ∈ t := by
+  intros Hlen H
+  induction t generalizing t' h <;> simp_all
+  case cons h t ih =>
+    cases t' with
+    | nil => simp at Hlen
+    | cons h' t' =>
+      simp_all
+      have HH := H h'
+      simp_all
+      exact ih rfl H
+
+/-- Symmetric to `zip_notin_fst_pair`: if `(x, h) ∉ List.zip t t'` for every
+    `x : α` and `t.length = t'.length`, then `h ∉ t'`. -/
+public theorem List.zip_notin_snd_pair {α β : Type _}
+    {h : β} {t : List α} {t' : List β} :
+    t.length = t'.length →
+    (∀ x, ¬(x, h) ∈ List.zip t t') →
+    ¬ h ∈ t' := by
+  intros Hlen H
+  induction t' generalizing t h <;> simp_all
+  case cons h t ih =>
+    cases t with
+    | nil => simp at Hlen
+    | cons h' t' =>
+      simp_all
+      have HH := H h'
+      simp_all
+      exact ih Hlen H
+
+/-- Decompose `(ks.zip ks').get n = (k1, k2)` into per-component equalities,
+    given explicit bounds for each list. -/
+public theorem List.zip_pair_split {α β} {ks : List α} {ks' : List β}
+    {n : Fin (ks.zip ks').length} {k1 : α} {k2 : β}
+    (hn : n.val < ks.length) (hn' : n.val < ks'.length)
+    (heq : (ks.zip ks').get n = (k1, k2)) :
+    k1 = ks[n.val]'hn ∧ k2 = ks'[n.val]'hn' := by
+  rw [show (ks.zip ks').get n = (ks.zip ks')[n.val]'n.isLt from rfl,
+      List.getElem_zip] at heq
+  exact ⟨((Prod.mk.injEq _ _ _ _).mp heq.symm).1,
+         ((Prod.mk.injEq _ _ _ _).mp heq.symm).2⟩
+
+/-- Decompose `(a ++ b ++ c).Nodup` into its three component-Nodups and three
+    pairwise disjointnesses (in the local `List.Disjoint` form: `a → b → False`).
+    Repackages `List.nodup_append` and `List.disjoint_of_nodup_append_three`. -/
+public theorem List.nodup_3_decompose {α} {a b c : List α}
+    (Hnd : (a ++ b ++ c).Nodup) :
+    a.Nodup ∧ b.Nodup ∧ c.Nodup ∧
+      a.Disjoint b ∧ a.Disjoint c ∧ b.Disjoint c :=
+  let Hsplit := List.nodup_append.mp Hnd
+  let Hab := List.nodup_append.mp Hsplit.1
+  let ⟨Hd_ab, Hd_ac, Hd_bc⟩ := List.disjoint_of_nodup_append_three Hnd
+  ⟨Hab.1, Hab.2.1, Hsplit.2.1, Hd_ab, Hd_ac, Hd_bc⟩
+
+/-- Build `x ∉ a ++ b ++ c` from per-list non-membership. -/
+public theorem List.notin_3_append_of {α} [DecidableEq α] {a b c : List α} {x : α}
+    (h₁ : x ∉ a) (h₂ : x ∉ b) (h₃ : x ∉ c) : x ∉ a ++ b ++ c := by
+  simp only [List.mem_append, not_or]; exact ⟨⟨h₁, h₂⟩, h₃⟩
+
+/-- Project the snd-component out of a doubly-zipped triple-list, given the
+    matching length facts.  Pure list-shape geometry helper used in
+    trip-shape computations. -/
+public theorem List.zip_zip_unzip_snd_of_lengths {α β γ}
+    {g : List α} {ys : List β} {xs : List γ}
+    (Hgx : g.length = xs.length) (Hyx : ys.length = xs.length) :
+    ((g.zip ys).zip xs).unzip.snd = xs := by
+  rw [List.unzip_zip_right]
+  rw [List.length_zip]
+  omega
+
+/-- Project the fst-fst-component out of a doubly-zipped triple-list, given
+    the matching length facts.  Pure list-shape geometry helper. -/
+public theorem List.zip_zip_unzip_fst_unzip_fst_of_lengths {α β γ}
+    {g : List α} {ys : List β} {xs : List γ}
+    (Hgx : g.length = xs.length) (Hyx : ys.length = xs.length) :
+    ((g.zip ys).zip xs).unzip.fst.unzip.fst = g := by
+  rw [List.unzip_zip_left (l₁ := (g.zip ys)) (l₂ := xs)]
+  · rw [List.unzip_zip_left (l₁ := g) (l₂ := ys)]
+    omega
+  · rw [List.length_zip]
+    omega

Strata/DL/Util/StringGen.lean

@@ -42,6 +42,7 @@ def StringGenState.emp : StringGenState := { cs := .emp, generated := [] }
   followed by an underscore (`_`), followed by a unique number given by its
   underlying counter `σ.cs`.
  -/
+@[expose]
 def StringGenState.gen (pf : String) (σ : StringGenState) : String × StringGenState :=
   let (counter, cs) := Counter.genCounter σ.cs
   let newString : String := (pf ++ "_" ++ toString counter)

Strata/Languages/Core/CoreGen.lean

@@ -27,6 +27,7 @@ structure CoreGenState where
   cs : StringGenState
   generated : List CoreIdent := []
 
+@[expose]
 def CoreGenState.WF (σ : CoreGenState)
   := StringGenState.WF σ.cs ∧
     List.map (fun s => (⟨s, ()⟩ : CoreIdent)) σ.cs.generated.unzip.snd = σ.generated ∧
@@ -42,6 +43,7 @@ def CoreGenState.emp : CoreGenState := { cs := .emp, generated := [] }
     NOTE: we need to wrap the prefix into a CoreIdent in order to conform with the interface of UniqueLabelGen.gen
     TODO: Maybe use genIdent or genIdents?
     -/
+@[expose]
 def CoreGenState.gen (pf : CoreIdent) (σ : CoreGenState)
   : CoreIdent × CoreGenState :=
   let (s, cs') := StringGenState.gen pf.name σ.cs

Strata/Languages/Core/Procedure.lean

@@ -255,17 +255,25 @@ def Procedure.Spec.preconditionNames (s : Procedure.Spec) : List CoreLabel :=
 def Procedure.Spec.postconditionNames (s : Procedure.Spec) : List CoreLabel :=
   s.postconditions.keys
 
+/-- Non-`Free` preconditions: those that are *checked* at call sites.
+    See `Procedure.CheckAttr` and Procedure.lean §92 for the meaning of `Free`. -/
+@[expose] abbrev Procedure.Spec.checkedPreconditions (s : Procedure.Spec) :
+    List (CoreLabel × Procedure.Check) :=
+  s.preconditions.filter (fun (_, c) => c.attr ≠ .Free)
+
 def Procedure.Spec.eraseTypes (s : Procedure.Spec) : Procedure.Spec :=
   { s with
     preconditions := s.preconditions.map (fun (l, c) => (l, c.eraseTypes)),
     postconditions := s.postconditions.map (fun (l, c) => (l, c.eraseTypes))
   }
 
+@[expose]
 def Procedure.Spec.getCheckExprs (conds : ListMap CoreLabel Procedure.Check) :
   List Expression.Expr :=
   let checks := conds.values
   checks.map (fun c => c.expr)
 
+@[expose]
 def Procedure.Spec.updateCheckExprs
   (es : List Expression.Expr) (conds : ListMap CoreLabel Procedure.Check) :
   ListMap CoreLabel Procedure.Check :=