Typed interchange programs

Program attaches element types and an input/output interface to the existing Graph. Shapes and dependencies remain in that graph; there is no second node language. Ordinary operators have homogeneous signatures, so a frontend must make its promotions explicit. Casts and registered heterogeneous primitives use the existing custom-node shape contract and a separate element-type signature.

The custom node's name is for display. Its typed primitive entry, indexed by node id, determines its meaning. An unregistered custom operation is rejected rather than inferred from a spelling. Interpreters must supply the implementation of every primitive they execute.

Type checking establishes consistency of the declared program, not equivalence with a frontend or correctness of an external numerical backend.

inductive NN.IR.Primitive : Type

Typed extension of a custom node; shape contracts remain in OpKind.custom.

• cast (rounding : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode := FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) : Primitive

  Convert one tensor to the node's result type, with an explicit rounding direction.

• call (name : Lean.Name) (inputs : Array DType) (output : DType) : Primitive

  A registered operation with an explicit, possibly heterogeneous element-type signature.

def NN.IR.instDecidableEqPrimitive.decEq (x✝ x✝¹ : Primitive) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance NN.IR.instDecidableEqPrimitive : DecidableEq Primitive

@[instance_reducible]

instance NN.IR.instReprPrimitive : Repr Primitive

def NN.IR.instReprPrimitive.repr : Primitive → ℕ → Std.Format

structure NN.IR.Program : Type

One canonical graph together with its SSA type assignment and external interface.

• graph : Graph

  Shared graph syntax, including all operation shape attributes.

• dtypes : Array DType

  Element type of every node result, indexed by node id.

• inputs : Array ℕ

  All runtime input nodes, in argument order.

• outputs : Array ℕ

  Designated result nodes, in return order.

• primitives : Array (Option Primitive)

  Typed bodies for custom nodes. Empty means no registrations; otherwise aligned with nodes.

def NN.IR.instReprProgram.repr : Program → ℕ → Std.Format

@[instance_reducible]

instance NN.IR.instReprProgram : Repr Program

def NN.IR.Program.dtype (program : Program) (id : ℕ) : Except String DType

Recover a result's declared element type, reporting an invalid SSA index.

def NN.IR.Program.primitive? (program : Program) (id : ℕ) : Option Primitive

Typed primitive attached to a node. An empty table represents no registrations.

def NN.IR.Program.checkNodeTypes (program : Program) (node : Node) : Except String Unit

Check one node's element-type rule; graph validation separately checks shape and arity.

def NN.IR.Program.check (program : Program) : Except String Unit

Check ids, shapes, element types, primitive signatures, and the input/output interface.

theorem NN.IR.Program.check_wellShaped {program : Program} (h : program.check = Except.ok ()) : program.graph.WellShaped

Passing the typed checker supplies the shape hypothesis used by graph semantics.

def NN.IR.Program.ofGraph (graph : Graph) (outputs : Array ℕ) : Program

Embed a scalar-polymorphic graph without changing its operations or dependencies.

def NN.IR.Program.cast (program : Program) (input : ℕ) (target : DType) (rounding : FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode := FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) : Except String (Program × ℕ)

Append a shape-preserving cast to a typed program and return its result id.

The target type is the result's entry in the typing context; the rounding direction is the primitive's explicit attribute. Existing custom-node shape checks remain applicable.