CallElimCorrect: rewrite using small-step semantics

[PROgram52bc]

Summary

This PR replaces the deprecated big-step CallElimCorrect proof with a small-step version, plus reusable infrastructure (SubstProps, CoreTransformProps) and shared-file helpers. The previous file carried a DEPRECATED notice flagging it for a small-step rewrite; this is that rewrite.

Top-level public theorem callElimStatementCorrect is preserved (now a conjunction over a _terminal arm and an _exiting arm), the contract semantics for procedure calls (EvalCommandContract.call_sem) is unified into a single failure-flag–parameterized rule, and the _terminal arm is fully polymorphic over the failure flag ({f : Bool}) — a source success trace maps to a target success trace and a source failure trace maps to a target failure trace, in one statement.

Net repository delta vs main2: +9,277 / -4,861 LoC across 19 files (the bulk being reusable infrastructure rather than CallElim-specific). Compared to the original 14,972-LoC big-step proof, this represents a ~-8k LoC reduction overall, while strictly strengthening what is proved.

What's added

The 19 files modified group into 4 layers:

Top-level proof (~10,525 LoC churn)

• Strata/Transform/CallElimCorrect.lean: full rewrite against small-step semantics. Same public theorem name callElimStatementCorrect; structured as _terminal ∧ ∀ lbl, _exiting, mirroring Specification.Overapproximates and TripleBlock. The _terminal arm is polymorphic in the failure flag {f : Bool}; the _exiting arm reuses the original Heval for non-call cases and is vacuously discharged for the call case (a singleton call statement only ever reaches .terminal, never .exiting).

Reusable infrastructure (~2,747 LoC, new files)

• Strata/Transform/SubstProps.lean (1,621 LoC, new): generic substitution-semantics infrastructure used by CallElim and reusable by future transforms. Includes H_asserts_zip / H_assumes_zip / H_check_block_zip walkers, singletonAssertEval / singletonAssumeEval and their _poly failure-flag variants, plus H_asserts_zip_fail (the L4 flag-flip walker that powers the polymorphic-f failure arm).
• Strata/Transform/CoreTransformProps.lean (1,126 LoC, new): reusable helpers for the Core small-step layer — singleCmdToStmts / _poly, H_havocs / _poly, H_init, H_inits, genIdent* correctness, fresh-name predicates, EvalCallElim_glue and EvalCallElim_glue_fail (composing the L1–L6 segments with the L4 success/failure flip).

Core semantics adjustments (~30 LoC)

