α-CROWN Transfer: Shared Extraction Lemmas

Helper lemmas shared by the per-operator cases of alphaCrown_transfer_sound. They turn the safe lookups getAff?, getVal?, and getAlpha? into plain array lookups, package the parent hypothesis of CrownTransferSound, and transport enclosures across output-dimension casts and constant boxes.

def NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.ParentsEnclosed (g : Graph) (cert : Array (Option (FlatAffineBounds ℝ))) (vals : Array (Option CertSoundness.Val)) (ctx : AffineCtx) (x : TorchLean.Tensor ℝ [ctx.inputDim]) (id : ℕ) : Prop

Every parent p of node id whose certificate entry and semantic value are both present is enclosed at the input point x. This is the parent hypothesis of CrownTransferSound with its match unfolded.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.parentsEnclosed_of_match {g : Graph} {cert : Array (Option (FlatAffineBounds ℝ))} {vals : Array (Option CertSoundness.Val)} {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {id : ℕ} (hparents : ∀ p ∈ g.nodes[id]!.parents, match cert[p]!, vals[p]! with | some bp, some vp => CrownCertSoundness.EnclosesAtInput ctx x bp vp | x, x_1 => True) : ParentsEnclosed g cert vals ctx x id

The match-shaped parent hypothesis of CrownTransferSound implies ParentsEnclosed.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.getElem!_of_getAff?_eq_some {cert : Array (Option (FlatAffineBounds ℝ))} {p : ℕ} {xin : FlatAffineBounds ℝ} (h : Cert.getAff? cert p = some xin) : cert[p]! = some xin

A successful safe certificate lookup is a plain array lookup.

getElem!_of_getVal?_eq_some is CertSoundness's lemma, opened at the top of this file. Two files in this directory carried their own copy of it, proved with by_cases where the original uses unfold and split; the statements were the same, so the copies are gone.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.lt_size_and_getElem!_of_getAlpha?_eq_some {alpha : Array (Option (FlatTensor ℝ))} {id : ℕ} {αv : FlatTensor ℝ} (h : Cert.getAlpha? alpha id = some αv) : id < alpha.size ∧ alpha[id]! = some αv

A successful safe α lookup is in bounds and is a plain array lookup.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.parent_encloses_of_unaryParent? {g : Graph} {cert : Array (Option (FlatAffineBounds ℝ))} {vals : Array (Option CertSoundness.Val)} {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {id p1 : ℕ} {xin : FlatAffineBounds ℝ} {vp : CertSoundness.Val} (hpar : ParentsEnclosed g cert vals ctx x id) (hps : IR.unaryParent? g.nodes[id]!.parents = some p1) (hxin : Cert.getAff? cert p1 = some xin) (hgv : CertSoundness.getVal? vals p1 = some vp) : CrownCertSoundness.EnclosesAtInput ctx x xin vp

The unique parent of a unary node is enclosed whenever its certificate entry and semantic value are both found by the safe lookups.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.evalNode?_eq_some_of_semLocalOK {g : Graph} {ps : ParamStore ℝ} {inputs : Std.HashMap ℕ CertSoundness.Val} {vals : Array (Option CertSoundness.Val)} {id : ℕ} {v : CertSoundness.Val} (hsem : CertSoundness.SemLocalOK g ps inputs vals) (hid : id < g.nodes.size) (hv : vals[id]! = some v) : CertSoundness.evalNode? g.nodes ps inputs vals id = some v

Under SemLocalOK, a present semantic value at id is the evaluator's output.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.sem_encloses_transport {B1 B2 : FlatBox ℝ} (h : B1 = B2) {x : TorchLean.Tensor ℝ [B1.dim]} {y : TorchLean.Tensor ℝ [B2.dim]} (hxy : x ≍ y) (hx : Theorems.Semantics.encloses B1 x) : Theorems.Semantics.encloses B2 y

Transport an enclosure along an equality of boxes and a heterogeneous equality of values.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.encloses_point_box {n : ℕ} (t : TorchLean.Tensor ℝ [n]) : Theorems.Semantics.encloses { dim := n, lo := t, hi := t } t

A point box encloses its own point.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.enclosesAtInput_congr_val {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {b : FlatAffineBounds ℝ} {v w : CertSoundness.Val} (h : v = w) (hv : CrownCertSoundness.EnclosesAtInput ctx x b v) : CrownCertSoundness.EnclosesAtInput ctx x b w

EnclosesAtInput respects equality of value payloads.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.enclosesAtInput_boundsConst_of_enclosesBox {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {B0 : FlatBox ℝ} {v : CertSoundness.Val} (hEnc : CertSoundness.EnclosesBox B0 v) : CrownCertSoundness.EnclosesAtInput ctx x (Cert.boundsConst ctx.inputDim B0.dim B0.lo B0.hi) v

A constant affine enclosure built from a box B0 is sound at every input point whenever B0 encloses the value.

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.Alpha.encloses_castOut_of_enclosesAtInput {ctx : AffineCtx} {x : TorchLean.Tensor ℝ [ctx.inputDim]} {xin : FlatAffineBounds ℝ} {vp : CertSoundness.Val} {n : ℕ} (hout : xin.outDim = n) (hvn : vp.n = n) (hinDim : xin.inDim = ctx.inputDim) (hpar : CrownCertSoundness.EnclosesAtInput ctx x xin vp) : Theorems.Semantics.encloses { dim := n, lo := CrownCertSoundness.affineEvalAt (castAffineOut hout xin.loAff) (castDimScalar ⋯ x), hi := CrownCertSoundness.affineEvalAt (castAffineOut hout xin.hiAff) (castDimScalar ⋯ x) } (castDimScalar hvn vp.v)

Casting the output dimension of enclosing affine bounds yields a box, evaluated at the input point, that encloses the correspondingly cast value. This is the componentwise form of enclosesAtInput_castOut used by the linear and ReLU cases.