A cool program to generate perfect brackets for Sportsball

z3xorshift.py

import requests
from z3 import *

# 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
    generated &= 0x0FFFFFFFFFFFFF # this was the part that tripped us up. Didn't realize we had to do this and operation here
    return state0, state1, generated

#xorshift128+ for symbolic objects (z3)
def sym_xs128p(sym_state0, sym_state1, last_generated):
    s1 = sym_state0
    s0 = sym_state1
    s1 ^= (s1 << 23)
    s1 ^= LShR(s1, 17)
    s1 ^= s0
    s1 ^= LShR(s0, 26)
    newSym_state0 = sym_state1
    newSym_state1 = s1
    new_generated = (newSym_state0 + newSym_state1)
    new_generated &= 0x0FFFFFFFFFFFFF
    return newSym_state0, newSym_state1, new_generated

#z3 BitVecs for the 2 seeds
ostate0, ostate1 = BitVecs('ostate0 ostate1', 64)
sym_state0 = ostate0
sym_state1 = ostate1
slvr = Solver()


print "generating new vals"
generated = []


# fetch the current xorshift128+ output and parse it
generated = requests.get("https://sports.haxkcd.com/{username}/xorshift128plus").text
generated = generated.replace("\n","").replace(" ","").replace("[","").replace("]","").split(",")
generated = [int(x) for x in generated]

print "generated="
print generated
print len(generated)
print "Adding constraints..."

# add 6 constraints and hope that it's enough. z3 is magic
for ea in range(6):
    sym_state0, sym_state1, nextGen = sym_xs128p(sym_state0, sym_state1, generated[ea])
    slvr.add(nextGen==generated[ea+1])

print "Check SAT..."
if slvr.check() == sat:
    # get a solved state
    m = slvr.model()
    print m
    ostate0val= m[ostate0].as_long()
    ostate1val= m[ostate1].as_long()

    # regenerate the GET request vals
    selfgen = []
    for x in range(199):
        ostate0val, ostate1val, gen = xs128p(ostate0val, ostate1val)
        selfgen.append(gen)
    print selfgen
    verify = generated[1:200]

    # check to make sure all our generated vals with the seed match up with what we got from the GET request
    success = True
    for x in range(len(verify)):
        if verify[x]!=selfgen[x]:
            success = False
    print "Success=%r"%success

    # generate the next val!
    print "Next val in pRNG:"
    ostate0val, ostate1val, gen = xs128p(ostate0val, ostate1val)
    print gen
    #now we just use this value by calling add_winners(gen); in the JS console on the site
    #this will regenerate the "last years winners" table and we just copy it into our prediction for this year and submit!
else:
    print "UNSAT!"