Problem
#1728 tracks nonreentrant as part of compile-time safety, but the remaining useful work is a concrete guard semantics rather than another umbrella item.
Scope
- Define the storage/state model for a generated non-reentrancy guard.
- Lower
nonreentrant functions to guard enter/exit code with revert-safe cleanup behavior.
- Ensure interactions with
return, revert, Leave, and internal calls are explicit.
- Add source/executable semantics and generated-Yul tests.
- Decide whether the first version is outside
SupportedSpec or prove the required guard preservation lemmas.
Problem
#1728 tracks
nonreentrantas part of compile-time safety, but the remaining useful work is a concrete guard semantics rather than another umbrella item.Scope
nonreentrantfunctions to guard enter/exit code with revert-safe cleanup behavior.return,revert,Leave, and internal calls are explicit.SupportedSpecor prove the required guard preservation lemmas.