UNSAT Condition Always

[NightZpy]

Why always get UNSAT condition?

Screenshot

[TACIXAT]

The code broke from Chrome shortly after publishing. I haven't had time to fix it yet as I'm unsure what changed.

[psrok1]

I think that in V8, things are going backwards...

On startup, V8 generates small buffer with double values from XorShift128+ PRNG. Math.random() calls are reading from it, starting from the last position.

Piece of code from Node.js 7.0.0 (deps/v8/src/js/math.js):

//-------------------------------------------------------------------
// ECMA 262 - 15.8.2.14
function MathRandom() {
  // While creating a startup snapshot, %GenerateRandomNumbers returns a
  // normal array containing a single random number, and has to be called for
  // every new random number.
  // Otherwise, it returns a pre-populated typed array of random numbers. The
  // first two elements are reserved for the PRNG state.
  if (nextRandomIndex <= kRandomNumberStart) {
    randomNumbers = %GenerateRandomNumbers(randomNumbers);
    if (%_IsTypedArray(randomNumbers)) {
      nextRandomIndex = %_TypedArrayGetLength(randomNumbers);
    } else {
      nextRandomIndex = randomNumbers.length;
    }
  }
  return randomNumbers[--nextRandomIndex];
}

[TACIXAT]

Ah, great find!

I reversed the array of rands (generated in Chromium) and got a SAT condition.

BROWSER: chrome
[0.21547668544366472, 0.6806077271641113, 0.9907360195029462]
0.770965940013
     [2, 15, 30, 54, 61] 15
0.872839138401
     [2, 15, 30, 40, 55] 17
0.0199015806922
     [14, 30, 40, 44, 55] 16
0.785316824102
     [14, 30, 40, 41, 44] 11
0.201477628876
---> [27, 30, 40, 41, 44] 22

[TACIXAT]

Alright, let's look at reversing the algorithm.

0   def xs128p(state0, state1):
1       s1 = state0 
2       s0 = state1 
3       s1 ^= (s1 << 23) 
4       s1 ^= (s1 >> 17) 
5       s1 ^= s0 
6       s1 ^= (s0 >> 26)  
7       state0 = state1 
8       state1 = s1 
9       generated = (state0 + state1) 
10
11      return state0, state1, generated

We recover the current state and then we need to recover previous numbers. We have 4 operations, lines 3-6. We can reverse lines 6 and 5 easily since we have s0 (state1, now state0), since that was unmodified.

For line 4, we can recover the original value 17 bits at a time.

def forward17(val):
    modded = val ^ (val >> 17)
    print hex(modded)
    return modded

def reverse17(val):
    top34 = (val ^ (val >> 17)) & 0xFFFFFFFFC0000000
    top51 = (val ^ (top34 >> 17)) & 0xFFFFFFFFFFFFE000
    original = (val ^ (top51 >> 17))
    print hex(original)
    return original

>>> modded = forward17(0xdeadbea7b0b1e7ea)
0xdeadd1f16fe23fb2L
>>> recovered = reverse17(modded)
0xdeadbea7b0b1e7eaL
>>> print recovered == 0xdeadbea7b0b1e7ea
True

A similar process can be used to recover line 3, 23 bits at a time.

def forward23(val):
    modded = val ^ (val << 23) & 0xFFFFFFFFFFFFFFFF
    print hex(modded)
    return modded

def reverse23(val):
    bot46 = (val ^ (val << 23)) & 0x3fffffffffff
    original = (val ^ (bot46 <<  23)) & 0xFFFFFFFFFFFFFFFF
    print hex(original)
    return original

>>> modded = forward23(0xdeadbea7b0b1e7ea)
0x8d75e65445b1e7eaL
>>> recovered = reverse23(modded)
0xdeadbea7b0b1e7eaL
>>> print recovered == 0xdeadbea7b0b1e7ea
True

Given all that, our reverse process will look something like this.

def reverse23(val):
    bot46 = (val ^ (val << 23)) & 0x3fffffffffff
    original = (val ^ (bot46 <<  23)) & 0xFFFFFFFFFFFFFFFF
    return original

def reverse17(val):
    top34 = (val ^ (val >> 17)) & 0xFFFFFFFFC0000000
    top51 = (val ^ (top34 >> 17)) & 0xFFFFFFFFFFFFE000
    original = (val ^ (top51 >> 17))
    return original

def get_prev_state(state0, state1):
    prev_state1 = state0
    prev_state0 = state1 ^ (state0 >> 26)
    prev_state0 = prev_state0 ^ state0
    prev_state0 = reverse17(prev_state0)
    prev_state0 = reverse23(prev_state0)
    return prev_state0, prev_state1

# xor_shift_128_plus algorithm
def xs128p(state0, state1):
    s1 = state0 & 0xFFFFFFFFFFFFFFFF
    s0 = state1 & 0xFFFFFFFFFFFFFFFF
    s1 ^= (s1 << 23) & 0xFFFFFFFFFFFFFFFF
    s1 ^= (s1 >> 17) & 0xFFFFFFFFFFFFFFFF
    s1 ^= s0 & 0xFFFFFFFFFFFFFFFF
    s1 ^= (s0 >> 26) & 0xFFFFFFFFFFFFFFFF 
    state0 = state1 & 0xFFFFFFFFFFFFFFFF
    state1 = s1 & 0xFFFFFFFFFFFFFFFF
    generated = (state0 + state1) & 0xFFFFFFFFFFFFFFFF
    return state0, state1, generated

>>> state0 = 0xdeadbea7b0b1e7ea
>>> state1 = 0xea7f1eecef00dbae
>>> state0, state1, gen = xs128p(state0, state1)
>>> state0, state1 = get_prev_state(state0, state1)
>>> print hex(state0)
0xdeadbea7b0b1e7eaL
>>> print hex(state1)
0xea7f1eecef00dbaeL
>>> state0 = 0xdeadbea7b0b1e7ea
>>> state1 = 0xea7f1eecef00dbae
>>> state0, state1, gen = xs128p(state0, state1)
>>> print hex(state0)
0xea7f1eecef00dbaeL
>>> print hex(state1)
0x670abe38c65ca5a7L
>>> state0, state1 = get_prev_state(state0, state1)
>>> print hex(state0)
0xdeadbea7b0b1e7eaL
>>> print hex(state1)
0xea7f1eecef00dbaeL

I'll integrate this when I have some time.

[TACIXAT]

Works now for me in Chromium with uBlock. No more Math.random() calls on click in Chrome, so I moved the arrow on the output too.

Thanks for finding that psrok1!