Mersenne Twister

Generic implementation for the Mersenne Twister pseudorandom number generator.

All choices of parameters from Matsumoto and Nishimura (1998) are supported, along with later refinements. Parameters for the standard 32-bit MT19937 and 64-bit MT19937-64 algorithms are provided. Both RandomGen and Stream interfaces are provided.

Use mt19937.init seed to create a MT19937 PRNG with a 32 bit seed value; use mt19937_64.init seed to create a MT19937-64 PRNG with a 64 bit seed value. If omitted, default seed choices will be used.

Sample usage:

import Batteries.Data.Random.MersenneTwister

open Batteries.Random.MersenneTwister

def mtgen := mt19937.init -- default seed 4357

#eval (Stream.take mtgen 5).fst -- [874448474, 2424656266, 2174085406, 1265871120, 3155244894]

References:

• Matsumoto, Makoto and Nishimura, Takuji (1998), Mersenne twister: A 623-dimensionally equidistributed uniform pseudo-random number generator, ACM Trans. Model. Comput. Simul. 8, No. 1, 3-30. ZBL0917.65005.

• Nishimura, Takuji (2000), Tables of 64-bit Mersenne twisters, ACM Trans. Model. Comput. Simul. 10, No. 4, 348-357. ZBL1390.65014.

structure Batteries.Random.MersenneTwister.Config : Type

Mersenne Twister configuration.

Letters in parentheses correspond to variable names used by Matsumoto and Nishimura (1998) and Nishimura (2000).

• wordSize : Nat

  Word size (w).

• stateSize : Nat

  Degree of recurrence (n).

• shiftSize : Fin self.stateSize

  Middle word (m).

• maskBits : Fin self.wordSize

  Twist value (r).

• xorMask : BitVec self.wordSize

  Coefficients of the twist matrix (a).

• temperingShifts : Nat × Nat × Nat × Nat

  Tempering shift parameters (u, s, t, l).

• temperingMasks : BitVec self.wordSize × BitVec self.wordSize × BitVec self.wordSize

  Tempering mask parameters (d, b, c).

• initMult : BitVec self.wordSize

  Initialization multiplier (f).

• initSeed : BitVec self.wordSize

  Default initialization seed value.

@[simp]

theorem Batteries.Random.MersenneTwister.Config.zero_lt_wordSize (cfg : Batteries.Random.MersenneTwister.Config) : 0 < cfg.wordSize

@[simp]

theorem Batteries.Random.MersenneTwister.Config.zero_lt_stateSize (cfg : Batteries.Random.MersenneTwister.Config) : 0 < cfg.stateSize

structure Batteries.Random.MersenneTwister.State (cfg : Batteries.Random.MersenneTwister.Config) : Type

Mersenne Twister State.

• data : Vector (BitVec cfg.wordSize) cfg.stateSize

  Data for current state.

• index : Fin cfg.stateSize

  Current data index.

@[specialize #[0]]

def Batteries.Random.MersenneTwister.Config.init (cfg : Batteries.Random.MersenneTwister.Config) (seed : BitVec cfg.wordSize := cfg.initSeed) : Batteries.Random.MersenneTwister.State cfg

Mersenne Twister initialization given an optional seed.

Equations

• cfg.init seed = { data := Batteries.Random.MersenneTwister.Config.init.loop cfg seed (Array.mkEmpty cfg.stateSize) ⋯, index := ⟨0, ⋯⟩ }

@[irreducible]

def Batteries.Random.MersenneTwister.Config.init.loop (cfg : Batteries.Random.MersenneTwister.Config) (w : BitVec cfg.wordSize) (v : Array (BitVec cfg.wordSize)) (h : v.size ≤ cfg.stateSize) : Vector (BitVec cfg.wordSize) cfg.stateSize

Inner loop for Mersenne Twister initalization.

Equations

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

@[specialize #[0]]

def Batteries.Random.MersenneTwister.State.twist {cfg : Batteries.Random.MersenneTwister.Config} (state : Batteries.Random.MersenneTwister.State cfg) : Batteries.Random.MersenneTwister.State cfg

Apply the twisting transformation to the given state.

Equations

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

def Batteries.Random.MersenneTwister.State.update {cfg : Batteries.Random.MersenneTwister.Config} (state : Batteries.Random.MersenneTwister.State cfg) (steps : Nat := 1) : Batteries.Random.MersenneTwister.State cfg

Update the state by a number of generation steps (default 1).

Equations

• state.update 0 = state
• state.update steps.succ = state.twist.update steps

@[specialize #[0]]

def Batteries.Random.MersenneTwister.State.next {cfg : Batteries.Random.MersenneTwister.Config} (state : Batteries.Random.MersenneTwister.State cfg) : BitVec cfg.wordSize × Batteries.Random.MersenneTwister.State cfg

Mersenne Twister iteration.

Equations

• state.next = (Batteries.Random.MersenneTwister.State.next.temper state.twist.data[state.index], state.twist)

@[inline]

def Batteries.Random.MersenneTwister.State.next.temper {cfg : Batteries.Random.MersenneTwister.Config} (x : BitVec cfg.wordSize) : BitVec cfg.wordSize

Tempering step for Mersenne Twister.

Equations

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

instance Batteries.Random.MersenneTwister.instStreamStateBitVecWordSize (cfg : Batteries.Random.MersenneTwister.Config) : Stream (Batteries.Random.MersenneTwister.State cfg) (BitVec cfg.wordSize)

Equations

• Batteries.Random.MersenneTwister.instStreamStateBitVecWordSize cfg = { next? := fun (s : Batteries.Random.MersenneTwister.State cfg) => some s.next }

def Batteries.Random.MersenneTwister.mt19937 : Batteries.Random.MersenneTwister.Config

32 bit Mersenne Twister (MT19937) configuration.

Equations

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

def Batteries.Random.MersenneTwister.mt19937_64 : Batteries.Random.MersenneTwister.Config

64 bit Mersenne Twister (MT19937-64) configuration.

Equations

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