proof(L2): admit the pure exp builtin lane to the compile core (#2084)

AUDIT.md

@@ -333,6 +333,41 @@ sibling entrypoint.
   `Stmt.revertReturndata`, `extcodesize`, and `externalCallBind` remain
   unmodeled.
 
+## Pure `exp` Builtin Lane (2026-08)
+
+- `pow a b` / `a ^ b` in the EDSL lowers to
+  `Expr.externalCall builtinExpName [base, exponent]`, a reserved sentinel that
+  the compiler already lowered to the pure Yul `exp` builtin rather than to a
+  foreign call. The node shape made it look like an external call to every
+  proof-side surface predicate, so the whole arm was gated as Tier-4 foreign
+  behaviour. That gate is now keyed on the sentinel: the eight
+  `exprTouchesUnsupported*Surface` / `exprTouchesInternalHelperSurface`
+  predicates recurse into `base`/`exponent` for `builtinExpName` at arity two
+  and keep their previous fail-closed constant for every other
+  `Expr.externalCall`.
+- The lane is executed, not assumed, at all four planes: `SourceSemantics`
+  (`evalExpr`, `evalExprWithHelpers`), the compiler-free denotation
+  (`Denote.evalExpr`, with `DenoteAgreement` extended), the IR interpreter
+  (which routes `"exp"` to the EVMYulLean backend), and EVMYulLean itself.
+  All four denote `Uint256.pow`, i.e. `(a % 2^256) ^ (b % 2^256) % 2^256`.
+- `evalPureBuiltinViaEvmYulLean_exp_native` closes the backend leg by proving
+  `EvmYul.UInt256.exp` equals that value, via `uint256_powAux_toNat` /
+  `uint256_pow_toNat` on the square-and-multiply loop. No `native_decide`.
+- `ExprCompileCore.builtinExp` admits the lane to the generic compile core, so
+  `pow` may appear in generic-fragment expressions, `require` conditions, and
+  `emit` arguments. `compileExpr_builtinExp_ok` and
+  `eval_compileExpr_builtinExp_of_compiled` prove compilation and evaluation
+  agreement against `YulExpr.call "exp"`.
+- `collectExprNames` no longer reports `builtinExpName` as a callee identifier.
+  The sentinel never reaches generated Yul (it becomes `exp`) and is already a
+  reserved name, so it cannot collide with a compiler-generated temp. This
+  matches `TrustSurface.collectExternalExprNames`, which has always skipped it,
+  and it restores `collectExprNames ⊆ exprBoundNames` on the compile core.
+- No new axiom and no new trust assumption: this eliminates an unsupported
+  surface rather than assuming one, and it removes `pow` from the assumed
+  external-call bucket. Genuine `Expr.externalCall` targets, `Expr.call` /
+  `staticcall` / `delegatecall`, and `Stmt.externalCallBind` remain gated.
+
 ## Audit Artifacts
 
 | Artifact | Purpose | Check |

Compiler/CompilationModel/ValidationHelpers.lean

@@ -77,7 +77,12 @@ def collectExprNames : Expr → List String
   | Expr.returndataSize => []
   | Expr.returndataOptionalBoolAt outOffset => collectExprNames outOffset
   | Expr.localVar name => [name]
-  | Expr.externalCall name args => name :: collectExprListNames args
+  | Expr.externalCall name args =>
+      -- `builtinExpName` is a reserved sentinel for the pure `exp` builtin, not a
+      -- callee identifier: it lowers to `YulExpr.call "exp"` and never reaches the
+      -- generated Yul, so it cannot collide with a compiler-generated temp name.
+      if name == builtinExpName then collectExprListNames args
+      else name :: collectExprListNames args
   | Expr.internalCall name args => name :: collectExprListNames args
   | Expr.arrayLength name | Expr.memoryArrayLength name => [name]
   | Expr.paramDynamicHeadWord name _ => [name]

Compiler/Proofs/IRGeneration/DenoteAgreement.lean

@@ -74,7 +74,8 @@ theorem denote_evalExpr_eq (fields : List Field) (s : DenoteState) :
   | .paramDynamicStaticComposite .. | .paramDynamicHeadWord ..
   | .arrayLength _ | .arrayElementWord ..
   | .call .. | .staticcall .. | .delegatecall ..
-  | .externalCall .. | .internalCall ..
+  | .externalCall _ [] | .externalCall _ [_] | .externalCall _ (_ :: _ :: _ :: _)
+  | .internalCall ..
   | .intrinsic .. | .forkIfAtLeast .. | .mulDiv512Down .. | .mulDiv512Up ..
   | .adtConstruct .. | .adtTag .. | .adtField ..
   | .caller | .contractAddress | .txOrigin | .chainid | .msgValue | .selfBalance
@@ -114,6 +115,15 @@ theorem denote_evalExpr_eq (fields : List Field) (s : DenoteState) :
         by_cases h : (v != 0) = true
         · simpa [h] using denote_evalExpr_eq fields s t
         · simpa [h] using denote_evalExpr_eq fields s e
+  -- Both evaluators guard the reserved `exp` builtin lane on the same name
+  -- test, so the arms agree branch-for-branch.
+  | .externalCall _ [base, exponent] => by
+      have guard : ∀ (c : Bool) (x y : Option Nat),
+          x = y → (if c then x else none) = (if c then y else none) := by
+        intro c x y h; cases c <;> simp [h]
+      exact guard _ _ _
+        (bindAgree (denote_evalExpr_eq fields s base) fun _ =>
+          bindAgree (denote_evalExpr_eq fields s exponent) fun _ => rfl)
 
 theorem denote_evalExprList_eq (fields : List Field) (s : DenoteState) :
     ∀ es : List Expr,

Compiler/Proofs/IRGeneration/ExprCore.lean

@@ -196,6 +196,12 @@ inductive ExprCompileCore : Expr → Prop where
   | keccak256 {offset size : Expr} :
       ExprCompileCore offset → ExprCompileCore size →
         ExprCompileCore (.keccak256 offset size)
+  /-- The reserved `exp` builtin lane. `pow`/`^` in the EDSL surfaces as an
+  `externalCall` node, but it lowers to the pure Yul `exp` builtin and carries
+  no foreign behaviour, so it belongs to the compile core. -/
+  | builtinExp {base exponent : Expr} :
+      ExprCompileCore base → ExprCompileCore exponent →
+        ExprCompileCore (.externalCall builtinExpName [base, exponent])
 
 /-! ## Scope analysis -/
 

Compiler/Proofs/IRGeneration/Function.lean

@@ -4472,7 +4472,24 @@ private theorem compileExpr_constructor_mode_eq
       simp only [exprTouchesUnsupportedConstructorRawCalldataSurface] at hraw
       simp [compileExprWithInternals, compileExpr_constructor_mode_eq hcore hcall hraw]
   | .localVar _, _, _, _ => by simp [compileExprWithInternals]
-  | .externalCall _ _, hcore, _, _ => by simp [exprTouchesUnsupportedCoreSurface] at hcore
+  | .externalCall name [base, exponent], hcore, hcall, hraw => by
+      by_cases hname : name = builtinExpName
+      · subst hname
+        simp only [exprTouchesUnsupportedCoreSurface, beq_self_eq_true, if_true,
+          Bool.or_eq_false_iff] at hcore
+        simp only [exprTouchesUnsupportedCallSurface, beq_self_eq_true, if_true,
+          Bool.or_eq_false_iff] at hcall
+        simp only [exprTouchesUnsupportedConstructorRawCalldataSurface,
+          exprListTouchesUnsupportedConstructorRawCalldataSurface, Bool.or_false,
+          Bool.or_eq_false_iff] at hraw
+        simp [compileExprWithInternals, compileExprListWithInternals,
+          compileExpr_constructor_mode_eq hcore.1 hcall.1 hraw.1,
+          compileExpr_constructor_mode_eq hcore.2 hcall.2 hraw.2]
+      · simp [exprTouchesUnsupportedCoreSurface, hname] at hcore
+  | .externalCall _ [], hcore, _, _ => by simp [exprTouchesUnsupportedCoreSurface] at hcore
+  | .externalCall _ [_], hcore, _, _ => by simp [exprTouchesUnsupportedCoreSurface] at hcore
+  | .externalCall _ (_ :: _ :: _ :: _), hcore, _, _ => by
+      simp [exprTouchesUnsupportedCoreSurface] at hcore
   | .internalCall _ _, hcore, _, _ => by simp [exprTouchesUnsupportedCoreSurface] at hcore
   | .arrayLength _, _, hcall, _ => by simp [exprTouchesUnsupportedCallSurface] at hcall
   | .arrayElement _ _, _, hcall, _ => by simp [exprTouchesUnsupportedCallSurface] at hcall

Compiler/Proofs/IRGeneration/FunctionBody/Base.lean

@@ -563,6 +563,25 @@ theorem evalIRExpr_mul_of_eval
     Compiler.Proofs.YulGeneration.Backends.evalBuiltinCallWithEvmYulLeanContext,
     Compiler.Proofs.YulGeneration.Backends.evalBuiltinCallViaEvmYulLean]
 
