TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Verification.Builtin.Proved.Correctness.Eval.Reductions

Reduction IR Evaluation #

Local semantics for reduction nodes accepted by the shared IR importer.

source
inductive NN.Verification.Builtin.Proved.Correctness.IRStep.AxisReductionOperation :
Type

Axis reductions whose evaluator branches share the same validity and output-shape contract.

Instances For
    source
    def NN.Verification.Builtin.Proved.Correctness.IRStep.AxisReductionOperation.toOpKind (op : AxisReductionOperation) (axis : ℕ) :
    IR.OpKind

    IR opcode for an axis reduction.

    Instances For
      source
      def NN.Verification.Builtin.Proved.Correctness.IRStep.AxisReductionOperation.denote {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (op : AxisReductionOperation) (axis : ℕ) (x : TorchLean.Tensor α s) (hAxis : Spec.Shape.NonemptyAxis axis s) :
      TorchLean.Tensor α (TorchLean.Tensor.shapeAfterSum s axis)

      Typed denotation of an axis reduction.

      Instances For
        source
        theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_axisReduction_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (op : AxisReductionOperation) (axis : ℕ) (x : TorchLean.Tensor α s) (hAxis : PLift (Spec.Shape.NonemptyAxis axis s)) (hAxisLookup : Spec.Shape.nonemptyAxis? axis s = some hAxis) :
        (unaryGraphOut (op.toOpKind axis) s (TorchLean.Tensor.shapeAfterSum s axis)).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := TorchLean.Tensor.shapeAfterSum s axis, tensor := op.denote axis x ⋯ }

        Evaluate either supported axis reduction in its canonical two-node graph.

        source
        theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_reduceSum_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (axis : ℕ) (x : TorchLean.Tensor α s) (hAxis : PLift (Spec.Shape.NonemptyAxis axis s)) (hAxisLookup : Spec.Shape.nonemptyAxis? axis s = some hAxis) :
        (unaryGraphOut (IR.OpKind.reduceSum axis) s (TorchLean.Tensor.shapeAfterSum s axis)).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := TorchLean.Tensor.shapeAfterSum s axis, tensor := TorchLean.Tensor.reduceSum axis x ⋯ }

        Local IR semantics for reduce_sum along a valid axis.

        source
        theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_reduceMean_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (axis : ℕ) (x : TorchLean.Tensor α s) (hAxis : PLift (Spec.Shape.NonemptyAxis axis s)) (hAxisLookup : Spec.Shape.nonemptyAxis? axis s = some hAxis) :
        (unaryGraphOut (IR.OpKind.reduceMean axis) s (TorchLean.Tensor.shapeAfterSum s axis)).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := TorchLean.Tensor.shapeAfterSum s axis, tensor := TorchLean.Tensor.reduceMean axis x ⋯ }

        Local IR semantics for reduce_mean along a valid axis.