Add Uint256 pow macro lowering

Compiler/CompilationModel/ExpressionCompile.lean

@@ -243,7 +243,12 @@ def compileExpr (fields : List Field)
   | Expr.localVar name => pure (YulExpr.ident name)
   | Expr.externalCall name args => do
       let argExprs ← compileExprList fields dynamicSource args
-      pure (YulExpr.call name argExprs)
+      if name == builtinExpName then
+        match argExprs with
+        | [base, exponent] => pure (YulExpr.call "exp" [base, exponent])
+        | _ => throw s!"Compilation error: builtin exp expects 2 args, got {argExprs.length}"
+      else
+        pure (YulExpr.call name argExprs)
   | Expr.internalCall functionName args => do
       let argExprs ← compileExprList fields dynamicSource args
       pure (YulExpr.call (internalFunctionYulName functionName) argExprs)

Compiler/CompilationModel/LogicalPurity.lean

@@ -9,7 +9,9 @@ partial def exprContainsCallLike (expr : Expr) : Bool :=
   | Expr.call _ _ _ _ _ _ _ => true
   | Expr.staticcall _ _ _ _ _ _ => true
   | Expr.delegatecall _ _ _ _ _ _ => true
-  | Expr.externalCall _ _ | Expr.internalCall _ _ => true
+  | Expr.externalCall name args =>
+      if name == builtinExpName then exprListContainsCallLike args else true
+  | Expr.internalCall _ _ => true
   | Expr.mapping _ key | Expr.mappingWord _ key _ | Expr.mappingPackedWord _ key _ _ | Expr.mappingUint _ key
   | Expr.structMember _ key _ =>
       exprContainsCallLike key

Compiler/CompilationModel/TrustSurface.lean

@@ -736,7 +736,10 @@ private def collectAxiomatizedPrimitivesByStatus
 
 private partial def collectExternalExprNames : Expr → List String
   | .externalCall name args =>
-      name :: args.flatMap collectExternalExprNames
+      if name == builtinExpName then
+        args.flatMap collectExternalExprNames
+      else
+        name :: args.flatMap collectExternalExprNames
   | .call gas target value inOffset inSize outOffset outSize =>
       collectExternalExprNames gas ++ collectExternalExprNames target ++ collectExternalExprNames value ++
         collectExternalExprNames inOffset ++ collectExternalExprNames inSize ++

Compiler/CompilationModel/Types.lean

