α/β-CROWN step function: case inversion

Lemmas that read off what stepAlphaBeta computed at a node.

Away from ReLU nodes that carry a β vector, stepAlphaBeta is stepAlpha. On a ReLU node with a β vector, the step succeeds only when the unary parent has a certificate entry and an IBP box of the same output dimension, and phaseRelaxVec? accepts the phases against that box. The inversion lemma stepAlphaBeta_relu_beta_inv exposes exactly those ingredients, together with the range of the α vector actually used (explicit or default).

Safe lookups

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.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 Cert.getAff? lookup is an in-bounds array read.

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.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 getAlpha? lookup is an in-bounds array read.

α vector range

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.getAlpha?_unit_range {alpha : Array (Option (FlatTensor ℝ))} {id : ℕ} {αv : FlatTensor ℝ} (halpha : AlphaOK alpha) (h : Cert.getAlpha? alpha id = some αv) (i : Fin αv.n) : 0 ≤ αv.v.getScalar i ∧ αv.v.getScalar i ≤ 1

Under AlphaOK, an α vector read by getAlpha? has every entry in [0, 1].

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.castDimScalar_unit_range {n n' : ℕ} (h : n = n') (t : TorchLean.Tensor ℝ [n]) (hr : ∀ (i : Fin n), 0 ≤ t.getScalar i ∧ t.getScalar i ≤ 1) (i : Fin n') : 0 ≤ (castDimScalar h t).getScalar i ∧ (castDimScalar h t).getScalar i ≤ 1

Casting the dimension of a tensor preserves the unit-interval range of its entries.

Reduction to α-CROWN

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.stepAlphaBeta_eq_stepAlpha (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (beta : Array (Option (Array ℤ))) (cert : Array (Option (FlatAffineBounds ℝ))) (ctx : AffineCtx) (id : ℕ) (hnb : g.nodes[id]!.kind = IR.OpKind.relu → Cert.getBeta? beta id = none) : stepAlphaBeta g ps ibp alpha beta ctx cert id = stepAlpha g ps ibp alpha ctx cert id

stepAlphaBeta is stepAlpha at every node that is not a ReLU carrying a β vector.

The hypothesis is phrased as an implication so that a single lemma covers both the non-ReLU kinds and ReLU nodes with no β entry.

Inversion of the β-phase ReLU branch

theorem NN.MLTheory.CROWN.Graph.AlphaCrownTransferSoundness.stepAlphaBeta_relu_beta_inv (g : Graph) (ps : ParamStore ℝ) (ibp : Array (Option (FlatBox ℝ))) (alpha : Array (Option (FlatTensor ℝ))) (beta : Array (Option (Array ℤ))) (cert : Array (Option (FlatAffineBounds ℝ))) (ctx : AffineCtx) (id : ℕ) (b : FlatAffineBounds ℝ) (phases : Array ℤ) (p1 : ℕ) (halpha : AlphaOK alpha) (hk : g.nodes[id]!.kind = IR.OpKind.relu) (hbeta : Cert.getBeta? beta id = some phases) (hps : IR.unaryParent? g.nodes[id]!.parents = some p1) (hs : stepAlphaBeta g ps ibp alpha beta ctx cert id = some b) : ∃ (xin : FlatAffineBounds ℝ) (preB : FlatBox ℝ) (hout : xin.outDim = preB.dim) (αt : TorchLean.Tensor ℝ [preB.dim]) (relaxLo : TorchLean.Tensor (Runtime.Ops.ReLURelax ℝ) [preB.dim]) (relaxHi : TorchLean.Tensor (Runtime.Ops.ReLURelax ℝ) [preB.dim]), Cert.getAff? cert p1 = some xin ∧ ibp[p1]! = some preB ∧ (∀ (i : Fin preB.dim), 0 ≤ αt.getScalar i ∧ αt.getScalar i ≤ 1) ∧ Cert.phaseRelaxVec? preB.lo preB.hi αt phases = some (relaxLo, relaxHi) ∧ b = { inDim := xin.inDim, outDim := preB.dim, loAff := Runtime.Ops.ReLU.propagateAffine relaxLo (castAffineOut hout xin.loAff), hiAff := Runtime.Ops.ReLU.propagateAffine relaxHi (castAffineOut hout xin.hiAff) }

What a successful α/β step on a ReLU node with a β vector must have computed.

The parent p1 has a certificate entry xin and an IBP box preB of matching output dimension, phaseRelaxVec? accepted phases against preB for some α vector αt with entries in [0, 1] (the explicit one, cast to preB.dim, or the default one), and the produced bounds are the phase relaxations propagated through the parent's affine bounds.