The CIFAR-CNN (Chapter 4, no-BN) train step, proof-tied to the certified SGD step #

The Chapter-4 peer of CnnFold — a deeper, two-spatial-scale conv net ((conv→relu)×2 → pool → (conv→relu)×2 → pool → (dense→relu)×2 → dense; 14 params: 4 conv kernels/biases + 3 dense layers). MainCifarVerified trains on verified_mlir/cifar_train_step.mlir; this file states what its parameter updates denote: each emitted SGD op denotes θ − lr·(certified per-layer Jacobian · the cotangent the rendered chain feeds it) (cifar_train_step_tied_certified, all fourteen); only the output weight W₇ is tied to the whole-loss gradient (cifar_W7_tied_totalloss).

Zero new core ops. The conv layers reuse the convWeightSgd/convBiasSgd ops added for cnn (CnnFold); the dense head reuses weightSgd/biasSgd. The only new content is the per-net den = certified capstones below.

• Conv layers (all four): convW_den/convB_den are generic in the conv dims and the cotangent c — den (convWeightSgd … (.operand _ c)) = θ − lr·(certified ∂conv/∂θ · c), the emitted op's den reduced (rfl) to the LHS of the generic cnn_render_conv{W,b}_certified. Instantiated at each conv layer's (b,x,W) and the cotangent the renderer feeds there, they certify W₁/b₁ … W₄/b₄ (one lemma each, all four layers — conv2d's weight/bias VJP is dim-generic).
• Dense head (W₅/W₆/W₇): the classifier head is a 3-layer MLP over the flattened pool output, so its cotangents are the IR mlpCotOut0/1 and its dens close via weight_grad_bridge/bias_grad_bridge — verbatim CnnFold (dW7_den, the op the whole-loss fold rewrites with).

Scope (same boundary as cnn/mlp/linear) #

• Below the output layer the cotangents are the rendered chain (mlpCotOut1/mlpCotOut0 in the head; cnnChainCotW1, cnnChainCotW2, cifarChainCotW2 below it). The loss-gradient statement is cifar_net_lossGrad (CifarParamGrad), at the un-fused *Grad nodes these ops step by and with each pool's cotangent routed to one maximal cell, as the rendered select_and_scatter does; this chain's maxPoolBackDenote routes it to the first maximal cell (maxPool2Argmax), the op's own choice, so it is the capstone's chain at that selection (cifarChainCotW2_eq_sel, CnnFold.cnnChainCotW2_eq_sel).
• Per-op pretty lexing + ℝ → Float32.

Dense classifier head (W₅/W₆/W₇) — weightSgd/biasSgd, mirrors CnnFold #

The head pool2 → W₅→relu→W₆→relu→W₇ is a 3-layer MLP; per-layer cotangents are the IR mlpCotOut0/1 (with (W₇,W₆,W₅) playing the MLP's (W₂,W₁,W₀)). Every head op's den = certified is SgdNode.denseW_den / SgdNode.denseB_den at that layer, and cifar_train_step_tied_certified states all six at the real forward; the output-layer weight op is stated here on its own because the whole-loss fold cifar_W7_tied_totalloss rewrites with it.

The tie — the conv layers/dense head, tied through the REAL cifar forward #

The conv/dense *_den theorems above hold for a FREE cotangent (convW_den/convB_den are ∀ c; the dense head's mlpCotOut0/1 are ∀ dy). The capstones below pin those cotangents to the ones the real cifar forward + softmax-CE loss actually drives — the cifar peer of CnnFold's last three theorems (cnnLossCot_den / cnn_W5_tied_totalloss / cnn_train_step_tied_certified).

cifar is the cnn shape with two conv→conv→pool stages instead of one, so its conv backward chain crosses an extra pool boundary. Three of the four conv-layer cotangents reuse the cnn chain cots verbatim (every one is generic in its downstream cotangent):

• W₄ (last conv before pool₂): cnnChainCotW2 W₅ W₆ W₇ h5 h6 ac4 hc4 g — relu₄ mask on the pool₂ input-VJP of the dense-head cotangent (the cnn conv₂ pattern, at the cifar head dims).
• W₃: cnnChainCotW1 W₄ hc3 cotW4 — relu₃ mask on conv₄'s input-VJP (the cnn conv₁ pattern).
• W₁: cnnChainCotW1 W₂ hc1 cotW2 — relu₁ mask on conv₂'s input-VJP (same pattern).

Only W₂ needs a new constructor cifarChainCotW2: its cotangent crosses pool₁ at the relu-free conv₃-input boundary, so it is relu₂ mask on maxpool₁-back(conv₃-back(W₃, cotW3)) — a conv input-VJP then a maxpool input-VJP, the step cnn (one pool) never had.