proof: bridge mappingPackedWord source reads (parallel/experimental)#2127
Open
Th0rgal wants to merge 117 commits into
Open
proof: bridge mappingPackedWord source reads (parallel/experimental)#2127Th0rgal wants to merge 117 commits into
Th0rgal wants to merge 117 commits into
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) |
Contributor
| \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``` |
Member
Author
|
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. |
Add the missing legacy-compatibility analog of the proven disjoint composition: - compileStmtList_legacyCompatible_of_interface: lift the per-statement StmtListCompiledLegacyCompatible interface to a whole-list LegacyCompatibleExternalStmtList witness for the emitted Yul body. - compileFunctionSpec_body_legacyCompatible_of_interface: per-function bridge composing genParamLoads_scalar_legacy with the body lemma. These lift the remaining per-statement #2080 legacy obligations toward the whole-contract LegacyCompatibleExternalBodies target.
…om per-statement interface
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
July 9, 2026 09:50
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) |
Member
Author
|
/ocr review |
Includes Verity-specific file types in OCR rules and avoids cancelling OCR runs on unrelated comments.
Tightens Verity-specific OCR rules and versions OCR dedupe by trusted rules hash so changed rules can re-review unchanged PR heads.
Member
Author
|
/ocr review |
Bounds OCR prompt context, extends job timeout, strips generated review tails, and keeps partial OCR outputs retryable without dropping completed findings.
Member
Author
|
/ocr review |
Add trusted OCR routing, metrics, and bounded large-Lean hotspot coverage.
Member
Author
|
/ocr review |
Contributor
|
No stderr captured. |
Fix the OCR router base fetch on self-hosted runners and avoid posting invalid legacy OCR output when routing fails.
Member
Author
|
/ocr review |
* ci: bootstrap OCR Lean toolchain client per run * test: isolate Lean LSP GitHub path harness * ci: preserve router-only OCR summaries * test: cover Lean LSP elan bootstrap * fix: isolate OCR elan bootstrap per run
Import IRInterpreter so the exact helper-dispatch lookup field (irInternalFunctionDefOfStmt?) resolves in SupportedSpec, tolerate termination goals already closed by simp in the surface decreasing_by, and newline-separate the packaged-dispatch witness struct fields so the anonymous-constructor literals parse in GenericInduction/Calls.
…dge-slice proof: package direct helper statement context bridge
…storageword-bridge # Conflicts: # PrintAxioms.lean
…dmap docs: queue Lean 4.30 migration last
…storageword-bridge
…eword-bridge proof: bridge setStorageWord statement preservation
…ofile Add external param binding witnesses
…y-offset-bridge Bridge dynamic ABI array member offsets to core model
Single conflict: the auto-generated theorem tally comment in PrintAxioms.lean (both sides bumped it). Kept main's line; the derived artifact refresh will regenerate the exact merged count.
… codex/2083-constructor-arg
The pilot's output buried the review under pipeline internals: - sanitizeCommentText backslash-escaped every markdown character, so findings rendered as 'ErrorRevert\.lean' / 'source\-level', flattened the model's paragraphs, and hard-sliced at 700 chars mid-word. Keep the injection protections (mention zero-width, <> entities, control chars) but stop escaping markdown, preserve paragraph breaks, and truncate at a word boundary with an explicit '… (truncated)' marker. - Added-line samples now render as inline code spans (new renderCodeSample) so Lean/Yul operators are not parsed as markdown. - renderPacketFinding leads with the finding, then the reviewer question, then the router's selection rationale — instead of burying the substance behind 'Large Lean packet selected…' boilerplate. - The summary comment now opens with a one-line human verdict with a severity rollup (e.g. '🟡 Scout triage only — 8 finding(s) (2 high / 4 medium / 2 low)…') instead of 'Status: scout_triage · Mode: large-lean-hotspots · 0 tokens · 0 tool calls'. Retryable runs say so in plain text; errored runs are explicit that the PR is unreviewed. - Ops telemetry (pilot metrics + packet coverage) folds into <details>; the duplicated scout-coverage warning is deduped; router mode names are dropped from inline badges (severity and semantic categories stay). node test-ocr-routing.js passes (300 asserts).
- renderCodeSample: substitute backticks with a prime mark and always
render inside one code span, instead of an unescaped prose fallback
- severityRollup: hasOwnProperty guard so inherited property names
('constructor', '__proto__') from model severities can't corrupt counts
- verdictLine: 'no-supported' runs now say OCR did not run instead of
claiming a clean first pass
fix(ocr): make posted reviews readable
Support constructorArg in core proof surface
scoutTimeoutMs was 45s; GLM-5.2 and MiniMax-M3 are thinking models that
reason at length on the 18k-char dossier before emitting the JSON
verdict, so every scout call aborted ('This operation was aborted') and
all large-Lean reviews silently ran fallback_deterministic — the LLM
scout has effectively never fired in production. Raise to 240s; the
scout runs once per review inside a 45-minute job budget.
node test-ocr-routing.js passes.
fix(ocr): give the scout model time to think
Single-scout review converged serially — a real PR needed 3 review cycles because each pass surfaced one new defect class (checksum-manifest scoping → verification-replay independence → shallow-clone verification contract). Multi-lens: fan out one scout call per lens (provenance, verification-independence, environment-determinism, proof-soundness) in parallel and union/de-dup findings, so one repair cycle addresses all classes. Per-lens failures are caught so one broken lens cannot lose the others; all-lenses-fail keeps the existing fallback_deterministic surface. Wall-clock stays one scoutTimeoutMs (concurrent). ROUTER_VERSION v9->v10 so the richer review is not suppressed by a prior single-lens dedup tag. Accumulating rubric (.github/ocr/rubric.json) seeded with the three known defect classes, injected into every scout dossier; appendRubricItem() is the documented growth hook. Lenses subsettable via OCR_SCOUT_LENSES. node test-ocr-routing.js passes (8 new tests). Input sanitization intact.
feat(ocr): multi-lens scout review + accumulating rubric
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_ef3880bd-0e35-494c-a834-d68ee0597a02) |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Contributor
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: 60 Lean file(s), 11131 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: 95 supported / 99 total; Lean 60, trust docs 2, workflow/scripts 30, contracts 0, docs 3
- Changed lines: 11131 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: .github/scripts/test-ocr-routing.js (+2113/-0), .github/scripts/ocr-router.js (+1576/-0), Compiler/Proofs/IRGeneration/Function.lean (+1039/-45), Compiler/Proofs/IRGeneration/GenericInduction/StorageWord.lean (+607/-0), Compiler/Proofs/IRGeneration/HelperSummaryEvidence.lean (+513/-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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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.