@@ -35,6 +35,8 @@ export Compiler.Constants (errorStringSelectorWord addressMask selectorShift fre
 open Compiler
 open Compiler.Yul
 
+def builtinExpName : String := "__verity_builtin_exp"
+
 /-!
 ## Compilation Model DSL
 

Compiler/CompilationModel/Validation.lean

@@ -270,7 +270,9 @@ def exprReadsStateOrEnv : Expr → Bool
   | Expr.returndataOptionalBoolAt _ => true
   | Expr.dynamicBytesEq _ _ => false
   | Expr.localVar _ => false
-  | Expr.externalCall _ _ | Expr.internalCall _ _ => true
+  | Expr.externalCall name args =>
+      if name == builtinExpName then exprListReadsStateOrEnv args else true
+  | Expr.internalCall _ _ => true
   | Expr.arrayLength _ => false
   | Expr.storageArrayLength _ => true
   | Expr.storageArrayElement _ index => true || exprReadsStateOrEnv index
@@ -338,7 +340,9 @@ def exprWritesState : Expr → Bool
       exprWritesState outOffset
   | Expr.dynamicBytesEq _ _ =>
       false
-  | Expr.externalCall _ _ | Expr.internalCall _ _ => true
+  | Expr.externalCall name args =>
+      if name == builtinExpName then exprListWritesState args else true
+  | Expr.internalCall _ _ => true
   | Expr.adtConstruct _ _ args => exprListWritesState args
   | Expr.extcodesize addr =>
       exprWritesState addr
@@ -592,7 +596,9 @@ mutual
     or externalCall).  Used by `no_external_calls` validation (#1729, Axis 3 Step 1c). -/
 def exprContainsExternalCall : Expr → Bool
   | Expr.call _ _ _ _ _ _ _ | Expr.staticcall _ _ _ _ _ _
-  | Expr.delegatecall _ _ _ _ _ _ | Expr.externalCall _ _ => true
+  | Expr.delegatecall _ _ _ _ _ _ => true
+  | Expr.externalCall name args =>
+      if name == builtinExpName then exprListContainsExternalCall args else true
   | Expr.add a b | Expr.sub a b | Expr.mul a b | Expr.div a b | Expr.sdiv a b
   | Expr.mod a b | Expr.smod a b
   | Expr.bitAnd a b | Expr.bitOr a b | Expr.bitXor a b | Expr.shl a b | Expr.shr a b | Expr.sar a b
@@ -647,7 +653,9 @@ mutual
 def exprMayContainExternalCall : Expr → Bool
   | Expr.internalCall _ _ => true
   | Expr.call _ _ _ _ _ _ _ | Expr.staticcall _ _ _ _ _ _
-  | Expr.delegatecall _ _ _ _ _ _ | Expr.externalCall _ _ => true
+  | Expr.delegatecall _ _ _ _ _ _ => true
+  | Expr.externalCall name args =>
+      if name == builtinExpName then exprListMayContainExternalCall args else true
   | Expr.add a b | Expr.sub a b | Expr.mul a b | Expr.div a b | Expr.sdiv a b
   | Expr.mod a b | Expr.smod a b
   | Expr.bitAnd a b | Expr.bitOr a b | Expr.bitXor a b | Expr.shl a b | Expr.shr a b | Expr.sar a b

Compiler/CompilationModel/ValidationCalls.lean

@@ -41,8 +41,9 @@ def reservedExternalNames
       [dynamicBytesEqCalldataHelperName, dynamicBytesEqMemoryHelperName]
     else
       []
+  let builtins := [builtinExpName]
   let entrypoints := ["fallback", "receive"]
-  (mappingHelpers ++ arrayHelpers ++ arrayElementWordHelpers ++ storageArrayHelpers ++ dynamicBytesEqHelpers ++ entrypoints).eraseDups
+  (mappingHelpers ++ arrayHelpers ++ arrayElementWordHelpers ++ storageArrayHelpers ++ dynamicBytesEqHelpers ++ builtins ++ entrypoints).eraseDups
 
 def firstReservedExternalCollision
     (spec : CompilationModel)
@@ -312,15 +313,19 @@ mutual
 def validateExternalCallTargetsInExpr
     (externals : List ExternalFunction) (context : String) : Expr → Except String Unit
   | Expr.externalCall name args => do
-      match externals.find? (fun ext => ext.name == name) with
-      | none =>
-          throw s!"Compilation error: {context} references unknown external call target '{name}' ({issue732Ref}). Declare it in spec.externals."
-      | some ext =>
-          if args.length != ext.params.length then
-            throw s!"Compilation error: {context} calls external '{name}' with {args.length} args, but spec.externals declares {ext.params.length} ({issue184Ref})."
-          let returns ← externalFunctionReturns ext
-          if returns.length != 1 then
-            throw s!"Compilation error: {context} uses Expr.externalCall '{name}' but spec.externals declares {returns.length} return values; Expr.externalCall requires exactly 1 ({issue184Ref})."
+      if name == builtinExpName then
+        if args.length != 2 then
+          throw s!"Compilation error: {context} calls builtin exp with {args.length} args, expected 2."
+      else
+        match externals.find? (fun ext => ext.name == name) with
+        | none =>
+            throw s!"Compilation error: {context} references unknown external call target '{name}' ({issue732Ref}). Declare it in spec.externals."
+        | some ext =>
+            if args.length != ext.params.length then
+              throw s!"Compilation error: {context} calls external '{name}' with {args.length} args, but spec.externals declares {ext.params.length} ({issue184Ref})."
+            let returns ← externalFunctionReturns ext
+            if returns.length != 1 then
+              throw s!"Compilation error: {context} uses Expr.externalCall '{name}' but spec.externals declares {returns.length} return values; Expr.externalCall requires exactly 1 ({issue184Ref})."
       validateExternalCallTargetsInExprList externals context args
   | Expr.call gas target value inOffset inSize outOffset outSize => do
       validateExternalCallTargetsInExpr externals context gas

Compiler/CompilationModelFeatureTest.lean

@@ -592,6 +592,43 @@ def feeOnModelInlinesContractConstants : Bool :=
 
 example : feeOnModelInlinesContractConstants = true := by native_decide
 
+def uint256PowSmokeLowersToBuiltinExp : Bool :=
+  match Contracts.Smoke.Uint256PowSmoke.scale_modelBody with
+  | [Stmt.letVar "exponent" (Expr.sub (Expr.literal 18) (Expr.param "decimals")),
+      Stmt.return (Expr.externalCall name [Expr.literal 10, Expr.localVar "exponent"])] =>
+      name == builtinExpName
+  | _ => false
+
+example : uint256PowSmokeLowersToBuiltinExp = true := by native_decide
+
+def uint256PowInfixLowersToBuiltinExp : Bool :=
+  match Contracts.Smoke.Uint256PowSmoke.scaleInfix_modelBody with
+  | [Stmt.letVar "exponent" (Expr.sub (Expr.literal 18) (Expr.param "decimals")),
+      Stmt.return (Expr.externalCall name [Expr.literal 10, Expr.localVar "exponent"])] =>
+      name == builtinExpName
+  | _ => false
+
+example : uint256PowInfixLowersToBuiltinExp = true := by native_decide
+
+def uint256PowBuiltinCompilesToYulExp : Bool :=
+  match compileExpr [] .calldata
+      (Expr.externalCall builtinExpName [Expr.param "base", Expr.param "exponent"]) with
+  | .ok (Compiler.Yul.YulExpr.call "exp"
+      [Compiler.Yul.YulExpr.ident "base", Compiler.Yul.YulExpr.ident "exponent"]) => true
+  | _ => false
+
+example : uint256PowBuiltinCompilesToYulExp = true := by native_decide
+
+def uint256PowBuiltinIsNotAnExternalInteraction : Bool :=
+  let expr := Expr.externalCall builtinExpName [Expr.literal 10, Expr.param "exponent"]
+  !exprReadsStateOrEnv expr &&
+    !exprWritesState expr &&
+    !exprContainsCallLike expr &&
+    !exprContainsExternalCall expr &&
+    !exprMayContainExternalCall expr
+
+example : uint256PowBuiltinIsNotAnExternalInteraction = true := by native_decide
+
 def treasuryAddrModelInlinesAddressConstant : Bool :=
   match MacroConstant.treasuryAddr_modelBody with
   | [Stmt.return (Expr.literal 42)] =>
@@ -2233,6 +2270,27 @@ private def effectOnlyExternalBindMismatchSpec : CompilationModel := {
   ]
 }
 
