Lowered Forward Evaluation: Payload-Free Nodes

One lemma per payload-free operator of the proved forward fragment. Each lemma assumes that the IR graph holds the node emitted by lowerNode at index id and that the runtime value array matches the typed shape context; it concludes that IR evaluation at id returns exactly what the typed evaluator evalNode returns for the source node. The IR payload is arbitrary because these operators never read it.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_add {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (a b : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[a.id, b.id], kind := IR.OpKind.add, outShape := s }) : G.evalAt payload input vals id = evalNode (Node.add a b) params vals

A lowered add node evaluates like the typed add node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_sub {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (a b : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[a.id, b.id], kind := IR.OpKind.sub, outShape := s }) : G.evalAt payload input vals id = evalNode (Node.sub a b) params vals

A lowered sub node evaluates like the typed sub node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_mulElem {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (a b : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[a.id, b.id], kind := IR.OpKind.mulElem, outShape := s }) : G.evalAt payload input vals id = evalNode (Node.mulElem a b) params vals

A lowered mulElem node evaluates like the typed mulElem node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_relu {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (xIdx : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[xIdx.id], kind := IR.OpKind.relu, outShape := s }) : G.evalAt payload input vals id = evalNode (Node.relu xIdx) params vals

A lowered relu node evaluates like the typed relu node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_exp {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (xIdx : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[xIdx.id], kind := IR.OpKind.exp, outShape := s }) : G.evalAt payload input vals id = evalNode (Node.exp xIdx) params vals

A lowered exp node evaluates like the typed exp node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_inv {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (xIdx : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[xIdx.id], kind := IR.OpKind.inv, outShape := s }) : G.evalAt payload input vals id = evalNode (Node.inv xIdx) params vals

A lowered inv node evaluates like the typed inv node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_log {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (xIdx : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[xIdx.id], kind := IR.OpKind.log, outShape := s }) : G.evalAt payload input vals id = evalNode (Node.log xIdx) params vals

A lowered log node evaluates like the typed log node. Both evaluators reject nonpositive inputs with the same error, so the agreement holds without a positivity side condition.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_matmul {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {leftShape rightShape outShape : Spec.Shape} (op : MatmulOperation leftShape rightShape outShape) (a : Idx (Ctx inShape ss) leftShape) (b : Idx (Ctx inShape ss) rightShape) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[a.id, b.id], kind := IR.OpKind.matmul, outShape := outShape }) : G.evalAt payload input vals id = evalNode (Node.matmul op a b) params vals

A lowered matmul node evaluates like the typed matmul node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_reshape {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} (inS outS : Spec.Shape) (h : inS.size = outS.size) (xIdx : Idx (Ctx inShape ss) inS) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[xIdx.id], kind := IR.OpKind.reshape inS outS, outShape := outS }) : G.evalAt payload input vals id = evalNode (Node.reshape inS outS h xIdx) params vals

A lowered reshape node evaluates like the typed reshape node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_transpose {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s out : Spec.Shape} (axis₁ axis₂ : ℕ) (hOut : IR.OpContracts.inferTransposeOutShape axis₁ axis₂ s = Except.ok out) (xIdx : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[xIdx.id], kind := IR.OpKind.transpose axis₁ axis₂, outShape := out }) : G.evalAt payload input vals id = evalNode (Node.transpose axis₁ axis₂ hOut xIdx) params vals

A lowered transpose node evaluates like the typed transpose node. Both evaluators run the same dynamic permutation, so the proof follows the three fallible steps case by case.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_softmax {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (axis : ℕ) (hAxis : Spec.Shape.AxisInBounds axis s) (xIdx : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[xIdx.id], kind := IR.OpKind.softmax axis, outShape := s }) : G.evalAt payload input vals id = evalNode (Node.softmax axis hAxis xIdx) params vals

A lowered softmax node evaluates like the typed softmax node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_mseLoss {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (yhat target : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (payload : IR.Payload α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hShapes : shapesOfVals vals = Ctx inShape ss) (hGetNode : G.getNode id = pure { id := id, parents := #[yhat.id, target.id], kind := IR.OpKind.mseLoss, outShape := Spec.Shape.scalar }) : G.evalAt payload input vals id = evalNode (Node.mseLoss yhat target) params vals

A lowered mseLoss node evaluates like the typed mseLoss node. Both evaluators perform the same dynamic equal-shape check before averaging the squared error.