Derivative Interval Passes

These passes propagate interval bounds for first and second derivatives through the same flat graph used by IBP. They are kept separate from the value IBP pass because derivative propagation has its own chain-rule state, and it reuses the same FlatBox representation.

def NN.MLTheory.CROWN.Graph.runDeriv1D {α : Type} [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) : Array (Option (FlatBox α))

Derivative IBP pass for 1D input: computes for each node an interval on dy/dx. Requires value IBP boxes for activations.

def NN.MLTheory.CROWN.Graph.runDerivDirectional {α : Type} [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (seed : FlatBox α) : Array (Option (FlatBox α))

Directional first-derivative pass: like runDeriv1D but seeds the derivative at the input node with a user-provided direction vector (as a FlatBox with lo=hi). This allows extracting partial derivatives for multi-dimensional inputs by choosing e_x, e_y, etc.

def NN.MLTheory.CROWN.Graph.runDeriv2D {α : Type} [Context α] [BoundOps α] (g : Graph) (ps : ParamStore α) (ibp d1 : Array (Option (FlatBox α))) : Array (Option (FlatBox α))

Second-derivative IBP pass for 1D input: computes per node an interval on d²y/dx². Requires value IBP boxes and first-derivative boxes. Covers input, linear/matmul, tanh, add/sub.