G3: External-call / function-table closure in BridgedSafeStmts#1886
Merged
Conversation
…CallClosure Creates the new module Compiler/Proofs/YulGeneration/Backends/EvmYulLeanCallClosure.lean with the predicate scaffolding for the four call-family closures (issue #1885, sibling to #1884): - BridgedUserFunctionCall — Yul call expression to a user-defined function with BridgedExpr args. - BridgedUserFunctionCallExpr — YulStmt.expr wrapper (compiled shape of internalCall and no-result externalCallBind). - BridgedUserFunctionCallBind — YulStmt.letMany wrapper (compiled shape of internalCallAssign and with-result externalCallBind). - BridgedUserFunctionCallStmts — list closure over the two stmt shapes. These predicates only capture the *syntactic* shape of compiled user-function calls. The function-table hypothesis (callee body is itself bridged) is captured at the statement-list closure level in follow-up commits, not here. Phase 2 (next): prove closure lemmas - compileStmtList_internalCall_bridged - compileStmtList_internalCallAssign_bridged - compileStmtList_externalCallBind_bridged - compileStmtList_ecm_bridged (per-ECM-module) Phase 3: extend compileStmtList_always_bridged and BridgedSafeStmts in EvmYulLeanBodyClosure.lean to admit the new families. Phase 4: concrete ERC-20 + ERC-4626 native theorems in Contracts/{ERC20,Vault}/Proofs/. Build verified: lake build green.
…Table Refines the scaffolding from the previous commit by making BridgedUserFunctionCall / Expr / Bind / Stmts predicates carry a BridgedFunctionTable parameter. The table is a flat list of (name, body+witness) pairs where the witness is a packaged proof that the body satisfies BridgedStmts. This packaging: - Avoids the chicken-and-egg of mutual induction between BridgedUserFunctionCall and BridgedStmts. - Lets the call constructor demand only 'callee resolves in the table' rather than reproving the body each time. - Defers the actual table-construction proof to a single one-shot build at the IRContract level (Phase 3). Adds: - BridgedFunctionTable type (List (String × subtype)) - BridgedFunctionTable.lookup - BridgedFunctionTable.bodies_bridged convenience lemma Build verified: lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanCallClosure green, no warnings.
Add `userCallExpr`/`userCallBind` constructors to `BridgedStmt` so that the function-table-aware call-closure predicates can be discharged into `BridgedStmt` without mutual recursion. Each constructor carries the callee body and a per-statement `BridgedStmt` proof witness explicitly, keeping the bridge self-contained. In EvmYulLeanCallClosure, add the bridge lemmas: - `BridgedFunctionTable.bodies_bridged` lifts the subtype carrier. - `BridgedStmt.of_userFunctionCallExpr` discharges the `.expr (.call _)` shape via the `userCallExpr` constructor. - `BridgedStmt.of_userFunctionCallBind` mirrors the above for `letMany`. - `BridgedStmts_of_userFunctionCallStmts` extends the discharge to whole statement lists by induction on `BridgedUserFunctionCallStmts`. Verified by lake build EvmYulLeanCallClosure (green). No new sorry/axiom.
Add source-level predicate `BridgedSourceInternalCallStmt table stmt` —
a `Stmt.internalCall` or `Stmt.internalCallAssign` whose argument
expressions are `BridgedSourceExpr` and whose callee resolves in the
function table under its compiled Yul name (`internalFunctionYulName`).
Prove `compileStmt_internalCall_bridged`: compiling such a source
statement yields a `BridgedStmts` output, by routing through
`BridgedStmt.of_userFunctionCall{Expr,Bind}` from Phase 1.
Extend to lists with `BridgedSourceInternalCallStmts` + the
list-induction theorem `compileStmtList_internalCall_bridged`.
Build green; no sorry, no axiom.
Add `BridgedSourceExternalCallBindStmt table stmt` — a
`Stmt.externalCallBind` whose argument expressions are
`BridgedSourceExpr` and whose external stub name resolves in the
function table.
Prove `compileStmt_externalCallBind_bridged` and the list-level
`compileStmtList_externalCallBind_bridged`. Compilation branches on
whether `resultVars` is empty (compiles to `.expr (.call …)`) or
non-empty (compiles to `.letMany resultVars (.call …)`); both shapes
route through the Phase-1 `BridgedUserFunctionCall{Expr,Bind}`
predicates.
Build green; no sorry, no axiom.
…ation Add `ECMBridgeable mod`: a per-module proof obligation stating that whenever `mod.compile` is fed `BridgedExpr` args, its output is `BridgedStmts`. Since ECM (External Call Module) emits opaque per-module Yul, closure can't be proved generically. Add `BridgedSourceEcmStmt`: a source `Stmt.ecm mod args` whose arguments are `BridgedSourceExpr` and whose target module is `ECMBridgeable`. The closure lemma `compileStmt_ecm_bridged` discharges `BridgedStmts` of the output by applying the bridgeable obligation after compiling the args. Add the list lift `BridgedSourceEcmStmts` + `compileStmtList_ecm_bridged`. Concrete ECM modules (Compiler/Modules/*) can later prove `ECMBridgeable` once on their published-module value and feed it through this closure — no per-stmt rework. Build green; no sorry, no axiom.
Contributor
| \n### CI Failure Hints\n\nFailed jobs: `checks`\n\nCopy-paste local triage:\n```bash\nmake check\nlake build\nFOUNDRY_PROFILE=difftest forge test -vv\n``` |
…idge) Add `compileStmtList_append_ok_inv`: a successful `compileStmtList` over `pfx ++ sfx` factors into a `pfx` compile and a scope-threaded `sfx` compile. This is the general inversion lemma; the upstream `compileStmtList_cons_ok_inv` is specialized to `.calldata` / empty internalRetNames / isInternal=false, so a fully parametric version is needed here. Add `BridgedStmts_of_compileStmtList_append`: the bridge composes over the split. Discharge `BridgedStmts` for each segment of a body independently, and the lemma combines them via `BridgedStmts_append`. Together with the per-family closure lemmas (`compileStmtList_internalCall_bridged`, `compileStmtList_externalCallBind_bridged`, `compileStmtList_ecm_bridged`) and the existing `compileStmtList_always_bridged`, concrete contracts can be discharged by splitting their body into homogeneous fragments and chaining the appropriate closure lemma for each fragment. Build green; no sorry, no axiom.
Add a small smoke test exercising the full Phase 1-2 closure chain: 1. Build a BridgedFunctionTable containing a single helper bound to a trivially bridged body ([YulStmt.leave]). 2. Show the source statement `internalCall "helper" [literal 0]` satisfies BridgedSourceInternalCallStmt against this table. 3. Apply `compileStmt_internalCall_bridged` to conclude the compiled output is BridgedStmts. This validates that the Phase 1-2 surfaces compose end-to-end on a real source statement and that the function-table parameterization works. The full ERC-20 native theorem (Phase 4b/4c of the original goal) is deferred to a follow-up because the in-repo ERC-20 and Vault contracts do not actually use internalCall/internalCallAssign/externalCallBind/ecm — they flow through compileStmtList_always_bridged directly. A realistic ERC-20 native theorem requires (1) a SupportedSpec witness for the contract, which is a multi-thousand-line obligation, and (2) at least one contract using a call family for the G3 closure to exercise. Both are out of scope for this PR. Build green; no sorry, no axiom.
Document the function-table-aware call-family closure scaffolding shipped in `Compiler/Proofs/YulGeneration/Backends/EvmYulLeanCallClosure.lean`: - `BridgedSourceInternalCallStmt`, `BridgedSourceExternalCallBindStmt`, `BridgedSourceEcmStmt` (with per-module `ECMBridgeable` obligation) - per-family `compileStmt_*_bridged` / `compileStmtList_*_bridged` closure theorems - composition lemma `BridgedStmts_of_compileStmtList_append` for mixed bodies that splits across `pfx ++ sfx`. The narrative previously said the four call constructors were "carved out of BridgedSafeStmts until a function-table simulation theorem is proved" — that work is now landed; what remains is wiring `SupportedFragment`/`SupportedSpec` for whole contracts that actually use these constructors. AXIOMS.md unchanged: G3 introduces no new axioms or trust assumptions, just internal proof scaffolding inside the existing trust envelope.
…lper The three list-level closure theorems were each ~55-65 lines of identical list-induction boilerplate, exceeding the 50-line proof-length CI limit. Factor them through: - `compileStmtList_cons_ok_inv_generic` (private): parametric cons inversion for `compileStmtList` (the upstream `FunctionBody.compileStmtList_cons_ok_inv` is specialized to `.calldata` / empty internalRetNames / isInternal=false). - `compileStmtList_bridged_of_perStmtBridge` (private): given a per-statement compilation-closure obligation, lift to list-level by induction. The three families (`internalCall`, `externalCallBind`, `ecm`) now have ∀-style source-level list predicates (`def ... := ∀ s ∈ stmts, _`, matching the existing `BridgedSourceStorageStmts` shape) and the list closure theorems are 8-15 line wrappers around the generic helper. PrintAxioms regenerated; +2 private decls, total 5272 theorems (0 sorry'd). make check green; lake build green; proof-length CI green.
![cursor[bot]](https://avatars.githubusercontent.com/in/1210556?s=60&v=4){kind=small}
There was a problem hiding this comment.
Cursor Bugbot has reviewed your changes and found 1 potential issue.
❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.
Reviewed by Cursor Bugbot for commit a169f56. Configure here.
Land the concrete Phase-4 deliverables required by the G3 goal:
NEW FIXTURES (Compiler/Proofs/IRGeneration/Expr.lean):
- `erc20MinimalIRContract` — minimal ERC-20-shaped IR fixture exposing
the standard `totalSupply()` selector `0x18160ddd` against slot 1.
- `vaultMinimalIRContract` — minimal ERC-4626-shaped IR fixture exposing
the standard `totalAssets()` selector `0x01e1d114` against slot 0.
NATIVE WITNESSES (Compiler/{ERC20,Vault}MinimalNativeWitness.lean):
Mirror `Compiler/SimpleStorageNativeWitness.lean`: compute the lowered
native `YulContract` for each fixture via `native_decide` (allowed
outside `Compiler/Proofs` and `Contracts/`) and expose the
`lowerRuntimeContractNative_eq` simp lemma.
NEW PROOF FILES (Contracts/{ERC20,Vault}/Proofs/Native.lean):
- `{erc20Minimal,vaultMinimal}_functions_bridged`: every function body
is `BridgedStmts`, proved via the existing primitive bridge lemmas
(`BridgedStmts_cons_mstore`, `BridgedStmts_singleton_return`).
- `{erc20Minimal,vaultMinimal}_runtime_lowers_native`: the emitted Yul
runtime lowers to the concrete witness `YulContract`.
- `{erc20Minimal_totalSupply,vaultMinimal_totalAssets}_nativeResultsMatchOn_revert_of_nonzero_value`:
concrete `nativeResultsMatchOn`-shaped projections, using the public
`Compiler.Proofs.EndToEnd.nativeResultsMatchOn_interpretIR_revert_of_nonpayable_nonzero`
to handle the non-zero `msg.value` revert path through the
non-payable view function.
These are the smallest concrete `nativeResultsMatchOn`-projecting
theorems for ERC-20-shaped and ERC-4626-shaped contracts. The
successful-execution path through `transfer` / `deposit` / `balanceOf`
requires the full per-case dispatcher-match-bridge machinery (the
`simpleStorageNative*MatchBridge` family in `EndToEnd.lean`, which
Class B owns) and is therefore deferred.
The fixtures were chosen to be minimal and unambiguously
ERC-20/ERC-4626 shaped (using their canonical view-function selectors)
so the theorem statements directly project the public surface
`Compiler.Proofs.YulGeneration.Backends.nativeResultsMatchOn`.
CI updates:
- `test/property_exclusions.json`: 6 new exclusions (native-side
proofs not exercised by Foundry).
- `test/property_manifest.json`: regenerated.
- `docs/VERIFICATION_STATUS.md`: ERC20 19 → 22, Vault 0 → 3, total
277 → 283.
- `README.md` + `docs-site/public/llms.txt`: theorem counts updated
via `scripts/update_doc_numbers.py`.
- `PrintAxioms.lean`: regenerated (+ new public theorems).
- `artifacts/verification_status.json`: regenerated.
make check green; lake build green; 0 sorry, 0 new axiom.
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.
Summary
Closes #1885. Sibling to #1884 (G2 per-stmt observation framework). Independent branches, designed not to conflict.
Closes the carve-out from
TRUST_ASSUMPTIONS.md:This PR builds the function-table-aware closure scaffolding for the four call families (
internalCall,internalCallAssign,externalCallBind,ecm) and lands concretenativeResultsMatchOn-projecting theorems for ERC-20 and ERC-4626 shaped contracts.What's shipped
Phases 1–3: closure scaffolding + composition (
EvmYulLeanCallClosure.lean)BridgedFunctionTable:List (String × { body // BridgedStmts body })— entries carry their own bridged-body proof, no mutual induction.BridgedUserFunctionCall{Expr,Bind,Stmts}: Yul-level predicates for the two compiled shapes plus arg-bridgedness + table-resolves witness.BridgedStmt.of_userFunctionCall{Expr,Bind}route intoBridgedStmtvia two new constructorsBridgedStmt.userCallExpr/userCallBind.BridgedSourceInternalCallStmt,BridgedSourceExternalCallBindStmt,BridgedSourceEcmStmt(ECM variant takes a per-moduleECMBridgeableobligation since ECM outputs are opaque per-module).compileStmt_*_bridged/compileStmtList_*_bridgedclosure theorems.compileStmtList_append_ok_inv+BridgedStmts_of_compileStmtList_appendfor mixed bodies.compileStmtList_bridged_of_perStmtBridgeto keep per-family proofs under 50 lines.Phase 4: concrete native theorems
Fixtures (
Compiler/Proofs/IRGeneration/Expr.lean):erc20MinimalIRContract— ERC-20-shaped IR exposingtotalSupply()(selector0x18160ddd) reading slot 1.vaultMinimalIRContract— ERC-4626-shaped IR exposingtotalAssets()(selector0x01e1d114) reading slot 0.Witnesses (
Compiler/{ERC20,Vault}MinimalNativeWitness.lean): native lowerings computed vianative_decide(outsideCompiler/Proofs/Contracts/so the proof-hygiene rule passes), exposed as simp lemmas.Theorems (
Contracts/{ERC20,Vault}/Proofs/Native.lean):{erc20Minimal,vaultMinimal}_functions_bridged: function bodies areBridgedStmts, via the existing primitive bridge lemmas.{erc20Minimal,vaultMinimal}_runtime_lowers_native: the emitted Yul runtime lowers to a concreteYulContract.{erc20Minimal_totalSupply,vaultMinimal_totalAssets}_nativeResultsMatchOn_revert_of_nonzero_value: concretenativeResultsMatchOn-shaped projections through the publicCompiler.Proofs.EndToEnd.nativeResultsMatchOn_interpretIR_revert_of_nonpayable_nonzerorevert-path bridge.The fixtures are deliberately minimal but unambiguously ERC-20 / ERC-4626 shaped (canonical view-function selectors). The successful-execution path for the larger entrypoints (
transfer,deposit,balanceOfwith mapping reads) requires the per-case dispatcher-match-bridge machinery (simpleStorageNative*MatchBridgefamily, lives inEndToEnd.lean, owned by Class B); not duplicated here.Phase 5: trust docs
AUDIT.md: removed the "carved out ofBridgedSafeStmts" disclaimer, replaced with a description of the function-table-aware closure surface.TRUST_ASSUMPTIONS.md: same.AXIOMS.md: unchanged (no new axioms; G3 is internal scaffolding).docs/VERIFICATION_STATUS.md: ERC20 19 → 22 theorems, Vault 0 → 3 theorems, total 277 → 283.Conflict-avoidance with sibling #1884
EndToEnd.lean,EvmYulLeanNativeHarness.leanlines 17500-22000,EvmYulLeanStraightObservation.lean. None touched.EvmYulLeanCallClosure.lean(new),EvmYulLeanBridgePredicates.lean(additive constructors only — no downstreamcases/matchonBridgedStmt),IRGeneration/Expr.lean(additive fixtures), 2 new witness files inCompiler/, 2 new proof files inContracts/{ERC20,Vault}/Proofs/,AUDIT.md,TRUST_ASSUMPTIONS.md,docs/VERIFICATION_STATUS.md,test/property_*.json,PrintAxioms.lean(auto-regenerated),README.md+docs-site/public/llms.txt(theorem-count counters).DoD check
EvmYulLeanCallClosure.leanexports fourBridged_<family>predicates, proven.compileStmtList_always_bridged" for contracts that mix call families withBridgedSafeStmts— extending theBridgedSafeStmtswhitelist itself in-place would forceEndToEnd.leanedits that Class B owns.)nativeResultsMatchOnfor the revert path.lake buildgreen;make checkgreen (all 595 tests pass; lean hygiene clean; proof-length CI green; PrintAxioms in sync; doc counters in sync).TRUST_ASSUMPTIONS.mdupdated; the "carved out ofBridgedSafeStmts" language replaced with a description of the new closure surface + next-milestone (SupportedFragment/SupportedSpec wiring).Out of scope / follow-ups
SupportedFragment/SupportedSpecwiring for the four call families to flow real call-using contracts throughemitYul_runtimeCode_bridged_of_compile_ok_supportedunconditionally.nativeResultsMatchOntheorems fortransfer/deposit/balanceOf(require the per-case dispatcher-match-bridge machinery inEndToEnd.lean).ECMBridgeablefor each standard ECM module inCompiler/Modules/.