structure Hex.GraphIso.Random.Gen : Type

SplitMix64 state.

• state : UInt64

  The current stream state.

@[instance_reducible]

instance Hex.GraphIso.Random.instInhabitedGen : Inhabited Gen

Equations

• Hex.GraphIso.Random.instInhabitedGen = { default := Hex.GraphIso.Random.instInhabitedGen.default }

def Hex.GraphIso.Random.seed1 : UInt64

The first corpus seed.

Equations

• Hex.GraphIso.Random.seed1 = 2611923443488327891

def Hex.GraphIso.Random.seed2 : UInt64

The second corpus seed.

Equations

• Hex.GraphIso.Random.seed2 = 1376283091369227076

def Hex.GraphIso.Random.next (g : Gen) : UInt64 × Gen

One SplitMix64 step: the next output and the advanced state.

Equations

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

def Hex.GraphIso.Random.nextBelow (g : Gen) (m : Nat) : Nat × Gen

A uniform value below m by threshold rejection: draws are discarded while they lie at or above 2^64 - (2^64 % m), then reduced. m = 0 returns 0 without consuming the stream.

Equations

• Hex.GraphIso.Random.nextBelow g m = if m = 0 then (0, g) else Hex.GraphIso.Random.nextBelow.go m g (64 + 2 * m)

def Hex.GraphIso.Random.nextBelow.go (m : Nat) (g : Gen) : Nat → Nat × Gen

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Random.nextBelow.go m g 0 = (0, g)

def Hex.GraphIso.Random.gnpMask (g : Gen) (n : Nat) : Nat × Gen

The Erdős–Rényi graph G(n, 1/2): one low bit per vertex pair (i, j), i < j, in lexicographic order. Returns the adjacency bitmask over pairs in that order.

Equations

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

def Hex.GraphIso.Random.shuffle (g : Gen) (a : Array Nat) : Array Nat × Gen

Fisher-Yates shuffle from the last position down.

Equations

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

def Hex.GraphIso.Random.ontoColoring (g : Gen) (n k : Nat) : Array Nat × Gen

A uniformly shuffled onto k-colouring of n ≥ k vertices: start from i % k and shuffle.

Equations

• Hex.GraphIso.Random.ontoColoring g n k = Hex.GraphIso.Random.shuffle g (Array.ofFn fun (i : Fin n) => ↑i % k)