TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Verification.Builtin.Proved.Correctness.Eval.PayloadOps

Payload-Backed IR Evaluation #

linear and conv nodes read weights from the external IR payload. These lemmas state the local contract at that boundary: when the expected payload is present and the shape preconditions are met, the IR evaluator returns the corresponding spec-layer operation.

source
def NN.Verification.Builtin.Proved.Correctness.IRStep.singletonAt {β : Type} (id : ℕ) (x : β) :
ℕ → Option β

A lookup table with one defined entry.

Instances For
    source
    @[simp]
    theorem NN.Verification.Builtin.Proved.Correctness.IRStep.singletonAt_self {β : Type} (id : ℕ) (x : β) :
    singletonAt id x id = some x

    Looking up the defining index of a singleton table returns its stored value.

    source
    def NN.Verification.Builtin.Proved.Correctness.IRStep.singletonConstPayload {α : Type} [TorchLean.Storage α] [Context α] (id : ℕ) (c : IR.ConstFlat α) :
    IR.Payload α

    A payload containing one flat constant at id.

    Instances For
      source
      def NN.Verification.Builtin.Proved.Correctness.IRStep.singletonLinearPayload {α : Type} [TorchLean.Storage α] [Context α] (id : ℕ) (p : IR.LinearWB α) :
      IR.Payload α

      A payload containing one linear layer at id.

      Instances For
        source
        def NN.Verification.Builtin.Proved.Correctness.IRStep.singletonConvPayload {α : Type} [TorchLean.Storage α] [Context α] (id : ℕ) (p : IR.ConvParams α) :
        IR.Payload α

        A payload containing one convolution layer at id.

        Instances For
          source
          def NN.Verification.Builtin.Proved.Correctness.IRStep.singletonBatchNormEvalPayload {α : Type} [TorchLean.Storage α] [Context α] (id : ℕ) (p : IR.BatchNormEvalParams α) :
          IR.Payload α

          A payload containing one eval-mode BatchNorm layer at id.

          Instances For
            source
            def NN.Verification.Builtin.Proved.Correctness.IRStep.constGraph (s : Spec.Shape) :
            IR.Graph

            A graph containing a zero-parent const node.

            Instances For
              source
              theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalConst_eq_unflatten {α : Type} [TorchLean.Storage α] [Context α] (id : ℕ) (s : Spec.Shape) (v : TorchLean.Tensor α [s.size]) :
              have c := { n := s.size, v := v }; IR.Graph.evalConst (singletonConstPayload id c) id s = Except.ok (TorchLean.Tensor.unflattenSpec s v)

              Local IR semantics for a payload-backed flat const node.

              source
              theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_const_eq_unflatten {α : Type} [TorchLean.Storage α] [Context α] (s : Spec.Shape) (v : TorchLean.Tensor α [s.size]) :
              have c := { n := s.size, v := v }; (constGraph s).evalAt (singletonConstPayload 0 c) { shape := s, tensor := TorchLean.Tensor.default } #[] 0 = Except.ok { shape := s, tensor := TorchLean.Tensor.unflattenSpec s v }

              Local IR semantics for a payload-backed flat const node.

              source
              theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalConst_missing_payload {α : Type} [TorchLean.Storage α] [Context α] (payload : IR.Payload α) (id : ℕ) (s : Spec.Shape) (hMissing : payload.const? id = none) :
              IR.Graph.evalConst payload id s = Except.error (toString "IR eval: missing const payload for node " ++ toString id)

              Missing constant payloads are rejected before unflattening.

              source
              theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalLinear_eq_affine {α : Type} [TorchLean.Storage α] [Context α] (id outDim inDim : ℕ) (W : TorchLean.Tensor α [outDim, inDim]) (b : TorchLean.Tensor α [outDim]) (x : TorchLean.Tensor α [inDim]) :
              have p := { outDim := outDim, inDim := inDim, W := W, b := b }; IR.Graph.evalLinear (singletonLinearPayload id p) id { shape := Spec.Shape.dim inDim Spec.Shape.scalar, tensor := x } (Spec.Shape.dim outDim Spec.Shape.scalar) = Except.ok { shape := Spec.Shape.dim outDim Spec.Shape.scalar, tensor := (Spec.matVecMulSpec W x).addSpec b }

              Local IR semantics for a payload-backed linear node.

              source
              theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalAt_linear_eq_affine {α : Type} [TorchLean.Storage α] [Context α] (outDim inDim : ℕ) (W : TorchLean.Tensor α [outDim, inDim]) (b : TorchLean.Tensor α [outDim]) (x : TorchLean.Tensor α [inDim]) :
              have p := { outDim := outDim, inDim := inDim, W := W, b := b }; (unaryGraphOut IR.OpKind.linear (Spec.Shape.dim inDim Spec.Shape.scalar) (Spec.Shape.dim outDim Spec.Shape.scalar)).evalAt (singletonLinearPayload 1 p) { shape := Spec.Shape.dim inDim Spec.Shape.scalar, tensor := x } #[{ shape := Spec.Shape.dim inDim Spec.Shape.scalar, tensor := x }] 1 = Except.ok { shape := Spec.Shape.dim outDim Spec.Shape.scalar, tensor := (Spec.matVecMulSpec W x).addSpec b }

              Local IR semantics for a payload-backed linear node.

              source
              theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalLinear_missing_payload {α : Type} [TorchLean.Storage α] [Context α] (payload : IR.Payload α) (id : ℕ) (hMissing : payload.linear? id = none) (x : Spec.SomeTensor α) (outShape : Spec.Shape) :
              IR.Graph.evalLinear payload id x outShape = Except.error (toString "IR eval: missing linear payload for node " ++ toString id)

              Missing linear payloads are rejected before the affine operation is evaluated.

              source
              def NN.Verification.Builtin.Proved.Correctness.IRStep.convolutionConfig {α : Type} [TorchLean.Storage α] [Context α] (params : IR.ConvParams α) :
              IR.ConvConfig

              The IR configuration carried by a convolution payload with no leading batch axes.

              Instances For
                source
                theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalConv_eq_spec {α : Type} [TorchLean.Storage α] [Context α] (id : ℕ) (params : IR.ConvParams α) (x : TorchLean.Tensor α (Spec.Shape.ofList (params.inChannels :: params.inputSpatial.to (List ℕ)))) (outShape : Spec.Shape) (hInfer : IR.OpContracts.inferConvConfigOutShape "conv" (convolutionConfig params) (Spec.Shape.ofList (params.inChannels :: params.inputSpatial.to (List ℕ))) = Except.ok outShape) :
                IR.Graph.evalConv (singletonConvPayload id params) id (convolutionConfig params) { shape := Spec.Shape.ofList (params.inChannels :: params.inputSpatial.to (List ℕ)), tensor := x } = Except.ok (Spec.SomeTensor.ofTensor (TorchLean.Tensor.mapLeading Spec.Shape.scalar (Spec.groupedConvSpec params.groups params.spec.kernel params.spec.bias) x))

                Local IR semantics for a payload-backed arbitrary-rank convolution.

                The shape-inference equation is exposed because it is exactly the dynamic check performed at the IR boundary. Once that check succeeds, evaluation is the typed Spec.groupedConvSpec operation.

                source
                theorem NN.Verification.Builtin.Proved.Correctness.IRStep.evalConv_missing_payload {α : Type} [TorchLean.Storage α] [Context α] (payload : IR.Payload α) (id : ℕ) (config : IR.ConvConfig) (x : Spec.SomeTensor α) (outShape : Spec.Shape) (hInfer : IR.OpContracts.inferConvConfigOutShape "conv" config x.shape = Except.ok outShape) (hMissing : payload.conv? id = none) :
                IR.Graph.evalConv payload id config x = Except.error (toString "IR eval: missing conv payload for node " ++ toString id)

                Missing convolution payloads are rejected before convolution is evaluated.