Elementwise IR Evaluation

These lemmas cover the common elementwise operators emitted by the PyTorch and ONNX bridges. Each statement is local to one IR node: if the parent values are already present in the evaluator table, Graph.evalAt returns the corresponding spec tensor operation.

inductive NN.Verification.Builtin.Proved.Correctness.IRStep.BinaryElementwiseOp : Type

Same-shape binary elementwise operations supported by the local evaluator theorem.

• add : BinaryElementwiseOp

  Elementwise addition.

• sub : BinaryElementwiseOp

  Elementwise subtraction.

• mul : BinaryElementwiseOp

  Elementwise multiplication.

• max : BinaryElementwiseOp

  Elementwise maximum.

• min : BinaryElementwiseOp

  Elementwise minimum.

def NN.Verification.Builtin.Proved.Correctness.IRStep.BinaryElementwiseOp.toOpKind : BinaryElementwiseOp → IR.OpKind

Translate a binary elementwise operation to its IR opcode.

def NN.Verification.Builtin.Proved.Correctness.IRStep.BinaryElementwiseOp.denote {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (op : BinaryElementwiseOp) (a b : TorchLean.Tensor α s) : TorchLean.Tensor α s

Denotation of a same-shape binary elementwise operation.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_binaryElementwise_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (op : BinaryElementwiseOp) (a b : TorchLean.Tensor α s) : (binaryGraph op.toOpKind s).evalAt { } { shape := s, tensor := a } #[{ shape := s, tensor := a }, { shape := s, tensor := b }] 2 = Except.ok { shape := s, tensor := op.denote a b }

Evaluate any supported same-shape binary elementwise node.

inductive NN.Verification.Builtin.Proved.Correctness.IRStep.UnaryElementwiseOp : Type

Same-shape unary elementwise operations without additional runtime side conditions.

• abs : UnaryElementwiseOp

  Elementwise absolute value.

• sqrt : UnaryElementwiseOp

  Elementwise square root.

• inv : UnaryElementwiseOp

  Elementwise reciprocal.

• relu : UnaryElementwiseOp

  Rectified linear unit.

• tanh : UnaryElementwiseOp

  Hyperbolic tangent.

• sigmoid : UnaryElementwiseOp

  Logistic sigmoid.

• softplus : UnaryElementwiseOp

  Stable softplus.

• exp : UnaryElementwiseOp

  Elementwise exponential.

• sin : UnaryElementwiseOp

  Elementwise sine.

• cos : UnaryElementwiseOp

  Elementwise cosine.

def NN.Verification.Builtin.Proved.Correctness.IRStep.UnaryElementwiseOp.toOpKind : UnaryElementwiseOp → IR.OpKind

Translate a unary elementwise operation to its IR opcode.

def NN.Verification.Builtin.Proved.Correctness.IRStep.UnaryElementwiseOp.denote {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (op : UnaryElementwiseOp) (x : TorchLean.Tensor α s) : TorchLean.Tensor α s

Denotation of a same-shape unary elementwise operation.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_unaryElementwise_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (op : UnaryElementwiseOp) (x : TorchLean.Tensor α s) : (unaryGraph op.toOpKind s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := op.denote x }

Evaluate any supported same-shape unary elementwise node.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_binaryElementwise_of_getNode {α : Type} [TorchLean.Storage α] [Context α] {inShape s : Spec.Shape} {ss : List Spec.Shape} (op : BinaryElementwiseOp) (a b : Idx (Ctx inShape ss) s) (g : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (i : ℕ) (n : IR.Node) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : g.getNode i = pure n) (hKind : n.kind = op.toOpKind) (hParents : n.parents = #[a.id, b.id]) (hOut : n.outShape = s) : g.evalAt payload input vals i = do let ta ← getVal vals a let tb ← getVal vals b pure { shape := s, tensor := op.denote ta tb }

Evaluate a binary elementwise node in an arbitrary graph from the lowering pass's shape invariant.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_unaryElementwise_of_getNode {α : Type} [TorchLean.Storage α] [Context α] {inShape s : Spec.Shape} {ss : List Spec.Shape} (op : UnaryElementwiseOp) (x : Idx (Ctx inShape ss) s) (g : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (i : ℕ) (n : IR.Node) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : g.getNode i = pure n) (hKind : n.kind = op.toOpKind) (hParents : n.parents = #[x.id]) (hOut : n.outShape = s) : g.evalAt payload input vals i = do let tx ← getVal vals x pure { shape := s, tensor := op.denote tx }

Evaluate a unary elementwise node in an arbitrary graph from the lowering pass's shape invariant.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_add_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (a b : TorchLean.Tensor α s) : (binaryGraph IR.OpKind.add s).evalAt { } { shape := s, tensor := a } #[{ shape := s, tensor := a }, { shape := s, tensor := b }] 2 = Except.ok { shape := s, tensor := a.addSpec b }

Local IR semantics for elementwise addition.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_sub_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (a b : TorchLean.Tensor α s) : (binaryGraph IR.OpKind.sub s).evalAt { } { shape := s, tensor := a } #[{ shape := s, tensor := a }, { shape := s, tensor := b }] 2 = Except.ok { shape := s, tensor := a.subSpec b }

Local IR semantics for elementwise subtraction.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_mulElem_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (a b : TorchLean.Tensor α s) : (binaryGraph IR.OpKind.mulElem s).evalAt { } { shape := s, tensor := a } #[{ shape := s, tensor := a }, { shape := s, tensor := b }] 2 = Except.ok { shape := s, tensor := a.mulSpec b }

Local IR semantics for elementwise multiplication.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_maxElem_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (a b : TorchLean.Tensor α s) : (binaryGraph IR.OpKind.maxElem s).evalAt { } { shape := s, tensor := a } #[{ shape := s, tensor := a }, { shape := s, tensor := b }] 2 = Except.ok { shape := s, tensor := a.maxSpec b }

Local IR semantics for elementwise maximum.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_minElem_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (a b : TorchLean.Tensor α s) : (binaryGraph IR.OpKind.minElem s).evalAt { } { shape := s, tensor := a } #[{ shape := s, tensor := a }, { shape := s, tensor := b }] 2 = Except.ok { shape := s, tensor := a.minSpec b }

Local IR semantics for elementwise minimum.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_abs_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.abs s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := x.absSpec }

Local IR semantics for elementwise absolute value.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_sqrt_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.sqrt s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := x.sqrtSpec }

Local IR semantics for elementwise square root.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_inv_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.inv s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := x.invSpec }

