Firefox now uses Xorshift128+ as PRNG.
See in source code here, here and here. Also, discussion.
This is partially reworked code from Firefox:
#include <stdint.h>
#include <stdio.h>
uint64_t a_ = initial...
uint64_t b_ = initial...
uint64_t RandUint64()
{
uint64_t t = a_;
uint64_t s = b_;
a_ = s;
t = t ^ (t << 23);
t = t ^ (t >> 17);
t = t ^ (s ^ (s >> 26));
b_ = t;
return t + s;
}
double RandDouble()
{
uint64_t x = RandUint64();
return (x & ((1ULL<<53)-1)) * 0x1.0p-53;
}
void main()
{
for (int i=0; i<20; i++)
printf ("%1.20f\n", RandDouble());
}
We can simulate this Xorshift128+ function in Z3Py and recover initial states.
Let's see.
Open this HTML file in Firefox:
<!doctype html>
<html><head></head><body><script>
for (x=0; x<20; x++)
console.log(Math.random());
</script></body></html>
Ctrl-Shift-K, you'll see console and something like that (20 random numbers):
0.5796002421038544 0.12380356735099862 0.3164341640263062 0.10154960825287196 0.6979105166875609 0.4842758872116074 0.03867662331649868 0.09293509478430384 0.07472055176571935 0.7421255506090144 0.2519793983241211 0.18063271919434798 0.19558750472843867 0.08712006860073973 0.8061333332601442 0.5827221994080843 0.3062905534575602 0.12242741891787368 0.18006629559552012 0.92675719287678
To predict them, we need to recover initial state of Xorshift128+. As it turned out, only first 3 real numbers are enough to get unique result:
#!/usr/bin/python3
from z3 import *
OUTPUTS=[
0.5796002421038544,
0.12380356735099862,
0.3164341640263062]
def get_53bit_mantissa(i):
# 0x1.0p-53:
divisor=0.00000000000000011102230246251565404236316680908203125
return int(i//divisor)
STATES=len(OUTPUTS)
a_ = BitVec('state_a_', 64)
b_ = BitVec('state_b_', 64)
def RandUint64():
global a_, b_
t = a_
s = b_
a_ = s
t = t ^ (t << 23)
t = t ^ (LShR(t, 17))
t = t ^ (s ^ (LShR(s, 26)))
b_ = t
return t + s
s = Solver()
results_=[]
for i in range(len(OUTPUTS)):
x=RandUint64()
results_.append(x)
for i in range(len(OUTPUTS)):
_53_mask=(1<<53)-1
c=get_53bit_mantissa(OUTPUTS[i])
rounding_errors=1
s.add((results_[i] & _53_mask) > (c-rounding_errors))
s.add((results_[i] & _53_mask) < (c+rounding_errors))
# enumerate all solutions:
results=[]
while s.check() == sat:
m = s.model()
print (m)
results.append(m)
block = []
for d in m:
t=d()
block.append(t != m[d])
s.add(Or(block))
print ("results total=", len(results))
There are must be only one solution:
[state_b_ = 17648855221291934500, state_a_ = 10330653656338108972] results total= 1
Plug in these values into my C code and see:
0.57960024210385441279 0.12380356735099862231 0.31643416402630619721 0.10154960825287195902 0.69791051668756087789 0.48427588721160741425 0.03867662331649868168 0.09293509478430383997 0.07472055176571934521 0.74212555060901441717 0.25197939832412108441 0.18063271919434797930 0.19558750472843866586 0.08712006860073973069 0.80613333326014424696 0.58272219940808434036 0.30629055345756017736 0.12242741891787367603 0.18006629559552012054 0.92675719287678004488
All perfect.
Also, I wanted to know if Math.random() can generate 5 consecutive numbers close to zero?
Let's modify our Z3Py script:
--- recover_state.py 2026-02-02 17:30:30.653222579 +0100
+++ recover_state_zeroes.py 2026-02-02 17:24:42.021407386 +0100
@@ -2,21 +2,18 @@
from z3 import *
-OUTPUTS=[
-0.5796002421038544,
-0.12380356735099862,
-0.3164341640263062]
-
-def get_53bit_mantissa(i):
- # 0x1.0p-53:
- divisor=0.00000000000000011102230246251565404236316680908203125
- return int(i//divisor)
+ZEROES=6
-STATES=len(OUTPUTS)
+STATES=ZEROES
+
+s = Solver()
a_ = BitVec('state_a_', 64)
b_ = BitVec('state_b_', 64)
+s.add(a_!=0)
+s.add(b_!=0)
+
def RandUint64():
global a_, b_
t = a_
@@ -30,19 +27,16 @@
return t + s
-s = Solver()
-
results_=[]
-for i in range(len(OUTPUTS)):
+for i in range(ZEROES):
x=RandUint64()
results_.append(x)
-for i in range(len(OUTPUTS)):
+for i in range(ZEROES):
_53_mask=(1<<53)-1
- c=get_53bit_mantissa(OUTPUTS[i])
- rounding_errors=1
- s.add((results_[i] & _53_mask) > (c-rounding_errors))
- s.add((results_[i] & _53_mask) < (c+rounding_errors))
+ rounding_errors=1<<31
+ s.add((results_[i] & _53_mask) > 0)
+ s.add((results_[i] & _53_mask) < rounding_errors)
# enumerate all solutions:
results=[]
Only one solution generated:
[state_b_ = 9007200328482944, state_a_ = 81350674939913364] results total= 1
Plug initial states into my C code:
0.00000011920930376164 0.00000000000001421085 0.00000000000002842171 0.00000011921021325634 0.00000011921021503269 0.00000011926752918612 0.00000011932674581772 0.00048828503544706692 0.00048923865054684157 0.03174055001003184273 0.06353915541073096307 0.06355417572480970279 ...
This blog post was inspited by Douglas Goddard's post.