Shared Checked-Lowering Context

Common dependent context and result types used by the operation-family lowering modules.

Every lowering branch validates parents and shapes once, while the graph is being lowered, and then builds a pure closure whose result type is the node's declared output shape. The closures apply typed specification operators directly to typed parent values; they never call the dynamic IR evaluator and never unwrap a runtime result, so the lowered graph contains no panic!.

structure Runtime.Autograd.IRExec.Internal.NodeLoweringContext (α : Type) [TorchLean.Storage α] [Context α] (Γ : List Spec.Shape) : Type

Data shared by checked lowerers for one IR node.

• graph : NN.IR.Graph

  The IR graph being lowered.

• payload : NN.IR.Payload α

  External parameters keyed by node id.

• index : ℕ

  Position of the node in the graph.

• node : NN.IR.Node

  The IR node being lowered.

• parentIdx (pid : ℕ) (s : Spec.Shape) : Except String (Proofs.Idx Γ s)

  Build a typed index for a parent id at an expected shape.

@[reducible, inline]

abbrev Runtime.Autograd.IRExec.Internal.NodeLoweringResult {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : Type

The checked executable node produced for a lowering context.