+theorem evalIRExpr_exp_of_eval
+    {state : IRState}
+    {lhs rhs : YulExpr}
+    {a b : Nat}
+    (hlhs : evalIRExpr state lhs = some a)
+    (hrhs : evalIRExpr state rhs = some b) :
+    evalIRExpr state (YulExpr.call "exp" [lhs, rhs]) =
+      some ((a % Compiler.Constants.evmModulus) ^ (b % Compiler.Constants.evmModulus)
+        % Compiler.Constants.evmModulus) := by
+  simp [evalIRExpr, evalIRCall, evalIRExprs, hlhs, hrhs,
+    Compiler.Proofs.YulGeneration.Backends.evalBuiltinCallWithEvmYulLeanContext,
+    Compiler.Proofs.YulGeneration.Backends.evalBuiltinCallViaEvmYulLean]
+
+private theorem uint256_pow_val (a b : Nat) :
+    (Verity.Core.Uint256.pow (Verity.Core.Uint256.ofNat a) (Verity.Core.Uint256.ofNat b)).val =
+      (a % Compiler.Constants.evmModulus) ^ (b % Compiler.Constants.evmModulus)
+        % Compiler.Constants.evmModulus := by
+  simp [Verity.Core.Uint256.pow, Verity.Core.Uint256.ofNat, Compiler.Constants.evmModulus]
+
 theorem evalIRExpr_div_of_eval
     {state : IRState}
     {lhs rhs : YulExpr}
