From c1b772e0c09395f1657a3c21dce37e7795fa30e7 Mon Sep 17 00:00:00 2001 From: Dickson Date: Tue, 1 Sep 2026 00:34:50 +0000 Subject: [PATCH] fix concrete zero-modulus ADDMOD and MULMOD --- src/halmos/bitvec.py | 4 ++++ tests/test_sevm.py | 2 ++ 2 files changed, 6 insertions(+) diff --git a/src/halmos/bitvec.py b/src/halmos/bitvec.py index e1d6ac3b7..8b2559b7a 100644 --- a/src/halmos/bitvec.py +++ b/src/halmos/bitvec.py @@ -734,6 +734,8 @@ def addmod( assert size == modulus.size if self.is_concrete and other.is_concrete and modulus.is_concrete: + if modulus.value == 0: + return modulus return HalmosBitVec((self.value + other.value) % modulus.value, size=size) # to avoid add overflow; and to be a multiple of 8-bit @@ -762,6 +764,8 @@ def mulmod( assert size == modulus.size if self.is_concrete and other.is_concrete and modulus.is_concrete: + if modulus.value == 0: + return modulus return HalmosBitVec((self.value * other.value) % modulus.value, size=size) # to avoid mul overflow diff --git a/tests/test_sevm.py b/tests/test_sevm.py index ef05c2af0..0d03c5de4 100644 --- a/tests/test_sevm.py +++ b/tests/test_sevm.py @@ -192,6 +192,7 @@ def byte_of(i, x): (o(EVM.SMOD), [x, BV(0)], BV(0)), (o(EVM.SMOD), [x, BV(1)], BV(0)), (o(EVM.ADDMOD), [BV(4), BV(1), BV(3)], BV(2)), + (o(EVM.ADDMOD), [BV(4), BV(1), BV(0)], BV(0)), (o(EVM.ADDMOD), [x, y, BV(0)], BV(0)), (o(EVM.ADDMOD), [x, y, BV(1)], BV(0)), ( @@ -229,6 +230,7 @@ def byte_of(i, x): BV(1), ), (o(EVM.MULMOD), [BV(5), BV(1), BV(3)], BV(2)), + (o(EVM.MULMOD), [BV(5), BV(1), BV(0)], BV(0)), (o(EVM.MULMOD), [x, y, BV(0)], BV(0)), (o(EVM.MULMOD), [x, y, BV(1)], BV(0)), (