The 95% Wilson score interval on an accuracy, as lo–hi in percentage points.

It sizes the digits an eval line can claim: on a 3,925-image validation set at p ≈ 0.85 the 95% half-width is ±1.11 pt.

Wilson, not the normal approximation p ± z·√(p(1−p)/n): the normal form collapses to ±0 at correct = 0 or correct = n, which would print a certain 0% on a run that scored nothing. Wilson stays finite there.

It is the measurement error only — how well 3,925 images pin this model's accuracy. It says nothing about seed-to-seed training variance, which needs n runs, and it is the WRONG test for comparing two models scored on the SAME set: that comparison is paired, so it wants McNemar over LEAN_MLIR_DUMP_CORRECT's per-example bitmaps, which is far more powerful.

The weight F32.ema puts on the NEW batch, i.e. 1 − decay, given the accumulation factor: some k on an acc variant (the EMA fires once per MICRO-batch, so the decay is k-th-rooted for k chained updates to compose to one bnMomentum/optimizer-step update), none otherwise.

One definition for its three consumers — trainAdamSched's loop, its startup banner, and the fp8 trainer — so a gate on it is a gate on the driver's expression.

The == 0.99 arm returns the double 0.01 rather than 1.0 - 0.99 (= 0.010000000000000009 — different bits, 9e-16 relative), so every net that leaves bnMomentum at its default keeps the exact weight 0.01. some 0 is reachable — VerifiedVariant.accK returns 0 when it cannot parse a k out of the variant name — and lands on 1/0 = inf, pow → 0, weight 1.0, i.e. the running stats become the latest batch. That is kept deliberately rather than quietly repaired: a variant name whose k does not parse is already training at a wrong effective LR (see accK), and this should not be the thing that hides it.

Param shapes in func-arg order (= specs dims).

Packed shape descriptors for the FFI (see packShapes).

Total float count across all params.

Packed x input shape [batch, d0].

EMA shadow — a FOURTH [θ|m|v|ema] blob region, 5 scalars not 3.

RMSProp — the mean-square slot initialises to 1.0, not 0. Substring, not prefix: the RMSProp+EMA spelling is emarms, which does not start with "rms".

Stochastic depth — N extra tensor<Bxf32> scale inputs. The marker is drop and not sd because rms ++ dp spells rmsdp, which contains "sd".

Classifier dropout — ONE extra tensor<B×wxf32> mask input. The marker is do and not dropout because dropout contains drop, so a dropout-only variant would read as a stochastic-depth one.

Gradient accumulation — a FOURTH [θ|m|v|G] region, 5 scalars. Substring, not prefix: RSB-A3's composed optimizer is lambaccdp8x64bce, where lamb ++ acc puts the marker in the MIDDLE.

LAMB — the per-tensor trust ratio (R34Opt.lambAccum), RSB-A3's optimizer. Substring, not prefix, for accOn's reason one spelling over: the EMA form is emalamb…, which does not start with "lamb".

BCE-with-logits (timm BinaryCrossEntropy), RSB's loss — not softmax CE. Substring: the marker trails the shape and is itself often trailed, by wd001 or bf16 (lambaccdp8x64wxclipbcebf16), so neither a prefix nor a suffix test finds it.

k, read back out of the name. The graph has 1/k BAKED in and the driver decides the apply cadence; a disagreement does not fail, it trains at a silently wrong effective learning rate. Parsed from AFTER the marker, not from a fixed offset — see accOn.

Blob regions: [θ|m|v], plus G (gradient accumulation) and/or E (the EMA shadow) — so 3, 4 or 5, and the two extras are INDEPENDENT. A 3-region file loaded by a 4-region driver (or the reverse) misaligns every parameter, so every consumer of a checkpoint sizes off this rather than off a literal.

