Phase 1D #1: canonical storage/state and mapping slots (SolidityStorage + four lemmas) - #2226
Conversation
…ge + four lemmas)
|
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_ff05e608-9133-4e56-b6cb-09ea7ecc714f) |
![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: 39a7c4d861
ℹ️ 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".
OpenCodeReview first-pass review🔁 Incomplete — this run did not finish and will retry on the same commit. Do not count it as review coverage. OCR produced no JSON output OCR stderr highlightsOCR pilot metrics & packet coverageOCR pilot metrics
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_5c672c31-2ba1-439b-b7c2-6cfc26f10739) |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 749f4b6163
ℹ️ 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".
| /-- The helper for a Yul packed read is the interpretation of the real compiler | ||
| path in `ExpressionCompile.lean`. -/ | ||
| theorem yulReadPackedWord_eq_compiledExpr (word : Word) (offset width : Nat) | ||
| (hwidth : width < 256) : |
There was a problem hiding this comment.
For a field with packedBits := { offset := 0, width := 256 }, which the validation contract explicitly permits (0 < width <= 256 in Compiler/CompilationModel/Dispatch.lean:517), the hwidth : width < 256 premise is impossible to satisfy, so this new compiler-output bridge cannot cover a valid full-word packed layout. This restriction was introduced by the fresh compiler bridge added after the earlier review; handle the compiler's width >= 256 mask branch or weaken the premise to include 256.
Useful? React with 👍 / 👎.
| storage id (mappingSlotPointer baseSlot key) = | ||
| storage id (KeccakEngine.keccak256 (abiEncodeMappingSlot baseSlot key)) := by |
There was a problem hiding this comment.
When this is used as the mapping-storage bridge, it only unfolds mappingSlotPointer and never references either the source read through abstractMappingSlot in Compiler/Proofs/IRGeneration/SourceSemantics.lean:1388 or the emitted mappingSlot helper in Compiler/CodegenCommon.lean:70-73. For example, reversing the helper's two mstore operations would produce the wrong EVM slot while this theorem would still prove by rfl; establish the equality against the generated helper or its executable semantics instead.
Useful? React with 👍 / 👎.
OpenCodeReview first-pass review🔁 Incomplete — this run did not finish and will retry on the same commit. Do not count it as review coverage. OCR produced no JSON output OCR stderr highlightsOCR pilot metrics & packet coverageOCR pilot metrics
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_3f824c55-1260-4793-8f1e-f87c2c6a8920) |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2eb6a1f2bf
ℹ️ 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".
OpenCodeReview first-pass review🔁 Incomplete — this run did not finish and will retry on the same commit. Do not count it as review coverage. OCR produced no JSON output OCR stderr highlightsOCR pilot metrics & packet coverageOCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
|
@codex review |
1 similar comment
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a18bb91b12
ℹ️ 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".
| def sourceReadPackedWord (word : Word) (offset width : Nat) : Word := | ||
| IRStorageWord.ofNat ((word.toNat / 2 ^ offset) % 2 ^ width) |
There was a problem hiding this comment.
The fresh compiler-expression bridge addresses only the Yul half of the earlier finding: sourceReadPackedWord still independently duplicates yulReadPackedWord, making sourceRead_of_packedWord provable by rfl without referencing the executable packed read in Compiler/Proofs/IRGeneration/SourceSemantics.lean:1411-1414. If that evaluator changes its shift, mask, or operand order, this source/Yul equivalence and the new compiler bridge will all continue to pass, so add a lemma relating this helper to the actual source evaluator.
Useful? React with 👍 / 👎.
| def applyYulSstores : StorageDiff → SolidityStorage → SolidityStorage := | ||
| applyStateRewrite |
There was a problem hiding this comment.
When a generated storage write has the wrong slot, value, ordering, or even uses tstore instead of sstore, this function cannot expose the regression because it accepts the already-normalized source StorageDiff rather than emitted Yul and simply aliases applyStateRewrite. In contrast, the real lowering constructs the calls in Compiler/CompilationModel/StorageWrites.lean:90-124; structurally interpret those statements or connect their executable semantics to this transformer before treating it as the Yul side of the state bridge.
Useful? React with 👍 / 👎.
…servable Addresses the two review threads on the canonical storage/state bridge, both of which flagged that the "bridge" theorems could not observe a compiler regression because each side of the equation was restating the same model. Packed reads (was: `sourceRead_of_packedWord := rfl`) `sourceReadPackedWord` used to be a hand-written arithmetic copy of `yulReadPackedWord`, so the equivalence theorem held by `rfl` and would keep holding even if the compiler's mask, shift offset, or operand order changed. It is now *executed* rather than restated: `sourceReadPackedWord` runs `SourceSemantics.evalExpr` on a synthetic `mappingStruct` field whose member is packed at `(offset, width)`, which drives the real packed-read branch of the source evaluator. `isSourcePackedRead` is the structural predicate selecting that branch, and `compiledPackedRead_eq_sourceEvalPackedRead` connects the evaluator's output to the compiled expression via `yulReadPackedWord_eq_compiledExpr`. Any change to the operand order, the mask (`packedMaskNat`) or the shift offset on either the source or the compiled path now breaks this bridge. `sourceRead_of_packedWord` / `packedWord_of_sourceRead` consequently gain `(hoffset : offset < 256) (hwidth : width <= 256)`. These are the EVM well-formedness side conditions the executable evaluator actually depends on; the statements are strictly stronger than the previous vacuous `rfl`. Sstore aliasing (was: `applyYulSstores := applyStateRewrite`) `applyYulSstores` was defined to *be* `applyStateRewrite`, so the aliasing theorem was again true by definition. It now runs `compiledYulSstores`, which pattern-matches the emitted `sstore(slot, value)` calls produced by the real `compileSetStorage`, checking both the slot literal and the value literal against the corresponding `StorageWrite` before applying it. `compiledSstoreStmts_eq` pins the exact shape of the emitted statement, and `applyYulSstores_eq_applyStateRewrite` proves the equivalence by induction on the diff. A change to the emitted opcode, argument order, or literal encoding now falls through to the catch-all branch and breaks the proof. No `sorry`, no `admit`, no new axioms. `PrintAxioms.lean` regenerated via `scripts/generate_print_axioms.py` (6042 -> 6051 theorems, 0 sorry'd).
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_e5d32b2a-4b44-42ff-a327-ea8828479e31) |
|
@codex review Pushed Packed reads — Note the signature change: Sstore aliasing — Local receipts
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4287e4ee2c
ℹ️ 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".
| def packedReadBridgeSourceExpr : Compiler.CompilationModel.Expr := | ||
| .structMember "__packed_read_bridge_struct" (.literal 0) "value" |
There was a problem hiding this comment.
The compiler half evaluates Expr.storage for a packed scalar field, but the source half here evaluates an unrelated Expr.structMember on a mapping struct. These dispatch to different SourceSemantics.evalExpr cases: notably, the .storage case at Compiler/Proofs/IRGeneration/SourceSemantics.lean:1158-1160 returns the entire word without consulting packedBits. For example, a raw word of 0x100 with offset 0 and width 8 evaluates to 256 through the source .storage case but compiles to 0, while this theorem still succeeds by exercising the struct-member extraction instead. Compile and evaluate the same expression shape so the bridge exposes this mismatch.
Useful? React with 👍 / 👎.
| | .exprStmt (.call "sstore" [.lit slot, .lit value]) :: stmts, write :: writes, storage => | ||
| if slot == writeSlotLit write && | ||
| value == write.value.toNat % Compiler.CompilationModel.uint256Modulus then | ||
| compiledYulSstores stmts writes (applyStorageWrite write storage) |
There was a problem hiding this comment.
When diff contains writes for multiple contract IDs, the emitted statements are ordinary sstore calls with no contract operand, yet this interpreter reintroduces write.contract by applying the original source write. For two writes to the same slot under different contract IDs, the Yul program overwrites one slot in the currently executing contract, whereas applyStateRewrite updates two separate contract-indexed stores, so the universal equivalence theorem succeeds without modeling the actual Yul behavior. Constrain the diff to one explicit current contract or interpret separate per-contract executions.
Useful? React with 👍 / 👎.
OpenCodeReview first-pass review🔁 Incomplete — this run did not finish and will retry on the same commit. Do not count it as review coverage. OCR produced no JSON output OCR stderr highlightsOCR pilot metrics & packet coverageOCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
|
@codex review |
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_2a2f1c6e-ef82-44c1-b15d-9f4dc2dae794) |
|
Codex Review: Didn't find any major issues. Chef's kiss. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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 + 0/3 paquet(s) reviewés sémantiquement. 5 finding(s) (1 high / 4 low); les hunks hors paquets restent à couvrir par un humain ou Codex.
Paquets non couverts par la review sémantique
- Compiler/Proofs/Storage/SolidityStorage.lean — timeout (spawnSync ocr ETIMEDOUT)
- PrintAxioms.lean — timeout (spawnSync ocr ETIMEDOUT)
- Compiler/Proofs/IRGeneration/SourceSemantics.lean — timeout (spawnSync ocr ETIMEDOUT)
Large Lean diff routed to bounded packet review: 5 Lean file(s), 568 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 5/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 5 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 5 supported / 5 total; Lean 5, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 568 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 5; files 3; tokens 0; tool calls 0; warnings 1; duration 2434s
- Largest changed files: Compiler/Proofs/Storage/SolidityStorage.lean (+500/-0), Compiler/Proofs/IRGeneration/SourceSemantics.lean (+24/-3), PrintAxioms.lean (+21/-1), Compiler/Proofs/IRGeneration/GenericInduction/Storage.lean (+2/-8), Verity/Core/Model/Denote.lean (+8/-1)
Packet coverage
- Packet review: enabled; selected 5/8 packet(s)
- Scout: configured; status success; 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: Triaged top 5 scout-ranked packet(s); remaining changed hunks/files require Codex or human proof review, and selected packets still need strong reviewer analysis.
- 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.
- Covered packets:
- Compiler/Proofs/Storage/SolidityStorage.lean:1 score 104 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: What is the external trusted source (Solidity spec / yellow paper /
solcgolden / cryptographic reference) that this 500-line file is checked against, and where is the checksum or equivalence proof that pins it? If none exists, then every downstream theorem proved aboutevalExpr_storage(pkt-3/4/5) is reasoning about an internally-consistent but externally-unverified model — i.e. the 'manifest' (the proof itself) covers a subset (self-consistency) of the full artifact set (real Solidity stor - PrintAxioms.lean:85 score 42 [lenses: provenance, verification-independence, proof-soundness] — changed imports; ask: Does
import Compiler.Proofs.Storage.SolidityStorageactually cause PrintAxioms to recursively walk and report every axiom/sorry in SolidityStorage.lean and its transitive imports (Compiler.Proofs.MappingSlot, Compiler.CompilationModel.StorageWrites, Verity.Core.Model.Types, IRStorageWord, etc.)? Is there any sibling artifact introduced by this PR that is depended on by the proofs but deliberately excluded from this manifest? Who audits that the set of imported files == the set of files whose a - Compiler/Proofs/IRGeneration/SourceSemantics.lean:1160 score 30 [lenses: verification-independence, proof-soundness] — hotspot path/churn; ask: Are the .storage branches in evalExpr, evalExpr_storage (pkt-4), and evalExprWithHelpers (pkt-5) generated from a single source, or maintained as three hand-written copies? If hand-maintained, what guarantees they remain equivalent — is there any non-defeq proof (e.g. mutual equivalence lemma) bridging the helper and helper-free variants?
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:1553 score 30 [lenses: verification-independence, proof-soundness] — hotspot path/churn; ask: After the packedBits branch was added, does the evalExpr_storage proof remain
rfl(definitional mirror), or has it been replaced with a substantive argument that touches anything other than the local evalExpr definition? Specifically: is there a separate lemma/derivation establishing thatUint256.and (Uint256.shr rawWord offset) (Uint256.ofNat (2^width-1))equals the expected packed-bits value, or is that arithmetic itself just trusted because it lives inVerity.Core.Uint256? - Compiler/Proofs/IRGeneration/SourceSemantics.lean:3544 score 30 [lenses: provenance, verification-independence, proof-soundness] — hotspot path/churn; ask: Where does the
Fieldrecord (and specificallyfield.packedBits,field.slot) originate, and is there any content-hash, golden-file, or independent recomputation that ties eachFieldvalue to the trusted Solidity source it is supposed to represent? Without such a pin, the producer can inject aFieldwhosepackedBitsdoes not correspond to the source's declared layout andevalExprWithHelperswill silently agree — the proof passes, the manifest (PrintAxioms) is unchanged, and the artif
- Compiler/Proofs/Storage/SolidityStorage.lean:1 score 104 [lenses: provenance, verification-independence, proof-soundness] — public declaration/signature changed, changed imports; ask: What is the external trusted source (Solidity spec / yellow paper /
Pilot mode: advisory only. Codex Review remains the merge gate.
1 participant
Closes the foundational slice of #2081 by adding canonical contract-indexed Solidity storage, Keccak mapping-slot/preimage bridges, packed-word source/Yul read equivalence, and a shared source/Yul state-rewrite transformer.\n\nValidation:\n- lake build\n- lake build PrintAxioms\n- forbidden-token scan: clean
Note
Medium Risk
Changes formal storage read semantics for packed fields across source and denote models; risk is proof-correctness and downstream verification dependencies, not live runtime services.
Overview
Introduces
Compiler/Proofs/Storage/SolidityStorage.leanas the Phase 1D foundation: contract-indexed canonical storage, Keccak mapping-slot bridges (emittedmappingSlothelper ↔abstractMappingSlot↔evalExpr), packed-word equivalence (compilerand/shr/sload↔ executableSourceSemantics), andsstoresequences interpreted as the sameapplyStateRewriteas source writes. New lemmas are wired intoPrintAxioms.Source semantics for
Expr.storagenow masks packed fields (shr+andwithpackedMaskNat) inSourceSemantics.lean,Verity/Core/Model/Denote.lean, andevalExprWithHelpers, aligning evaluation with the existing Yul lowering inExpressionCompile.IR generation proofs in
GenericInduction/Storage.leansimplifyhEvalSrcsteps by rewriting viaSourceSemantics.evalExprinstead of manualmatch/changeonfindFieldWithResolvedSlot.Reviewed by Cursor Bugbot for commit 880acb1. Bugbot is set up for automated code reviews on this repo. Configure here.