@@ -2033,6 +2052,56 @@ theorem compileExpr_keccak256_ok
   rw [CompilationModel.compileExpr, CompilationModel.compileExprWithInternals, hoffset, hsize]
   rfl
 
+/-- `pow`/`^` in the EDSL surfaces as `externalCall builtinExpName [base, exponent]`, but the
+compiler lowers it to the pure Yul `exp` builtin rather than emitting a foreign call. -/
+theorem compileExpr_builtinExp_ok
+    {fields : List Field}
+    {base exponent : Expr}
+    {baseIR exponentIR : YulExpr}
+    (hbase : CompilationModel.compileExpr fields .calldata base = Except.ok baseIR)
+    (hexp : CompilationModel.compileExpr fields .calldata exponent = Except.ok exponentIR) :
+    CompilationModel.compileExpr fields .calldata
+        (.externalCall builtinExpName [base, exponent]) =
+      Except.ok (YulExpr.call "exp" [baseIR, exponentIR]) := by
+  rw [← CompilationModel.compileExprWithInternals_nil_eq] at hbase hexp
+  rw [CompilationModel.compileExpr, CompilationModel.compileExprWithInternals]
+  simp only [CompilationModel.compileExprListWithInternals, hbase, hexp]
+  rfl
+
+private theorem eval_compileExpr_builtinExp_of_compiled
+    {fields : List Field}
+    {runtime : SourceSemantics.RuntimeState}
+    {state : IRState}
+    {base exponent : Expr}
+    {baseIR exponentIR : YulExpr}
+    (hbase : CompilationModel.compileExpr fields .calldata base = Except.ok baseIR)
+    (hexp : CompilationModel.compileExpr fields .calldata exponent = Except.ok exponentIR)
+    (hEvalBase : evalIRExpr state baseIR =
+      some (SourceSemantics.evalExpr fields runtime base))
+    (hEvalExp : evalIRExpr state exponentIR =
+      some (SourceSemantics.evalExpr fields runtime exponent)) :
+    evalIRExpr state
+      (CompilationModel.compileExpr fields .calldata
+          (.externalCall builtinExpName [base, exponent]) |>.toOption.getD (YulExpr.lit 0)) =
+      some (SourceSemantics.evalExpr fields runtime
+        (.externalCall builtinExpName [base, exponent])) := by
+  rw [compileExpr_builtinExp_ok hbase hexp]
+  simp only [Except.toOption, Option.getD]
+  rcases hB : evalIRExpr state baseIR with _ | bv
+  · simp [hB] at hEvalBase
+  · rcases hE : evalIRExpr state exponentIR with _ | ev
+    · simp [hE] at hEvalExp
+    · simp only [hB] at hEvalBase
+      simp only [hE] at hEvalExp
+      simp only [Option.pure_def, Option.bind_eq_bind, Option.bind_some] at hEvalBase hEvalExp
+      have hsrcB : SourceSemantics.evalExpr fields runtime base = some bv := by
+        simpa using hEvalBase.symm
+      have hsrcE : SourceSemantics.evalExpr fields runtime exponent = some ev := by
+        simpa using hEvalExp.symm
+      rw [evalIRExpr_exp_of_eval hB hE,
+        SourceSemantics.evalExpr_externalCall_builtinExp fields runtime base exponent]
+      simp [hsrcB, hsrcE, uint256_pow_val]
+
 private theorem eval_compileExpr_keccak256_of_compiled
     {fields : List Field}
     {runtime : SourceSemantics.RuntimeState}
