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:
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
Edit: Trying to fix formatting differences between kbin and lemmy
Edit 2: Spoiler tags and code blocks don’t seem to play well together. I’ve got it mostly working on Lemmy (where I’m guessing most people will see the comment), but I don’t think I can fix it on kbin.
It’s not a GUI library, but Jupyter was pretty much made for the kind of mathematical/scientific exploratory programming you’re interested in doing. It’s not the right tool for making finished products, but is intended for creating lab notebooks that contain executable code snippets, formatted text, and visual output together. Given your background experience and the libraries you like, it seems like it’d be right up your alley.