Nodes

Convenience constructors for algebraic tape nodes/graphs.

This is the "approach (a)" authoring layer: you build an SSA/DAG graph out of local nodes, then compile it to a runtime tape via NN/Proofs/Autograd/Runtime/Link.lean.

This file focuses on unary nodes that depend on a single context entry (an Idx). That is enough to build many fixed-parameter inference graphs (e.g. MLP forward + input gradients). Extending to multi-parent nodes (e.g. weight gradients) is intended, but left incremental.

def Proofs.Autograd.Algebra.NodeData.ofOpSpec {α Δ : Type} [Zero α] {Γ : List Spec.Shape} {σ τ : Spec.Shape} (idx : Idx Γ σ) (op : Spec.OpSpec α σ τ) : NodeData α Δ Γ τ

Build an executable unary node from a spec OpSpec, storing the VJP in a sparse TList.

def Proofs.Autograd.Algebra.NodeData.add {α Δ : Type} [Zero α] [Add α] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : NodeData α Δ Γ s

Executable binary add node (two parents of the same shape).

def Proofs.Autograd.Algebra.Node.ofOpSpecCorrect {α Δ : Type} [CommSemiring α] {Γ : List Spec.Shape} {σ τ : Spec.Shape} (idx : Idx Γ σ) (op : OpSpecCorrect α σ τ) : Node Δ Γ τ

Build a proof-carrying unary node from an OpSpecCorrect.

def Proofs.Autograd.Algebra.Node.add {α Δ : Type} [CommSemiring α] {Γ : List Spec.Shape} {s : Spec.Shape} (a b : Idx Γ s) : Node Δ Γ s

Proof-carrying binary add node (two parents of the same shape).

def Proofs.Autograd.Algebra.GraphData.snocOpSpec {α Δ : Type} {Γ : List Spec.Shape} [Zero α] {ss : List Spec.Shape} {σ τ : Spec.Shape} (g : GraphData α Δ Γ ss) (idx : Idx (Γ ++ ss) σ) (op : Spec.OpSpec α σ τ) : GraphData α Δ Γ (ss ++ [τ])

Append a unary node built from an OpSpec (executable-only).

def Proofs.Autograd.Algebra.Graph.snocOpSpecCorrect {α : Type} [CommSemiring α] {Δ : Type} {Γ ss : List Spec.Shape} {σ τ : Spec.Shape} (g : Graph Δ Γ ss) (idx : Idx (Γ ++ ss) σ) (op : OpSpecCorrect α σ τ) : Graph Δ Γ (ss ++ [τ])

Append a unary node built from an OpSpecCorrect (proof-carrying).