α-CROWN Transfer: Leaf Nodes #
The .input and .const cases of alphaCrown_transfer_sound. Neither reads a parent
certificate: the input node returns the identity bounds and the constant node returns the point
box of its stored value.
theorem
NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.input_sound
{g : Graph}
{ps : ParamStore ℝ}
{ibp : Array (Option (FlatBox ℝ))}
{alpha : Array (Option (FlatTensor ℝ))}
{cert : Array (Option (FlatAffineBounds ℝ))}
{inputs : Std.HashMap ℕ CertSoundness.Val}
{vals : Array (Option CertSoundness.Val)}
{ctx : AffineCtx}
{x : TorchLean.Tensor ℝ [ctx.inputDim]}
{id : ℕ}
{b : FlatAffineBounds ℝ}
{v : CertSoundness.Val}
(hk : g.nodes[id]!.kind = IR.OpKind.input)
(hs : stepAlpha g ps ibp alpha ctx cert id = some b)
(hEvalSome : CertSoundness.evalNode? g.nodes ps inputs vals id = some v)
(hinputs : InputsMatch inputs ctx x)
:
CrownCertSoundness.EnclosesAtInput ctx x b v
The .input case: the step succeeds only at the designated input node and returns the identity
bounds, which enclose the input point x, and InputsMatch identifies the semantic value with
x.
theorem
NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.const_sound
{g : Graph}
{ps : ParamStore ℝ}
{ibp : Array (Option (FlatBox ℝ))}
{alpha : Array (Option (FlatTensor ℝ))}
{cert : Array (Option (FlatAffineBounds ℝ))}
{inputs : Std.HashMap ℕ CertSoundness.Val}
{vals : Array (Option CertSoundness.Val)}
{ctx : AffineCtx}
{x : TorchLean.Tensor ℝ [ctx.inputDim]}
{id : ℕ}
{b : FlatAffineBounds ℝ}
{v : CertSoundness.Val}
{shape : Spec.Shape}
(hk : g.nodes[id]!.kind = IR.OpKind.const shape)
(hs : stepAlpha g ps ibp alpha ctx cert id = some b)
(hEvalSome : CertSoundness.evalNode? g.nodes ps inputs vals id = some v)
:
CrownCertSoundness.EnclosesAtInput ctx x b v
The .const case: the step and the evaluator both read ps.constVals[id]?, and the step
returns the point box of the constant, which encloses it.