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. NFB: Nfb.v's writer writes the words nfb.pl writes and its reader reads them back (rocq/backend/tests/nfb.sh, docs/nfb.md), on the same files; full=true takes the whole corpus, with and without -O. M3: the lines the backend gives each function's plan, each data item, alias and weak thunk are the reference emission's, and without -O the whole module's text is nanofilcompile's wherever every function is in the subset (rocq/backend/tests/emit.sh), on the same files and the fixtures of rocq/backend/tests/edge, which reach the arms the corpus does not; full=true takes the whole corpus, with and without -O, and then every translation unit of zlib, GNU hello and Lua as nanofil-cc preprocesses it (nanofil-cc.nix, hello.nix, lua.nix), where the whole text must be nanofilcc's. M4: Pizlonate.v makes of a module the term pizlonate.pl makes of it (rocq/backend/tests/pizlonate.sh), on the same files and the fixtures of rocq/backend/tests/pizlonate; full=true takes the whole corpus, with and without -O, and the translation units. M5b: Promote.v makes of a module the term promote.pl makes of it, and Copy.v of that the term copy.pl makes of it (rocq/backend/tests/promote.sh), on the same files and the fixtures of rocq/backend/tests/promote; full=true takes the whole corpus. And nanofil-backendcompile, which reads IR text itself, prints what nanofilcompile prints and refuses what it refuses (rocq/backend/tests/compile.sh), on the same files and the fixtures of rocq/backend/tests/compile; full=true takes the whole corpus and the translation units; the files it does not take are exactly those rocq/backend/tests/compile/none.txt names. And nanofil-backendcompile-promoted, which promotes, propagates copies and selects branches, prints what nanofilcompile-promoted prints, on the same files and the fixtures of rocq/backend/tests/promote. Its reader, IrText.v, reads the module Prolog reads and nothing where Prolog throws (rocq/backend/tests/read.sh), on the IR fixtures and on a thousand adversarial texts, those also cut into pieces of one and of seven bytes. Then parse.sh reads every backend sentence back (web/rocq).