Typed graph artifacts

Frontends share the tensor graph schema and its shape checker. Each tensor node also declares dtype; a custom node with primitive = "cast" declares an explicit rounding mode. Constants for binary execution carry complete unsigned words in bits, so parsing never loses precision through JSON floating-point numbers.

An artifact records all runtime inputs in input_ids, in argument order. Each input has its own shape and element type. Typed container lowering still needs explicit container type rules.

def Import.IR.Internal.rounding (value : Lean.Json) : Except String FloatLib.Floats.Formats.BinaryInterchange.Model.IEEERoundingMode

Decode one explicit rounding direction; unknown policies are not silently defaulted.

def Import.IR.Internal.parameter (interpreter : NN.IR.Interpreter) (load : NN.IR.DType → Spec.Shape → Array ℕ → Except String interpreter.Value) (dtype : NN.IR.DType) (shape : Spec.Shape) (name : String) (object : PyTorch.StateDict) : Except String (TorchLean.Tensor (interpreter.Scalar dtype) shape)

Read a parameter at its declared element type through the selected tensor decoder.

def Import.IR.Internal.parse (artifact : Lean.Json) : Except String (PyTorch.TorchExport.Internal.CapturedValueGraph × PyTorch.TorchExport.CapturedGraph × NN.IR.Program)

Parse once so the type assignment and payload use the same raw-to-tensor mapping.

def Import.IR.parseProgram (artifact : Lean.Json) : Except String NN.IR.Program

Import element types and explicit casts using the existing tensor graph lowering.

theorem Import.IR.parseProgram_checked {artifact : Lean.Json} {program : NN.IR.Program} (h : parseProgram artifact = Except.ok program) : program.check = Except.ok ()

The returned program passed the shared checker, including its complete input interface.

theorem Import.IR.parseProgram_wellShaped {artifact : Lean.Json} {program : NN.IR.Program} (h : parseProgram artifact = Except.ok program) : program.graph.WellShaped

Every accepted typed artifact has a well-shaped graph, regardless of its frontend.

def Import.IR.parsePayload (interpreter : NN.IR.Interpreter) (load : NN.IR.DType → Spec.Shape → Array ℕ → Except String interpreter.Value) (artifact : Lean.Json) : Except String interpreter.Payload

Load typed constants and linear parameters using one explicitly selected word decoder.

The decoder's returned type and shape are checked before accepting its tensor. Loading a parameter does not establish that the selected interpreter implements that operation's arithmetic.