feat: Solidity-compatible packed storage lowering - #2249
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_630bcaad-5b54-41e7-9981-5f90bbf0d715) |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3d7a295453
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| | .scalar .bytes => throwError "storage field cannot be Bytes; use Uint256 encoding" | ||
| | .scalar (.array _) => throwError "storage field cannot be Array; use mapping encodings" | ||
| | .scalar (.fixedArray _ _) => throwError "storage field cannot be FixedArray; use mapping encodings" | ||
| | .scalar (.fixedArray (.uintN 128) _) => `(List Uint128) |
There was a problem hiding this comment.
Mapping FixedArray Uint128 N to List Uint128 routes its executable contract body through the dynamic-array helpers in Verity/Core.lean, which use the current list length and default to an empty list. Consequently, a valid access such as index 0 of a newly deployed nonempty fixed array reverts in the Lean/source model, while the generated Yul bounds-checks against N and returns the zero-initialized packed element. This can make proofs and executable specifications disagree with the deployed contract unless every test manually seeds an N-element list.
Useful? React with 👍 / 👎.
| let sameAnchor := anchor? == some field.slotNum | ||
| let nextOffset := if sameAnchor then offset else 0 |
There was a problem hiding this comment.
When adjacent narrow persistent and transient fields use the same numeric slot, sameAnchor treats them as sharing one packing sequence because it compares only slotNum. Since sload/sstore and tload/tstore are separate storage spaces, each field should start at offset 0 in its own layout; currently the second declaration is shifted after the first, producing an incorrect external layout without triggering a slot conflict.
Useful? React with 👍 / 👎.
| let packedSlot := YulExpr.call "add" [YulExpr.lit slot, | ||
| YulExpr.call "div" [YulExpr.ident "__array_index", YulExpr.lit 2]] |
There was a problem hiding this comment.
For a fixedArrayUint128 field with compatibility aliasSlots, this address calculation and the subsequent store use only the canonical slot. The Field.aliasSlots contract says writes are mirrored, and layout validation now reserves the full fixed-array footprint at every alias, but setStorageArrayElement leaves all alias copies stale. Iterate the packed read-modify-write over the canonical base and each alias base, as scalar and mapping compatibility writes already do.
Useful? React with 👍 / 👎.
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 26 Lean file(s), 371 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 29 supported / 29 total; Lean 26, trust docs 0, workflow/scripts 1, contracts 2, docs 0
- Changed lines: 371 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Contracts/Smoke/Storage.lean (+55/-0), Compiler/CompilationModel/StorageWrites.lean (+36/-18), artifacts/macro_property_tests/PropertyPackedStorageLoweringSmoke.t.sol (+53/-0), Verity/Macro/Translate/Parsing.lean (+32/-0), Compiler/Proofs/Storage/StructArrayStorage.lean (+24/-0)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
1 participant
Summary
Validation
make checks(641 tests): passmake test-evmyullean-fork: passlake build Contracts.Smoke.Storage: passlake build Compiler.Proofs.IRGeneration.GenericInduction.Storage: passlake build Compiler.Proofs.IRGeneration.Contract: passlake build PrintAxioms Compiler Contracts: all Lean modules compile, but the aggregate exits on the existing LakeContracts: some modules have bad importsjob-computation issue from the current library glob surfaceNo
sorry,admit, sourceaxiom, or newunsafedeclarations.Closes #2060
Note
Medium Risk
Changes contract storage layout and emitted sload/sstore bit-packing for new field types; mistakes could corrupt packed words or break upgrade compatibility, though validation, layout reports, and proofs are extended accordingly.
Overview
Adds Solidity-style packed storage to the contract DSL: narrow scalars (
Uint16,Uint32,Uint128, etc.) andFixedArray Uint128 Nare accepted in storage declarations instead of being rejected or forced to full-word encodings.applyAutomaticPackedLayoutruns after parsing and assigns LSB-first bit offsets for consecutive narrow fields that share the same explicit slot anchor, including spill to the next word when a slot fills (smoke-tested inPackedStorageSpillSmoke).The compiler gains
FieldType.fixedArrayUint128, maps it touint128[N]in ABI/storage JSON, and lowers indexed reads/writes for fixeduint128arrays as two elements per storage word (read-modify-write on write). A new Yul helperstorage_array_index_access_uint128is emitted when storage array element access is used, alongside the existing dynamic-array helper.Layout validation and compatibility reports treat fixed arrays as occupying
(size+1)/2packed words. Proof bridges, reserved helper prefixes, smoke contracts, Foundry property stubs, andPrintAxiomsentries are updated to cover the new paths.Reviewed by Cursor Bugbot for commit 3d7a295. Bugbot is set up for automated code reviews on this repo. Configure here.