proof: reduce whole-contract legacy-bodies premise to per-statement interface#2128
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_961d6c55-da7d-45df-94e2-04bd9cc9b0f1) |
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
2544beb to
64a61de
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_7f337ef3-dabc-4419-8160-c03cdd309e92) |
|
/ocr review |
|
/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: completed_with_errors · 0 finding(s) · 3 files · 742245 tokens · 80 tool calls
Some files could not be reviewed due to errors.
Warnings
- subtask_error Compiler/Proofs/IRGeneration/Contract.lean: LLM completion error: context deadline exceeded
- subtask_error PrintAxioms.lean: LLM completion error: context deadline exceeded
Pilot mode: advisory only. Codex Review remains the merge gate.
|
/ocr review |
OpenCodeReview first-pass reviewStatus: completed_with_errors · 0 finding(s) · 3 files · 1259023 tokens · 121 tool calls Some files could not be reviewed due to errors. Warnings
Pilot mode: advisory only. Codex Review remains the merge gate. |
|
/ocr review |
|
No stderr captured. |
|
/ocr review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: packetized_review · Mode: large-lean-hotspots · 7 finding(s) · 3 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 3 Lean file(s), 138 changed supported line(s). Full-file OCR was not attempted; this is deterministic hotspot coverage, not complete review coverage.
✅ Posted 7 inline comment(s).
Warnings
- coverage : Packetized Lean review covers ranked hotspots only. Codex/human review must cover skipped hunks and proof obligations.
OCR pilot metrics
- Routing: large-lean-hotspots (router-v3)
- Changed files: 3 supported / 3 total; Lean 3, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 138 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status packetized_review; comments 7; files 3; tokens 0; tool calls 0; warnings 1; duration 1s
- Largest changed files: Compiler/Proofs/IRGeneration/Contract.lean (+83/-0), Compiler/Proofs/IRGeneration/Function.lean (+49/-0), PrintAxioms.lean (+5/-1)
Packet coverage
- Packet review: enabled; selected 7/8 packet(s)
- Residual risk: Reviewed top 7 packet(s) by deterministic risk score; remaining changed hunks/files require Codex or human proof review.
- Covered packets:
- PrintAxioms.lean:5964 score 92 — introduced sorry/admit
- Compiler/Proofs/IRGeneration/Function.lean:2861 score 66 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/Contract.lean:2876 score 66 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/Contract.lean:1349 score 65 — public declaration/signature changed
- PrintAxioms.lean:2139 score 12 — hotspot path/churn
- PrintAxioms.lean:1884 score 12 — hotspot path/churn
- PrintAxioms.lean:1922 score 12 — hotspot path/churn
Pilot mode: advisory only. Codex Review remains the merge gate.
|
/ocr review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 7 finding(s) · 3 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 3 Lean file(s), 138 changed supported line(s). Deterministic fallback triage; scout model not configured and strong packet review required. Full-file OCR was not attempted.
✅ Posted 7 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-v4)
- Changed files: 3 supported / 3 total; Lean 3, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 138 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 7; files 3; tokens 0; tool calls 0; warnings 1; duration 1s
- Largest changed files: Compiler/Proofs/IRGeneration/Contract.lean (+83/-0), Compiler/Proofs/IRGeneration/Function.lean (+49/-0), PrintAxioms.lean (+5/-1)
Packet coverage
- Packet review: enabled; selected 7/8 packet(s)
- Scout: not configured; status not_configured; model none
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 7 deterministically 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/Function.lean:2861 score 66 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/Contract.lean:2876 score 66 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/Contract.lean:1349 score 65 — public declaration/signature changed
- PrintAxioms.lean:2139 score 12 — hotspot path/churn
- PrintAxioms.lean:5964 score 12 — hotspot path/churn
- PrintAxioms.lean:1884 score 12 — hotspot path/churn
- PrintAxioms.lean:1922 score 12 — hotspot path/churn
Pilot mode: advisory only. Codex Review remains the merge gate.
|
/ocr review |
1 similar comment
|
/ocr review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 7 finding(s) · 3 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 3 Lean file(s), 138 changed supported line(s). Scout triage fallback_deterministic; strong packet review required. Full-file OCR was not attempted.
✅ Posted 7 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-v5)
- Changed files: 3 supported / 3 total; Lean 3, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 138 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 7; files 3; tokens 0; tool calls 0; warnings 1; duration 1s
- Largest changed files: Compiler/Proofs/IRGeneration/Contract.lean (+83/-0), Compiler/Proofs/IRGeneration/Function.lean (+49/-0), PrintAxioms.lean (+5/-1)
Packet coverage
- Packet review: enabled; selected 7/8 packet(s)
- Scout: configured; status fallback_deterministic; model MiniMax-M3
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 7 deterministically 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/Function.lean:2861 score 66 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/Contract.lean:2876 score 66 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/Contract.lean:1349 score 65 — public declaration/signature changed
- PrintAxioms.lean:2139 score 12 — hotspot path/churn
- PrintAxioms.lean:5964 score 12 — hotspot path/churn
- PrintAxioms.lean:1884 score 12 — hotspot path/churn
- PrintAxioms.lean:1922 score 12 — hotspot path/churn
Pilot mode: advisory only. Codex Review remains the merge gate.
|
/ocr review |
|
/ocr review |
|
/ocr review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 7 finding(s) · 3 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 3 Lean file(s), 138 changed supported line(s). Scout triage fallback_deterministic; strong packet review required. Full-file OCR was not attempted.
✅ Posted 7 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: 138 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 7; files 3; tokens 0; tool calls 0; warnings 1; duration 1s
- Largest changed files: Compiler/Proofs/IRGeneration/Contract.lean (+83/-0), Compiler/Proofs/IRGeneration/Function.lean (+49/-0), PrintAxioms.lean (+5/-1)
Packet coverage
- Packet review: enabled; selected 7/8 packet(s)
- Scout: configured; status fallback_deterministic; model MiniMax-M3
- Scout provider HTTP status: 400
- Scout provider error: {"error":{"message":"Model 'MiniMax-M3' is not a known chain or a 'provider/model' id. List chains at /api/model-routing/chains and all supported models at /api/providers/catalog.","type":"error","code":"model_not_found"}}
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 7 deterministically 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/Function.lean:2861 score 66 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/Contract.lean:2876 score 66 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/Contract.lean:1349 score 65 — public declaration/signature changed
- PrintAxioms.lean:2139 score 12 — hotspot path/churn
- PrintAxioms.lean:5964 score 12 — hotspot path/churn
- PrintAxioms.lean:1884 score 12 — hotspot path/churn
- PrintAxioms.lean:1922 score 12 — hotspot path/churn
Pilot mode: advisory only. Codex Review remains the merge gate.
|
/ocr review |
1 similar comment
|
/ocr review |
|
@codex review |
|
Codex Review: Didn't find any major issues. 👍 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". |
|
/ocr review |
OpenCodeReview first-pass reviewStatus: error · Mode: legacy · 0 finding(s) · files unknown OCR produced no JSON output OCR stderr highlightsOCR pilot metrics
Pilot mode: advisory only. Codex Review remains the merge gate. |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: large-lean-hotspots · Mode: large-lean-hotspots · 0 finding(s) · 0 files · 0 tokens · 0 tool calls
Lean packet budget exceeded: 25 Lean file(s), 3963 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics
- Routing: large-lean-hotspots (router-v8)
- Changed files: 36 supported / 36 total; Lean 25, trust docs 0, workflow/scripts 9, contracts 0, docs 2
- Changed lines: 3963 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 0s
- Largest changed files: .github/scripts/test-ocr-routing.js (+0/-1808), .github/scripts/ocr-router.js (+0/-1307), .github/scripts/post-ocr-review.js (+17/-334), docs/C2_STORAGE_LENS_PART2_SCOPE.md (+0/-72), .github/workflows/ocr-review.yml (+9/-60)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model reviewer_scout
- 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.5 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.
|
Resolving the 28 open |
1 participant
Summary
Complementary #2080 fragment slice built on top of the phase30 whole-contract
retarget (depends on #2126; base =
paloma/issue-2080-whole-contract-retarget-phase30).It closes the body-shape half of the whole-contract plumbing by reducing the
LegacyCompatibleExternalBodies irpremise still carried bycompile_preserves_semantics_with_helper_proofs_and_helper_ir_of_compileValidatedCoredown to the same per-statement
StmtListCompiledLegacyCompatibleinterfacethat #2080 already tracks for the proven-disjoint infrastructure.
New results (purely additive, no existing declaration touched):
Function.leancompileStmtList_legacyCompatible_of_interface(private) — reusable legacycomposition: a per-statement legacy interface + a successful
compileStmtListyields a
LegacyCompatibleExternalStmtListcompiled body, by structuralinduction mirroring the existing disjoint-composition chain.
compileFunctionSpec_body_legacyCompatible_of_interface— lifts that to awhole function body (param loads ++ compiled statements).
Contract.leanlegacyCompatibleExternalBodies_of_compileValidatedCore_of_interface— bridgesthe per-function interface across every selector-dispatched function to
LegacyCompatibleExternalBodies irfor a concretecompileValidatedCoreoutput.compile_preserves_semantics_with_helper_proofs_and_helper_ir_of_compileValidatedCore_of_interface— whole-contract retarget theorem restated directly on the per-statement
interface; discharges the
hlegacyBodiespremise internally.This does not duplicate the active storage/mapping bridge work; it reuses the
existing legacy-subset predicates and mirrors the already-landed disjoint chain.
Validation
lean-slot lake build Compiler.Proofs.IRGeneration.Function— greenlean-slot lake build Compiler.Proofs.IRGeneration.Contract— greenweakened, no signature changed, so no downstream module can regress.
sorry/admit/axiom/native_decidein any added line.lake buildwas launched as the authoritative confirmation andGitHub CI runs it independently on this PR.
Test plan
lake buildgreenNote
Low Risk
Purely additive Lean proofs with no signature changes to existing theorems; risk is limited to proof maintenance in the IR generation proof layer, not runtime or auth behavior.
Overview
Adds legacy-compatibility composition lemmas so the helper-aware whole-contract retarget theorem can take per-statement
StmtListCompiledLegacyCompatibleobligations (aligned with #2080) instead of a whole-contractLegacyCompatibleExternalBodies irpremise.In
Function.lean,compileStmtList_legacyCompatible_of_interfaceinductively lifts the per-statement interface to aLegacyCompatibleExternalStmtListfor a successfulcompileStmtList, andcompileFunctionSpec_body_legacyCompatible_of_interfaceextends that to full external function bodies (param loads plus compiled statements).In
Contract.lean,legacyCompatibleExternalBodies_of_compileValidatedCore_of_interfacewalks every selector-dispatched function from acompileValidatedCoreoutput and assemblesLegacyCompatibleExternalBodies.compile_preserves_semantics_with_helper_proofs_and_helper_ir_of_compileValidatedCore_of_interfaceis the same semantic conclusion as the existing..._of_compileValidatedCoretheorem but dischargeshlegacyBodiesinternally fromhbodies.PrintAxioms.leanregisters the new public theorems.Reviewed by Cursor Bugbot for commit 64a61de. Bugbot is set up for automated code reviews on this repo. Configure here.