Transpose IR Evaluation

Local semantics for swapping any two tensor axes. The graph operation is rank-polymorphic; axis validity and the resulting shape are checked by OpContracts.inferTransposeOutShape.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_transpose_eq {α : Type} [TorchLean.Storage α] [Context α] {inputShape outputShape : Spec.Shape} (axis₁ axis₂ : ℕ) (input : TorchLean.Tensor α inputShape) (perm : Array ℕ) (output : Spec.SomeTensor α) (hPerm : IR.OpContracts.transposePerm inputShape.rank axis₁ axis₂ = Except.ok perm) (hEval : IR.Graph.permuteSomeTensor { shape := inputShape, tensor := input } perm = Except.ok output) (hShape : output.shape = outputShape) : (unaryGraphOut (IR.OpKind.transpose axis₁ axis₂) inputShape outputShape).evalAt { } { shape := inputShape, tensor := input } #[{ shape := inputShape, tensor := input }] 1 = Except.ok { shape := outputShape, tensor := hShape ▸ output.tensor }

Local IR semantics for swapping two arbitrary axes.