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

A net's T2 theorem (resnet34FwdGraphB_full_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 T2 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 T2 graph's nesting order, with the T2 graph's prefixes and shapes, each block reading the previous block's output name.

Scope. f32, convBias := false, one replica (sync := false) — the configuration the T2 graphs describe. The bf16 renders swap in …Bf16 constructors (Bf16Fold, Bf16GradNodes); 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. Not covered: ConvNeXt-T and ViT, whose T2 graphs are per-example, with their own constructors.

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.