Certificate Soundness: Leaf and Pass-Through Nodes #
Operator cases input, const, and detach of the IBP certificate induction. These nodes do
no arithmetic: input is discharged by the input-box assumption, const by the point-box
enclosure, and detach by forwarding the parent enclosure.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.input_node_encloses
{nodes : Array Node}
{ps : ParamStore ℝ}
{cert : Array (Option (FlatBox ℝ))}
{inputs : Std.HashMap ℕ Val}
{vals : Array (Option Val)}
{k : ℕ}
{B : FlatBox ℝ}
{v : Val}
(hkKind : nodes[k]!.kind = IR.OpKind.input)
(hcertStep : certStepNode? nodes ps cert k = some B)
(hvalStep : evalNode? nodes ps inputs vals k = some v)
(hin : ∃ (Bin : FlatBox ℝ) (vin : Val), ps.inputBoxes[k]? = some Bin ∧ inputs[k]? = some vin ∧ EnclosesBox Bin vin)
:
EnclosesBox B v
Certificate soundness at an input node, given that the semantic input lies in the certified
input box.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.const_node_encloses
{nodes : Array Node}
{ps : ParamStore ℝ}
{cert : Array (Option (FlatBox ℝ))}
{inputs : Std.HashMap ℕ Val}
{vals : Array (Option Val)}
{k : ℕ}
{B : FlatBox ℝ}
{v : Val}
{valueShape : Spec.Shape}
(hkKind : nodes[k]!.kind = IR.OpKind.const valueShape)
(hcertStep : certStepNode? nodes ps cert k = some B)
(hvalStep : evalNode? nodes ps inputs vals k = some v)
:
EnclosesBox B v
Certificate soundness at a const node: the point box [c, c] encloses c.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.detach_node_encloses
{nodes : Array Node}
{ps : ParamStore ℝ}
{cert : Array (Option (FlatBox ℝ))}
{inputs : Std.HashMap ℕ Val}
{vals : Array (Option Val)}
{k : ℕ}
{B : FlatBox ℝ}
{v : Val}
(hkKind : nodes[k]!.kind = IR.OpKind.detach)
(hcertStep : certStepNode? nodes ps cert k = some B)
(hvalStep : evalNode? nodes ps inputs vals k = some v)
(hpe : ParentsEnclosed nodes cert vals k)
:
EnclosesBox B v
Certificate soundness at a detach node: box and value are forwarded from the parent.