The fifth region lets accumulation and EMA run together (RSB-A2/A1's recipe sets both gradAccumSteps := 4 and useEMA := true).

G comes before E, and that ordering is not free: at acc alone G is region 3 and at ema alone E is region 3, so a single-axis checkpoint reads at the same index either way. The reverse order would re-home every ema* blob.

Rank-0 scalar slots in the blob tail: lr,bc₁,bc₂, then %aup,%akeep (accumulation) and then %emad,%oemad (EMA) — so 3, 5 or 7, in that order. Same independence and same ordering rule as nRegions: the accumulation pair keeps slots 3–4 and the EMA pair moves to 5–6 only when both are on, so neither single-axis layout moves.

The blob index of the EMA shadow region, or none when the variant has no shadow. It is not the literal 3: under accumulation G takes region 3 and the shadow is region 4. scoreCheckpoint and the per-epoch eval both slice θ out of the blob with this, and a stale literal there does not fail — it scores the gradient accumulator as if it were weights and prints a plausible percentage off it.

Offset of the %emad,%oemad pair inside the scalar tail — 3 alone, 5 behind %aup,%akeep.

The eval forward's suffix for a variant rendered at a non-default BatchNorm ε: _eps0001 for an …eps0001… variant (ε = 1e-3), empty otherwise. ε is baked into every BN site, so a train step at one ε must be scored through an eval graph at the same ε — <slug>_fwd_eval_eps0001.mlir, entry @<slug>_fwd_eval_eps0001 — while every checkpoint trained at 1e-5 keeps scoring through <slug>_fwd_eval.mlir.

iree-compile one .mlir → .vmfb, surfacing failures. Skips when the .vmfb is already newer than the .mlir (a content-stable cache): avoids the ~minutes-long 224² recompile, and lets two same-net runs share one GPU-pair safely — they only read the cached vmfb (concurrent reads are fine; it's the concurrent writes of an identical compile that would race).

Open a session for one Lean-emitted graph, on whichever backend this binary dlopened.

• XLA — hand the .mlir straight to PJRT, which compiles it in-process. Nothing is written to disk.
• IREE — iree-compile the .mlir to a cache file first, then load that.

The cache path is derived from mlirPath rather than passed in, so two graphs cannot land on one cache file — the failure the target scoping below prevents from the other direction.

Both backends consume the same verified_mlir/*.mlir — the emitter, the spec, and the train-step ties are identical. Only the trusted lowerer differs.

mkSession for the eval forward at replicas devices, the sharded-inference session (LowererSession.createDp, outputs gathered). replicas ≤ 1 IS mkSession, so a single-GPU run and every IREE run are unchanged. Past 1 it is XLA-only and says so rather than quietly evaluating on one card.

bs labels, class (i + off) % nc, as the driver's int32 records — the shard labels the sync-BN, shard and tie gates feed.

Init one parameter from its (dims, initKind) spec, matching the JAX reference's initialisers — they are the oracle these nets are paired against:

• rank-4 conv kernel [oc, ic, kH, kW] → He fan-OUT, variance 2/(oc·kH·kW)
• rank-2 dense matrix [in, out] → Glorot, variance 2/(in + out)
• γ = 1 (kind 1), β / bias = 0 (kind 2), layer scale = 1e-6 (kind 3)

The weight variances are those of jax/Jax/Codegen.lean: uniform(±√(6/fan_out)) for convs (torchvision's kaiming_normal_(mode='fan_out', nonlinearity='relu') convention, emitConvBnInit) and uniform(±√(6/(fan_in+fan_out))) for dense (emitDenseInit); kind 3 is the reference's ConvNeXt layer-scale init, 1e-6. Kind 3 must be matched explicitly: the _ branch is the weight rule, which is the wrong answer for a per-channel scale. cnxInit and vitInit override the weight variance (see VerifiedConfig); heFanIn switches to fan-in for one gate.

Init is host-side: no verified_mlir/ file mentions it, so changing it moves no committed artifact.

Variance-matched, not distribution-matched: F32.heInit sums three uniforms (Bates-3, ≈ normal) where JAX draws one uniform. torchvision itself uses a normal here, so neither side is canonical on that axis.

Fill buf with EXACTLY n more bytes, looping until they arrive. A pipe read returns what is available, not what was asked for — at 154 MB per batch a short read is the normal case, not the edge case, and treating one read as a batch silently misaligns the stream from then on.

Read EXACTLY n bytes into a fresh buffer of exactly that capacity, allocated HERE — on the calling thread, which is what readInto is about. Allocating the exact capacity up front avoids ByteArray.append's doubling (a 308 MB batch would cost a 616 MB buffer and a copy).

Resolve a net's generated shim to a path on disk, or none. The candidate list is spawnShim's, factored out so the two callers cannot disagree about WHICH file they are reading — one of them decides the wire, the other spawns it.

The SHIM_MIX default a generated shim bakes — read out of the producer rather than restated here. "" when the shim cannot be found or declares nothing.

The shim text is the single source: a useMixup field on VerifiedNet would be a second definition of what generateShim already baked from the same config.

The stdio shape every shim child is spawned with. It has a name because IO.Process.Child is INDEXED by its config: without a concrete one the child cannot be stored in a structure, and without storing it the trainer holds a pipe it can neither kill nor reap.

Spawn the shim for one split and consume its preamble.

The preamble (LMSH | version | batch | flat) is checked rather than skipped: a batch or resolution mismatch between the render and the shim would otherwise read as garbage pixels and look like a broken net. Same reasoning as the FFI's G4 arity guard.

One batch off the wire: int32[batch] labels then float32[batch*flat] images, in that order (the shim writes labels first so a partial record is detectable at the smaller read).

Read up to n bytes, returning what actually arrived instead of throwing at EOF. The peer of readExact, and the only difference is which of "short read" and "clean end of stream" it treats as the error.

One shim batch, tolerating a SHORT FINAL BATCH — the validation-split reader.

The shim sets drop_remainder=training, so the validation split ends in a partial batch (ImageNet's 50,000 images at 256 are 195 full batches and an 80-image tail) that readExact refuses by construction. This reader accepts it, so every image is scored — timm's validate.py denominator, not 49,920.

Returns (img, lbl, rows) where rows ≤ batch, and rows = 0 means the stream ended cleanly.

Each batch starts with a 4-byte row count (read, not inferred: a pipe does not preserve write boundaries), then exactly rows labels and rows images, in wire order. A short read of either block is a torn write and throws instead of returning a silently short batch.

The eval graph keeps its baked batch width: F32.sliceImagesPad zero-pads the tail up to it and the eval loop scores min bs (nEval − bi·bs) real rows, so the pad never reaches the accuracy count. That is safe because eval normalises PER EXAMPLE everywhere — running-stat BN through @<slug>_fwd_eval, LayerNorm through @<slug>_fwd. The one exception is LEAN_MLIR_EVAL_BATCHSTATS=1, which scores through @<slug>_fwd with batch statistics: there the zero rows would shift the real rows' normalisation. That flag is a declared diagnostic, and the drain refuses to keep the tail under it.

Spawn n shim processes over disjoint shards of one split, and read them round-robin.

One shim process can be slower than a multi-replica step consumes images; several producers raise the loader's throughput.

It adds no second definition of the transform: each worker runs the same generated shim with SHIM_SHARD=i/n, which selects which examples it emits (ds.shard, before the map) and leaves _pp — the crop, flip and normalization — untouched.

Round-robin over batches is not the unsharded stream. ds.shard interleaves elements, so taking whole batches from each worker in turn gives a different batch composition than one producer would. Both are valid shuffled streams over the same epoch of data, and each worker shuffles its own slice with the pipeline's own seed — but the two are not byte-comparable, so a determinism hash from the unsharded config does not carry to a sharded one. Re-run SHIM_HASH per shard if you need that property.

Each worker gets a distinct seed (seed + i). With one shared seed every worker draws the same augmentation sequence, and since the shards hold different images that is not a correctness bug — but it needlessly correlates the crops across workers.

Round-robin read: batch k comes from worker k % n. readExact already blocks until a whole record has arrived, so a slow worker throttles rather than corrupting — the framing cannot slip.

Pull the next gB rows off the stream: (xb, lbl, real) with xb zero-padded to gB × flat floats and real ≤ gB the rows to score; real = 0 means the pass is over. The first rows = 0 in round-robin order IS the end: every producer has emitted all of its blocks by then (producer b % n has exactly ⌊b / n⌋ of them when global batch b is the first past the end). Sequential by construction — evalScore issues the next pull only after awaiting this one — so the carry needs no lock.

Spawn the per-pass val producers: n batch-block producers of the validation split at shimBatch rows — fresh for every pass and reaped by reapValStream, so nothing accumulates across epochs and the closed pipe stays the end-of-pass marker. flat is the EVAL width (RSB-A3 trains at 160² and evaluates at 224²), read off the artifact by the caller.

The gate-only fault knobs, in the PJRT_FFI_FAULT style — controls that must go red: LEAN_MLIR_VAL_FAULT=order starts the round-robin on producer 1 (every image scored against another image's label: same count, different bitmap), =tail drops the 80-row tail (a 49,920-image pass). scripts/gates/streamed_val_gate.sh.

Kill then wait, so no <defunct> child is left: the val stream ends by itself, but a dropped tail or a refusal can leave a child still writing.

The eval pass: score nEval images through a forward session, replicas × evalBs per invoke. (top-1 correct, top-5 correct, images scored, per-image top-1 bitmap). The bitmap is filled only when wantBits, in eval order, one byte per image. rows is where the images come from: the held split, or ImageNet's per-pass stream (EvalRows).

One copy, shared by the per-epoch eval in trainAdamSched and by scoreCheckpoint, because scripts/gates/sharded_eval_gate.sh compares 1 replica against N through score-checkpoint, and a gate on a copy of the loop says nothing about the loop that runs.

The ragged tail: 50,000 is not a multiple of 4 × 64 = 256: it is 195 full invokes and an 80-image tail, which fills replica 0 and a quarter of replica 1, while replicas 2 and 3 score pure padding. F32.sliceImagesPad zero-pads the invoke to the global batch, the shim gathers the logits back in ROW ORDER, and only min gB (nEval − bi·gB) rows are scored. The pad rows are computed and never read.

Load the train + eval splits for a dataset. Returns (trainImg, trainLbl, nTrain, evalImg, evalLbl, nEval, trainPix, crop?) where trainPix is the stored per-example width of the training images (256² for Imagenette, d0 otherwise) and crop? requests the 256²→224² center-crop.

evalOnly skips the TRAIN split entirely — for scoreCheckpoint, which never touches it. It is inert on .imagenet, whose train split is never preloaded (it streams off the shim), and worth having on the others: Imagenette's is 9,469 × 256² × 3 f32 = 7.4 GB read and held for a job that only scores 3,925 val images. nTrain comes back 0 under it, so a caller that starts using it gets a division rather than a plausible epoch.

Write bytes to path all-or-nothing: a sibling .tmp, then rename(2) over the target. A crash mid-write leaves the PREVIOUS file intact rather than a truncated one — the same guarantee the JAX reference's save_train_state gets from os.replace.

Where this (net, variant) writes and resumes its checkpoint.

Scoped by BACKEND: without the suffix an XLA run would happily resume from an IREE checkpoint and vice versa, silently fusing two trajectories into one while looking completely normal on screen. $LEAN_MLIR_CKPT_TAG appends a run-scoped suffix — without it every pass of the same (net, variant, backend) shares one path, so parallel passes clobber each other's blob and a later pass resumes from an earlier one's finished run.

A function because scoreCheckpoint has to land on the same path the trainer wrote, and "score the checkpoint the run just finished" is that tool's zero-argument case. Two spellings of this string would not fail — they would score a file that is not there, or worse, an older one from a different tag.

Print the startup banner with %LOWERER% resolved to the lowerer that actually ran.

The blurb carries a placeholder rather than a transport, so the banner states the run, not the build; every print site goes through here.

Train a VerifiedNet end-to-end on its proof-rendered StableHLO: compile both MLIRs → lowerer sessions → load data → spec init (mkParam) → SGD train + eval loop. The SGD update (and lr) are baked into <slug>_train_step.mlir; we only feed batches.

AdamW training driver — threads the first/second moment buffers as a single packed [θ|m|v] param blob through the generic FFI (n_params = 3k; the moments ride in the params slot, so the prebuilt .so is unchanged), against the committed baked-hyperparameter render <mlirDir>/<slug>_adam_train_step.mlir (rendered by LeanMlir/Proofs/Codegen/; its optimizer ops are tied to Proofs.adamWStep by Proofs.StableHLO.adamW_triple_faithful). Compiles through compileVmfb, so it runs on IREE only. Moments init to 0; eval reads the θ slice (first nParams floats). The Adam analogue of VerifiedNet.train.

Scheduled AdamW driver — trainAdamPacked with a runtime LR and bias correction. lr/bc₁/bc₂ ride as three rank-0 scalar params in the blob tail ([θ|m|v|lr|bc₁|bc₂], the FFI takes no scalar slot) and are returned unchanged; the host recomputes them each step: cosine decay + linear warmup for lr, and bc₁=1−β₁ᵗ, bc₂=1−β₂ᵗ (proper bias correction). Drives the committed <mlirDir>/<slug>_<variant>_train_step.mlir, rendered by LeanMlir/Proofs/Codegen/; its optimizer ops are tied per op (for example Proofs.StableHLO.adamW_triple_faithful, Proofs.StableHLO.lamb_triple_faithful, Proofs.StableHLO.mom_pair_faithful).

expDecayRate > 0 selects the EfficientNet/MobileNetV2 exponential schedule over cosine: after warmup, lr = baseLR · rate^((epoch − warmupEpochs)/decayEpochs). Both references use it (mnv2 ×0.98 per epoch, EfficientNet ×0.97 every 2.4). It is a driver item, not a render one, because lr is already a runtime operand. Default 0.0 keeps cosine.

RMSProp variants also need a different initial state (the mean-square slot starts at 1.0, VerifiedVariant.rmsOn), handled in the body.

Score a checkpoint, standalone — the eval half of trainAdamSched with no training in front of it. It scores any saved checkpoint, not only the weights live during training — the verified peer of the JAX side's eval_*_full50k.py. No new MLIR: every piece is the eval half's own:

The gate is an equality, not a smoke test: for the same checkpoint at the same region, the number printed here must equal the one the training run printed for that epoch — same denominator, same batching, same graph.

BN nets score through @<slug>_fwd_eval with the running statistics read from the <ckpt>.bn companion ([running | ema_bn], written at every epoch end): the EMA shadow with ema_bn, the live weights with the running stats — the training eval's pairing. A checkpoint older than the companion is refused, since scoring the .bin alone would normalise by zeros and still print a plausible percentage.

timm's test protocol: LEAN_MLIR_EVAL_SIZE / LEAN_MLIR_EVAL_CROP score through the eval graph rendered at that size (…_fwd_eval_s<S>.mlir) with the val stream resized and cropped to match (SHIM_EVAL_SIZE / SHIM_EVAL_CROP). scripts/parity/score_timm.sh reads the per-net values from jax/timm_eval_protocols.json.

region is what one checkpoint cannot otherwise yield: the driver picks live-or-shadow at TRAIN time (LEAN_MLIR_EMA_BN), so an EMA run reports one of the two numbers and discards the other. timm reports the shadow and RSB-A2 sets emaDecay := 0.9999, so without this an A2 result is not quotable the way its reference is. "auto" = the shadow when the variant has one, matching what the training run would have scored; "live" and "ema" name it explicitly.

Train driver for the 2-parameter linear path (Chapter 1). The verified @<slug>_train_step takes W0/b0 as separate arguments (linearTrainStepV), weights are zero-initialized, and the loss/lr are baked into the MLIR — distinct from the packed-params, mkParam-init train above. Only the linear classifier uses this; shares mkSession / loadData with the main driver.

fp8 (E4M3) Lean trainer — the low-precision sibling of trainLinear.

Keeps fp32 master weights and, each step, projects the weights (per-output-column) and the activations (per-tensor) onto the E4M3 grid (LeanMlir/E4M3Quant.lean), runs the same verified @<slug>_train_step kernel (the matmul accumulates in fp32 — the dotMixed model: u_leaf = E4M3, u_acc = fp32), and applies the recovered gradient delta to the fp32 master via addDelta (master += Wout − Wq = master − lr·∇). The MLIR and FFI are unchanged: fp8 here is host-side operand byte-prep, exactly the render-tie model of Proofs/Float/E4M3Fold.lean). Eval runs the fp32 master through @<slug>_fwd (the "fp32-infer" accuracy of the fp8-trained model, mirroring scripts/demos/mnist_e4m3_demo.py).

Run: lake exe mnist-linear-e4m3-verified data

fp8 (E4M3) packed-params trainer — the low-precision sibling of VerifiedNet.train, for the depth>1 nets (MLP, CNN). Keeps fp32 master params and, each step, projects every weight slot onto the E4M3 grid (dense per-output-column, conv per-output-channel; biases kept fp32 — F32E4M3.quantPackedParams) and the input per-tensor, runs the same verified @<slug>_train_step (fp32 accumulate inside), and folds the gradient delta back into the master with addDelta over the whole packed buffer (master += out − paramsQ: weight slots get −lr·∇, bias slots the exact update). MLIR/FFI unchanged.

Scope: host-side prep reaches weights + the input activation only. The intermediate activations (relu/pool/flatten outputs feeding the deeper matmuls) and the backward-chain cotangents are computed inside the fused kernel and stay fp32 — quantizing them would need in-graph E4M3 ops, not host byte-prep. So this is fp8 weights + fp8 input, fp32 intermediates. Eval runs the fp32 master.

Run: lake exe mnist-mlp-e4m3-verified data

fp8 (E4M3) variant of trainAdamSched — runs the Adam / Nesterov-momentum optimizer demos in fp8. Keeps an fp32 master [θ|m|v]; each step projects the weight third θ onto the E4M3 grid (quantPackedParams: dense per-column, conv per-channel; biases fp32) and the input per-tensor, runs the same verified @<slug>_<variant>_train_step (the optimizer is baked into the MLIR, so fp8 needs no new module — operand byte-prep only; fp32 accumulate), and folds the optimizer-step delta back into the fp32 master θ (addDelta), keeping the returned m'/v' moments in fp32. Distinct _e4m3 checkpoint (won't resume an fp32 run); honors LEAN_MLIR_MAX_EPOCHS. Same scope as trainE4M3: fp8 weights + input, fp32 intermediates / moments.

Lower to the runtime VerifiedNet the driver consumes.

Train end-to-end (delegates to the shared VerifiedNet.train driver).

Train the 2-parameter linear path (Chapter 1); see VerifiedNet.trainLinear.