structure 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.

• state : UInt64

  The 64-bit generator state.

def Hex.instReprRand.repr : Rand → Nat → Std.Format

Equations

• Hex.instReprRand.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "state" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.state)).group) " }"

@[instance_reducible]

instance Hex.instReprRand : Repr Rand

Equations

• Hex.instReprRand = { reprPrec := Hex.instReprRand.repr }

@[instance_reducible]

instance Hex.instDecidableEqRand : DecidableEq Rand

Equations

• Hex.instDecidableEqRand = Hex.instDecidableEqRand.decEq

def Hex.instDecidableEqRand.decEq (x✝ x✝¹ : Rand) : Decidable (x✝ = x✝¹)

Equations

• Hex.instDecidableEqRand.decEq { state := a } { state := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

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

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

Equations

• One or more equations did not get rendered due to their size.

inductive Hex.RandError : Type

Why a bounded draw failed.

• zeroBound : RandError

  The requested bound was 0, so no value below it exists.

• exhausted (attempts : Nat) (rand : Rand) : RandError

  Rejection sampling ran out of fuel; the attempt count and the advanced state are returned so the caller can resume rather than replay a failed stream.

@[instance_reducible]

instance Hex.instReprRandError : Repr RandError

Equations

• Hex.instReprRandError = { reprPrec := Hex.instReprRandError.repr }

def Hex.instReprRandError.repr : RandError → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Hex.instReprRandError.repr Hex.RandError.zeroBound prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hex.RandError.zeroBound")).group prec✝

def Hex.Rand.words (r : Rand) : Nat → Nat × Rand

Concatenate w fresh 64-bit words into one natural number below 2 ^ (64 * w).

Equations

• r.words 0 = (0, r)
• r.words w.succ = match r.next with | (x, r') => match r'.words w with | (rest, r'') => (rest <<< 64 ||| x.toNat, r'')

def Hex.Rand.nat (r : Rand) (bound fuel : Nat) : Except RandError (Nat × 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.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Rand.ofSeed (seed : Nat) : Rand

Construct the initial state from a seed.

Equations

• Hex.Rand.ofSeed seed = { state := UInt64.ofNat seed }

theorem Hex.Rand.nat_lt {r : Rand} {bound fuel v : Nat} {r' : Rand} (h : r.nat bound fuel = Except.ok (v, r')) : v < bound

Range correctness: a successful bounded draw is below the bound.