Parameter Store To IR Payload Bridge

The verifier stores parameters in ParamStore, while executable graph semantics reads Payload. The declarations below state how that conversion affects lookups and the payload-backed operations used by the proved forward language. Convolution is stated for an arbitrary number of spatial axes; tensor layout is represented by the node's channel axis rather than by a format-specific operator.

def NN.Verification.Builtin.Proved.Correctness.IRStep.irConstOfFlatTensor {α : Type} [TorchLean.Storage α] [Context α] (c : MLTheory.CROWN.Graph.FlatTensor α) : IR.ConstFlat α

Convert a verifier flat tensor into the IR constant payload format.

def NN.Verification.Builtin.Proved.Correctness.IRStep.irLinearOfLinParams {α : Type} [TorchLean.Storage α] [Context α] (p : MLTheory.CROWN.Graph.LinParams α) : IR.LinearWB α

Convert verifier affine parameters into the IR linear payload format.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.payloadOfParamStore_const?_eq {α : Type} [TorchLean.Storage α] [Context α] (ps : MLTheory.CROWN.Graph.ParamStore α) (id : ℕ) : (payloadOfParamStore ps).const? id = Option.map irConstOfFlatTensor (ps.constVals.get? id)

Constant lookup after converting a verifier parameter store to an IR payload.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.payloadOfParamStore_linear?_eq {α : Type} [TorchLean.Storage α] [Context α] (ps : MLTheory.CROWN.Graph.ParamStore α) (id : ℕ) : (payloadOfParamStore ps).linear? id = Option.map irLinearOfLinParams (ps.linearWB.get? id)

Affine-layer lookup after converting a verifier parameter store to an IR payload.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.payloadOfParamStore_conv?_eq {α : Type} [TorchLean.Storage α] [Context α] (ps : MLTheory.CROWN.Graph.ParamStore α) (id : ℕ) : (payloadOfParamStore ps).conv? id = ps.convCfg.get? id

Convolution lookup after converting a verifier parameter store to an IR payload.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.payloadOfParamStore_batchNormEval?_eq {α : Type} [TorchLean.Storage α] [Context α] (ps : MLTheory.CROWN.Graph.ParamStore α) (id : ℕ) : (payloadOfParamStore ps).batchNormEval? id = ps.batchNormEval.get? id

BatchNorm lookup after converting a verifier parameter store to an IR payload.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.payloadOfParamStore_layerNorm?_eq {α : Type} [TorchLean.Storage α] [Context α] (ps : MLTheory.CROWN.Graph.ParamStore α) (id : ℕ) : (payloadOfParamStore ps).layerNorm? id = ps.layerNorm.get? id

LayerNorm lookup after converting a verifier parameter store to an IR payload.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_const_from_paramStore_of_getNode {α : Type} [TorchLean.Storage α] [Context α] (g : IR.Graph) (ps : MLTheory.CROWN.Graph.ParamStore α) (i id : ℕ) (s inputShape : Spec.Shape) (input : TorchLean.Tensor α inputShape) (vals : Array (Spec.SomeTensor α)) (v : TorchLean.Tensor α [s.size]) (hNode : g.getNode i = pure { id := id, parents := #[], kind := IR.OpKind.const s, outShape := s }) (hStore : ps.constVals.get? id = some { n := s.size, v := v }) : g.evalAt (payloadOfParamStore ps) (Spec.SomeTensor.ofTensor input) vals i = Except.ok (Spec.SomeTensor.ofTensor (TorchLean.Tensor.unflattenSpec s v))

A const node reads its value from the matching parameter-store entry.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_linear_from_paramStore_of_getNode {α : Type} [TorchLean.Storage α] [Context α] (g : IR.Graph) (ps : MLTheory.CROWN.Graph.ParamStore α) (i id parentId outDim inDim : ℕ) (inputShape : Spec.Shape) (input : TorchLean.Tensor α inputShape) (vals : Array (Spec.SomeTensor α)) (weight : TorchLean.Tensor α [outDim, inDim]) (bias : TorchLean.Tensor α [outDim]) (x : TorchLean.Tensor α [inDim]) (parent : Spec.SomeTensor α) (hNode : g.getNode i = pure { id := id, parents := #[parentId], kind := IR.OpKind.linear, outShape := Spec.Shape.dim outDim Spec.Shape.scalar }) (hParentValue : vals[parentId]? = some parent) (hParent : IR.Graph.expectShape (Spec.Shape.dim inDim Spec.Shape.scalar) parent = Except.ok x) (hStore : ps.linearWB.get? id = some { m := outDim, n := inDim, w := weight, b := bias }) : g.evalAt (payloadOfParamStore ps) (Spec.SomeTensor.ofTensor input) vals i = Except.ok (Spec.SomeTensor.ofTensor ((Spec.matVecMulSpec weight x).addSpec bias))

A linear node reads its weights and bias from the matching parameter-store entry.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalConv_from_paramStore {α : Type} [TorchLean.Storage α] [Context α] (ps : MLTheory.CROWN.Graph.ParamStore α) (id : ℕ) (params : IR.ConvParams α) (config : IR.ConvConfig) (parent : Spec.SomeTensor α) (leading : Spec.Shape) (hStore : ps.convCfg.get? id = some params) (hConfig : params.matchesConfig config = true) (hInfer : IR.OpContracts.inferConvConfigOutShape "conv" config parent.shape = Except.ok (params.output leading)) (hLeading : Spec.Shape.ofList (List.take config.channelAxis parent.shape.toList) = leading) (hInput : parent.shape = params.input leading) : IR.Graph.evalConv (payloadOfParamStore ps) id config parent = Except.ok (Spec.SomeTensor.ofTensor (TorchLean.Tensor.mapLeading leading (Spec.groupedConvSpec params.groups params.spec.kernel params.spec.bias) (hInput ▸ parent.tensor)))

Evaluation reads arbitrary-rank convolution parameters from the matching store entry.

theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_conv_from_paramStore_of_getNode {α : Type} [TorchLean.Storage α] [Context α] (g : IR.Graph) (ps : MLTheory.CROWN.Graph.ParamStore α) (i id parentId : ℕ) (params : IR.ConvParams α) (config : IR.ConvConfig) (leading inputShape : Spec.Shape) (input : TorchLean.Tensor α inputShape) (vals : Array (Spec.SomeTensor α)) (x : TorchLean.Tensor α (params.input leading)) (parent : Spec.SomeTensor α) (hNode : g.getNode i = pure { id := id, parents := #[parentId], kind := IR.OpKind.conv config, outShape := params.output leading }) (hParentValue : vals[parentId]? = some parent) (hParent : IR.Graph.expectShape (params.input leading) parent = Except.ok x) (hStore : ps.convCfg.get? id = some params) (hConfig : params.matchesConfig config = true) (hInfer : IR.OpContracts.inferConvConfigOutShape "conv" config parent.shape = Except.ok (params.output leading)) (hLeading : Spec.Shape.ofList (List.take config.channelAxis parent.shape.toList) = leading) : g.evalAt (payloadOfParamStore ps) (Spec.SomeTensor.ofTensor input) vals i = Except.ok (Spec.SomeTensor.ofTensor (TorchLean.Tensor.mapLeading leading (Spec.groupedConvSpec params.groups params.spec.kernel params.spec.bias) x))

A convolution node reads arbitrary-rank convolution parameters from the matching store entry.

The shape-inference equation is the graph's dynamic check. The remaining hypotheses identify the typed parent and output shapes; none fixes a spatial rank or memory layout.