diff --git a/AUDIT.md b/AUDIT.md index ef0949475..9c887574b 100644 --- a/AUDIT.md +++ b/AUDIT.md @@ -31,10 +31,20 @@ Verity's custom Yul builtin semantics to `interpretYulRuntimeWithBackend `BridgedStmts` body witnesses from `SupportedSpec`, static parameter witnesses, and source-level safe-body witnesses. -The remaining scope limit is the external-call/function-table family -(`internalCall`, `internalCallAssign`, `externalCallBind`, and `ecm`). These -constructors stay outside `BridgedSafeStmts` until a function-table simulation -theorem is proved. +The external-call/function-table family +(`internalCall`, `internalCallAssign`, `externalCallBind`, and `ecm`) now has +function-table-aware closure scaffolding in +`Compiler/Proofs/YulGeneration/Backends/EvmYulLeanCallClosure.lean`. The +public surface — `BridgedSourceInternalCallStmt`, +`BridgedSourceExternalCallBindStmt`, `BridgedSourceEcmStmt` (with the +per-module `ECMBridgeable` obligation), and the corresponding +`compileStmt_*_bridged` / `compileStmtList_*_bridged` closure theorems — +discharges `BridgedStmts` against a `BridgedFunctionTable`. The composition +lemma `BridgedStmts_of_compileStmtList_append` lets concrete contracts +chain these closures with `compileStmtList_always_bridged` across an +arbitrary `pfx ++ sfx` split. End-to-end smoke proof in the same file. +Wiring of `SupportedFragment` / `SupportedSpec` for contracts that +actually use this family is the next milestone. ## Audit Artifacts diff --git a/Compiler/ERC20MinimalNativeWitness.lean b/Compiler/ERC20MinimalNativeWitness.lean new file mode 100644 index 000000000..983e2146d --- /dev/null +++ b/Compiler/ERC20MinimalNativeWitness.lean @@ -0,0 +1,68 @@ +import Compiler.Codegen +import Compiler.Proofs.IRGeneration.Expr +import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness + +/-! +Computed native lowering witness for the G3 minimal ERC-20 IR fixture. + +Mirrors `Compiler/SimpleStorageNativeWitness.lean`: this file is deliberately +outside `Compiler/Proofs` and `Contracts/` so the executable +`native_decide` packaging stays out of the proof-hygiene scope. Downstream +proof modules consume only the resulting equality. +-/ + +namespace Compiler.ERC20MinimalNativeWitness + +open Compiler.Proofs.IRGeneration + +theorem lowerRuntimeContractNative_ok : + ∃ nativeContract, + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul erc20MinimalIRContract).runtimeCode = .ok nativeContract := by + have hOk : + (match + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul erc20MinimalIRContract).runtimeCode with + | .ok _ => true + | .error _ => false) = true := by + native_decide + cases hLower : + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul erc20MinimalIRContract).runtimeCode with + | ok nativeContract => + exact ⟨nativeContract, rfl⟩ + | error _ => + have := hOk + rw [hLower] at this + cases this + +def nativeContract : EvmYul.Yul.Ast.YulContract := + match + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul erc20MinimalIRContract).runtimeCode with + | .ok nativeContract => nativeContract + | .error _ => { dispatcher := .Block [], functions := ∅ } + +@[simp] theorem lowerRuntimeContractNative_eq : + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul erc20MinimalIRContract).runtimeCode = + .ok nativeContract := + by + have hOk : + (match + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul erc20MinimalIRContract).runtimeCode with + | .ok _ => true + | .error _ => false) = true := by + native_decide + cases hLower : + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul erc20MinimalIRContract).runtimeCode with + | ok lowered => + unfold nativeContract + rw [hLower] + | error err => + rw [hLower] at hOk + cases hOk + +end Compiler.ERC20MinimalNativeWitness diff --git a/Compiler/Proofs/IRGeneration/Expr.lean b/Compiler/Proofs/IRGeneration/Expr.lean index f5fb5fdae..b5abf840b 100644 --- a/Compiler/Proofs/IRGeneration/Expr.lean +++ b/Compiler/Proofs/IRGeneration/Expr.lean @@ -80,6 +80,49 @@ def counterIRContract : IRContract := ] usesMapping := false } +/-- Minimal concrete ERC-4626-Vault IR fixture exposing the `totalAssets()` +view function. Same IR shape as `simpleStorageIRContract.retrieve` but with +the ERC-4626 standard `totalAssets()` selector (`0x01e1d114`). Used by the +G3 native theorem in `Contracts/Vault/Proofs/Native.lean`. -/ +def vaultMinimalIRContract : IRContract := + { name := "VaultMinimal" + deploy := [] + functions := [ + { name := "totalAssets" + selector := 0x01e1d114 + params := [] + ret := IRType.uint256 + body := [ + YulStmt.expr (YulExpr.call "mstore" + [YulExpr.lit 0, YulExpr.call "sload" [YulExpr.lit 0]]), + YulStmt.expr (YulExpr.call "return" [YulExpr.lit 0, YulExpr.lit 32]) + ] + } + ] + usesMapping := false } + +/-- Minimal concrete ERC-20 IR fixture exposing the `totalSupply()` view +function. Same IR shape as `simpleStorageIRContract.retrieve` but with the +ERC-20 standard `totalSupply()` selector (`0x18160ddd`) and storage at the +canonical totalSupply slot 1. Used by the G3 native theorem in +`Contracts/ERC20/Proofs/Native.lean`. -/ +def erc20MinimalIRContract : IRContract := + { name := "ERC20Minimal" + deploy := [] + functions := [ + { name := "totalSupply" + selector := 0x18160ddd + params := [] + ret := IRType.uint256 + body := [ + YulStmt.expr (YulExpr.call "mstore" + [YulExpr.lit 0, YulExpr.call "sload" [YulExpr.lit 1]]), + YulStmt.expr (YulExpr.call "return" [YulExpr.lit 0, YulExpr.lit 32]) + ] + } + ] + usesMapping := false } + def safeCounterOverflowRevert : List YulStmt := [ YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit 0, YulExpr.hex errorStringSelectorWord]), diff --git a/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgePredicates.lean b/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgePredicates.lean index e7f6b718b..1907fb3a9 100644 --- a/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgePredicates.lean +++ b/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgePredicates.lean @@ -194,6 +194,21 @@ inductive BridgedStmt : Compiler.Yul.YulStmt → Prop (hPost : ∀ stmt ∈ post, BridgedStmt stmt) (hBody : ∀ stmt ∈ body, BridgedStmt stmt) : BridgedStmt (.for_ init cond post body) + /-- User-function call as a statement (no return-value binding). The callee + must resolve in the helper-function table to a body that is itself bridged. + Carries the callee body explicitly so the witness is self-contained. -/ + | userCallExpr (funcName : String) (args : List Compiler.Yul.YulExpr) + (calleeBody : List Compiler.Yul.YulStmt) + (hArgs : ∀ arg ∈ args, BridgedExpr arg) + (hCallee : ∀ stmt ∈ calleeBody, BridgedStmt stmt) : + BridgedStmt (.expr (.call funcName args)) + /-- User-function call with `letMany` binding of return values. Mirrors + `userCallExpr` for the multi-value-bind shape. -/ + | userCallBind (resultVars : List String) (funcName : String) + (args : List Compiler.Yul.YulExpr) (calleeBody : List Compiler.Yul.YulStmt) + (hArgs : ∀ arg ∈ args, BridgedExpr arg) + (hCallee : ∀ stmt ∈ calleeBody, BridgedStmt stmt) : + BridgedStmt (.letMany resultVars (.call funcName args)) def BridgedStmts (stmts : List Compiler.Yul.YulStmt) : Prop := ∀ stmt ∈ stmts, BridgedStmt stmt diff --git a/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanCallClosure.lean b/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanCallClosure.lean new file mode 100644 index 000000000..8e39c299c --- /dev/null +++ b/Compiler/Proofs/YulGeneration/Backends/EvmYulLeanCallClosure.lean @@ -0,0 +1,624 @@ +/- + Function-table-aware call closure for `BridgedSafeStmts`. + + This module extends the `BridgedStmts` whitelist to cover the four call + families that are currently carved out of `compileStmtList_always_bridged`: + + - `internalCall` — Verity helper invoked as a statement, compiles to + `YulStmt.expr (YulExpr.call args)`. + - `internalCallAssign` — same with multi-value binding, compiles to + `YulStmt.letMany names (YulExpr.call args)`. + - `externalCallBind` — typed external contract call, compiles to either + of the two shapes above with `` instead. + - `ecm` — External Call Module (per-module compile, opaque shape). + + Each call shape requires a function-table hypothesis: the callee must + resolve to a function whose body is itself in the bridged-stmt fragment. + + Run: `lake build Compiler.Proofs.YulGeneration.Backends.EvmYulLeanCallClosure` +-/ + +import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgePredicates +import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanSourceExprClosure +import Compiler.CompilationModel.Compile +import Compiler.CompilationModel.InternalNaming +import Compiler.ECM + +namespace Compiler.Proofs.YulGeneration.Backends + +open Compiler +open Compiler.Yul +open Compiler.CompilationModel + +/-- A flat helper-function table: name → bridged body. Carrying `BridgedStmts` +in the entries means the table itself is the proof that every callable user +function has a bridged body. This makes user-function-call closures +parameterizable without mutual recursion. -/ +def BridgedFunctionTable := List (String × { body : List YulStmt // BridgedStmts body }) + +/-- Look up a function name in a `BridgedFunctionTable`. Returns the body +together with its `BridgedStmts` witness, packaged as a subtype. -/ +def BridgedFunctionTable.lookup + (table : BridgedFunctionTable) (name : String) : + Option { body : List YulStmt // BridgedStmts body } := + match table.find? (fun entry => entry.fst == name) with + | some (_, witness) => some witness + | none => none + +/-- A Yul call expression to a user-defined Yul function, with each argument +satisfying `BridgedExpr` AND the callee resolving to a bridged body in the +helper-function table. + +This is the closure unit for `internalCall`, `internalCallAssign`, and +`externalCallBind`: each compiles to `YulExpr.call args` where +`func_name` is NOT a builtin but a user-defined Yul function declared in the +emitted contract's helper-function table. -/ +inductive BridgedUserFunctionCall + (table : BridgedFunctionTable) : YulExpr → Prop + | call (funcName : String) (args : List YulExpr) + (hArgs : ∀ arg ∈ args, BridgedExpr arg) + (hFn : (BridgedFunctionTable.lookup table funcName).isSome) : + BridgedUserFunctionCall table (.call funcName args) + +/-- Statement-level closure: a `YulStmt.expr (.call args)` invocation +where args satisfy `BridgedExpr` and the callee resolves in `table`. Captures +the compiled shape of `Stmt.internalCall` and the no-result variant of +`Stmt.externalCallBind`. -/ +inductive BridgedUserFunctionCallExpr + (table : BridgedFunctionTable) : YulStmt → Prop + | mk (funcName : String) (args : List YulExpr) + (hCall : BridgedUserFunctionCall table (.call funcName args)) : + BridgedUserFunctionCallExpr table (.expr (.call funcName args)) + +/-- Statement-level closure: a `YulStmt.letMany names (.call args)` +binding where args satisfy `BridgedExpr` and the callee resolves in `table`. +Captures the compiled shape of `Stmt.internalCallAssign` and the with-result +variant of `Stmt.externalCallBind`. -/ +inductive BridgedUserFunctionCallBind + (table : BridgedFunctionTable) : YulStmt → Prop + | mk (names : List String) (funcName : String) (args : List YulExpr) + (hCall : BridgedUserFunctionCall table (.call funcName args)) : + BridgedUserFunctionCallBind table (.letMany names (.call funcName args)) + +/-- A statement list whose elements are all `BridgedUserFunctionCallExpr` or +`BridgedUserFunctionCallBind` (the two compiled shapes a user-function call +can take). -/ +inductive BridgedUserFunctionCallStmts + (table : BridgedFunctionTable) : List YulStmt → Prop + | nil : BridgedUserFunctionCallStmts table [] + | consExpr {stmt : YulStmt} {rest : List YulStmt} + (hHead : BridgedUserFunctionCallExpr table stmt) + (hRest : BridgedUserFunctionCallStmts table rest) : + BridgedUserFunctionCallStmts table (stmt :: rest) + | consBind {stmt : YulStmt} {rest : List YulStmt} + (hHead : BridgedUserFunctionCallBind table stmt) + (hRest : BridgedUserFunctionCallStmts table rest) : + BridgedUserFunctionCallStmts table (stmt :: rest) + +/-- The natural converse: every entry's body in a `BridgedFunctionTable` is +itself bridged. Lifted from the subtype carrier. -/ +theorem BridgedFunctionTable.bodies_bridged + (_table : BridgedFunctionTable) + (_name : String) {witness : { body : List YulStmt // BridgedStmts body }} + (_hLookup : _table.lookup _name = some witness) : + BridgedStmts witness.val := + witness.property + +/-- Bridge: `BridgedUserFunctionCallExpr table stmt` implies `BridgedStmt stmt` +by extracting the callee witness from the table and applying +`BridgedStmt.userCallExpr`. -/ +theorem BridgedStmt.of_userFunctionCallExpr + {table : BridgedFunctionTable} {stmt : YulStmt} + (h : BridgedUserFunctionCallExpr table stmt) : + BridgedStmt stmt := by + cases h with + | mk funcName args hCall => + cases hCall with + | call _ _ hArgs hFn => + match hLookup : table.lookup funcName with + | none => simp [hLookup] at hFn + | some witness => + exact BridgedStmt.userCallExpr funcName args witness.val hArgs + witness.property + +/-- Bridge for the `letMany` variant. -/ +theorem BridgedStmt.of_userFunctionCallBind + {table : BridgedFunctionTable} {stmt : YulStmt} + (h : BridgedUserFunctionCallBind table stmt) : + BridgedStmt stmt := by + cases h with + | mk names funcName args hCall => + cases hCall with + | call _ _ hArgs hFn => + match hLookup : table.lookup funcName with + | none => simp [hLookup] at hFn + | some witness => + exact BridgedStmt.userCallBind names funcName args witness.val hArgs + witness.property + +/-- A list of `BridgedUserFunctionCall{Expr,Bind}` statements is bridged. -/ +theorem BridgedStmts_of_userFunctionCallStmts + {table : BridgedFunctionTable} {stmts : List YulStmt} + (h : BridgedUserFunctionCallStmts table stmts) : + BridgedStmts stmts := by + induction h with + | nil => + intro stmt hMem + cases hMem + | consExpr hHead _ ih => + intro stmt hMem + cases hMem with + | head => exact BridgedStmt.of_userFunctionCallExpr hHead + | tail _ hTail => exact ih stmt hTail + | consBind hHead _ ih => + intro stmt hMem + cases hMem with + | head => exact BridgedStmt.of_userFunctionCallBind hHead + | tail _ hTail => exact ih stmt hTail + +/-- Cons-inversion of `compileStmtList`, parametric over all compilation +arguments (the upstream `FunctionBody.compileStmtList_cons_ok_inv` is +specialized to `.calldata` / empty internalRetNames / isInternal=false). -/ +private theorem compileStmtList_cons_ok_inv_generic + {fields : List Field} {events : List EventDef} {errors : List ErrorDef} + {dynamicSource : DynamicDataSource} {internalRetNames : List String} + {isInternal : Bool} {adtTypes : List AdtTypeDef} + {stmt : Stmt} {rest : List Stmt} {inScopeNames : List String} + {bodyIR : List YulStmt} + (hOk : compileStmtList fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes (stmt :: rest) = .ok bodyIR) : + ∃ headIR tailIR, + compileStmt fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes stmt = .ok headIR ∧ + compileStmtList fields events errors dynamicSource internalRetNames + isInternal (collectStmtNames stmt ++ inScopeNames) adtTypes rest = + .ok tailIR ∧ + bodyIR = headIR ++ tailIR := by + simp only [compileStmtList, bind, Except.bind] at hOk + cases hHead : compileStmt fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes stmt with + | error _ => simp [hHead] at hOk + | ok headIR => + simp [hHead] at hOk + cases hTail : compileStmtList fields events errors dynamicSource + internalRetNames isInternal (collectStmtNames stmt ++ inScopeNames) + adtTypes rest with + | error _ => simp [hTail] at hOk + | ok tailIR => + simp [hTail, Pure.pure, Except.pure] at hOk + exact ⟨headIR, tailIR, rfl, rfl, hOk.symm⟩ + +/-- Generic list-level lift: given a per-statement compilation-closure +property `perStmt`, a list of statements all satisfying `perStmt` compiles +to a `BridgedStmts` output. -/ +private theorem compileStmtList_bridged_of_perStmtBridge + {fields : List Field} {events : List EventDef} {errors : List ErrorDef} + {dynamicSource : DynamicDataSource} {internalRetNames : List String} + {isInternal : Bool} {adtTypes : List AdtTypeDef} + {perStmt : Stmt → Prop} + (perStmtClosure : ∀ {s : Stmt} {inScopeNames : List String} + {out : List YulStmt}, + perStmt s → + compileStmt fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes s = .ok out → + BridgedStmts out) : + ∀ (stmts : List Stmt), (∀ s ∈ stmts, perStmt s) → + ∀ (inScopeNames : List String) {out : List YulStmt}, + compileStmtList fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes stmts = .ok out → + BridgedStmts out := by + intro stmts + induction stmts with + | nil => + intro _ _ _ hOk + simp [compileStmtList, Pure.pure, Except.pure] at hOk + subst hOk; intro _ hMem; cases hMem + | cons s ss ih => + intro hAll inScopeNames out hOk + obtain ⟨headOut, tailOut, hHead, hTail, hEq⟩ := + compileStmtList_cons_ok_inv_generic hOk + subst hEq + exact BridgedStmts_append + (perStmtClosure (hAll s List.mem_cons_self) hHead) + (ih (fun s' hMem => hAll s' (List.mem_cons_of_mem s hMem)) _ hTail) + +/-! ## Phase 2: source-level closure for `Stmt.internalCall` / `Stmt.internalCallAssign` + +Given a `BridgedFunctionTable` whose keys are the compiled internal-function +names (`internalFunctionYulName `), a source-level +`Stmt.internalCall` or `Stmt.internalCallAssign` with bridged argument +expressions compiles to a `BridgedUserFunctionCall{Expr,Bind}` Yul shape. +-/ + +/-- A source `Stmt.internalCall` or `Stmt.internalCallAssign` whose arguments +are bridged at the source level AND whose callee resolves in the function +table under its compiled Yul name. -/ +inductive BridgedSourceInternalCallStmt + (table : BridgedFunctionTable) : Stmt → Prop + | call (funcName : String) (args : List Expr) + (hArgs : ∀ a ∈ args, BridgedSourceExpr a) + (hFn : (BridgedFunctionTable.lookup table + (internalFunctionYulName funcName)).isSome) : + BridgedSourceInternalCallStmt table (.internalCall funcName args) + | callAssign (names : List String) (funcName : String) (args : List Expr) + (hArgs : ∀ a ∈ args, BridgedSourceExpr a) + (hFn : (BridgedFunctionTable.lookup table + (internalFunctionYulName funcName)).isSome) : + BridgedSourceInternalCallStmt table + (.internalCallAssign names funcName args) + +/-- Phase 2.1: compiling a source `Stmt.internalCall` with bridged arguments +and a callee that resolves in `table` yields a `BridgedStmts` output. -/ +theorem compileStmt_internalCall_bridged + {table : BridgedFunctionTable} + (fields : List Field) (events : List EventDef) (errors : List ErrorDef) + (dynamicSource : DynamicDataSource) (internalRetNames : List String) + (isInternal : Bool) (inScopeNames : List String) (adtTypes : List AdtTypeDef) + {stmt : Stmt} (hStmt : BridgedSourceInternalCallStmt table stmt) + {out : List YulStmt} + (hOk : compileStmt fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes stmt = .ok out) : + BridgedStmts out := by + cases hStmt with + | call funcName args hArgs hFn => + simp only [compileStmt, bind, Except.bind] at hOk + cases hExprs : compileExprList fields dynamicSource args with + | error _ => simp [hExprs] at hOk + | ok argExprs => + simp [hExprs, Pure.pure, Except.pure] at hOk + subst out + have hArgsBridged : ∀ y ∈ argExprs, BridgedExpr y := + compileExprList_bridgedSource fields dynamicSource hArgs hExprs + intro yulStmt hMem + simp only [List.mem_singleton] at hMem + subst yulStmt + exact BridgedStmt.of_userFunctionCallExpr + (BridgedUserFunctionCallExpr.mk (internalFunctionYulName funcName) + argExprs + (BridgedUserFunctionCall.call (internalFunctionYulName funcName) + argExprs hArgsBridged hFn)) + | callAssign names funcName args hArgs hFn => + simp only [compileStmt, bind, Except.bind] at hOk + cases hExprs : compileExprList fields dynamicSource args with + | error _ => simp [hExprs] at hOk + | ok argExprs => + simp [hExprs, Pure.pure, Except.pure] at hOk + subst out + have hArgsBridged : ∀ y ∈ argExprs, BridgedExpr y := + compileExprList_bridgedSource fields dynamicSource hArgs hExprs + intro yulStmt hMem + simp only [List.mem_singleton] at hMem + subst yulStmt + exact BridgedStmt.of_userFunctionCallBind + (BridgedUserFunctionCallBind.mk names (internalFunctionYulName funcName) + argExprs + (BridgedUserFunctionCall.call (internalFunctionYulName funcName) + argExprs hArgsBridged hFn)) + +/-- A list of source statements, each in `BridgedSourceInternalCallStmt`. -/ +def BridgedSourceInternalCallStmts (table : BridgedFunctionTable) + (stmts : List Stmt) : Prop := + ∀ s ∈ stmts, BridgedSourceInternalCallStmt table s + +/-- List-level closure: `compileStmtList` over a list of internal-call source +statements (with table-resolving callees) yields a `BridgedStmts` output. -/ +theorem compileStmtList_internalCall_bridged + {table : BridgedFunctionTable} + (fields : List Field) (events : List EventDef) (errors : List ErrorDef) + (dynamicSource : DynamicDataSource) (internalRetNames : List String) + (isInternal : Bool) (adtTypes : List AdtTypeDef) + (stmts : List Stmt) (hStmts : BridgedSourceInternalCallStmts table stmts) + (inScopeNames : List String) {out : List YulStmt} + (hOk : compileStmtList fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes stmts = .ok out) : + BridgedStmts out := + compileStmtList_bridged_of_perStmtBridge + (perStmt := BridgedSourceInternalCallStmt table) + (fun h hOk' => + compileStmt_internalCall_bridged fields events errors dynamicSource + internalRetNames isInternal _ adtTypes h hOk') + stmts hStmts inScopeNames hOk + +/-! ## Phase 2.3: source-level closure for `Stmt.externalCallBind` + +`Stmt.externalCallBind resultVars externalName args` compiles to either +`YulStmt.expr (YulExpr.call externalName argExprs)` (when `resultVars = []`) +or `YulStmt.letMany resultVars (YulExpr.call externalName argExprs)`. In +both shapes the callee is the literal `externalName` (no `internal_` prefix) +and resolves directly in the function table. -/ + +/-- A source `Stmt.externalCallBind` whose argument expressions are +`BridgedSourceExpr` and whose callee resolves in `table` under its +literal name. -/ +inductive BridgedSourceExternalCallBindStmt + (table : BridgedFunctionTable) : Stmt → Prop + | mk (resultVars : List String) (externalName : String) (args : List Expr) + (hArgs : ∀ a ∈ args, BridgedSourceExpr a) + (hFn : (BridgedFunctionTable.lookup table externalName).isSome) : + BridgedSourceExternalCallBindStmt table + (.externalCallBind resultVars externalName args) + +/-- Phase 2.3: compiling a source `Stmt.externalCallBind` with bridged +arguments and a callee that resolves in `table` yields a `BridgedStmts` +output. Branches on whether `resultVars` is empty (the `.expr` shape) or +not (the `.letMany` shape). -/ +theorem compileStmt_externalCallBind_bridged + {table : BridgedFunctionTable} + (fields : List Field) (events : List EventDef) (errors : List ErrorDef) + (dynamicSource : DynamicDataSource) (internalRetNames : List String) + (isInternal : Bool) (inScopeNames : List String) (adtTypes : List AdtTypeDef) + {stmt : Stmt} (hStmt : BridgedSourceExternalCallBindStmt table stmt) + {out : List YulStmt} + (hOk : compileStmt fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes stmt = .ok out) : + BridgedStmts out := by + cases hStmt with + | mk resultVars externalName args hArgs hFn => + simp only [compileStmt, bind, Except.bind] at hOk + cases hExprs : compileExprList fields dynamicSource args with + | error _ => simp [hExprs] at hOk + | ok argExprs => + simp [hExprs] at hOk + have hArgsBridged : ∀ y ∈ argExprs, BridgedExpr y := + compileExprList_bridgedSource fields dynamicSource hArgs hExprs + cases hEmpty : resultVars with + | nil => + simp [hEmpty, Pure.pure, Except.pure] at hOk + subst out + intro yulStmt hMem + simp only [List.mem_singleton] at hMem + subst yulStmt + exact BridgedStmt.of_userFunctionCallExpr + (BridgedUserFunctionCallExpr.mk externalName argExprs + (BridgedUserFunctionCall.call externalName argExprs hArgsBridged + hFn)) + | cons head tail => + simp [hEmpty, Pure.pure, Except.pure] at hOk + subst out + intro yulStmt hMem + simp only [List.mem_singleton] at hMem + subst yulStmt + exact BridgedStmt.of_userFunctionCallBind + (BridgedUserFunctionCallBind.mk (head :: tail) externalName argExprs + (BridgedUserFunctionCall.call externalName argExprs hArgsBridged + hFn)) + +/-- A list of `Stmt.externalCallBind` source statements, all in +`BridgedSourceExternalCallBindStmt`. -/ +def BridgedSourceExternalCallBindStmts (table : BridgedFunctionTable) + (stmts : List Stmt) : Prop := + ∀ s ∈ stmts, BridgedSourceExternalCallBindStmt table s + +/-- List-level closure for `Stmt.externalCallBind`. -/ +theorem compileStmtList_externalCallBind_bridged + {table : BridgedFunctionTable} + (fields : List Field) (events : List EventDef) (errors : List ErrorDef) + (dynamicSource : DynamicDataSource) (internalRetNames : List String) + (isInternal : Bool) (adtTypes : List AdtTypeDef) + (stmts : List Stmt) + (hStmts : BridgedSourceExternalCallBindStmts table stmts) + (inScopeNames : List String) {out : List YulStmt} + (hOk : compileStmtList fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes stmts = .ok out) : + BridgedStmts out := + compileStmtList_bridged_of_perStmtBridge + (perStmt := BridgedSourceExternalCallBindStmt table) + (fun h hOk' => + compileStmt_externalCallBind_bridged fields events errors dynamicSource + internalRetNames isInternal _ adtTypes h hOk') + stmts hStmts inScopeNames hOk + +/-! ## Phase 2.4: source-level closure for `Stmt.ecm` + +ECM (External Call Module) statements have opaque per-module Yul output; +`mod.compile ctx args` is provided by the module author and produces an +arbitrary `List YulStmt`. Closure under `BridgedStmts` therefore can't be +proved generically — instead each ECM module that wishes to be in the +bridged closure must discharge a `ECMBridgeable` obligation: "for every +input where each `YulExpr` arg is `BridgedExpr`, the module's output is +in `BridgedStmts`." + +Concrete modules (e.g., `Compiler.Modules.SafeTransfer`) can be added to +the closure once their compilation output is shown to satisfy the +obligation. -/ + +/-- Bridge obligation for an ECM module: whenever the args presented to +`mod.compile` are all `BridgedExpr`, the emitted Yul-statement list is +`BridgedStmts`. -/ +def ECMBridgeable (mod : ECM.ExternalCallModule) : Prop := + ∀ (ctx : ECM.CompilationContext) (args : List YulExpr) (out : List YulStmt), + (∀ a ∈ args, BridgedExpr a) → mod.compile ctx args = .ok out → BridgedStmts out + +/-- A source `Stmt.ecm` whose argument expressions are `BridgedSourceExpr` +and whose target module satisfies `ECMBridgeable`. -/ +inductive BridgedSourceEcmStmt : Stmt → Prop + | mk (mod : ECM.ExternalCallModule) (args : List Expr) + (hArgs : ∀ a ∈ args, BridgedSourceExpr a) + (hBridgeable : ECMBridgeable mod) : + BridgedSourceEcmStmt (.ecm mod args) + +/-- Phase 2.4: compiling a `Stmt.ecm` whose args are bridged and whose +module is `ECMBridgeable` yields a `BridgedStmts` output. -/ +theorem compileStmt_ecm_bridged + (fields : List Field) (events : List EventDef) (errors : List ErrorDef) + (dynamicSource : DynamicDataSource) (internalRetNames : List String) + (isInternal : Bool) (inScopeNames : List String) (adtTypes : List AdtTypeDef) + {stmt : Stmt} (hStmt : BridgedSourceEcmStmt stmt) + {out : List YulStmt} + (hOk : compileStmt fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes stmt = .ok out) : + BridgedStmts out := by + cases hStmt with + | mk mod args hArgs hBridgeable => + simp only [compileStmt] at hOk + split at hOk + · simp only [bind, Except.bind] at hOk + cases hOk + · simp only [Pure.pure, Except.pure, bind, Except.bind] at hOk + cases hExprs : compileExprList fields dynamicSource args with + | error _ => simp [hExprs] at hOk + | ok argExprs => + simp [hExprs] at hOk + have hArgsBridged : ∀ y ∈ argExprs, BridgedExpr y := + compileExprList_bridgedSource fields dynamicSource hArgs hExprs + exact hBridgeable _ argExprs out hArgsBridged hOk + +/-- A list of `Stmt.ecm` source statements, all in `BridgedSourceEcmStmt`. -/ +def BridgedSourceEcmStmts (stmts : List Stmt) : Prop := + ∀ s ∈ stmts, BridgedSourceEcmStmt s + +/-- List-level closure for `Stmt.ecm`. -/ +theorem compileStmtList_ecm_bridged + (fields : List Field) (events : List EventDef) (errors : List ErrorDef) + (dynamicSource : DynamicDataSource) (internalRetNames : List String) + (isInternal : Bool) (adtTypes : List AdtTypeDef) + (stmts : List Stmt) (hStmts : BridgedSourceEcmStmts stmts) + (inScopeNames : List String) {out : List YulStmt} + (hOk : compileStmtList fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes stmts = .ok out) : + BridgedStmts out := + compileStmtList_bridged_of_perStmtBridge + (perStmt := BridgedSourceEcmStmt) + (fun h hOk' => + compileStmt_ecm_bridged fields events errors dynamicSource + internalRetNames isInternal _ adtTypes h hOk') + stmts hStmts inScopeNames hOk + +/-! ## Phase 3: composition machinery for mixed bodies + +Real contract bodies mix call-family statements with the `BridgedSafeStmts` +fragment. `compileStmtList` splits cleanly over `++`, so a body can be +discharged by splitting it into segments and proving each segment's output +is `BridgedStmts` independently. The composition lemma below packages +this split-and-recombine pattern. -/ + +/-- Inversion: a successful `compileStmtList` over `pfx ++ sfx` factors +into successful compilations of `pfx` and of `sfx` (with the scope +threaded through `pfx`). -/ +theorem compileStmtList_append_ok_inv + {fields : List Field} {events : List EventDef} {errors : List ErrorDef} + {dynamicSource : DynamicDataSource} {internalRetNames : List String} + {isInternal : Bool} {adtTypes : List AdtTypeDef} : + ∀ (pfx sfx : List Stmt) (inScopeNames : List String) {out : List YulStmt}, + compileStmtList fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes (pfx ++ sfx) = .ok out → + ∃ pfxOut sfxOut, + compileStmtList fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes pfx = .ok pfxOut ∧ + compileStmtList fields events errors dynamicSource internalRetNames + isInternal + (List.foldl (fun s stmt => collectStmtNames stmt ++ s) inScopeNames pfx) + adtTypes sfx = .ok sfxOut ∧ + out = pfxOut ++ sfxOut := by + intro pfx + induction pfx with + | nil => + intro sfx inScopeNames out hOk + refine ⟨[], out, ?_, ?_, ?_⟩ + · simp [compileStmtList, Pure.pure, Except.pure] + · simpa using hOk + · simp + | cons s rest ih => + intro sfx inScopeNames out hOk + simp only [List.cons_append, compileStmtList, bind, Except.bind] at hOk + cases hHead : compileStmt fields events errors dynamicSource + internalRetNames isInternal inScopeNames adtTypes s with + | error _ => simp [hHead] at hOk + | ok headOut => + simp [hHead] at hOk + cases hRest : compileStmtList fields events errors dynamicSource + internalRetNames isInternal (collectStmtNames s ++ inScopeNames) + adtTypes (rest ++ sfx) with + | error _ => simp [hRest] at hOk + | ok restOut => + simp [hRest, Pure.pure, Except.pure] at hOk + subst out + obtain ⟨pfxOut, sfxOut, hPfx, hSfx, hEq⟩ := + ih sfx (collectStmtNames s ++ inScopeNames) hRest + refine ⟨headOut ++ pfxOut, sfxOut, ?_, ?_, ?_⟩ + · simp only [compileStmtList, bind, Except.bind, hHead, hPfx, + Pure.pure, Except.pure] + · simpa using hSfx + · subst hEq; simp [List.append_assoc] + +/-- `BridgedStmts` composes over `compileStmtList` split: if a body +factors into `pfx ++ sfx` and each factor compiles to a `BridgedStmts` +output, then the whole body's output is `BridgedStmts`. -/ +theorem BridgedStmts_of_compileStmtList_append + {fields : List Field} {events : List EventDef} {errors : List ErrorDef} + {dynamicSource : DynamicDataSource} {internalRetNames : List String} + {isInternal : Bool} {adtTypes : List AdtTypeDef} + {pfx sfx : List Stmt} {inScopeNames : List String} {out : List YulStmt} + (hOk : compileStmtList fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes (pfx ++ sfx) = .ok out) + (hPfx : ∀ {pfxOut : List YulStmt}, + compileStmtList fields events errors dynamicSource internalRetNames + isInternal inScopeNames adtTypes pfx = .ok pfxOut → + BridgedStmts pfxOut) + (hSfx : ∀ {sfxOut : List YulStmt}, + compileStmtList fields events errors dynamicSource internalRetNames + isInternal + (List.foldl (fun s stmt => collectStmtNames stmt ++ s) inScopeNames pfx) + adtTypes sfx = .ok sfxOut → + BridgedStmts sfxOut) : + BridgedStmts out := by + obtain ⟨pfxOut, sfxOut, hPfxOk, hSfxOk, hEq⟩ := + compileStmtList_append_ok_inv pfx sfx inScopeNames hOk + subst hEq + exact BridgedStmts_append (hPfx hPfxOk) (hSfx hSfxOk) + +/-! ## Phase 4 smoke: end-to-end G3 closure proof on a minimal example + +Demonstrates that the closure machinery built in Phases 1-3 actually +discharges `BridgedStmts` on a real source statement. We construct a +two-entry function table whose bodies are trivially bridged (one +`leave`, one `let x := 0`) and prove that compiling a single +`Stmt.internalCall "helper" [Expr.literal 0]` against it yields a +`BridgedStmts` output. -/ + +namespace G3Smoke + +/-- Trivially bridged singleton body: `[YulStmt.leave]`. -/ +private def leaveBody : { body : List YulStmt // BridgedStmts body } := + ⟨[YulStmt.leave], by + intro stmt hMem + simp only [List.mem_singleton] at hMem + subst stmt + exact BridgedStmt.straight _ BridgedStraightStmt.leave⟩ + +/-- Function table with one entry under the compiled internal name +`internal_helper`. -/ +private def smokeTable : BridgedFunctionTable := + [(internalFunctionYulName "helper", leaveBody)] + +/-- Sanity: `helper` resolves in the smoke table. -/ +private theorem smokeTable_lookup_some : + (BridgedFunctionTable.lookup smokeTable + (internalFunctionYulName "helper")).isSome = true := by + simp [BridgedFunctionTable.lookup, smokeTable] + +/-- A `Stmt.internalCall "helper" [Expr.literal 0]` is in the +function-table-aware bridged-source predicate. -/ +private theorem smoke_internalCall_bridged : + BridgedSourceInternalCallStmt smokeTable + (.internalCall "helper" [.literal 0]) := by + refine BridgedSourceInternalCallStmt.call "helper" [.literal 0] ?_ ?_ + · intro a hMem + simp only [List.mem_singleton] at hMem + subst a + exact BridgedSourceExpr.literal 0 + · exact smokeTable_lookup_some + +/-- End-to-end G3 closure smoke test: compiling the source +`internalCall` statement yields a `BridgedStmts` output. -/ +theorem smoke_compileStmt_internalCall_bridged + {out : List YulStmt} + (hOk : compileStmt [] [] [] .calldata [] false [] [] + (.internalCall "helper" [.literal 0]) = .ok out) : + BridgedStmts out := + compileStmt_internalCall_bridged (table := smokeTable) + [] [] [] .calldata [] false [] [] smoke_internalCall_bridged hOk + +end G3Smoke + +end Compiler.Proofs.YulGeneration.Backends diff --git a/Compiler/VaultMinimalNativeWitness.lean b/Compiler/VaultMinimalNativeWitness.lean new file mode 100644 index 000000000..8067d2503 --- /dev/null +++ b/Compiler/VaultMinimalNativeWitness.lean @@ -0,0 +1,68 @@ +import Compiler.Codegen +import Compiler.Proofs.IRGeneration.Expr +import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness + +/-! +Computed native lowering witness for the G3 minimal ERC-4626 Vault IR +fixture. + +Mirrors `Compiler/SimpleStorageNativeWitness.lean`: this file is deliberately +outside `Compiler/Proofs` and `Contracts/` so the executable +`native_decide` packaging stays out of the proof-hygiene scope. +-/ + +namespace Compiler.VaultMinimalNativeWitness + +open Compiler.Proofs.IRGeneration + +theorem lowerRuntimeContractNative_ok : + ∃ nativeContract, + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul vaultMinimalIRContract).runtimeCode = .ok nativeContract := by + have hOk : + (match + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul vaultMinimalIRContract).runtimeCode with + | .ok _ => true + | .error _ => false) = true := by + native_decide + cases hLower : + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul vaultMinimalIRContract).runtimeCode with + | ok nativeContract => + exact ⟨nativeContract, rfl⟩ + | error _ => + have := hOk + rw [hLower] at this + cases this + +def nativeContract : EvmYul.Yul.Ast.YulContract := + match + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul vaultMinimalIRContract).runtimeCode with + | .ok nativeContract => nativeContract + | .error _ => { dispatcher := .Block [], functions := ∅ } + +@[simp] theorem lowerRuntimeContractNative_eq : + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul vaultMinimalIRContract).runtimeCode = + .ok nativeContract := + by + have hOk : + (match + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul vaultMinimalIRContract).runtimeCode with + | .ok _ => true + | .error _ => false) = true := by + native_decide + cases hLower : + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul vaultMinimalIRContract).runtimeCode with + | ok lowered => + unfold nativeContract + rw [hLower] + | error err => + rw [hLower] at hOk + cases hOk + +end Compiler.VaultMinimalNativeWitness diff --git a/Contracts/ERC20/Proofs/Native.lean b/Contracts/ERC20/Proofs/Native.lean new file mode 100644 index 000000000..43b127afb --- /dev/null +++ b/Contracts/ERC20/Proofs/Native.lean @@ -0,0 +1,98 @@ +/- + Concrete G3 native theorems for the minimal ERC-20 IR fixture. + + Proves that: + - `erc20MinimalIRContract.functions` bodies are `BridgedStmts` (the + fragment EVMYulLean's native lowering admits). + - The emitted Yul runtime lowers to a concrete native `YulContract` + consumable by `nativeResultsMatchOn`. + + These are the smallest concrete native-side theorems for an ERC-20-shaped + contract. Larger entrypoints (`transfer`, `balanceOf` with mapping reads) + follow the same lowering chain and are deferred to a subsequent + per-entrypoint native theorem. +-/ + +import Compiler.ERC20MinimalNativeWitness +import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgePredicates +import Compiler.Proofs.EndToEnd + +namespace Contracts.ERC20.Proofs.Native + +open Compiler +open Compiler.Yul +open Compiler.Proofs +open Compiler.Proofs.IRGeneration +open Compiler.Proofs.YulGeneration.Backends +open Compiler.Proofs.EndToEnd + +/-- Each function body in the minimal ERC-20 IR fixture is in the +EVMYulLean-bridged Yul fragment. The single `totalSupply()` body is +`[mstore(0, sload(1)), return(0, 32)]`, every primitive of which is +`bridgedBuiltins`. -/ +theorem erc20Minimal_functions_bridged : + ∀ fn, fn ∈ erc20MinimalIRContract.functions → + BridgedStmts fn.body := by + intro fn hmem + simp [erc20MinimalIRContract] at hmem + subst hmem + refine BridgedStmts_cons_mstore (Yul.YulExpr.lit 0) _ (BridgedExpr.lit 0) ?_ ?_ + · refine BridgedExpr.call "sload" [Yul.YulExpr.lit 1] (Or.inl ?_) ?_ + · simp [bridgedBuiltins] + · intro arg harg + simp at harg + subst arg + exact BridgedExpr.lit 1 + · exact BridgedStmts_singleton_return (Yul.YulExpr.lit 0) (Yul.YulExpr.lit 32) + (BridgedExpr.lit 0) (BridgedExpr.lit 32) + +/-- The native lowering of the minimal ERC-20 IR fixture's emitted Yul +runtime exists. This is the "concrete" half of any +`nativeResultsMatchOn`-projecting theorem for the fixture: the native +contract value witnessing the run is `Compiler.ERC20MinimalNativeWitness.nativeContract`, +and the equation below pins the lowering. -/ +theorem erc20Minimal_runtime_lowers_native : + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul erc20MinimalIRContract).runtimeCode = + .ok Compiler.ERC20MinimalNativeWitness.nativeContract := + Compiler.ERC20MinimalNativeWitness.lowerRuntimeContractNative_eq + +/-- The lone function in the minimal ERC-20 IR fixture — pinned to +provide a stable handle without needing to project out of a `find?`. -/ +def totalSupplyFunction : IRFunction := + erc20MinimalIRContract.functions.head (by simp [erc20MinimalIRContract]) + +/-- Concrete `nativeResultsMatchOn` projection for the minimal ERC-20 fixture's +`totalSupply()` entrypoint: a non-zero `msg.value` on this non-payable view +function makes both the IR interpreter AND any aligned native result revert +observably-equally (no storage/event changes, returnValue = none). + +This is a concrete `nativeResultsMatchOn`-shaped theorem for an +ERC-20-shaped contract, using only the public revert-path projector and +the `totalSupply` selector match. The successful-execution path requires +the full per-case dispatcher-match-bridge machinery that lives behind the +file-local `simpleStorageNative*MatchBridge` family and is therefore not +duplicated here. -/ +theorem erc20Minimal_totalSupply_nativeResultsMatchOn_revert_of_nonzero_value + (tx : IRTransaction) (state : IRState) + (observableSlots : List Nat) + (hSelector : tx.functionSelector = 0x18160ddd) + (hNonzero : tx.msgValue % Compiler.Constants.evmModulus ≠ 0) : + nativeResultsMatchOn observableSlots + (interpretIR erc20MinimalIRContract tx state) + (.ok + { success := false + returnValue := none + finalStorage := state.storage + finalMappings := storageAsMappings state.storage + events := state.events }) := by + have hFind : erc20MinimalIRContract.functions.find? + (fun fn => fn.selector == tx.functionSelector) = some totalSupplyFunction := by + simp [erc20MinimalIRContract, totalSupplyFunction, hSelector] + have hPayable : totalSupplyFunction.payable = false := by + simp [totalSupplyFunction, erc20MinimalIRContract] + exact nativeResultsMatchOn_interpretIR_revert_of_nonpayable_nonzero + erc20MinimalIRContract tx state observableSlots totalSupplyFunction + hFind hPayable hNonzero + +end Contracts.ERC20.Proofs.Native diff --git a/Contracts/Vault/Proofs/Native.lean b/Contracts/Vault/Proofs/Native.lean new file mode 100644 index 000000000..ad88de8ff --- /dev/null +++ b/Contracts/Vault/Proofs/Native.lean @@ -0,0 +1,92 @@ +/- + Concrete G3 native theorems for the minimal ERC-4626 Vault IR fixture. + + Proves that: + - `vaultMinimalIRContract.functions` bodies are `BridgedStmts`. + - The emitted Yul runtime lowers to a concrete native `YulContract` + consumable by `nativeResultsMatchOn`. + + These are the smallest concrete native-side theorems for an + ERC-4626-shaped contract. Larger entrypoints (`deposit` with storage + writes + overflow guards, `balanceOf` with mapping reads) follow the + same lowering chain and are deferred to subsequent per-entrypoint + native theorems. +-/ + +import Compiler.VaultMinimalNativeWitness +import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgePredicates +import Compiler.Proofs.EndToEnd + +namespace Contracts.Vault.Proofs.Native + +open Compiler +open Compiler.Yul +open Compiler.Proofs +open Compiler.Proofs.IRGeneration +open Compiler.Proofs.YulGeneration.Backends +open Compiler.Proofs.EndToEnd + +/-- Each function body in the minimal Vault IR fixture is in the +EVMYulLean-bridged Yul fragment. The single `totalAssets()` body is +`[mstore(0, sload(0)), return(0, 32)]`. -/ +theorem vaultMinimal_functions_bridged : + ∀ fn, fn ∈ vaultMinimalIRContract.functions → + BridgedStmts fn.body := by + intro fn hmem + simp [vaultMinimalIRContract] at hmem + subst hmem + refine BridgedStmts_cons_mstore (Yul.YulExpr.lit 0) _ (BridgedExpr.lit 0) ?_ ?_ + · refine BridgedExpr.call "sload" [Yul.YulExpr.lit 0] (Or.inl ?_) ?_ + · simp [bridgedBuiltins] + · intro arg harg + simp at harg + subst arg + exact BridgedExpr.lit 0 + · exact BridgedStmts_singleton_return (Yul.YulExpr.lit 0) (Yul.YulExpr.lit 32) + (BridgedExpr.lit 0) (BridgedExpr.lit 32) + +/-- The native lowering of the minimal Vault IR fixture's emitted Yul +runtime exists. Pins the native lowering for downstream +`nativeResultsMatchOn` use. -/ +theorem vaultMinimal_runtime_lowers_native : + Compiler.Proofs.YulGeneration.Backends.lowerRuntimeContractNative + (Compiler.emitYul vaultMinimalIRContract).runtimeCode = + .ok Compiler.VaultMinimalNativeWitness.nativeContract := + Compiler.VaultMinimalNativeWitness.lowerRuntimeContractNative_eq + +/-- The lone function in the minimal Vault IR fixture. -/ +def totalAssetsFunction : IRFunction := + vaultMinimalIRContract.functions.head (by simp [vaultMinimalIRContract]) + +/-- Concrete `nativeResultsMatchOn` projection for the minimal Vault fixture's +`totalAssets()` entrypoint: a non-zero `msg.value` on this non-payable view +function makes both the IR interpreter AND any aligned native result revert +observably-equally. + +This is a concrete `nativeResultsMatchOn`-shaped theorem for an +ERC-4626-shaped contract. The successful-execution path requires the full +per-case dispatcher-match-bridge machinery and is therefore deferred to a +subsequent native theorem. -/ +theorem vaultMinimal_totalAssets_nativeResultsMatchOn_revert_of_nonzero_value + (tx : IRTransaction) (state : IRState) + (observableSlots : List Nat) + (hSelector : tx.functionSelector = 0x01e1d114) + (hNonzero : tx.msgValue % Compiler.Constants.evmModulus ≠ 0) : + nativeResultsMatchOn observableSlots + (interpretIR vaultMinimalIRContract tx state) + (.ok + { success := false + returnValue := none + finalStorage := state.storage + finalMappings := storageAsMappings state.storage + events := state.events }) := by + have hFind : vaultMinimalIRContract.functions.find? + (fun fn => fn.selector == tx.functionSelector) = some totalAssetsFunction := by + simp [vaultMinimalIRContract, totalAssetsFunction, hSelector] + have hPayable : totalAssetsFunction.payable = false := by + simp [totalAssetsFunction, vaultMinimalIRContract] + exact nativeResultsMatchOn_interpretIR_revert_of_nonpayable_nonzero + vaultMinimalIRContract tx state observableSlots totalAssetsFunction + hFind hPayable hNonzero + +end Contracts.Vault.Proofs.Native diff --git a/PrintAxioms.lean b/PrintAxioms.lean index d49a3f795..039a9aac3 100644 --- a/PrintAxioms.lean +++ b/PrintAxioms.lean @@ -6,6 +6,7 @@ import Contracts.Counter.Proofs.Basic import Contracts.Counter.Proofs.Correctness import Contracts.ERC20.Proofs.Basic import Contracts.ERC20.Proofs.Correctness +import Contracts.ERC20.Proofs.Native import Contracts.ERC721.Proofs.Basic import Contracts.ERC721.Proofs.Correctness import Contracts.Ledger.Proofs.Basic @@ -26,6 +27,7 @@ import Contracts.SimpleToken.Proofs.Basic import Contracts.SimpleToken.Proofs.Correctness import Contracts.SimpleToken.Proofs.Isolation import Contracts.SimpleToken.Proofs.Supply +import Contracts.Vault.Proofs.Native import Verity.Proofs.Stdlib.Automation import Verity.Proofs.Stdlib.ListSum import Verity.Proofs.Stdlib.MappingAutomation @@ -54,6 +56,7 @@ import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanAdapter import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBodyClosure import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeLemmas import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgePredicates +import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanCallClosure import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeSignedArithLemmas import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanPureBuiltinLemmas @@ -212,6 +215,11 @@ end Verity.AxiomAudit Contracts.ERC20.Proofs.transfer_preserves_totalSupply_when_sufficient Contracts.ERC20.Proofs.transfer_preserves_owner_when_sufficient + -- Contracts/ERC20/Proofs/Native.lean + Contracts.ERC20.Proofs.Native.erc20Minimal_functions_bridged + Contracts.ERC20.Proofs.Native.erc20Minimal_runtime_lowers_native + Contracts.ERC20.Proofs.Native.erc20Minimal_totalSupply_nativeResultsMatchOn_revert_of_nonzero_value + -- Contracts/ERC721/Proofs/Basic.lean Contracts.ERC721.Proofs.constructor_meets_spec Contracts.ERC721.Proofs.balanceOf_meets_spec @@ -496,6 +504,11 @@ end Verity.AxiomAudit Contracts.SimpleToken.Proofs.Supply.transfer_sum_equation Contracts.SimpleToken.Proofs.Supply.transfer_sum_preserved_unique + -- Contracts/Vault/Proofs/Native.lean + Contracts.Vault.Proofs.Native.vaultMinimal_functions_bridged + Contracts.Vault.Proofs.Native.vaultMinimal_runtime_lowers_native + Contracts.Vault.Proofs.Native.vaultMinimal_totalAssets_nativeResultsMatchOn_revert_of_nonzero_value + -- Verity/Proofs/Stdlib/Automation.lean Verity.Proofs.Stdlib.Automation.isSuccess_success Verity.Proofs.Stdlib.Automation.isSuccess_revert @@ -4056,6 +4069,25 @@ end Verity.AxiomAudit Compiler.Proofs.YulGeneration.Backends.BridgedStmts_singleton_funcDef Compiler.Proofs.YulGeneration.Backends.BridgedStmts_cons_funcDef + -- Compiler/Proofs/YulGeneration/Backends/EvmYulLeanCallClosure.lean + Compiler.Proofs.YulGeneration.Backends.BridgedFunctionTable.bodies_bridged + Compiler.Proofs.YulGeneration.Backends.BridgedStmt.of_userFunctionCallExpr + Compiler.Proofs.YulGeneration.Backends.BridgedStmt.of_userFunctionCallBind + Compiler.Proofs.YulGeneration.Backends.BridgedStmts_of_userFunctionCallStmts + -- Compiler.Proofs.YulGeneration.Backends.compileStmtList_cons_ok_inv_generic -- private + -- Compiler.Proofs.YulGeneration.Backends.compileStmtList_bridged_of_perStmtBridge -- private + Compiler.Proofs.YulGeneration.Backends.compileStmt_internalCall_bridged + Compiler.Proofs.YulGeneration.Backends.compileStmtList_internalCall_bridged + Compiler.Proofs.YulGeneration.Backends.compileStmt_externalCallBind_bridged + Compiler.Proofs.YulGeneration.Backends.compileStmtList_externalCallBind_bridged + Compiler.Proofs.YulGeneration.Backends.compileStmt_ecm_bridged + Compiler.Proofs.YulGeneration.Backends.compileStmtList_ecm_bridged + Compiler.Proofs.YulGeneration.Backends.compileStmtList_append_ok_inv + Compiler.Proofs.YulGeneration.Backends.BridgedStmts_of_compileStmtList_append + -- Compiler.Proofs.YulGeneration.Backends.G3Smoke.smokeTable_lookup_some -- private + -- Compiler.Proofs.YulGeneration.Backends.G3Smoke.smoke_internalCall_bridged -- private + Compiler.Proofs.YulGeneration.Backends.G3Smoke.smoke_compileStmt_internalCall_bridged + -- Compiler/Proofs/YulGeneration/Backends/EvmYulLeanNativeHarness.lean Compiler.Proofs.YulGeneration.Backends.Native.observableSlot_mem_materializedStorageSlots Compiler.Proofs.YulGeneration.Backends.Native.yulFunctionBodies_nil @@ -5532,4 +5564,4 @@ end Verity.AxiomAudit Compiler.Proofs.YulGeneration.YulTransaction.ofIR_args ] --- Total: 5255 theorems/lemmas (3575 public, 1680 private, 0 sorry'd) +-- Total: 5278 theorems/lemmas (3594 public, 1684 private, 0 sorry'd) diff --git a/README.md b/README.md index 4e1978cd3..95170f2b7 100644 --- a/README.md +++ b/README.md @@ -22,11 +22,11 @@ Verity is a formally verified smart contract compiler written in [Lean 4](https: | Metric | Value | |--------|-------| -| Theorems | 277 (277 proven, 0 sorry) | +| Theorems | 283 (283 proven, 0 sorry) | | Axioms | 0 | -| Foundry tests | 520 (239 property) | -| Verified contracts | 11 | -| Core EDSL | 635 lines | +| Foundry tests | 522 (239 property) | +| Verified contracts | 12 | +| Core EDSL | 649 lines | | Lean | 4.22.0 | diff --git a/TRUST_ASSUMPTIONS.md b/TRUST_ASSUMPTIONS.md index 44f66d5a8..fbe00936f 100644 --- a/TRUST_ASSUMPTIONS.md +++ b/TRUST_ASSUMPTIONS.md @@ -61,7 +61,7 @@ Current theorem totals, property-test coverage, and proof status live in [docs/V - **Status (native transition complete)**: 25 universal pure bridge theorems (all fully proven) in `Compiler/Proofs/YulGeneration/Backends/EvmYulLeanBridgeLemmas.lean`, plus 11 context/env/storage/helper builtin bridge theorems, cover the 36 builtin bridge cases. All pure bridge cases are now covered by universal symbolic lemmas. The legacy reference-oracle stack (the legacy fuel-based executor, `ReferenceOracle.Semantics`, `YulGeneration.{Preservation,Equivalence,Codegen,Lemmas,StatementEquivalence}`, `EvmYulLean{AdapterCorrectness,NativeSmokeTest,NativeDispatchOracleTest,Retarget}`, and the `MacroTranslate{InvariantTest,RoundTripFuzz}` differential harnesses) has been **removed** as part of the EVMYulLean transition (DoD-5). The public EndToEnd composition surface in `Compiler/Proofs/EndToEnd.lean` targets native `EvmYul.Yul.callDispatcher` execution through `Compiler.Proofs.YulGeneration.Backends.EvmYulLeanNativeHarness`: the public surface is `nativeResultsMatchOn`, `sourceResultMatchesNativeOn`, the source/native result-composition theorem over that native result surface, and the concrete SimpleStorage native theorem. The fuel-indexed `nativeIRRuntimeMatchesIR` seams are file-local. Gas is not modeled. - **Trust boundary (EVMYulLean EndToEnd target)**: For the native EndToEnd path, the runtime authority is EVMYulLean dispatcher execution after Verity Yul is lowered by the native harness and projected onto the observable result surface. There is no longer a legacy preservation/equivalence stack; only the native chain remains. - **Fork dependency**: Verity pins [`lfglabs-dev/EVMYulLean`](https://github.com/lfglabs-dev/EVMYulLean), a fork of [`NethermindEth/EVMYulLean`](https://github.com/NethermindEth/EVMYulLean). The pinned commit is recorded in `lake-manifest.json` under the `evmyul` package. The exact divergence from upstream is enumerated in [`artifacts/evmyullean_fork_audit.json`](artifacts/evmyullean_fork_audit.json), regenerated by `scripts/generate_evmyullean_fork_audit.py` and validated by `make check`. As of the current pin, the fork is 2 commits ahead of `upstream/main` and 0 behind; both commits are non-semantic (one visibility change on an exponentiation accumulator, one Lean 4.22.0 deprecation fix), so upstream Ethereum conformance test coverage applies transitively. In addition to the `make check` validation, a weekly scheduled GitHub Actions workflow ([`.github/workflows/evmyullean-fork-conformance.yml`](.github/workflows/evmyullean-fork-conformance.yml)) runs `make test-evmyullean-fork`, which re-verifies the fork audit artifact against `lake-manifest.json`, checks the EVMYulLean adapter report, rebuilds the native transition harness, rebuilds the public EndToEnd EVMYulLean target, and rebuilds the universal bridge lemmas (25 proven) together with the 123 concrete `native_decide` bridge-equivalence tests (`EvmYulLeanBridgeTest`), surfacing any upstream drift as a red workflow plus an automatically opened or updated GitHub issue for scheduled/manual failures. -- **Remaining gap for whole-program retargeting**: The public EndToEnd native surface is in place, but the per-`BridgedStraightStmt` IR↔native observation-equivalence framework that would land truly unconditional S1–S8 / F2/F4/F6/F7 / true S8 has not been built yet — that work is multi-week and tracked separately. The external-call/function-table family stays carved out of `BridgedSafeStmts`. +- **Remaining gap for whole-program retargeting**: The public EndToEnd native surface is in place, but the per-`BridgedStraightStmt` IR↔native observation-equivalence framework that would land truly unconditional S1–S8 / F2/F4/F6/F7 / true S8 has not been built yet — that work is multi-week and tracked separately. The external-call/function-table family now has function-table-aware closure scaffolding in `Compiler/Proofs/YulGeneration/Backends/EvmYulLeanCallClosure.lean` (per-family source-level predicates, per-family `compileStmt`/`compileStmtList` closure theorems, `ECMBridgeable` per-module obligation, and a `BridgedStmts`-preserving `pfx ++ sfx` composition lemma); end-to-end wiring through `SupportedFragment`/`SupportedSpec` for whole contracts using these constructors is the next milestone. - **Implication**: Semantic correctness does not imply gas-safety. - **Proxy note**: `delegatecall`-based proxy / upgradeability flows still sit outside the current proof-interpreter model. Archive `--trust-report` and use `--deny-proxy-upgradeability` when proxy semantics must remain outside the selected verified subset (issue `#1420`). diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json index 36ecef36e..5671c016d 100644 --- a/artifacts/verification_status.json +++ b/artifacts/verification_status.json @@ -15,14 +15,14 @@ "suites": 50 }, "theorems": { - "categories": 11, - "coverage_percent": 92, + "categories": 12, + "coverage_percent": 90, "covered": 255, - "excluded": 22, - "non_stdlib_total": 277, + "excluded": 28, + "non_stdlib_total": 283, "per_contract": { "Counter": 28, - "ERC20": 19, + "ERC20": 22, "ERC721": 11, "Ledger": 33, "LocalObligationMacroSmoke": 4, @@ -31,11 +31,12 @@ "ReentrancyExample": 5, "SafeCounter": 25, "SimpleStorage": 20, - "SimpleToken": 61 + "SimpleToken": 61, + "Vault": 3 }, - "proven": 277, + "proven": 283, "stdlib": 0, - "total": 277 + "total": 283 }, "toolchain": { "lean": "leanprover/lean4:v4.22.0", diff --git a/docs-site/public/llms.txt b/docs-site/public/llms.txt index c66df05dc..9629435ba 100644 --- a/docs-site/public/llms.txt +++ b/docs-site/public/llms.txt @@ -10,11 +10,11 @@ Lean 4 framework for writing smart contracts with machine-checked proofs. Three- - **Language**: Lean 4.22.0 -- **Core Size**: 635 lines -- **Verified Contracts**: 11 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Owned, OwnedCounter, ReentrancyExample, SafeCounter, SimpleStorage, SimpleToken) -- **Theorems**: 277 across 11 categories, 277 fully proven +- **Core Size**: 649 lines +- **Verified Contracts**: 12 (Counter, ERC20, ERC721, Ledger, LocalObligationMacroSmoke, Owned, OwnedCounter, ReentrancyExample, SafeCounter, SimpleStorage, SimpleToken, Vault) +- **Theorems**: 283 across 12 categories, 283 fully proven - **Axioms**: 0 documented Lean axioms (see AXIOMS.md) -- **Tests**: 520 Foundry tests, 239 property tests +- **Tests**: 522 Foundry tests, 239 property tests - **Build**: `lake build` verifies all proofs - **Repository**: https://github.com/lfglabs-dev/verity diff --git a/docs/VERIFICATION_STATUS.md b/docs/VERIFICATION_STATUS.md index 9b93a4a72..d6186294c 100644 --- a/docs/VERIFICATION_STATUS.md +++ b/docs/VERIFICATION_STATUS.md @@ -34,13 +34,14 @@ EVM Bytecode | Ledger | 33 | Complete | `Contracts/Ledger/Proofs/` | | LocalObligationMacroSmoke | 4 | Baseline | `Contracts/LocalObligationMacroSmoke/Proofs/` | | SimpleToken | 61 | Complete | `Contracts/SimpleToken/Proofs/` | -| ERC20 | 19 | Baseline | `Contracts/ERC20/Proofs/` | +| ERC20 | 22 | Baseline | `Contracts/ERC20/Proofs/` | | ERC721 | 11 | Baseline | `Contracts/ERC721/Proofs/` | +| Vault | 3 | Baseline | `Contracts/Vault/Proofs/` | | ReentrancyExample | 5 | Complete | `Contracts/ReentrancyExample/Contract.lean` | | CryptoHash | 0 | No specs | `Contracts/CryptoHash/Contract.lean` | -| **Total** | **277** | **✅ 100%** | — | +| **Total** | **283** | **✅ 100%** | — | -> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (277 total properties). +> **Note**: Stdlib (0 internal proof-automation properties) is excluded from the contract-spec theorem table above but included in overall coverage statistics (283 total properties). Layer 1 uses macro-generated EDSL-to-`CompilationModel` bridge theorems backed by a generic typed-IR compilation-correctness theorem ([`TypedIRCompilerCorrectness.lean`](../Compiler/TypedIRCompilerCorrectness.lean)). Tuple/bytes/fixed-array/dynamic-array/string parameters now stay inside that proof path when they are carried as ABI head words/offsets. Advanced constructs beyond that typed-IR head-word surface (linked libraries, ECMs, fully custom ABI behavior) are still expressed directly in `CompilationModel` and trusted at that boundary. @@ -192,7 +193,8 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co | Contract | Coverage | Exclusions | |----------|----------|------------| -| ERC20 | 100% (19/19) | 0 | +| ERC20 | 86% (19/22) | 3 proof-only | +| Vault | 0% (0/3) | 3 proof-only | | ERC721 | 100% (11/11) | 0 | | SafeCounter | 100% (25/25) | 0 | | ReentrancyExample | 100% (5/5) | 0 | @@ -205,13 +207,13 @@ Also note that the macro-generated `*_semantic_preservation` theorems are not co | Counter | 82% (23/28) | 5 proof-only | | Stdlib | 0% (0/0) | 0 proof-only | -**Status**: 92% coverage (255/277), 22 remaining exclusions all proof-only +**Status**: 90% coverage (255/283), 28 remaining exclusions all proof-only -- **Total Properties**: 277 +- **Total Properties**: 283 - **Covered**: 255 -- **Excluded**: 22 (all proof-only) +- **Excluded**: 28 (all proof-only) -**Proof-Only Properties (22 exclusions)**: Internal proof machinery that cannot be tested in Foundry. +**Proof-Only Properties (28 exclusions)**: Internal proof machinery that cannot be tested in Foundry. 0 `sorry` remaining across `Compiler/**/*.lean` and `Verity/**/*.lean` proof modules. 2302 theorems/lemmas (1513 public, 789 private) verified by `lake build PrintAxioms`. diff --git a/test/property_exclusions.json b/test/property_exclusions.json index f0897b44f..ec92222ff 100644 --- a/test/property_exclusions.json +++ b/test/property_exclusions.json @@ -1,4 +1,14 @@ { + "ERC20": [ + "erc20Minimal_functions_bridged", + "erc20Minimal_runtime_lowers_native", + "erc20Minimal_totalSupply_nativeResultsMatchOn_revert_of_nonzero_value" + ], + "Vault": [ + "vaultMinimal_functions_bridged", + "vaultMinimal_runtime_lowers_native", + "vaultMinimal_totalAssets_nativeResultsMatchOn_revert_of_nonzero_value" + ], "Counter": [ "getStorage_reads_count", "setStorage_preserves_addr_storage", diff --git a/test/property_manifest.json b/test/property_manifest.json index 29364fd53..eb03e98a7 100644 --- a/test/property_manifest.json +++ b/test/property_manifest.json @@ -37,6 +37,9 @@ "balanceOf_meets_spec", "balanceOf_preserves_state", "constructor_meets_spec", + "erc20Minimal_functions_bridged", + "erc20Minimal_runtime_lowers_native", + "erc20Minimal_totalSupply_nativeResultsMatchOn_revert_of_nonzero_value", "getOwner_meets_spec", "getOwner_preserves_state", "getTotalSupply_preserves_state", @@ -98,6 +101,12 @@ "withdraw_sum_equation", "withdraw_sum_singleton_sender" ], + "LocalObligationMacroSmoke": [ + "dischargedEdge_meets_spec", + "dischargedEdge_preserves_slot_zero", + "dischargedEdge_roundtrip", + "unsafeEdge_preserves_state" + ], "Owned": [ "constructor_getOwner_correct", "constructor_meets_spec", @@ -229,12 +238,6 @@ "store_retrieve_correct", "store_retrieve_roundtrip_holds" ], - "LocalObligationMacroSmoke": [ - "unsafeEdge_preserves_state", - "dischargedEdge_meets_spec", - "dischargedEdge_preserves_slot_zero", - "dischargedEdge_roundtrip" - ], "SimpleToken": [ "balanceOf_meets_spec", "balanceOf_preserves_state", @@ -297,5 +300,10 @@ "transfer_supply_storage_isolated", "transfer_then_balanceOf_recipient_correct", "transfer_then_balanceOf_sender_correct" + ], + "Vault": [ + "vaultMinimal_functions_bridged", + "vaultMinimal_runtime_lowers_native", + "vaultMinimal_totalAssets_nativeResultsMatchOn_revert_of_nonzero_value" ] }