Exp (ReadWord (Lit 0x0) (AbstractBuf "txdata")) (Lit 0x0) runs infinitely on exprToSMT

[msooseth]

As reported by @charles-cooper in chat. Thanks!

[msooseth]

Oooops, base case was not handled....

@@ -921,6 +941,7 @@ copySlice _ _ _ _ _ = Left "CopySlice with a symbolically sized region not curre
 -- | Unrolls an exponentiation into a series of multiplications
 expandExp :: Expr EWord -> W256 -> Err Builder
 expandExp base expnt
+  | expnt == 0 = pure one
   | expnt == 1 = exprToSMT base
   | otherwise = do
     b <- exprToSMT base

[msooseth]

Note that in evm.codes:

// Example 1
PUSH1 0
PUSH1 0
EXP

Gives us 1, so 0^0 is 1. Every other value is also 1.

[charles-cooper]

just for reference, here is where it is defined in execution specs -- https://github.com/ethereum/execution-specs/blob/e4d7b402a7bda2812e1723642b99614fcdd55193/src/ethereum/cancun/vm/instructions/arithmetic.py#L325