@@ -5108,6 +5177,12 @@ theorem compileExpr_core_ok
       rcases ihS with ⟨sizeIR, hsize⟩
       exact ⟨YulExpr.call "keccak256" [offsetIR, sizeIR],
         compileExpr_keccak256_ok hoffset hsize⟩
+  | builtinExp hB hE ihB ihE =>
+      rename_i base exponent
+      rcases ihB with ⟨baseIR, hbase⟩
+      rcases ihE with ⟨exponentIR, hexp⟩
+      exact ⟨YulExpr.call "exp" [baseIR, exponentIR],
+        compileExpr_builtinExp_ok hbase hexp⟩
 
 mutual
 theorem eval_compileExpr_core_onExpr
@@ -6253,6 +6328,37 @@ theorem eval_compileExpr_core_onExpr
         simpa only [Except.toOption, Option.getD_some] using htmp
       exact eval_compileExpr_keccak256_of_compiled
         hoffset hsize hEvalOff hEvalSize hruntime
+  | builtinExp hB hE ihB ihE =>
+      rename_i base exponent
+      rcases compileExpr_core_ok hB with ⟨baseIR, hbase⟩
+      rcases compileExpr_core_ok hE with ⟨exponentIR, hexp⟩
+      have hexactB : bindingsExactlyMatchIRVarsOnExpr base runtime.bindings state :=
+        bindingsExactlyMatchIRVarsOnExpr_of_subset hexact (by
+          intro name hmem
+          simpa [exprBoundNames, exprListBoundNames] using
+            List.mem_append.mpr (Or.inl hmem))
+      have hexactE : bindingsExactlyMatchIRVarsOnExpr exponent runtime.bindings state :=
+        bindingsExactlyMatchIRVarsOnExpr_of_subset hexact (by
+          intro name hmem
+          simpa [exprBoundNames, exprListBoundNames] using
+            List.mem_append.mpr (Or.inr hmem))
+      have hpresentB := exprBoundNamesPresent_of_subset hpresent (by
+        intro name hmem
+        simpa [exprBoundNames, exprListBoundNames] using List.mem_append.mpr (Or.inl hmem))
+      have hpresentE := exprBoundNamesPresent_of_subset hpresent (by
+        intro name hmem
+        simpa [exprBoundNames, exprListBoundNames] using List.mem_append.mpr (Or.inr hmem))
+      have hEvalBase : evalIRExpr state baseIR =
+          some (SourceSemantics.evalExpr fields runtime base) := by
+        have htmp := ihB hexactB hbounded hpresentB hruntime
+        rw [hbase] at htmp
+        simpa only [Except.toOption, Option.getD_some] using htmp
+      have hEvalExp : evalIRExpr state exponentIR =
+          some (SourceSemantics.evalExpr fields runtime exponent) := by
+        have htmp := ihE hexactE hbounded hpresentE hruntime
+        rw [hexp] at htmp
+        simpa only [Except.toOption, Option.getD_some] using htmp
+      exact eval_compileExpr_builtinExp_of_compiled hbase hexp hEvalBase hEvalExp
 
 theorem eval_compileExpr_core
     {fields : List Field}
