stuff

training/IntroZ3/tasks/chall1_rot128/z3test.py

@@ -0,0 +1,39 @@
+import random
+import z3
+
+_ROL_ = lambda x, i : ((x << i) | (x >> (N-i))) & (2**N - 1)
+
+
+N = 128
+
+def parity(x):
+    res = 0
+    while x:
+        res ^= x & 1
+        x >>= 1
+    return res
+
+
+while True:
+    x = random.randint(0, 2**128)
+    if parity(x) == 0:
+        break
+
+# Compute y and c, such that y ^ _ROL_(y,c) == x
+# Hint: to implement _ROL_, z3 already has the function z3.RotateLeft
+def compute_yc(x):
+    s = z3.Solver()
+    y = z3.BitVec("y", N)
+    c = z3.BitVec("c", N)
+    s.add((y ^ z3.RotateLeft(y,c)) == x)
+    s.check()
+    m = s.model()
+
+    return m[y].as_long(), m[c].as_long()
+
+
+y, c = compute_yc(x)
+
+print(f'{y=}, {c=}')
+print(f'{x=}, {y ^ _ROL_(y, c)=}')
+print(f'{x==y ^ _ROL_(y, c)=}')