PoC: the MNIST-linear train step, proof-tied to the certified SGD step #
Companion to planning/archive/verified_faithful_sweep.md. MainMnistLinearVerified
trains on verified_mlir/linear_train_step.mlir, which is written by
Proofs.StableHLO.linTrainStepFaithfulV (the #eval writer at the end of
StableHLO.lean). This file certifies that renderer: every value the emitted module produces is the
certified (Mathlib-fderiv-derived) softmax-CE loss-descent SGD step.
(Namespace/name lengths are kept short on purpose: tests/AuditAxioms.lean's
three-axiom closure check greps #print axioms output per line, which Lean wraps
past ~120 cols — long qualified names would split the benign triple across lines
and false-fail the check. Keep future per-chapter capstone names short.)
What is closed here (kernel, [propext, Classical.choice, Quot.sound]) #
fwdGraph_faithful+poc_fwd_is_render— the forward-eval module isrenderModuleof a graph whosedenismnistLinear(text =render(graph)∧den(graph) = math). Forward: end-to-end tied.poc_train_step_tail_certified— fully tied. The two emitted SGD ops consume the provenlossCotGraphnode directly (no SSA-name pin), so each output'sdenis proven = the certifiedfderiv-derived step end-to-end, with the forward = the provenfwdGraph(nested inlossCotGraph)._fwdand_train_stepnow share the same forward graph — the connection §1a of the planning doc calls for.
The committed-bytes tie (verified_mlir/linear_train_step.mlir == linTrainStepFaithfulV(…)) is enforced in CI (regenerate + git diff, the
"Verified-render drift guard" step in proofs.yml), not here.
Honest residual (the boundary shared with the forward SHlo den) #
- Per-op
den⇄ MLIR text for the four tail ops:tailDenW/tailDenBmodel whatdot_general/reduce/multiply/subtractcompute; that they do is the same trusted op-level modelling the forwarddenalready relies on (the weight-grad piece iswGrad, tied toIR.emitWeightGradbywGrad_faithful). Adding these asSHlonodes with aden(whole module onepretty(provenGraph)) is the last mechanical step. - Single example (B = 1):
wGrad x dy = x ⊗ dy; the emitted module batch-contracts. The mean-loss cotangent makes the batch sum the mean gradient. - ℝ → Float32: deferred (a future pass);
FloatBridge.leancovers the linear/MLP rounding budget separately.
Forward eval — end-to-end tied #
The committed linear_fwd.mlir generator linearFwdModuleV is renderModule
applied to the proven fwdGraph — the emitted bytes are literally the print of
the graph fwdGraph_faithful is about.
The tail fold (closed) — the emitted tail ops are pretty(provenNode) #
StableHLO.linTrainStepFaithfulV (what generates verified_mlir/linear_train_step.mlir)
renders the whole module as pretty of SHlo nodes, fully tied: each of
SHlo.weightSgd / SHlo.biasSgd consumes the proven lossCotGraph node DIRECTLY
(not a .operand %dy <placeholder> name-pin), so the forward = the proven fwdGraph
(nested inside lossCotGraph) and den(output) = certified is one composed theorem
below — no trusted SSA-name linkage between the cotangent and the SGD ops. The shared
cotangent is rendered once per output (2×); iree CSEs the duplicate. (lr/W,b,x
values are skel-erased, so the render is value-independent — the placeholders
linTrainStepFaithfulV passes print the same text as the live graph here.)
The emitted weightSgd op — consuming the proven lossCotGraph node DIRECTLY (the
fully-tied render) — denotes linWeightDen (the certified sgdW step).
The emitted biasSgd op — consuming the proven lossCotGraph node DIRECTLY — denotes
linBiasDen (the certified bias step).
Tail fold (in-kernel, closed). The two emitted tail ops weightSgd/biasSgd
— the actual SHlo nodes linTrainStepFaithfulV prints — denote the certified
fderiv-derived loss-descent SGD step. The tail's meaning is now a property of
the emitted node (via den), proven — not a separately-supplied model.