ONNX Graph Adapter

This module emits a Python-side ONNX adapter for TorchLean graph import.

The adapter does not give ONNX a separate Lean semantics. It reads an ONNX model, lowers the supported static graph fragment to the same torchlean.ir.v1 JSON used by the torch.export/FX bridge, and then the Lean side should call NN.Runtime.PyTorch.Import.TorchExport.parseGraph.

That boundary is intentional: ONNX parsing, protobuf handling, and shape inference stay outside Lean; TorchLean accepts only the small checked graph artifact.

Every "kind" string written by the adapter comes from NN.Runtime.PyTorch.Wire, the table the Lean importer parses with.

structure Export.PyTorch.ONNX.BridgeOptions : Type

Options for the generated ONNX-to-TorchLean-IR adapter script.

• functionName : String

  Name of the Python helper function emitted into the script.

• includeDebugTargets : Bool

  Include ONNX node names/op types in each node for debugging.

@[instance_reducible]

instance Export.PyTorch.ONNX.instReprBridgeOptions : Repr BridgeOptions

def Export.PyTorch.ONNX.instReprBridgeOptions.repr : BridgeOptions → ℕ → Std.Format

Python sections

Each section is an array of Python lines ending in one blank separator line.

def Export.PyTorch.ONNX.imports : Array String

Imports and the artifact format marker.

def Export.PyTorch.ONNX.shapeHelpers : Array String

Static shape collection and attribute readers.

def Export.PyTorch.ONNX.rule (opType : String) (tag : NN.IR.OpTag) : String

One-line _lower_node rule mapping an ONNX op type to a payload-free kind.

def Export.PyTorch.ONNX.nodeLowering : Array String

_lower_node: single-node lowerings keyed on the ONNX op type.

def Export.PyTorch.ONNX.unaryTags : List NN.IR.OpTag

Kinds whose single parent is the first ONNX input.

def Export.PyTorch.ONNX.binaryTags : List NN.IR.OpTag

Kinds that take exactly two ONNX inputs as parents.

def Export.PyTorch.ONNX.parentNames : Array String

_ir_parent_names: select the ONNX inputs that become IR parents for a lowered kind.

def Export.PyTorch.ONNX.convLowering : Array String

_lower_conv: channels-first Conv with explicit padding, optionally unwrapping a batch.

def Export.PyTorch.ONNX.gemmLowering : Array String

_lower_gemm: Gemm as matmul plus an optional broadcast bias add.

def Export.PyTorch.ONNX.broadcastLine (target source fromShape : String) : String

One add_node(<broadcastTo>, ...) call expanding a per-channel tensor to the input shape.

def Export.PyTorch.ONNX.batchNormLowering : Array String

_lower_batchnorm: inference-mode BatchNormalization expanded into elementwise nodes.

def Export.PyTorch.ONNX.entrypoint (options : BridgeOptions) : Array String

The exported entry point: walk the ONNX graph and write the artifact.

def Export.PyTorch.ONNX.mainFunction (options : BridgeOptions) : Array String

Command-line main for the generated script.

def Export.PyTorch.ONNX.generateBridgeScript (options : BridgeOptions := { }) : String

Emit a Python script that lowers a conservative ONNX fragment to torchlean.ir.v1.

Supported first-pass ops are tensor ops that map to current NN.IR.OpKind: elementwise arithmetic/activations, MatMul, ReduceSum, ReduceMean, Softmax, Reshape, Flatten, Concat, Transpose, Gemm, inference-style BatchNormalization, and arbitrary-rank channels-first Conv. Graph initializers become constant nodes. The graph artifact is still separate from the runtime payload store, so this adapter validates graph structure and shapes; executing imported convolution or linear constants still requires a matching payload importer.