lemire / crackingxoroshiro128plus Goto Github PK

I made an error when trying to search for next soln
Last line of xoroshiftall.py :

s.add( x0 != soln[x0], y0 != soln[y0] )

What I intended were to remove 1 (solved) seed from search space.
But above rule added simultaneous equations instead.

-> comma acted like a AND (not OR)
-> possibly remove more than 1 state: (x0, ?) and (?, y0)

To remove just 1 state, I should use z3.Or

s.add( z3.Or(x0 != soln[x0], y0 != soln[y0]) )

The bug is probably not serious enough to give the wrong answer.
But with bigger states, say 256 bits, z3.Or is REQUIRED

see my xoshiro256-seed solver: https://github.com/achan001/xoshiro256-seed

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