proof(L2): admit calldatacopy into the proved statement surface (#2084 slice 1) - #2385
Merged
Conversation
…evel surface Add a shared word-granular calldatacopy memory model and wire it through the source executors and IR interpreter so the low-level surface no longer has to reject calldatacopy outright. Fan-out to induction sites is still pending. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…d native bridge Adds the runtime/IR memory transfer lemma, the CompiledStmtStep witness, the BridgedStraightStmt/BridgedSourceCalldatacopyStmt bridge chain, and the calldatacopySingle arms at every SupportedStmtList induction site. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…mmas The new 3-arg `calldatacopy` case in execIRStmt/execIRStmtWithInternals overlaps the generic `.call func args` arms, so the conservative-extension and opaque-call lemmas now split on it explicitly. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
…cipline Extends Denote.execStmt with the calldatacopy memory write so the denotation/source-semantics agreement stays definitional, and adds the matching StmtListScopeCore constructor now that the contract surface recurses into calldatacopy's subexpressions. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Records the new BridgedSafeStmts coverage for singleton calldatacopy bodies in the EndToEnd trust-boundary summary, so the doc tracks the surface flip. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Adds the seven new public calldatacopy lemmas (and six private helpers) to the axiom audit list. Total moves 6696 -> 6709 with the sorry count still at zero. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Restores returnValues/returnArray to the rfl group in execStmt_eq, which an earlier edit had accidentally rerouted through denote_stmt_arm, and recompacts the arm so the theorem stays at its original length. Allowlists the calldatacopy preserves proof alongside its mstore/tstore siblings. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Making the core surface recurse into calldatacopy's subexpressions removed the hcore contradiction that previously discharged this case through the catch-all arm, so derive the contract surface from the three subexpression witnesses the way the mstore/tstore arm does. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
StmtListScopeCore gained a calldatacopy constructor without its StmtListScopeDiscipline counterpart, leaving the two Core-to-Discipline conversions with no constructor to produce. Adds the constructor and the matching alternative in all three inductions. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
The interpreter feature matrix still listed `Stmt.calldatacopy` as a codegen no-op outside the proof-backed subset. Both source interpreters, the IR interpreter, and the supported-fragment now model the word-granular calldata->memory copy, so move it to the proved tier and drop it from the not-modeled proof-boundary catalog and the linear-memory boundary notes. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
Member
Author
|
@codex review |
|
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_76c02d1a-8b7e-4eab-9344-04c66da05af7) |
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
Contributor
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: 21 Lean file(s), 1040 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: 25 supported / 27 total; Lean 21, trust docs 0, workflow/scripts 3, contracts 0, docs 1
- Changed lines: 1040 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/GenericInduction/Storage.lean (+203/-0), Compiler/Proofs/IRGeneration/IRInterpreter.lean (+123/-32), Compiler/Proofs/IRGeneration/SupportedSpec.lean (+135/-14), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure/Base.lean (+120/-0), Compiler/Proofs/IRGeneration/GenericInduction/Scope.lean (+105/-1)
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.
…surface # Conflicts: # PrintAxioms.lean
…surface # 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_0afc4213-8651-4d98-ae6f-8fbebe75a02c) |
Contributor
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: 21 Lean file(s), 1040 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: 25 supported / 27 total; Lean 21, trust docs 0, workflow/scripts 3, contracts 0, docs 1
- Changed lines: 1040 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/GenericInduction/Storage.lean (+203/-0), Compiler/Proofs/IRGeneration/IRInterpreter.lean (+123/-32), Compiler/Proofs/IRGeneration/SupportedSpec.lean (+135/-14), Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBodyClosure/Base.lean (+120/-0), Compiler/Proofs/IRGeneration/GenericInduction/Scope.lean (+105/-1)
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
First slice of #2084 (Tier 4). Takes
Stmt.calldatacopyout of the unsupportedlow-level surface by giving it real semantics on every interpreter in the chain,
rather than by weakening a predicate.
What changed
calldatacopyused to be a codegen no-op on the source side and an opaquefallthrough on the IR side, which is why it sat in
stmtTouchesUnsupportedLowLevelSurface(and in the core / state / call / helper/ internal-helper / foreign / contract / constructor-raw-calldata surfaces) as an
unconditional
true.compiler-free denotation (
Verity/Core/Model/Denote.lean), in both sourceinterpreters (basic and fuel,
SourceSemantics.lean), and in the IRinterpreter (
IRInterpreter.lean), all sharingYulGeneration.calldatacopyWritesAt/calldatacopyMemoryso the threelayers agree by construction.
...TouchesUnsupported*Surfacearm forcalldatacopynow recurses into its three operand expressions instead of returning
true,so a
calldatacopywhose destination, source, and size areExprCompileCoreis inside the supported fragment.
SupportedStmtList.calldatacopySingleconstructor,matching
BridgedSafeStmtscoverage(
bridgedSafeStmts_calldatacopySingle_of_exprCompileCore), generic-inductionarms (
stmtListGenericCore_of_supportedStmtList_calldatacopySingle_of_surface),scope discipline, and the native-harness preservation arm.
IRStmtPreservesObsAt_of_calldatacopyis strengthened: it no longer claims thestate is unchanged, it produces the actual copied state, and the opaque
expr_callfallthrough lemma now explicitly excludes"calldatacopy".Scope / what is deferred
Of the four builtins named in the issue's low-level bullet,
returndataSizeandreturndataOptionalBoolAtwere already off the low-level surface onmain; thisslice lands
calldatacopy.returndataCopyandrevertReturndataremaintrue: they need returndata modeled as an observable component of the callframe, which is the CallFrame line from #2362 and is left to a following slice.
The
call/foreignsurfaces are untouched.Docs
The interpreter feature matrix listed
calldatacopyasno_op/n/a/not_modeled; it moves to the proved tier (statement features 24 -> 25 proved,6 -> 5 not-modeled), and it is dropped from the not-modeled proof-boundary
catalog and from the linear-memory boundary notes in
docsync.pyand thedocs-site pages those notes are checked against.
Test plan
All at head
9e9d00c2:lake build-> exit 0 (2473 jobs)lake build PrintAxioms-> exit 0 (2617 jobs); 6709 theorems/lemmas, 0 sorry'd (was 6696; +13, all calldatacopy arms). Axiom surface unchanged frommain:propext/Classical.choice/Quot.soundplus the three pre-existing native_decide contract witnesses andsolidityMappingSlot_injective.make check-> exit 0 ("All checks passed.")python3 scripts/generate_trust_surface_report.py --check-> exit 0 (no native_decide / implemented_by delta, report already up to date)sorry/admit/axiom/native_decide/implemented_by/unsafe) -> only match is the regenerated-- Total: ... 0 sorry'dheader commentgit diff --check-> exit 0No merge, no thread resolution.
Note
Medium Risk
Large, cross-cutting proof and interpreter changes to memory/calldata semantics; risk is mitigated by aligned helpers across layers and parity with existing
mstore/tstorepatterns, but regressions in IR/source agreement would affect correctness claims.Overview
Stmt.calldatacopyis no longer a no-op / opaque IR fallthrough. Destination, source, and size are evaluated and memory is updated via shared helperscalldatacopyWritesAt,calldataloadWord, andcalldatacopyMemoryinYulGeneration/Calldata.lean, mirrored inVerity/Core/Model/Denote.lean,SourceSemantics.lean, andIRInterpreter.lean.Unsupported-surface predicates now recurse on the three operands instead of marking
calldatacopyunconditionally unsupported (including the former low-level surface), so bodies in theSupportedFragment.calldatacopySingleshape enter the proved fragment. New proof plumbing matchesmstore/tstore:CompiledStmtStep_calldatacopy_single,runtimeStateMatchesIR_calldatacopyBothMemory, scope discipline, generic induction,BridgedSafeStmts/ Yul bridge predicates, and a dedicateddenote_stmt_arminDenoteAgreement.lean. IR lemmas treatcalldatacopyas a real builtin (not opaqueexpr_call), including updatedIRStmtPreservesObsAt_of_calldatacopy.Docs and artifacts: interpreter feature matrix and docs-site copy move
calldatacopyto proved; linear-memory boundary text no longer lists it among partially modeled intrinsics.PrintAxiomsregisters the new public theorems (+13 lemmas, still 0 sorry).Reviewed by Cursor Bugbot for commit e50ccba. Bugbot is set up for automated code reviews on this repo. Configure here.