Graph wire format

NN.IR.OpTag identifies semantic operators. This module assigns each identity its fixed spelling in torchlean.ir.v2: for example, .mulElem is written as "mul_elem". Keeping this table separate from diagnostic names lets us improve an error message while keeping existing graphs readable. Exporters and importers use the same table.

The tag round trip is proved for every constructor. Static attributes are parsed separately; parse? constructs only operations that need none. Tuple projections and supported container nodes belong to the external value graph, not the tensor graph's semantic operator vocabulary.

Pointwise operators are spelled by operator rather than by their shared constructor: "div", "pow", "neg", "rsqrt", "erf", "gelu" and "clamp_min". GELU writes PyTorch's "approximate" string, and a rounded division writes its "rounding_mode"; true division has no such field. The family spelling "pointwise" names the constructor in diagnostics and is not an artifact kind.

def Interop.PyTorch.Wire.format : String

Format marker written to the root format field.

def Interop.PyTorch.Wire.projection : String

Projection of one component out of a tuple-valued FX node.

def Interop.PyTorch.Wire.attention : String

Container-valued nn.MultiheadAttention call kept in the value graph.

def Interop.PyTorch.Wire.tag : NN.IR.OpTag → String

Fixed constructor spelling in the torchlean.ir.v2 artifact.

def Interop.PyTorch.Wire.parseTag? (s : String) : Option NN.IR.OpTag

Parse a constructor spelling into its semantic identity.

def Interop.PyTorch.Wire.parse? (s : String) : Option NN.IR.OpKind

Parse an attribute-free operation; attributed operators need their separate fields.

def Interop.PyTorch.Wire.field (op : NN.IR.OpTag) : String

JSON or Python "kind": "<wire>" field for an operator identity.

def Interop.PyTorch.Wire.object (op : NN.IR.OpTag) : String

JSON or Python object holding only the kind field.

def Interop.PyTorch.Wire.quoted (op : NN.IR.OpTag) : String

The wire string as a quoted JSON or Python literal.

def Interop.PyTorch.Wire.set : List NN.IR.OpTag → String

Python set expression of quoted wire strings. Empty input uses set(), not a dictionary.

def Interop.PyTorch.Wire.pointwiseTag : Spec.PointwiseOp → String

Fixed wire kind of a pointwise operator; its attribute is a separate field.

def Interop.PyTorch.Wire.geluApproximateField : String

Attribute field of gelu: PyTorch's approximate argument.

def Interop.PyTorch.Wire.divRoundingField : String

Attribute field of a rounded div: PyTorch's rounding_mode argument.

def Interop.PyTorch.Wire.pointwiseAttributeField (kind : String) : Option String

Name of the attribute field written with a pointwise kind, if that kind has one.

def Interop.PyTorch.Wire.pointwiseAttribute : Spec.PointwiseOp → Option String

Value of a pointwise operator's attribute field, using PyTorch's strings.

def Interop.PyTorch.Wire.parsePointwise? (kind : String) (value : Option String) : Option Spec.PointwiseOp

Parse a pointwise operator from its kind and the value of its attribute field.

def Interop.PyTorch.Wire.pointwiseObject (op : Spec.PointwiseOp) : String

JSON or Python object holding a pointwise operator's kind and attribute fields.

theorem Interop.PyTorch.Wire.parseTag_pointwiseTag (op : Spec.PointwiseOp) : parseTag? (pointwiseTag op) = none

No pointwise kind collides with an ordinary constructor spelling.

theorem Interop.PyTorch.Wire.parse_pointwise (op : Spec.PointwiseOp) : parsePointwise? (pointwiseTag op) (pointwiseAttribute op) = some op

Every pointwise operator parses back from its kind and attribute: the codec is complete and collision free.

theorem Interop.PyTorch.Wire.parse_op_tag (tag : NN.IR.OpTag) : parseTag? (Wire.tag tag) = some tag

Every tag parses back to its identity: the codec is complete and collision free.

theorem Interop.PyTorch.Wire.parse_op_kind_tag (kind : NN.IR.OpKind) : parseTag? (tag kind.opTag) = some kind.opTag

Serializing and parsing an operation preserves its identity, regardless of its attributes.

theorem Interop.PyTorch.Wire.parse_op_kind (kind : NN.IR.OpKind) (h : kind.opTag.hasAttributes = false) : parse? (tag kind.opTag) = some kind

The attribute-free round trip reconstructs the original operation.