Local IR semantics for elementwise reciprocal.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_relu_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.relu s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := Activation.reluSpec x }

Local IR semantics for ReLU.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_tanh_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.tanh s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := Activation.tanhSpec x }

Local IR semantics for tanh.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_sigmoid_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.sigmoid s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := Activation.sigmoidSpec x }

Local IR semantics for sigmoid.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_softplus_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.softplus s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := Activation.softplusSpec x }

Local IR semantics for softplus.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalNode_safeLog_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) (epsilon : α) : IR.Graph.evalNode { } { shape := s, tensor := x } #[{ shape := s, tensor := x }, { shape := Spec.Shape.scalar, tensor := TorchLean.Tensor.scalar epsilon }] 2 { id := 2, parents := #[0, 1], kind := IR.OpKind.safeLog, outShape := s } = Except.ok { shape := s, tensor := Activation.safeLogSpec x epsilon }

The scalar epsilon parent is read in the same context as the input tensor.

In particular, this equality also preserves an epsilon tangent when the context is a dual number type. The IR node uses the source operation's total logarithm semantics; checking a positive logarithm interval belongs to certificate construction.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_exp_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.exp s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := x.expSpec }

Local IR semantics for exp.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_sin_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.sin s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := TorchLean.Tensor.mapSpec (fun (v : α) => MathFunctions.sin v) x }

Local IR semantics for sin.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_cos_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) : (unaryGraph IR.OpKind.cos s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := TorchLean.Tensor.mapSpec (fun (v : α) => MathFunctions.cos v) x }

Local IR semantics for cos.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_log_eq {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (x : TorchLean.Tensor α s) (hpos : TorchLean.Tensor.allSpec (fun (v : α) => decide (0 < v)) x = true) : (unaryGraph IR.OpKind.log s).evalAt { } { shape := s, tensor := x } #[{ shape := s, tensor := x }] 1 = Except.ok { shape := s, tensor := x.logSpec }

Local IR semantics for log on inputs satisfying the IR positivity side condition.