API Rand

Deterministic RNG helpers.

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

PyTorch mapping (rough):

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

Convenience wrappers for "PyTorch-like" dimension-first workflows.

uniform / mask are shape-indexed (Tensor α s) and are best used when s is already inferred. When you start from a runtime dims list (e.g. CLI args), uniformND/maskND are the ergonomic bridge.

def NN.API.rand.uniformND {α : Type} [Context α] (key : UInt64) (dims : List ℕ) : Spec.Tensor α (Tensor.shapeOfDims dims)

Dimension-first wrapper: uniform random tensor at runtime dims.

def NN.API.rand.maskND {α : Type} [Context α] (key : UInt64) (keepProb : α) (dims : List ℕ) : Spec.Tensor α (Tensor.shapeOfDims dims)

Dimension-first wrapper: Bernoulli keep-mask at runtime dims (useful for dropout-style masks).

def NN.API.rand.randND {α : Type} [Context α] (seed counter : ℕ) (dims : List ℕ) : Spec.Tensor α (Tensor.shapeOfDims dims)

Deterministic uniform tensor at runtime dims, using (seed,counter) to derive a key.

structure NN.API.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 (ensures each draw is distinct).

def NN.API.rand.instReprSeedStream.repr : SeedStream → ℕ → Std.Format

@[implicit_reducible]

instance NN.API.rand.instReprSeedStream : Repr SeedStream

@[implicit_reducible]

instance NN.API.rand.instDecidableEqSeedStream : DecidableEq SeedStream

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

def NN.API.rand.instInhabitedSeedStream.default : SeedStream

@[implicit_reducible]

instance NN.API.rand.instInhabitedSeedStream : Inhabited SeedStream

@[reducible, inline]

abbrev NN.API.rand.SeedStream.init (seed : ℕ) : SeedStream

Create a fresh stream from a base seed.

def NN.API.rand.SeedStream.next (s : SeedStream) : ℕ × SeedStream

Draw a fresh seed and advance the stream.

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

def NN.API.rand.SeedStream.nextN (n : ℕ) (s : SeedStream) : List ℕ × SeedStream

Draw n fresh seeds.

def NN.API.rand.SeedStream.nextN.go : ℕ → SeedStream → List ℕ → List ℕ × SeedStream

@[reducible, inline]

abbrev NN.API.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.

So we define this seed builder directly (as a pure state monad), and run it in Type 2, which is sufficient for the public API.

@[implicit_reducible]

instance NN.API.rand.SeedM.instMonad : Monad SeedM

opaque NN.API.rand.globalSeedStream : IO.Ref SeedStream

Global seed stream used by rand.runGlobal / nn.runGlobal.

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.run) and pass the base seed explicitly.

def NN.API.rand.manualSeed (seed : ℕ) : IO Unit

Reset the global seed stream.

PyTorch analogue: torch.manual_seed.

def NN.API.rand.runGlobal {α : Type} (x : 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 NN.API.rand.nextSeedGlobal : IO ℕ

Draw one fresh seed from the global seed stream.

def NN.API.rand.nextSeedsGlobal (n : ℕ) : IO (List ℕ)

Draw n fresh seeds from the global seed stream.