Lowering Pass Payload Insertion #
The forward-fragment lowering pass emits an IR node and, when the node needs external data,
records that data in the verifier ParamStore at the same fresh node id. These lemmas pin down
that insertion step for every constructor of the proved forward fragment that touches the store.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerNode_const_payload
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{s : Spec.Shape}
(id : ℕ)
(wf : s.WellFormed)
(t : TorchLean.Tensor α s)
(params : TorchLean.TensorPack α paramShapes)
(ps : MLTheory.CROWN.Graph.ParamStore α)
:
Lowering a literal constant stores its flattened tensor at the fresh IR node id.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerNode_paramConst_payload
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{s : Spec.Shape}
(id : ℕ)
(wf : s.WellFormed)
(p : Idx paramShapes s)
(params : TorchLean.TensorPack α paramShapes)
(ps : MLTheory.CROWN.Graph.ParamStore α)
:
(lowerNode id (Node.paramConst wf p) params ps).2.constVals.get? id = some (flatOfTensor wf (getParam params p))
Lowering a parameter constant stores the selected parameter tensor at the fresh IR node id.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerNode_linear_payload
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
(id 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))
(x : Idx (Ctx inShape ss) (Spec.Shape.dim inDim Spec.Shape.scalar))
(params : TorchLean.TensorPack α paramShapes)
(ps : MLTheory.CROWN.Graph.ParamStore α)
:
Lowering a linear node stores exactly the selected weight and bias tensors.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerNode_layerNorm_payload
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{s : Spec.Shape}
(id : ℕ)
(op : LayerNormOperation s)
(x : Idx (Ctx inShape ss) s)
(params : TorchLean.TensorPack α paramShapes)
(ps : MLTheory.CROWN.Graph.ParamStore α)
:
Lowering a LayerNorm node leaves no LayerNorm payload at the fresh IR node id, so the IR evaluator falls back to unit affine parameters.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerNode_conv_payload
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{d : ℕ}
(id 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))
(x : Idx (Ctx inShape ss) (Spec.Shape.ofList (inC :: inSpatial.to (List ℕ))))
(params : TorchLean.TensorPack α paramShapes)
(ps : MLTheory.CROWN.Graph.ParamStore α)
:
Lowering a convolution stores the dense kernel and bias as a unit-dilation, symmetric-padding convolution payload at the fresh IR node id.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerNode_const_node
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{s : Spec.Shape}
(id : ℕ)
(wf : s.WellFormed)
(t : TorchLean.Tensor α s)
(params : TorchLean.TensorPack α paramShapes)
(ps : MLTheory.CROWN.Graph.ParamStore α)
:
(lowerNode id (Node.const wf t) params ps).1 = { id := id, parents := #[], kind := IR.OpKind.const s, outShape := s }
The lowered IR node for a literal constant is the corresponding payload-backed const node.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerNode_paramConst_node
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{s : Spec.Shape}
(id : ℕ)
(wf : s.WellFormed)
(p : Idx paramShapes s)
(params : TorchLean.TensorPack α paramShapes)
(ps : MLTheory.CROWN.Graph.ParamStore α)
:
(lowerNode id (Node.paramConst wf p) params ps).1 = { id := id, parents := #[], kind := IR.OpKind.const s, outShape := s }
The lowered IR node for a parameter constant is the corresponding payload-backed const
node.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerNode_linear_node
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
(id 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))
(x : Idx (Ctx inShape ss) (Spec.Shape.dim inDim Spec.Shape.scalar))
(params : TorchLean.TensorPack α paramShapes)
(ps : MLTheory.CROWN.Graph.ParamStore α)
:
(lowerNode id (Node.linear inDim outDim w b x) params ps).1 = { id := id, parents := #[x.id], kind := IR.OpKind.linear, outShape := Spec.Shape.dim outDim Spec.Shape.scalar }
The lowered IR node for a linear source node has one activation parent and external payload.