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 the payload-backed constructors in the proved forward fragment.
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_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.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerForwardLetChain_payloadOfParamStore_const?_lt
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{out : Spec.Shape}
(g : ForwardLetChain α paramShapes inShape ss out)
(params : TorchLean.TensorPack α paramShapes)
(c : LoweredIR α)
{k : ℕ}
(hk : k < c.graph.nodes.size)
:
(payloadOfParamStore (lowerForwardLetChain g params c).ps).const? k = (payloadOfParamStore c.ps).const? k
Lowering a suffix preserves already-existing constant payload lookups seen by IR evaluation.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerForwardLetChain_payloadOfParamStore_linear?_lt
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{out : Spec.Shape}
(g : ForwardLetChain α paramShapes inShape ss out)
(params : TorchLean.TensorPack α paramShapes)
(c : LoweredIR α)
{k : ℕ}
(hk : k < c.graph.nodes.size)
:
(payloadOfParamStore (lowerForwardLetChain g params c).ps).linear? k = (payloadOfParamStore c.ps).linear? k
Lowering a suffix preserves already-existing linear payload lookups seen by IR evaluation.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerForwardLetChain_payloadOfParamStore_conv?_lt
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{out : Spec.Shape}
(g : ForwardLetChain α paramShapes inShape ss out)
(params : TorchLean.TensorPack α paramShapes)
(c : LoweredIR α)
{k : ℕ}
(hk : k < c.graph.nodes.size)
:
(payloadOfParamStore (lowerForwardLetChain g params c).ps).conv? k = (payloadOfParamStore c.ps).conv? k
Lowering a suffix preserves already-existing convolution payload lookups seen by IR evaluation.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerForwardLetChain_payloadOfParamStore_batchNormEval?_lt
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{out : Spec.Shape}
(g : ForwardLetChain α paramShapes inShape ss out)
(params : TorchLean.TensorPack α paramShapes)
(c : LoweredIR α)
{k : ℕ}
(hk : k < c.graph.nodes.size)
:
(payloadOfParamStore (lowerForwardLetChain g params c).ps).batchNormEval? k = (payloadOfParamStore c.ps).batchNormEval? k
Lowering a suffix preserves already-existing BatchNorm payload lookups seen by IR evaluation.
theorem
NN.Verification.Builtin.Proved.Correctness.IRStep.lowerForwardLetChain_payloadOfParamStore_layerNorm?_lt
{α : Type}
[TorchLean.Storage α]
[Context α]
{paramShapes : List Spec.Shape}
{inShape : Spec.Shape}
{ss : List Spec.Shape}
{out : Spec.Shape}
(g : ForwardLetChain α paramShapes inShape ss out)
(params : TorchLean.TensorPack α paramShapes)
(c : LoweredIR α)
{k : ℕ}
(hk : k < c.graph.nodes.size)
:
(payloadOfParamStore (lowerForwardLetChain g params c).ps).layerNorm? k = (payloadOfParamStore c.ps).layerNorm? k
Lowering a suffix preserves already-existing LayerNorm payload lookups seen by IR evaluation.