α-CROWN Transfer: Value-Preserving Nodes #
The .detach, .reshape, and .flatten cases of alphaCrown_transfer_sound. These operators
forward the parent's value, at most recasting its dimension, so the parent's affine bounds are
forwarded (and recast) as well.
theorem
NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.detach_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.detach)
(hs : stepAlpha g ps ibp alpha ctx cert id = some b)
(hEvalSome : CertSoundness.evalNode? g.nodes ps inputs vals id = some v)
(hpar : ParentsEnclosed g cert vals ctx x id)
:
CrownCertSoundness.EnclosesAtInput ctx x b v
The .detach case: the step forwards the parent's affine bounds and the evaluator forwards the
parent's value, so the parent enclosure is the result.
theorem
NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.reshape_flatten_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 :
(∃ (s₁ : Spec.Shape) (s₂ : Spec.Shape), g.nodes[id]!.kind = IR.OpKind.reshape s₁ s₂) ∨ ∃ (s : Spec.Shape), g.nodes[id]!.kind = IR.OpKind.flatten s)
(hs : stepAlpha g ps ibp alpha ctx cert id = some b)
(hEvalSome : CertSoundness.evalNode? g.nodes ps inputs vals id = some v)
(hpar : ParentsEnclosed g cert vals ctx x id)
:
CrownCertSoundness.EnclosesAtInput ctx x b v
The shared .reshape and .flatten case: the step casts the parent's affine bounds to the
node's output size and the evaluator casts the parent's value, both guarded by the same size check,
so the parent enclosure transports along the cast.