v8 java script z3 math.floor and math.random predict next number

gistfile1.txt

#!/usr/bin/python3
import math

import z3
import struct
import sys
import numpy
from decimal import Decimal

from z3 import Or

""" 
Solving for seed states in XorShift128+ used in V8
> https://v8.dev/blog/math-random
> https://apechkurov.medium.com/v8-deep-dives-random-thoughts-on-math-random-fb155075e9e5
> https://blog.securityevaluators.com/hacking-the-javascript-lottery-80cc437e3b7f

> Tested on Chrome(102.0.5005.61) or Nodejs(v18.2.0.) 
"""

"""
Plug in a handful random number sequences from node/chrome
> Array.from(Array(5), Math.random)

(Optional) In node, we can specify the seed
> node --random_seed=1337
"""

multi = 5000 # multiplier before math.random
sequence = [
    2415,
    3331,
    2574,
    496,
    2699,
    4109,
    538,
    428,
    266,
    164,
    2455,
    3924,
    2811,
    2772,
    #2813,

] # values from math.floor(math.random() * multi)
boundaries = []
categories = []


def count_leading_bits(n1, n2):
    # Convert the numbers to binary and remove the '0b' prefix
    bin1 = bin(n1)[2:].zfill(52)
    bin2 = bin(n2)[2:].zfill(52)

    # Initialize the count of leading bits
    count = []

    # Iterate over the bits
    for b1, b2 in zip(bin1, bin2):
        if b1 == b2:
            count += b1
        else:
            break

    return count


for i in range(multi):
    number = i / multi + 1
    if Decimal(number) * Decimal(multi) < Decimal(i):
        number = numpy.nextafter(number, 1)
    if Decimal(number) * Decimal(multi) < Decimal(i):
        raise Exception("can not be")
    float_64 = struct.pack("d", number)
    u_long_long_64 = struct.unpack("<Q", float_64)[0]

    mantissa = u_long_long_64 & ((1 << 52) - 1)
    boundaries.append(mantissa)

highest_52_bit_number = '1' * 52
highest_52_bit_number_int = int(highest_52_bit_number, 2)

boundaries.append(highest_52_bit_number_int)

for i in range(multi):
    lower = boundaries[i]
    upper = boundaries[i + 1] -1
    categories.append(count_leading_bits(lower, upper))

"""
Random numbers generated from xorshift128+ is used to fill an internal entropy pool of size 64
> https://github.com/v8/v8/blob/7a4a6cc6a85650ee91344d0dbd2c53a8fa8dce04/src/numbers/math-random.cc#L35

Numbers are popped out in LIFO(Last-In First-Out) manner, hence the numbers presented from the entropy pool are reveresed.
"""
sequence = sequence[::-1]

solver = z3.Solver()

"""
Create 64 bit states, BitVec (uint64_t)
> static inline void XorShift128(uint64_t* state0, uint64_t* state1);
> https://github.com/v8/v8/blob/a9f802859bc31e57037b7c293ce8008522ca03d8/src/base/utils/random-number-generator.h#L119
"""
se_state0, se_state1, se_state2 = z3.BitVecs("se_state0 se_state1 se_state2", 64)

for i in range(len(sequence)):
    """
    XorShift128+
    > https://vigna.di.unimi.it/ftp/papers/xorshiftplus.pdf
    > https://github.com/v8/v8/blob/a9f802859bc31e57037b7c293ce8008522ca03d8/src/base/utils/random-number-generator.h#L119

    class V8_BASE_EXPORT RandomNumberGenerator final {
        ...
        static inline void XorShift128(uint64_t* state0, uint64_t* state1) {
            uint64_t s1 = *state0;
            uint64_t s0 = *state1;
            *state0 = s0;
            s1 ^= s1 << 23;
            s1 ^= s1 >> 17;
            s1 ^= s0;
            s1 ^= s0 >> 26;
            *state1 = s1;
        }
        ...
    }
    """
    se_s1 = se_state0
    se_s0 = se_state1
    se_state0 = se_s0
    se_s1 ^= se_s1 << 23
    se_s1 ^= z3.LShR(se_s1, 17)  # Logical shift instead of Arthmetric shift
    se_s1 ^= se_s0
    se_s1 ^= z3.LShR(se_s0, 26)
    se_state1 = se_s1

    output_random = sequence[i]
    category = categories[output_random]

    binary_string = ''.join(category)
    cat_number = int(binary_string, 2)
    # Compare Mantissas
    solver.add(cat_number == z3.LShR(se_state0, (12 + (52-len(category)))))
#solver.add(se_state1 == se_state2) comment in to reverse

if solver.check() == z3.sat:
    model = solver.model()

    states = {}
    for state in model.decls():
        states[state.__str__()] = model[state]

    print(states)
    solver.add(Or([model[decl] != decl() for decl in model.decls()]))

    # Check if there is another solution
    if solver.check() == z3.sat:
        print("There is more than one solution.")
    else:
        print("There is a unique solution.")

    state0 = states["se_state0"].as_long() # se_state2 to reverse order

    """
    Extract mantissa
    - Add `1.0` (+ 0x3FF0000000000000) to 52 bits
    - Get the double and Subtract `1` to obtain the random number between [0, 1)

    > https://github.com/v8/v8/blob/a9f802859bc31e57037b7c293ce8008522ca03d8/src/base/utils/random-number-generator.h#L111

    static inline double ToDouble(uint64_t state0) {
        // Exponent for double values for [1.0 .. 2.0)
        static const uint64_t kExponentBits = uint64_t{0x3FF0000000000000};
        uint64_t random = (state0 >> 12) | kExponentBits;
        return base::bit_cast<double>(random) - 1;
    }
    """
    u_long_long_64 = (state0 >> 12) | 0x3FF0000000000000
    float_64 = struct.pack("<Q", u_long_long_64)
    next_sequence = struct.unpack("d", float_64)[0]
    next_sequence -= 1

    print(math.floor(next_sequence*multi))

print("There is more than one solution.") means multiplier is too small or number of entries is too small.
For a unique solution you will need need a multipliere ~>2000 and ~15 entries

Be aware the seed is changed after 64 numbers