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.

structure Export.PyTorch.ONNX.ONNXBridgeOptions : 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.

def Export.PyTorch.ONNX.instReprONNXBridgeOptions.repr : ONNXBridgeOptions → ℕ → Std.Format

@[implicit_reducible]

instance Export.PyTorch.ONNX.instReprONNXBridgeOptions : Repr ONNXBridgeOptions

def Export.PyTorch.ONNX.generateONNXBridgeScript (opts : ONNXBridgeOptions := { }) : 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 CHW/single-batch NCHW 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 Conv/Linear constants still requires a matching payload importer.