hi

I am trying to compile these codes but there is some errors so need help on it and make it able to run in the end =)

Thanks

from z3 import * from binascii import unhexlify

s = Solver() seed = [Bool('seed[{}]'.format(i)) for i in range(256)]

def RULE(x, y, z): return Or( And(Not(x), Not(y), z), # 001 = 1 -> 1 And(Not(x), y, Not(z)), # 010 = 2 -> 1 And(x, Not(y), Not(z)), # 100 = 4 -> 1 And(x, y, Not(z)) # 110 = 6 -> 1 )

def next(x): x = [x[-1]] + x + [x[0]] return [RULE(x[i + 2], x[i + 1], x[i]) for i in range(256)]

target = 37450399269036614778703305999225837723915454186067915626747458322635448226786 next_value = seed

steps = 8

for i in range(steps): next_value = next(next_value)

for i in range(128 // steps): # take a snapshots of the solver constraints s.push() for j in range(256): bit = ((1 = 1 s.add(next_value[j] == bit) if s.check() == sat: m = s.model() ans = 0 for j in range(256): ans |= (1 if m[seed[j]] else 0)

if 'INS' in unhexlify('%064x' % ans)[::-1]: print(repr(unhexlify('%064x' % ans)[::-1])) # restore the snapshot s.pop()

###next is not injective (e.g. not invertible)###

s = Solver() seed = [Bool('seed[{}]'.format(i)) for i in range(256)] seed1 = [Bool('seed1[{}]'.format(i)) for i in range(256)]

nv = next(seed) nv1 = next(seed1) # we want same output for j in range(256): s.add(nv[j] == nv1[j]) # we want different input dis = False for i in range(256): dis = Or(dis, seed[i] != seed1[i])

s.add(dis) print(s.check())

m = s.model() ans = 0 for j in range(256): ans |= (1 if m[seed[j]] else 0)

Python 3.6.6 Shell File Edit Shell Debug Options Window Help Python 3.6.6 (v3.6.6:4cf1f54eb7, Jun 27 2018, 03:37:03) [MSC v. 1900 64 bit (AMD6 A 4) on win32 Type "copyright", "credits" or "1icense )" for more information. Traceback (most recent call last) File "C:z3-4.6.0-x86-win\bin\Rule86 SAT.py", line 4, in s = Solver ( ) NameError name 'Solver' is not defined