IBP Certificate Step

Safe, option-returning certificate-step semantics for the graph IBP checker. This is the proof layer counterpart of the executable bound propagation step.

The IBP “certificate step” (safe, total)

This is a safe version of propagateIBPNode tailored to the subset of ops we prove soundness for. It defines what it means for a per-node certificate to be “locally well-formed”.

Important: the runtime implementation propagateIBPNode uses get! on parent boxes; it assumes topological order and that earlier boxes exist. Here we avoid partiality by returning none whenever parents are missing.

def NN.MLTheory.CROWN.Graph.CertSoundness.getBox? (cert : Array (Option (FlatBox ℝ))) (pid : ℕ) : Option (FlatBox ℝ)

Safe lookup of the interval box recorded for node id pid, none when out of range.

noncomputable def NN.MLTheory.CROWN.Graph.CertSoundness.certStepNode? (nodes : Array Node) (ps : ParamStore ℝ) (cert : Array (Option (FlatBox ℝ))) (id : ℕ) : Option (FlatBox ℝ)

Safe per-node IBP step for the checker semantics.

This is the total (option-returning) analogue of the runtime propagateIBPNode, restricted to the ops handled in the soundness development.

def NN.MLTheory.CROWN.Graph.CertSoundness.CertLocalOK (g : Graph) (ps : ParamStore ℝ) (cert : Array (Option (FlatBox ℝ))) : Prop

A certificate is locally consistent if every node equals certStepNode? at that node.