太好玩了 z3-solver
https://www.arealme.com/luck-test/cn/
这个网站是用 Math.random() 来抛随机数的，而众所周知， Math.random() 不是密码学安全的，它在 v8 用的是 xorshift128+，它很快，但是所有运算都是线性的
于是我们可以用 z3-solver 通过几个随机数求解出其内部 state，然后算出接下来一段时间内的随机数
一直知道可以这么干，今天终于实践了一下（
https://www.arealme.com/luck-test/cn/
这个网站是用 Math.random() 来抛随机数的，而众所周知， Math.random() 不是密码学安全的，它在 v8 用的是 xorshift128+，它很快，但是所有运算都是线性的
于是我们可以用 z3-solver 通过几个随机数求解出其内部 state，然后算出接下来一段时间内的随机数
一直知道可以这么干，今天终于实践了一下（