Transient storage fields (#1995)

[Th0rgal]

Summary

• Adds transient name : Type := slot n storage syntax with Field.isTransient macro metadata plumbing
• Scalar transient reads/writes lower to tload/tstore; source semantics and denotation go through the transient state map
• Verified supported-fragment surface for scalar transient stores (property closure + IR source/denote agreement helpers); generic induction storage surface is transient-aware
• Smoke contract + PropertyTransientStorageSmoke.t.sol

Part 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 successfully
• scripts/refresh_verification_artifacts.sh — [refresh] PASS
• make 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 to tload/tstore instead of sload/sstore across scalar storage, mapping reads/writes, packed slots, and struct members. Mapping write helpers gain an allowTransient flag; setMapping, setMappingWord, setMappingPackedWord, setMappingUint, and struct-member setters pass true so transient mappings use the correct builtins.

Source semantics and proofs route transient scalar writes through writeUintFieldSlots / writeAddressFieldSlots (transient vs persistent split via writeTransientTargets). Frames.lean adds preservation lemmas for those helpers and updates setStorage / setStorageAddr execution summaries. DenoteAgreement.lean adds field-aware mapping write bridges and extends the denote_stmt_arm tactic. Stmt.lean normalizes tstore offsets with evmModulus so IR execution matches source semantics.

Persistent-only paths (e.g. setMapping2, setMappingChain) still pick tstore when the field is transient at compile time; the PR description notes verified surface focuses on scalar transient storage and mapping writes enabled via allowTransient on the generic mapping setters.

^{Reviewed by Cursor Bugbot for commit 04ecafc. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jun 19, 2026 8:16am

[cursor]

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.}

[github-actions]

\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```

[Th0rgal]

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 execStmt mapping-write handler routes through the transient-aware *FieldSlots wrappers (writeAddressFieldSlots / writeTransientTargets, gated by fieldIsTransient), which is symmetric with the transient-aware readFieldWord on the read side. A transient field is written to and read from the transient component on both sides; a persistent field uses the persistent component on both sides. There is no read/write routing mismatch.

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 4c0338cf — the transient branch now applies the same wordToAddress masking as the persistent branch.