z3 python z3.If always False (keygen)

Question

I want to generate a keygen in python with z3. here is the validation function:

def f(a):
    a = ord(a)
    if a <= 47 or a > 57:
        if a <= 64 or a > 98:
            exit()
        else:
            return a - 55
    else:
        return a - 48


def validate(key):
    if len(key) != 16:
        return False

    for k in key:
        if f(k)%2== 0:
            return False
    return True

I tried to write a solver for this

from z3 import *
solver = Solver()

def f_z3(a):
    return If(
        Or(a<=47, a>57),
        If(
            Or(a<=64, a>98),
            False, #  exit()???
            a -55
        ),
        a -48
    )

key = IntVector("key", 16)
for k in key:
    solver.add(f_z3(k)%2==0)

solver.check()
print(solver.model())

and here is the output

[key__1 = 48,
 key__10 = 48,
 key__9 = 48,
 key__15 = 48,
 key__6 = 48,
 key__8 = 48,
 key__4 = 48,
 key__0 = 48,
 key__14 = 48,
 key__11 = 48,
 key__7 = 48,
 key__5 = 48,
 key__2 = 48,
 key__12 = 48,
 key__13 = 48,
 key__3 = 48]

Which returns the key "0000000000000000", but validate("0000000000000000") return False.

I know that the problem is in the f_z3 function, I don't know how to express the exit() inside the if, I want something always False. But instead am just returning False.

Any idea how to solve this problem?

Answer 1

There are two issues with your code:

1. As you observed, the replacement of exit with False isn't right in the f_z3 function. (The python version is just bizarre here that it would return a boolean in certain cases and just plain die in others. But that's beside the point.) In all other branches you're returning an integer, and in that one you're returning a boolean. In z3 you always want to return the same type; an integer. So pick something that will cause that case to produce False eventually. Since later on you're checking for evenness, any odd number will do. Say 1; so modify it to produce 1 instead of False when exit is called.

2. While you're validating, the Python code returns False if the result is even; so you need to assert that correctly. Currently you're doing solver.add(f_z3(k)%2==0), instead you should require the modulus to be not-even, like this: solver.add(f_z3(k)%2!=0).

With those two modifications, you'll have the following code:

from z3 import *
solver = Solver()

def f_z3(a):
    return If(
        Or(a<=47, a>57),
        If(
            Or(a<=64, a>98),
            1,
            a -55
        ),
        a -48
    )

key = IntVector("key", 16)
for k in key:
    solver.add(f_z3(k)%2!=0)

solver.check()
print(solver.model())

When run, this produces:

[key__1 = 49,
 key__10 = 49,
 key__9 = 49,
 key__15 = 49,
 key__6 = 49,
 key__8 = 49,
 key__4 = 49,
 key__0 = 49,
 key__14 = 49,
 key__11 = 49,
 key__7 = 49,
 key__12 = 49,
 key__5 = 49,
 key__2 = 49,
 key__13 = 49,
 key__3 = 49]

which suggests the valid key "1111111111111111".

Answer 2

For the second point I didn't notice, I was more concentrate in the first one. returning 1 doesn't solve my problem sins I just simplified the real problem with a smaller example. I want a general solution for this pattern.

def f(x):
   if condition(x):
       exit()
   else:
       return g(x) # return something in relation with x

I found this pattern which is working now

def f_z3(x):
    global solver
    solver.add(Not(condition(x))
    return g(x)

So my first function will be something like

def f_z3(a):
    global solver
    # sins we have two nested condition we have to add an And
    solver.add(
        Not(
            And(
                Or(a<=47, a>57),
                Or(a<=64, a>98)
            )
        )
    )
    return If(
        Or(a<=47, a>57),
        a-55,
        a - 48
    )

I still search a better approach to solve this kind of pattern, something that tell the If condition to be always False.