Finding a hash collision with z3

hash_collision.py

from itertools import cycle
from z3 import *


class NameGen:
    def __init__(self, prefix):
        self.prefix = prefix
        self.count = 0

    def gen(self):
        name = f"{self.prefix}{self.count}"
        self.count += 1
        return name


def main():
    s = Solver()

    xs = [BitVecVal(ord(x), 32) for x in "Hello there"]
    xhash = hash(s, xs)

    for length in range(0, 20, 2):
        print(f"Trying length {length}")

        s.push()

        y_gen = NameGen("y")

        ys = [
            *[BitVecVal(ord(c), 32) for c in "General Ke"],
            *[
                with_constraint(
                    s,
                    BitVec(y_gen.gen(), 32),
                    lambda y: And(
                        y >= ord("a"),
                        y <= ord("z"),
                        Or(y == ord("y"), is_vowel(y) == (i % 2 != 0)),
                    ),
                )
                for i in range(length)
            ],
            *[BitVecVal(ord(c), 32) for c in "bi"],
        ]

        yhash = hash(s, ys)

        s.add(xhash == yhash)

        if s.check() == sat:
            while s.check() == sat:
                m = s.model()
                x_str = "".join([chr(m.evaluate(y).as_long()) for y in ys])
                print(x_str)

                # Exclude this solution and try again to find other solutions
                # with the same length.
                s.add(Or(*[y != m.evaluate(y) for y in ys]))

            break

        s.pop()


def hash(s, values):
    h = BitVecVal(5381, 32)

    for x in reversed(values):
        h = (h * 33) ^ x

    return h


def with_constraint(s, val, constraints):
    s.add(constraints(val))
    return val


def is_vowel(x):
    return Or(*[x == ord(c) for c in "AEIOUaeiou"])


if __name__ == "__main__":
    main()