Programming

17490 readers

74 users here now

Welcome to the main community in programming.dev! Feel free to post anything relating to programming here!

Cross posting is strongly encouraged in the instance. If you feel your post or another person's post makes sense in another community cross post into it.

Hope you enjoy the instance!

Rules

Follow the programming.dev instance rules
Keep content related to programming in some way
If you're posting long videos try to add in some form of tldr for those who don't want to watch videos

Wormhole

Follow the wormhole through a path of communities [email protected]

founded 1 year ago

MODERATORS

[email protected]

Who's up for a challenge? (linux.community)

submitted 9 months ago by [email protected] to c/[email protected]

9 comments fedilink hide all child comments

Hi all,

Some time ago I've been thinking about a programming challenge that's not simply another HackerRank style algorithm task and came up with something that I myself had a lot of fun solving. It goes like this:

We have a well known function (as in I didn't come up with it):

 function xoshiro128ss(a, b, c, d) {
                return function() {
                    var t = b << 9, r = b * 5; r = (r << 7 | r >>> 25) * 9;
                    c ^= a; 
                    d ^= b;
                    b ^= c; 
                    a ^= d; 
                    c ^= t;
                    d = d << 11 | d >>> 21;
                    
                    return (r >>> 0) / 4294967296;
                }
            }

We initialize it with 4 random parameters a,b,c,d (that I selected) :

  let rnd = xoshiro128ss(a, b, c, d);

and we do:

  let rand1 = rnd();
  let rand2 = rnd();
  let rand3 = rnd();
  let rand4 = rnd();

Knowing that:

rand1 == 0.38203435111790895
rand2 == 0.5012949781958014
rand3 == 0.5278898433316499
rand4 == 0.5114834443666041

What are the values of a,b,c and d?

I was wandering if it's possible to figure it out and couldn't stop trying until I did. It was an interesting journey and I learned some new things along the way Maybe someone else here will also have fun with it. As for prizes, I don't know... whoever posts the right answer first gets an upvote and eternal fame.

you are viewing a single comment's thread
view the rest of the comments

[–] [email protected] 8 points 9 months ago (1 children)

If I understand the problem correctly, this is the solution:

solution

a = 2299200278
b = 2929959606
c = 2585800174
d = 3584110397

I solved it with Z3. Took less than a second of computer time, and about an hour of my time -- mostly spent trying to remember how the heck to use Z3 and then a little time debugging my initial program.

[–] [email protected] 4 points 9 months ago (1 children)

Yep, that's correct. I never heard about Z3 and I did it by reverting all the operation. It takes couple of seconds of computer time to solve my way but it took me closer to 7h to figure it out. 1h is impressive.

There are actually two possible solutions because some bits are lost when generating numbers. Can Z3 account for lost bits? Did it come up with just one solution?

[–] [email protected] 4 points 9 months ago* (last edited 9 months ago) (1 children)

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:

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.

[–] [email protected] 3 points 9 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.