# coding: utf-8
import os, sys
from z3 import *


# 'hashed' password we have from the 'binary'
hashed_password=168372036536695091

# we are going to try different lengths of passwords
for password_length in range(5,15):
    # init solver, this will wipe any residual constraints in each loop
    solver = Solver()

    # initialize constraints for each character of the password
    # we are only going to allow ascii values from 'a' to 'z'
    chars = [Int(c) for c in range(password_length)]

    # initialization value
    n = 7
    # the 'hashing' algorithm we have extracted from the binary
    for c in chars:
        # this essentially extends the symbolic constraints associated with each 'c'
        n = n * 27 + c * 5

    # the solver should return sat iff
    # the hashed input is equal the hashed_password
    solver.add(n == hashed_password)

    for c in chars:
        # each 'c' should be a lowercase ascii character
        solver.add(And(c >= ord('a'),
                       c <= ord('z')))


    res = solver.check()
    if res != sat:
        print("No possible password found...")
        continue

    # print the model/password found
    m = solver.model()
    for d in m.decls():
        print("%s = %s -> %c" % (d.name(), m[d], chr(m[d].as_long())))
    password = ''.join(chr(m[c].as_long()) for c in chars)
    print("Trying '" + password + "' as password")
    os.system("./password_storage.sh {}".format(password))