Permutation IR Evaluation

Local semantics for axis permutation. The theorem assumes that the shared dynamic interpreter, Graph.permuteSomeTensor, succeeded and returned the declared output shape; it then proves that the complete IR node returns that value. Softmax's axis handling follows its tensor specification directly and is proved separately in Eval.Softmax.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_permute_eq {α : Type} [TorchLean.Storage α] [Context α] {s out : Spec.Shape} (perm : Array ℕ) (x : TorchLean.Tensor α s) (vOut : Spec.SomeTensor α) (hPerm : IR.Graph.permuteSomeTensor { shape := s, tensor := x } perm = Except.ok vOut) (hShape : vOut.shape = out) : (unaryGraphOut (IR.OpKind.permute perm) s out).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := out, tensor := hShape ▸ vOut.tensor }

Local IR semantics for permute, using the shared dynamic-value permutation interpreter.