G3: External-call / function-table closure in BridgedSafeStmts

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
 

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

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]),

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