+private def reservedBuiltinExpExternalSpec : CompilationModel := {
+  name := "ReservedBuiltinExpExternal"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "scale"
+      params := [{ name := "exponent", ty := ParamType.uint256 }]
+      returnType := some FieldType.uint256
+      body := [Stmt.return (Expr.externalCall builtinExpName [Expr.literal 10, Expr.param "exponent"])]
+    }
+  ]
+  externals := [
+    { name := builtinExpName
+      params := [ParamType.uint256, ParamType.uint256]
+      returnType := some ParamType.uint256
+      returns := [ParamType.uint256]
+      axiomNames := ["malicious_shadow_exp"]
+    }
+  ]
+}
+
 private def rawLogTraceSmokeSpec : CompilationModel := {
   name := "RawLogTraceSmoke"
   fields := []
@@ -3649,6 +3707,10 @@ set_option maxRecDepth 4096 in
     "effect-only external call bind still rejects non-void externals"
     effectOnlyExternalBindMismatchSpec
     "binds 0 values from external function 'echo', but it returns 1."
+  expectCompileErrorContains
+    "reserved builtin exp name cannot be shadowed by externals"
+    reservedBuiltinExpExternalSpec
+    s!"external declaration '{builtinExpName}' collides with compiler-generated/reserved symbol '{builtinExpName}'"
   expectCompileErrorContains
     "reserved compiler prefix is rejected in ECM result binders"
     reservedEcmResultVarSpec
@@ -4331,6 +4393,9 @@ set_option maxRecDepth 4096 in
   expectTrue "macro externals surface in the trust report"
     (contains macroExternalTrustReport "\"linkedExternals\"" &&
       contains macroExternalTrustReport "\"echo\"")
+  let macroPowTrustReport := emitTrustReportJson [Contracts.Smoke.Uint256PowSmoke.spec]
+  expectTrue "macro pow builtin does not surface as a linked external"
+    (!contains macroPowTrustReport builtinExpName)
   expectTrue "macro constant expressions inline into model bodies"
     MacroConstantSmoke.feeOnModelInlinesContractConstants
   expectTrue "macro address constants inline through the executable and model paths"

Contracts/MacroTranslateInvariantTest.lean

@@ -286,6 +286,7 @@ private def macroSpecs : List CompilationModel :=
   , Contracts.SimpleToken.spec
   , Contracts.ERC20.spec
   , Contracts.ERC721.spec
+  , Contracts.Smoke.Uint256PowSmoke.spec
   , Contracts.Smoke.UintMapSmoke.spec
   , Contracts.Smoke.MappingChainSmoke.spec
   , Contracts.Smoke.MixedMappingChainSmoke.spec
@@ -395,6 +396,7 @@ private def expectedExternalSignatures : List (String × List String) :=
   , ("ERC721", ["balanceOf(address)", "ownerOf(uint256)", "getApproved(uint256)",
       "isApprovedForAll(address,address)", "approve(address,uint256)", "setApprovalForAll(address,bool)",
       "mint(address)", "transferFrom(address,address,uint256)"])
+  , ("Uint256PowSmoke", ["scale(uint256)", "scaleInfix(uint256)"])
   , ("UintMapSmoke", ["setValue(uint256,uint256)", "getValue(uint256)"])
   , ("MappingChainSmoke", ["setApproval(address,address,address,uint256)", "getApproval(address,address,address)"])
   , ("MixedMappingChainSmoke", ["setApproval(address,uint256,address,uint256)", "getApproval(address,uint256,address)"])
@@ -519,6 +521,7 @@ private def expectedExternalSelectors : List (String × List String) :=
       "0x8da5cb5b"])
   , ("ERC721", ["0x70a08231", "0x6352211e", "0x081812fc", "0xe985e9c5", "0x095ea7b3", "0xa22cb465",
       "0x6a627842", "0x23b872dd"])
