The Gallina backend (rocq/backend, docs/gallina-backend.md): the compiler's middle and back end in Gallina, extracted to OCaml and held to the Prolog compiler's output byte for byte. Off the quick Rocq gate: nothing in the model imports it.

nix build -L .#checks.x86_64-linux.nanofil-backend
nix build -L .#checks.x86_64-linux.nanofil-backend-full

It compiles the backend and the model files it imports (theories; not the model's proofs, so this does not wait for them), printing each file's time, extracts and links bin/nanofil-backend, and runs the gates of the milestones reached so far. M1: the extracted printer prints asm.pl's text from the lines the Prolog compiler emits (rocq/backend/tests/asm.sh), on the Fil-C IR fixtures and seven C programs that between them reach every line form; full=true takes the whole corpus, with and without -O. M2: the extracted ABI plans are the terms filc_abi.pl prints (rocq/backend/tests/abi.sh), on the same files and six more C programs that reach the plan forms the others lack; full=true takes the whole corpus. Then parse.sh reads every backend sentence back (web/rocq).