Random Seeds

Deterministic RNG helpers.

TorchLean treats randomness explicitly (via seeds/keys) so examples are reproducible.

PyTorch mapping:

• torch.Generator and seed management
• torch.rand / Bernoulli masks for dropout

structure TorchLean.rand.SeedStream : Type

Deterministic seed stream (seed + monotone counter).

This is intended for model construction (parameter init keys, dropout keys, etc.) where you want PyTorch-like ergonomics but reproducible results.

• seed : ℕ

  Base seed (think torch.manual_seed).

• counter : ℕ

  Monotone counter mixed with the base seed for each draw.

@[instance_reducible]

instance TorchLean.rand.instReprSeedStream : Repr SeedStream

def TorchLean.rand.instReprSeedStream.repr : SeedStream → ℕ → Std.Format

def TorchLean.rand.instDecidableEqSeedStream.decEq (x✝ x✝¹ : SeedStream) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance TorchLean.rand.instDecidableEqSeedStream : DecidableEq SeedStream

@[instance_reducible]

instance TorchLean.rand.instInhabitedSeedStream : Inhabited SeedStream

@[reducible, inline]

abbrev TorchLean.rand.SeedStream.init (seed : ℕ) : SeedStream

Create a fresh stream from a base seed.

def TorchLean.rand.SeedStream.next (stream : SeedStream) : ℕ × SeedStream

Draw a fresh seed and advance the stream.

Implementation: we reuse Spec.Random.nextSeed as a small deterministic mixing function.

@[reducible, inline]

abbrev TorchLean.rand.SeedM (α : Type u) : Type u

State monad for deterministic seed allocation.

Lean's StateT/StateM ties the state/result universes together, while TorchLean model definitions (e.g. nn.Sequential) live above Type 0.

This pure state-function representation preserves the result universe, including the higher universe used by model definitions.

@[instance_reducible]

instance TorchLean.rand.SeedM.instMonad : Monad SeedM

opaque TorchLean.rand.globalSeedStream : IO.Ref SeedStream

Global seed stream used by rand.runGlobal and nn.withModel.

This is a convenience for script-like code that wants PyTorch-style "set the seed once" ergonomics. In proofs and reproducibility-sensitive code, prefer the pure interfaces (nn.build) and pass the base seed explicitly.

def TorchLean.rand.manualSeed (seed : ℕ) : IO Unit

Reset the global seed stream.

PyTorch analogue: torch.manual_seed.

def TorchLean.rand.runGlobal {α : Type} (computation : SeedM α) : IO α

Run a seeded builder using the global seed stream and advance it.

This lets you build multiple models/layers in IO without explicitly threading seeds, while still remaining deterministic.

def TorchLean.rand.nextSeedGlobal : IO ℕ

Draw one fresh seed from the global seed stream.