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.propagateIBPNode {α : Type} [Context α] [BoundOps α] (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} [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) : Array (Option (FlatBox α))

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