Spec → math (the verification tie), Rung 1: the linear classifier #
The shape #guard beside resnet34Verified in VerifiedNets.lean only checks the
parameter interface
(typechecking). This file is the first rung of connecting a readable VerifiedNetSpec
to the actual math — the proven VJP — on the simplest net, the Chapter-1 linear
classifier (dense 784→10).
The pattern (extends to MLP → conv nets, each rigid/per-net):
denotemaps the spec's layers to the Mathlib math function the proofs are about;- a
rfllemma ties the spec's denotation to that named function (mnistLinear); - the whole-model VJP theorem is stated about the spec's denotation and discharged
by the audited op-level VJP (
dense_has_vjp).
If the spec's layers drifts from [.dense 784 10], step 2/3 stop reducing and the
proofs fail to typecheck — so the readable architecture is provably the verified one,
at the math level, not just the shape level.
Math denotation of the linear spec. The Chapter-1 model is a single dense layer, so
[.dense 784 10] denotes to the Mathlib dense W b. Any other layer list is not the
linear model (0), which makes the tie below drift-sensitive.
Equations
- denoteLinear [VLayer.dense 784 10] W b = Proofs.dense W b
- denoteLinear layers W b = fun (x : Proofs.Vec 784) => 0
Instances For
Spec ≡ the proven model. linearVerified's denotation is exactly mnistLinear
(the function the Chapter-1 VJP capstone is about) — by rfl, so it's checked by the
kernel and breaks if linearVerified.layers changes.
The spec carries the math. The linear spec's denotation has the proven VJP —
discharged by the audited dense_has_vjp. This is the whole-model verification
stated about the readable layer list, not a hand-written function.
Equations
Instances For
…and its correctness headline carries over verbatim (the backward is the
pdiv-contracted Jacobian of the spec's denotation).
Rung 2: the MLP — the first genuine vjp_comp 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 vjp_comp_at down that chain (mlp_has_vjp_at). So this is where the spec→math
tie first exercises the chain rule, not just a single op.
Math denotation of the MLP spec: the 5-layer list denotes to mlpForward.
Equations
- denoteMLP [VLayer.dense 784 512, VLayer.relu, VLayer.dense 512 512, VLayer.relu, VLayer.dense 512 10] W₀ b₀ W₁ b₁ W₂ b₂ = Proofs.mlpForward W₀ b₀ W₁ b₁ W₂ b₂
- denoteMLP layers W₀ b₀ W₁ b₁ W₂ b₂ = fun (x : Proofs.Vec 784) => 0
Instances For
Spec ≡ the proven model. mlpVerified's denotation is exactly mlpForward
(dense ∘ relu ∘ dense ∘ relu ∘ dense) — by rfl, drift-sensitive.
The spec carries the math (canonical witness). The MLP spec's denotation has a
VJP — the global pdiv-derived witness (mlp_has_vjp; relu uses the framework
subgradient convention at the kinks, per Proofs/README.md).
Equations
- mlpVerified_has_vjp W₀ b₀ W₁ b₁ W₂ b₂ = Proofs.mlp_has_vjp W₀ b₀ W₁ b₁ W₂ b₂
Instances For
The spec carries the math (the real fold). At a smooth input — the two ReLU
pre-activations avoid zero — the MLP spec's denotation has a VJP built by folding
vjp_comp_at through dense → relu → dense → relu → dense (no rfl escape at the
kinks). This is the chain rule applied to the spec, the step linear couldn't show.
Equations
- mlpVerified_has_vjp_at W₀ b₀ W₁ b₁ W₂ b₂ x h0 h1 = Proofs.mlp_has_vjp_at W₀ b₀ W₁ b₁ W₂ b₂ x h0 h1
Instances For
…correctness headline for the canonical witness carries over to the spec.
Rung 3: the CNN — the fold now runs through conv + maxpool #
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 vjp_comp_at through conv/maxpool/dense) is the audited
mnistCnnNoBn_has_vjp_at, conditional on the four ReLU kinks + the maxpool being smooth at
the input. Here we headline the unconditional canonical witness (mlp_has_vjp style); the
spec is exactly the subject of that conditional fold via cnnVerified_denote_eq.
Math denotation of the CNN spec: the 11-layer list denotes to mnistCnnNoBnForward
(c=32, h=w=14, the Chapter-3 MNIST CNN).
Equations
- One or more equations did not get rendered due to their size.
- denoteCNN layers W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ = fun (x : Proofs.Vec 784) => 0
Instances For
Spec ≡ the proven model. cnnVerified's denotation is exactly mnistCnnNoBnForward
— the function the Chapter-3 fold mnistCnnNoBn_has_vjp_at is about — by rfl.
The spec carries the math. The CNN spec's denotation (conv→relu→conv→relu→maxpool
→dense→…) has a VJP — the canonical pdiv-derived witness. The conditional chain-rule
fold through conv/maxpool is the audited mnistCnnNoBn_has_vjp_at.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rung E (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.
Generated forward MLIR ↔ spec. The forward graph (rendered to linear_fwd.mlir,
the eval path) denotes the spec's forward function.
Generated train-step cotangent ↔ spec. The loss-cotangent graph (in
linear_train_step.mlir) denotes ∂(softmax-CE)/∂logits at the spec's logits.
Rung E (MLP): the spec ↔ the generated MLIR — both forward and backward #
The MLP has faithfulness for the whole forward graph (mlpFwdGraph_faithful) AND the whole
backward input-VJP graph (mlpBackGraph_faithful). Composed with denoteMLP = mlpForward
and mlpVerified_has_vjp_at = mlp_has_vjp_at, both halves of the generated train step are
tied to the spec: the rendered forward computes the spec's forward, and the rendered
backward computes the spec's VJP backward (at a smooth input).
Generated MLP forward MLIR ↔ spec. The forward graph (→ mlp_fwd.mlir) denotes
the spec's forward function.
Generated MLP backward MLIR ↔ spec. The backward input-VJP graph (in
mlp_train_step.mlir) denotes the spec's VJP backward (mlpVerified_has_vjp_at), at a
smooth input (the two ReLU pre-activations avoid zero).
Rung E (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 mnistCnnNoBn_has_vjp_at.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 (matching
cnnVerified_has_vjp, the canonical witness).
Generated CNN forward MLIR ↔ spec. The forward graph (→ cnn_fwd.mlir) denotes
the spec's forward (mnistCnnNoBnForward, c=32 / h=w=14).
Rung 4 + E (CIFAR, both variants): completing the ch5 ladder #
The two CIFAR-10 nets (ic=3, c1=32, c2=64, h=w=8 — spatial 32→16→8). Each gets the
spec→math denotation (= cifarCnnForward / cifarCnnBnForward by rfl), the canonical
witness VJP, and the forward spec→generated-MLIR tie (cifarFwdGraph_faithful /
cifarBnFwdGraph_faithful). The conditional folds are cifarCnn_has_vjp_at /
cifarCnnBn_has_vjp_at (six ReLU kinks + two maxpools; BN adds 0 < εᵢ). The BN here is
the SCALAR bnForward (one γ/β over c·h·w), the same op ViT's LayerNorm witness reduces to.
Equations
- One or more equations did not get rendered due to their size.
- denoteCifar layers W₁ b₁ W₂ b₂ W₃ b₃ W₄ b₄ W₅ b₅ W₆ b₆ W₇ b₇ = fun (x : Proofs.Vec 3072) => 0
Instances For
The (no-BN) CIFAR spec carries the math.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Generated (no-BN) CIFAR forward MLIR ↔ spec.
Equations
- One or more equations did not get rendered due to their size.
- denoteCifarBn layers W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ W₃ b₃ ε₃ γ₃ β₃ W₄ b₄ ε₄ γ₄ β₄ W₅ b₅ W₆ b₆ W₇ b₇ = fun (x : Proofs.Vec 3072) => 0
Instances For
The (per-channel-BN) CIFAR spec carries the math.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Generated (per-channel-BN) CIFAR forward MLIR ↔ spec. (epsStr = the rendered ε text;
the denotation uses the real εᵢ, so it holds for any string.)
Rung B/C (ch7 MobileNetV2, representative): the strided 6-block witness #
Representative tie, like the other imagenette nets below: denoteMobilenet maps
mobilenetv2RepLayers — the 10-entry strided 6-block layer list (stem-s2 → 6
inverted-residual blocks [16→64→24, 24→96→24, 24→96→32, 32→128→32, 32→128→64, 64→256→64] with 4 stride-2 depthwise downsamples 224→7 and 2 stride-1 skips → 1×1
conv-bn-relu6 head → GAP → dense) — to mobilenetv2Forward_full, the faithful 6-block
composition built in Proofs/MobileNetV2.lean from the strided inverted-residual VJP
infrastructure (invresBodyStrided, flatConvStride2Xla, depthwiseStride2FlatXla). The
rfl tie is drift-sensitive: change any block's [t,c,n,s] and the match stops reducing.
History note: this rung used to tie mobilenetv2Verified.layers itself — true while
the committed spec WAS the 6-block net. The spec was promoted to the full-paper 17-block
net (e9cd890), so this rung is now representative; the committed spec's full tie is the
next section (denoteMobilenetPaper → mobilenetv2ForwardPaper).
The honest chain-rule fold is carried by the new strided inverted-residual block witness
Proofs.invresBodyStrided_has_vjp_at (expand-SAME → stride-2 depthwise → project-SAME,
the downsampling block the render uses) composed with the representative inverted-residual
fold Proofs.mobilenetv2_has_vjp_at; here the rung-C headline is the unconditional
canonical witness, matching the ch4/ch5 conv nets (cnnVerified_has_vjp /
cifarVerified_has_vjp).
Stated gap (intrinsic, shared with ch5-BN / every BN net here): the proof's bnForward
is SCALAR-global (one γ/β over the whole c·h·w map per example); the render uses
per-channel [c] BN. Topology, channel flow, stride schedule, relu6 sites and residual
placement are all faithful — only BN granularity differs.
The representative MobileNetV2 layer list: the strided 6-block net that
mobilenetv2Forward_full actually renders and proves. A prefix-shaped slice of the
committed full-paper mobilenetv2Verified spec (17 blocks, 210 tensors), whose full
tie is the next section (denoteMobilenetPaper).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Math denotation of the representative MobileNetV2 spec: the 10-entry strided 6-block
layer list denotes to mobilenetv2Forward_full. Any other list is not the net (0),
making the tie below drift-sensitive.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Spec ≡ the representative proven render. mobilenetv2RepLayers's denotation is
exactly mobilenetv2Forward_full (the strided 6-block net) — by rfl, drift-sensitive.
The representative spec carries the math. The strided 6-block MobileNetV2 spec's
denotation has a VJP, the canonical pdiv-derived witness.
The honest strided chain-rule fold is mobilenetv2_full_has_vjp_at
(MobileNetV2FullVJP.lean), which folds stem + all seventeen bottlenecks + head over
the paper [t,c,n,s] table. ⚠ Read it, not mobilenetv2_has_vjp_at, which is the
representative-depth fold: stem + two inverted-residual blocks + head.
▶ It did not close by copying EfficientNet's, and that is the trap worth naming here
rather than rediscovering. efficientnetForwardB_full_has_vjp is a GLOBAL HasVJP over
all sixteen MBConv blocks, and it can be global because swish is smooth everywhere.
MobileNetV2 is relu6, and a global VJP through a kink is false, so the full-depth version
keeps the pointwise _at form this net already had: the axis that moved is DEPTH
(2 → 17), not pointwise → global. Anyone who conflates the two will spend the day proving
something untrue.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rung B/C/E (ch7 MobileNetV2, FULL): the committed spec ↔ the paper-spec net #
The real thing: denoteMobilenetPaper 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 mobilenetv2ForwardPaper
(MobileNetV2FullPaper.lean: per-channel BN throughout, the t=1 no-expand first block,
4 stride-2 depthwise downsamples 224→7). Weights ride in the MNV2PaperWeights bundle,
so the tie stays readable. The rfl is drift-sensitive: any [t,c,n,s] edit to the spec
stops the match reducing — exactly the tripwire the 6→17-block promotion fired while this
file was orphaned; certs.yml now re-elaborates it on every spec push.
This restores (and upgrades) the full mnv2 B/C lost in the promotion: the old full tie was
the scalar-BN 6-block net; this one is the committed per-channel-BN 17-block net, with
rung E on top (mobilenetv2FwdGraphPaper_faithful composed with the tie).
Math denotation of the committed MobileNetV2 spec: the 21-entry full-paper layer list
denotes to mobilenetv2ForwardPaper. Any other list is not the net (0), making the
tie below drift-sensitive.
Equations
- One or more equations did not get rendered due to their size.
- denoteMobilenetPaper layers w = fun (x : Proofs.Vec (3 * 224 * 224)) => 0
Instances For
Spec ≡ the full paper-spec net. The committed mobilenetv2Verified's denotation
is exactly mobilenetv2ForwardPaper (all 17 bottlenecks, per-channel BN) — by rfl,
drift-sensitive.
The committed spec carries the math. The full-paper spec's denotation has a VJP —
the canonical pdiv-derived witness (relu6 is kinked, so the honest whole-net
input-VJP stays pointwise-only, the repo standard for relu-family nets; the
dim-polymorphic MobileNetV2Close/ChainClose param-grad bridges apply at the paper
shapes verbatim, per MobileNetV2FullPaper.lean's header).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rung E at the committed spec. The generated full-paper StableHLO graph denotes the
committed spec's function: mobilenetv2FwdGraphPaper_faithful composed with the tie.
Rung B/C/E (FULL, unified weight bundles): r34 / enet / convnext / vit #
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); r34 and vit get bundles here (R34Weights, ViTTinyWeights —
SpecVJP-local so no proof module's signature changes). Rung E composes each net's
full graph-faithfulness apex with the tie (vit's is vitFwdGraphKMHV_faithful,
ViTDepthK §3 — the depth-k multi-head vector-LN graph). Rung C is the canonical
witness except vit: all-smooth, so vit's rung C is the REAL whole-net VJP
vitForwardKV_has_vjp (only 0 < ε) at the committed spec.
Identity basic-block weights (conv-BN ×2), per-channel γ/β.
- W1 : Proofs.Kernel4 c c 3 3
- b1 : Proofs.Vec c
- g1 : Proofs.Vec c
- t1 : Proofs.Vec c
- W2 : Proofs.Kernel4 c c 3 3
- b2 : Proofs.Vec c
- g2 : Proofs.Vec c
- t2 : Proofs.Vec c
Instances For
Downsample basic-block weights (strided conv-BN ×2 + projection conv-BN).
kHp kWp is the projection kernel: 3×3 as this repo renders it, 1×1 in He et al.'s
option-B shortcut (§2k/§2l). R34Weights below is the single place that picks it.
- W1 : Proofs.Kernel4 oc ic 3 3
- b1 : Proofs.Vec oc
- g1 : Proofs.Vec oc
- t1 : Proofs.Vec oc
- W2 : Proofs.Kernel4 oc oc 3 3
- b2 : Proofs.Vec oc
- g2 : Proofs.Vec oc
- t2 : Proofs.Vec oc
- Wp : Proofs.Kernel4 oc ic kHp kWp
- bp : Proofs.Vec oc
- gp : Proofs.Vec oc
- tp : Proofs.Vec oc
Instances For
All ResNet-34 parameters (shared BN ε): stem + [3,4,6,3] basic blocks + dense.
- ε : ℝ
- sW : Proofs.Kernel4 64 3 7 7
- sb : Proofs.Vec 64
- sγ : Proofs.Vec 64
- sβ : Proofs.Vec 64
- a0 : R34BlockW 64
- a1 : R34BlockW 64
- a2 : R34BlockW 64
- d2 : R34DownW 64 128 1 1
- b0 : R34BlockW 128
- b1 : R34BlockW 128
- b2 : R34BlockW 128
- d3 : R34DownW 128 256 1 1
- c0 : R34BlockW 256
- c1 : R34BlockW 256
- c2 : R34BlockW 256
- c3 : R34BlockW 256
- c4 : R34BlockW 256
- d4 : R34DownW 256 512 1 1
- e0 : R34BlockW 512
- e1 : R34BlockW 512
- Wd : Proofs.Mat 512 10
- bd : Proofs.Vec 10
Instances For
resnet34Forward_full_pc at the bundle (the 145-arg field expansion, once).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Math denotation of the committed ResNet-34 spec: the 8-entry stage-level layer list
denotes to the full per-channel [3,4,6,3] render. Any other list is not the net (0).
Equations
- One or more equations did not get rendered due to their size.
- denoteR34Full layers w = fun (x : Proofs.Vec (3 * 224 * 224)) => 0
Instances For
Spec ≡ the full proven render. resnet34Verified's denotation is exactly
resnet34Forward_full_pc (per-channel BN, [3,4,6,3] at 224²) — by rfl.
The committed spec carries the math — canonical pdiv witness (relu is kinked,
so the honest whole-net input-VJP stays pointwise; the live/seal theorems
(ResNet34Live*) discharge nontriviality at full depth and realistic dims).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rung E at the committed spec. The full per-channel [3,4,6,3] graph denotes the
committed spec's function: resnet34FwdGraphFullPC_faithful composed with the tie.
Math denotation of the committed EfficientNet-B0 spec at batch N: the 21-entry
[t,c,n,s,k] layer list denotes to efficientnetForwardB_full (all 16 MBConv
blocks, true batch-norm + SE). The spec ties the batched net at EVERY batch size.
Equations
- One or more equations did not get rendered due to their size.
- denoteEfficientnetB0 N layers w = fun (x : Proofs.Vec (N * (3 * 224 * 224))) => 0
Instances For
Spec ≡ the full proven net. efficientnetVerified's denotation is exactly
efficientnetForwardB_full (16 MBConv, batched, per-channel BN + SE) — by rfl.
The committed spec carries the math — canonical pdiv witness (swish/SE are
smooth but relu6 clamps; the per-block differentiability lemmas live in
EfficientNetFullB0.lean).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rung E at the committed spec (batched). The full 16-MBConv batched graph denotes
the committed spec's function: efficientnetFwdGraphB_full_faithful ∘ the tie.
Math denotation of the committed ConvNeXt-T spec: the 29-entry [3,3,9,3] layer list
denotes to convNextForwardTCh — the channel-LayerNorm net (§2m), whose 23 LN sites
are 1 stem + 18 block + 3 downsample + 1 head, the first 22 reducing over the c channels
at one spatial position with a per-channel [c] affine and the head one over the [768] GAP
output (which is the same function at one spatial position — rowLNVecFlat 1 768).
⚠ The head LN was RESTORED 2026-08-30 (planning/archive/next_session_execution_and_parity.md §7.1).
§2m/§2n had deleted it to match the JAX reference, which was itself missing it against both
the paper and timm; the parameter count was short by exactly 2×768.
⚠ This used to match a .convNextBlock/.bn list and denote the SCALAR-LN net: one mean and
one variance over the whole c·h·w map, two scalars, and no stem LN but a head LN. §2n
deleted that chain outright, so the trap it guarded against — silently re-pointing this at the
scalar function, which would typecheck by rfl and assert that the channel-LN layer list
denotes the scalar-LN one (§2k's own sin, one level down) — is no longer expressible. Keeping
the note because the SHAPE of that mistake is what §2k was about, not the specific symbol.
Equations
- One or more equations did not get rendered due to their size.
- denoteConvnextT layers w = fun (x : Proofs.Vec (3 * 224 * 224)) => 0
Instances For
Spec ≡ the full proven net. convnextVerified's denotation is exactly
convNextForwardTCh ([3,3,9,3] @ [96,192,384,768], channel LN + head LN, 28,589,128 params at
K = 1000 — the JAX reference's own count) — by rfl.
The committed spec carries the math — canonical pdiv witness; the REAL
whole-net VJP exists at full depth (convNextForwardTCh_has_vjp_correct,
all-smooth, the 22 LN positivities only) on the ∘-chain form.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rung E at the committed spec. The committed-config [3,3,9,3] channel-LN graph denotes
the committed spec's function: convNextFwdGraphTCh_faithful ∘ the tie.
All ViT-Tiny parameters at the committed config (D=192, 3 heads, d_head=64,
mlpDim=768, 12 untied blocks, vector-LN): patch embed + CLS/pos + 12 per-block
BlockParamsV bundles + final LN + CLS head. Shared LN ε rides along.
- ε : ℝ
- Wc : Proofs.Kernel4 192 3 16 16
- bc : Proofs.Vec 192
- cls : Proofs.Vec 192
- pos : Proofs.Mat 197 192
- blocks : Fin 12 → Proofs.BlockParamsV 192 768
- γF : Proofs.Vec 192
- βF : Proofs.Vec 192
- Wcls : Proofs.Mat 192 10
- bcls : Proofs.Vec 10
Instances For
vitForwardKV at the committed ViT-Tiny config (depth 12, 3 heads × 64).
Equations
Instances For
Math denotation of the committed ViT-Tiny spec: the 17-entry layer list (12 untied
.transformerBlocks, per-channel [192] LN, 1D CLS) denotes to vitForwardTiny.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Spec ≡ the full proven net. vitVerified's denotation is exactly
vitForwardKV at the committed config (depth-12 DISTINCT-param multi-head,
per-token vector-LN — ViTDepthK.lean) — by rfl. Retires the rep tie's
weight-shared scalar-LN caveats at the spec level.
The committed spec carries the math — the REAL whole-net VJP. ViT is all-smooth
(GELU/softmax/LN), so unlike the conv nets the honest chain-rule fold applies
globally: vitForwardKV_has_vjp at the committed config, hypothesis 0 < ε only.
The strongest rung C in this file — no canonical-witness fallback needed.
Equations
Instances For
Rung E at the committed spec. The depth-12 3-head vector-LN forward graph
(vitFwdGraphKMHV, ViTDepthK §3 — patch embed → 12 spelled multi-head blocks →
final vector-LN → CLS → head) denotes the committed spec's function:
vitFwdGraphKMHV_faithful composed with the tie. Completes the B/C/E ladder for
all five imagenette nets.
Rung B/C (representative): the imagenette nets' proof witnesses #
Every committed imagenette spec is now tied in FULL above (mnv2 denoteMobilenetPaper,
r34 denoteR34Full, enet denoteEfficientnetB0, convnext denoteConvnextT, vit
denoteVitTiny). The representative rungs below remain as the smaller readable
skeletons the ORIGINAL per-net proof witnesses actually state (<net>Forward + the
audited <net>_has_vjp apex), tied to generic-dim VLayer lists exactly like ch2–5:
denote <rep layers> = <net>Forward := rfl (rung B) + canonical HasVJP witness
(rung C; the honest fold is the apex).
Math denotation of the representative EfficientNet layer list → efficientnetForward.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Spec ≡ the representative proven model.
The representative spec carries the math (canonical witness; the honest
unconditional fold is Proofs.efficientnet_has_vjp).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Math denotation of the representative ConvNeXt layer list → convNextForward.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Spec ≡ the representative proven model.
The representative spec carries the math (canonical witness; the honest
unconditional fold is Proofs.convnext_has_vjp).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Math denotation of the representative ViT layer list → vit_full. The single
.transformerBlock VLayer stands for the kBlocks-deep weight-shared vit_body;
per the proof witness the LayerNorm is scalar (layerNormForward = bnForward), so this
ties the spec to the scalar-LN witness, not the rendered per-channel [D] LN.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Spec ≡ the representative proven model.
The representative spec carries the math (canonical witness; the honest
unconditional fold is Proofs.vit_full_has_vjp).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Math denotation of the representative ResNet-34 layer list → the skeleton composition
dense ∘ gap ∘ chainComp ids4 ∘ down4 ∘ … ∘ chainComp ids1 ∘ mp ∘ stem that the audited
parametric apex resnet34_has_vjp_at is about. r34 has no concrete whole-net Forward
(only this abstract [3,4,6,3]-stage skeleton over abstract block maps); the full faithful
forward at real Imagenette dims is the deferred build.
Equations
- One or more equations did not get rendered due to their size.
- denoteR34Rep layers stem mp ids1 down2 ids2 down3 ids3 down4 ids4 gap dense = fun (x : Proofs.Vec s0) => 0
Instances For
Spec ≡ the representative proven skeleton.
The representative spec carries the math (canonical witness; the honest conditional
fold through the [3,4,6,3] stages is Proofs.resnet34_has_vjp_at).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rung E (ch7 mnv2, representative): the spec's math ↔ the generated MLIR #
The forward graph mobilenetv2FwdGraphFull (StableHLO) — the strided 6-block render —
denotes the representative spec's forward: den graph = mobilenetv2Forward_full
(mobilenetv2FwdGraphFull_faithful) composed with mobilenetv2Rep_denote_eq gives
den graph = denoteMobilenet mobilenetv2RepLayers. So the generated StableHLO provably
computes the representative spec's function — the A+B+C+E ladder at the 6-block witness
(the committed 17-block spec's E rung is mobilenetv2Verified_fwd_faithful, above). E is
simp-based, so it does NOT hit the
VJP-fold's concrete-dim isDefEq wall. (Forward only; the backward graph + the .mlir re-route
off the committed tests/Test* string emitter are the remaining E work — see planning doc.)
Rung E (ch9 convnext, representative): the spec's math ↔ the generated MLIR #
The representative forward graph convNextFwdGraph (StableHLO; patchify → LN → block×2 →
GAP → head-LN → dense, via geluF/layerScaleF/bnF/addV) denotes the representative
convNextForward (convNextFwdGraph_faithful), composed with convnextRep_denote_eq ⇒
den graph = denoteConvnextRep <rep layers>. So convnext has the representative A+B+C+E(fwd)
ladder. (Scalar LN; the full-render E is convnextVerified_fwd_faithful above.)