CallElimCorrect: lift _terminal to polymorphic {f : Bool}

Strata/Languages/Core/StatementSemantics.lean

@@ -413,10 +413,13 @@ inductive EvalCommandContract : (String → Option Procedure)  → CoreEval →
   /-- Contract-based semantics: like `EvalCommand.call_sem` but replaces
       body execution with havoc + postcondition check.
       The Bool failure flag `failed` is connected to the precondition status
-      via an iff: the call fails iff some precondition fails to evaluate to
-      `tt` at the post-init/pre-havoc store `σAO`.  When `failed = true`,
-      the result store is unchanged (`σ' = σ`); when `failed = false`, the
-      result store is produced by havoc + write-back via `UpdateStates`.
+      via an iff: the call fails iff some *checked* precondition fails to
+      evaluate to `tt` at the post-init/pre-havoc store `σAO`.  Free
+      preconditions (`free requires`) are assumed by the implementation but
+      not checked at call sites (Procedure.lean §92), so they are excluded
+      from the iff — the iff and definedness premises both range over
+      non-Free preconditions only.  The result store `σ'` is unconditionally
+      the writeback result via `UpdateStates`, regardless of `failed`.
       Same positional matching as `EvalCommand.call_sem`. -/
   | call_sem {π δ σ σ₀ inArgs oVals vals σA σAO σO n p modvals callArgs σ' md failed} :
     π n = .some p →
@@ -433,21 +436,23 @@ inductive EvalCommandContract : (String → Option Procedure)  → CoreEval →
     InitStates σ (ListMap.keys (p.header.inputs)) vals σA →
     -- positional: oVals[i] initializes p.header.outputs[i]
     InitStates σA (ListMap.keys (p.header.outputs)) oVals σAO →
-    -- preconditions are always defined; their truth controls `failed`
-    (∀ pre, (Procedure.Spec.getCheckExprs p.spec.preconditions).contains pre →
+    -- non-Free preconditions are always defined; their truth controls `failed`
+    (∀ pre, (Procedure.Spec.getCheckExprs
+              (p.spec.preconditions.filter
+                (fun (_, c) => c.attr ≠ .Free))).contains pre →
       isDefinedOver (HasVarsPure.getVars) σAO pre) →
     (failed = false ↔
-      (∀ pre, (Procedure.Spec.getCheckExprs p.spec.preconditions).contains pre →
+      (∀ pre, (Procedure.Spec.getCheckExprs
+                (p.spec.preconditions.filter
+                  (fun (_, c) => c.attr ≠ .Free))).contains pre →
         δ σAO pre = .some HasBool.tt)) →
     HavocVars σAO (ListMap.keys p.header.outputs) σO →
     (∀ post, (Procedure.Spec.getCheckExprs p.spec.postconditions).contains post →
       isDefinedOver (HasVarsPure.getVars) σAO post ∧
       δ σO post = .some HasBool.tt) →
     ReadValues σO (ListMap.keys (p.header.outputs)) modvals →
-    -- success path: positional write-back
-    (failed = false → UpdateStates σ lhs modvals σ') →
-    -- failure path: store unchanged
-    (failed = true → σ' = σ) →
+    -- positional write-back (unconditional)
+    UpdateStates σ lhs modvals σ' →
     ----
     EvalCommandContract π δ σ (.call n callArgs md) σ' failed
 

Strata/Languages/Core/StatementSemanticsProps.lean

@@ -2200,215 +2200,6 @@ theorem InvStoresExceptInvStores :
   exact List.Disjoint.symm Hdis
   assumption
 
-/-
-NOTE:
-  In order to prove this refinement theorem, we need to reason about the
-  asymmetry between the two semantics regarding the temporary variables
-  created in the concrete semantics. That is, evaluating the procedure body may
-  create new variables in the store, and since the temporary variables are
-  discarded at the end of the call, it is possible to show that those created
-  variables are irrelevant.
--/
-/--
-Refinement of a procedure call from concrete (Layer-A small-step body trace)
-semantics to contract (havoc-and-postcondition) semantics.
-
-The proof requires three side-conditions that the concrete `call_sem`
-constructor does not by itself supply:
-
-* `δ_wfCong` — the evaluator respects free-variable congruence; needed to
-  rewrite `δ ρ'.store post` into `δ σO post` (where `σO` is the post-havoc
-  store the contract semantics evaluates against).
-
-* `p_outputs_nodup` — the procedure's output parameter list has no duplicate
-  keys; needed by `readValues_updatedStatesSame` to construct
-  `ReadValues σO outs modvals`.
-
-* `p_post_scoped` — every postcondition's free variables are a subset of
-  the output parameters.  This is the well-formed-postcondition assumption
-  that lets us reduce the per-key store agreement to the output keys.
-  Without this assumption, the proof would also need a body-locals
-  invariance lemma over `CoreStepStar` (i.e., a structural lemma like
-  `stmts_invStoresExcept_modifiedVarsTrans`); none such exists in the
-  codebase yet.  Since `p_post_scoped` is a natural well-formedness
-  consequence of `WFProcedureProp` (postconditions reference only the
-  procedure's outputs) we take it as a hypothesis here and let the caller
-  discharge it.
--/
-theorem EvalCallBodyRefinesContract :
-  ∀ {π : String → Option Procedure}
-    {φ : CoreEval → PureFunc Expression → CoreEval}
-    {δ : CoreEval} {σ : CoreStore} {n : String}
-    {callArgs : List (CallArg Expression)} {σ' : CoreStore}
-    {p : Procedure} {md md' : MetaData Expression},
-  WellFormedSemanticEvalExprCongr δ →
-  (ListMap.keys p.header.outputs).Nodup →
-  (∀ post : Expression.Expr,
-    (Procedure.Spec.getCheckExprs p.spec.postconditions).contains post →
-    (HasVarsPure.getVars (P := Expression) post).Subset (ListMap.keys p.header.outputs)) →
-  π n = .some p →
-  EvalCommand π φ δ σ (CmdExt.call n callArgs md) σ' false →
-  EvalCommandContract π δ σ (CmdExt.call n callArgs md') σ' false := by
-  intros π φ δ σ n callArgs σ' p md md'
-         δ_wfCong p_outputs_nodup p_post_scoped pFound H
-  -- Generalize `false` so dependent elimination produces an equality
-  -- between the constructor's `ρ'.hasFailure` and the goal's index.
-  generalize hf : (false : Bool) = b at H
-  cases H with
-  | @call_sem _ _ _ σ₀ inArgs vals oVals σA σAO _ p_c modvals _ σ_final ρ' _
-              hπ heqIn heqLhs Hev_in HrdLhs hwfV hwfVar hwfBool hwf2s hdef
-              Hin_inputs Hin_outputs Hpre Hbody Hpost_at_ρ' Hrd_body Hupd =>
-    -- Unify the case-bound `p_c` with the theorem-level `p`.
-    rw [pFound] at hπ
-    have hp_eq := Option.some.inj hπ
-    subst hp_eq
-    -- ρ'.hasFailure = false from generalize equation.
-    have hρ'_failure := hf.symm
-    -- Bind σO := updatedStates σAO outs modvals as a definitional unfold.
-    -- Length: outs.length = modvals.length (from Hrd_body).
-    have h_len := ReadValuesLength Hrd_body
-    -- `outs` are defined in σAO (initialized via Hin_outputs).
-    have h_def := InitStatesDefined Hin_outputs
-    -- HavocVars step: σAO can havoc to σO := updatedStates σAO outs modvals.
-    have h_upd := updatedStatesUpdate h_len h_def
-    have h_havoc := UpdateStatesHavocVars h_upd
-    -- ReadValues σO outs modvals, by readValues_updatedStatesSame.
-    have h_rd_σO :
-        ReadValues
-          (updatedStates σAO (ListMap.keys p.header.outputs) modvals)
-          (ListMap.keys p.header.outputs) modvals :=
-      readValues_updatedStatesSame h_len p_outputs_nodup
-    -- Postconditions transport from ρ'.store to σO via δ_wfCong.
-    have h_post : ∀ post : Expression.Expr,
-        (Procedure.Spec.getCheckExprs p.spec.postconditions).contains post →
-        isDefinedOver (HasVarsPure.getVars (P := Expression)) σAO post ∧
-        δ (updatedStates σAO (ListMap.keys p.header.outputs) modvals) post
-          = some HasBool.tt := by
-      intros post hin
-      have ⟨hdefp, heq⟩ := Hpost_at_ρ' post hin
-      refine ⟨hdefp, ?_⟩
-      -- σO and ρ'.store agree on getVars(post) (subset of outs).
-      have h_agree : ∀ x ∈ HasVarsPure.getVars (P := Expression) post,
-          updatedStates σAO (ListMap.keys p.header.outputs) modvals x
-            = ρ'.store x := by
-        intros x hx
-        have hx_in_outs : x ∈ (ListMap.keys p.header.outputs) :=
-          p_post_scoped post hin hx
-        -- Both σO x and ρ'.store x equal modvals[i] for x = outs[i].
-        have ⟨i, hi_lt, hi_eq⟩ :
-            ∃ i, ∃ (h : i < (ListMap.keys p.header.outputs).length),
-              (ListMap.keys p.header.outputs)[i]'h = x :=
-          List.getElem_of_mem hx_in_outs
-        have hi_lt' : i < modvals.length := h_len ▸ hi_lt
-        have hl := hi_eq ▸ readValues_get h_rd_σO (hi := hi_lt) (hi' := hi_lt')
-        have hr := hi_eq ▸ readValues_get Hrd_body (hi := hi_lt) (hi' := hi_lt')
-        rw [hl, hr]
-      -- Apply expression congruence.
-      rw [δ_wfCong post _ _ h_agree]
-      exact heq
-    -- ρ'.hasFailure = false closes the index mismatch in the goal.
-    rw [hρ'_failure]
-    -- Split the combined Hpre into the new (def, iff) shape required by the
-    -- bool-indicator EvalCommandContract.call_sem rule.
-    have Hpre_def : ∀ pre,
-        (Procedure.Spec.getCheckExprs p.spec.preconditions).contains pre →
-        isDefinedOver (HasVarsPure.getVars (P := Expression)) σAO pre :=
-      fun pre h => (Hpre pre h).1
-    have Hpre_iff :
-        (false = false ↔
-          ∀ pre, (Procedure.Spec.getCheckExprs p.spec.preconditions).contains pre →
-            δ σAO pre = .some HasBool.tt) :=
-      ⟨fun _ pre h => (Hpre pre h).2, fun _ => rfl⟩
-    exact EvalCommandContract.call_sem pFound heqIn heqLhs Hev_in HrdLhs hwfV hwfVar hwfBool
-            hwf2s hdef Hin_inputs Hin_outputs Hpre_def Hpre_iff h_havoc h_post h_rd_σO
-            (fun _ => Hupd) (fun h => Bool.noConfusion h)
-
-/-- `EvalCommand` with concrete semantics (`f = false` non-failure case)
-    refines `EvalCommandContract`.  Threads through the three side-conditions
-    needed by `EvalCallBodyRefinesContract`. -/
-theorem EvalCommandRefinesContract
-    {π : String → Option Procedure}
-    {φ : CoreEval → PureFunc Expression → CoreEval}
-    {δ : CoreEval} {σ σ' : CoreStore} {c : Command}
-    (δ_wfCong : @Imperative.WellFormedSemanticEvalExprCongr Expression _ δ)
-    (π_wf : ∀ {n : String} {p : Procedure}, π n = .some p →
-      (ListMap.keys p.header.outputs).Nodup ∧
-      (∀ post : Expression.Expr,
-        (Procedure.Spec.getCheckExprs p.spec.postconditions).contains post →
-        (HasVarsPure.getVars (P := Expression) post).Subset
-          (ListMap.keys p.header.outputs))) :
-    EvalCommand π φ δ σ c σ' false →
-    EvalCommandContract π δ σ c σ' false := by
-  intro H
-  -- Generalize the failure-flag index to enable dependent elimination on H.
-  generalize hb : (false : Bool) = b at H
-  cases H with
-  | cmd_sem H' =>
-    cases hb
-    exact EvalCommandContract.cmd_sem H'
-  | @call_sem _ _ _ σ₀ inArgs vals oVals σA σAO _ p_c modvals _ _ ρ' _
-              hπ heqIn heqLhs Hev_in HrdLhs hwfV hwfVar hwfBool hwf2s hdef
-              Hin_inputs Hin_outputs Hpre Hbody Hpost_at_ρ' Hrd_body Hupd =>
-    -- ρ'.hasFailure = false from generalize equation
-    have hρ'_failure : ρ'.hasFailure = false := hb.symm
-    have ⟨h_outs_nodup, h_post_scoped⟩ := π_wf hπ
-    -- Apply the leaf refinement (with md' := md) under the failure rewrite.
-    exact hρ'_failure ▸
-      EvalCallBodyRefinesContract δ_wfCong h_outs_nodup h_post_scoped hπ
-        (hρ'_failure ▸ EvalCommand.call_sem hπ heqIn heqLhs Hev_in HrdLhs hwfV
-          hwfVar hwfBool hwf2s hdef Hin_inputs Hin_outputs Hpre Hbody
-          Hpost_at_ρ' Hrd_body Hupd)
-
-/-- A single `StepStmt` with `EvalCommand` ending in a non-failed terminal can
-    be simulated by a single `StepStmt` with `EvalCommandContract`.  Threads
-    through the three side-conditions plus an explicit non-failure witness. -/
-private theorem StepStmt_refines_contract
-    {π : String → Option Procedure}
-    {φ : CoreEval → PureFunc Expression → CoreEval}
-    {c₁ c₂ : Imperative.Config Expression Command}
-    (δ_wfCong : @Imperative.WellFormedSemanticEvalExprCongr Expression _ c₁.getEnv.eval)
-    (π_wf : ∀ {n : String} {p : Procedure}, π n = .some p →
-      (ListMap.keys p.header.outputs).Nodup ∧
-      (∀ post : Expression.Expr,
-        (Procedure.Spec.getCheckExprs p.spec.postconditions).contains post →
-        (HasVarsPure.getVars (P := Expression) post).Subset
-          (ListMap.keys p.header.outputs)))
-    (h_no_fail : c₂.getEnv.hasFailure = false) :
-    Imperative.StepStmt Expression (EvalCommand π φ) (EvalPureFunc φ) c₁ c₂ →
-    Imperative.StepStmt Expression (EvalCommandContract π) (EvalPureFunc φ) c₁ c₂ := by
-  intro H
-  induction H with
-  | @step_cmd ρ c σ' hasAssertFailure hcmd =>
-    -- step_cmd produces hasFailure := ρ.hasFailure || hasAssertFailure.
-    -- h_no_fail says this OR is false; extract that hasAssertFailure = false.
-    simp only [Imperative.Config.getEnv] at h_no_fail
-    have ⟨_, h_aff⟩ := Bool.or_eq_false_iff.mp h_no_fail
-    subst h_aff
-    -- δ_wfCong is at c₁.getEnv.eval = ρ.eval
-    simp only [Imperative.Config.getEnv] at δ_wfCong
-    exact .step_cmd (EvalCommandRefinesContract δ_wfCong π_wf hcmd)
-  | step_seq_inner _ ih => exact .step_seq_inner (ih δ_wfCong h_no_fail)
-  | step_block_body _ ih => exact .step_block_body (ih δ_wfCong h_no_fail)
-  | step_block => exact .step_block
-  | step_ite_true h1 h2 => exact .step_ite_true h1 h2
-  | step_ite_false h1 h2 => exact .step_ite_false h1 h2
-  | step_ite_nondet_true => exact .step_ite_nondet_true
-  | step_ite_nondet_false => exact .step_ite_nondet_false
-  | step_loop_enter h1 h2 h3 h4 => exact .step_loop_enter h1 h2 h3 h4
-  | step_loop_exit h1 h2 h3 h4 => exact .step_loop_exit h1 h2 h3 h4
-  | step_loop_nondet_enter h1 h2 => exact .step_loop_nondet_enter h1 h2
-  | step_loop_nondet_exit h1 h2 => exact .step_loop_nondet_exit h1 h2
-  | step_exit => exact .step_exit
-  | step_funcDecl => exact .step_funcDecl
-  | step_typeDecl => exact .step_typeDecl
-  | step_stmts_nil => exact .step_stmts_nil
-  | step_stmts_cons => exact .step_stmts_cons
-  | step_seq_done => exact .step_seq_done
-  | step_seq_exit => exact .step_seq_exit
-  | step_block_done => exact .step_block_done
-  | step_block_exit_match h => exact .step_block_exit_match h
-  | step_block_exit_mismatch h => exact .step_block_exit_mismatch h
-
 /-- If an expression is defined, all its free variables are defined in the store.
     Relies on the definedness propagation properties in `WellFormedCoreEvalCong`
     together with the variable-evaluation condition in `WellFormedSemanticEvalVar`. -/
@@ -2666,86 +2457,6 @@ theorem core_wfExprCongr_preserved
   | step _ _ _ hstep _ ih =>
     exact ih (core_step_preserves_wfExprCongr π φ h_wf_ext _ _ hwf₀ hstep)
 
-/-- Small-step star with `EvalCommand` ending in non-failure refines
-    `EvalCommandContract`.  Uses `StepStmtStar_hasFailure_monotone` to back-
-    propagate the non-failure witness, and `core_step_preserves_wfExprCongr`
-    to refresh the expression-congruence hypothesis after each step. -/
-theorem StepStmtStar_refines_contract
-    {π : String → Option Procedure}
-    {φ : CoreEval → PureFunc Expression → CoreEval}
-    {c₁ c₂ : Imperative.Config Expression Command}
-    (h_wf_ext : WFEvalExtension φ)
-    (π_wf : ∀ {n : String} {p : Procedure}, π n = .some p →
-      (ListMap.keys p.header.outputs).Nodup ∧
-      (∀ post : Expression.Expr,
-        (Procedure.Spec.getCheckExprs p.spec.postconditions).contains post →
-        (HasVarsPure.getVars (P := Expression) post).Subset
-          (ListMap.keys p.header.outputs)))
-    (δ_wfCong : @Imperative.WellFormedSemanticEvalExprCongr Expression _ c₁.getEnv.eval)
-    (h_no_fail : c₂.getEnv.hasFailure = false) :
-    Imperative.StepStmtStar Expression (EvalCommand π φ) (EvalPureFunc φ) c₁ c₂ →
-    Imperative.StepStmtStar Expression (EvalCommandContract π) (EvalPureFunc φ) c₁ c₂ := by
-  intro H
-  -- Generalize δ_wfCong and h_no_fail so the IH stays usable across steps.
-  revert δ_wfCong h_no_fail
-  induction H with
-  | refl => intros; exact .refl _
-  | @step c₁ cm c₂ hstep hrest ih =>
-    intro δ_wfCong h_no_fail
-    -- Backwards-propagate the no-failure witness via monotonicity:
-    -- case-split on cm.getEnv.hasFailure; the `true` case contradicts
-    -- h_no_fail by `StepStmtStar_hasFailure_monotone`.
-    have h_cm_no_fail : cm.getEnv.hasFailure = false := by
-      cases hcm : cm.getEnv.hasFailure
-      · rfl
-      · have h_c2_true :=
-          Imperative.StepStmtStar_hasFailure_monotone Expression
-            (EvalCommand π φ) (EvalPureFunc φ) hrest hcm
-        rw [h_c2_true] at h_no_fail
-        exact Bool.noConfusion h_no_fail
-    -- Refresh δ_wfCong for the IH at cm.
-    have hwf_cm : @Imperative.WellFormedSemanticEvalExprCongr Expression _ cm.getEnv.eval :=
-      core_step_preserves_wfExprCongr π φ h_wf_ext _ _ δ_wfCong hstep
-    exact .step _ _ _
-      (StepStmt_refines_contract δ_wfCong π_wf h_cm_no_fail hstep)
-      (ih hwf_cm h_no_fail)
-
-/-- `EvalStatements` with concrete semantics refines contract semantics. -/
-theorem EvalStatementsRefinesContract
-    {π : String → Option Procedure}
-    {φ : CoreEval → PureFunc Expression → CoreEval}
-    {ρ ρ' : Env Expression} {ss : List Statement}
-    (h_wf_ext : WFEvalExtension φ)
-    (π_wf : ∀ {n : String} {p : Procedure}, π n = .some p →
-      (ListMap.keys p.header.outputs).Nodup ∧
-      (∀ post : Expression.Expr,
-        (Procedure.Spec.getCheckExprs p.spec.postconditions).contains post →
-        (HasVarsPure.getVars (P := Expression) post).Subset
-          (ListMap.keys p.header.outputs)))
-    (δ_wfCong : @Imperative.WellFormedSemanticEvalExprCongr Expression _ ρ.eval)
-    (h_no_fail : ρ'.hasFailure = false) :
-    EvalStatements π φ ρ ss ρ' →
-    EvalStatementsContract π φ ρ ss ρ' :=
-  StepStmtStar_refines_contract h_wf_ext π_wf δ_wfCong h_no_fail
-
-/-- `EvalStatement` with concrete semantics refines contract semantics. -/
-theorem EvalStatementRefinesContract
-    {π : String → Option Procedure}
-    {φ : CoreEval → PureFunc Expression → CoreEval}
-    {ρ ρ' : Env Expression} {s : Statement}
-    (h_wf_ext : WFEvalExtension φ)
-    (π_wf : ∀ {n : String} {p : Procedure}, π n = .some p →
-      (ListMap.keys p.header.outputs).Nodup ∧
-      (∀ post : Expression.Expr,
-        (Procedure.Spec.getCheckExprs p.spec.postconditions).contains post →
-        (HasVarsPure.getVars (P := Expression) post).Subset
-          (ListMap.keys p.header.outputs)))
-    (δ_wfCong : @Imperative.WellFormedSemanticEvalExprCongr Expression _ ρ.eval)
-    (h_no_fail : ρ'.hasFailure = false) :
-    EvalStatement π φ ρ s ρ' →
-    EvalStatementContract π φ ρ s ρ' :=
-  StepStmtStar_refines_contract h_wf_ext π_wf δ_wfCong h_no_fail
-
 /-! ## projectStore and expression evaluation -/
 
 /-- If an expression evaluates in the projected store, it evaluates identically