Simplify exponentiation over conditional constants

CHANGELOG.md

@@ -8,6 +8,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ## [Unreleased]
 
 ## Added
+- Exponentiation over conditional constants folds to conditional powers, allowing
+  packed-array writes with a conditionally selected index to reach the SMT solver.
 - Invariant testing: `hevm test` checks `invariant_` functions after every
   sequence of at most `--invariant-depth` calls to the target contracts, with
   symbolic arguments, callers and timestamps. States reached before are not

src/EVM/Expr.hs

@@ -576,6 +576,7 @@ liftLitITE = \case
   Add a b -> two add a b
   Sub a b -> two sub a b
   Mul a b -> two mul a b
+  Exp a b -> two EVM.Expr.exp a b
   Div a b -> two EVM.Expr.div a b
   Mod a b -> two EVM.Expr.mod a b
   And a b -> two EVM.Expr.and a b
@@ -1570,6 +1571,7 @@ simplifyNoLitToKeccak e = untilFixpoint (mapExprShared (static (HC.Rewrite go)))
     go o@(Add {}) | Just r <- liftLitITE o = r
     go o@(Sub {}) | Just r <- liftLitITE o = r
     go o@(Mul {}) | Just r <- liftLitITE o = r
+    go o@(Exp {}) | Just r <- liftLitITE o = r
     go o@(Div {}) | Just r <- liftLitITE o = r
     go o@(Mod {}) | Just r <- liftLitITE o = r
     go o@(And {}) | Just r <- liftLitITE o = r

test/EVM/Expr/ExprTests.hs

@@ -1117,6 +1117,19 @@ basicSimplificationTests = testGroup "Basic simplification tests"
         a = successPath [PEq (Add (Lit 1) (Lit 2)) (Sub (Lit 4) (Lit 1))]
         b = Expr.simplify a
       assertEqual "Must simplify down" (successPath []) b
+  , testCase "simp-exp-ite-lits" $ do
+      let c = Var "c"
+          choices = ITE c (Lit 3) (Lit 5)
+      assertEqual "packed-array byte offsets"
+        (ITE c (Lit (1 `shiftL` 224)) (Lit (1 `shiftL` 32)))
+        (Expr.simplify (Exp (Lit 256) (ITE c (Lit 28) (Lit 4))))
+      assertEqual "powers wrap at 256 bits"
+        (ITE c (Lit (1 `shiftL` 248)) (Lit 0))
+        (Expr.simplify (Exp (Lit 256) (ITE c (Lit 31) (Lit 32))))
+      assertEqual "conditional base" (ITE c (Lit 9) (Lit 25))
+        (Expr.simplify (Exp choices (Lit 2)))
+      assertEqual "shared condition" (ITE c (Lit 27) (Lit 3125))
+        (Expr.simplify (Exp choices choices))
   , testCase "simp-mul-neg1" $ do
       let simp = Expr.simplify $ Mul (Lit Expr.maxLit) (Var "x")
       assertEqual "mul by -1 is negation" (Sub (Lit 0) (Var "x")) simp

test/EVM/Expr/RewriteFuzz.hs

@@ -521,7 +521,7 @@ genTemplate s shiftAmt = oneof
       pure $ Sub (foldr1 Add (take 6 xs')) (foldr1 Add (take 6 ys'))
     -- literal branches, sharing a condition from a small set so that ITEs pair up
     ite = ITE <$> elements [Var "a", LT (Var "a") (Var "b"), IsZero (Var "c")] <*> lit <*> lit
-    litOp' = elements [Add, Sub, Mul, Div, Mod, And, Or, Xor, Eq, LT, SLT, SHL, SHR, SAR]
+    litOp' = elements [Add, Sub, Mul, Exp, Div, Mod, And, Or, Xor, Eq, LT, SLT, SHL, SHR, SAR]
     lit = Lit <$> genSpecialLit
     pow2 = Lit . (2 ^) <$> choose (0 :: Int, 255)
     litOp = elements [Add, Sub, Xor, Mul]

test/EVM/SymExec/SymExecTests.hs

@@ -48,7 +48,24 @@ solidityExplorationTests = testGroup "Exploration of Solidity"
 
 basicTests :: TestTree
 basicTests = testGroup "simple-checks"
-  [ testCase "read-byte-from-word-mapping-key" $ do
+  [ testCase "packed-array-conditional-index" $ do
+      Just c <- solcRuntime "C" [i|
+        contract C {
+          uint32[8] values;
+          function f(bool high) external {
+            uint256 index = 1;
+            if (high) index = 7;
+            values[0] = 42;
+            values[index] = 99;
+            assert(values[0] == 42);
+          }
+        }
+        |]
+      (paths, results) <- executeWithBitwuzla $ \s ->
+        checkAssert s defaultPanicCodes c (Just (Sig "f(bool)" [AbiBoolType])) [] defaultVeriOpts
+      assertEqual "the other packed element is unchanged" [] results
+      assertBool "no partial paths" (not (any isPartial paths))
+  , testCase "read-byte-from-word-mapping-key" $ do
       Just c <- solcRuntime "C" [i|
         contract C {
           mapping(address => uint256) balances;