proof(L2): admit the pure exp builtin lane to the compile core (#2084) - #2397
proof(L2): admit the pure exp builtin lane to the compile core (#2084)#2397Th0rgal wants to merge 4 commits into
exp builtin lane to the compile core (#2084)#2397Conversation
Excludes the reserved `builtinExpName` sentinel from `collectExprNames`: it is a marker for the pure `exp` builtin, never a callee identifier reaching the generated Yul, so it cannot collide with a compiler-generated temp name. This keeps `collectExprNames ⊆ exprBoundNames` true on the compile core now that `ExprCompileCore.builtinExp` admits the lane.
Threads the reserved `builtinExpName` lane through the constructor-mode compilation equality, refreshes the axiom audit, and records the surface change in AUDIT.md. Also decomposes `collectExprNames_mem_exprBoundNames_of_core` so the 50-line proof gate stays satisfied.
|
The latest updates on your projects. Learn more about Vercel for GitHub.
|
![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: 72713d0737
ℹ️ 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".
| pure (Verity.Core.Uint256.pow | ||
| (Verity.Core.Uint256.ofNat baseVal) | ||
| (Verity.Core.Uint256.ofNat exponentVal)).val |
There was a problem hiding this comment.
When the exponent comes from a uint256 parameter and is large, this newly reachable arm calls Uint256.pow, which is defined as ofNat (base.val ^ exponent.val) in Verity/Core/Uint256.lean. That materializes an astronomically large Nat before reducing it modulo 2^256, so source-semantics and denotation executions can hang or exhaust memory even though EVM EXP and the EvmYul backend finish using modular square-and-multiply. Compute the power modulo 2^256 incrementally so this admitted lane remains executable over its full input domain.
Useful? React with 👍 / 👎.
Resolves the Codex finding on PR #2397 (discussion r3836627045): the newly reachable builtinExp arm called Uint256.pow, which materialises base.val ^ exponent.val as a raw Nat before reducing mod 2^256, so full-domain uint256 exponents hang the source semantics and denotation. - Verity/Core/Uint256.lean: add powBySquaring (square-and-multiply accumulating acc * base ^ exp mod 2^256) with powBySquaring_val, and powEff with powEff_eq_pow : powEff base exponent = pow base exponent. - SourceSemantics.evalExpr, evalExprWithHelpers, Denote.evalExpr: the exp lane now computes with powEff; proofs bridge to pow via powEff_eq_pow, so the compiler agreement theorems are unchanged. - FunctionBody/Base.lean: evalExpr_lt_evmModulus_core_onExpr uses powEff (bounds proof identical through powEff_eq_pow). - SourceSemanticsFeatureTest.lean: 4 regression examples exercising the lane at exponent 2^256 - 1 (executable, no Nat.pow blow-up), wrap fidelity (3^300), and the helper-aware and denotation evaluators. - artifacts/trust_surface_report.json: regenerated (4 new test-only native_decide examples).
![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. no findings; a human or Codex must still cover the unflagged hunks and proof obligations.
Lean packet budget exceeded: 13 Lean file(s), 722 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: 15 supported / 15 total; Lean 13, trust docs 1, workflow/scripts 1, contracts 0, docs 0
- Changed lines: 722 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/IRGeneration/SupportedSpec.lean (+175/-5), Compiler/Proofs/IRGeneration/FunctionBody/Base.lean (+141/-0), Compiler/Proofs/IRGeneration/SourceSemantics.lean (+76/-5), Verity/Core/Uint256.lean (+61/-0), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanPureBuiltinLemmas.lean (+59/-0)
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 Pushed head: Resolves the current-head P2 finding #2397 (comment) — the |
|
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". |
|
@codex review |
|
Codex Review: Didn't find any major issues. Nice work! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
If Codex has suggestions, it will comment; otherwise it will react with 👍. Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". |
1 participant
Summary
Closes one more Tier-4 external-call/foreign surface from #2084 by giving the pure
expbuiltin a first-class compiler/proof surface instead of leaving it misfiled as a foreign call.pow a b/a ^ bin the EDSL desugars toExpr.externalCall builtinExpName [base, exponent](Verity/Macro/Translate/Expr.lean:3404). That node shape is pure arithmetic — it lowers to the Yulexpbuiltin and never reaches a foreign address — but every unsupported-surface predicate treated it as an opaqueexternalCall, so it was excluded from the compile core and undenoted.This slice admits exactly that one sentinel-keyed shape:
SupportedSpec.lean): all 8 predicates now recurse intobase/exponentwhenname == builtinExpName, and keep their original constant for every otherexternalCall. Genuine foreign calls remain unsupported.ExprCore.lean): newExprCompileCore.builtinExpconstructor.SourceSemantics.lean):evalExpr_externalCall_builtinExp, plus_of_ne/_of_aritylemmas pinning the non-exp behaviour.Verity/Core/Model/Denote.lean): the exp lane denotes without an oracle; otherexternalCalls staynone.FunctionBody/Base.lean):evalIRExpr_exp_of_eval,compileExpr_builtinExp_ok,eval_compileExpr_builtinExp_of_compiled.EvmYulLeanPureBuiltinLemmas.lean):evalPureBuiltinViaEvmYulLean_exp_native, proved throughuint256_powAux_toNat/uint256_pow_toNat. Nonative_decide.All four planes agree on
Uint256.pow, i.e.(a % 2^256) ^ (b % 2^256) % 2^256.collectExprNamesconsistency fixValidationHelpers.collectExprNamesprependedbuiltinExpNameto its result. That is a fresh-name-avoidance collector feeding onlypickFreshName(Compile.lean:109/116/123, 308/323/341), andbuiltinExpNameis already in the reserved-identifier list (ValidationCalls.lean:83) so no user can bind it.TrustSurface.collectExternalExprNames:579-583already skips the sentinel identically — this brings the two collectors into agreement. Without it,collectExprNames_mem_exprBoundNames_of_coreis genuinely false for the exp lane and its downstream consumereventCollectExprListNames_subset_scopebreaks.No gate was weakened: the proof-length limit hit on
collectExprNames_mem_exprBoundNames_of_core(52 lines) was resolved by extractingcollectExprNames_builtinExp_split, not by allowlisting.Validation receipts
Forbidden-token scan on added lines vs
origin/main: zero newsorry/admit/axiom/unsafe. Two benign textual hits only — the AUDIT.md prose "Nonative_decide." and the generatedPrintAxioms.leancounter line0 sorry'd.PrintAxioms.leanregenerated viascripts/generate_print_axioms.py: 6849 → 6862 theorems (4918 public, 1944 private, 0 sorry'd). No new axiom, no new trust assumption;AUDIT.mdgains a "PureexpBuiltin Lane (2026-08)" section.Test plan
lake buildgreenlake build PrintAxiomsgreen (note:Compiler.Proofs.IRGeneration.Functionis reachable only through this target)make checkgreen