The small-step semantics of Imperative must have scoped var init, remove unlabeled exit from Core

[aqjune-aws]

Issue #, if available:

Closes #372

Description of changes:

Formalizing scoped variable initialization:

• Adds scoped environment semantics to blocks: step_block_done now projects the store through the parent store via projectStore, discarding block-local variables on exit. This applies to both StepStmt (deterministic) and StepKleene
  (nondeterministic).
• Adds PostWF helper definition in Specification.lean for postcondition stability under projectStore.
• Adds .block constructor to KleeneStmt and corresponding step_block/step_block_body/step_block_done to StepKleene, mirroring the deterministic block semantics.
• Changes StmtToKleeneStmt (.block _ bss _) to produce .block b (wrapping in a Kleene block), so the Kleene translation preserves scoping.

Removing unlabeled exit command (exit;, not exit lbl;):

• The unlabeled exit command doesn't have clear meaning when it is inside while. In while cond { ... exit; ... }, is exit equivalent to continue or break in C/Python? No translation to Core was introducing the unlabeled exit, and the small-step semantics wasn't clear about the meaning of exit inside a loop.
• The type checker of Core (Strata/Languages/Core/StatementType.lean) fails when an unlabeled exit appears inside the body of a while loop / if statement (unless it is wrapped by another nested block), but the DDM syntax of core allows it, so from user's perspective this gap is kind of surprising.
• This patch removes the unlabeled exit case because it can always be simulated by a labeled block + labeled exit.

On top of this, this also renames touchedVars to modifiedOrDefinedVars for clarity, and instead makes touchedVars all vars that are read + modified + defined.

How to review?

• Strata/DL/Imperative/StmtSemantics.lean has the most important update: the .block constructor now has the input store which will be used to 'project' the output store to the variables that have been defined before. Also, any block-exiting small steps like step_block_done will do the projection, to define variables which were defined inside the inner scope.
• Correspondingly, the Kleene language was updated to add a notion of block and scoping to its syntax and semantics, otherwise DetToKleene doesn't prove. (Strata/DL/Imperative/KleeneStmt.lean, Strata/DL/Imperative/KleeneStmtSemantics.lean)
• StrataTest/DL/Imperative/StepStmtTest.lean has a few new tests that show scoping works well.
• DetToKleeneCorrect.lean and ProcBodyVerifyCorrect.lean shows that the top-level statements are not touched after this update.
• Strata/DL/Imperative/HasVars.lean has the touchedVars update and Strata/Languages/Core/StatementSemantics.lean has some additional well-formedness about evaluator extension that are useful.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[MikaelMayer]

🤖 Overall this is a well-structured PR that correctly implements block-scoped variable semantics via projectStore. The Kleene language extension mirrors the deterministic semantics cleanly, and the new tests provide good coverage of the scoping behavior.

A few items to consider:

• The PostWF definition quantifies over all σ_parent, which is stronger than needed (in practice only the actual parent store matters). This is conservative and safe, but worth documenting that it means postconditions must not reference block-local variables.
• There is significant code duplication in the new core_step_preserves_wf* / core_wf*_preserved theorems — all six follow the exact same proof pattern as core_step_preserves_wfBool.
• Stmt.labels / Block.labels appear to be dead code (not referenced anywhere outside their definition).

[MikaelMayer]

🔍 The new commit is a merge of main — no changes to the files I previously commented on. My three suggestions (deduplicating the wf-preservation proofs, clarifying whether Stmt.labels/Block.labels are dead code, and documenting PostWF's universal quantification over σ_parent) remain unaddressed. These were non-blocking suggestions so LGTM overall, but it would be good to get a response on the labels question in particular.

[MikaelMayer]

🔍 Verified the new commits since last review:

• .labels dead code: ✅ Fixed — removed in commit 917ea90.
• Deduplicating wf-preservation proofs: Not addressed (non-blocking, still a nice-to-have).
• PostWF documentation: Not addressed (non-blocking).

The one actionable item was properly fixed. The "Disallow unlabeled exit" commit is a clean refactor that simplifies the semantics. LGTM.

[MikaelMayer]

🔍 LGTM — the latest commit (3a875b08) is a minor omit annotation cleanup. My previous non-blocking suggestions (deduplicating wf-preservation proofs, documenting PostWF) remain open but are not blockers.

[MikaelMayer]

🔍 LGTM — the latest commit is a merge of main with no changes to PR files. Previous non-blocking suggestions (deduplicating wf-preservation proofs, documenting PostWF) remain open but are not blockers.

[MikaelMayer]

I think this is an excellent move to have scoped semantics. It will likely make proofs simpler

[MikaelMayer]

🔍 LGTM — the latest commit removes @[simp] from variable-tracking definitions, keeping only @[expose]. Clean change. Previous non-blocking suggestions (deduplicating wf-preservation proofs, documenting PostWF) remain open but are not blockers.

[joscoh]

Also, could you update the docs please? Right now it says "An exit statement transfers control out of the nearest enclosing block with a matching label, or, if no label is provided, the nearest enclosing block.".

[aqjune-aws]

Fixed, thanks. Setifying the result of touchedVars and relevant helper functions make sense to me (their item order in the list shouldn't matter).

[MikaelMayer]

🔍 LGTM — the "address comments" commit properly addresses feedback: @[expose] removed from variable-tracking and sizeOf defs, anonymous suffices hypotheses named (h_gen), @call_sem simplified to named-argument style, outdated test comment removed, and docs updated to reflect unlabeled exit removal. Previous non-blocking suggestions (deduplicating wf-preservation proofs, documenting PostWF) remain open but are not blockers.

[PROgram52bc]

I think a similar Option construct for the GOTO exits could be simplified as well. This is non-blocking, but perhaps they can be addressed in future PRs.

[PROgram52bc]

Mutual block unnecessary?