Merge pull request #638 from ethereum/fix-exp-basecase

Adding missing base-case for exponentiation && improve Exp handling via simplification and "ite" in SMT

CHANGELOG.md

@@ -23,6 +23,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   unnecessarily output
 - Not all testcases ran due to incorrect filtering, fixed
 - Removed dead code related to IOAct in the now deprecated and removed debugger
+- Base case of exponentiation to 0 was not handled, leading to infinite loop
+- Better exponential simplification
 - Dumping of END states (.prop) files is now default for `--debug`
 
 ## [0.54.2] - 2024-12-12

src/EVM/Expr.hs

@@ -1190,6 +1190,12 @@ simplify e = if (mapExpr go e == e)
     go (SDiv _ (Lit 0)) = Lit 0 -- divide anything by 0 is zero in EVM
     go (SDiv a (Lit 1)) = a
     -- NOTE: Div x x is NOT 1, because Div 0 0 is 0, not 1.
+    --
+    go (Exp _ (Lit 0)) = Lit 1 -- everything, including 0, to the power of 0 is 1
+    go (Exp a (Lit 1)) = a -- everything, including 0, to the power of 1 is itself
+    go (Exp (Lit 1) _) = Lit 1 -- 1 to any value (including 0) is 1
+    -- NOTE: we can't simplify (Lit 0)^k. If k is 0 it's 1, otherwise it's 0.
+    --       this is encoded in SMT.hs instead, via an SMT "ite"
 
     -- If a >= b then the value of the `Max` expression can never be < b
     go o@(LT (Max (Lit a) _) (Lit b))

src/EVM/SMT.hs

@@ -705,9 +705,14 @@ exprToSMT = \case
   Add a b -> op2 "bvadd" a b
   Sub a b -> op2 "bvsub" a b
   Mul a b -> op2 "bvmul" a b
-  Exp a b -> case b of
-               Lit b' -> expandExp a b'
-               _ -> Left "cannot encode symbolic exponentiation into SMT"
+  Exp a b -> case a of
+    -- Lit 1 has already been handled via Expr.simplify
+    Lit 0 -> do
+      benc <- exprToSMT b
+      pure $ "(ite (= " <> benc `sp` zero <> " ) " <> one `sp` zero <> ")"
+    _ -> case b of
+      Lit b' -> expandExp a b'
+      _ -> Left $ "Cannot encode symbolic exponent into SMT. Offending symbolic value: " <> show b
   Min a b -> do
     aenc <- exprToSMT a
     benc <- exprToSMT b
@@ -921,6 +926,8 @@ 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
+  -- in EVM, anything (including 0) to the power of 0 is 1
+  | expnt == 0 = pure one
   | expnt == 1 = exprToSMT base
   | otherwise = do
     b <- exprToSMT base

test/test.hs

@@ -1372,6 +1372,42 @@ tests = testGroup "hevm"
         let a = fromJust $ Map.lookup (Var "arg1") cex.vars
         assertEqualM "unexpected cex value" a 44
         putStrLnM "expected counterexample found"
+      , test "symbolic-exp-0-to-n" $ do
+        Just c <- solcRuntime "MyContract"
+            [i|
+            contract MyContract {
+              function fun(uint256 a, uint256 b, uint256 k) external pure {
+                uint x = 0 ** b;
+                assert (x == 1);
+              }
+             }
+            |]
+        let sig = Just (Sig "fun(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])
+        a <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        case a of
+          (_, [Cex (_, ctr)]) -> do
+            let b = getVar ctr "arg2"
+            putStrLnM $ "b:" <> show b
+            assertBoolM "b must be non-0" (b /= 0)
+          _ -> assertBoolM "Wrong" False
+      , test "symbolic-exp-0-to-n2" $ do
+        Just c <- solcRuntime "MyContract"
+            [i|
+            contract MyContract {
+              function fun(uint256 a, uint256 b, uint256 k) external pure {
+                uint x = 0 ** b;
+                assert (x == 0);
+              }
+             }
+            |]
+        let sig = Just (Sig "fun(uint256,uint256,uint256)" [AbiUIntType 256, AbiUIntType 256, AbiUIntType 256])
+        a <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        case a of
+          (_, [Cex (_, ctr)]) -> do
+            let b = getVar ctr "arg2"
+            putStrLnM $ "b:" <> show b
+            assertBoolM "b must be 0" (b == 0)
+          _ -> assertBoolM "Wrong" False
       ,
       test "symbolic-mcopy" $ do
         Just c <- solcRuntime "MyContract"