chore: migrate to Lean 4.31 - #2209
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_d18745ae-5522-483b-a55b-6ee5438f24ff) |
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_83fa17b1-eb5f-445f-bd77-4ef69a2dbc48) |
![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: b692394e91
ℹ️ 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".
| \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
🟡 Scout triage only — not a full review. 5 finding(s) (5 low); a human or Codex must still cover the unflagged hunks and proof obligations.
Large Lean diff routed to bounded packet review: 3 Lean file(s), 46 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 5/5 packet(s) for stronger review. Scout triage success; strong packet review required. Full-file OCR was not attempted.
✅ Posted 5 inline comment(s).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 5 supported / 6 total; Lean 3, trust docs 0, workflow/scripts 2, contracts 0, docs 0
- Changed lines: 46 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 5; files 4; tokens 0; tool calls 0; warnings 1; duration 125s
- Largest changed files: lake-manifest.json (+17/-16), Verity/Core/FiniteSet.lean (+4/-2), Verity/Specs/Common/Sum.lean (+1/-2), artifacts/verification_status.json (+1/-1), lakefile.lean (+1/-1)
Packet coverage
- Packet review: enabled; selected 5/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: 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:
- Verity/Core/FiniteSet.lean:260 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Confirm that
FiniteAddressSet.insert bunfolds definitionally toFiniteSet.insert b s.addressesand thata ∈ s(FiniteAddressSet membership) unfolds definitionally toa ∈ s.addresses.elementswithout requiring@[simp]orIfflemmas. If these equalities are only propositional, thechangewould fail — so verify the proof still compiles underset_option pp.all true. - Verity/Core/FiniteSet.lean:362 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Same as pkt-1 but for the
Natvariant: verifyFiniteNatSet.insert bandn ∈ sunfold definitionally toFiniteSet.insert b s.nats/n ∈ s.nats.elements. Also check whetherFiniteSet.mem_elements_insertis stated generically enough to cover bothAddressandNatelement types without hidden assumptions. - Verity/Specs/Common/Sum.lean:204 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Verify that (1) removing
simp only [] at h_resultdoes not alter the normal form ofh_resultin a way the subsequentrw [h_old]/exactdepends on, (2) thesimp [BEq.beq]side-condition proofs at lines 202-203 are not vacuously true due to a degenerateBEqinstance or trivially-satisfied inequality, and (3) the definitional equality between HSub/HAdd and add/sub at line 208 is genuinely kernel-verified byexactand not relying on adecide/rflshortcut that could fail under diff - lakefile.lean:8 score 12 [lenses: provenance, environment-determinism, proof-soundness] — hotspot path/churn; ask: Is commit f7e4ee0dc8f8d5265ce822a937ab5be771f182e9 of github.com/lfglabs-dev/EVMYulLean.git a trusted, reviewed revision, and was the change from 38d53df8b4488d5322894619ea8385fcbb2e6f5d intentional and verified rather than a silent producer swap of the dependency the proofs depend on?
- lake-manifest.json:1 score 1 [lenses: provenance, environment-determinism] — hotspot path/churn; ask: Does this manifest revision bump cover ALL dependencies the proofs depend on, are both new revisions (EVMYulLean f7e4ee0d..., mathlib fabf563a...) trusted/traceable commits, and could any artifact or dependency be added/swap without being pinned here?
- Verity/Core/FiniteSet.lean:260 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Confirm that
Pilot mode: advisory only. Codex Review remains the merge gate.
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_236e888c-4af9-4496-bc37-ce1bd2f1ae33) |
|
@codex review |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. 8 finding(s) (8 low); a human or Codex must still cover the unflagged hunks and proof obligations.
Large Lean diff routed to bounded packet review: 4 Lean file(s), 407 changed supported line(s). Multi-lens scout (4/4 lens(es): provenance, verification-independence, environment-determinism, proof-soundness) surfaced 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).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 11 supported / 15 total; Lean 4, trust docs 0, workflow/scripts 7, contracts 0, docs 0
- Changed lines: 407 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status scout_triage; comments 8; files 7; tokens 0; tool calls 0; warnings 1; duration 98s
- Largest changed files: scripts/generate_evmyullean_fork_audit.py (+138/-5), artifacts/evmyullean_fork_audit.json (+134/-4), lake-manifest.json (+17/-16), packages/verity-compiler/lake-manifest.json (+13/-13), packages/verity-edsl/lake-manifest.json (+13/-13)
Packet coverage
- Packet review: enabled; selected 8/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: 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:
- Verity/Core/FiniteSet.lean:260 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Confirm that the
changetarget is definitionally equal to the original goal in both directions of the iff, and thatFiniteSet.mem_elements_inserthas the exact statement needed (no hidden assumption like decidable equality or ordering). Was thesimparemoval prompted by a simp-normalization change in Lean 4.24? - Verity/Core/FiniteSet.lean:362 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Same verification as pkt-1: is the
changetarget a faithful definitional unfolding of the original goal, and doesFiniteSet.mem_elements_insertapply without additional assumptions (e.g.,LawfulBEq,DecidableEq)? - Verity/Specs/Common/Sum.lean:204 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: After removing
simp only [] at h_result, doesrw [h_old]still fire on the intended subterm, and is theexact h_resultclosing step truly kernel-checked definitional equality (not a coincidence of notation coercion)? Could a future Mathlib/Lean update to arithmetic instance normalization break this bridge silently? - lakefile.lean:8 score 12 [lenses: provenance, environment-determinism] — hotspot path/churn; ask: Is there a build-time or CI check that fails if the evmyul revision pinned in lakefile.lean is not the last entry in the fork-audit artifact, or can the pin and the audit drift independently so that a trusted-looking manifest backs an untrusted commit?
- packages/verity-edsl/lakefile.lean:8 score 12 [lenses: environment-determinism] — hotspot path/churn; ask: Are the verity root and verity-edsl pins guaranteed identical by a CI check, or is this a manual-sync invariant? Does Lake's lock resolution ever fall back to a branch/tag if the SHA fetch fails?
- artifacts/evmyullean_fork_audit.json:60 score 6 [lenses: provenance, verification-independence, environment-determinism] — hotspot path/churn; ask: Cross-reference the audited SHAs in this JSON against
git rev-list 38d53df..f7e4ee0for the evmyul repository. Are there any commits in the actual range that have no audit entry here? If so, those commits' changes are unprovenanced. - scripts/generate_evmyullean_fork_audit.py:200 score 6 [lenses: provenance, verification-independence, environment-determinism] — hotspot path/churn; ask: Does the generator independently walk the full git rev-list between the old pinned SHA (38d53df) and the new pinned SHA (f7e4ee0) and require an audit entry for each commit, or is the commit list a hardcoded, producer-editable array whose completeness is never enforced? If the latter, how many commits in the actual range are silently missing from the audit?
- lake-manifest.json:1 score 1 [lenses: provenance, verification-independence, environment-determinism] — hotspot path/churn; ask: Is the mathlib revision change (f897ebcf → fabf563a) independently audited or covered by any provenance artifact? If not, a critical dependency that the proof artifacts depend on has been silently swapped without a corresponding trust manifest entry.
- Verity/Core/FiniteSet.lean:260 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Confirm that the
Pilot mode: advisory only. Codex Review remains the merge gate.
|
Codex Review: Didn't find any major issues. 👍 Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
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_918d0472-2a7c-439d-8b10-08c0e1f766c3) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. 5 finding(s) (5 low); a human or Codex must still cover the unflagged hunks and proof obligations.
Large Lean diff routed to bounded packet review: 5 Lean file(s), 550 changed supported line(s). Multi-lens scout (3/4 lens(es): provenance, verification-independence, environment-determinism) surfaced 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).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 12 supported / 16 total; Lean 5, trust docs 0, workflow/scripts 7, contracts 0, docs 0
- Changed lines: 550 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 126s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean (+85/-58), scripts/generate_evmyullean_fork_audit.py (+138/-5), artifacts/evmyullean_fork_audit.json (+134/-4), lake-manifest.json (+17/-16), packages/verity-compiler/lake-manifest.json (+13/-13)
Packet coverage
- Packet review: enabled; selected 5/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness (1 lens(es) failed; union of the rest used); rubric items checked 3
- 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/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean:135 score 39 [lenses: environment-determinism] — hotspot path/churn; ask: Does uint256_neg_val discharge the same goal that the deleted literal-based habs_b_lit did? Are there any Lean versions where EvmYul.UInt256.size might unfold differently (e.g. via an environment override or redefinition in the new evmyul commit)?
- Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean:26 score 36 [lenses: environment-determinism] — hotspot path/churn; ask: Is the Lean toolchain version pinned (e.g. via lean-toolchain or lake-manifest)? What happens if a reviewer builds with Lean 4.30 or 4.32? Does the comment 'Lean 4.31 keeps the Fin instance' indicate the proof would have a different meaning or fail under a different toolchain?
- Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean:491 score 35 [lenses: environment-determinism] — hotspot path/churn; ask: Does the change tactic produce the identical proof term as the deleted simp+norm_num path? If a reviewer uses a different Lean version, would simp/norm_num on EvmYul.UInt256.size produce a different result, making this refactor necessary?
- lakefile.lean:8 score 12 [lenses: provenance, environment-determinism] — hotspot path/churn; ask: Does commit f7e4ee0dc8f8d5265ce822a937ab5be771f182e9 correspond to an independently reviewed/tagged release of lfglabs-dev/EVMYulLean, and do the root and all package lakefiles plus lake-manifest. files pin the exact same commit with no branch/tag fallback or stale lockfile?
- packages/verity-edsl/lakefile.lean:8 score 12 [lenses: provenance, environment-determinism] — hotspot path/churn; ask: Is the verity-edsl evmyul pin required to match the root and all other package pins exactly, and does the build verify that all resolved evmyul artifacts come from f7e4ee0... rather than an alternate local, cached, or manifest-uncovered source?
Pilot mode: advisory only. Codex Review remains the merge gate.
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_8c1ce329-0ffd-47de-9224-f7df03774ccf) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. 5 finding(s) (5 low); a human or Codex must still cover the unflagged hunks and proof obligations.
Large Lean diff routed to bounded packet review: 6 Lean file(s), 564 changed supported line(s). Multi-lens scout (3/4 lens(es): provenance, environment-determinism, proof-soundness) surfaced 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).
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 13 supported / 17 total; Lean 6, trust docs 0, workflow/scripts 7, contracts 0, docs 0
- Changed lines: 564 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 126s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean (+93/-58), scripts/generate_evmyullean_fork_audit.py (+138/-5), artifacts/evmyullean_fork_audit.json (+134/-4), lake-manifest.json (+17/-16), packages/verity-compiler/lake-manifest.json (+13/-13)
Packet coverage
- Packet review: enabled; selected 5/8 packet(s)
- Scout: configured; status success; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness (1 lens(es) failed; union of the rest used); rubric items checked 3
- 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/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean:135 score 40 [lenses: proof-soundness] — hotspot path/churn; ask: Verify that
hbsupplied touint256_neg_valat line 138 actually entails bothb < EvmYul.UInt256.sizeand0 < b, and that the resulting identity is the one the surrounding proof ofint256_div_toUint256_val_eq_uint256_sdivrequires. - Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean:26 score 36 [lenses: environment-determinism, proof-soundness] — hotspot path/churn; ask: Is the Lean toolchain version (4.31 or otherwise) pinned in lake-manifest.? If a reviewer builds with a different Lean patch version, will the normalization assumptions in this lemma (relying on how the Fin instance is elaborated) still hold, or could elaboration silently change the proof obligation?
- Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean:499 score 35 [lenses: proof-soundness] — hotspot path/churn; ask: Confirm
hpos : 0 < ais in scope at line 499 and that thechangeterm is definitionally equal to the original goal (not a syntactically-rewritten weaker statement that loses thea = 0disjunct). - PrintAxioms.lean:6070 score 12 [lenses: proof-soundness] — hotspot path/churn; ask: Run
#print axiomson each of the four newly listed private lemmas and confirm none transitively depends onsorry/admit/Classical.choice/Std.Tactic.Breaking.unsafeAxor any axioms not already declared in the manifest. - lakefile.lean:8 score 12 [lenses: provenance, environment-determinism] — hotspot path/churn; ask: Has commit f7e4ee0dc8f8d5265ce822a937ab5be771f182e9 of EVMYulLean.git been independently audited? What axioms, definitions, or tactics changed between 38d53df and f7e4ee0? Do all four lake-manifest. files (root + three packages) pin the same commit, or can a package silently resolve to a different ref?
- Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean:135 score 40 [lenses: proof-soundness] — hotspot path/churn; ask: Verify that
Pilot mode: advisory only. Codex Review remains the merge gate.
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 29 Lean file(s), 1516 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 38 supported / 42 total; Lean 29, trust docs 1, workflow/scripts 8, contracts 0, docs 0
- Changed lines: 1516 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 1s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness/Base.lean (+218/-181), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean (+93/-58), scripts/generate_evmyullean_fork_audit.py (+138/-5), artifacts/evmyullean_fork_audit.json (+134/-4), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean (+51/-51)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 85c1cfde25
ℹ️ 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_aeb84b88-141c-4555-ba82-9488ef9a3c23) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 29 Lean file(s), 1522 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 38 supported / 42 total; Lean 29, trust docs 1, workflow/scripts 8, contracts 0, docs 0
- Changed lines: 1522 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness/Base.lean (+220/-185), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean (+93/-58), scripts/generate_evmyullean_fork_audit.py (+138/-5), artifacts/evmyullean_fork_audit.json (+134/-4), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean (+51/-51)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
|
@codex review |
|
@terra 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_7e6c3ae7-cccb-461a-8bbc-ae65576baf93) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 29 Lean file(s), 1517 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 38 supported / 42 total; Lean 29, trust docs 1, workflow/scripts 8, contracts 0, docs 0
- Changed lines: 1517 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness/Base.lean (+217/-184), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean (+93/-58), scripts/generate_evmyullean_fork_audit.py (+138/-5), artifacts/evmyullean_fork_audit.json (+134/-4), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean (+51/-51)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
|
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". |
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_6b7e91e6-cfaf-4d5f-82e3-363636e36be5) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 29 Lean file(s), 1527 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 38 supported / 42 total; Lean 29, trust docs 1, workflow/scripts 8, contracts 0, docs 0
- Changed lines: 1527 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness/Base.lean (+216/-195), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean (+93/-58), scripts/generate_evmyullean_fork_audit.py (+138/-5), artifacts/evmyullean_fork_audit.json (+134/-4), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean (+51/-51)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f6696ab378
ℹ️ 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_804f159c-80aa-44f7-9417-c4c281dfdbcf) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 29 Lean file(s), 1535 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 38 supported / 42 total; Lean 29, trust docs 1, workflow/scripts 8, contracts 0, docs 0
- Changed lines: 1535 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness/Base.lean (+221/-198), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean (+93/-58), scripts/generate_evmyullean_fork_audit.py (+138/-5), artifacts/evmyullean_fork_audit.json (+134/-4), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean (+51/-51)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
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_1e5bca2e-0c7a-4a57-abe5-3b82419553f4) |
There was a problem hiding this comment.
OpenCodeReview first-pass review
🟡 Scout triage only — not a full review. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 29 Lean file(s), 1537 changed supported line(s).
Warnings
- routing : Diff exceeded bounded packet review capability; full OCR not attempted.
OCR pilot metrics & packet coverage
OCR pilot metrics
- Routing: large-lean-hotspots (router-v10)
- Changed files: 38 supported / 42 total; Lean 29, trust docs 1, workflow/scripts 8, contracts 0, docs 0
- Changed lines: 1537 supported; thresholds large Lean >=3 files or >800 lines
- OCR: status large-lean-hotspots; comments 0; files 0; tokens 0; tool calls 0; warnings 1; duration 0s
- Largest changed files: Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness/Base.lean (+217/-204), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeSignedArithLemmas.lean (+93/-58), scripts/generate_evmyullean_fork_audit.py (+138/-5), artifacts/evmyullean_fork_audit.json (+134/-4), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanSourceExprClosure.lean (+51/-51)
Packet coverage
- Packet review: not used; selected 0/8 packet(s)
- Scout: configured; status skipped_no_packets; model builtin/assistant
- Scout lenses: provenance, verification-independence, environment-determinism, proof-soundness; rubric items checked 3
- Strong review: required; status blocked_packet_input
- Residual risk: Diff exceeded packet budget; use top changed files and deterministic signals as required Codex/human review checklist.
- Strong packet-review blocker: OpenCodeReview 1.7.9 supports --from/--to full diff ranges, but this workflow does not have a safe packet/window input bridge for Lean hunks yet.
Pilot mode: advisory only. Codex Review remains the merge gate.
1 participant
Summary
f7e4ee0dc8f8d5265ce822a937ab5be771f182e9FiniteSetwrapper insertion proofs explicit enough for Lean 4.31 elaborationScope
Migration compatibility only; no proof or contract semantics are changed.
Merge gate
Do not merge until all checks below succeed on one immutable PR head, with receipts retained:
lake build PrintAxioms,lake env lean PrintAxioms.lean, andscripts/check_axioms.py --log axiom-report-raw.logafter regeneration/check;make test-evmyullean-fork, including the native harness target;Current status
Head
47aa29680a84e6eb93a7b516320f2afc55aa8cf7is blocked: requiredbuildand EVMYulLean fork-conformanceprobeboth fail. A focused exact-head remote validation has also failed; the full exact-head remote build has not yet reached a terminal receipt. No merge has been attempted.Note
Medium Risk
Large proof-only surface area with no runtime logic changes, but mistakes in TreeMap or storage-bridge lemmas could silently weaken verified properties. CI was still failing on this head at PR open time, so merge should wait on a green full build and fork conformance.
Overview
Lean 4.31 compatibility pass across the compiler and proof libraries: no intended change to compilation or contract semantics, only API and proof-script updates so the tree typechecks against the repinned EVMYulLean and new stdlib.
Data structures and lookups: EVMYulLean storage and account maps move from
Batteries.RBMaptoStd.TreeMap, with proofs rewritten fromfind?/ RBMap lemmas toget?,getElem?_insert, andgetElem?_erase. The state bridge adds local TreeMap insert/lookup helpers and comments out the old RB-tree lemma block.String, hex, and naming:
String.mk/.datagive way toString.ofList,toList, andcopyin hex parsing and internal fresh-name suffix construction, with small proof fixes (e.g.String.length+omega).Native Yul harness: Account/storage projection and
sstore/sloadend-to-end proofs are updated for TreeMap and forbyteArrayGet?via backingdata.nativeStmtWriteNamesfreshness hypotheses consistently use(name : String)where identifiers no longer unify withStringin membership tests. Primitive-call result types drop the nestedYul.Ast.Literalwrapper where EVMYulLean now exposesEvmYul.Literal.Proof ergonomics: Widespread tactic swaps (
simpa→rw/exact,rflwhereExcept.bindsimplifies),simp [-ByteArray.size_data]for size lemmas, and refactored UInt256 / Fin negation and signed-arithmetic proofs to avoid brittlenorm_numon huge literals under 4.31’s dependentFininstances.Reviewed by Cursor Bugbot for commit ef7925f. Bugbot is set up for automated code reviews on this repo. Configure here.