# Definitional laws for Prng (xorshift32 over U32).
#
# Zero-seed policy: Prng.seed(0) aliases Prng.seed(1). Raw xorshift32 has a
# fixed point at 0, so an empty/zero seed would otherwise emit an infinite
# stream of zeros. Non-zero seeds are stored unchanged.
import Base
import ./lib.bend as P

# Zero seed is rewritten to 1 before the first step.
law seed_zero_aliases_one:
  { P.Prng.seed(0) == P.Prng.seed(1) : P.Prng }

# Concrete first outputs for fixed seeds (xorshift32 reference vectors).
law seed1_first:
  { P.Prng.next_value(P.Prng.seed(1)) == 270369 : U32 }

law seed1_second:
  { P.Prng.next_value(P.Prng.next_state(P.Prng.seed(1))) == 67634689 : U32 }

law seed42_first:
  { P.Prng.next_value(P.Prng.seed(42)) == 11355432 : U32 }

# Same seed always yields the same first value (determinism).
law same_seed_same_first:
  { P.Prng.next_value(P.Prng.seed(7)) == P.Prng.next_value(P.Prng.seed(7)) : U32 }

# The returned value is exactly the new internal state.
law next_value_is_state:
  {
    P.Prng.next_value(P.Prng.seed(42))
      == P.Prng.state(P.Prng.next_state(P.Prng.seed(42)))
    : U32
  }

# Bounded draws: max 1 always yields 0; max 0 is documented to yield 0.
law bounded_max1_zero:
  { P.Prng.next_bounded_value(P.Prng.seed(1), 1) == 0 : U32 }

law bounded_max0_zero:
  { P.Prng.next_bounded_value(P.Prng.seed(1), 0) == 0 : U32 }

# 11355432 mod 100 == 32
law bounded_seed42_mod100:
  { P.Prng.next_bounded_value(P.Prng.seed(42), 100) == 32 : U32 }