Certificate theorem examples

Most files in this directory are runnable checkers: they parse an artifact, recompute the relevant bounds, and reject the artifact if it disagrees with Lean. This file shows the complementary theorem-backed layer. The public theorems below are the bridge from “the checker accepted this certificate” to “the represented graph semantics is enclosed.”

The split is deliberate:

• executable examples are fast, concrete, and good for interoperability with JSON artifacts;
• theorem-backed results explain what those checks mean mathematically once their hypotheses are discharged for a supported graph and certificate format.

In other words, a JSON checker answers "does this artifact match Lean recomputation?" The theorem handles below answer the stronger question: "assuming the local checker hypotheses, what semantic fact follows?"

Theorem handles

These aliases keep the important public theorem names visible in generated docs and catch namespace/API mismatches during builds.

@[reducible, inline]

noncomputable abbrev NN.Verification.ProofBackedCertificates.ibpCertificateSoundness (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore ℝ) (cert : Array (Option (MLTheory.CROWN.FlatBox ℝ))) (inputs : Std.HashMap ℕ MLTheory.CROWN.Graph.CertSoundness.Val) (vals : Array (Option MLTheory.CROWN.Graph.CertSoundness.Val)) (htopo : MLTheory.CROWN.Graph.CertSoundness.TopoSorted g) (hsupp : MLTheory.CROWN.Graph.CertSoundness.Supported g) (hcert : MLTheory.CROWN.Graph.CertSoundness.CertLocalOK g ps cert) (hsem : MLTheory.CROWN.Graph.CertSoundness.SemLocalOK g ps inputs vals) (hinputs : MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed g ps inputs) (id : ℕ) : id < g.nodes.size → match cert[id]!, vals[id]! with | some B, some v => MLTheory.CROWN.Graph.CertSoundness.EnclosesBox B v | x, x_1 => True

Local IBP certificate soundness: locally valid boxes enclose graph semantics.

@[reducible, inline]

noncomputable abbrev NN.Verification.ProofBackedCertificates.runIBPSoundness (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore ℝ) (inputs : Std.HashMap ℕ MLTheory.CROWN.Graph.CertSoundness.Val) (htopo : MLTheory.CROWN.Graph.CertSoundness.TopoSorted g) (hsupp : MLTheory.CROWN.Graph.CertSoundness.Supported g) (hinputs : MLTheory.CROWN.Graph.CertSoundness.InputsEnclosed g ps inputs) (id : ℕ) : id < g.nodes.size → match (MLTheory.CROWN.Graph.CertSoundness.runIBP? g ps)[id]!, (MLTheory.CROWN.Graph.CertSoundness.evalGraphRec g ps inputs)[id]! with | some B, some v => MLTheory.CROWN.Graph.CertSoundness.EnclosesBox B v | x, x_1 => True

Concrete Lean runIBP? soundness against the recursive graph evaluator.

@[reducible, inline]

noncomputable abbrev NN.Verification.ProofBackedCertificates.crownCertificateSoundness (g : MLTheory.CROWN.Graph) (ps : MLTheory.CROWN.Graph.ParamStore ℝ) (step : Array (Option (MLTheory.CROWN.Graph.FlatAffineBounds ℝ)) → ℕ → Option (MLTheory.CROWN.Graph.FlatAffineBounds ℝ)) (cert : Array (Option (MLTheory.CROWN.Graph.FlatAffineBounds ℝ))) (inputs : Std.HashMap ℕ MLTheory.CROWN.Graph.CrownCertSoundness.Val) (vals : Array (Option MLTheory.CROWN.Graph.CrownCertSoundness.Val)) (ctx : MLTheory.CROWN.Graph.AffineCtx) (x : Spec.Tensor ℝ (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar)) (htopo : MLTheory.CROWN.Graph.CrownCertSoundness.TopoSorted g) (_hsem : MLTheory.CROWN.Graph.CrownCertSoundness.SemLocalOK g ps inputs vals) (hcert : MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK g step cert) (hsound : MLTheory.CROWN.Graph.CrownCertSoundness.CrownTransferSound g ps inputs vals ctx x step cert) (id : ℕ) : id < g.nodes.size → match cert[id]!, vals[id]! with | some b, some v => MLTheory.CROWN.Graph.CrownCertSoundness.EnclosesAtInput ctx x b v | x, x_1 => True

Generic affine CROWN-family checker soundness over real semantics.

@[reducible, inline]

noncomputable abbrev NN.Verification.ProofBackedCertificates.crownCertificateSoundnessIEEE32 (g : MLTheory.CROWN.Graph) (_ps : MLTheory.CROWN.Graph.ParamStore TorchLean.Floats.IEEE754.IEEE32Exec) (step : Array (Option (MLTheory.CROWN.Graph.FlatAffineBounds TorchLean.Floats.IEEE754.IEEE32Exec)) → ℕ → Option (MLTheory.CROWN.Graph.FlatAffineBounds TorchLean.Floats.IEEE754.IEEE32Exec)) (cert : Array (Option (MLTheory.CROWN.Graph.FlatAffineBounds TorchLean.Floats.IEEE754.IEEE32Exec))) (_inputs : Std.HashMap ℕ (MLTheory.CROWN.Graph.FlatVec TorchLean.Floats.IEEE754.IEEE32Exec)) (vals : Array (Option (MLTheory.CROWN.Graph.FlatVec TorchLean.Floats.IEEE754.IEEE32Exec))) (ctx : MLTheory.CROWN.Graph.AffineCtx) (x : Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec (Spec.Shape.dim ctx.inputDim Spec.Shape.scalar)) [Preorder TorchLean.Floats.IEEE754.IEEE32Exec] (htopo : MLTheory.CROWN.Graph.CrownCertSoundness.TopoSorted g) (_hsem : vals.size = g.nodes.size ∧ ∀ id < g.nodes.size, vals[id]! = vals[id]!) (hcert : MLTheory.CROWN.Graph.CrownCertSoundness.CrownCertLocalOK g step cert) (hsound : ∀ id < g.nodes.size, (∀ p ∈ g.nodes[id]!.parents, match cert[p]!, vals[p]! with | some bp, some vp => MLTheory.CROWN.Graph.CrownCertSoundness.EnclosesAtInput ctx x bp vp | x, x_1 => True) → match step cert id, vals[id]! with | some b, some v => MLTheory.CROWN.Graph.CrownCertSoundness.EnclosesAtInput ctx x b v | x, x_1 => True) (id : ℕ) : id < g.nodes.size → match cert[id]!, vals[id]! with | some b, some v => MLTheory.CROWN.Graph.CrownCertSoundness.EnclosesAtInput ctx x b v | x, x_1 => True

Schematic IEEE32Exec version used when the local transfer rule is supplied for floats.