diff --git a/xs128p.py b/xs128p.py index a4b762a..0fcf83b 100644 --- a/xs128p.py +++ b/xs128p.py @@ -2,7 +2,7 @@ import sys import math import struct import random -sys.path.append('/home/dgoddard/tools/z3/build/') +sys.path.append('/home/taxicat/prog/z3/build') from z3 import * # xor_shift_128_plus algorithm @@ -41,6 +41,26 @@ def sym_xs128p(slvr, sym_state0, sym_state1, generated, browser): slvr.add(impl) return sym_state0, sym_state1, [condition] +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 xs128p_backward(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) + generated = (prev_state0 + prev_state1) & 0xFFFFFFFFFFFFFFFF + return prev_state0, prev_state1, generated + # Print 'last seen' random number # and winning numbers following that. # This was for debugging. We know that Math.random() @@ -73,7 +93,7 @@ def power_ball(generated, browser): nums.append(val) # print indicator - if idx == 4 and browser == 'chrome': + if idx == 0 and browser == 'chrome': print '--->', elif idx == 2 and browser == 'firefox': print '--->', @@ -93,6 +113,16 @@ def power_ball(generated, browser): # ((rand_uint64 & ((1 << 52) - 1)) | 0x3FF0000000000000) - 1.0 # Safari weakRandom.get(): # (rand_uint64 & ((1 << 53) - 1) * (1.0 / (1 << 53))) +def to_double(browser, out): + if browser == 'chrome': + double_bits = (out & 0xFFFFFFFFFFFFF) | 0x3FF0000000000000 + double = struct.unpack('d', struct.pack('