Transient storage fields (#1995)#2021
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
# Conflicts: # PrintAxioms.lean # Verity/Macro/Translate.lean
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit 23529c9. Configure here.
| \n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
|
Bugbot HIGH "Transient mapping read/write mismatch" — assessed as a FALSE POSITIVE (no change to mapping read/write routing). The finding suggests transient mapping writes and reads are routed asymmetrically. They are not: every For the record, the MED finding in the same area ("transient address write skips the address mask that the persistent path applies") was a real bug and is fixed in |
Merge origin/main (26344a0) into grind/2021-proofs. UNION resolution: keep both main's features/tests and grind's transient-storage proof repair. Net delta vs main = 21 files (transient-storage feature + sound proofs). lake build + lake build PrintAxioms both green; only standard axioms on #2021's proofs (ofReduceBool present only on main's pre-existing native lowering witnesses, which #2021 does not touch).
Recover field-aware frame lemmas left unstaged in the prior merge commit:
- Frames.lean: writeUint/AddressFieldSlots_preserves_{storage,address,arrays,
calldata} + rewire execStmt_setStorage/setStorageAddr_execution_summary to
the field-aware (transient-capable) writers.
- DenoteAgreement.lean: writeAddressKeyedMapping2PackedWordFieldSlots_eq.
- ExpressionCompile.lean: use the outer resolved field binding for the
tload/sload selection (drop redundant re-match); adapt compileExpr_bridgedSource
closure proofs accordingly.
Regenerate PrintAxioms.lean (5316 thms, 0 sorry'd). Allowlist the long
add-wrapped multi-slot bridging closure compileMappingSlotWrite_multiSlot_nonzero_bridged
(twin of the already-allowlisted compileMappingSlotWrite_multiSlot_bridged).
make check: All checks passed.
1 participant
Summary
transient name : Type := slot nstorage syntax withField.isTransientmacro metadata plumbingtload/tstore; source semantics and denotation go through the transient state mapPropertyTransientStorageSmoke.t.solPart of #1995. Known gap: mapping syntax/metadata parses, but verified surface here covers scalar transient storage only — transient mapping writes remain on the persistent generic path.
Test plan
lake build Verity Contracts Compiler PrintAxioms— Build completed successfullyscripts/refresh_verification_artifacts.sh— [refresh] PASSmake check— All checks passed (607 tests)Note
Medium Risk
Changes core storage lowering and verified semantics for a new storage class; incorrect transient vs persistent routing would miscompile contracts, though the diff is localized and proof-backed.
Overview
Extends the compilation pipeline so fields marked transient (
Field.isTransient) lower totload/tstoreinstead ofsload/sstoreacross scalar storage, mapping reads/writes, packed slots, and struct members. Mapping write helpers gain anallowTransientflag;setMapping,setMappingWord,setMappingPackedWord,setMappingUint, and struct-member setters passtrueso transient mappings use the correct builtins.Source semantics and proofs route transient scalar writes through
writeUintFieldSlots/writeAddressFieldSlots(transient vs persistent split viawriteTransientTargets).Frames.leanadds preservation lemmas for those helpers and updatessetStorage/setStorageAddrexecution summaries.DenoteAgreement.leanadds field-aware mapping write bridges and extends thedenote_stmt_armtactic.Stmt.leannormalizeststoreoffsets withevmModulusso IR execution matches source semantics.Persistent-only paths (e.g.
setMapping2,setMappingChain) still picktstorewhen the field is transient at compile time; the PR description notes verified surface focuses on scalar transient storage and mapping writes enabled viaallowTransienton the generic mapping setters.Reviewed by Cursor Bugbot for commit 04ecafc. Bugbot is set up for automated code reviews on this repo. Configure here.