Comment on Who's up for a challenge?

• e0qdk@kbin.social ⁨11⁩ ⁨months⁩ ago

  Can Z3 account for lost bits? Did it come up with just one solution?

  It gave me just one solution the way I asked for it. With additional constraints added to exclude the original solution, it also gives me a second solution -- but the solution it produces is peculiar to my implementation and does not match your implementation. If you implemented exactly how the bits are supposed to end up in the result, you could probably find any other solutions that exist correctly, but I just did it in a quick and dirty way.

  This is (with a little clean up) what my code looked like:

  ::: spoiler solver code
  #!/usr/bin/env python3

  import z3
  
  rand1 = 0.38203435111790895
  rand2 = 0.5012949781958014
  rand3 = 0.5278898433316499
  rand4 = 0.5114834443666041
  
  def xoshiro128ss(a,b,c,d):
      t = 0xFFFFFFFF & (b << 9)
      r = 0xFFFFFFFF & (b * 5)
      r = 0xFFFFFFFF & ((r << 7 | r >> 25) * 9)
      c = 0xFFFFFFFF & (c ^ a)
      d = 0xFFFFFFFF & (d ^ b)
      b = 0xFFFFFFFF & (b ^ c)
      a = 0xFFFFFFFF & (a ^ d)
      c = 0xFFFFFFFF & (c ^ t)
      d = 0xFFFFFFFF & (d << 11 | d >> 21)
      return r, (a, b, c, d)
  
  a,b,c,d = z3.BitVecs("a b c d", 64)
  nodiv_rand1, state = xoshiro128ss(a,b,c,d)
  nodiv_rand2, state = xoshiro128ss(*state)
  nodiv_rand3, state = xoshiro128ss(*state)
  nodiv_rand4, state = xoshiro128ss(*state)
  
  z3.solve(a >= 0, b >= 0, c >= 0, d >= 0, 
    nodiv_rand1 == int(rand1*4294967296),
    nodiv_rand2 == int(rand2*4294967296),
    nodiv_rand3 == int(rand3*4294967296),
    nodiv_rand4 == int(rand4*4294967296)
    )
  

  :::

  I never heard about Z3

  If you're not familiar with SMT solvers, they are a useful tool to have in your toolbox. Here are some links that may be of interest:

  • https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
  • https://en.wikipedia.org/wiki/Z3_Theorem_Prover

  source

  • ExLisper@linux.community ⁨11⁩ ⁨months⁩ ago

    a >= 0, b >= 0, c >= 0, d >= 0

    I think that’s the issue, in the second possible solution one of the parameters is negative :)

    This looks great, I didn’t even know it’s possible to solve it this way. I’m glad someone dedicated some time to it. Let’s see if anyone will try solving it in other way.

    source