Verification

Verification widgets (bounds / certificates).

This module provides small infoview panels for bound propagation artifacts, aimed at debugging and teaching rather than proofs:

• #crown_view g, st shows a per-node table for a CROWN.graph.PropState, including optional IBP boxes and optional affine forms.

The panel makes it easy to inspect:

• which nodes got bounds,
• the shapes and flattened dimensions that the propagation engine believes it is operating on,
• and small previews of the vectors/matrices involved.

Main definitions

• crownPropHtml: interactive per-node state viewer for CROWN/IBP propagation.
• boundsTightnessHtml: interval-width diagnostic panel ($\mathrm{hi}-\mathrm{lo}$) per node.
• #crown_view g, st: command form for crownPropHtml.
• #bounds_tightness_view g, st: command form for boundsTightnessHtml.

def NN.Widgets.crownPropHtml {α : Type} [TorchLean.Storage α] [Context α] [ToString α] (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.PropState α) (maxNodes : ℕ := 200) : ProofWidgets.Html

Render a CROWN.graph.PropState as a per-node HTML panel.

Bounds Tightness

When IBP boxes exist, a very fast diagnostic for "where are my bounds blowing up?" is to look at interval widths $\mathrm{hi}-\mathrm{lo}$ node-by-node.

This viewer computes width summaries per node and highlights missing IBP coverage.

def NN.Widgets.boundsTightnessHtml {α : Type} [TorchLean.Storage α] [Context α] [ToString α] (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.PropState α) (maxNodes : ℕ := 200) : ProofWidgets.Html

Render a per-node diagnostic panel summarizing IBP interval widths $\mathrm{hi}-\mathrm{lo}$.

Commands

def NN.Widgets.crownViewCmd : Lean.ParserDescr

def NN.Widgets.«command#crown_view_,_» : Lean.ParserDescr

def NN.Widgets.boundsTightnessViewCmd : Lean.ParserDescr

def NN.Widgets.«command#bounds_tightness_view_,_» : Lean.ParserDescr