Concat IR Evaluation

Local semantics for IR concat. The evaluator keeps the generic-axis implementation in the shared Graph.evalConcat helper, which moves the requested axis to the front, folds Tensor.concatAxisSpec, and moves the result back. LeadingAxisConcat.Input packages an input with its leading dimension, LeadingAxisConcat.fold specifies nonempty list concatenation, and evalAt_concat_leadingAxis_eq proves end-to-end graph evaluation correct for every arity of at least two.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_concat_binary_eq {α : Type} [TorchLean.Storage α] [Context α] {s₁ s₂ out : Spec.Shape} (axis : ℕ) (lhs : TorchLean.Tensor α s₁) (rhs : TorchLean.Tensor α s₂) : (binaryGraphOut (IR.OpKind.concat axis) s₁ s₂ out).evalAt { } { shape := s₁, tensor := lhs } #[{ shape := s₁, tensor := lhs }, { shape := s₂, tensor := rhs }] 2 = (IR.Graph.evalConcat 2 (binaryNodeOut (IR.OpKind.concat axis) out) axis #[{ shape := s₁, tensor := lhs }, { shape := s₂, tensor := rhs }]).bind (IR.Graph.normalizeNodeOutput 2 (binaryNodeOut (IR.OpKind.concat axis) out))

Local IR semantics for binary concat, pinned to the shared generic concat interpreter.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_concat_binary_ok {α : Type} [TorchLean.Storage α] [Context α] {s₁ s₂ out : Spec.Shape} (axis : ℕ) (lhs : TorchLean.Tensor α s₁) (rhs : TorchLean.Tensor α s₂) (y : TorchLean.Tensor α out) (hConcat : IR.Graph.evalConcat 2 (binaryNodeOut (IR.OpKind.concat axis) out) axis #[{ shape := s₁, tensor := lhs }, { shape := s₂, tensor := rhs }] = Except.ok { shape := out, tensor := y }) : (binaryGraphOut (IR.OpKind.concat axis) s₁ s₂ out).evalAt { } { shape := s₁, tensor := lhs } #[{ shape := s₁, tensor := lhs }, { shape := s₂, tensor := rhs }] 2 = Except.ok { shape := out, tensor := y }

Successful binary concat evaluation, once the shared concat interpreter has produced a value with the node's declared output shape.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_concat_binary_error {α : Type} [TorchLean.Storage α] [Context α] {s₁ s₂ out : Spec.Shape} (axis : ℕ) (lhs : TorchLean.Tensor α s₁) (rhs : TorchLean.Tensor α s₂) (msg : String) (hConcat : IR.Graph.evalConcat 2 (binaryNodeOut (IR.OpKind.concat axis) out) axis #[{ shape := s₁, tensor := lhs }, { shape := s₂, tensor := rhs }] = Except.error msg) : (binaryGraphOut (IR.OpKind.concat axis) s₁ s₂ out).evalAt { } { shape := s₁, tensor := lhs } #[{ shape := s₁, tensor := lhs }, { shape := s₂, tensor := rhs }] 2 = Except.error msg

Binary concat evaluation rejects the node whenever the shared concat interpreter rejects it.

def NN.Verification.Builtin.Proved.Correctness.IRStep.LeadingAxisConcat.shapes (rest : Spec.Shape) (sizes : List ℕ) : List Spec.Shape

Shapes with a common tail and the supplied leading dimensions.

def NN.Verification.Builtin.Proved.Correctness.IRStep.LeadingAxisConcat.totalSize (head : ℕ) (tail : List ℕ) : ℕ

Sum a nonempty sequence of leading dimensions from left to right.

@[reducible, inline]

abbrev NN.Verification.Builtin.Proved.Correctness.IRStep.LeadingAxisConcat.Input (α : Type) [TorchLean.Storage α] [Context α] (rest : Spec.Shape) : Type

A tensor whose leading dimension is existentially quantified while its tail shape stays fixed.

def NN.Verification.Builtin.Proved.Correctness.IRStep.LeadingAxisConcat.Input.toSomeTensor {α : Type} [TorchLean.Storage α] [Context α] {rest : Spec.Shape} (input : Input α rest) : Spec.SomeTensor α

Erase the leading-axis witness to the dynamic value consumed by the IR evaluator.

def NN.Verification.Builtin.Proved.Correctness.IRStep.LeadingAxisConcat.fold {α : Type} [TorchLean.Storage α] [Context α] {rest : Spec.Shape} (head : Input α rest) (tail : List (Input α rest)) : Input α rest

Concatenate a nonempty sequence of compatible leading-axis inputs from left to right.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.LeadingAxisConcat.fold_size {α : Type} [TorchLean.Storage α] [Context α] {rest : Spec.Shape} (head : Input α rest) (tail : List (Input α rest)) : (fold head tail).fst = List.foldl (fun (x1 x2 : ℕ) => x1 + x2) head.fst (List.map Sigma.fst tail)

The leading dimension of a concat fold is the left-associated sum of its input dimensions.

@[simp]

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.expectLeadingAxisInput_toSomeTensor {α : Type} [TorchLean.Storage α] [Context α] {rest : Spec.Shape} (i : ℕ) (input : LeadingAxisConcat.Input α rest) : IR.Graph.expectLeadingAxisInput i rest input.toSomeTensor = Except.ok input

Packaging and then decoding a typed leading-axis input preserves it exactly.

@[simp]

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.mapM_expectLeadingAxisInput_toSomeTensor {α : Type} [TorchLean.Storage α] [Context α] {rest : Spec.Shape} (i : ℕ) (inputs : List (LeadingAxisConcat.Input α rest)) : List.mapM (IR.Graph.expectLeadingAxisInput i rest) (List.map LeadingAxisConcat.Input.toSomeTensor inputs) = Except.ok inputs

Decoding a list of typed leading-axis inputs after packaging preserves the whole list.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalConcatLeadingAxisFold_eq {α : Type} [TorchLean.Storage α] [Context α] {rest : Spec.Shape} (i : ℕ) (head : LeadingAxisConcat.Input α rest) (tail : List (LeadingAxisConcat.Input α rest)) : have result := LeadingAxisConcat.fold head tail; IR.Graph.evalConcatLeadingAxisFold i result.fst rest (List.map LeadingAxisConcat.Input.toSomeTensor (head :: tail)).toArray = Except.ok result.toSomeTensor

The dynamic leading-axis evaluator agrees with the typed concat fold for every nonempty input list. This single list-indexed result subsumes the former pair, triple, and quadruple theorems.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.inferConcatOutShape_leadingAxis_eq {rest : Spec.Shape} (first second : ℕ) (tail : List ℕ) : IR.OpContracts.inferConcatOutShape 0 (LeadingAxisConcat.shapes rest (first :: second :: tail)).toArray = Except.ok (Spec.Shape.dim (LeadingAxisConcat.totalSize first (second :: tail)) rest)

Leading-axis shape inference sums every input's leading dimension for any arity of at least two.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalConcat_leadingAxis_eq {α : Type} [TorchLean.Storage α] [Context α] {rest : Spec.Shape} (i : ℕ) (first second : LeadingAxisConcat.Input α rest) (tail : List (LeadingAxisConcat.Input α rest)) : have inputs := first :: second :: tail; have result := LeadingAxisConcat.fold first (second :: tail); have parentShapes := (List.map (fun (input : LeadingAxisConcat.Input α rest) => Spec.Shape.dim input.fst rest) inputs).toArray; IR.Graph.evalConcat i (variadicNodeOut (IR.OpKind.concat 0) parentShapes (Spec.Shape.dim result.fst rest)) 0 (List.map LeadingAxisConcat.Input.toSomeTensor inputs).toArray = Except.ok result.toSomeTensor

The shared concat interpreter agrees with the typed fold for every arity of at least two.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_concat_leadingAxis_eq {α : Type} [TorchLean.Storage α] [Context α] {rest : Spec.Shape} (first second : LeadingAxisConcat.Input α rest) (tail : List (LeadingAxisConcat.Input α rest)) : have inputs := first :: second :: tail; have result := LeadingAxisConcat.fold first (second :: tail); have parentShapes := (List.map (fun (input : LeadingAxisConcat.Input α rest) => Spec.Shape.dim input.fst rest) inputs).toArray; have values := (List.map LeadingAxisConcat.Input.toSomeTensor inputs).toArray; (variadicGraphOut (IR.OpKind.concat 0) parentShapes (Spec.Shape.dim result.fst rest)).evalAt { } first.toSomeTensor values parentShapes.size = Except.ok result.toSomeTensor

End-to-end local IR semantics for leading-axis concat with any number of inputs greater than one. The graph, parent values, inferred output dimension, and tensor result are all derived from the same shape-erased input list.