~/bend-docscommunity

LAWS.bend open laws/TODOs

raw source on the hub · import 0xfd7037736e4fa1794a671d0278638da7/LAWS.bend as LAWS

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.

2 imports
import Base
import ./lib.bend as P

Laws

law seed_zero_aliases_one provedin PROOF.bendsource · line 10 · raw

{0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(0) == 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(1) : 0xfd7037736e4fa1794a671d0278638da7/lib.Prng}

Zero seed is rewritten to 1 before the first step.

law seed1_first provedin PROOF.bendsource · line 14 · raw

{0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_value(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(1)) == 270369 : U32}

Concrete first outputs for fixed seeds (xorshift32 reference vectors).

law seed1_second provedin PROOF.bendsource · line 17 · raw

{0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_value(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_state(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(1))) == 67634689 : U32}

law seed42_first provedin PROOF.bendsource · line 20 · raw

{0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_value(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42)) == 11355432 : U32}

law same_seed_same_first provedin PROOF.bendsource · line 24 · raw

{0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_value(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(7)) == 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_value(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(7)) : U32}

Same seed always yields the same first value (determinism).

law next_value_is_state provedin PROOF.bendsource · line 28 · raw

{0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_value(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42)) == 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.state(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_state(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42))) : U32}

The returned value is exactly the new internal state.

law bounded_max1_zero provedin PROOF.bendsource · line 36 · raw

{0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_bounded_value(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(1), 1) == 0 : U32}

Bounded draws: max 1 always yields 0; max 0 is documented to yield 0.

law bounded_max0_zero provedin PROOF.bendsource · line 39 · raw

{0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_bounded_value(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(1), 0) == 0 : U32}

law bounded_seed42_mod100 provedin PROOF.bendsource · line 43 · raw

{0xfd7037736e4fa1794a671d0278638da7/lib.Prng.next_bounded_value(0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42), 100) == 32 : U32}

11355432 mod 100 == 32