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.

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.

@[reducible, inline]

abbrev NN.Verification.Builtin.Proved.Correctness.loweredConvConfig {d : ℕ} (inC outC : ℕ) (kernelShape stride padding : TorchLean.Tensor ℕ [d]) : IR.ConvConfig

The IR convolution configuration emitted by lowering a conv node.

@[reducible, inline]

abbrev NN.Verification.Builtin.Proved.Correctness.loweredConvParams {α : Type} [TorchLean.Storage α] [Context α] {d : ℕ} (inC outC : ℕ) (kernelShape stride padding inSpatial : TorchLean.Tensor ℕ [d]) (hKernel : ∀ (i : Fin d), kernelShape.getScalar i ≠ 0) (hStride : ∀ (i : Fin d), stride.getScalar i ≠ 0) (kT : TorchLean.Tensor α (Spec.Shape.ofList (outC :: inC :: kernelShape.to (List ℕ)))) (bT : TorchLean.Tensor α [outC]) : IR.ConvParams α

The convolution payload written to the parameter store by lowering a conv node.

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 conv node evaluates like the typed conv node. The IR evaluates a grouped, dilated convolution with groups = 1, unit dilation, and symmetric padding, which agrees with the dense Spec.convSpec used by the typed evaluator up to a shape cast.