CertLayer — composing certified backward graphs, so a NET is one object #
A CertLayer is a layer that carries its own proof that its backward graph denotes its VJP, and
CertLayer.comp composes two of them into a third. Users: r34NetLayer / r50NetLayer
(ResNet-34/50, stem pool to logits), the MobileNetV2 bodies (mnv2BodyLayer,
mnv2DownBodyLayer), MobileNetV4's layer groups (its trunk is several CertLayers, not one),
the ConvNeXt channel-LN block (cnxBlockChLayer), and ViT's tower (ViTBackNet, which proves
the generic chain reproduces ViT's bespoke induction term for term). EfficientNet-B0's backward
chain does not use CertLayer; it is composed directly (EfficientNetChainClose). The head
layers shared across nets are in HeadLayers.
Why. Without it the chaining is open-coded. Look at any
<body>BackBatchedGraph_faithful: it builds G₁ x (G₂ (f₁ x) e), rewrites with the two component
faithfulness lemmas, and closes by rfl on vjpCompAt's definitional
backward dy = f₁.backward (f₂.backward dy). That argument is identical every time and is
re-typed per composition, so a 16-block net would be 16 copies of it with ever-larger terms.
This file does it once. CertLayer.comp is that proof; everything else is bookkeeping.
The structure #
A CertLayer m n is a forward map plus, at every input satisfying its own smoothness
precondition, a VJP, differentiability, a backward StableHLO graph, and the theorem that the
graph denotes the VJP. Carrying ok inside the layer is what makes composition work: relu nets
are _at, so a block is only certified where its pre-activations miss the kinks, and the composite
of two layers is certified exactly where the first is certified and the second is certified at
the first's output. That is ok x := L₁.ok x ∧ L₂.ok (L₁.fwd x), and it threads the deepening
hypothesis stack automatically instead of by hand.
This is not a new trust assumption. CertLayer.comp proves faithfulness of the composite
from the components' faithfulness; it introduces no axiom and no sorry. A chain built from
certified blocks is certified, and the fold is where that stops being a sentence and becomes a
theorem.
Reading the list order #
chain [L₁, L₂, L₃] runs L₁ first: fwd = L₃.fwd ∘ L₂.fwd ∘ L₁.fwd. List order is forward
execution order, which is how a block table reads. The backward graph nests the other way
automatically — L₁.graph x (L₂.graph _ (L₃.graph _ e)) — because that is what the chain rule
says, and getting it backwards is a silent wrong-gradient rather than a type error whenever the
widths happen to agree.
A layer whose backward StableHLO graph is proven to denote its VJP, wherever its own
smoothness precondition ok holds.
ok is a predicate on the INPUT because that is what relu smoothness is: a condition on the
activations this particular layer sees. A globally-smooth layer (swish, a bare conv-bn) sets
ok := fun _ => True and loses nothing.
The forward map.
Where this layer is certified — the smoothness hypotheses, as a predicate on the input.
- diff (x : Vec m) : self.ok x → DifferentiableAt ℝ self.fwd x
Differentiability at any certified point (needed to compose via
vjpCompAt). The proven VJP at any certified point.
The backward graph, as a function of the forward activation and the incoming cotangent.
- faithful (x : Vec m) (hx : self.ok x) (e : SHlo n) : den (self.graph x e) = (self.vjp x hx).backward (den e)
The theorem that makes it a certified layer: the graph denotes the VJP.
Instances For
A certified layer is determined by its forward, its certification domain and its backward
graph: vjp is pinned by fwd (HasVJPAt is a subsingleton), and diff, faithful are proofs.
The identity layer — certified everywhere, and its backward graph is the cotangent verbatim.
The unit of chain.
Equations
- One or more equations did not get rendered due to their size.
Instances For
THE COMPOSITION THEOREM — the whole point of this file.
Two certified layers compose into a certified layer. The backward graph nests (L₁'s graph
fed L₂'s graph at L₁'s output), the smoothness preconditions conjoin, and faithfulness
follows from the components' faithfulness plus vjpCompAt's definitional backward.
This is the argument every <body>BackBatchedGraph_faithful in the repo writes out by hand.
Proven once here, a chain of any length costs nothing.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Wrap a layer in an identity skip — x ↦ L.fwd x + x. The backward graph is the additive
fan-in addV (L.graph …) ecot: the body's input-cotangent plus the skip's verbatim cotangent.
Certified exactly where the body is (ok := L.ok), because an identity skip is smooth
everywhere and contributes no new condition. Every residual net in the repo hand-writes this
fan-in per block; here it is a combinator, so a residual block is residual (chain [...]).
Equations
- One or more equations did not get rendered due to their size.
Instances For
A projected residual — x ↦ P.fwd x + F.fwd x, both paths nontrivial. The backward
graph is the fan-in addV (P.graph …) (F.graph …), certified where both paths are. The
downsample-block peer of residual: a projection skip changes the width, so the layer is
m → n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The post-residual relu of a ResNet block, as a layer: certified where its input misses the
kink, with the %outR mask as its backward. (residual F).comp (reluOut _) is a whole identity
block, so its capstone is .faithful of that composite.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The net-level statement, in one line. Whatever the chain's length, its backward graph
denotes its VJP — so a stage, a trunk, or a whole net assembled from certified blocks is
certified, with no per-length proof. This is just CertLayer.faithful at chain Ls; it is
restated here because it is the theorem the fold exists to provide.
Projecting .fwd out of a composed CertLayer — the four lemmas below, and why they exist.
simp only [CertLayer.comp] rewrites L₁.comp L₂ to the full structure literal — fwd, ok,
diff, vjp, graph AND faithful — and only then projects .fwd out of it; over a 24-stage
chain that builds an enormous intermediate term whose bulk is proofs the goal never mentions
(on MobileNetV4's chain: minutes without these, seconds with them). And at literal widths the
peel itself is a kernel deterministic timeout by rfl / Function.comp_apply / Function.comp_assoc
— proved once here between variables, comp_fwd_apply is applied there in 2 s.
comp's ok, with the intermediate activation NAMED. A whole-net chain whose hypotheses are
stated at named prefixes proves its .ok one refine per block through this, so the goal
stays at the prefix; one anonymous constructor for the whole chain instead makes every
prefix a defeq check against the nested layer forwards, and that exceeds maxRecDepth by the
fifth block. Note: Discharge hy by rw at literal widths, not rfl (r34SmoothAtB_ok).