Lowered Forward Evaluation: Payload-Backed Nodes

One lemma per operator of the proved forward fragment whose lowering writes to the verifier ParamStore: constants, linear layers, LayerNorm (which erases its own entry so the IR falls back to unit affine parameters), and convolutions. Each lemma assumes the IR graph holds the node emitted by lowerNode at index id and that the parameter store agrees with the lowering at that id; it concludes that IR evaluation returns exactly what the typed evaluator evalNode returns.

The convolution theorem covers arbitrary spatial rank, but this source fragment is unbatched, with one group, unit dilation, and symmetric padding. PayloadBridge separately relates the more general parameter-store convolution to its IR evaluation.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_const {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (wf : s.WellFormed) (t : TorchLean.Tensor α s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (P : MLTheory.CROWN.Graph.ParamStore α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hGetNode : G.getNode id = pure { id := id, parents := #[], kind := IR.OpKind.const s, outShape := s }) (hConst : P.constVals.get? id = some (flatOfTensor wf t)) : G.evalAt (payloadOfParamStore P) input vals id = evalNode (Node.const wf t) params vals

A lowered const node evaluates like the typed const node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_paramConst {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (wf : s.WellFormed) (p : Idx paramShapes s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (P : MLTheory.CROWN.Graph.ParamStore α) (input : Spec.SomeTensor α) (vals : Array (Spec.SomeTensor α)) (id : ℕ) (hGetNode : G.getNode id = pure { id := id, parents := #[], kind := IR.OpKind.const s, outShape := s }) (hConst : P.constVals.get? id = some (flatOfTensor wf (getParam params p))) : G.evalAt (payloadOfParamStore P) input vals id = evalNode (Node.paramConst wf p) params vals

A lowered paramConst node evaluates like the typed paramConst node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_linear {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} (inDim outDim : ℕ) (w : Idx paramShapes (Spec.Shape.dim outDim (Spec.Shape.dim inDim Spec.Shape.scalar))) (b : Idx paramShapes (Spec.Shape.dim outDim Spec.Shape.scalar)) (xIdx : Idx (Ctx inShape ss) (Spec.Shape.dim inDim Spec.Shape.scalar)) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (P : MLTheory.CROWN.Graph.ParamStore α) (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.linear, outShape := Spec.Shape.dim outDim Spec.Shape.scalar }) (hLin : P.linearWB.get? id = some { m := outDim, n := inDim, w := getParam params w, b := getParam params b }) : G.evalAt (payloadOfParamStore P) input vals id = evalNode (Node.linear inDim outDim w b xIdx) params vals

A lowered linear node evaluates like the typed linear node.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_layerNorm {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {s : Spec.Shape} (op : LayerNormOperation s) (xIdx : Idx (Ctx inShape ss) s) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (P : MLTheory.CROWN.Graph.ParamStore α) (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.layernorm op.axis, outShape := s }) (hLayerNorm : P.layerNorm.get? id = none) : G.evalAt (payloadOfParamStore P) input vals id = evalNode (Node.layerNorm op xIdx) params vals

A lowered layerNorm node evaluates like the typed layerNorm node. The lowering erases any LayerNorm payload at the fresh id, so the IR evaluator applies unit affine parameters, matching the typed evaluator's gamma = 1, beta = 0.

theorem NN.Verification.Builtin.Proved.Correctness.evalAt_eq_evalNode_conv {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {d : ℕ} (inC outC : ℕ) (kernelShape stride padding inSpatial : TorchLean.Tensor ℕ [d]) (hIn : inC ≠ 0) (hKernel : ∀ (i : Fin d), kernelShape.getScalar i ≠ 0) (hStride : ∀ (i : Fin d), stride.getScalar i ≠ 0) (hInfer : IR.OpContracts.inferConvOutShape "conv" 0 inC outC kernelShape stride padding (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ))) = Except.ok (Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernelShape stride padding).to (List ℕ)))) (kernel : Idx paramShapes (Spec.Shape.ofList (outC :: inC :: kernelShape.to (List ℕ)))) (bias : Idx paramShapes (Spec.Shape.dim outC Spec.Shape.scalar)) (xIdx : Idx (Ctx inShape ss) (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ)))) (params : TorchLean.TensorPack α paramShapes) (G : IR.Graph) (P : MLTheory.CROWN.Graph.ParamStore α) (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.conv (loweredConvConfig inC outC kernelShape stride padding), outShape := Spec.Shape.ofList (outC :: (Spec.convOutSpatial inSpatial kernelShape stride padding).to (List ℕ)) }) (hConv : P.convCfg.get? id = some (loweredConvParams inC outC kernelShape stride padding inSpatial hKernel hStride (getParam params kernel) (getParam params bias))) : G.evalAt (payloadOfParamStore P) input vals id = evalNode (Node.conv inC outC kernelShape stride padding inSpatial hIn hKernel hStride hInfer kernel bias xIdx) params vals

A lowered unbatched conv node evaluates like the typed conv node. The IR evaluates a grouped, dilated convolution with groups = 1, unit dilation, and symmetric padding, agreeing with the dense Spec.convSpec used by the typed evaluator up to a shape cast.