Interval Bound Propagation

This module runs the flat graph IBP pass. It computes one interval box per node from input boxes, constant tensors, and per-op interval transfer rules. The proof layer states the topological and shape hypotheses; this executable pass is the checker-facing computation they refer to.

def NN.MLTheory.CROWN.Graph.ibpSilu? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (input : FlatBox α) : Option (FlatBox α)

Enclose real SiLU by multiplying the input box and its sigmoid enclosure.

This is a real-function enclosure, not a bound on the rounding error of a native SiLU kernel.

def NN.MLTheory.CROWN.Graph.ibpStepNodeAt? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (nodes : Array Node) (ps : ParamStore α) (boxes : Array (Option (FlatBox α))) (id : ℕ) (node : Node) : Option (FlatBox α)

Compute one interval transfer. Missing parents and unavailable transfers return none.

def NN.MLTheory.CROWN.Graph.propagateIBPNodeAt {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (nodes : Array Node) (ps : ParamStore α) (boxes : Array (Option (FlatBox α))) (id : ℕ) (node : Node) : Array (Option (FlatBox α))

Store the result of one transfer, clearing any previous result if the transfer fails.

def NN.MLTheory.CROWN.Graph.propagateIBPNode {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (nodes : Array Node) (ps : ParamStore α) (boxes : Array (Option (FlatBox α))) (id : ℕ) : Array (Option (FlatBox α))

Propagate one node. Missing nodes or parent boxes leave the result unresolved.

def NN.MLTheory.CROWN.Graph.runIBP {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (g : Graph) (ps : ParamStore α) : Array (Option (FlatBox α))

Run an IBP pass over the whole graph. Caller seeds inputs via ParamStore.inputBoxes.

The body is exposed so that the proof layer can relate this pass to CertSoundness.runIBP?.