cracked solution may be wrong

[achan001]

2 xoroshiro128+ random 64-bits numbers are not enough to produce a unqiue state.
It is possible your script will solve for the wrong state, i.e. wrong prediction.

Example: random sequence = 0xdfd1045768598cde , 0x86eae8a4b518de64, ...
There are 3 solutions:

state = 0x2369b5a08e5846c1 , 0xbc674eb6da01461d
state = 0x5a0b43baa54eccbb , 0x85c5c09cc30ac023
state = 0xdeadbeefdeadbeef , 0x123456789abcdef

[achan001]

Since xoroshiro128+ is implemented in C (64-bits variable),
solver rule should be mask with 0xffffffffffffffff

Without the mask, it might fail Python try clause by mistake.

P.S. you might want to rename xorshift.py as xoroshiro.py

[lemire]

I don't think you have shown that the solutions are wrong. You have argued, correctly, that there may be more than one solution. That is correct and I have modified the README file to make this point clear.

Without the mask, it might fail Python try clause by mistake.

I don't see this... if you think that there is a bug in the Python script, please provide a failing example.

[achan001]

A possible seed is not the same as "cracking" PRNG, which imply we can predict the sequence.
Only the right seed will predict the sequences correctly.

A simple fix is to solve for all possible seeds:

import sys, z3
bit64 = 0xffffffffffffffff

def LShL(x, n): return (x << n) & bit64

def xo128(x, y, LShR = lambda x,i: x>>i):
    y ^= x
    return y ^ LShL(y, 14) ^ (LShL(x,55)|LShR(x,9)), (LShL(y,36)|LShR(y,28))

if sys.argv[1] == 'seed':       # usage xo128.py seed x y
    x = int(sys.argv[2], 0)
    y = int(sys.argv[3], 0)
    for i in range(10):         # generate random numbers
        print hex((x+y)&bit64)
        x, y = xo128(x, y)
    sys.exit()

x0, y0 = z3.BitVecs('x0 y0', 64)
x, y = x0, y0
s = z3.SimpleSolver()

for v in sys.argv[1:]:
    n = int(v, 0)
    s.add((x + y) & bit64 == n)
    x, y = xo128(x, y, z3.LShR)
                       
for i in xrange(1, sys.maxint):
    print '\n#%d = %s' % (i, s.check())
    if s.check().r != 1: break  # quit if failed
    soln = s.model()
    x, y = (soln[i].as_long() for i in (x0,y0))
    print 'state =', hex(x), hex(y)
    for j in range(10):         # show predictions
        print hex((x+y) & bit64)
        x, y = xo128(x, y)
    s.add(x0 != soln[x0], y0 != soln[y0])

Without mask FAILING example: random sequence = 0, 0xdeadbeef
-> no solution, since first rule x0 + y0 = 0, imply x0 = y0 = 0
-> contradicted xoroshiro128+ non-zero seed requirement

With mask, we get unique seed, thus correct prediction.

>run xo128all.py 0 0xdeadbeef

#1 = sat
state = 0x7ffe1a2a4fde000L 0xf8001e5d5b022000L
0x0L
0xdeadbeefL
0x8d244754497ed7c2L
0xf4c54d37a8ef8204L
0xa12370969dfd3ed9L
0x53a85f83719868adL
0xbedcb85e11438ff5L
0xb1a965c10bf09ea5L
0x4c19f8c964f809e9L
0x591dc69d53f6e523L

#2 = unsat

[lemire]

Thank you

[lemire]

Great. Merged your script with credit.