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
    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 payload-backed convolution nodes.

    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 α

      Lower a forward let-chain into a LoweredIR graph.

      This threads an accumulator LoweredIR that contains:

      • the growing NN.IR.Graph,
      • the payload store (ParamStore),
      • and the current output id.
      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, and we prove (in this file) that its denotation agrees with evalForward.

        Instances For