rng.smt

(set-logic QF_BV)

; Quicker way to find fixpoints in the rng discussed in
; https://roadrunnerwmc.github.io/blog/2020/05/08/nsmb-rng.html .
;
; On my machine (AMD Ryzen 5 3550H with 8G RAM), running this with z3
; finds a fixedpoint in about 80 seconds

; Here's the code we'll be  modelling:
;
; uint32_t rand_nsmb(uint32_t *state) {
;     uint64_t value = (uint64_t)(*state) * 1664525 + 1013904223;
;     return *state = value + (value >> 32);
; }

(declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(declare-const shift (_ BitVec 64))

; smt-lib is a bit user unfriendly in the way you have to handle bit
; vector literals it seems. Could be I'm missing a trick?
(assert (= a (_ bv1664525 64)))
(assert (= b (_ bv1013904223 64)))
(assert (= shift (_ bv32 64)))


(define-fun rng ((state (_ BitVec 32))) (_ BitVec 32)
        (let (
                (value  (bvadd (bvmul ((_ zero_extend 32) state) a) b))
            ) (( _ extract 31 0) (bvadd value (bvlshr value shift)))
        )
)

(declare-const s (_ BitVec 32))

(assert (= s (rng s)))

(check-sat)
(get-value (s))