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: `build`\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) |
…owering-2060 # Conflicts: # PrintAxioms.lean
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_3ff49b8c-4dd5-4ec4-8197-afbe1563ca4c) |
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), 1242 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 32, trust docs 0, workflow/scripts 1, contracts 5, docs 0
- Changed lines: 1242 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 (+150/-0), Contracts/TypedIRTests.lean (+69/-69), Verity/Macro/Translate.lean (+76/-30), Compiler/CompilationModel/LayoutValidation.lean (+56/-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: adffaf73f5
ℹ️ 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_85e5ec8f-0cce-442a-8f03-b50e4928121c) |
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), 1308 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 32, trust docs 0, workflow/scripts 1, contracts 5, docs 0
- Changed lines: 1308 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 (+182/-0), Contracts/TypedIRTests.lean (+69/-69), Verity/Macro/Translate.lean (+96/-30), Compiler/CompilationModel/LayoutValidation.lean (+56/-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: 180f013e73
ℹ️ 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_82932573-31fe-4f3b-b651-ef0dfa6a7287) |
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), 1350 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: 1350 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 (+182/-0), Contracts/TypedIRTests.lean (+69/-69), Verity/Macro/Translate.lean (+96/-30), Compiler/CompilationModel/LayoutValidation.lean (+56/-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: 9925e8155b
ℹ️ 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_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".
| let baselineWriteSlots := baselineFields.foldl (fun acc field => | ||
| if field.isTransient == candidateField.isTransient then acc ++ field.writeSlots else acc) [] | ||
| let overlaps := overlappingSlots candidateField.writeSlots baselineWriteSlots |
There was a problem hiding this comment.
When a baseline ends with a partially occupied packed slot and the candidate adds a field in the unused bits—such as adding a second Uint128 beside an existing low-half Uint128—this comparison considers only the numeric write slots and reports newFieldOverlapsBaselineWriteSet. The existing field's packed write already preserves those unused bits, so this is a safe packed-layout extension; compare packedBits when the shared slot is occupied by packed fields rather than treating every same-slot addition as incompatible.
Useful? React with 👍 / 👎.
| | .scalar (.fixedArray (.uintN 128) size) => | ||
| `(Compiler.CompilationModel.FieldType.fixedArrayUint128 $(natTerm size)) |
There was a problem hiding this comment.
When the declaration is FixedArray Uint128 0, this new conversion accepts it because no positive-size check exists. Every generated element access then reverts, while layout validation and reports reserve one word via max 1 ((size + 1) / 2) and the storage JSON advertises the invalid Solidity type uint128[0]; reject size zero before constructing fixedArrayUint128.
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, code generation, and formal proof bridges; incorrect packing or slot accounting could corrupt contract state or break verified compilation equivalence.
Overview
Adds Solidity-style packed storage for narrow scalars (
Uint16/Uint32/Uint128) andFixedArray Uint128, with DSL slot/bit layout, read-modify-write Yul lowering, and astorage_array_index_access_uint128helper for indexed access.Layout and validation now treat
fixedArrayUint128as multi-word footprints, emit packedoffset/widthin storage layout JSON, and separate persistent vs transient slot conflicts (same numeric slot allowed across spaces). Transient fixed arrays are rejected at compile time.Semantics and proofs extend source/denote eval for fixed-array get/set, transient-aware field resolution, and compatibility reports; contract tests move from
Compiler.SpecstoContracts.Specs.Runtime API adds packed get/set helpers on
Verity.Coreplus fixed-array contract primitives alongside existing dynamic-array ops.Reviewed by Cursor Bugbot for commit a54d2c5. Bugbot is set up for automated code reviews on this repo. Configure here.