# CRACKING RANDOM PYTHON LESS THAN 32 BITS

import random
import binteger
from Crypto.Cipher import AES
from Crypto.Util.Padding import pad

def getbit():
    return random.getrandbits(1)

known = b''
for _ in range(2500):
    word = binteger.Bin([getbit() for _ in range(8)]).int
    known += word.to_bytes(1, "big")

FLAG = b'W1{day-la-flag}'
key = b""
for _ in range(16):
    word = binteger.Bin([getbit() for _ in range(8)]).int
    key += word.to_bytes(1, "big")

cipher = AES.new(key, AES.MODE_ECB)
ciphertext = cipher.encrypt(pad(FLAG, 16))

# out 5f0512a86cd89a47ecd5cb77af672f9137ecb5cd0c6141d0d5cd4257f0b4e72588d87fbc0f4cb0660ee0a4483bfbdf1a

### rbtree_mersenne.py

class Twister:
    N = 624
    M = 397
    A = 0x9908b0df

    def __init__(self):
        self.state = [ [ (1 << (32 * i + (31 - j))) for j in range(32) ] for i in range(624)]
        self.index = 0
    
    @staticmethod
    def _xor(a, b):
        return [x ^ y for x, y in zip(a, b)]
    
    @staticmethod
    def _and(a, x):
        return [ v if (x >> (31 - i)) & 1 else 0 for i, v in enumerate(a) ]
    
    @staticmethod
    def _shiftr(a, x):
        return [0] * x + a[:-x]
    
    @staticmethod
    def _shiftl(a, x):
        return a[x:] + [0] * x

    def get32bits(self):
        if self.index >= self.N:
            for kk in range(self.N):
                y = self.state[kk][:1] + self.state[(kk + 1) % self.N][1:]
                z = [ y[-1] if (self.A >> (31 - i)) & 1 else 0 for i in range(32) ]
                self.state[kk] = self._xor(self.state[(kk + self.M) % self.N], self._shiftr(y, 1))
                self.state[kk] = self._xor(self.state[kk], z)
            self.index = 0

        y = self.state[self.index]
        y = self._xor(y, self._shiftr(y, 11))
        y = self._xor(y, self._and(self._shiftl(y, 7), 0x9d2c5680))
        y = self._xor(y, self._and(self._shiftl(y, 15), 0xefc60000))
        y = self._xor(y, self._shiftr(y, 18))
        self.index += 1

        return y
    
    def getrandbits(self, bit):
        return self.get32bits()[:bit]

class Solver:
    def __init__(self):
        self.equations = []
        self.outputs = []
    
    def insert(self, equation, output):
        for eq, o in zip(self.equations, self.outputs):
            lsb = eq & -eq
            if equation & lsb:
                equation ^= eq
                output ^= o
        
        if equation == 0:
            return

        lsb = equation & -equation
        for i in range(len(self.equations)):
            if self.equations[i] & lsb:
                self.equations[i] ^= equation
                self.outputs[i] ^= output
    
        self.equations.append(equation)
        self.outputs.append(output)
    
    def solve(self):
        num = 0
        for i, eq in enumerate(self.equations):
            if self.outputs[i]:
                # Assume every free variable is 0
                num |= eq & -eq
        
        state = [ (num >> (32 * i)) & 0xFFFFFFFF for i in range(624) ]
        return state

### Solve.py

from z3 import *
import rbtree_mersenne
import random
import time

def rbtree_solve(outputs):
    twister = rbtree_mersenne.Twister()
    solver = rbtree_mersenne.Solver()

    for tup in outputs:
        res, bits = tup
        equation = twister.getrandbits(bits)

        for i in range(bits):
            solver.insert(equation[i], (res >> (bits - 1 - i)) & 1)

    state = solver.solve()
    return (3, tuple(state + [0]), None)


def z3_solve(outputs):
    MT = [BitVec(f'm{i}', 32) for i in range(624)]
    s = Solver()
    
    def tamper(y):
        y ^= LShR(y, 11)
        y ^= (y << 7) & 0x9D2C5680
        y ^= (y << 15) & 0xEFC60000
        return y ^ LShR(y, 18)
        
    def getnext():
        x = Concat(Extract(31, 31, MT[0]), Extract(30, 0, MT[1]))
        y = If(x & 1 == 0, BitVecVal(0, 32), 0x9908B0DF)
        MT.append(MT[397] ^ LShR(x, 1) ^ y)
        return tamper(MT.pop(0))
        
    def getrandbits(n):
        return Extract(31, 32 - n, getnext())
        
    s.add([getrandbits(op[1]) == op[0] for op in outputs])
    assert(s.check() == sat)
    state = [s.model()[x].as_long() for x in [BitVec(f'm{i}', 32) for i in range(624)]]
    
    return (3, tuple(state + [0]), None)

def int_to_binary(num):
    binary_string = bin(num)[2:]  
    padded_binary_string = binary_string.zfill(8) 
    return padded_binary_string

if __name__ == "__main__":
    with open('known','rb') as file:
        data = file.read()
    binary = ""
    for i in data:
        binary += str(int_to_binary(i))
    bits = 1
    number = 2500*8

    output = []
    for _ in range(number):
        output.append((int(binary[_]), bits))
    print(output)

    st = time.time()
    random.setstate(rbtree_solve(output))
    for _ in range(number):
        assert output[_][0] == random.getrandbits(bits)
    key = ""
    for _ in range(16*8):
        key += str(random.getrandbits(bits))
    fin = time.time()
    print(f"rbtree took {fin - st} seconds.")
    print(key)

    st = time.time()
    random.setstate(z3_solve(output))
    for _ in range(number):
        assert output[_][0] == random.getrandbits(bits)
    for _ in range(10000):
        assert check[_] == random.getrandbits(bits)
    fin = time.time()
    print(f"z3 took {fin - st} seconds.")

import random
import binteger
from Crypto.Cipher import AES
from Crypto.Util.Padding import pad

key = "00011101111110110010011101011111100111101101001000111110110000001101101010011110010001010101101000011100110100101110010011010001"
integer_value = int(key, 2)
key = integer_value.to_bytes((len(key) + 7) // 8, byteorder='big')


cipher = AES.new(key, AES.MODE_ECB)
ciphertext = cipher.decrypt(bytes.fromhex("5f0512a86cd89a47ecd5cb77af672f9137ecb5cd0c6141d0d5cd4257f0b4e72588d87fbc0f4cb0660ee0a4483bfbdf1a"))
print(ciphertext)