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 goal is to make it easy to sanity-check:

• 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 (hi - lo) per node.
• #crown_view g, st: command form for crownPropHtml.
• #bounds_tightness_view g, st: command form for boundsTightnessHtml.

Implementation notes

• We keep this viewer "pure HTML" using ProofWidgets #html with no custom JS.
• The same node ids are used for IR nodes and propagated states, so mismatches are easy to spot.
• DOT text is intentionally clipped for large graphs to keep infoview rendering responsive.

References

• CROWN / LiRPA style bound propagation
• GraphViz DOT language
• ProofWidgets
• Lean community documentation style

Tags

verification, crown, ibp, bounds, certificates, widgets

def NN.Widgets.crownPropHtml {α : Type} [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 hi - lo node-by-node.

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

def NN.Widgets.boundsTightnessHtml {α : Type} [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 (hi - 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