TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Runtime.Autograd.IRExec.Lowering.Basic

Basic and Random IR Lowering #

Checked lowering for graph inputs, constants, detachment, and random operations.

Each operation has its own small lower* definition. lowerBasic only dispatches on the operation kind, and the lowerBasic_* equation lemmas let correctness proofs reduce a dispatch to the branch they care about without unfolding the whole dispatcher.

source
def Runtime.Autograd.IRExec.Internal.lowerInput {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) :
NodeLoweringResult ctx

A second .input node cannot appear after node 0; the lowering loop rejects it.

Instances For
    source
    def Runtime.Autograd.IRExec.Internal.lowerConst {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (s : Spec.Shape) :
    NodeLoweringResult ctx

    Checked lowering for .const s: read the payload tensor and retag it at the declared shape.

    Instances For
      source
      def Runtime.Autograd.IRExec.Internal.lowerDetach {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) :
      NodeLoweringResult ctx

      Checked lowering for .detach, including scalar tangent removal for dual-valued execution.

      Instances For
        source
        def Runtime.Autograd.IRExec.Internal.lowerRandUniform {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (seed : ℕ) :
        NodeLoweringResult ctx

        Checked lowering for .randUniform seed: a deterministic tensor keyed by seed and node id.

        Instances For
          source
          def Runtime.Autograd.IRExec.Internal.lowerBernoulliMask {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (seed : ℕ) :
          NodeLoweringResult ctx

          Checked lowering for .bernoulliMask seed: a keyed mask with a scalar keep probability.

          Instances For
            source
            def Runtime.Autograd.IRExec.Internal.lowerBasic {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (kind : NN.IR.OpKind) :
            NodeLoweringResult ctx

            Checked lowering for graph inputs, constants, detachment, and random operations.

            Instances For
              source
              @[simp]
              theorem Runtime.Autograd.IRExec.Internal.lowerBasic_input {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) :
              lowerBasic ctx NN.IR.OpKind.input = lowerInput ctx

              Dispatch equation for .input.

              source
              @[simp]
              theorem Runtime.Autograd.IRExec.Internal.lowerBasic_const {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (s : Spec.Shape) :
              lowerBasic ctx (NN.IR.OpKind.const s) = lowerConst ctx s

              Dispatch equation for .const s.

              source
              @[simp]
              theorem Runtime.Autograd.IRExec.Internal.lowerBasic_detach {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) :
              lowerBasic ctx NN.IR.OpKind.detach = lowerDetach ctx

              Dispatch equation for .detach.

              source
              @[simp]
              theorem Runtime.Autograd.IRExec.Internal.lowerBasic_randUniform {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (seed : ℕ) :
              lowerBasic ctx (NN.IR.OpKind.randUniform seed) = lowerRandUniform ctx seed

              Dispatch equation for .randUniform seed.

              source
              @[simp]
              theorem Runtime.Autograd.IRExec.Internal.lowerBasic_bernoulliMask {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (seed : ℕ) :
              lowerBasic ctx (NN.IR.OpKind.bernoulliMask seed) = lowerBernoulliMask ctx seed

              Dispatch equation for .bernoulliMask seed.