Permutation IR Evaluation

Local semantics for axis permutation. The theorem is stated against Graph.permuteSomeTensor, the shared permutation interpreter used by permute, non-last-axis softmax, and axis-generic concat.

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.