LAWS.bend source

LAWS.bend on the hub · documented module

# 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 Baseimport ./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 == 32law bounded_seed42_mod100:  { P.Prng.next_bounded_value(P.Prng.seed(42), 100) == 32 : U32 }