+  , ("Uint256PowSmoke", ["0x2bec1547", "0x09c39250"])
   , ("UintMapSmoke", ["0x7b8d56e3", "0x0ff4c916"])
   , ("MappingChainSmoke", ["0xd5264fdd", "0xf7531281"])
   , ("MixedMappingChainSmoke", ["0xd3bf29a3", "0xa75ac7f0"])
@@ -813,7 +816,10 @@ private def checkSignedBuiltinSmoke : IO Unit := do
   let loadSigned := loadSigned?.getD { name := "", params := [], returnType := none, returns := [], body := [] }
   expectTrue "SignedBuiltinSmoke: Int256 storage is modeled as a word slot"
     (match Contracts.Smoke.SignedBuiltinSmoke.spec.fields with
-    | [field] => field.name == "signedSlot" && field.ty == FieldType.uint256 && field.slot == some 0
+    | [field] =>
+        field.name == "signedSlot" &&
+        field.ty == FieldType.uint256 &&
+        field.slot == some 0
     | _ => false)
   expectTrue "SignedBuiltinSmoke: signedDiv body uses Expr.sdiv"
     (bodyUsesSignedBuiltin signedDiv.body "Expr.sdiv")

Contracts/MacroTranslateRoundTripFuzz.lean

@@ -46,6 +46,7 @@ private def macroSpecs : List CompilationModel :=
   , Contracts.Vault.spec
   , Contracts.ERC20.spec
   , Contracts.ERC721.spec
