Elementwise and Activation IR Lowering

Checked lowering for pointwise arithmetic, unary functions, and activation operations.

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

The .log closure applies Tensor.logSpec to every input. The IR evaluator additionally rejects nonpositive inputs, so the end-to-end semantic equivalence theorem carries the NoRawLog side condition; the lowered closure itself is total and never panics.

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

Checked lowering for .add.

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

Checked lowering for .sub.

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

Checked lowering for .mulElem.

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

Checked lowering for .abs.

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

Checked lowering for .sqrt.

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

Checked lowering for .inv.

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

Checked lowering for .maxElem.

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

Checked lowering for .minElem.

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

Checked lowering for .relu.

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

Checked lowering for .tanh.

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

Checked lowering for .sigmoid.

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

Lower stable softplus through the scalar specification.

Retaining its sign branch preserves both the finite positive tail and the selected computation at zero when the scalar carries first or higher derivatives.

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

Checked lowering for .safeLog.

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

Checked lowering for .exp.

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

Checked lowering for .log.

The closure is total: it applies Tensor.logSpec to the parent value. The IR evaluator rejects nonpositive inputs at runtime, which is why the end-to-end equivalence theorem excludes raw .log through NoRawLog. A positive-input construction can avoid the domain failure, but its .log node remains outside that syntactic theorem and requires a separate domain-aware argument.

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

Checked lowering for .sin.

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

Checked lowering for .cos.

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

Checked lowering for .softmax axis.

def Runtime.Autograd.IRExec.Internal.lowerHardMaskedSoftmax {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (mask : NN.IR.HardMask) : NodeLoweringResult ctx

Checked lowering for .hardMaskedSoftmax mask.

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

Checked lowering for pointwise arithmetic, unary functions, and activation operations.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_add {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.add = lowerAdd ctx

Dispatch equation for .add.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_sub {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.sub = lowerSub ctx

Dispatch equation for .sub.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_mulElem {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.mulElem = lowerMulElem ctx

Dispatch equation for .mulElem.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_abs {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.abs = lowerAbs ctx

Dispatch equation for .abs.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_sqrt {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.sqrt = lowerSqrt ctx

Dispatch equation for .sqrt.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_inv {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.inv = lowerInv ctx

Dispatch equation for .inv.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_maxElem {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.maxElem = lowerMaxElem ctx

Dispatch equation for .maxElem.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_minElem {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.minElem = lowerMinElem ctx

Dispatch equation for .minElem.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_relu {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.relu = lowerRelu ctx

Dispatch equation for .relu.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_tanh {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.tanh = lowerTanh ctx

Dispatch equation for .tanh.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_sigmoid {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.sigmoid = lowerSigmoid ctx

Dispatch equation for .sigmoid.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_softplus {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.softplus = lowerSoftplus ctx

Dispatch equation for .softplus.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_safeLog {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.safeLog = lowerSafeLog ctx

Dispatch equation for .safeLog.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_exp {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.exp = lowerExp ctx

Dispatch equation for .exp.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_log {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.log = lowerLog ctx

Dispatch equation for .log.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_sin {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.sin = lowerSin ctx

Dispatch equation for .sin.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_cos {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerElementwise ctx NN.IR.OpKind.cos = lowerCos ctx

Dispatch equation for .cos.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_softmax {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (axis : ℕ) : lowerElementwise ctx (NN.IR.OpKind.softmax axis) = lowerSoftmax ctx axis

Dispatch equation for .softmax axis.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerElementwise_hardMaskedSoftmax {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (mask : NN.IR.HardMask) : lowerElementwise ctx (NN.IR.OpKind.hardMaskedSoftmax mask) = lowerHardMaskedSoftmax ctx mask

Dispatch equation for .hardMaskedSoftmax mask.