proof: bridge mappingPackedWord source reads (parallel/experimental)#2127
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_6b58932e-f287-4bea-8866-68ac2ae26ea2) |
| \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``` |
|
Review status: merge blocked only on still-running CI (runner queue) Reviewed the diff (single commit 5c7d97d, Local validation (warm cache, at PR head 5c7d97d):
CI: original Will merge once those two shards complete green under the standing merge policy. |
Widen the native-safe source-expression read grammar to cover packed mapping-word reads (`Expr.mappingPackedWord`). These lower to `and(shr(lit offset, mappingSlotRead), lit mask)`, exactly the shape already discharged for packed struct-member and packed storage reads. - Add `BridgedSourceExpr.mappingPackedWord` constructor. - Prove the corresponding case in `compileExpr_bridgedSource` using the existing `compileMappingSlotRead_bridged` and `bridgedExpr_packed_read` lemmas. - Handle the constructor in `compileRequireFailCond_bridgedSource` via the default (non-comparison) path. - Sync module/inductive docs (mappingPackedWord now in scope). No gate flip: `mappingPackedWord` remains on the state-surface gate; this is a building block toward removing it. Both theorems depend only on [propext, Quot.sound]; no new sorry/admit/axiom.
Th0rgal
force-pushed
the
paloma/parallel-claude-fragment-2081
branch
from
5c7d97d to
abbf8d5
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_03ef24dc-6530-484e-82b2-27cbbe097e59) |
|
/ocr review |
|
/ocr review |
|
/ocr review |
|
/ocr review |
|
No stderr captured. |
|
/ocr review |
![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: small-lean · 0 finding(s) · 1 files · 560563 tokens · 28 tool calls
No comments generated. Looks good to me.
OCR pilot metrics
- Routing: small-lean (router-v3)
- Changed files: 1 supported / 1 total; Lean 1, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 40 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 1; tokens 560563; tool calls 28; warnings 0; duration 465s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean (+36/-4)
Pilot mode: advisory only. Codex Review remains the merge gate.
|
/ocr review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: success · Mode: small-lean · 0 finding(s) · 1 files · 192286 tokens · 20 tool calls
No comments generated. Looks good to me.
OCR pilot metrics
- Routing: small-lean (router-v4)
- Changed files: 1 supported / 1 total; Lean 1, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 40 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 1; tokens 192286; tool calls 20; warnings 0; duration 195s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean (+36/-4)
Pilot mode: advisory only. Codex Review remains the merge gate.
|
/ocr review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: success · Mode: small-lean · 0 finding(s) · 1 files · 137565 tokens · 12 tool calls
No comments generated. Looks good to me.
OCR pilot metrics
- Routing: small-lean (router-v8)
- Changed files: 1 supported / 1 total; Lean 1, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 40 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 1; tokens 137565; tool calls 12; warnings 0; duration 196s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean (+36/-4)
Pilot mode: advisory only. Codex Review remains the merge gate.
1 participant
Parallel / experimental fragment slice
Do not merge into the #2080 review stack gate. This is an independent, parallel proof-fragment expansion opened off the current stack tip (
paloma/issue-2080-whole-contract-retarget-phase30, currently under review as #2126). It is intended to advance the proven fragment without blocking or reordering the #2122 → #2124 → #2126 drain.Summary
Widens the native-safe source-expression read grammar (
BridgedSourceExpr) to cover packed mapping-word reads (Expr.mappingPackedWord). These lower toand(shr(lit offset, mappingSlotRead), lit mask)— the exact bridged shape already proven for packed struct-member reads (structMember) and packed storage reads.BridgedSourceExpr.mappingPackedWord.compileExpr_bridgedSource, discharged with the pre-existingcompileMappingSlotRead_bridgedandbridgedExpr_packed_readlemmas (no new supporting lemmas needed).compileRequireFailCond_bridgedSourcevia the default (non-comparison) path.What this is NOT
This does not flip the state-surface gate:
mappingPackedWordremains marked unsupported inexprTouchesUnsupportedStateSurface. This PR only widens the read-bridge grammar — a building block toward later removingmappingPackedWordfrom that gate. No existing theorem is weakened; no check is disabled.Validation (lean-slot / DGX Spark offload)
lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanSourceExprClosure→ green (exit 0).lake build PrintAxioms→ green (exit 0), full elaboration,sorryAxcount 0.#print axioms compileExpr_bridgedSource→[propext, Quot.sound]#print axioms compileRequireFailCond_bridgedSource→[propext, Quot.sound]No new
sorry/admit/axiom/native_decide. Diff is +36 / -4, single file.Note
Low Risk
Single-file Lean proof extension reusing established packed-read lemmas; no compiler behavior, auth, or gate changes.
Overview
Extends the
BridgedSourceExprread grammar soExpr.mappingPackedWordis in scope, with module docs updated to list it alongside othermappingSlotbridges instead of treating packed mapping reads as unsupported in this fragment.compileExpr_bridgedSourcegains a case that follows the packedstructMemberpattern: compile the key, runcompileMappingSlotRead, then wrap the slot word withbridgedExpr_packed_readusing existingcompileMappingSlotRead_bridgedlemmas (no new helper theorems).compileRequireFailCond_bridgedSourceadds the matching constructor and routes it through the defaultiszero(cond)path.This is proof-only widening of the bridged compile closure; it does not change
exprTouchesUnsupportedStateSurfaceor relax runtime/state-surface gates.Reviewed by Cursor Bugbot for commit abbf8d5. Bugbot is set up for automated code reviews on this repo. Configure here.