Python Z3 proofs of the rules.

Author: ekpyron

test/formal/mod_add_to_addmod.py

@@ -0,0 +1,31 @@
+from opcodes import MOD, ADD, ADDMOD
+from rule import Rule
+from z3 import BitVec
+
+"""
+Rule:
+MOD(ADD(X, Y), A) -> ADDMOD(X, Y, A)
+given
+    A > 0
+    A & (A - 1) == 0
+"""
+
+rule = Rule()
+
+n_bits = 32
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+
+# Non optimized result
+nonopt = MOD(ADD(X, Y), A)
+
+# Optimized result
+opt = ADDMOD(X, Y, A)
+
+rule.require(A > 0)
+rule.require(((A & (A - 1)) == 0))
+
+rule.check(nonopt, opt)

test/formal/mod_mul_to_mulmod.py

@@ -0,0 +1,31 @@
+from opcodes import MOD, MUL, MULMOD
+from rule import Rule
+from z3 import BitVec
+
+"""
+Rule:
+MOD(MUL(X, Y), A) -> MULMOD(X, Y, A)
+given
+    A > 0
+    A & (A - 1) == 0
+"""
+
+rule = Rule()
+
+n_bits = 8
+
+# Input vars
+X = BitVec('X', n_bits)
+Y = BitVec('Y', n_bits)
+A = BitVec('A', n_bits)
+
+# Non optimized result
+nonopt = MOD(MUL(X, Y), A)
+
+# Optimized result
+opt = MULMOD(X, Y, A)
+
+rule.require(A > 0)
+rule.require(((A & (A - 1)) == 0))
+
+rule.check(nonopt, opt)

test/formal/opcodes.py

@@ -1,4 +1,4 @@
-from z3 import BitVecVal, BV2Int, If, LShR, UDiv, ULT, UGT, URem
+from z3 import BitVecVal, BV2Int, If, LShR, UDiv, ULT, UGT, URem, ZeroExt, Extract
 
 def ADD(x, y):
 	return x + y
@@ -18,6 +18,12 @@ def SDIV(x, y):
 def MOD(x, y):
 	return If(y == 0, 0, URem(x, y))
 
+def MULMOD(x, y, m):
+	return If(m == 0, 0, Extract(x.size() - 1, 0, URem(ZeroExt(x.size(), x) * ZeroExt(x.size(), y), ZeroExt(m.size(), m))))
+
+def ADDMOD(x, y, m):
+	return If(m == 0, 0, Extract(x.size() - 1, 0, URem(ZeroExt(1, x) + ZeroExt(1, y), ZeroExt(1, m))))
+
 def SMOD(x, y):
 	return If(y == 0, 0, x % y)