proof: package direct helper statement context bridge#2147
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
| \n### CI Failure Hints\n\nFailed jobs: `build`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
|
@codex review |
|
Integration note (Fable, integration boss): this PR is a central helper-semantics bridge. It has been retargeted to main after the legacy-compatibility stack (#2128, #2134, #2141, #2143, #2145, #2146) merged. It intentionally remains DRAFT and MUST NOT be merged without explicit human proof-interface review. |
![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: cdae87fa38
ℹ️ 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".
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ad2525595a
ℹ️ 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".
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_bbea732d-fd18-4b8d-9bab-5a35dc8871f0) |
OpenCodeReview first-pass reviewStatus: scout_triage · Mode: large-lean-hotspots · 6 finding(s) · 5 files · 0 tokens · 0 tool calls Large Lean diff routed to bounded packet review: 7 Lean file(s), 980 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.
Warnings
OCR pilot metrics
Packet coverage
Pilot mode: advisory only. Codex Review remains the merge gate. Inline findings that could not be posted
|
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b634483022
ℹ️ 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".
| have hfindSome : (findInternalFunction? runtimeContract | ||
| (CompilationModel.internalFunctionYulName calleeName)).isSome = true := by | ||
| simpa [hcalleeName] using findInternalFunction?_of_compileInternalFunction_mem | ||
| compiledHelper.compileOk compiledHelper.presentInRuntime |
There was a problem hiding this comment.
In runtime contracts that contain two internal function definitions with the same generated helper name, findInternalFunction? returns the first match, but this proof only uses compiledHelper.presentInRuntime to prove that some match exists. The helper exported by this dispatch can therefore be a different same-name function than compiledHelper.compiledStmt, so a later theorem proving the summary for compiledHelper would not apply to the function actually executed here; please thread an exact/unique lookup invariant instead of only isSome.
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_c262341e-2c59-49e8-b8a5-d64faa7559e9) |
OpenCodeReview first-pass reviewStatus: scout_triage · Mode: large-lean-hotspots · 8 finding(s) · 6 files · 0 tokens · 0 tool calls Large Lean diff routed to bounded packet review: 8 Lean file(s), 980 changed supported line(s). Scout triage fallback_deterministic; 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
|
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e2393b9c77
ℹ️ 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".
|
|
||
| private theorem internalFunctionYulName_isYulLogName_false (name : String) : | ||
| /-- Compiler-generated internal function names cannot be Yul log builtins. -/ | ||
| theorem internalFunctionYulName_isYulLogName_false (name : String) : |
There was a problem hiding this comment.
Because this declaration is no longer private, the generated axiom-audit file needs to list it as a public theorem. In this commit PrintAxioms.lean still contains -- Compiler.Proofs.IRGeneration.internalFunctionYulName_isYulLogName_false -- private and the totals do not reflect the visibility change; I verified python3 scripts/generate_print_axioms.py --check exits with PrintAxioms.lean is out of date. Please regenerate PrintAxioms.lean after making this theorem public.
Useful? React with 👍 / 👎.
…er-bridge-slice # 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_d7a618af-0891-4df9-a365-472957ee0b58) |
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_8dba7ade-53ea-4dd4-9a3d-68fad41d8629) |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 37979a43d2
ℹ️ 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".
| (args := args) | ||
| (hbridge hmem)) | ||
|
|
||
| /-! |
There was a problem hiding this comment.
With this module comment inserted between stmtListDirectInternalHelperAssignStepInterfaceWithInternals_of_assignHeadStepBridgesWithInternals and the next declaration, scripts/check_proof_length.py strips the comment text but still counts its preserved lines as part of that previous theorem. Running python3 scripts/check_proof_length.py reports that theorem as 71 lines and exits non-zero, so CI will fail unless this block is moved outside the preceding proof span or the affected theorem is explicitly allowlisted.
Useful? React with 👍 / 👎.
|
@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_0a65f883-f432-42b8-9a8d-f87960a07eb5) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8fbcc8c2f1
ℹ️ 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".
| compiledHelper : | ||
| SupportedCompiledInternalHelperWitness spec runtimeContract calleeName |
There was a problem hiding this comment.
Please add an invariant tying compiledHelper.sourceWitness to sourceWitness (or make summarySound live on compiledHelper.sourceWitness). The constructor passes hHelpers.summaryOfCall to compiledOfCall, but SupportedRuntimeHelperTableInterface.compiledOfWitness is only typed to return some SupportedCompiledInternalHelperWitness spec runtimeContract calleeName, so it can legally choose a different witness/summary for the same calleeName. In that context the source evidence proves sourceWitness.summary.contract.post, while the IR dispatch executes the helper from compiledHelper, leaving the documented compiled-helper summary theorem unable to consume this package without an extra equality hypothesis.
Useful? React with 👍 / 👎.
![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: scout_triage · Mode: large-lean-hotspots · 5 finding(s) · 5 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 5 Lean file(s), 377 changed supported line(s). Scout model ranked 5/8 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 5 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-v9)
- Changed files: 6 supported / 6 total; Lean 5, trust docs 0, workflow/scripts 1, contracts 0, docs 0
- Changed lines: 377 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 5; files 5; tokens 0; tool calls 0; warnings 1; duration 41s
- Largest changed files: Compiler/Proofs/HelperStepProofs.lean (+254/-0), Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean (+101/-0), PrintAxioms.lean (+6/-2), scripts/check_proof_length.py (+6/-0), Compiler/Proofs/IRGeneration/SupportedSpec.lean (+5/-0)
Packet coverage
- Packet review: enabled; selected 5/8 packet(s)
- Scout: configured; status success; model reviewer_scout
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 5 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.9 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/HelperStepProofs.lean:588 score 74 — public declaration/signature changed; ask: Does the new
directInternalHelperStatementContextBridge_*machinery (lines 588-864) honestly thread through the existingcompiledStmtStepWithHelpersAndHelperIRWithInternals_internalCallAssign_of_assignHeadStepBridgeWithInternalshypotheses, or does it introduce a weakening step that bypasses some of the bridge hypotheses? In particular, verify that the new 'bounded N2/N3 bridge-instantiation slice' does not silently drop thespec,fields,scope, ornamesconstraints from the original - Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean:1611 score 69 — public declaration/signature changed; ask: Does
execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness_with_internalscorrectly close all cases ofirInternalFunctionDefOfStmt?(in particular rejecting builtins likesstore/mstore/revert/return/stopvia theinternalFunctionYulName_ne_*hypotheses), and does it reuse — not re-prove — thepresentInRuntime/uniqueInRuntimeevidence fromSupportedCompiledInternalHelperWitness? Also confirm thatcompileStmt fields [] [] .calldata [] false scope [] ...is c - Compiler/Proofs/IRGeneration/IRInterpreter.lean:5734 score 64 — public declaration/signature changed; ask: Is the
simpproof ofinternalFunctionYulName_isYulLogName_falseexhaustive over theisYulLogNamepredicate (i.e. it covers all string literals for whichisYulLogNamereturns true, not onlylog0..log4)? Confirm the list oflognames matches the canonical Yul log builtin set in the rest of the codebase, and that thedecidecalls used ininternalFunctionYulName_ne_logare actuallyDecidablefor the relevantStringequalities. - Compiler/Proofs/IRGeneration/SupportedSpec.lean:2630 score 30 — hotspot path/churn; ask: Which structure gained the
uniqueInRuntimefield, and have all existing constructors/witnesses in the repo been updated to provide a proof of it? Confirm the proof does not silently assume the conclusion (i.e. it is not closed byfun _ _ _ _ h => (by ...)that depends on the very property being added). Also verify the projectionirInternalFunctionDefOfStmt?is the one used by the dispatch theorems in pkt-2, so the new field is actually consumable there. - PrintAxioms.lean:6134 score 12 — hotspot path/churn; ask: Re-run the PrintAxioms regeneration from scratch and confirm (a) the public-count delta is exactly +4 corresponding to the four new public items in pkt-1/pkt-2/pkt-3, (b) the private-count delta is exactly -1 (the single demotion of
internalFunctionYulName_isYulLogName_false), and (c) nosorry/admittoken appears anywhere in the four new code regions (pkt-1 lines 588-864, pkt-2 lines 1611-1711, pkt-3 line 5734, pkt-4 lines 2630-2634).
- Compiler/Proofs/HelperStepProofs.lean:588 score 74 — public declaration/signature changed; ask: Does the new
Pilot mode: advisory only. Codex Review remains the merge gate.
| hctx.sourceWitness | ||
| hnodup | ||
| · simpa [result] using hctx.summarySound fuel state.world argVals | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 254 changed line(s) near Compiler/Proofs/HelperStepProofs.lean:588.
Risk signals: public declaration/signature changed.
Scout reason: Largest single addition (254 lines) introducing a new 'Direct statement helper context bridge' subsection in the core HelperStepProofs file, with public-declaration/signature changes. The diff begins a `section` block right after a delicate compiledStmtStepWithHelpersAndHelperIRWithInternals_internalCallAssign_of_assignHeadStepBridgeWithInternals call site (line 576-586), implying the new bridge slices into existing per-helper dispatch machinery. The wording 'bounded N2/N3 bridge-instantiation s
Question for stronger reviewer: Does the new `directInternalHelperStatementContextBridge_*` machinery (lines 588-864) honestly thread through the existing `compiledStmtStepWithHelpersAndHelperIRWithInternals_internalCallAssign_of_assignHeadStepBridgeWithInternals` hypotheses, or does it introduce a weakening step that bypasses some of the bridge hypotheses? In particular, verify that the new 'bounded N2/N3 bridge-instantiation slice' does not silently drop the `spec`, `fields`, `scope`, or `names` constraints from the original
Added-line sample:
- L588: section
- L589:
- L590: /-!
- L591: ### Direct statement helper context bridge
- L592:
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| (internalFunctionYulName_ne_revert calleeName) | ||
| (internalFunctionYulName_ne_return calleeName) | ||
| (internalFunctionYulName_isYulLogName_false calleeName) | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 101 changed line(s) near Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean:1611.
Risk signals: public declaration/signature changed.
Scout reason: Adds a new public theorem `execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness_with_internals` (101 lines) inside GenericInduction/Calls. The theorem takes a `SupportedCompiledInternalHelperWitness` and a `CompilationModel.compileStmt` hypothesis and produces an execution result; the body shown sets up `hargCompile` and references the suite of `internalFunctionYulName_ne_*` facts (stop/sstore/mstore/revert/return). This is exactly the kind of dispatch theorem that, if its `refin
Question for stronger reviewer: Does `execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness_with_internals` correctly close all cases of `irInternalFunctionDefOfStmt?` (in particular rejecting builtins like `sstore`/`mstore`/`revert`/`return`/`stop` via the `internalFunctionYulName_ne_*` hypotheses), and does it reuse — not re-prove — the `presentInRuntime` / `uniqueInRuntime` evidence from `SupportedCompiledInternalHelperWitness`? Also confirm that `compileStmt fields [] [] .calldata [] false scope [] ...` is c
Added-line sample:
- L1611: /-- Runtime-helper-table packaged dispatch for a direct helper return-binding
- L1612: compiled with the caller's internal-function environment. -/
- L1613: theorem execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness_with_internals
- L1614: {runtimeContract : IRContract} {spec : CompilationModel} {fields : List Field}
- L1615: {scope : List String} {names : List String} {calleeName : String} {args : List Expr}
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
|
||
| private theorem internalFunctionYulName_isYulLogName_false (name : String) : | ||
| /-- Compiler-generated internal function names cannot be Yul log builtins. -/ | ||
| theorem internalFunctionYulName_isYulLogName_false (name : String) : |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 3 changed line(s) near Compiler/Proofs/IRGeneration/IRInterpreter.lean:5734.
Risk signals: public declaration/signature changed.
Scout reason: Promotes the previously private theorem `internalFunctionYulName_isYulLogName_false` (IRInterpreter.lean:5734) to a public `theorem` with a docstring. This is a trust-boundary widening: the lemma now appears on the `PrintAxioms.lean` whitelist (pkt-7) and on the public axiom-list count, and downstream proof files are expected to be able to call it. Any weakness in its proof (it dispatches on `isYulLogName` and applies five `internalFunctionYulName_ne_log` facts) is now externally visible.
Question for stronger reviewer: Is the `simp` proof of `internalFunctionYulName_isYulLogName_false` exhaustive over the `isYulLogName` predicate (i.e. it covers all string literals for which `isYulLogName` returns true, not only `log0..log4`)? Confirm the list of `log` names matches the canonical Yul log builtin set in the rest of the codebase, and that the `decide` calls used in `internalFunctionYulName_ne_log` are actually `Decidable` for the relevant `String` equalities.
Added-line sample:
- L5734: /-- Compiler-generated internal function names cannot be Yul log builtins. -/
- L5735: theorem internalFunctionYulName_isYulLogName_false (name : String) :
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| ∀ stmt ∈ runtimeContract.internalFunctions, | ||
| ∀ p r b, irInternalFunctionDefOfStmt? stmt = | ||
| some ⟨CompilationModel.internalFunctionYulName calleeName, p, r, b⟩ → | ||
| stmt = compiledStmt |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 5 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:2630.
Risk signals: hotspot path/churn.
Scout reason: Adds a new field `uniqueInRuntime` to a structure (likely `SupportedCompiledInternalHelperWitness` or sibling, around line 2630 of SupportedSpec.lean) requiring that the only `stmt` in `runtimeContract.internalFunctions` matching `CompilationModel.internalFunctionYulName calleeName` is `compiledStmt`. This is a breaking change for any code that constructs the structure: every existing `⟨...⟩` will need the new proof, and any producer that silently relies on 'at most one such stmt' will fail to t
Question for stronger reviewer: Which structure gained the `uniqueInRuntime` field, and have all existing constructors/witnesses in the repo been updated to provide a proof of it? Confirm the proof does not silently assume the conclusion (i.e. it is not closed by `fun _ _ _ _ h => (by ...)` that depends on the very property being added). Also verify the projection `irInternalFunctionDefOfStmt?` is the one used by the dispatch theorems in pkt-2, so the new field is actually consumable there.
Added-line sample:
- L2630: uniqueInRuntime :
- L2631: ∀ stmt ∈ runtimeContract.internalFunctions,
- L2632: ∀ p r b, irInternalFunctionDefOfStmt? stmt =
- L2633: some ⟨CompilationModel.internalFunctionYulName calleeName, p, r, b⟩ →
- L2634: stmt = compiledStmt
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| ] | ||
|
|
||
| -- Total: 5745 theorems/lemmas (3983 public, 1762 private, 0 sorry'd) | ||
| -- Total: 5749 theorems/lemmas (3988 public, 1761 private, 0 sorry'd) |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 2 changed line(s) near PrintAxioms.lean:6134.
Risk signals: hotspot path/churn.
Scout reason: PrintAxioms.lean is regenerated and now reports 5749 theorems/lemmas (3988 public, 1761 private, 0 sorry'd) up from 5745. The '0 sorry'd' claim is load-bearing: a non-zero sorry count is the canonical soundness red flag. The +4 public count must correspond exactly to the four new public declarations introduced in this PR (the two new `*_with_internals` theorems, the new `directInternalHelperStatementContextBridge_*` pair, and the now-public `internalFunctionYulName_isYulLogName_false`). A mismat
Question for stronger reviewer: Re-run the PrintAxioms regeneration from scratch and confirm (a) the public-count delta is exactly +4 corresponding to the four new public items in pkt-1/pkt-2/pkt-3, (b) the private-count delta is exactly -1 (the single demotion of `internalFunctionYulName_isYulLogName_false`), and (c) no `sorry`/`admit` token appears anywhere in the four new code regions (pkt-1 lines 588-864, pkt-2 lines 1611-1711, pkt-3 line 5734, pkt-4 lines 2630-2634).
Added-line sample:
- L6134: -- Total: 5749 theorems/lemmas (3988 public, 1761 private, 0 sorry'd)
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
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.
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_ca5e8fac-94e7-4523-a343-c3e92a05a767) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 8 finding(s) · 5 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 5 Lean file(s), 382 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-v9)
- Changed files: 6 supported / 6 total; Lean 5, trust docs 0, workflow/scripts 1, contracts 0, docs 0
- Changed lines: 382 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 8; files 5; tokens 0; tool calls 0; warnings 1; duration 45s
- Largest changed files: Compiler/Proofs/HelperStepProofs.lean (+254/-0), Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean (+103/-0), Compiler/Proofs/IRGeneration/SupportedSpec.lean (+7/-1), PrintAxioms.lean (+6/-2), scripts/check_proof_length.py (+6/-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.9 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/HelperStepProofs.lean:588 score 74 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean:1611 score 69 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/IRInterpreter.lean:5734 score 64 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/SupportedSpec.lean:2 score 60 — changed imports
- Compiler/Proofs/IRGeneration/SupportedSpec.lean:2631 score 30 — hotspot path/churn
- Compiler/Proofs/IRGeneration/SupportedSpec.lean:4518 score 30 — hotspot path/churn
- PrintAxioms.lean:1848 score 12 — hotspot path/churn
- PrintAxioms.lean:2723 score 12 — hotspot path/churn
Pilot mode: advisory only. Codex Review remains the merge gate.
| hctx.sourceWitness | ||
| hnodup | ||
| · simpa [result] using hctx.summarySound fuel state.world argVals | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 254 changed line(s) near Compiler/Proofs/HelperStepProofs.lean:588.
Risk signals: public declaration/signature changed.
Added-line sample:
- L588: section
- L589:
- L590: /-!
- L591: ### Direct statement helper context bridge
- L592:
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| (internalFunctionYulName_ne_revert calleeName) | ||
| (internalFunctionYulName_ne_return calleeName) | ||
| (internalFunctionYulName_isYulLogName_false calleeName) | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 103 changed line(s) near Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean:1611.
Risk signals: public declaration/signature changed.
Added-line sample:
- L1611: /-- Runtime-helper-table packaged dispatch for a direct helper return-binding
- L1612: compiled with the caller's internal-function environment. -/
- L1613: theorem execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness_with_internals
- L1614: {runtimeContract : IRContract} {spec : CompilationModel} {fields : List Field}
- L1615: {scope : List String} {names : List String} {calleeName : String} {args : List Expr}
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
|
||
| private theorem internalFunctionYulName_isYulLogName_false (name : String) : | ||
| /-- Compiler-generated internal function names cannot be Yul log builtins. -/ | ||
| theorem internalFunctionYulName_isYulLogName_false (name : String) : |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 3 changed line(s) near Compiler/Proofs/IRGeneration/IRInterpreter.lean:5734.
Risk signals: public declaration/signature changed.
Added-line sample:
- L5734: /-- Compiler-generated internal function names cannot be Yul log builtins. -/
- L5735: theorem internalFunctionYulName_isYulLogName_false (name : String) :
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| @@ -1,4 +1,5 @@ | |||
| import Compiler.Proofs.IRGeneration.SupportedFragment | |||
| import Compiler.Proofs.IRGeneration.IRInterpreter | |||
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: changed imports; 1 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:2.
Risk signals: changed imports.
Added-line sample:
- L2: import Compiler.Proofs.IRGeneration.IRInterpreter
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| ∀ stmt ∈ runtimeContract.internalFunctions, | ||
| ∀ p r b, irInternalFunctionDefOfStmt? stmt = | ||
| some ⟨CompilationModel.internalFunctionYulName calleeName, p, r, b⟩ → | ||
| stmt = compiledStmt |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 5 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:2631.
Risk signals: hotspot path/churn.
Added-line sample:
- L2631: uniqueInRuntime :
- L2632: ∀ stmt ∈ runtimeContract.internalFunctions,
- L2633: ∀ p r b, irInternalFunctionDefOfStmt? stmt =
- L2634: some ⟨CompilationModel.internalFunctionYulName calleeName, p, r, b⟩ →
- L2635: stmt = compiledStmt
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| simp_wf | ||
| try simp [Stmt.ite.sizeOf_spec, Stmt.forEach.sizeOf_spec, List.cons.sizeOf_spec] at * | ||
| omega | ||
| try omega |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 2 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:4518.
Risk signals: hotspot path/churn.
Added-line sample:
- L4518: try omega
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| Compiler.Proofs.HelperStepProofs.stmtListDirectInternalHelperAssignStepInterfaceWithInternals_of_assignHeadStepBridgesWithInternals | ||
| Compiler.Proofs.HelperStepProofs.stmtListDirectInternalHelperAssignStepInterface_of_perCalleeAssignBridgeCatalog | ||
| Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceCallEvidence | ||
| Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceAssignEvidence |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 2 changed line(s) near PrintAxioms.lean:1848.
Risk signals: hotspot path/churn.
Added-line sample:
- L1848: Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceCallEvidence
- L1849: Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceAssignEvidence
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| Compiler.Proofs.IRGeneration.execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness | ||
| Compiler.Proofs.IRGeneration.execIRStmtsWithInternals_of_internalCall_compiledHelperWitness | ||
| Compiler.Proofs.IRGeneration.execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness_with_internals | ||
| Compiler.Proofs.IRGeneration.execIRStmtsWithInternals_of_internalCall_compiledHelperWitness_with_internals |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 2 changed line(s) near PrintAxioms.lean:2723.
Risk signals: hotspot path/churn.
Added-line sample:
- L2723: Compiler.Proofs.IRGeneration.execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness_with_internals
- L2724: Compiler.Proofs.IRGeneration.execIRStmtsWithInternals_of_internalCall_compiledHelperWitness_with_internals
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
@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". |
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_dbcb8408-549c-4e2a-bdab-b6d963307e47) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 8 finding(s) · 5 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 5 Lean file(s), 429 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.
✅ 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-v9)
- Changed files: 6 supported / 6 total; Lean 5, trust docs 0, workflow/scripts 1, contracts 0, docs 0
- Changed lines: 429 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 8; files 5; tokens 0; tool calls 0; warnings 1; duration 36s
- Largest changed files: Compiler/Proofs/HelperStepProofs.lean (+278/-0), Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean (+103/-0), Compiler/Proofs/IRGeneration/SupportedSpec.lean (+28/-1), PrintAxioms.lean (+8/-2), scripts/check_proof_length.py (+6/-0)
Packet coverage
- Packet review: enabled; selected 8/8 packet(s)
- Scout: configured; status success; model reviewer_scout
- Strong review: required; status blocked_packet_input
- Residual risk: Triaged top 8 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.9 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/SupportedSpec.lean:4539 score 30 — hotspot path/churn; ask: Under what concrete goal shapes does the original
omegasucceed buttry omegacould fail silently? Does the surroundingsimp_wfguarantee that any remaining subgoal is arithmetically decidable, or could thetrymask a regression in the well-foundedness proof ofstmtOrListTouchesUnsupportedCallSurface_eq_featureOr? - Compiler/Proofs/HelperStepProofs.lean:588 score 74 — public declaration/signature changed; ask: Read the full new
section(lines 588–~880). Are all three newdirectInternalHelperStatementContextBridge_*theorems justified fromSupportedBodyHelperInterface/SupportedBodyHelperSummariesSound/SupportedRuntimeHelperTableInterfacewithoutsorry/admit, and are their statement types exactly what PrintAxioms (pkt-8) advertises? - Compiler/Proofs/IRGeneration/SupportedSpec.lean:2631 score 30 — hotspot path/churn; ask: List every constructor/intro site for
SupportedCompiledInternalHelperWitness(in particularcompiledOfCallin pkt-3 and the helper registry around lines 4280–4290). Verify each one supplies a realuniqueInRuntimeproof, notadmitor auto-derived tautology. Also verifyuniqueInRuntimeis provable in general, i.e. that compiler-generated internal functions have uniquecompiledStmts inruntimeContract.internalFunctions. - Compiler/Proofs/IRGeneration/SupportedSpec.lean:4291 score 64 — public declaration/signature changed; ask: Does
compiledOfCall_sourceWitnessclose byrfl/definitional equality, or does it require a non-trivial path viacompiledOfWitness? Confirm the proof body and rule out hidden dependence onClassical.choiceorQuot.sound. - Compiler/Proofs/IRGeneration/SupportedSpec.lean:2 score 60 — changed imports; ask: Confirm the import graph remains acyclic (SupportedSpec → IRInterpreter → … not back into SupportedSpec/GenericInduction) and that no new axioms from IRInterpreter are pulled into the supported-spec trust surface.
- Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean:1611 score 69 — public declaration/signature changed; ask: Walk the new theorem’s proof: does the
hcompile/argExprs/hargCompilehypothesis bundle correctly tie the compiled IR tocompiledHelper, and is the dispatch step free of circular reasoning with thecompiledOfCall/compiledOfCall_sourceWitnessinterface? - Compiler/Proofs/IRGeneration/IRInterpreter.lean:5734 score 64 — public declaration/signature changed; ask: Diff-check that only the
privatemodifier was removed; the statement and proof must be byte-identical. Grep for any priorprivatesibling with the same name in IRInterpreter that would now collide. - PrintAxioms.lean:1848 score 12 — hotspot path/churn; ask: Confirm the three new PrintAxioms entries exactly match the fully-qualified theorem names declared in HelperStepProofs.lean lines 588–~880; no typos, no missing parameters.
- Compiler/Proofs/IRGeneration/SupportedSpec.lean:4539 score 30 — hotspot path/churn; ask: Under what concrete goal shapes does the original
Pilot mode: advisory only. Codex Review remains the merge gate.
| simp_wf | ||
| try simp [Stmt.ite.sizeOf_spec, Stmt.forEach.sizeOf_spec, List.cons.sizeOf_spec] at * | ||
| omega | ||
| try omega |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 2 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:4539.
Risk signals: hotspot path/churn.
Scout reason: Direct proof-strength regression: `omega` is replaced by `try omega` inside a `decreasing_by` decreasing-trasure block. `try` silently swallows failure, so a goal that previously closed can now pass as ‘true by default’ without actually being discharged. This is the clearest trust-boundary/theorem-weakening signal in the diff.
Question for stronger reviewer: Under what concrete goal shapes does the original `omega` succeed but `try omega` could fail silently? Does the surrounding `simp_wf` guarantee that any remaining subgoal is arithmetically decidable, or could the `try` mask a regression in the well-foundedness proof of `stmtOrListTouchesUnsupportedCallSurface_eq_featureOr`?
Added-line sample:
- L4539: try omega
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| hctx.sourceWitness | ||
| hnodup | ||
| · simpa [result] using hctx.summarySound fuel state.world argVals | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 278 changed line(s) near Compiler/Proofs/HelperStepProofs.lean:588.
Risk signals: public declaration/signature changed.
Scout reason: Largest churn packet: 278 added lines in a single hunk of HelperStepProofs.lean, plus a new `section` introducing three new public declarations (`directInternalHelperStatementContextBridge_*`) referenced from PrintAxioms. Public-signature expansion of the core helper-step bridge file is a structural change that downstream step proofs and the PrintAxioms trust surface depend on.
Question for stronger reviewer: Read the full new `section` (lines 588–~880). Are all three new `directInternalHelperStatementContextBridge_*` theorems justified from `SupportedBodyHelperInterface`/`SupportedBodyHelperSummariesSound`/`SupportedRuntimeHelperTableInterface` without `sorry`/`admit`, and are their statement types exactly what PrintAxioms (pkt-8) advertises?
Added-line sample:
- L588: section
- L589:
- L590: /-!
- L591: ### Direct statement helper context bridge
- L592:
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| be paired with a compiled helper it does not describe. -/ | ||
| compiledOfWitness_sourceWitness : | ||
| ∀ calleeName (witness : SupportedInternalHelperWitness spec calleeName), | ||
| (compiledOfWitness calleeName witness).sourceWitness = witness |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 12 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:2631.
Risk signals: hotspot path/churn.
Scout reason: Hotspot payload that materially alters a structure: a new field `uniqueInRuntime` is added to `SupportedCompiledInternalHelperWitness`, changing its arity. Every existing constructor/inhabitant site and every subsequent lemma that pattern-matches the structure must be updated; if any call site is missed, the whole downstream `SupportedRuntimeHelperTableInterface` machinery can become vacuous or unsound.
Question for stronger reviewer: List every constructor/intro site for `SupportedCompiledInternalHelperWitness` (in particular `compiledOfCall` in pkt-3 and the helper registry around lines 4280–4290). Verify each one supplies a real `uniqueInRuntime` proof, not `admit` or auto-derived tautology. Also verify `uniqueInRuntime` is provable in general, i.e. that compiler-generated internal functions have unique `compiledStmt`s in `runtimeContract.internalFunctions`.
Added-line sample:
- L2631: uniqueInRuntime :
- L2632: ∀ stmt ∈ runtimeContract.internalFunctions,
- L2633: ∀ p r b, irInternalFunctionDefOfStmt? stmt =
- L2634: some ⟨CompilationModel.internalFunctionYulName calleeName, p, r, b⟩ →
- L2635: stmt = compiledStmt
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| (hmem : calleeName ∈ helperCallNames fn) : | ||
| (hRuntime.compiledOfCall hHelpers hmem).sourceWitness = hHelpers.summaryOfCall hmem := | ||
| hRuntime.compiledOfWitness_sourceWitness calleeName (hHelpers.summaryOfCall hmem) | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 14 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:4291.
Risk signals: public declaration/signature changed.
Scout reason: New public equality theorem `compiledOfCall_sourceWitness` equating `(hRuntime.compiledOfCall hHelpers hmem).sourceWitness` with `hHelpers.summaryOfCall hmem`. This is the trust boundary between the runtime-side compiled-witness and the body-side summary; if the equality is only provable by rewriting/cast abuse, downstream ‘source semantics matches compiled’ arguments become unsound.
Question for stronger reviewer: Does `compiledOfCall_sourceWitness` close by `rfl`/definitional equality, or does it require a non-trivial path via `compiledOfWitness`? Confirm the proof body and rule out hidden dependence on `Classical.choice` or ` Quot.sound`.
Added-line sample:
- L4291: /-- The compiled helper produced by `compiledOfCall` carries exactly the source
- L4292: witness inventoried for that call, so a source summary proof about
- L4293: `hHelpers.summaryOfCall hmem` is a proof about `compiledHelper.sourceWitness`. -/
- L4294: theorem SupportedRuntimeHelperTableInterface.compiledOfCall_sourceWitness
- L4295: {spec : CompilationModel}
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| @@ -1,4 +1,5 @@ | |||
| import Compiler.Proofs.IRGeneration.SupportedFragment | |||
| import Compiler.Proofs.IRGeneration.IRInterpreter | |||
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: changed imports; 1 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:2.
Risk signals: changed imports.
Scout reason: Module-dependency change: SupportedSpec.lean now imports `Compiler.Proofs.IRGeneration.IRInterpreter`, while IRInterpreter.lean already sits in the dependency chain used by GenericInduction/Calls (pkt-2). This can introduce an import cycle or new transitively-leaked `private → public` visibility (cf. pkt-4).
Question for stronger reviewer: Confirm the import graph remains acyclic (SupportedSpec → IRInterpreter → … not back into SupportedSpec/GenericInduction) and that no new axioms from IRInterpreter are pulled into the supported-spec trust surface.
Added-line sample:
- L2: import Compiler.Proofs.IRGeneration.IRInterpreter
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| (internalFunctionYulName_ne_revert calleeName) | ||
| (internalFunctionYulName_ne_return calleeName) | ||
| (internalFunctionYulName_isYulLogName_false calleeName) | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 103 changed line(s) near Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean:1611.
Risk signals: public declaration/signature changed.
Scout reason: Large new public theorem (`execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness_with_internals`, 103 added lines) extending the GenericInduction dispatch proof with a witness-packaged variant. The expanded arity and dispatch via `compiledOfCall` (pkt-3/pkt-6) make it sensitive to the new structure field and the new equality.
Question for stronger reviewer: Walk the new theorem’s proof: does the `hcompile`/`argExprs`/`hargCompile` hypothesis bundle correctly tie the compiled IR to `compiledHelper`, and is the dispatch step free of circular reasoning with the `compiledOfCall`/`compiledOfCall_sourceWitness` interface?
Added-line sample:
- L1611: /-- Runtime-helper-table packaged dispatch for a direct helper return-binding
- L1612: compiled with the caller's internal-function environment. -/
- L1613: theorem execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness_with_internals
- L1614: {runtimeContract : IRContract} {spec : CompilationModel} {fields : List Field}
- L1615: {scope : List String} {names : List String} {calleeName : String} {args : List Expr}
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
|
||
| private theorem internalFunctionYulName_isYulLogName_false (name : String) : | ||
| /-- Compiler-generated internal function names cannot be Yul log builtins. -/ | ||
| theorem internalFunctionYulName_isYulLogName_false (name : String) : |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 3 changed line(s) near Compiler/Proofs/IRGeneration/IRInterpreter.lean:5734.
Risk signals: public declaration/signature changed.
Scout reason: Visibility promotion: `internalFunctionYulName_isYulLogName_false` is changed from `private theorem` to public `theorem`. Combined with the new public helper-witness machinery (pkt-1/pkt-3), this enlarges the trusted theory by exposing a previously encapsulated fact; reviewers should confirm the lemma statement is unchanged and that no downstream code was shadowing it.
Question for stronger reviewer: Diff-check that only the `private` modifier was removed; the statement and proof must be byte-identical. Grep for any prior `private` sibling with the same name in IRInterpreter that would now collide.
Added-line sample:
- L5734: /-- Compiler-generated internal function names cannot be Yul log builtins. -/
- L5735: theorem internalFunctionYulName_isYulLogName_false (name : String) :
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| Compiler.Proofs.HelperStepProofs.stmtListDirectInternalHelperAssignStepInterface_of_perCalleeAssignBridgeCatalog | ||
| Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_summarySound_compiledHelper | ||
| Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceCallEvidence | ||
| Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceAssignEvidence |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 3 changed line(s) near PrintAxioms.lean:1848.
Risk signals: hotspot path/churn.
Scout reason: PrintAxioms.lean additions are mechanically driven by pkt-1 (the three new `directInternalHelperStatementContextBridge_*` theorems). Auto-generated audit file — only dangerous if pkt-1’s names/types are wrong, but worth a transitive check.
Question for stronger reviewer: Confirm the three new PrintAxioms entries exactly match the fully-qualified theorem names declared in HelperStepProofs.lean lines 588–~880; no typos, no missing parameters.
Added-line sample:
- L1848: Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_summarySound_compiledHelper
- L1849: Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceCallEvidence
- L1850: Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceAssignEvidence
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 45f47670dd
ℹ️ 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".
| (hcompile : CompilationModel.compileStmt fields [] [] .calldata [] false scope [] | ||
| (Stmt.internalCallAssign names calleeName args) spec.functions = Except.ok compiledIR) |
There was a problem hiding this comment.
For the intended WithInternals bridge assembly, the compile hypothesis comes from DirectInternalHelper*HeadStepBridgeWithInternals, whose compile/bridge fields use compileStmt fields spec.events spec.errors ... spec.functions (see this file around lines 493-499 and 528-534). This new dispatch theorem instead requires the same statement to have been compiled with empty event/error catalogs, so downstream code cannot apply the packaged dispatch directly to the existing WithInternals compile hypothesis without adding a separate erasure conversion; specs carrying events or custom errors hit this mismatch even though internal-call compilation itself is catalog-independent. The call variant below and the context bridge fields have the same shape.
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_9c00037f-b2b5-4be3-8f23-053ec5b96e95) |
|
@codex review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 8 finding(s) · 5 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 5 Lean file(s), 429 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-v9)
- Changed files: 6 supported / 6 total; Lean 5, trust docs 0, workflow/scripts 1, contracts 0, docs 0
- Changed lines: 429 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 8; files 5; tokens 0; tool calls 0; warnings 1; duration 45s
- Largest changed files: Compiler/Proofs/HelperStepProofs.lean (+278/-0), Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean (+103/-0), Compiler/Proofs/IRGeneration/SupportedSpec.lean (+28/-1), PrintAxioms.lean (+8/-2), scripts/check_proof_length.py (+6/-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.9 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/HelperStepProofs.lean:588 score 74 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean:1611 score 69 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/SupportedSpec.lean:4291 score 64 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/IRInterpreter.lean:5734 score 64 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/SupportedSpec.lean:2 score 60 — changed imports
- Compiler/Proofs/IRGeneration/SupportedSpec.lean:2631 score 30 — hotspot path/churn
- Compiler/Proofs/IRGeneration/SupportedSpec.lean:4539 score 30 — hotspot path/churn
- PrintAxioms.lean:1848 score 12 — hotspot path/churn
Pilot mode: advisory only. Codex Review remains the merge gate.
| hctx.sourceWitness | ||
| hnodup | ||
| · simpa [result] using hctx.summarySound fuel state.world argVals | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 278 changed line(s) near Compiler/Proofs/HelperStepProofs.lean:588.
Risk signals: public declaration/signature changed.
Added-line sample:
- L588: section
- L589:
- L590: /-!
- L591: ### Direct statement helper context bridge
- L592:
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| (internalFunctionYulName_ne_revert calleeName) | ||
| (internalFunctionYulName_ne_return calleeName) | ||
| (internalFunctionYulName_isYulLogName_false calleeName) | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 103 changed line(s) near Compiler/Proofs/IRGeneration/GenericInduction/Calls.lean:1611.
Risk signals: public declaration/signature changed.
Added-line sample:
- L1611: /-- Runtime-helper-table packaged dispatch for a direct helper return-binding
- L1612: compiled with the caller's internal-function environment. -/
- L1613: theorem execIRStmtsWithInternals_of_internalCallAssign_compiledHelperWitness_with_internals
- L1614: {runtimeContract : IRContract} {spec : CompilationModel} {fields : List Field}
- L1615: {scope : List String} {names : List String} {calleeName : String} {args : List Expr}
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| (hmem : calleeName ∈ helperCallNames fn) : | ||
| (hRuntime.compiledOfCall hHelpers hmem).sourceWitness = hHelpers.summaryOfCall hmem := | ||
| hRuntime.compiledOfWitness_sourceWitness calleeName (hHelpers.summaryOfCall hmem) | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 14 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:4291.
Risk signals: public declaration/signature changed.
Added-line sample:
- L4291: /-- The compiled helper produced by `compiledOfCall` carries exactly the source
- L4292: witness inventoried for that call, so a source summary proof about
- L4293: `hHelpers.summaryOfCall hmem` is a proof about `compiledHelper.sourceWitness`. -/
- L4294: theorem SupportedRuntimeHelperTableInterface.compiledOfCall_sourceWitness
- L4295: {spec : CompilationModel}
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
|
||
| private theorem internalFunctionYulName_isYulLogName_false (name : String) : | ||
| /-- Compiler-generated internal function names cannot be Yul log builtins. -/ | ||
| theorem internalFunctionYulName_isYulLogName_false (name : String) : |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 3 changed line(s) near Compiler/Proofs/IRGeneration/IRInterpreter.lean:5734.
Risk signals: public declaration/signature changed.
Added-line sample:
- L5734: /-- Compiler-generated internal function names cannot be Yul log builtins. -/
- L5735: theorem internalFunctionYulName_isYulLogName_false (name : String) :
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| @@ -1,4 +1,5 @@ | |||
| import Compiler.Proofs.IRGeneration.SupportedFragment | |||
| import Compiler.Proofs.IRGeneration.IRInterpreter | |||
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: changed imports; 1 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:2.
Risk signals: changed imports.
Added-line sample:
- L2: import Compiler.Proofs.IRGeneration.IRInterpreter
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| be paired with a compiled helper it does not describe. -/ | ||
| compiledOfWitness_sourceWitness : | ||
| ∀ calleeName (witness : SupportedInternalHelperWitness spec calleeName), | ||
| (compiledOfWitness calleeName witness).sourceWitness = witness |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 12 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:2631.
Risk signals: hotspot path/churn.
Added-line sample:
- L2631: uniqueInRuntime :
- L2632: ∀ stmt ∈ runtimeContract.internalFunctions,
- L2633: ∀ p r b, irInternalFunctionDefOfStmt? stmt =
- L2634: some ⟨CompilationModel.internalFunctionYulName calleeName, p, r, b⟩ →
- L2635: stmt = compiledStmt
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| simp_wf | ||
| try simp [Stmt.ite.sizeOf_spec, Stmt.forEach.sizeOf_spec, List.cons.sizeOf_spec] at * | ||
| omega | ||
| try omega |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 2 changed line(s) near Compiler/Proofs/IRGeneration/SupportedSpec.lean:4539.
Risk signals: hotspot path/churn.
Added-line sample:
- L4539: try omega
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| Compiler.Proofs.HelperStepProofs.stmtListDirectInternalHelperAssignStepInterface_of_perCalleeAssignBridgeCatalog | ||
| Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_summarySound_compiledHelper | ||
| Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceCallEvidence | ||
| Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceAssignEvidence |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 3 changed line(s) near PrintAxioms.lean:1848.
Risk signals: hotspot path/churn.
Added-line sample:
- L1848: Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_summarySound_compiledHelper
- L1849: Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceCallEvidence
- L1850: Compiler.Proofs.HelperStepProofs.directInternalHelperStatementContextBridge_sourceAssignEvidence
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
@codex review |
|
Codex Review: Didn't find any major issues. Keep them coming! 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
Compiler/Proofs/HelperStepProofs.leanSupportedBodyHelperInterface,SupportedBodyHelperSummariesSound, andSupportedRuntimeHelperTableInterfaceValidation
git diff --checklean-slot lake build Compiler.Proofs.HelperStepProofssorry/axiom/admitdiff scanNotes
helperSurfaceClosedfor the new helper obligations.PrintAxioms.leanartifacts changed.Note
Medium Risk
Changes are proof-only but touch core helper-step and IR dispatch seams; incorrect witness pairing laws or dispatch lemmas could undermine later correctness arguments without affecting runtime code paths.
Overview
Adds
DirectInternalHelperStatementContextBridgeinHelperStepProofs.leanto bundle source helper witnesses, summary soundness, compiled-helper table facts, and IR dispatch for directinternalCall/internalCallAssign, withdirectInternalHelperStatementContextBridge_of_supportedEvidencewiring it fromSupportedBodyHelperInterface,SupportedBodyHelperSummariesSound, andSupportedRuntimeHelperTableInterface. New lemmas expose source-side exec and summary evidence; module docs state the remaining gap (execIRInternalFunctionWithInternals_obeys_internal_helper_summary) before building the existing direct head-step bridge catalog.IR generation gains
execIRStmtsWithInternals_of_internalCall*_compiledHelperWitness_with_internalsinCalls.lean(callerspec.functionsenvironment).SupportedCompiledInternalHelperWitnesspicks upuniqueInRuntime;SupportedRuntimeHelperTableInterfaceaddscompiledOfWitness_sourceWitnessandcompiledOfCall_sourceWitnessso source summaries cannot be paired with unrelated compiled helpers.internalFunctionYulName_isYulLogName_falseis exported;PrintAxioms.leanand proof-length allowlist entries track the new lemmas.Reviewed by Cursor Bugbot for commit 645ac34. Bugbot is set up for automated code reviews on this repo. Configure here.