CrownParamstore

PyTorch → CROWN ParamStore helpers.

This module is not about JSON parsing; it is about what we do after we have already loaded weights into typed Lean tensors.

Why this exists:

• PyTorch “weights” are keyed by module names (state_dict keys).
• TorchLean’s graph backend stores parameters by node id in NN.MLTheory.CROWN.Graph.ParamStore.

So any real bridge needs a small amount of “wiring code” that:

1. chooses a node-id scheme (model-specific),
2. inserts the corresponding (W,b) tensors into the right slots.

These helpers keep NN.Runtime.PyTorch.Import.Core focused on JSON, and so model example loaders can share the same ParamStore-building utilities.

def Import.CROWNParamStore.insertLinearWB (nodeId : ℕ) (p : NN.MLTheory.CROWN.Graph.LinParams Float) (ps : NN.MLTheory.CROWN.Graph.ParamStore Float) : NN.MLTheory.CROWN.Graph.ParamStore Float

Insert one linear layer's parameters at a given node id.

def Import.CROWNParamStore.ofLinearStack (nodeIdOfIndex : ℕ → ℕ) (layers : List (NN.MLTheory.CROWN.Graph.LinParams Float)) : NN.MLTheory.CROWN.Graph.ParamStore Float

Build a ParamStore Float from a list of linear-layer parameters.

nodeIdOfIndex tells us which graph node id corresponds to the i-th layer in the list. This is the only model-specific decision; the remaining steps are model-agnostic parameter assembly.

def Import.CROWNParamStore.ofLinearStack.go (nodeIdOfIndex : ℕ → ℕ) : List (NN.MLTheory.CROWN.Graph.LinParams Float) → ℕ → NN.MLTheory.CROWN.Graph.ParamStore Float → NN.MLTheory.CROWN.Graph.ParamStore Float

def Import.CROWNParamStore.castLinParams {α : Type} [Context α] (ofFloat : Float → α) (p : NN.MLTheory.CROWN.Graph.LinParams Float) : NN.MLTheory.CROWN.Graph.LinParams α

Cast linear parameters from Float to an arbitrary scalar type.

def Import.CROWNParamStore.ofLinearStackWith {α : Type} [Context α] (ofFloat : Float → α) (nodeIdOfIndex : ℕ → ℕ) (layers : List (NN.MLTheory.CROWN.Graph.LinParams Float)) : NN.MLTheory.CROWN.Graph.ParamStore α

Build a ParamStore α from Float parameters by casting each tensor entry with ofFloat.

def Import.CROWNParamStore.ofLinearStackWith.go {α : Type} [Context α] (nodeIdOfIndex : ℕ → ℕ) : List (NN.MLTheory.CROWN.Graph.LinParams α) → ℕ → NN.MLTheory.CROWN.Graph.ParamStore α → NN.MLTheory.CROWN.Graph.ParamStore α