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.propagateIBPNodeAt {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (nodes : Array Node) (ps : ParamStore α) (boxes : Array (Option (FlatBox α))) (id : ℕ) (node : Node) : Array (Option (FlatBox α))

IBP propagation for one node, with the node record passed explicitly.

propagateIBPNode instantiates node with nodes[id]!. Taking the record as an argument lets the proof layer rewrite it to a literal and evaluate the array-pattern matches below definitionally, which is how the step is identified with its safe counterpart CertSoundness.certStepNode?.

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 α))

IBP propagation for one node using ParamStore.

This executable function expects parents to have already been processed. The proof layer makes that precondition explicit via TopoSorted; callers that execute graphs directly should use graphs whose parents appear before their children.

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?.