FwdGraphTextTies — the rendered forward blocks are pretty of the typed block graphs #

A net's graph-faithfulness theorem (resnet34FwdGraphBFull_faithful, …) says a typed graph denotes the proven forward. The artifact in verified_mlir/ is written by the renderer's forward chain (r34FwdChainB, …), a separate definition that emits one block at a time. This module ties the two by TEXT: for every block kind, the renderer's block emitter and pretty of the typed block graph — the block input an .operand leaf named as the emitter's input, every weight zero (pretty reads names and shapes only) — print the same bytes from the same EmitS start state.

Why per block. The whole-net graph cannot be printed and compared: pretty shares nothing, and a residual graph repeats its block-input subtree in both addVB operands, so the prefix is re-emitted at every skip (≈2¹⁶ copies of the stem for ResNet-34). Per block the input is a leaf, so repeating it emits nothing — exactly what the chain does when it names the input twice. What stays outside the guards is the chain's glue: it calls these emitters in the typed graph's nesting order, with the typed graph's prefixes and shapes, each block reading the previous block's output name.

Scope. convBias := false, one replica (sync := false) — the configuration the typed graphs describe; f32 throughout, and for ResNet-34, ResNet-50, MobileNetV2, MobileNetV4-Conv-M and EfficientNet-B0 also bf16: their typed graphs take the renderer's bf16 flag (StableHLO.PrecisionSwitch), so their stem, block and (for the three depthwise nets) head rows are checked at both values, the bf16 text against the bf16 graph. ConvNeXt's bf16 render swaps in …Bf16 constructors (Bf16Fold, Bf16GradNodes) that its typed graph does not select — that graph is the per-example convNextFwdGraphTCh, whose renderer has no bf16 (the batched bf16 chain has no typed graph at either precision); ViT's batched graph takes the flags but has no text tie at either precision (below); sync-BN renders swap the BN site (SyncBnSites, the *SyncB twins). Covered: ResNet-34, ResNet-50, MobileNetV2, MobileNetV4-Conv-M and EfficientNet-B0 — every block kind, stem and head, each checked by #guard at batch 2 on one concrete shape (for MobileNetV4, every row of the 21-row table), MobileNetV2's per-example inference forward (MobileNetV2FullPaperEval), the MobileNetV2, MobileNetV4 and EfficientNet-B0 heads with classifier dropout (cd := true), EfficientNet-B0's residual block and every MobileNetV4 skip row with its stochastic-depth site (sd := true), and MobileNetV4's inference forward (.eval, frozen-statistics BN) at both input sizes its evals are rendered at, and EfficientNet-B0's inference forward (efficientnetFwdGraphBFullEval: stem, the four block shapes, head). ConvNeXt-T's per-example forward (convNextFwdGraphTCh) is covered per kind too: block, downsample, stem and head at batch 2. What stays outside is its chain's prefixes: the render names block j of stage si s{si}b{j} and the typed graph numbers them b{n}_ across stages, so the two agree block by block, not name by name across the net.

Not covered: ViT. vitBlockGraphMHV shares non-leaf subterms (LN1's output feeds Q, K and V; Q, K and V feed every head; the first residual feeds LN2 and the second residual), and pretty shares nothing, so the graph prints them again at every use where the render names each once; the render also slices Q, K and V for a head before any of that head's products, where the graph's postorder interleaves them. A text tie would need a sharing printer or a reordered render. The batched graph the vitin_* artifacts' forward is rendered from, vitFwdGraphBDrop, has the same sharing; it takes the renderer's bf16 / bf16Conv flags and is faithful at every value (vitFwdGraphBDrop_faithful), so for ViT the bf16 forward is covered by that theorem alone, as the f32 one is.

A #guard failing here means the emitted text and the proven graph drifted: the graph's operand order, a name, a constructor or a shape differs from what the renderer writes. Fix the side that is wrong; the artifact is the ground truth unless it is the bug.