+  , Contracts.Smoke.Uint256PowSmoke.spec
   , Contracts.Smoke.UintMapSmoke.spec
   , Contracts.Smoke.MappingChainSmoke.spec
   , Contracts.Smoke.MixedMappingChainSmoke.spec

Contracts/Smoke.lean

@@ -36,6 +36,17 @@ private def genericECMEffectDemoModule : Compiler.ECM.ExternalCallModule where
   axioms := []
   compile := fun _ctx _args => pure []
 
+verity_contract Uint256PowSmoke where
+  storage
+
+  function scale (decimals : Uint256) : Uint256 := do
+    let exponent := sub 18 decimals
+    return (pow 10 exponent)
+
+  function scaleInfix (decimals : Uint256) : Uint256 := do
+    let exponent := sub 18 decimals
+    return (10 ^ exponent)
+
 verity_contract UintMapSmoke where
   storage
     values : Uint256 → Uint256 := slot 0
@@ -1860,6 +1871,7 @@ example (owner : Address) (value : Uint256) (s s' : ContractState) :
 end SpecGenSmoke
 
 #check_contract Contracts.Counter
+#check_contract Uint256PowSmoke
 #check_contract UintMapSmoke
 #check_contract Bytes32Smoke
 #check_contract StorageAddressArraySmoke

Verity/Core/Uint256.lean

@@ -114,6 +114,9 @@ def sub (a b : Uint256) : Uint256 :=
 -- Modular multiplication (wraps at 2^256)
 def mul (a b : Uint256) : Uint256 := ofNat (a.val * b.val)
 
+/-- EVM EXP semantics: exponentiation modulo `2^256`. -/
+def pow (base exponent : Uint256) : Uint256 := ofNat (base.val ^ exponent.val)
+
 -- Division (returns 0 on division by zero, matching EVM)
 def div (a b : Uint256) : Uint256 :=
   if b.val = 0 then ofNat 0 else ofNat (a.val / b.val)
@@ -159,11 +162,13 @@ def willMulOverflow (a b : Uint256) : Bool :=
 instance : HAdd Uint256 Uint256 Uint256 := ⟨add⟩
 instance : HSub Uint256 Uint256 Uint256 := ⟨sub⟩
 instance : HMul Uint256 Uint256 Uint256 := ⟨mul⟩
+instance : HPow Uint256 Uint256 Uint256 := ⟨pow⟩
 instance : HDiv Uint256 Uint256 Uint256 := ⟨div⟩
 instance : HMod Uint256 Uint256 Uint256 := ⟨mod⟩
 instance : Add Uint256 := ⟨add⟩
 instance : Sub Uint256 := ⟨sub⟩
 instance : Mul Uint256 := ⟨mul⟩
+instance : Pow Uint256 Uint256 := ⟨pow⟩
 instance : Div Uint256 := ⟨div⟩
 instance : Mod Uint256 := ⟨mod⟩
 
@@ -179,6 +184,11 @@ theorem mul_eq_of_lt {a b : Uint256} (h : a.val * b.val < modulus) :
   simp [HMul.hMul, mul, ofNat]
   exact Nat.mod_eq_of_lt h
 
+theorem pow_eq_of_lt {a b : Uint256} (h : a.val ^ b.val < modulus) :
+  ((a ^ b : Uint256) : Nat) = a.val ^ b.val := by
+  simp [HPow.hPow, Pow.pow, pow, ofNat]
+  exact Nat.mod_eq_of_lt h
+
 theorem sub_eq_of_le {a b : Uint256} (h : b.val ≤ a.val) :
   ((a - b : Uint256) : Nat) = a.val - b.val := by
   have hlt : a.val - b.val < modulus := by

Verity/EVM/Uint256.lean

@@ -18,6 +18,7 @@ abbrev modulus := Verity.Core.Uint256.modulus
 abbrev add := Verity.Core.Uint256.add
 abbrev sub := Verity.Core.Uint256.sub
 abbrev mul := Verity.Core.Uint256.mul
+abbrev pow := Verity.Core.Uint256.pow
 abbrev div := Verity.Core.Uint256.div
 abbrev mod := Verity.Core.Uint256.mod
 

Verity/Macro/Translate.lean

@@ -2245,6 +2245,7 @@ private partial def inferPureExprType
       let lhsTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants
       let rhsTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals b visitingConstants
       classifyUnsignedWordArithmeticResultType stx "bitwise word arithmetic" lhsTy rhsTy
+  | `(term| pow $a $b) | `(term| $a ^ $b)
   | `(term| min $a $b) | `(term| max $a $b) | `(term| wMulDown $a $b) | `(term| wDivUp $a $b)
   | `(term| ceilDiv $a $b) => do
       let lhsTy ← inferPureExprType fields constDecls immutableDecls externalDecls params locals a visitingConstants
@@ -3074,6 +3075,10 @@ partial def translatePureExprWithTypes
   | `(term| add $a $b) => `(Compiler.CompilationModel.Expr.add $(← translatePureExprWithTypes fields constDecls immutableDecls params locals a visitingConstants) $(← translatePureExprWithTypes fields constDecls immutableDecls params locals b visitingConstants))
   | `(term| sub $a $b) => `(Compiler.CompilationModel.Expr.sub $(← translatePureExprWithTypes fields constDecls immutableDecls params locals a visitingConstants) $(← translatePureExprWithTypes fields constDecls immutableDecls params locals b visitingConstants))
   | `(term| mul $a $b) => `(Compiler.CompilationModel.Expr.mul $(← translatePureExprWithTypes fields constDecls immutableDecls params locals a visitingConstants) $(← translatePureExprWithTypes fields constDecls immutableDecls params locals b visitingConstants))
+  | `(term| pow $a $b) | `(term| $a ^ $b) =>
+      `(Compiler.CompilationModel.Expr.externalCall Compiler.CompilationModel.builtinExpName
+          [$(← translatePureExprWithTypes fields constDecls immutableDecls params locals a visitingConstants),
+           $(← translatePureExprWithTypes fields constDecls immutableDecls params locals b visitingConstants)])
   | `(term| div $a $b) | `(term| $a / $b) => do
       let lhsTy ← inferPureExprType fields constDecls immutableDecls #[] params locals a visitingConstants
       let rhsTy ← inferPureExprType fields constDecls immutableDecls #[] params locals b visitingConstants

artifacts/macro_property_tests/PropertyUint256PowSmoke.t.sol

@@ -0,0 +1,38 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyUint256PowSmokeTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke.lean
+ */
+contract PropertyUint256PowSmokeTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("Uint256PowSmoke");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: TODO decode and assert `scale` result
+    function testTODO_Scale_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("scale(uint256)", uint256(1)));
+        require(ok, "scale reverted unexpectedly");
+        assertEq(ret.length, 32, "scale ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 2: TODO decode and assert `scaleInfix` result
+    function testTODO_ScaleInfix_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("scaleInfix(uint256)", uint256(1)));
+        require(ok, "scaleInfix reverted unexpectedly");
+        assertEq(ret.length, 32, "scaleInfix ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+}