proof: repair helper body seam main merge#2154
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_469c8078-1f21-4e74-ae17-d1cf88e91c24) |
![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 · 122377 tokens · 16 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: 82 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 2; tokens 122377; tool calls 16; warnings 0; duration 367s
- Largest changed files: Compiler/Proofs/IRGeneration/Function.lean (+78/-0), PrintAxioms.lean (+3/-1)
Pilot mode: advisory only. Codex Review remains the merge gate.
…ict-repair # Conflicts: # PrintAxioms.lean
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_5489365b-e9ac-4374-ab19-78b557adaeca) |
|
@codex review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 6 finding(s) · 4 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 4 Lean file(s), 617 changed supported line(s). Scout model ranked 6/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 6 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: 4 supported / 4 total; Lean 4, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 617 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 6; files 4; tokens 0; tool calls 0; warnings 1; duration 27s
- Largest changed files: Compiler/Proofs/IRGeneration/HelperSummaryEvidence.lean (+513/-0), Compiler/Proofs/IRGeneration/Function.lean (+78/-0), PrintAxioms.lean (+24/-1), Compiler.lean (+1/-0)
Packet coverage
- Packet review: enabled; selected 6/8 packet(s)
- Scout: configured; status success; model reviewer_scout
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 6 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/HelperSummaryEvidence.lean:1 score 104 — public declaration/signature changed, changed imports; ask: Audit each newly introduced public theorem in HelperSummaryEvidence.lean (exactInternalHelperSummary_sound, exactInternalHelperSummary_preservesWorldOnSuccess_of_readOnly_body, exactInternalHelperSummary_preservesWorldOnSuccess_of_empty_body, exactInternalHelperSupport_toWitness_contract_eq_exact, exactInternalHelperSupport_toWitness_summary_sound, exactInternalHelperSupport_toWitness_preservesWorldOnSuccess): verify that no sorry/admit is used, that the proof does not silently rely on classical
- Compiler/Proofs/IRGeneration/Function.lean:3551 score 65 — public declaration/signature changed; ask: Check the proof of stmtList_setStructMember2Single_compiledLegacyCompatible: does it actually unfold CompilationModel.compileSetStructMember2 (which is the change site in pkt-5) and confirm LegacyCompatibleExternalStmtList on the resulting Yul, or does it merely dispatch to compileSetStructMember2_legacyCompatible? Verify the hslot / hmember / hmembers hypotheses are connected and that there is no use of sorry / native.decide / a dubious classical side-condition.
- Compiler/Proofs/IRGeneration/Function.lean:3367 score 32 — hotspot path/churn; ask: Step through compileSetStructMember2_legacyCompatible: confirm that every branch of the unfold (isMapping2, findStructMembers, findStructMember, the inner match on packed fields) is actually discharged and not silently absorbed by simp or a sorry. Check whether the 'packed := none' hypothesis in hmember is actually used or whether the lemma would equally prove a packed-struct case — if yes, the strengthening is unsafe.
- PrintAxioms.lean:3171 score 13 — hotspot path/churn; ask: Re-run #print axioms on each newly listed HelperSummaryEvidence lemma; confirm that none emits 'propext', 'Classical.choice', 'sorryAx', or any other axiom beyond those already accepted elsewhere in the project. Pay special attention to exactInternalHelperSupport_toWitness_contract_eq_exact — 'eq_exact' wording often hides a sorry or propext shortcut.
- PrintAxioms.lean:2157 score 12 — hotspot path/churn; ask: Verify that the visibility asymmetry is intentional: stmtList_setStructMember2Single_compiledLegacyCompatible is public while compileSetStructMember2_legacyCompatible is private. Confirm that exporting the public theorem cannot be used to bypass any invariant enforced only inside the private proof (e.g., by constructing inputs where the private lemma's hypotheses are vacuously satisfied).
- Compiler.lean:43 score 42 — changed imports; ask: Confirm that the import ordering of HelperSummaryEvidence is consistent with how the file references SourceSemantics (opened in pkt-1) and that no transitive import cycle or name-shadowing with HelperBodyBridge is introduced by placing it directly after SourceSemantics.
Pilot mode: advisory only. Codex Review remains the merge gate.
|
Post-merge gate evidence for head 19b5245 / OCR scout threads:
|
![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: 19b52454ee
ℹ️ 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".
| simp [hkey1Expr, hkey2Expr, hvalueExpr, bind, Except.bind] at hcompile | ||
| cases hcompile | ||
| exact .exprStmt _ _ .nil | ||
| | cons slot' rest => |
There was a problem hiding this comment.
cases alternative
This | cons alternative is indented inside the preceding | nil => branch rather than aligned with it in the cases rest with block. Lean's layout-sensitive parser treats the following token as part of the nil branch instead of a sibling case, so importing Compiler.Proofs.IRGeneration.Function will fail to parse/build; align this branch with | nil =>.
Useful? React with 👍 / 👎.
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_32701bdd-d402-4d07-a655-4583fa5ca5b3) |
|
@codex review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 8 finding(s) · 4 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 4 Lean file(s), 617 changed supported line(s). Scout triage fallback_deterministic; strong packet review required. Full-file OCR was not attempted.
✅ Posted 8 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: 4 supported / 4 total; Lean 4, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 617 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 8; files 4; tokens 0; tool calls 0; warnings 1; duration 45s
- Largest changed files: Compiler/Proofs/IRGeneration/HelperSummaryEvidence.lean (+513/-0), Compiler/Proofs/IRGeneration/Function.lean (+78/-0), PrintAxioms.lean (+24/-1), Compiler.lean (+1/-0)
Packet coverage
- Packet review: enabled; selected 8/8 packet(s)
- Scout: configured; status fallback_deterministic; model reviewer_scout
- Scout provider error: This operation was aborted
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 8 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/HelperSummaryEvidence.lean:1 score 104 — public declaration/signature changed, changed imports
- Compiler/Proofs/IRGeneration/Function.lean:3551 score 65 — public declaration/signature changed
- Compiler.lean:43 score 42 — changed imports
- PrintAxioms.lean:68 score 42 — changed imports
- Compiler/Proofs/IRGeneration/Function.lean:3367 score 32 — hotspot path/churn
- PrintAxioms.lean:3171 score 13 — hotspot path/churn
- PrintAxioms.lean:2157 score 12 — hotspot path/churn
- PrintAxioms.lean:6020 score 12 — hotspot path/churn
Pilot mode: advisory only. Codex Review remains the merge gate.
|
Codex Review: Didn't find any major issues. Already looking forward to the next diff. 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". |
|
@codex review |
|
Codex Review: Didn't find any major issues. Nice work! 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". |
|
@codex review |
|
Codex Review: Didn't find any major issues. What shall we delve into next? 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". |
…am' into codex/2153-main-conflict-repair # Conflicts: # PrintAxioms.lean
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_7ec62ea5-19dc-4510-97c1-0f4ba9c928b4) |
|
@codex review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: success · Mode: small-lean · 0 finding(s) · 1 files · 7777 tokens · 1 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: 2 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status success; comments 0; files 1; tokens 7777; tool calls 1; warnings 0; duration 16s
- Largest changed files: Compiler/Proofs/IRGeneration/Function.lean (+1/-1)
Pilot mode: advisory only. Codex Review remains the merge gate.
|
Codex Review: Didn't find any major issues. What shall we delve into next? 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
Summary
origin/mainintopaloma/issue-2080-helper-body-seamwithout modifying the helper-body proof slice.PrintAxioms.leanconflict by preserving both:setStructMember2legacy-compatible theorem entries from proof: package legacy compatibility for struct member2 writes #2146HelperBodyBridgelookup/body-shape theorem entriesFunction.leansetStructMember2legacy-compatible theorem pair through the main merge, addressing the OCR proof-interface concern that proof: bridge compiled helper-body shape for rank-0 seam #2153 appeared to drop those public/private names.Validation
git diff --cached --checkpassed before commitpython3 scripts/check_proof_length.pypassedpython3 scripts/generate_print_axioms.py --checkpassedlean-slot lake build Compiler.Proofs.IRGeneration.HelperBodyBridge PrintAxiomspassed via Spark (remote build finished (exit=0),Build completed successfully.)sorry,admit, oraxiom; only generatedPrintAxiomscomment text containssorry'd.Notes
This is only a conflict/proof-interface repair for #2153. It does not claim #2080 closure and does not prove
execIRInternalFunctionWithInternals_obeys_internal_helper_summary.Note
Low Risk
Pure proof-structure/indentation repair in an existing theorem; no runtime or compiler behavior changes.
Overview
Repairs the
compileSetStructMember2legacy-compatible proof inFunction.leanafter mergingmaininto the helper-body seam branch.The
cons slot' restarm of thecases rest withon write slots was incorrectly indented under thenilbranch, so Lean treated it as nested inside the single-slot case instead of as the separate multi-slot path. Re-indenting restores the intended structure: single-slot still ends withexact .exprStmt _ _ .nil, and two-or-more slots still uselegacyCompatibleExternalStmtList_block_key1_key2_value_writeswith the nestedmappingSlot/wordOffsetslot function. No change to proof content—only case-tree layout so thesetStructMember2theorem pair from main stays buildable alongside the helper-body work.Reviewed by Cursor Bugbot for commit abce908. Bugbot is set up for automated code reviews on this repo. Configure here.