Softmax IR Evaluation

The IR evaluator gives every in-bounds softmax axis the canonical axis-indexed tensor semantics.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_hardMaskedSoftmax_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (scores : TorchLean.Tensor α s) (allowed : TorchLean.Tensor Bool s) : (unaryGraphOut (IR.OpKind.hardMaskedSoftmax (IR.HardMask.ofTensor allowed)) s s).evalAt { } { shape := s, tensor := scores } #[{ shape := s, tensor := scores }] 1 = Except.ok { shape := s, tensor := Spec.hardMaskedSoftmaxSpec scores allowed }

Local IR semantics for stable innermost-axis softmax with a hard Boolean mask.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_softmax_axis_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (axis : ℕ) [Spec.Shape.AxisInBounds axis s] (x : TorchLean.Tensor α s) : (unaryGraphOut (IR.OpKind.softmax axis) s s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := Activation.softmaxSpec axis x }

Local IR semantics for softmax along any in-bounds tensor dimension.