'''
Script based on
https://github.com/PwnFunction/v8-randomness-predictor/blob/main/main.py
https://github.com/d0nutptr/v8_rand_buster/blob/master/xs128p.py
'''

import z3
import struct
from decimal import Decimal

animals = open('animals.txt').read().splitlines()
adjectives = open('adjectives.txt').read().splitlines()

animals_length = len(animals)
adjectives_length = len(adjectives)

filenames = ['miniature-strong-buck', 'ironclad-sniveling-ichidna', 'orange-full-nandoo', 'wobbly-shy-jaguarundi', 'fabulous-liquid-waxwing', 'burdensome-stimulating-axisdeer', 'mean-knowing-lion']

sequence = []

for c in filenames[1:6]:
    words = c.split('-')
    for w in words[:2]:
        index = adjectives.index(w)
        n_upper = Decimal(index + 1) / Decimal(adjectives_length)
        n_lower = Decimal(index) / Decimal(adjectives_length)
        sequence.append((n_upper, n_lower))
    index = animals.index(words[2])
    n_upper = Decimal(index + 1) / Decimal(animals_length)
    n_lower = Decimal(index) / Decimal(animals_length)
    sequence.append((n_upper, n_lower))

def last_rng_state(state0, state1):
    se_s1 = state0
    se_s0 = state1
    state0 = se_s0
    se_s1 ^= (se_s1 << 23) & 0xFFFFFFFFFFFFFFFF
    se_s1 ^= se_s1 >> 17  # Logical shift (LShR equivalent)
    se_s1 ^= se_s0
    se_s1 ^= se_s0 >> 26
    state1 = se_s1
    return state0, state1    

def rng_to_double(state0):
    u_long_long_64 = (state0 >> 12) | 0x3FF0000000000000
    float_64 = struct.pack("<Q", u_long_long_64)
    next_sequence = struct.unpack("d", float_64)[0]
    next_sequence -= 1
    return next_sequence

def float_to_adj(state0):
    num = rng_to_double(state0)
    return adjectives[int(num * adjectives_length)]

def float_to_animal(state0):
    num = rng_to_double(state0)
    return animals[int(num * animals_length)]

def from_double(num):
    float_64 = struct.pack("d", num + 1)
    u_long_long_64 = struct.unpack("<Q", float_64)[0]
    return u_long_long_64

sequence = sequence[::-1]

solver = z3.SolverFor('QF_BV')

se_state0, se_state1 = z3.BitVecs("se_state0 se_state1", 64)

for i in range(len(sequence)):
    se_s1 = se_state0
    se_s0 = se_state1
    se_state0 = se_s0
    se_s1 ^= se_s1 << 23
    se_s1 ^= z3.LShR(se_s1, 17)  # Logical shift instead of Arthmetric shift
    se_s1 ^= se_s0
    se_s1 ^= z3.LShR(se_s0, 26)
    se_state1 = se_s1

    upper = from_double(sequence[i][0])
    lower = from_double(sequence[i][1])

    # Get the lower 52 bits (mantissa)
    mantissa_upper = upper & ((1 << 52) - 1)
    mantissa_lower = lower & ((1 << 52) - 1)
    upper_expr = (upper >> 52) & 0x7FF

    calc = z3.LShR(se_state0, 12)
    solver.add(z3.And(mantissa_lower <= calc, z3.Or(mantissa_upper >= calc, upper_expr == 1024)))

if solver.check() == z3.sat:
    model = solver.model()

    states = {}
    for state in model.decls():
        states[state.__str__()] = model[state]

    print(states)

    state0 = states["se_state0"].as_long()
    state1 = states["se_state1"].as_long()

    # get next
    code = float_to_adj(state0)
    print('Next code:', code)

    # get previous filename
    state0_, state1_ = state0, state1
    for i in range(16): # rollback random state
        state0_, state1_ = last_rng_state(state0_, state1_)
    animal = float_to_animal(state0_)
    previous_filename = animal
    for i in range(2):
        state0_, state1_ = last_rng_state(state0_, state1_)
        previous_filename = float_to_adj(state0_) + '-' + previous_filename
    print('Previous filename:', previous_filename)