proof: model typed errors and bridge requireError/revertError#2164
proof: model typed errors and bridge requireError/revertError#2164Th0rgal wants to merge 8 commits into
Conversation
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_a3f5adae-47d6-462c-be94-3951f7ba5d38) |
OpenCodeReview first-pass reviewStatus: scout_triage · Mode: large-lean-hotspots · 8 finding(s) · 7 files · 0 tokens · 0 tool calls Large Lean diff routed to bounded packet review: 8 Lean file(s), 1716 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
|
![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: 56b415854f
ℹ️ 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".
# 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_12908cbd-8e59-461d-bc6a-4dfad50147de) |
| \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``` |
![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 · 6 finding(s) · 4 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 4 Lean file(s), 245 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: 245 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 32s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.lean (+195/-0), Compiler/Proofs/IRGeneration/SourceSemantics.lean (+38/-2), PrintAxioms.lean (+8/-1), Compiler/Proofs/IRGeneration/GenericInduction.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/GenericInduction/ErrorRevert.lean:1 score 103 — public declaration/signature changed, changed imports; ask: Is the universal
∀ state fuel, ∃ next, execIRStmts fuel state revertStmts = .revert nextpremise feasible to discharge for the actual generated Yul bodies in the codegen? If the premise is unreachable for any realrevertStmts, does the lemma silently become a vacuous truth that papers over a non-equivalence between sourcerequireErrorand the compiledif_ failCond revertStmts? ArehelperFuel/extraFuelaccounted for on both sides — the IR side uses an extra+ extraFuel + 1shell, bu - Compiler/Proofs/IRGeneration/SourceSemantics.lean:2254 score 64 — public declaration/signature changed; ask: Is the discard of
evalExprListsound? Specifically: (a) argument evaluation may itself revert or consume gas — does the catch-all| _ => .revertcorrectly distinguish 'arg eval succeeded with non-empty list' from 'arg eval produced no values' / 'arg eval failed'? (b) Does callingevalExprListhere, while.require(line 3937) usesevalExprWithHelpers, create a divergence that downstreamStmtResult/IRResultrefinement will have to thread back? (c) Is there a TODO marker or migration - Compiler/Proofs/IRGeneration/SourceSemantics.lean:2486 score 30 — hotspot path/churn; ask: Confirm that
requireError's condition is provably helper-free (soevalExprvsevalExprWithHelpersis intentional). Confirm that the.revertErrorpath never needs to act on theerrorNameat this abstraction level. If packets 5, 6, 7 are three differentexecStmtvariants, verify all three use the same helper surface — does theevalExpr(no helpers) choice hold for each call site? - Compiler/Proofs/IRGeneration/SourceSemantics.lean:5473 score 30 — hotspot path/churn; ask: Does the new
simpactually close, or is it leaving a residual goal that the lossytypedErrorRevertResultdefinition will silently absorb? If the lemma previously proved a richer equality (e.g., carried some error-payload info), is there a regression? Is there a separate proof obligation stating thatevalExprListproduces a returndata that survives — or is that contract purely deferred? - Compiler/Proofs/IRGeneration/GenericInduction.lean:1 score 60 — changed imports; ask: Does any other module under
Compiler/Proofs/IRGeneration/indirectly import this and then re-export thecompiledStmtStep_requireError_revert_casetheorem (visibility being the only thing keeping it contained)? Trace the import graph one hop beyondGenericInduction.lean. - PrintAxioms.lean:58 score 42 — changed imports; ask: Run the project's
PrintAxiomstarget before and after the PR and diff the output. Any newaxiom/sorryintroduced by the newErrorRevertmodule would appear here. Also: does the new module introducenoncomputabledefs,classical,Decidable, orexternthat could shift the axiom inventory even if noaxiomkeyword is used?
- Compiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.lean:1 score 103 — public declaration/signature changed, changed imports; ask: Is the universal
Pilot mode: advisory only. Codex Review remains the merge gate.
|
Gating update for
Blocking merge: GitHub Verify proofs is not green. The rerun of |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ad0ae379ce
ℹ️ 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".
| if resolved != 0 then .continue state else .revert | ||
| | none => .revert | ||
| | .requireError cond _ args => | ||
| match evalExpr fields state cond with |
There was a problem hiding this comment.
In execStmtWithHelpers, this new arm falls back to the plain evalExpr for the condition. When a requireError condition contains an Expr.internalCall (the supported-spec helper collectors include this case) and that helper returns a nonzero word, evalExpr treats the expression as unsupported and returns none, so the source semantics reverts even though the helper-aware compiled execution evaluates the helper and skips the revert block. This makes the helper-aware source/IR relation wrong for valid helper-backed requireError guards; use evalExprWithHelpers spec fields fuel state cond here.
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_fa093854-9718-44ef-9397-1db3a8b9a62f) |
OpenCodeReview first-pass reviewStatus: scout_triage · Mode: large-lean-hotspots · 8 finding(s) · 5 files · 0 tokens · 0 tool calls Large Lean diff routed to bounded packet review: 8 Lean file(s), 314 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
|
…ed-error-semantics # Conflicts: # PrintAxioms.lean
|
@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_9a4dfbf3-6ffc-48d3-9046-fff684dc13be) |
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_33420d74-6f60-4aa5-bac4-95e3d2a86384) |
|
@codex review |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 350b871045
ℹ️ 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".
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: 7 Lean file(s), 267 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: 7 supported / 7 total; Lean 7, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 267 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/GenericInduction/ErrorRevert.lean (+195/-0), Compiler/Proofs/IRGeneration/SourceSemantics.lean (+40/-2), Verity/Core/Model/Denote.lean (+12/-0), PrintAxioms.lean (+8/-1), Compiler/Proofs/IRGeneration/DenoteAgreement.lean (+2/-2)
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/GenericInduction/ErrorRevert.lean:1 score 103 — public declaration/signature changed, changed imports
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:2254 score 64 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/GenericInduction.lean:1 score 60 — changed imports
- PrintAxioms.lean:58 score 42 — changed imports
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:5473 score 30 — hotspot path/churn
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:2486 score 30 — hotspot path/churn
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:2769 score 30 — hotspot path/churn
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:3942 score 30 — hotspot path/churn
Pilot mode: advisory only. Codex Review remains the merge gate.
| refine ⟨.revert, .revert revState, hSrcExec, hrev, ?_⟩ | ||
| simp [stmtStepMatchesIRExec] | ||
|
|
||
| end Compiler.Proofs.IRGeneration |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · high]
Large Lean packet selected for stronger review: public declaration/signature changed, changed imports; 195 changed line(s) near Compiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.lean:1.
Risk signals: public declaration/signature changed, changed imports.
Added-line sample:
- L1: import Compiler.Proofs.IRGeneration.GenericInduction.ExprStmt
- L2:
- L3: set_option linter.unnecessarySeqFocus false
- L4: set_option linter.unnecessarySimpa false
- L5: set_option linter.unusedSimpArgs false
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| StmtResult := | ||
| match evalExprList fields state args with | ||
| | _ => .revert | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 13 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2254.
Risk signals: public declaration/signature changed.
Added-line sample:
- L2254: /-- Source-level custom-error revert at the current observable granularity.
- L2255:
- L2256: `StmtResult` does not yet carry returndata, so the ABI selector and encoded
- L2257: typed payload produced by compiled Yul are intentionally not observable here.
- L2258: That richer payload relation is deferred to the planned `StmtResult`/`IRResult`
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| @@ -1 +1,2 @@ | |||
| import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert | |||
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/GenericInduction.lean:1.
Risk signals: changed imports.
Added-line sample:
- L1: import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| import Compiler.Proofs.IRGeneration.FunctionShape | ||
| import Compiler.Proofs.IRGeneration.GenericInduction.Calls | ||
| import Compiler.Proofs.IRGeneration.GenericInduction.DenoteSound | ||
| import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: changed imports; 1 changed line(s) near PrintAxioms.lean:58.
Risk signals: changed imports.
Added-line sample:
- L58: import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult, | ||
| evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state cond hsurface] | ||
| | .revertError _ args => | ||
| simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult] |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 8 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:5473.
Risk signals: hotspot path/churn.
Added-line sample:
- L5473: | .requireError cond _ args =>
- L5474: simp only [stmtTouchesUnsupportedHelperSurface] at hsurface
- L5475: simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult,
- L5476: evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state cond hsurface]
- L5477: | .revertError _ args =>
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| if resolved != 0 then .continue state else typedErrorRevertResult fields state args | ||
| | none => .revert | ||
| | state, .revertError _ args => | ||
| typedErrorRevertResult fields state args |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 7 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2486.
Risk signals: hotspot path/churn.
Added-line sample:
- L2486: | state, .requireError cond _ args =>
- L2487: match evalExpr fields state cond with
- L2488: | some resolved =>
- L2489: if resolved != 0 then .continue state else typedErrorRevertResult fields state args
- L2490: | none => .revert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| if resolved != 0 then .continue state else typedErrorRevertResult fields state args | ||
| | none => .revert | ||
| | state, .revertError _ args => | ||
| typedErrorRevertResult fields state args |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 7 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2769.
Risk signals: hotspot path/churn.
Added-line sample:
- L2769: | state, .requireError cond _ args =>
- L2770: match evalExpr fields state cond with
- L2771: | some resolved =>
- L2772: if resolved != 0 then .continue state else typedErrorRevertResult fields state args
- L2773: | none => .revert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| if resolved != 0 then .continue state else typedErrorRevertResult fields state args | ||
| | none => .revert | ||
| | .revertError _ args => | ||
| typedErrorRevertResult fields state args |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 7 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:3942.
Risk signals: hotspot path/churn.
Added-line sample:
- L3942: | .requireError cond _ args =>
- L3943: match evalExprWithHelpers spec fields fuel state cond with
- L3944: | some resolved =>
- L3945: if resolved != 0 then .continue state else typedErrorRevertResult fields state args
- L3946: | none => .revert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
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_d4c0a78f-a488-406f-8c3d-4cc8512e6686) |
|
@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: 8 Lean file(s), 285 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: 8 supported / 8 total; Lean 8, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 285 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/IRGeneration/GenericInduction/ErrorRevert.lean (+195/-0), Compiler/Proofs/IRGeneration/SourceSemantics.lean (+40/-2), Compiler/Proofs/IRGeneration/SourceSemanticsFeatureTest.lean (+18/-0), Verity/Core/Model/Denote.lean (+12/-0), PrintAxioms.lean (+8/-1)
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/GenericInduction/ErrorRevert.lean:1 score 103 — public declaration/signature changed, changed imports
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:2254 score 64 — public declaration/signature changed
- Compiler/Proofs/IRGeneration/GenericInduction.lean:1 score 60 — changed imports
- PrintAxioms.lean:58 score 42 — changed imports
- Compiler/Proofs/IRGeneration/SourceSemanticsFeatureTest.lean:284 score 30 — hotspot path/churn
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:5473 score 30 — hotspot path/churn
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:2486 score 30 — hotspot path/churn
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:2769 score 30 — hotspot path/churn
Pilot mode: advisory only. Codex Review remains the merge gate.
| refine ⟨.revert, .revert revState, hSrcExec, hrev, ?_⟩ | ||
| simp [stmtStepMatchesIRExec] | ||
|
|
||
| end Compiler.Proofs.IRGeneration |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · high]
Large Lean packet selected for stronger review: public declaration/signature changed, changed imports; 195 changed line(s) near Compiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.lean:1.
Risk signals: public declaration/signature changed, changed imports.
Added-line sample:
- L1: import Compiler.Proofs.IRGeneration.GenericInduction.ExprStmt
- L2:
- L3: set_option linter.unnecessarySeqFocus false
- L4: set_option linter.unnecessarySimpa false
- L5: set_option linter.unusedSimpArgs false
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| StmtResult := | ||
| match evalExprList fields state args with | ||
| | _ => .revert | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 13 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2254.
Risk signals: public declaration/signature changed.
Added-line sample:
- L2254: /-- Source-level custom-error revert at the current observable granularity.
- L2255:
- L2256: `StmtResult` does not yet carry returndata, so the ABI selector and encoded
- L2257: typed payload produced by compiled Yul are intentionally not observable here.
- L2258: That richer payload relation is deferred to the planned `StmtResult`/`IRResult`
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| @@ -1 +1,2 @@ | |||
| import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert | |||
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/GenericInduction.lean:1.
Risk signals: changed imports.
Added-line sample:
- L1: import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| import Compiler.Proofs.IRGeneration.FunctionShape | ||
| import Compiler.Proofs.IRGeneration.GenericInduction.Calls | ||
| import Compiler.Proofs.IRGeneration.GenericInduction.DenoteSound | ||
| import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: changed imports; 1 changed line(s) near PrintAxioms.lean:58.
Risk signals: changed imports.
Added-line sample:
- L58: import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| stmtTouchesUnsupportedHelperSurface | ||
| (.requireError (.internalCall "helper" []) "HelperFailed" []) = true := by | ||
| native_decide | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 18 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemanticsFeatureTest.lean:284.
Risk signals: hotspot path/churn.
Added-line sample:
- L284: /-- `requireError` guards use the broad call-surface gate: foreign calls are
- L285: excluded there, while the distinct helper-surface gate continues to track only
- L286: internal helper calls. -/
- L287: example :
- L288: stmtTouchesUnsupportedCallSurface
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult, | ||
| evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state cond hsurface] | ||
| | .revertError _ args => | ||
| simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult] |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 8 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:5473.
Risk signals: hotspot path/churn.
Added-line sample:
- L5473: | .requireError cond _ args =>
- L5474: simp only [stmtTouchesUnsupportedHelperSurface] at hsurface
- L5475: simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult,
- L5476: evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state cond hsurface]
- L5477: | .revertError _ args =>
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| if resolved != 0 then .continue state else typedErrorRevertResult fields state args | ||
| | none => .revert | ||
| | state, .revertError _ args => | ||
| typedErrorRevertResult fields state args |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 7 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2486.
Risk signals: hotspot path/churn.
Added-line sample:
- L2486: | state, .requireError cond _ args =>
- L2487: match evalExpr fields state cond with
- L2488: | some resolved =>
- L2489: if resolved != 0 then .continue state else typedErrorRevertResult fields state args
- L2490: | none => .revert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| if resolved != 0 then .continue state else typedErrorRevertResult fields state args | ||
| | none => .revert | ||
| | state, .revertError _ args => | ||
| typedErrorRevertResult fields state args |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 7 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2769.
Risk signals: hotspot path/churn.
Added-line sample:
- L2769: | state, .requireError cond _ args =>
- L2770: match evalExpr fields state cond with
- L2771: | some resolved =>
- L2772: if resolved != 0 then .continue state else typedErrorRevertResult fields state args
- L2773: | none => .revert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f02423c23c
ℹ️ 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".
| | .requireError cond _ _ => | ||
| exprTouchesUnsupportedCallSurface cond |
There was a problem hiding this comment.
When a custom-error argument contains an .externalCall or .internalCall and the guard itself is call-free, this branch now returns false. However compileStmt still compiles args with compileExprListWithInternals and puts the resulting expressions in the revert block (Compiler/CompilationModel/Compile.lean:267-269), so a failing requireError can execute a call that this support predicate promised was absent. Please include args.any exprTouchesUnsupportedCallSurface here (and keep revertError consistent) before relying on the new bridge.
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_6f748e2a-36c3-4463-bfd3-077ca8409e82) |
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: 8 Lean file(s), 308 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-v8)
- Changed files: 8 supported / 8 total; Lean 8, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 308 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 30s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.lean (+195/-0), Compiler/Proofs/IRGeneration/SourceSemantics.lean (+40/-2), Compiler/Proofs/IRGeneration/SupportedSpec.lean (+20/-4), Compiler/Proofs/IRGeneration/SourceSemanticsFeatureTest.lean (+21/-0), Verity/Core/Model/Denote.lean (+12/-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.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/SourceSemantics.lean:2254 score 64 — public declaration/signature changed; ask: Confirm
typedErrorRevertResultis the intended (interim) StmtResult abstraction: verify (a) every downstreamexecStmt/execIRStmtsagreement lemma that touches.requireError/.revertErroris paired with a corresponding obligation on the Yul side, and (b) no existing proof silently relied on the prior bare.revertequality. Also confirm the docstring's deferral plan (StmtResult/IRResult returndata extension) is tracked as an open follow-up before merge. - Compiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.lean:1 score 103 — public declaration/signature changed, changed imports; ask: Audit each hypothesis in
compiledStmtStep_requireError_revert_casefor findability: does the production code supplying.requireError cond errorName argsproduce (i)hCondSrcfrom the literal-0 gate, (ii)hfailEval = some 1, and (iii)hrevertExecfor the emitted revert body? Flag any site where the IR emission could emit a non-if_ failCond revertStmtsshape (e.g. helper-using revert, bare revert, orrevert(0,…)) that would make this lemma inapplicable. - Compiler/Proofs/IRGeneration/SourceSemantics.lean:5473 score 30 — hotspot path/churn; ask: Verify the helper-surface assumption
hsurfaceis discharged at every reachable call-site that emits a.requireError(and that theargslist likewise sits on the closed helper surface for the revert branch). Specifically: confirm there is no construction of a.requireErrorwhosecondor argument expressions use helpers/libraries that would forceevalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosedto fail. - PrintAxioms.lean:58 score 42 — changed imports; ask: Run the axiom-printing pipeline (or
lean --print axiomspath used by this file) overCompiler.Proofs.IRGeneration.GenericInduction.ErrorRevertand report the full axiom list. Confirm there are noClassical.choice,sorryAx,propositional extensionality, or other non-proof irrelevant axioms newly introduced, and that any newly required axioms are intentional and cross-referenced in the PR description. - Compiler/Proofs/IRGeneration/GenericInduction.lean:1 score 60 — changed imports; ask: Verify
Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevertdoes not introduce a namespace collision with sibling files (e.g.Calls,Loops,Helpers,InternalCalls) and that theset_option/privatesettings it introduces don't leak across the umbrella file. - Compiler/Proofs/IRGeneration/SourceSemantics.lean:2486 score 30 — hotspot path/churn; ask: Confirm
evalExpr fields state argsintypedErrorRevertResultis pure with respect tostate.world(no storage write or transient-storage side effects), and that the| _ => .revertcatch-all matches the comment that 'the argument list is still evaluated ... to match the compiled code's control-flow surface'. Flag any case where arg-evaluation may panic/revert on its own before reaching the outer revert wrapper. - Compiler/Proofs/IRGeneration/SourceSemantics.lean:2769 score 30 — hotspot path/churn; ask: Diff this block against pkt-7's analogous block (line 2486-2492) byte-for-byte. Confirm both variants agree on the order: (1) eval
cond, (2) short-circuit.continue stateon success, (3) fall totypedErrorRevertResult fields state args(or.revertif cond-eval fails), and that no event/log/trace emission is silently inserted or removed between the two. - Compiler/Proofs/IRGeneration/SourceSemanticsFeatureTest.lean:284 score 31 — hotspot path/churn; ask: Confirm
stmtTouchesUnsupportedCallSurface (.requireError (.literal 0) "OracleFailed" [.externalCall "oracle" []])is the intended classification (gate correctly includes the.externalCalleven whencondis a literal), and thatnative_decidedoes not mask a semantic error here — e.g. by hand-running the function on the same inputs to cross-check.
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:2254 score 64 — public declaration/signature changed; ask: Confirm
Pilot mode: advisory only. Codex Review remains the merge gate.
| StmtResult := | ||
| match evalExprList fields state args with | ||
| | _ => .revert | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 13 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2254.
Risk signals: public declaration/signature changed.
Scout reason: Introduces the new public definition `typedErrorRevertResult` in SourceSemantics. Despite an explicit docstring acknowledging that ABI selectors and encoded typed payloads are intentionally not observable (deferred to a 'planned returndata extension'), it is being wired into the core execStmt/execStmtWithHelpers semantics. Any proof obligations equating this StmtResult to a corresponding IRResult will be carried out at this coarser abstraction, so a stronger reviewer must confirm this weakening
Question for stronger reviewer: Confirm `typedErrorRevertResult` is the intended (interim) StmtResult abstraction: verify (a) every downstream `execStmt`/`execIRStmts` agreement lemma that touches `.requireError`/`.revertError` is paired with a corresponding obligation on the Yul side, and (b) no existing proof silently relied on the prior bare `.revert` equality. Also confirm the docstring's deferral plan (StmtResult/IRResult returndata extension) is tracked as an open follow-up before merge.
Added-line sample:
- L2254: /-- Source-level custom-error revert at the current observable granularity.
- L2255:
- L2256: `StmtResult` does not yet carry returndata, so the ABI selector and encoded
- L2257: typed payload produced by compiled Yul are intentionally not observable here.
- L2258: That richer payload relation is deferred to the planned `StmtResult`/`IRResult`
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| refine ⟨.revert, .revert revState, hSrcExec, hrev, ?_⟩ | ||
| simp [stmtStepMatchesIRExec] | ||
|
|
||
| end Compiler.Proofs.IRGeneration |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · high]
Large Lean packet selected for stronger review: public declaration/signature changed, changed imports; 195 changed line(s) near Compiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.lean:1.
Risk signals: public declaration/signature changed, changed imports.
Scout reason: Largest new file (195 added lines) introducing `compiledStmtStep_requireError_revert_case`, with a public-declaration/signature change and new import. This is the IR-side helper theorem that the eventual requireError agreement will likely be assembled from; its conclusion pins together the result triple via `SourceSemantics.execStmtWithHelpers spec … (.requireError cond errorName args)` and `execIRStmts … [YulStmt.if_ failCond revertStmts]`. A reviewer must verify hypotheses line up with the pro
Question for stronger reviewer: Audit each hypothesis in `compiledStmtStep_requireError_revert_case` for findability: does the production code supplying `.requireError cond errorName args` produce (i) `hCondSrc` from the literal-0 gate, (ii) `hfailEval = some 1`, and (iii) `hrevertExec` for the emitted revert body? Flag any site where the IR emission could emit a non-`if_ failCond revertStmts` shape (e.g. helper-using revert, bare revert, or `revert(0,…)`) that would make this lemma inapplicable.
Added-line sample:
- L1: import Compiler.Proofs.IRGeneration.GenericInduction.ExprStmt
- L2:
- L3: set_option linter.unnecessarySeqFocus false
- L4: set_option linter.unnecessarySimpa false
- L5: set_option linter.unusedSimpArgs false
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult, | ||
| evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state cond hsurface] | ||
| | .revertError _ args => | ||
| simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult] |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 8 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:5473.
Risk signals: hotspot path/churn.
Scout reason: Edits the helper-surface-closure proof for `.requireError` and `.revertError`. The `.requireError cond _ args` branch now rewrites using `evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed` on `cond` plus `typedErrorRevertResult`. If pkt-2's abstraction is too coarse (e.g. still returns `.revert` regardless of args), this step may close a goal that should remain open, and the closure obligation for `args` could be missing.
Question for stronger reviewer: Verify the helper-surface assumption `hsurface` is discharged at every reachable call-site that emits a `.requireError` (and that the `args` list likewise sits on the closed helper surface for the revert branch). Specifically: confirm there is no construction of a `.requireError` whose `cond` or argument expressions use helpers/libraries that would force `evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed` to fail.
Added-line sample:
- L5473: | .requireError cond _ args =>
- L5474: simp only [stmtTouchesUnsupportedHelperSurface] at hsurface
- L5475: simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult,
- L5476: evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state cond hsurface]
- L5477: | .revertError _ args =>
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| import Compiler.Proofs.IRGeneration.FunctionShape | ||
| import Compiler.Proofs.IRGeneration.GenericInduction.Calls | ||
| import Compiler.Proofs.IRGeneration.GenericInduction.DenoteSound | ||
| import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: changed imports; 1 changed line(s) near PrintAxioms.lean:58.
Risk signals: changed imports.
Scout reason: PrintAxioms.lean registration. Adding `GenericInduction.ErrorRevert` to the axiom inventory is a trust-boundary change; reviewers must check that the new module does not silently introduce `axiom`, `sorry`, or non-externally-validated `native_decide` facts that should be visible in the Printed output.
Question for stronger reviewer: Run the axiom-printing pipeline (or `lean --print axioms` path used by this file) over `Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert` and report the full axiom list. Confirm there are no `Classical.choice`, `sorryAx`, `propositional extensionality`, or other non-proof irrelevant axioms newly introduced, and that any newly required axioms are intentional and cross-referenced in the PR description.
Added-line sample:
- L58: import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| @@ -1 +1,2 @@ | |||
| import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert | |||
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/GenericInduction.lean:1.
Risk signals: changed imports.
Scout reason: A single-line import addition re-exporting the new ErrorRevert module into `GenericInduction`. While the diff itself is tiny, the import is the propagation point for any errors in pkt-1/pkt-4 downstream — and any cyclic-import or namespace overlap from the new module's `private theorem` and `open Compiler.CompilationModel`/`open Compiler.Yul` must be checked.
Question for stronger reviewer: Verify `Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert` does not introduce a namespace collision with sibling files (e.g. `Calls`, `Loops`, `Helpers`, `InternalCalls`) and that the `set_option`/`private` settings it introduces don't leak across the umbrella file.
Added-line sample:
- L1: import Compiler.Proofs.IRGeneration.GenericInduction.ErrorRevert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| if resolved != 0 then .continue state else typedErrorRevertResult fields state args | ||
| | none => .revert | ||
| | state, .revertError _ args => | ||
| typedErrorRevertResult fields state args |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 7 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2486.
Risk signals: hotspot path/churn.
Scout reason: Semantics of `.requireError`/`.revertError` added to one of the SourceSemantics `execStmt` variants. On the failing-cond path it now returns `typedErrorRevertResult fields state args` instead of plain `.revert`. Reviewer must ensure neither the success-cond short-circuit (`.continue state`) nor the `none` (subtly underflow / out-of-gas) branch is silently altered, and that argument evaluation in `typedErrorRevertResult` cannot observe a different world than was active before the revert.
Question for stronger reviewer: Confirm `evalExpr fields state args` in `typedErrorRevertResult` is pure with respect to `state.world` (no storage write or transient-storage side effects), and that the `| _ => .revert` catch-all matches the comment that 'the argument list is still evaluated ... to match the compiled code's control-flow surface'. Flag any case where arg-evaluation may panic/revert on its own before reaching the outer revert wrapper.
Added-line sample:
- L2486: | state, .requireError cond _ args =>
- L2487: match evalExpr fields state cond with
- L2488: | some resolved =>
- L2489: if resolved != 0 then .continue state else typedErrorRevertResult fields state args
- L2490: | none => .revert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| if resolved != 0 then .continue state else typedErrorRevertResult fields state args | ||
| | none => .revert | ||
| | state, .revertError _ args => | ||
| typedErrorRevertResult fields state args |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 7 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2769.
Risk signals: hotspot path/churn.
Scout reason: Mirror image of pkt-7 in a second `execStmt` variant (likely `execStmtWithEvents` or `execStmtWithHelpers`). Keeping these two patches structurally identical is a non-trivial maintenance/duplication risk; if the two diverge later, the agreement lemmas will silently break.
Question for stronger reviewer: Diff this block against pkt-7's analogous block (line 2486-2492) byte-for-byte. Confirm both variants agree on the order: (1) eval `cond`, (2) short-circuit `.continue state` on success, (3) fall to `typedErrorRevertResult fields state args` (or `.revert` if cond-eval fails), and that no event/log/trace emission is silently inserted or removed between the two.
Added-line sample:
- L2769: | state, .requireError cond _ args =>
- L2770: match evalExpr fields state cond with
- L2771: | some resolved =>
- L2772: if resolved != 0 then .continue state else typedErrorRevertResult fields state args
- L2773: | none => .revert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| stmtTouchesUnsupportedCallSurface | ||
| (.requireError (.literal 0) "CallFree" [.literal 1]) = false := by | ||
| native_decide | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 21 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemanticsFeatureTest.lean:284.
Risk signals: hotspot path/churn.
Scout reason: New `native_decide` examples asserting that `.requireError` triggers the unsupported-call-surface gate even when the call lives inside `args`. A reviewer should verify the gate's classification is actually correct (i.e. that any compiled `requireError` whose args contain a disallowed call still surfaces through the gate), and that `native_decide` here is decidable over a small-enough term that compiler evaluation matches the intended proposition.
Question for stronger reviewer: Confirm `stmtTouchesUnsupportedCallSurface (.requireError (.literal 0) "OracleFailed" [.externalCall "oracle" []])` is the *intended* classification (gate correctly includes the `.externalCall` even when `cond` is a literal), and that `native_decide` does not mask a semantic error here — e.g. by hand-running the function on the same inputs to cross-check.
Added-line sample:
- L284: /-- Custom-error guards and payloads use the broad call-surface gate. -/
- L285: example :
- L286: stmtTouchesUnsupportedCallSurface
- L287: (.requireError (.externalCall "oracle" []) "OracleFailed" []) = true := by
- L288: native_decide
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
Codex Review: Didn't find any major issues. Breezy! 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". |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2d373955b6
ℹ️ 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_e39b5a17-47d5-4e1f-a229-65a1b3538819) |
|
@codex review Please review immutable head |
There was a problem hiding this comment.
OpenCodeReview first-pass review
Status: scout_triage · Mode: large-lean-hotspots · 5 finding(s) · 3 files · 0 tokens · 0 tool calls
Large Lean diff routed to bounded packet review: 10 Lean file(s), 319 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-v8)
- Changed files: 10 supported / 10 total; Lean 10, trust docs 0, workflow/scripts 0, contracts 0, docs 0
- Changed lines: 319 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 5; files 3; tokens 0; tool calls 0; warnings 1; duration 37s
- Largest changed files: Compiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.lean (+195/-0), Compiler/Proofs/IRGeneration/SourceSemantics.lean (+40/-2), Compiler/Proofs/IRGeneration/SupportedSpec.lean (+20/-4), Compiler/Proofs/IRGeneration/SourceSemanticsFeatureTest.lean (+21/-0), Verity/Core/Model/Denote.lean (+12/-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.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/SourceSemantics.lean:2254 score 64 — public declaration/signature changed; ask: Is the lossy
typedErrorRevertResultabstraction safe for all downstreamcompiledStmtStep_*_caseproofs inGenericInduction/ErrorRevert.lean? In particular, does the IR side of the iff actually produce an indistinguishable.revert(no observable returndata), or does the Yul revert carry a payload that downstreamexecStmt/execStmtWithHelpersconsumers might later need? Verify thatmatch _ => .revertis not silently hiding a case where argument evaluation diverges (e.g. a future `Stmt - Compiler/Proofs/IRGeneration/SourceSemantics.lean:2486 score 30 — hotspot path/churn; ask: Does the
.requireErrorbranch correctly model that (a)condis evaluated first, (b) on success (non-zero) the argument list is NOT evaluated and execution continues, and (c) on failure (zero ornone) the argument list IS evaluated (for side-effect reads) before the.revertresult? Confirm there is no path whereargsare evaluated on the success branch (which would be unsound w.r.t. the compiled Yul's short-circuitif_ failCond revertStmts). - Compiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.lean:1 score 103 — public declaration/signature changed, changed imports; ask: Read the full proof body of
compiledStmtStep_requireError_revert_caseend-to-end. Confirm there are nosorry,admit,native_decideover an unbounded payload, or unproved side conditions. In particular, verify that thehrevertExechypothesis (∀ state fuel, ∃ next, execIRStmts fuel state revertStmts = .revert next) is correctly discharged from the surrounding induction, and that the existentialsourceResult/irResultproduced matches thetypedErrorRevertResultshape from pkt-2 (i.e. - Compiler/Proofs/IRGeneration/SourceSemantics.lean:5473 score 30 — hotspot path/churn; ask: Does the new
.requireErrorcase correctly dischargeevalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosedforcondgiven onlyhsurface : stmtTouchesUnsupportedHelperSurface (.requireError cond _ args) = false? And does the finalsimp [..., typedErrorRevertResult]actually rewrite both sides to the sameStmtResult(i.e. is the helper-instrumented execution oftypedErrorRevertResultdefinitionally equal to the bare one)? Ifsimpleaves a subgoal aboutevalExprListwith vs withou - Compiler/Proofs/GeneratedTransitionTest.lean:23 score 30 — hotspot path/churn; ask: Trace the
extractimplementation forStmt.requireErrorand confirm: (a)failingRequireError.reads.contains "balance"is true because the failing-path argument listevalExprs.storage "balance", and (b)literalRequireError.reads.isEmptyholds because literals contribute no reads. Cross-check against the pkt-8 semantics: the.continueshort-circuit means a passingrequireErrorshould NOT include payload reads in the summary — but the test only covers the failing case. Is there a
- Compiler/Proofs/IRGeneration/SourceSemantics.lean:2254 score 64 — public declaration/signature changed; ask: Is the lossy
Pilot mode: advisory only. Codex Review remains the merge gate.
| StmtResult := | ||
| match evalExprList fields state args with | ||
| | _ => .revert | ||
|
|
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · medium]
Large Lean packet selected for stronger review: public declaration/signature changed; 13 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2254.
Risk signals: public declaration/signature changed.
Scout reason: Defines `typedErrorRevertResult` as a `def` whose body is `match evalExprList ... with | _ => .revert` — argument evaluation is computed but its result is discarded, so the function is observably identical to a constant `.revert`. The accompanying docstring explicitly admits that the ABI selector and encoded typed payload are 'intentionally not observable here' and defers the richer payload relation to a future `StmtResult`/`IRResult` returndata extension. This is a deliberate semantic weakening
Question for stronger reviewer: Is the lossy `typedErrorRevertResult` abstraction safe for all downstream `compiledStmtStep_*_case` proofs in `GenericInduction/ErrorRevert.lean`? In particular, does the IR side of the iff actually produce an indistinguishable `.revert` (no observable returndata), or does the Yul revert carry a payload that downstream `execStmt`/`execStmtWithHelpers` consumers might later need? Verify that `match _ => .revert` is not silently hiding a case where argument evaluation diverges (e.g. a future `Stmt
Added-line sample:
- L2254: /-- Source-level custom-error revert at the current observable granularity.
- L2255:
- L2256: `StmtResult` does not yet carry returndata, so the ABI selector and encoded
- L2257: typed payload produced by compiled Yul are intentionally not observable here.
- L2258: That richer payload relation is deferred to the planned `StmtResult`/`IRResult`
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| if resolved != 0 then .continue state else typedErrorRevertResult fields state args | ||
| | none => .revert | ||
| | state, .revertError _ args => | ||
| typedErrorRevertResult fields state args |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 7 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:2486.
Risk signals: hotspot path/churn.
Scout reason: Adds the `.requireError` and `.revertError` cases to the core `SourceSemantics.execStmt` interpreter. The `.requireError` branch routes through the lossy `typedErrorRevertResult` defined in pkt-2, and the docstring/spec for `requireError` semantics (success path does not evaluate args; revert path does) is encoded directly here. Any error in the ordering of `evalExpr cond` vs `evalExprList args`, or in the `.continue` short-circuit, would silently change observable behavior of every contract usi
Question for stronger reviewer: Does the `.requireError` branch correctly model that (a) `cond` is evaluated first, (b) on success (non-zero) the argument list is NOT evaluated and execution continues, and (c) on failure (zero or `none`) the argument list IS evaluated (for side-effect reads) before the `.revert` result? Confirm there is no path where `args` are evaluated on the success branch (which would be unsound w.r.t. the compiled Yul's short-circuit `if_ failCond revertStmts`).
Added-line sample:
- L2486: | state, .requireError cond _ args =>
- L2487: match evalExpr fields state cond with
- L2488: | some resolved =>
- L2489: if resolved != 0 then .continue state else typedErrorRevertResult fields state args
- L2490: | none => .revert
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| refine ⟨.revert, .revert revState, hSrcExec, hrev, ?_⟩ | ||
| simp [stmtStepMatchesIRExec] | ||
|
|
||
| end Compiler.Proofs.IRGeneration |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · high]
Large Lean packet selected for stronger review: public declaration/signature changed, changed imports; 195 changed line(s) near Compiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.lean:1.
Risk signals: public declaration/signature changed, changed imports.
Scout reason: A new 195-line file introducing a private theorem `compiledStmtStep_requireError_revert_case` that is the source-of-truth bridge between source-level `.requireError cond errorName args` and IR-level `[YulStmt.if_ failCond revertStmts]`. The diff header lists 'public declaration/signature changed' and 'changed imports' — the file is brand new and is imported by `GenericInduction.lean` and registered in `PrintAxioms.lean`, so any axiom or `sorry` inside it would propagate to the entire trusted bas
Question for stronger reviewer: Read the full proof body of `compiledStmtStep_requireError_revert_case` end-to-end. Confirm there are no `sorry`, `admit`, `native_decide` over an unbounded payload, or unproved side conditions. In particular, verify that the `hrevertExec` hypothesis (∀ state fuel, ∃ next, execIRStmts fuel state revertStmts = .revert next) is correctly discharged from the surrounding induction, and that the existential `sourceResult`/`irResult` produced matches the `typedErrorRevertResult` shape from pkt-2 (i.e.
Added-line sample:
- L1: import Compiler.Proofs.IRGeneration.GenericInduction.ExprStmt
- L2:
- L3: set_option linter.unnecessarySeqFocus false
- L4: set_option linter.unnecessarySimpa false
- L5: set_option linter.unusedSimpArgs false
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult, | ||
| evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state cond hsurface] | ||
| | .revertError _ args => | ||
| simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult] |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 8 changed line(s) near Compiler/Proofs/IRGeneration/SourceSemantics.lean:5473.
Risk signals: hotspot path/churn.
Scout reason: Modifies the `execStmtWithHelpers_eq_execStmt_of_helperSurfaceClosed` proof in `SourceSemantics.lean` to add `.requireError` and `.revertError` cases. The `.requireError` branch now uses `stmtTouchesUnsupportedHelperSurface` and invokes `evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed` on `cond`, then closes with `typedErrorRevertResult`. This is the proof machinery that says 'if a statement's helper surface is closed, with-helpers and without-helpers executions agree' — extending it to c
Question for stronger reviewer: Does the new `.requireError` case correctly discharge `evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed` for `cond` given only `hsurface : stmtTouchesUnsupportedHelperSurface (.requireError cond _ args) = false`? And does the final `simp [..., typedErrorRevertResult]` actually rewrite both sides to the same `StmtResult` (i.e. is the helper-instrumented execution of `typedErrorRevertResult` definitionally equal to the bare one)? If `simp` leaves a subgoal about `evalExprList` with vs withou
Added-line sample:
- L5473: | .requireError cond _ args =>
- L5474: simp only [stmtTouchesUnsupportedHelperSurface] at hsurface
- L5475: simp [execStmtWithHelpers, execStmtWithEvents, typedErrorRevertResult,
- L5476: evalExprWithHelpers_eq_evalExpr_of_helperSurfaceClosed spec fields fuel state cond hsurface]
- L5477: | .revertError _ args =>
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
| (failingRequireError.reads.contains "balance") | ||
| let literalRequireError := extract | ||
| [Stmt.requireError (Expr.literal 0) "InsufficientBalance" [Expr.literal 1]] | ||
| assert "literal requireError payload remains read-free" literalRequireError.reads.isEmpty |
There was a problem hiding this comment.
OpenCodeReview [large-lean-hotspots · low]
Large Lean packet selected for stronger review: hotspot path/churn; 7 changed line(s) near Compiler/Proofs/GeneratedTransitionTest.lean:23.
Risk signals: hotspot path/churn.
Scout reason: Adds two new behavioral assertions in `GeneratedTransitionTest.lean`: a `failing requireError` should include the payload's storage reads in `summary.reads`, and a `literal requireError` payload should remain read-free. These tests pin down a *new* invariant about `requireError` payload analysis that is not asserted anywhere else in the PR. If the `extract`/summary logic disagrees with how the source semantics (pkt-8) actually evaluates arguments — for instance, if a literal expression is incorr
Question for stronger reviewer: Trace the `extract` implementation for `Stmt.requireError` and confirm: (a) `failingRequireError.reads.contains "balance"` is true because the failing-path argument list `evalExpr`s `.storage "balance"`, and (b) `literalRequireError.reads.isEmpty` holds because literals contribute no reads. Cross-check against the pkt-8 semantics: the `.continue` short-circuit means a *passing* `requireError` should NOT include payload reads in the summary — but the test only covers the failing case. Is there a
Added-line sample:
- L23: let failingRequireError := extract
- L24: [Stmt.requireError (Expr.literal 0) "InsufficientBalance" [Expr.storage "balance"]]
- L25: assert "failing requireError includes payload storage reads"
- L26: (failingRequireError.reads.contains "balance")
- L27: let literalRequireError := extract
This packet is scout triage and a coverage marker; it is not a final OCR semantic review or approval.
|
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 |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 66c0517600
ℹ️ 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".
| (hnextScopeIncl : FunctionBody.scopeNamesIncluded | ||
| (stmtNextScope scope (.requireError cond errorName args)) scope) |
There was a problem hiding this comment.
For normal custom errors this premise is not provable: collectStmtNames (.requireError ...) includes errorName, so stmtNextScope asks callers to show the custom error name is already present as a runtime/IR binding even though executing requireError never creates such a binding. As a result the continue branch of this new bridge theorem cannot be applied to ordinary requireError cond InsufficientBalance(...) statements unless a dummy variable named InsufficientBalance is in scope; the theorem should use a scope that excludes the error name (or otherwise avoid requiring it in the post-scope).
Useful? React with 👍 / 👎.
1 participant
Theorems
Compiler.Proofs.IRGeneration.compiledStmtStep_requireErrorCompiler.Proofs.IRGeneration.compiledStmtStep_revertErrorSemantic modeling decisions
Stmt.requireError cond errName argsnow evaluatescondin the source semantics.condresolves to a nonzero word, the statement continues with the unchanged state.args, matching the compiled Yul shape where the custom-error encoding block is guarded behindiszero(cond).condresolves to zero, the argument list is evaluated on the reverting path, but the observable result is still.revertwhether argument evaluation succeeds or fails.condfails to evaluate, the result is.revert.Stmt.revertError errName argsalways results in.revertat the current source-result granularity.StmtResult/IRResultdo not carry returndata; the helper docstring records that this is deferred to the planned result-extension work.Proof intuition
compiledStmtStep_requireErrorfollows the plainrequirebranch shape: compile/evaluate the source condition and compiled fail condition, then split on whether the condition word is zero.ifexecutes the custom-error revert block and the source result is.revert.ifskips the revert block and the source result is.continue, preserving runtime/state/scope invariants.compiledStmtStep_revertErrorrelates the source.revertresult to the compiled custom-error revert block at the current observable granularity.hrevertExecpremise because returndata is not yet part of the statement/IR result relation.Files
Compiler/Proofs/IRGeneration/SourceSemantics.leanCompiler/Proofs/IRGeneration/GenericInduction/ErrorRevert.leanCompiler/Proofs/IRGeneration/GenericInduction.leanPrintAxioms.leanBase
origin/main=bd54fa9c47b9abb43895c312fe1f874192ba8327Dependencies
Validation
lean-slot lake buildpassed; remote DGX Spark offload finished with exit 0.python3 scripts/generate_print_axioms.py --checkpassed:PrintAxioms.lean is up to date.python3 scripts/lean_lint.py --only axiomspassed: registry complete and synchronized with 0 source axioms.make checkpassed:All checks passed.git diff --checkpassed on the staged diff.sorry/admit/axiom/#exitfound no new Lean proof placeholders or axiom declarations; the only textual hit was the generatedPrintAxioms.leansummary line0 sorry'd.Note
Medium Risk
Touches core compiler proof semantics and IR/source agreement for error/revert paths; observable revert payload is intentionally abstracted until returndata is modeled.
Overview
Adds source semantics for
requireErrorandrevertErrorviatypedErrorRevertResult: both end in.revertat the current granularity (no returndata yet).requireErrorevaluates the condition; on success it continues without evaluating args; on failure it evaluates args then reverts.revertErroralways evaluates args and reverts.New
ErrorRevert.leanprovescompiledStmtStep_requireErrorandcompiledStmtStep_revertError, relating compiledif failCond revertStmtsIR to source behavior (revert vs continue split on the condition word).SupportedSpec,GeneratedTransition,Denote, andDenoteAgreementare updated so surface checks, transition reads, and denotation stay aligned. Tests coverrequireErrorread extraction and call-surface gates.Reviewed by Cursor Bugbot for commit 66c0517. Bugbot is set up for automated code reviews on this repo. Configure here.