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".
![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.
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_553dc81f-f702-4c96-aed0-74b6efe99de8) |
| \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``` |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e6be9dc25f
ℹ️ 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".
…0' into feat/packed-storage-lowering-2060
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_29376038-8efa-4f5a-8242-c6c468dfdab3) |
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_44d55849-e4cf-4d1e-8ef3-5c5c0c06f9d5) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: c406cf4082
ℹ️ 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".
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), 504 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: 30 supported / 30 total; Lean 26, trust docs 0, workflow/scripts 1, contracts 3, docs 0
- Changed lines: 504 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: Verity/Macro/Translate.lean (+52/-30), Contracts/Smoke/Storage.lean (+70/-0), Compiler/CompilationModel/StorageWrites.lean (+42/-18), artifacts/macro_property_tests/PropertyPackedStorageLoweringSmoke.t.sol (+53/-0), Verity/Macro/Translate/Parsing.lean (+33/-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.
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_de51f7e6-dd49-48d4-819d-ca1bb0838455) |
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: 33 Lean file(s), 1146 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: 38 supported / 38 total; Lean 33, trust docs 0, workflow/scripts 1, contracts 4, docs 0
- Changed lines: 1146 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 1s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/Storage.lean (+135/-105), Contracts/TypedIRTests.lean (+69/-69), Contracts/Smoke/Storage.lean (+118/-0), Verity/Macro/Translate.lean (+71/-30), Compiler/CompilationModel/StorageWrites.lean (+42/-18)
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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8b4f615734
ℹ️ 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".
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_700eae79-88e6-4ad6-af77-88838c4dafd5) |
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_7b78099b-dca0-4121-bedf-039e317b07a8) |
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: 32 Lean file(s), 1395 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: 41 supported / 41 total; Lean 32, trust docs 0, workflow/scripts 3, contracts 6, docs 0
- Changed lines: 1395 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: Compiler/Proofs/IRGeneration/GenericInduction/Storage.lean (+135/-105), Contracts/Smoke/Storage.lean (+199/-0), Verity/Macro/Translate.lean (+115/-30), Contracts/TypedIRTests.lean (+69/-69), Compiler/CompilationModel/LayoutValidation.lean (+57/-13)
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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 550647e94f
ℹ️ 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".
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_71c83afc-f5eb-45e6-802e-fe875e6e3657) |
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: 33 Lean file(s), 1508 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: 43 supported / 43 total; Lean 33, trust docs 0, workflow/scripts 3, contracts 7, docs 0
- Changed lines: 1508 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: Compiler/Proofs/IRGeneration/GenericInduction/Storage.lean (+135/-105), Contracts/Smoke/Storage.lean (+217/-0), Verity/Macro/Translate.lean (+111/-30), Contracts/TypedIRTests.lean (+69/-69), artifacts/macro_property_tests/PropertyPackedStorageLoweringSmoke.t.sol (+76/-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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e67e76af75
ℹ️ 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".
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_e7c02580-6404-475d-bd63-5a5a3b41a05a) |
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: 34 Lean file(s), 1566 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: 45 supported / 45 total; Lean 34, trust docs 0, workflow/scripts 4, contracts 7, docs 0
- Changed lines: 1566 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: Compiler/Proofs/IRGeneration/GenericInduction/Storage.lean (+135/-105), Contracts/Smoke/Storage.lean (+217/-0), Verity/Macro/Translate.lean (+111/-30), Contracts/TypedIRTests.lean (+69/-69), artifacts/macro_property_tests/PropertyPackedStorageLoweringSmoke.t.sol (+76/-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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a54d2c5def
ℹ️ 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".
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_f9dcfaf1-2670-4212-b34e-ab3ab1fc4e89) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e2a33da5c1
ℹ️ 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".
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: 34 Lean file(s), 1646 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: 45 supported / 45 total; Lean 34, trust docs 0, workflow/scripts 4, contracts 7, docs 0
- Changed lines: 1646 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: Compiler/Proofs/IRGeneration/GenericInduction/Storage.lean (+135/-105), Contracts/Smoke/Storage.lean (+229/-0), Verity/Macro/Translate.lean (+111/-30), Contracts/TypedIRTests.lean (+69/-69), artifacts/macro_property_tests/PropertyPackedStorageLoweringSmoke.t.sol (+76/-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.
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_59784bab-a600-4c4d-b1f7-d7c55301569f) |
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: 34 Lean file(s), 1707 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: 46 supported / 46 total; Lean 34, trust docs 0, workflow/scripts 5, contracts 7, docs 0
- Changed lines: 1707 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: Compiler/Proofs/IRGeneration/GenericInduction/Storage.lean (+135/-105), Contracts/Smoke/Storage.lean (+229/-0), Verity/Macro/Translate.lean (+111/-30), Contracts/TypedIRTests.lean (+69/-69), Compiler/CompileDriverTest.lean (+93/-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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 888f61733c
ℹ️ 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".
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_9abfcf62-1840-4771-8941-1cadb9468588) |
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: 35 Lean file(s), 1882 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: 47 supported / 48 total; Lean 35, trust docs 0, workflow/scripts 5, contracts 7, docs 0
- Changed lines: 1882 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 1s
- Largest changed files: Contracts/Smoke/Storage.lean (+251/-0), Compiler/Proofs/IRGeneration/GenericInduction/Storage.lean (+139/-107), Verity/Macro/Translate.lean (+111/-30), Contracts/TypedIRTests.lean (+69/-69), Compiler/Proofs/IRGeneration/SourceSemantics.lean (+81/-13)
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.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1df21adf73
ℹ️ 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 .uint16 => `(Compiler.CompilationModel.FieldType.uint256) | ||
| | .scalar (.uintN _) => `(Compiler.CompilationModel.FieldType.uint256) |
There was a problem hiding this comment.
When a newly supported narrow field is compiled through compileFunctionNamed, this erasure leaves it as .uint256 plus packedBits, but Compiler/TypedIRCompiler.lean::compileStorageRead and the .setStorage branch ignore packedBits and emit full-word getStorage/setStorage operations. A typed-IR execution of PackedStorageLoweringSmoke.setEpoch, for example, overwrites neighboring packed fields even though the normal Yul lowering performs masked read-modify-write; either lower packed ranges in typed IR or reject these fields there.
Useful? React with 👍 / 👎.
| | some { ty := .scalar (.fixedArray (.uintN 128) size), .. } => | ||
| pure (#[← `(doElem| let $name:ident ← | ||
| _root_.Verity.getFixedStorageArrayElement $field:ident $(natTerm size) $index:term)], locals) |
There was a problem hiding this comment.
When a fixed-array element is bound and then used in a packed write, such as let value ← getStorageArrayElement items 0; setStorage packedValue value, this rewrite returns the original locals array. Fresh evidence beyond the prior packed-getter fix is that the fixed-array getter branch still omits its Uint128 binding, so the later packed-write rewrite calls inferPureExprType on an unknown identifier and rejects an otherwise valid contract instead of applying UIntN.toUint256; push a .uintN 128 typed local here.
Useful? React with 👍 / 👎.
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
High Risk
Touches core storage layout, Yul generation, and formal IR/source agreement proofs; incorrect packing or slot accounting could corrupt contract state or break upgrade compatibility guarantees.
Overview
Adds Solidity-style packed scalar storage and
uint128[N]fixed arrays end-to-end: DSL declarations, Yul lowering, layout/ABI artifacts, source semantics, and proof bridges.Packed fields —
writeUintFieldSlots/ source semantics now perform read-modify-write viapackedWordWritefor fields withpackedBits, including transient storage. Storage layout JSON emitsoffset/widthper field. Layout and upgrade-compatibility reports treat disjoint packed ranges in the same word as non-overlapping (distinctPackedRanges) and flag intersecting ranges aswriteSetsOverlap. Slot conflict detection separates persistent vs transient storage spaces so the same slot index can hold both.Fixed
uint128arrays — NewFieldType.fixedArrayUint128stores two elements per word; compilation emitsstorage_array_index_access_uint128and packed set lowering on canonical/alias slots. Validation rejects zero length, packedBits on fixed arrays, and transient fixed arrays. Layout reports expand multi-word footprints for arrays and aliases.Surface area — ABI/storage JSON and typed IR recognize the new type;
Expr.storageArrayElement/setStorageArrayElementsupport fixed arrays; contract smoke tests cover packing, spill, mixed transient/persistent, and reserved-slot conflicts. Typed IR tests switch fromCompiler.SpecstoContracts.*.spec.Reviewed by Cursor Bugbot for commit 1df21ad. Bugbot is set up for automated code reviews on this repo. Configure here.