8.1. Tensors and Graphs
TorchLean starts with shape-indexed tensors and then offers three ways to describe a computation.
GraphSpec is a typed sequential architecture, GraphSpec.DAG adds sharing, and NN.IR.Graph is
the ordinary op-tagged graph used at runtime boundaries. Keeping those representations distinct
makes the claims attached to each one easier to read.
Definition8.1.1
Context α collects the arithmetic, order, constants, and transcendental operations needed by
scalar-polymorphic model code.
Lean code for Definition8.1.1●1 definition
Associated Lean declarations
-
Context[complete]
Associated Lean declarations
-
Context[complete]
-
classdefined in NN/Spec/Core/Context.leancomplete
class Context (α : Type) : Type
class Context (α : Type) : Type
The full scalar interface required by spec‑level tensors and models.
Extends
-
Inhabited α -
One α -
Zero α -
Add α -
Sub α -
Mul α -
Div α -
Neg α -
Pow α α -
Max α -
Min α -
BEq α -
LT α -
LE α -
MathFunctions α -
Numbers α -
Coe ℕ α
Methods
default : α
Inherited from-
Inhabited
one : α
Inherited from-
One
zero : α
Inherited from-
Zero
add : α → α → α
Inherited from-
Add
sub : α → α → α
Inherited from-
Sub
mul : α → α → α
Inherited from-
Mul
div : α → α → α
Inherited from-
Div
neg : α → α
Inherited from-
Neg
pow : α → α → α
Inherited from-
Pow
max : α → α → α
Inherited from-
Max
min : α → α → α
Inherited from-
Min
beq : α → α → Bool
Inherited from-
BEq
lt : α → α → Prop
Inherited from-
LT
le : α → α → Prop
Inherited from-
LE
exp : α → α
Inherited from-
MathFunctions
tanh : α → α
Inherited from-
MathFunctions
cosh : α → α
Inherited from-
MathFunctions
sqrt : α → α
Inherited from-
MathFunctions
abs : α → α
Inherited from-
MathFunctions
log : α → α
Inherited from-
MathFunctions
pi : α
Inherited from-
MathFunctions
cos : α → α
Inherited from-
MathFunctions
sin : α → α
Inherited from-
MathFunctions
sinh : α → α
Inherited from-
MathFunctions
neg_point_five : α
Backend representation of `-0.5`.
neg_one : α
Backend representation of `-1`.
pointone : α
Backend representation of `0.1`.
pointfive : α
Backend representation of `0.5`.
two : α
Backend representation of `2`.
three : α
Backend representation of `3`.
four : α
Backend representation of `4`.
five : α
Backend representation of `5`.
ten : α
Backend representation of `10`.
log10 : α
Backend representation of the natural logarithm of `10`.
log10000 : α
Backend representation of the natural logarithm of `10000`.
epsilon : α
Backend-supplied tolerance for numerically guarded formulas.
coe : ℕ → α
Inherited from-
Coe
decidable_gt : DecidableRel fun x1 x2 => x1 > x2
Decision procedure for the scalar type's strict order.
-
Definition8.1.2
Spec.Shape indexes Spec.Tensor α s, so the dimensions of a pure tensor are present in its type.
Lean code for Definition8.1.2●1 definition
Associated Lean declarations
-
Spec.Tensor[complete]
Associated Lean declarations
-
Spec.Tensor[complete]
-
inductivedefined in NN/Spec/Core/Tensor/Core.leancomplete
inductive Spec.Tensor (α : Type) : Spec.Shape → Type
inductive Spec.Tensor (α : Type) : Spec.Shape → Type
Shape-indexed tensor datatype for the spec layer. This is a *functional* representation: - a scalar tensor is just an `α`, - an `n`-dimensional tensor is a function `Fin n → Tensor α s`. The spec layer does not commit to a concrete memory layout.
Constructors
Spec.Tensor.scalar {α : Type} : α → Spec.Tensor α Spec.Shape.scalar
Construct a rank-zero tensor from one scalar value.
Spec.Tensor.dim {α : Type} {n : ℕ} {s : Spec.Shape} : (Fin n → Spec.Tensor α s) → Spec.Tensor α (Spec.Shape.dim n s)
Construct an outer dimension from its shape-indexed entries.
Definition8.1.3
A shape is well formed when every dimension in its tree is positive.
Lean code for Definition8.1.3●1 definition
Associated Lean declarations
-
Spec.Shape.wellFormed[complete]
Associated Lean declarations
-
Spec.Shape.wellFormed[complete]
-
defdefined in NN/Spec/Core/Shape.leancomplete
def Spec.Shape.wellFormed : Spec.Shape → Prop
def Spec.Shape.wellFormed : Spec.Shape → Prop
`well_formed s` means "all dimensions of `s` are positive" (recursively).
Definition8.1.4
CanBroadcastTo s₁ s₂ records when values with shape s₁ can be expanded to shape s₂.
Lean code for Definition8.1.4●1 definition
Associated Lean declarations
-
Spec.Shape.CanBroadcastTo[complete]
Associated Lean declarations
-
Spec.Shape.CanBroadcastTo[complete]
-
inductivedefined in NN/Spec/Core/Shape.leancomplete
inductive Spec.Shape.CanBroadcastTo : Spec.Shape → Spec.Shape → Type
inductive Spec.Shape.CanBroadcastTo : Spec.Shape → Spec.Shape → Type
Evidence that shape `s₁` can be broadcast to shape `s₂` (PyTorch-style broadcasting).
Constructors
Spec.Shape.CanBroadcastTo.scalar_to_any (s : Spec.Shape) : Spec.Shape.scalar.CanBroadcastTo s
A scalar can be broadcast to any target shape.
Spec.Shape.CanBroadcastTo.dim_eq {n : ℕ} {s₁ s₂ : Spec.Shape} (tail : s₁.CanBroadcastTo s₂) : (Spec.Shape.dim n s₁).CanBroadcastTo (Spec.Shape.dim n s₂)
Matching outer dimensions preserve broadcasting of their tails.
Spec.Shape.CanBroadcastTo.dim_1_to_n {n : ℕ} {s₁ s₂ : Spec.Shape} (tail : s₁.CanBroadcastTo s₂) : (Spec.Shape.dim 1 s₁).CanBroadcastTo (Spec.Shape.dim n s₂)
An outer dimension of length one can expand to any target length.
Spec.Shape.CanBroadcastTo.expand_dims {n : ℕ} {s₁ s₂ : Spec.Shape} (tail : s₁.CanBroadcastTo s₂) : s₁.CanBroadcastTo (Spec.Shape.dim n s₂)
A new outer target dimension aligns a source of lower rank.
Theorem8.1.5
A well-formed shape has positive total size.
Lean code for Theorem8.1.5●1 theorem
Associated Lean declarations
-
Spec.Shape.size_pos_of_well_formed[complete]
Associated Lean declarations
-
Spec.Shape.size_pos_of_well_formed[complete]
-
theoremdefined in NN/Spec/Core/Shape.leancomplete
theorem Spec.Shape.size_pos_of_well_formed {s : Spec.Shape} : s.wellFormed → 0 < s.size
theorem Spec.Shape.size_pos_of_well_formed {s : Spec.Shape} : s.wellFormed → 0 < s.size
If `s.well_formed`, then `Spec.Shape.size s > 0`.
Proof for Theorem 8.1.5
The proof follows the shape tree and uses positivity of every dimension.
Theorem8.1.6
Rebuilding a flattened shape-indexed tensor at its original shape returns that tensor.
Lean code for Theorem8.1.6●1 theorem
Associated Lean declarations
-
Spec.Tensor.flatten_unflatten_inverse[complete]
Associated Lean declarations
-
Spec.Tensor.flatten_unflatten_inverse[complete]
-
theoremdefined in NN/Spec/Core/TensorReductionShape/ShapeChange.leancomplete
theorem Spec.Tensor.flatten_unflatten_inverse {α : Type} [Inhabited α] {s : Spec.Shape} (t : Spec.Tensor α s) : Spec.Tensor.unflattenSpec s t.flattenSpec = t
theorem Spec.Tensor.flatten_unflatten_inverse {α : Type} [Inhabited α] {s : Spec.Shape} (t : Spec.Tensor α s) : Spec.Tensor.unflattenSpec s t.flattenSpec = t
Round-trip `unflatten ∘ flatten = id`. This is the spec-layer analogue of `reshape`/`view` round-tripping in PyTorch when the element count matches.
Proof for Theorem 8.1.6
Induction on the tensor shape follows the same scalar and dimension structure used by flattening and rebuilding.
Matrix-vector multiplication satisfies the dot-product adjoint identity used by the linear-layer gradient rule for typed tensors over a commutative semiring.
Lean code for Theorem8.1.7●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in NN/Proofs/Tensor/Algebra.leancomplete
theorem Proofs.TensorAlgebra.dot_mat_linear_adjoint {α : Type} [CommSemiring α] {inDim outDim : ℕ} (W : Spec.Tensor α (Spec.Shape.dim outDim (Spec.Shape.dim inDim Spec.Shape.scalar))) (dLdy : Spec.Tensor α (Spec.Shape.dim outDim Spec.Shape.scalar)) (dx : Spec.Tensor α (Spec.Shape.dim inDim Spec.Shape.scalar)) : Proofs.TensorAlgebra.dot dLdy (Spec.matVecMulSpec W dx) = Proofs.TensorAlgebra.dot (Spec.vecMatMulSpec dLdy W) dx
theorem Proofs.TensorAlgebra.dot_mat_linear_adjoint {α : Type} [CommSemiring α] {inDim outDim : ℕ} (W : Spec.Tensor α (Spec.Shape.dim outDim (Spec.Shape.dim inDim Spec.Shape.scalar))) (dLdy : Spec.Tensor α (Spec.Shape.dim outDim Spec.Shape.scalar)) (dx : Spec.Tensor α (Spec.Shape.dim inDim Spec.Shape.scalar)) : Proofs.TensorAlgebra.dot dLdy (Spec.matVecMulSpec W dx) = Proofs.TensorAlgebra.dot (Spec.vecMatMulSpec dLdy W) dx
Adjointness identity for matvec under `dot`. Informally: `⟨dLdy, W dx⟩ = ⟨dLdy W, dx⟩`, i.e. the transpose-adjoint relationship between matrix-vector and vector-matrix multiplication. In PyTorch this corresponds to the familiar identity `(dLdyᵀ @ (W @ dx)) = ((dLdyᵀ @ W) @ dx)`, written with explicit sums.
Proof for Theorem 8.1.7
The proof expands the typed tensor operations into finite sums and rearranges those sums.
Definition8.1.8
A sequential GraphSpec records its parameter shapes, input shape, and output shape in its type.
Graphs are built from identity, primitive, and sequential-composition nodes.
Lean code for Definition8.1.8●1 definition
Associated Lean declarations
-
NN.GraphSpec.Graph[complete]
Associated Lean declarations
-
NN.GraphSpec.Graph[complete]
-
inductivedefined in NN/GraphSpec/Core.leancomplete
inductive NN.GraphSpec.Graph : List NN.Tensor.Shape → NN.Tensor.Shape → NN.Tensor.Shape → Type 2
inductive NN.GraphSpec.Graph : List NN.Tensor.Shape → NN.Tensor.Shape → NN.Tensor.Shape → Type 2
`Graph ps σ τ` is a (restricted) model that: - takes an input tensor of shape `σ`, - produces an output tensor of shape `τ`, - and uses parameters whose shapes are listed in `ps` (in order). This is a *sequential* (chain) graph language: the only composition operator is `seq` (`>>>`). For sharing/skip connections, use `NN.GraphSpec.DAG`. Implementation note: - We encode the parameter list at the type level so composition automatically concatenates parameter lists (`ps := ps₁ ++ ps₂`). - This means every graph has a canonical “ABI” for parameters: a single typed list `TList α ps`. When composing `g₁ : Graph ps₁ σ τ` and `g₂ : Graph ps₂ τ υ`, the composite graph expects parameters of shape list `ps₁ ++ ps₂`, and evaluation splits that list into the pieces needed by each subgraph.
Constructors
NN.GraphSpec.Graph.id (s : NN.Tensor.Shape) : NN.GraphSpec.Graph [] s s
Identity graph: passes the input through unchanged and requires no parameters.
NN.GraphSpec.Graph.seq {ps₁ ps₂ : List NN.Tensor.Shape} {σ τ υ : NN.Tensor.Shape} : NN.GraphSpec.Graph ps₁ σ τ → NN.GraphSpec.Graph ps₂ τ υ → NN.GraphSpec.Graph (ps₁ ++ ps₂) σ υ
Sequential composition. Parameter lists concatenate.
NN.GraphSpec.Graph.prim {ps : List NN.Tensor.Shape} {σ τ : NN.Tensor.Shape} : NN.GraphSpec.Primitive ps σ τ → NN.GraphSpec.Graph ps σ τ
Embed a single primitive node as a graph.
Definition8.1.9
The pure interpreter evaluates a sequential graph on typed parameter and input tensors using scalar-polymorphic operations.
Lean code for Definition8.1.9●1 definition
Associated Lean declarations
-
NN.GraphSpec.Interp.spec[complete]
Associated Lean declarations
-
NN.GraphSpec.Interp.spec[complete]
-
defdefined in NN/GraphSpec/Core.leancomplete
def NN.GraphSpec.Interp.spec {ps : List NN.Tensor.Shape} {σ τ : NN.Tensor.Shape} (g : NN.GraphSpec.Graph ps σ τ) {α : Type} [Context α] : NN.GraphSpec.Interp.Params α ps → Spec.Tensor α σ → Spec.Tensor α τ
def NN.GraphSpec.Interp.spec {ps : List NN.Tensor.Shape} {σ τ : NN.Tensor.Shape} (g : NN.GraphSpec.Graph ps σ τ) {α : Type} [Context α] : NN.GraphSpec.Interp.Params α ps → Spec.Tensor α σ → Spec.Tensor α τ
Pure Spec semantics of a sequential `Graph`.
Definition8.1.10
The runtime translation turns a sequential graph into a backend-polymorphic TorchLean program over the same scalar operations.
Lean code for Definition8.1.10●1 definition
Associated Lean declarations
-
NN.GraphSpec.Compile.torchProgram[complete]
Associated Lean declarations
-
NN.GraphSpec.Compile.torchProgram[complete]
-
defdefined in NN/GraphSpec/Core.leancomplete
def NN.GraphSpec.Compile.torchProgram {ps : List NN.Tensor.Shape} {σ τ : NN.Tensor.Shape} (g : NN.GraphSpec.Graph ps σ τ) {α : Type} [Context α] [DecidableEq NN.Tensor.Shape] : Runtime.Autograd.TorchLean.Program α (ps ++ [σ]) τ
def NN.GraphSpec.Compile.torchProgram {ps : List NN.Tensor.Shape} {σ τ : NN.Tensor.Shape} (g : NN.GraphSpec.Graph ps σ τ) {α : Type} [Context α] [DecidableEq NN.Tensor.Shape] : Runtime.Autograd.TorchLean.Program α (ps ++ [σ]) τ
Compile a sequential `Graph` to a backend-generic TorchLean `Program`.
Definition8.1.11
A typed DAG model pairs initialized parameters with a term whose environment contains the parameter and input shapes. Terms may name arguments and share intermediate results.
Lean code for Definition8.1.11●1 definition
Associated Lean declarations
-
NN.GraphSpec.DAG.Model[complete]
Associated Lean declarations
-
NN.GraphSpec.DAG.Model[complete]
-
structuredefined in NN/GraphSpec/DAG/Core.leancomplete
structure NN.GraphSpec.DAG.Model (ps ins : List NN.Tensor.Shape) (τ : NN.Tensor.Shape) : Type 1
structure NN.GraphSpec.DAG.Model (ps ins : List NN.Tensor.Shape) (τ : NN.Tensor.Shape) : Type 1
A small “model” wrapper around DAG terms. This mirrors the sequential `Graph` surface: - `ps` are parameter tensor shapes (tracked at the type level), - `ins` are the shapes of *non-parameter inputs* (e.g. data tensors), - `τ` is the output shape. The model body is a `Term (ps ++ ins) τ`, i.e. it expects an environment that starts with parameters and then contains the actual inputs.
Fields
initParams : Runtime.Autograd.Torch.TList Float ps
init Params.
body : NN.GraphSpec.DAG.Term (ps ++ ins) τ
body.
Definition8.1.12
The DAG interpreter evaluates the model body from typed parameter and input lists under the scalar context.
Lean code for Definition8.1.12●1 definition
Associated Lean declarations
-
NN.GraphSpec.DAG.Model.specFwd[complete]
Associated Lean declarations
-
NN.GraphSpec.DAG.Model.specFwd[complete]
-
defdefined in NN/GraphSpec/DAG/Core.leancomplete
def NN.GraphSpec.DAG.Model.specFwd {ps ins : List NN.Tensor.Shape} {τ : NN.Tensor.Shape} (m : NN.GraphSpec.DAG.Model ps ins τ) {α : Type} [Context α] (params : Runtime.Autograd.Torch.TList α ps) (xs : Runtime.Autograd.Torch.TList α ins) : Spec.Tensor α τ
def NN.GraphSpec.DAG.Model.specFwd {ps ins : List NN.Tensor.Shape} {τ : NN.Tensor.Shape} (m : NN.GraphSpec.DAG.Model ps ins τ) {α : Type} [Context α] (params : Runtime.Autograd.Torch.TList α ps) (xs : Runtime.Autograd.Torch.TList α ins) : Spec.Tensor α τ
Pure forward semantics of a DAG model. We build the full environment `Γ = ps ++ ins` by appending the parameter list and the input list, then evaluate the body using `Term.eval`.
Definition8.1.13
The DAG compiler turns the same model body into a backend-polymorphic TorchLean program over the same scalar operations.
Lean code for Definition8.1.13●1 definition
Associated Lean declarations
-
NN.GraphSpec.DAG.Model.torchProgram[complete]
Associated Lean declarations
-
NN.GraphSpec.DAG.Model.torchProgram[complete]
-
defdefined in NN/GraphSpec/DAG/Core.leancomplete
def NN.GraphSpec.DAG.Model.torchProgram {ps ins : List NN.Tensor.Shape} {τ : NN.Tensor.Shape} (m : NN.GraphSpec.DAG.Model ps ins τ) {α : Type} [Context α] [DecidableEq NN.Tensor.Shape] : Runtime.Autograd.TorchLean.Program α (ps ++ ins) τ
def NN.GraphSpec.DAG.Model.torchProgram {ps ins : List NN.Tensor.Shape} {τ : NN.Tensor.Shape} (m : NN.GraphSpec.DAG.Model ps ins τ) {α : Type} [Context α] [DecidableEq NN.Tensor.Shape] : Runtime.Autograd.TorchLean.Program α (ps ++ ins) τ
Compile a DAG model to a backend-generic TorchLean program. The resulting program expects arguments in the order `ps ++ ins` (parameters first, then inputs), matching the environment discipline used by `specFwd`.
Definition8.1.14
The sequential GraphSpec MLP composes two linear maps with an intervening ReLU. Its type fixes the order and shapes of both weights and biases.
Lean code for Definition8.1.14●1 definition
Associated Lean declarations
-
NN.GraphSpec.Models.mlp[complete]
Associated Lean declarations
-
NN.GraphSpec.Models.mlp[complete]
-
defdefined in NN/GraphSpec/Models/Mlp.leancomplete
def NN.GraphSpec.Models.mlp (inDim hidDim outDim : ℕ) : NN.GraphSpec.Graph [Spec.Shape.dim hidDim (Spec.Shape.dim inDim Spec.Shape.scalar), Spec.Shape.dim hidDim Spec.Shape.scalar, Spec.Shape.dim outDim (Spec.Shape.dim hidDim Spec.Shape.scalar), Spec.Shape.dim outDim Spec.Shape.scalar] (Spec.Shape.dim inDim Spec.Shape.scalar) (Spec.Shape.dim outDim Spec.Shape.scalar)
def NN.GraphSpec.Models.mlp (inDim hidDim outDim : ℕ) : NN.GraphSpec.Graph [Spec.Shape.dim hidDim (Spec.Shape.dim inDim Spec.Shape.scalar), Spec.Shape.dim hidDim Spec.Shape.scalar, Spec.Shape.dim outDim (Spec.Shape.dim hidDim Spec.Shape.scalar), Spec.Shape.dim outDim Spec.Shape.scalar] (Spec.Shape.dim inDim Spec.Shape.scalar) (Spec.Shape.dim outDim Spec.Shape.scalar)
2-layer MLP: `Linear(in,hid) → ReLU → Linear(hid,out)`. Notice how the parameter interface is explicit in the type: - the first `Linear(in,hid)` contributes `W₁ : Mat hid in` and `b₁ : Vec hid`, - the second `Linear(hid,out)` contributes `W₂ : Mat out hid` and `b₂ : Vec out`, - and `ReLU` contributes no parameters. So the overall parameter list is exactly: `[Mat hid in, Vec hid, Mat out hid, Vec out]`.
Theorem8.1.15
Interpreting the GraphSpec MLP gives the same tensor as the hand-written two-layer MLP specification.
Lean code for Theorem8.1.15●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in NN/GraphSpec/Models/MlpSpecEquivalence.leancomplete
theorem NN.GraphSpec.Models.mlp_interp_eq_spec_mlp_forward {α : Type} [Context α] {inDim hidDim outDim : ℕ} (params : Runtime.Autograd.Torch.TList α (NN.GraphSpec.Models.MLPParams inDim hidDim outDim)) (x : Spec.Tensor α (Spec.Shape.dim inDim Spec.Shape.scalar)) : NN.GraphSpec.Interp.spec (NN.GraphSpec.Models.mlp inDim hidDim outDim) params x = match match params with | Proofs.Autograd.Algebra.TList.cons w1 (Proofs.Autograd.Algebra.TList.cons b1 (Proofs.Autograd.Algebra.TList.cons w2 (Proofs.Autograd.Algebra.TList.cons b2 Proofs.Autograd.Algebra.TList.nil))) => (w1, b1, w2, b2) with | (w1, b1, w2, b2) => have l1 := { weights := w1, bias := b1 }; have l2 := { weights := w2, bias := b2 }; Examples.mlpForward l1 l2 x
theorem NN.GraphSpec.Models.mlp_interp_eq_spec_mlp_forward {α : Type} [Context α] {inDim hidDim outDim : ℕ} (params : Runtime.Autograd.Torch.TList α (NN.GraphSpec.Models.MLPParams inDim hidDim outDim)) (x : Spec.Tensor α (Spec.Shape.dim inDim Spec.Shape.scalar)) : NN.GraphSpec.Interp.spec (NN.GraphSpec.Models.mlp inDim hidDim outDim) params x = match match params with | Proofs.Autograd.Algebra.TList.cons w1 (Proofs.Autograd.Algebra.TList.cons b1 (Proofs.Autograd.Algebra.TList.cons w2 (Proofs.Autograd.Algebra.TList.cons b2 Proofs.Autograd.Algebra.TList.nil))) => (w1, b1, w2, b2) with | (w1, b1, w2, b2) => have l1 := { weights := w1, bias := b1 }; have l2 := { weights := w2, bias := b2 }; Examples.mlpForward l1 l2 x
**Theorem (GraphSpec MLP agrees with Spec reference).** Fix dimensions `inDim → hidDim → outDim`. Let `params` be the 4-tensor parameter list `(W₁, b₁, W₂, b₂)` and `x` an input vector. Then the GraphSpec interpreter applied to the GraphSpec MLP graph computes exactly the same tensor as the reference `Examples.mlp_forward` from `NN.Spec.Models.Mlp`, after interpreting the parameter list as two `LinearSpec`s. Informally, both sides compute the same explicit formula: $$ \begin{aligned} z_1 &= W_1x+b_1,\\ a_1 &= \operatorname{ReLU}(z_1),\\ \mathrm{out} &= W_2a_1+b_2. \end{aligned} $$ where the dot/plus are the `Spec.linear_spec` and `Activation.relu_spec` operations already used by the Spec model.
The proof unpacks the four-tensor parameter list, unfolds the pure interpreter for the MLP, and reduces both sides to the same two linear maps with an intervening ReLU.
Theorem8.1.16
Deterministic initialization for the GraphSpec MLP produces the same typed parameter list, in the same order, as the two TorchLean linear-layer initializers.
Lean code for Theorem8.1.16●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in NN/GraphSpec/Models/MlpDeterministicInit.leancomplete
theorem NN.GraphSpec.Models.mlp_detInitParams_eq_torchlean_linear_inits (inDim hidDim outDim : ℕ) : NN.GraphSpec.LowerToDAG.Graph.detInitParams? (NN.GraphSpec.Models.mlp inDim hidDim outDim) = Except.ok (Proofs.Autograd.Algebra.TList.append (Runtime.Autograd.TorchLean.NN.linear inDim hidDim 0 1).initParams (Runtime.Autograd.TorchLean.NN.linear hidDim outDim 2 3).initParams)
theorem NN.GraphSpec.Models.mlp_detInitParams_eq_torchlean_linear_inits (inDim hidDim outDim : ℕ) : NN.GraphSpec.LowerToDAG.Graph.detInitParams? (NN.GraphSpec.Models.mlp inDim hidDim outDim) = Except.ok (Proofs.Autograd.Algebra.TList.append (Runtime.Autograd.TorchLean.NN.linear inDim hidDim 0 1).initParams (Runtime.Autograd.TorchLean.NN.linear hidDim outDim 2 3).initParams)
Deterministic init for `Models.mlp` is exactly the concatenation of the two TorchLean `Linear` initializers. Seed discipline: - first linear layer uses occurrence index `0`, hence seeds `(0, 1)`, - second linear layer uses occurrence index `1`, hence seeds `(2, 3)`.
Proof for Theorem 8.1.16
For the two-layer graph, the occurrence-indexed seed calculation
reduces to seeds 0, 1 for the first layer and 2, 3 for the second.
Definition8.1.17
The Boolean structural predicate checks that node identifiers match their array positions, operation arities are valid, and every parent points to an earlier node.
Lean code for Definition8.1.17●1 definition
Associated Lean declarations
-
NN.IR.Graph.wellFormed[complete]
Associated Lean declarations
-
NN.IR.Graph.wellFormed[complete]
-
defdefined in NN/IR/Graph.leancomplete
def NN.IR.Graph.wellFormed (g : NN.IR.Graph) : Bool
def NN.IR.Graph.wellFormed (g : NN.IR.Graph) : Bool
Basic well-formedness check used by verifier code paths. This checks: - node ids match array indices (common construction invariant), - each node respects its op arity convention, and - all parent ids are strictly smaller than the node id (topological order). We keep this as a boolean predicate because some passes want a fast “yes/no” filter. If you need a human-facing error, use `checkWellFormed`.
Definition8.1.18
The diagnostic checker enforces the same conditions as the
Boolean structural predicate, but returns the first useful error
message instead of a bare false. The two implementations are kept separate; no equivalence
theorem currently connects them.
Lean code for Definition8.1.18●1 definition
Associated Lean declarations
-
NN.IR.Graph.checkWellFormed[complete]
Associated Lean declarations
-
NN.IR.Graph.checkWellFormed[complete]
-
defdefined in NN/IR/Graph.leancomplete
def NN.IR.Graph.checkWellFormed (g : NN.IR.Graph) : Except String Unit
def NN.IR.Graph.checkWellFormed (g : NN.IR.Graph) : Except String Unit
Like `wellFormed`, but returns a helpful error message on failure. This is useful when you want a *clean* user error rather than a silent `false`.
Definition8.1.19
After the structural check, shape validation infers every node's output shape and compares it with the shape stored in the graph.
Lean code for Definition8.1.19●1 definition
Associated Lean declarations
-
NN.IR.Graph.checkShapes[complete]
Associated Lean declarations
-
NN.IR.Graph.checkShapes[complete]
-
defdefined in NN/IR/Infer.leancomplete
def NN.IR.Graph.checkShapes (g : NN.IR.Graph) : Except String Unit
def NN.IR.Graph.checkShapes (g : NN.IR.Graph) : Except String Unit
Infer shapes for every node (in topo/id order) and check that `Node.outShape` matches. This is meant as a compiler/back-end consistency check and as a clean IR invariant for the docs: well-formed graphs have *self-consistent declared shapes*.
Definition8.1.20
After the structural check, IR denotation evaluates every node into a table of shape-tagged tensor values using scalar-polymorphic operations and the supplied external payload.
Lean code for Definition8.1.20●1 definition
Associated Lean declarations
-
NN.IR.Graph.denoteAll[complete]
Associated Lean declarations
-
NN.IR.Graph.denoteAll[complete]
-
defdefined in NN/IR/Semantics.leancomplete
def NN.IR.Graph.denoteAll {α : Type} [Context α] [DecidableEq Spec.Shape] (g : NN.IR.Graph) (payload : NN.IR.Payload α) (input : NN.IR.DVal α) : Except String (Array (NN.IR.DVal α))
def NN.IR.Graph.denoteAll {α : Type} [Context α] [DecidableEq Spec.Shape] (g : NN.IR.Graph) (payload : NN.IR.Payload α) (input : NN.IR.DVal α) : Except String (Array (NN.IR.DVal α))
Evaluate a graph to a table of node values. This returns an array `vals` of length `g.size` where `vals[i]` is the value of node `i`. We do a structural well-formedness check once up front (ids/arity/topology). For compiler-produced graphs, the boolean `Graph.wellFormed` check is a fast path; if it fails we fall back to the exception-producing `Graph.checkWellFormed` so callers get a readable error message. The evaluator is total in the sense that it always returns either: - `.ok vals` (all nodes evaluated successfully), or - `.error msg` describing the first failure (malformed IR, missing payload, or a local shape error).