TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Verification.Builtin.Lowering

TorchLean Verification Lowering #

Umbrella import for the graph builder and the public TorchLean-to-verifier-IR lowering API.

source
def NN.Verification.Builtin.withBoundArithmetic (arithmetic : TorchLean.Runtime.Arithmetic) (k : {α : Type} → [inst : TorchLean.Storage α] → [inst_1 : Context α] → [ToString α] → [TorchLean.Runtime.FromFloat α] → [MLTheory.CROWN.BoundOps α] → [MLTheory.CROWN.NonlinearBoundOps α] → IO Unit) :
IO Unit

Dispatch an executable bound-propagation computation under arithmetic semantics with explicit outward endpoint operations, including nonlinear division and normalization bounds.

Native Float32 and the bit-level ExecFloat.Binary 8 23 backend meet that interface. Complex arithmetic is rejected instead of receiving an invalid real-valued bound implementation.

Instances For
    source
    def NN.Verification.Builtin.runWithBoundArithmetic (title : String) (args : List String) (k : {α : Type} → [inst : TorchLean.Storage α] → [inst_1 : Context α] → [ToString α] → [TorchLean.Runtime.FromFloat α] → [MLTheory.CROWN.BoundOps α] → [MLTheory.CROWN.NonlinearBoundOps α] → IO Unit) :
    IO Unit

    Parse and log arithmetic semantics, then run withBoundArithmetic.

    Instances For