Spec → math: nine committed VerifiedNetSpecs denote their proven forwards #

The shape #guard beside resnet34Verified in Verified.NetsCore only checks the parameter interface (typechecking). This file ties nine committed specs' layer lists — the linear classifier, MLP, MNIST CNN, CIFAR CNN, and the 10-class Imagenette MobileNetV2, ResNet-34, EfficientNet-B0, ConvNeXt-T and ViT-Tiny — to the math the proofs are about. The other specs (the ImageNet ones, ResNet-50, MobileNetV4, the cifar8* family) are not tied here. Per net, up to three pieces:

1. a denotation denote* mapping the spec's layer list to the proven forward function, and a *_denote_eq lemma equating the two by rfl (drift-sensitive: any other layer list denotes 0, so editing the spec's layers breaks the rfl);
2. for the linear classifier, the MLP and ViT-Tiny, a VJP witness at the spec's denotation (linearVerifiedHasVJP is denseHasVJP, vitVerifiedHasVJP transports vitForwardKVHasVJP, and at a smooth input the MLP has the folded mlpVerifiedHasVJPAt). The other nets' whole-net VJPs are stated on their forwards (mnistCnnNoBnHasVJPAt, cifarCnnHasVJPAt, mobilenetv2ForwardBFullHasVJPAt, resnet34ForwardBFullHasVJPAt, efficientnetForwardBFullHasVJP, convNextForwardTChHasVJP), which *_denote_eq equates with the spec's denotation;
3. a *_fwd_faithful lemma composing the forward graph's faithfulness theorem with the tie, so the generated forward MLIR denotes the spec's function.

ConvNeXt-T's and ViT-Tiny's denotations take the form of the GELU (GeluForm) as an argument. A spec's layer list does not record it: like weight-decay exclusion, clipping or drop-path it is a property of the render variant, and the ties hold at either form.

The MLP — a vjpCompAt fold #

The linear model was the degenerate case (one layer, no fold). The MLP's denotation is a chain — dense ∘ relu ∘ dense ∘ relu ∘ dense (mlpForward) — and its VJP is built by folding vjpCompAt down that chain (mlpHasVJPAt). So this is where the spec→math tie first exercises the chain rule, not just a single op.

The MNIST CNN #

The CNN's denotation is mnistCnnNoBnForward — a flat Vec 784 → Vec 10 chain flatConv → relu → flatConv → relu → maxPoolFlat → dense → relu → dense → relu → dense. The honest chain-rule fold (via vjpCompAt through conv/maxpool/dense) is the audited mnistCnnNoBnHasVJPAt, conditional on its ReLU and max-pool smoothness hypotheses at the input. The witness below is the canonical one; the spec is the subject of that conditional fold via cnnVerified_denote_eq.

Linear: the spec ↔ the generated MLIR #

The ties above connect the spec to the math (denote = the proven forward, which has the proven VJP). This connects the spec to the StableHLO the trainer actually compiles and runs: the generated forward graph fwdGraph (→ verified_mlir/linear_fwd.mlir, the eval path) and the train-step loss-cotangent graph lossCotGraph (→ linear_train_step.mlir) denote the spec's forward and its softmax-CE gradient — via the audited faithfulness theorems (fwdGraph_faithful, lossCotGraph_isCEgrad) composed with denoteLinear = mnistLinear (rfl). So the generated code provably computes the spec's function.

What stays trusted (the codegen boundary, per Proofs/README.md): the text render linearFwdModuleV = pretty (emit fwdGraph) and that the committed .mlir equals that text — the pretty-printer + regeneration, NOT the semantics, which are proven here.

MLP: the spec ↔ the generated MLIR — both forward and backward #

The MLP has faithfulness for the whole forward graph (mlpFwdGraph_faithful, the graph mlp_fwd.mlir prints) AND for a whole backward input-VJP graph (mlpBackGraph_faithful). Composed with denoteMLP = mlpForward and mlpVerifiedHasVJPAt = mlpHasVJPAt, both denote the spec: the rendered forward computes the spec's forward, and mlpBackGraph computes the spec's VJP backward (at a smooth input). mlpBackGraph is a spec-level graph no committed artifact prints: mlp_train_step.mlir is MlpRender.lean's mlpTrainStepText, whose parameter ops MlpFold ties to the certified step.

MNIST CNN: the spec ↔ the generated MLIR (forward) #

The generated CNN forward graph (flatConv→relu→flatConv→relu→maxPoolFlat→dense→relu→ dense→relu→dense) denotes the spec's forward. The backward graph faithfulness exists too (cnnBackGraph_faithful denotes mnistCnnNoBnHasVJPAt.backward — the VJP of exactly this spec's forward), but it carries the same five ReLU/maxpool smoothness hypotheses as the conditional fold, so we headline the unconditional forward tie.

The CIFAR CNN (no BN) #

The CIFAR-10 net (ic=3, c1=32, c2=64, h=w=8 — spatial 32→16→8) gets the spec→math denotation (= cifarCnnForward by rfl), the canonical witness, and the forward spec→generated-MLIR tie (cifarFwdGraph_faithful). The conditional fold is cifarCnnHasVJPAt (ReLU and max-pool smoothness hypotheses at the input).

MobileNetV2 (full, batched): the committed spec ↔ the batch-BN net #

denoteMobilenetB maps mobilenetv2Verified.layers — the committed 21-entry full-paper [t,c,n,s] list the trainer runs (stem-s2 3→32 → 17 bottlenecks → 1×1 head 320→1280 → GAP → dense 1280→10) — to mobilenetv2ForwardBFull (MobileNetV2FullB.lean: batch BN throughout, the t=1 no-expand first block, 4 stride-2 depthwise downsamples 224→7), at every batch size. Weights ride in the MNV2BWeights bundle, so the tie stays readable. The rfl is drift-sensitive: any [t,c,n,s] edit to the spec stops the match reducing; certs.yml re-elaborates it on every spec push.

ResNet-34, EfficientNet-B0, ConvNeXt-T, ViT-Tiny (full, weight bundles) #

The mnv2 full-paper pattern applied to the remaining imagenette nets: each committed spec's ENTIRE layer list (literal dims, drift-sensitive) denotes the full proven forward, with weights riding a structure bundle so the ties stay readable. Existing bundles are reused where the Full module already has one (B0Weights, CnxTWeightsCh, R34BWeights); vit gets its bundle here (ViTTinyWeights, SpecVJP-local so no proof module's signature changes). Each *_fwd_faithful composes the net's full graph-faithfulness theorem with the tie (vit's is vitFwdGraphKMHV_faithful, the depth-k multi-head vector-LN graph of ViTDepthK). ViT alone gets a VJP witness at the spec: all-smooth, so it is the whole-net VJP vitForwardKVHasVJP (only 0 < ε).