proof: bridge setStorageWord statement preservation#2168
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_7fe91418-9ee5-4f14-b0c6-69f3a761b463) |
![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
Status: scout_triage · Mode: large-lean-hotspots · 4 finding(s) · 3 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 3 Lean file(s), 628 changed supported line(s). Scout model ranked 4/5 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 4 inline comment(s).
Warnings
- coverage : Large Lean scout mode covers ranked hotspots only. Codex/human review must cover skipped hunks and proof obligations; OCR strong packet review is not wired yet.
OCR pilot metrics
- Routing: large-lean-hotspots (router-v8)
- Changed files: 3 supported / 3 total; Lean 3, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 628 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 4; files 3; tokens 0; tool calls 0; warnings 1; duration 27s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/StorageWord.lean (+601/-0), PrintAxioms.lean (+25/-1), Compiler/Proofs/IRGeneration/GenericInduction.lean (+1/-0)
Packet coverage
- Packet review: enabled; selected 4/8 packet(s)
- Scout: configured; status success; model reviewer_scout
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 4 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.5 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/IRGeneration/GenericInduction/StorageWord.lean:1 score 104 — public declaration/signature changed, changed imports; ask: Walk the end-to-end chain setStorageWordPreservesGoal → bindingsExactlyMatchIRVarsOnScope_writeStorageWordSlot → encodeStorageAt_writeStorageWordSlot_target → execIRStmt_sstore_of_eval: (a) confirm there is no sorry/admit/axiom and that each lemma actually discharges its stated goal rather than being admitted via non-terminal simp/rfl; (b) check that the wordOffset/wordNormalize arithmetic (uint256_add_val_eq_mod, IRStorageSlot.toNat_ofNat_wordNormalize, ne_toNat_wordNormalize_of_ne_ofNat) match
- PrintAxioms.lean:3163 score 13 — hotspot path/churn; ask: Confirm that the listed private StorageWord lemmas are the complete set the new module exports (cross-check against
Total: 5656in pkt-5: 21 new entries vs 3889-3888=1 new public, 1767-1747=20 new private, plus 0 sorry'd), and that no lemma required by downstream callers in Compiler.Proofs.IRGeneration.GenericInduction was inadvertently left private. Specifically check whether encodeStorageAt_writeStorageWordSlot_target is the right public-facing statement for downstream composition. - Compiler/Proofs/IRGeneration/GenericInduction.lean:2 score 60 — changed imports; ask: Verify the new import is positioned consistently with sibling imports (alphabetical/grouping convention) and that GenericInduction does not inadvertently expose any StorageWord lemma through
exportor unqualifiedopenthat would change the public trust surface. Confirm the import is strictly additive and does not require recompiling or re-checking other downstream modules under a different namespace. - PrintAxioms.lean:67 score 42 — changed imports; ask: Confirm the import is inserted in the correct alphabetical position among the other GenericInduction submodules, and that PrintAxioms still produces a consistent axiom/declaration inventory (cross-check the count delta in pkt-5: +21 total, +1 public, +20 private, 0 sorry'd). Ensure no other module's import was accidentally perturbed by the insertion.
Pilot mode: advisory only. Codex Review remains the merge gate.
![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: a161684147
ℹ️ 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".
| \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``` |
|
@codex address that feedback. Scope only the unresolved P2 finding about the exported theorem exposing the private setStorageWordTargetSafe premise; preserve theorem strength, add no sorry/admit/axiom, and update PrintAxioms if declaration visibility changes. |
|
To use Codex here, create an environment for this repo. |
|
Recovery gate disposition for current head |
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_0cdd40e9-4eaf-42e0-9b0a-abaaabb335b4) |
|
@codex review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 4 finding(s) · 3 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 3 Lean file(s), 634 changed supported line(s). Scout model ranked 4/5 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 4 inline comment(s).
Warnings
- coverage : Large Lean scout mode covers ranked hotspots only. Codex/human review must cover skipped hunks and proof obligations; OCR strong packet review is not wired yet.
OCR pilot metrics
- Routing: large-lean-hotspots (router-v8)
- Changed files: 3 supported / 3 total; Lean 3, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 634 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 4; files 3; tokens 0; tool calls 0; warnings 1; duration 28s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/StorageWord.lean (+607/-0), PrintAxioms.lean (+25/-1), Compiler/Proofs/IRGeneration/GenericInduction.lean (+1/-0)
Packet coverage
- Packet review: enabled; selected 4/8 packet(s)
- Scout: configured; status success; model reviewer_scout
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 4 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.5 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/IRGeneration/GenericInduction/StorageWord.lean:1 score 104 — public declaration/signature changed, changed imports; ask: Verify the full set of private lemmas in StorageWord.lean (especially writeStorageWordSlot_target, storageWordTarget_eq_wordNormalize, execIRStmt_sstore_of_eval, bindingsExactlyMatchIRVarsOnScope_writeStorageWordSlot, findDynamicArrayElementAtSlot_writeStorageWordSlots_none, encodeStorageAt_writeStorageWordSlot_target, uint256_add_val_eq_mod, toNat_ofNat_wordNormalize, ne_toNat_wordNormalize_of_ne_ofNat) are actually sound and that the public surface exposed via the import in GenericInduction.le
- PrintAxioms.lean:3163 score 13 — hotspot path/churn; ask: Cross-check every name listed under 'Compiler/Proofs/IRGeneration/GenericInduction/StorageWord.lean' against the actual definitions in pkt-1; flag any mismatch between the documented name and the real lemma, and any lemma that is in fact non-private (would change the public count in pkt-5). Confirm 0 sorry'd invariant holds for this module.
- Compiler/Proofs/IRGeneration/GenericInduction.lean:2 score 60 — changed imports; ask: Confirm the new import does not introduce namespace collisions, does not transitively pull axioms, and that the GenericInduction proofs in this file actually use the new StorageWord lemmas (or at minimum are type-checked against the new defs). Check that no public signature in GenericInduction.lean is widened by the new import.
- PrintAxioms.lean:6035 score 12 — hotspot path/churn; ask: Reconcile the +1 public / +20 private / 0 sorry delta against pkt-4's listing (11 explicit private names are shown — are the remaining 9 documented elsewhere or missing from PrintAxioms?). Identify the single new public declaration and judge whether its public exposure is appropriate.
Pilot mode: advisory only. Codex Review remains the merge gate.
|
Codex Review: Didn't find any major issues. More of your lovely PRs please. 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". |
# Conflicts: # PrintAxioms.lean
|
@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_3befc5dc-7893-441c-a91b-b01c199eb223) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 3 finding(s) · 3 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 3 Lean file(s), 634 changed supported line(s). Scout model ranked 3/5 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 3 inline comment(s).
Warnings
- coverage : Large Lean scout mode covers ranked hotspots only. Codex/human review must cover skipped hunks and proof obligations; OCR strong packet review is not wired yet.
OCR pilot metrics
- Routing: large-lean-hotspots (router-v8)
- Changed files: 3 supported / 3 total; Lean 3, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 634 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 3; files 3; tokens 0; tool calls 0; warnings 1; duration 28s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/StorageWord.lean (+607/-0), PrintAxioms.lean (+25/-1), Compiler/Proofs/IRGeneration/GenericInduction.lean (+1/-0)
Packet coverage
- Packet review: enabled; selected 3/8 packet(s)
- Scout: configured; status success; model reviewer_scout
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 3 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.5 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/IRGeneration/GenericInduction/StorageWord.lean:1 score 104 — public declaration/signature changed, changed imports; ask: Independently reconstruct: (1) what 'wordNormalize' means here (Nat mod 2^256? a Uint256/Aesop wrapper?), and whether storageWordTarget_eq_wordNormalize + evalIRExpr_storageWordTarget_of_eval really give a pointwise equivalence between the Yul sstore semantics used in execIRStmt_sstore_of_eval and the Solidity-style encoding in encodeStorageAt_writeStorageWordSlot_target; (2) whether bindingsExactlyMatchIRVarsOnScope_writeStorageWordSlot preserves the storage-stays-unchanged invariant for siblin
- PrintAxioms.lean:3164 score 13 — hotspot path/churn; ask: Identify the single new public declaration implied by the public count going 3889 → 3890 (grep StorageWord.lean for non-
privatedefs/lemmas) and verify it is appropriately scoped. Then for each of the 12 private declarations listed in the new comment block, confirm none containssorry/admitand that the names match the actualprivate theorem/private lemmadeclarations in StorageWord.lean. - Compiler/Proofs/IRGeneration/GenericInduction.lean:2 score 60 — changed imports; ask: Confirm that nothing in GenericInduction.lean or its existing imports was depending on a previously absent StorageWord module via name resolution in a way that silently changes proof behavior (e.g., a previously undefined name now resolving to a new lemma that weakens a side condition). Also confirm the import is alphabetically/structurally consistent with neighbors.
Pilot mode: advisory only. Codex Review remains the merge gate.
|
Codex Review: Didn't find any major issues. Swish! 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". |
1 participant
Theorems added
Compiler.Proofs.IRGeneration.compiledStmtStep_setStorageWord_singleSlotCompiler.Proofs.IRGeneration.compiledStmtStep_setStorageWord_singleSlot_preservesProof intuition
setStorageWordcompiles to onesstore, where the slot expression is either the base field slot oradd(baseSlot, wordOffset). The source semantics write throughwriteStorageWordSlots, so the preservation proof shows the IR storage update at the normalized target slot matches the source world update. The proof reuses the existing single-slot storage bridge shape: compile characterization comes fromCompilationModel.compileStmt, and runtime preservation is factored throughFunctionBody.runtimeStateMatchesIR. The word-offset case adds only the slot arithmetic normalization and target-slot safety needed to rule out conflicting address or dynamic-array interpretations at the written slot.Files touched
Compiler/Proofs/IRGeneration/GenericInduction/StorageWord.leanCompiler/Proofs/IRGeneration/GenericInduction.leanPrintAxioms.leanBase and dependencies
origin/main(bd54fa9c47b9abb43895c312fe1f874192ba8327)a16168414757e212ca7d6d3c94305ddf6ba6f728Validation
lean-slot lake build-> passed (Build completed successfully, remote exit 0)python3 scripts/generate_print_axioms.py --check-> passed (PrintAxioms.lean is up to date)python3 scripts/lean_lint.py --only axioms-> passed (registry is complete and synchronized with 0 source axioms)make check-> passed (All checks passed)git diff --check && git diff --cached --check-> passed (no output)git show --format= -- . ':(exclude)PrintAxioms.lean' | rg -n "\\b(sorry|admit|axiom)\\b|#exit" || true-> passed (no matches)Note
Low Risk
Formal Lean proofs only; no runtime compiler or semantics changes beyond the axiom registry update.
Overview
Adds
Compiler/Proofs/IRGeneration/GenericInduction/StorageWord.leanand wires it into generic induction andPrintAxioms.lean, extending the IR-generation proof suite with aCompiledStmtStepforsetStorageWordon a single non-transient field slot.The public theorem
compiledStmtStep_setStorageWord_singleSlotshows compilation emits onesstore(base slot oradd(base, wordOffset)) and that execution preservesruntimeStateMatchesIR: sourcewriteStorageWordSlotsaligns with IRabstractStoreStorageOrMappingat the EVM-normalized target slot. Supporting lemmas coversstoreevaluation, slot arithmetic vswordNormalize, andencodeStorageAton the written slot vs other slots, undersetStorageWordTargetSafe(no conflicting address/dynamic-array interpretation at the target).Reviewed by Cursor Bugbot for commit 686757e. Bugbot is set up for automated code reviews on this repo. Configure here.