proof: bridge zero-offset storage word writes#2163
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_970364c3-711e-4eb8-ba38-135a6b20617e) |
OpenCodeReview first-pass reviewStatus: scout_triage · Mode: large-lean-hotspots · 8 finding(s) · 4 files · 0 tokens · 0 tool calls Large Lean diff routed to bounded packet review: 5 Lean file(s), 1503 changed supported line(s). Scout model ranked 8/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
Warnings
OCR pilot metrics
Packet coverage
Pilot mode: advisory only. Codex Review remains the merge gate. Inline findings that could not be posted
|
Th0rgal
force-pushed
the
codex/2081-storageword-single-slot
branch
from
861b721 to
51b524c
Compare
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_975a70a9-2202-409a-aaa7-bcc9be4ed3c4) |
| \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``` |
![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: success · Mode: medium-lean · 0 finding(s) · 2 files · 1249840 tokens · 88 tool calls
No comments generated. Looks good to me.
OCR pilot metrics
- Routing: medium-lean (router-v8)
- Changed files: 2 supported / 2 total; Lean 2, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 168 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 2; tokens 1249840; tool calls 88; warnings 0; duration 1264s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/Storage.lean (+163/-0), PrintAxioms.lean (+4/-1)
Pilot mode: advisory only. Codex Review remains the merge gate.
|
@codex review |
|
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". |
|
Recovery gate disposition for current head |
…d-single-slot # 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_d7c6650b-1f2b-46be-8023-d63707bfd68d) |
|
Codex Review: Didn't find any major issues. You're on a roll. 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". |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: success · Mode: medium-lean · 0 finding(s) · 3 files · 641972 tokens · 50 tool calls
No comments generated. Looks good to me.
OCR pilot metrics
- Routing: medium-lean (router-v8)
- Changed files: 3 supported / 3 total; Lean 2, trust docs 0, workflow/scripts 1, contracts 0, docs 0
- Changed lines: 173 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 3; tokens 641972; tool calls 50; warnings 0; duration 696s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/Storage.lean (+163/-0), PrintAxioms.lean (+4/-1), scripts/check_proof_length.py (+5/-0)
Pilot mode: advisory only. Codex Review remains the merge gate.
1 participant
Summary
runtimeStateMatchesIR_writeStorageWordSlot_zeroOffsetfor zero-offset single-slotwriteStorageWordSlotspreservation.compiledStmtStep_setStorageWord_singleSlot_zeroOffsetproving.setStorageWord fieldName 0 valuelowers to the expected singletonsstorewhen the resolved field is a non-address, non-dynamic, non-transient, unaliased uint slot.stmtListGenericCore_singleton_setStorageWord_zeroOffset_singleSlotconsumer/regression coverage.PrintAxioms.lean.Validation
lake build Compiler.Proofs.IRGeneration.GenericInduction.Storagelake build Compiler.Proofs.IRGeneration.GenericInductionlake build PrintAxiomspython3 scripts/lean_lint.py --only lean_hygienepython3 scripts/generate_print_axioms.py --checkpython3 scripts/lean_lint.py --only axiomsgit diff --checkNotes
sorry,admit,axiom, ornative_decide; no theorem weakening; no fake Yul shim.origin/mainatb8b9896d.wordOffsettarget-slot arithmetic and alias-slot multiwrite variants, plus transient storage-word writes, before broader generic gates can be flipped.Note
Low Risk
Proof-only changes in the formal verification layer; no compiler or runtime behavior is modified.
Overview
Extends the generic storage induction proofs so zero-offset storage-word writes are covered the same way scalar
setStoragealready is.A private lemma
runtimeStateMatchesIR_writeStorageWordSlot_zeroOffsetshows that updating the source world viawriteStorageWordSlotswith offset0stays in sync withabstractStoreStorageOrMappingon the IR side (including the non-written-slot case viaencodeStorageAt_congr).The public theorem
compiledStmtStep_setStorageWord_singleSlot_zeroOffsetproves that.setStorageWord fieldName 0 valuelowers to a singlesstorewith a literal slot when the field is a resolved, unaliased, unpacked, non-address, non-dynamic, non-transient uint slot with no write-slot conflicts, and that execution preserves runtime state, fuel, bindings, and scope discipline.A private
stmtListGenericCore_singleton_setStorageWord_zeroOffset_singleSlothooks this into the stmt-list generic core for regression-style coverage.PrintAxioms.leanis regenerated to export the new compiled-step theorem, andcheck_proof_length.pyallowlists the long coupled preservation witness.Reviewed by Cursor Bugbot for commit 5e4b958. Bugbot is set up for automated code reviews on this repo. Configure here.