The chapter 3–4 artifact writers #

Each #eval below writes one committed verified_mlir/ file (the MNIST CNN, the CIFAR CNN and the cifar8 family) from CnnRender.lean's faithful renderers, when this module is elaborated. Nothing imports this file: the proofs import CnnRender, so building them never rewrites an artifact. scripts/regen_verified_mlir.sh proofs and the proofs.yml drift guard both elaborate it.