1.5. Deterministic bounded randomness🔗

structure

Hex.Rand : Type
Hex.Rand : Type

A splitmix64 state. Deterministic, seedable, and reproducible across runs and platforms; this is a source of arbitrary values for Las Vegas search, not a cryptographic generator, and nothing in the tree may treat it as one.

Constructor

Hex.Rand.mk

Fields

state : UInt64

The 64-bit generator state.

def

Hex.Rand.next (r : Hex.Rand) : UInt64 × Hex.Rand
Hex.Rand.next (r : Hex.Rand) :
  UInt64 × Hex.Rand

Advance the splitmix64 state and produce one 64-bit output.

def

Hex.Rand.nat (r : Hex.Rand) (bound fuel : Nat) :
  Except Hex.RandError (Nat × Hex.Rand)
Hex.Rand.nat (r : Hex.Rand)
  (bound fuel : Nat) :
  Except Hex.RandError (Nat × Hex.Rand)

Draw a natural number below bound by rejection sampling: form a candidate from enough 64-bit words and reject the incomplete top interval (rather than folding it in with next % bound, which would add modulo bias). fuel bounds the rejection retries, including the initial candidate; bound = 0 returns zeroBound.

The state is explicit and reproducible. Bounded draws use rejection sampling, return the advanced state, and consume explicit fuel; they never introduce global randomness or an unbounded search. The generator is suitable for Las Vegas algorithm scheduling, not cryptography.

open Hex

namespace HexBasicChapter

#guard (Rand.ofSeed 0).next.1 = 0xe220a8397b1dcdaf
#guard ((Rand.ofSeed 1).nat 10 8).isOk

end HexBasicChapter