TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Verification.Builtin.Proved.Lowering

Verified Forward Fragment: Lowering #

Lowering from the first-order forward fragment into the verifier IR graph and parameter store.

Lowering to verifier IR #

source
def NN.Verification.Builtin.Proved.flatOfTensor {α : Type} [TorchLean.Storage α] [Context α] {s : Spec.Shape} (_wf : s.WellFormed) (t : TorchLean.Tensor α s) :
MLTheory.CROWN.Graph.FlatTensor α

Flatten a well-formed tensor into the FlatTensor payload format used by CROWN/LiRPA IR nodes.

Instances For
    source
    @[reducible, inline]
    abbrev NN.Verification.Builtin.Proved.loweredConvConfig {d : ℕ} (inC outC : ℕ) (kernelShape stride padding : TorchLean.Tensor ℕ [d]) :
    IR.ConvConfig

    The IR convolution configuration emitted by lowering a conv node.

    Instances For
      source
      @[reducible, inline]
      abbrev NN.Verification.Builtin.Proved.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.

      Instances For
        source
        def NN.Verification.Builtin.Proved.lowerNode {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape : Spec.Shape} {ss : List Spec.Shape} {out : Spec.Shape} (id : ℕ) (node : Node α paramShapes inShape ss out) (params : TorchLean.TensorPack α paramShapes) (ps : MLTheory.CROWN.Graph.ParamStore α) :
        IR.Node × MLTheory.CROWN.Graph.ParamStore α

        Lower a single forward-fragment node into the verifier IR.

        Returns the corresponding NN.IR.Node together with an updated CROWN ParamStore that contains any payload required by .const, .linear, and convolution nodes. LayerNorm erases the entry at this id so that the IR uses unit affine parameters, as the source node does.

        Instances For
          source
          def NN.Verification.Builtin.Proved.lowerForwardLetChain {α : 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 α) :
          LoweredIR α

          Append a forward let-chain to the graph and payload store in c. Node ids follow the graph's current size; the return node sets the output id, which may name an earlier value.

          Instances For
            source
            def NN.Verification.Builtin.Proved.lowerForwardProgramToIR {α : Type} [TorchLean.Storage α] [Context α] {paramShapes : List Spec.Shape} {inShape outShape : Spec.Shape} (p : ForwardProgram α paramShapes inShape outShape) (params : TorchLean.TensorPack α paramShapes) :
            LoweredIR α

            Lower a proved forward-fragment program into the verifier IR.

            The resulting LoweredIR can be executed by the IR evaluator. The modules under NN.Verification.Builtin.Proved.Correctness prove that its denotation agrees with evalForward.

            Instances For