• Strata/Languages/Core/StatementSemantics.lean: EvalCommandContract.call_sem unified — previously two separate path shapes (success: havoc + write-back; failure: σ' = σ and the precondition iff in the wrong direction); now a single rule parameterized by a Bool failure flag indicator, with the precondition iff narrowed to non-Free preconditions to match callElimCmd's actual emission rule. EvalCommand.call_sem propagates the callee body's terminal hasFailure flag to the caller (previously hardcoded to false, silently dropping any failures inside callee bodies).
• Strata/Languages/Core/StatementSemanticsProps.lean (+297 LoC): 8 new helpers around updatedStates / readValues / evalExpressions / initStates, plus the revived 5-theorem refinement-transit chain (EvalCommandRefinesContract, StepStmt[Star]_refines_contract, EvalStatement[s]RefinesContract) over the unified call_sem shape. EvalCallBodyRefinesContract is closed (was a long-standing sorry inside a comment block).
• Strata/Languages/Core/WF.lean: WFCallSiteProp.preBoolTyped and WFPrePostProp.boolTyped per-precondition Bool-totality clauses, used by the failure-arm to derive a failing-pre witness.
• Strata/Transform/ProcBodyVerifyCorrect.lean: takes CalleesNoFailure π φ as a new hypothesis (every procedure body, run from a non-failing init env, terminates with hasFailure = false), threaded through core_noFailure_preserved. The hypothesis is exactly the body-noFailure clause that clause 2 of the theorem's own conclusion (ProcedureCorrect) establishes per procedure, so callers discharge it inductively.

Shared-file helpers (~250 LoC)

• Strata/Languages/Core/StatementSemanticsProps.lean (above): 8 new shared helpers consumed by both CallElim and its sibling Core proofs.
• Strata/DL/Util/ListUtils.lean (+150 LoC net): adds notin_append4, unzip_snd_length, disjoint_of_nodup_append_three, zip_pair_split, nodup_3_decompose, notin_3_append_of, zip_zip_unzip_{snd,fst_unzip_fst}_of_lengths, zip_notin_{fst,snd}_pair; promotes existing helpers to public.
• Strata/DL/Imperative/CmdSemanticsProps.lean (new, +33 LoC): generalized pure-Imperative lemmas subst_defined_tail, subst_nodup_tail (P : PureExpr).
• @[expose] attributes added where required by the new module-system reductions:
  • Strata/DL/Imperative/CmdSemantics.lean: isNotDefined, substStores, substDefined, substNodup, invStores, substSwap, WellFormedSemanticEvalVal.
  • Strata/DL/Lambda/LExprWF.lean: substFvar, substFvars.
  • Strata/DL/Util/StringGen.lean: StringGenState.gen.
  • Strata/Languages/Core/CoreGen.lean: CoreGenState.WF, CoreGenState.gen.
  • Strata/Languages/Core/Procedure.lean: Procedure.Spec.getCheckExprs, Procedure.Spec.updateCheckExprs.
  • Strata/Languages/Core/StatementSemantics.lean: updatedState, updatedStates', updatedStates, WellFormedCoreEvalTwoState.
  • Strata/Transform/CoreTransform.lean: ~17 generator/transform defs.
  • Strata/Transform/CallElim.lean: callElimCmd, plus an extracted oldTyLookupCallElim helper required for the proof to share auxiliary match definitions across two do-blocks.

Notable commits

The branch is structured so each landed commit can be reviewed independently:

• 286c6ce36 — initial small-step rewrite (preserves the original _terminal-only theorem at f = false).
• 3710bb339 — add the exit-arm to callElimStatementCorrect (review feedback from @aqjune-aws): mirrors Specification.Overapproximates shape; non-call cases reuse the original Heval, the call case is vacuously discharged via seq_reaches_exiting.
• 0eb0342ee — review-feedback rename *Semantics → *SemanticsProps and relocate generic lemmas to ListUtils / CmdSemanticsProps / SubstSemanticsProps.
• 4bfccc31b — integrate hasFailure flag into EvalCommand.call_sem (closes a soundness gap inherited from the original semantics).
• e679bd560 — second review-feedback rename *SemanticsProps → *Props (the Semantics qualifier was misleading: these files hold transform machinery and substitution lemmas, not semantics defs).
• 44deb44b2 — close EvalCallBodyRefinesContract and revive the dormant Core refinement bridge.
• ba122da08 — unify EvalCommandContract.call_sem (failure-flag-parameterized) and revive the 5-theorem refinement-transit chain.
• 3daec283b — cleanup pass: 6 unused theorems in CoreTransformProps, 5-helper dead chain in SubstProps, dangling docstring references, TODO disposition. Net -327 LoC.
• be987fddc — lift _terminal to polymorphic {f : Bool} (PR CallElimCorrect: lift _terminal to polymorphic {f : Bool} #1340, merged into this branch).

Build status

• lake build: clean (490 jobs)
• 0 sorries introduced (baseline sorry inventory in ProgramWF / ProcedureWF / StatementWF / CmdEval is unchanged; this PR closes one previously commented-out sorry in EvalCallBodyRefinesContract)
• 0 axioms introduced
• #print axioms callElimStatementCorrect → [propext, Classical.choice, Quot.sound] (Lean stdlib only)

Test plan

• lake build clean across all 490 jobs
• #print axioms callElimStatementCorrect reports stdlib axioms only
• No new sorries / admits / axioms introduced
• Conjunctive shape of callElimStatementCorrect matches Specification.Overapproximates / TripleBlock
• _terminal arm polymorphic in {f : Bool} (success and failure traces both covered)
• Review-feedback follow-ups landed (exit arm, file renames, generic-lemma relocation)
• CI passes

Warning: This repository will shortly undergo a split into several separate repositories. If you're creating a PR that crosses the boundaries between these repositories, you may want to hold off until the split is complete or be prepared to rework your PR into multiple PRs once the split is complete.

The code that will be moved includes:

• Strata/DDM/*
• Strata/Languages/Boole/*
• Strata/Languages/Python/* along with Tools/Python/*
• Tools/BoogieToStrata

[aqjune-aws]

I left a few comments which can be applied orthogonally to our ongoing discussion in a private channel.
One extra question is that, I think the correctness of the top-level statement must also consider the case when a program may 'throw', through Imperative.exit. For example,

call f();
exit "some-block";

Note that the original program exits to "some-block", hence the final state after small-steps isn't ".terminal" (unlike what EvalStmtsSmall states, which is used transitively by EvalStatementsContract). If we apply call-elimination on this,

(omit temporary vars)
assume <pre>;
assert <post>;
exit "some-block";

it will have to exit to the right state.

[PROgram52bc]

Fixed in 3710bb3. The theorem now has a conjunctive shape, refactored into three theorems: _terminal (private, unchanged), _exit (private, new for the call case), and a public conjunction. No external callers needed updating.

[aqjune-aws]

Thanks for adding the exiting cases. It is good to see them proven :)

I have two high-level important comments which will more be related to what is to be proven.

1. The call_sem of EvalCommandContract

You would have already figured out the issue in call_sem. To talk about its proper fix, let me introduce the difference between the small-step semantics of assume and assert first:

• For assume, if the program state doesn't satisfy its condition, it is simply stuck; it doesn't proceed.
• For assert, even if the program state doesn't satisfy the condition, it proceeds; it only updates the hasFailure flag.
  You can confirm this from EvalCmd which has eval_assert_pass, eval_assert_fail and eval_assume. This is designed in this way so that even if a program includes multiple asserts and the first assert fails, we can still talk about the second assert individually (without using hasFailure, because hasFailure will already have been marked as true in this case).

Now coming to call_sem... When we are calling a procedure and the procedure has pre-post condition, from the caller's side I think a natural flow would be (1) we assert the precondition, (2) execute the body, and (3) assume the postcondition. It means that actually this part is too strong:

    (∀ pre, (Procedure.Spec.getCheckExprs p.spec.preconditions).contains pre →
      isDefinedOver (HasVarsPure.getVars) σAO pre ∧
      δ σAO pre = .some HasBool.tt) →

This has to be something like this:

    preconditionPassed <-> (∀ pre, (Procedure.Spec.getCheckExprs p.spec.preconditions).contains pre →
      isDefinedOver (HasVarsPure.getVars) σAO pre ∧
      δ σAO pre = .some HasBool.tt) →
...
    ----
    EvalCommandContract π δ σ (.call n callArgs md) σ' (\neg preconditionPassed)

2. Connection between EvalCommand and EvalCommandContract

I thought EvalCommand should be the ground-truth operational semantics for procedure call in a closed program, because when we do a procedure call, its interpreter will actually get into the body of the procedure call and concretely execute stuffs. How are EvalCommand and EvalCommandContracts related? Is there a theorem stating equivalence or refinement relation betweeen these two?

[PROgram52bc]

The call_sem of EvalCommandContract

Thanks for pointing it out. That makes sense. I will weaken the precondition requirement in call_sem, and adapt the proof accordingly.

Connection between EvalCommand and EvalCommandContract

Here is a potential theorem we could prove to connect the two. It is currently commented out because the contract version doesn't create the extra variables in the store, which makes the proof a little more complicated than it needs to be. But thanks for the question -- I will try to look into that next.

[aqjune-aws]

Hi David, thanks for working on this topic - I think that including the refinement proof might be a too big work & interfere with the unstructured CFG. I will be glad to work on the task.
In parallel, I am trying to port a few updates that fixes problems in small-step semantics and extending the definition of correctness of transformation.
Could you wait for a while until the updates from my end are delivered please? :)

[PROgram52bc]

Hi June, Yes. I am still working on adapting the call elimination proof to work with a generic failure flag (the case where preconditions fail). So I can definitely wait for your updates while iterating on that. I think it would be good to reuse some of the definitions in your updates in the current call-elimination proof.

As for the refinement proof, I do think it is quite complicated with the failure flag integrated -- if we constrain it to failed = false, I believe the proof should be straightforward, but that's just a conjecture.