Compute concrete ADDMOD and MULMOD with Integer

CHANGELOG.md

@@ -128,6 +128,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   writes of zero.
 
 ## Changed
+- Concrete ADDMOD and MULMOD are computed with `Integer` instead of `Word512`,
+  which is several times faster in code that uses them heavily, such as `mulDiv`.
 - `EVM.SymExec` is split: concrete replay of counterexamples moves to
   `EVM.CexReplay`, and equivalence checking to `EVM.Equivalence`. Symbolic
   calldata (`EVM.SymExec.Calldata`) and counterexample models and printing

src/EVM/Expr.hs

@@ -255,12 +255,12 @@ smod = op2 SMod (\x y ->
 addmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
 addmod = op3 AddMod (\x y z ->
   if z == 0 then 0
-  else fromIntegral $ (into @Word512 x + into y) `Prelude.mod` into z)
+  else fromIntegral $ (into @Integer x + into y) `Prelude.mod` into z)
 
 mulmod :: Expr EWord -> Expr EWord -> Expr EWord -> Expr EWord
 mulmod = op3 MulMod (\x y z ->
   if z == 0 then 0
-  else fromIntegral $ (into @Word512 x * into y) `Prelude.mod` into z)
+  else fromIntegral $ (into @Integer x * into y) `Prelude.mod` into z)
 
 exp :: Expr EWord -> Expr EWord -> Expr EWord
 exp = op2 Exp (^)

test/EVM/Expr/ExprTests.hs

@@ -1651,6 +1651,24 @@ concretizationTests = testGroup "Concretization tests"
       -- sign-extend byte 0 of 0xff -> all 1s (since bit 7 is set)
       let simp = Expr.simplify $ SEx (Lit 0) (Lit 0xff)
       assertEqual "SEx should be concretized" (Lit Expr.maxLit) simp
+  , testCase "conc-modular-arithmetic-full-width" $ do
+      let top = Expr.maxLit
+      Expr.addmod (Lit top) (Lit top) (Lit top) @?= Lit 0
+      Expr.addmod (Lit top) (Lit top) (Lit (top - 1)) @?= Lit 2
+      Expr.mulmod (Lit top) (Lit top) (Lit top) @?= Lit 0
+      Expr.mulmod (Lit top) (Lit top) (Lit (top - 1)) @?= Lit 1
+      Expr.mulmod (Lit top) (Lit top) (Lit 0) @?= Lit 0
+  , testProperty "conc-modular-arithmetic-matches-wide-words" $
+      \(x :: W256) (y :: W256) (z :: W256) ->
+        let wideX = fromIntegral x :: Word512
+            wideY = fromIntegral y :: Word512
+            wideZ = fromIntegral z :: Word512
+            expected op = Lit $ if z == 0 then 0
+                          else fromIntegral (op wideX wideY `mod` wideZ)
+        in conjoin
+          [ Expr.addmod (Lit x) (Lit y) (Lit z) === expected (+)
+          , Expr.mulmod (Lit x) (Lit y) (Lit z) === expected (*)
+          ]
   , testCase "conc-sex-no-extend" $ do
       -- sign-extend byte 30 of 0xff -> 0xff (bit 247 is not set)
       let simp = Expr.simplify $ SEx (Lit 30) (Lit 0xff)