@@ -6781,6 +6887,20 @@ theorem evalExpr_lt_evmModulus_core_onExpr
         · trivial
         · simp only [Bind.bind, Option.bind, Pure.pure]
           exact Nat.mod_lt _ (by norm_num [Compiler.Constants.evmModulus])
+  | @builtinExp base exponent _ _ ihB ihE =>
+      show (do
+        let b ← SourceSemantics.evalExpr fields runtime base
+        let e ← SourceSemantics.evalExpr fields runtime exponent
+        some (Verity.Core.Uint256.powEff (Verity.Core.Uint256.ofNat b)
+          (Verity.Core.Uint256.ofNat e)).val) < _
+      rcases SourceSemantics.evalExpr fields runtime base with _ | bv
+      · trivial
+      · rcases SourceSemantics.evalExpr fields runtime exponent with _ | ev
+        · trivial
+        · simp only [Bind.bind, Option.bind, Pure.pure]
+          have hModEq : Verity.Core.Uint256.modulus = Compiler.Constants.evmModulus := rfl
+          exact hModEq ▸ (Verity.Core.Uint256.powEff (Verity.Core.Uint256.ofNat bv)
+            (Verity.Core.Uint256.ofNat ev)).isLt
 end
 
 theorem evalExpr_lt_evmModulus_core
@@ -7260,6 +7380,15 @@ theorem compileRequireFailCond_core_ok
         rw [CompilationModel.compileRequireFailCond]
         rw [← CompilationModel.compileExprWithInternals_nil_eq] at hcompile
         simp [CompilationModel.compileRequireFailCondWithInternals, hcompile]⟩
+  | builtinExp hB hE =>
+      rename_i base exponent
+      rcases compileExpr_core_ok (fields := fields) hB with ⟨baseIR, hbase⟩
+      rcases compileExpr_core_ok (fields := fields) hE with ⟨exponentIR, hexp⟩
+      exact ⟨YulExpr.call "iszero" [YulExpr.call "exp" [baseIR, exponentIR]], by
+        have hcompile := compileExpr_builtinExp_ok hbase hexp
+        rw [CompilationModel.compileRequireFailCond]
+        rw [← CompilationModel.compileExprWithInternals_nil_eq] at hcompile
+        simp [CompilationModel.compileRequireFailCondWithInternals, hcompile]⟩
 
 theorem eval_compileRequireFailCond_core_onExpr
     {fields : List Field}
@@ -7905,6 +8034,18 @@ theorem eval_compileRequireFailCond_core_onExpr
       · simpa using finishIszeroEval (expr := .keccak256 offset size)
           (show ExprCompileCore (.keccak256 offset size) from
             ExprCompileCore.keccak256 hO hS) hexact hpresent hexpr
+  | builtinExp hB hE =>
+      rename_i base exponent
+      rcases compileExpr_core_ok (fields := fields)
+          (show ExprCompileCore (.externalCall builtinExpName [base, exponent]) from
+            ExprCompileCore.builtinExp hB hE) with ⟨exprIR, hexpr⟩
+      refine ⟨YulExpr.call "iszero" [exprIR], ?_, ?_⟩
+      · rw [← CompilationModel.compileExprWithInternals_nil_eq] at hexpr
+        simp [CompilationModel.compileRequireFailCond,
+          CompilationModel.compileRequireFailCondWithInternals, hexpr]
+      · simpa using finishIszeroEval (expr := .externalCall builtinExpName [base, exponent])
+          (show ExprCompileCore (.externalCall builtinExpName [base, exponent]) from
+            ExprCompileCore.builtinExp hB hE) hexact hpresent hexpr
 
 
 end FunctionBody