Use Z3 to "crack" xoroshiro128+

partyover.py

from z3 import *

"""
Solver for this kind of stuff (z3 is the solver here, this tool simply uses it):
http://www.pcg-random.org/posts/predictability-party-tricks.html
https://lemire.me/blog/2017/08/22/cracking-random-number-generators-xoroshiro128/

I still don't know how they did it, but it seems solvers can crack this pretty easily.
This generates the same output though :)

Since not everything can be solved, sometimes this will throw...
"""

#target = b'Is this RANDOM?!'
#offset = 8

#target = b'\x00\x20\x44\x61\x6e\x69\x65\x6c\x00\x4c\x65\x6d\x69\x72\x65\x20'
#offset = 0

target = b'Open Knowledge!!'
offset = 0

target = target[:16].ljust(16)

r1_val = int.from_bytes(target[:8], byteorder='little')
r2_val = int.from_bytes(target[8:], byteorder='little')

s0, s1, n0, n1, r1, r2 = BitVecs('s0 s1 n0 n1 r1 r2', 64)

s = Solver()

s.add(r1 == BitVecVal(r1_val, 64), r2 == BitVecVal(r2_val, 64))
s.add(n0 == RotateLeft(s0, 55) ^ s1 ^ s0 ^ (s0 << 14) ^ (s1 << 14))
s.add(n1 == RotateLeft(s0, 36) ^ RotateLeft(s1, 36))
s.add(r1 == s0+s1, r2 == n0+n1)

s.check()
model = s.model()

s0 = model[s0].as_long()
s1 = model[s1].as_long()

def rotr(x, k):
  return (x >> k) | (x << (64 - k) & 0xffffffffffffffff)
  
def prev_xsr128(n0, n1):
  s0, s1 = 0, 0
  
  s1 = rotr(n1, 36)
  s0 = n0 ^ s1 ^ (s1 << 14 & 0xffffffffffffffff)
  s0 = rotr(s0, 55)
  s1 ^= s0
  
  return s0, s1
  
for _ in range(offset):
  s0, s1 = prev_xsr128(s0, s1)
	
print('s[0] = '+hex(s0).upper()+'L;')
print('s[1] = '+hex(s1).upper()+'L;')