Fix the small-step semantics of Imperative to consider block scopes for var initialization#1141
Fix the small-step semantics of Imperative to consider block scopes for var initialization#1141aqjune-aws wants to merge 7 commits into
Conversation
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
🤖 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
PostWFdefinition 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*_preservedtheorems — all six follow the exact same proof pattern ascore_step_preserves_wfBool. Stmt.labels/Block.labelsappear to be dead code (not referenced anywhere outside their definition).
| | step _ _ _ hstep _ ih => | ||
| exact ih (core_step_preserves_wfBool π φ h_wf_ext _ _ hwf₀ hstep) | ||
|
|
||
| theorem core_step_preserves_wfVar |
There was a problem hiding this comment.
🤖 core_step_preserves_wfVar, core_wfVar_preserved, core_step_preserves_wfCong, core_wfCong_preserved, core_step_preserves_wfExprCongr, core_wfExprCongr_preserved are all structurally identical to core_step_preserves_wfBool / core_wfBool_preserved — only the property type and the WFEvalExtension field differ. Consider extracting a generic helper parameterized by the property and the field accessor to avoid this 6× duplication.
There was a problem hiding this comment.
Yes, indeed they have very similar but slightly different proofs.... I have tried this but resolving the duplication was non-trivial.
| /-! ### Labels -/ | ||
|
|
||
| mutual | ||
| @[expose] def Stmt.labels (s : Stmt P C) : List String := |
There was a problem hiding this comment.
🤖 Stmt.labels and Block.labels are defined here but not referenced anywhere else in the codebase. Is this dead code left over from development, or is it intended for future use? If the latter, a brief docstring explaining the intended purpose would help.
There was a problem hiding this comment.
Removed, thanks :)
| omit [HasVal P] in | ||
| /-- Lift a `TripleBlock` to a `Triple` by wrapping in a block. -/ | ||
| /-- A postcondition is well-formed if it is stable under `projectStore`. -/ | ||
| def PostWF (Post : Env P → Prop) : Prop := |
There was a problem hiding this comment.
🤖 PostWF quantifies over all σ_parent, meaning the postcondition must hold even when projected through a store that defines no variables (making everything none). In practice, TripleBlock.toTriple only applies projection with the actual parent store at block entry. Would it be more precise (and easier for callers to discharge) to parameterize PostWF by the specific σ_parent that will be used? Or at minimum, document that this means the postcondition must only reference variables that are guaranteed to be defined in the parent scope.
There was a problem hiding this comment.
This had to be forall σ_parent because in general we don't know which variables are defined in this scope unless we know the information of the exact context. A Hoare triple is only aware of the code block inside the pre-postconditions, but can't know the code outside of it:
c1
{pre}
c2 <-- A Hoare triple must only be aware of this c2; we can't give information about c1 or c2 (which will have .init) to post.
{post}
c3
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
🔍 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.
2 participants
Issue #, if available:
Closes #372
Description of changes:
(nondeterministic).
On top of this, this also renames
touchedVarstomodifiedOrDefinedVarsfor clarity, and instead makestouchedVarsall vars that are read + modified + defined.How to review?
.blockconstructor 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 likestep_block_donewill do the projection, to define variables which were defined inside the inner scope.touchedVarsupdate 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.