The Gallina backend extracted to C++ by Crane (rocq/backend/crane, docs/gallina-backend.md, M6): the same Gallina as nix/backend.nix extracts to OCaml, held to the same Prolog output.

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

It builds the OCaml backend, for the model files and backend files the compiler imports and as the reference of the allocated compiler, extracts the compiler with Crane (nix/crane.nix) and compiles the C++ with clang, which is most of its time. Then:

• the self-test: each stdlib function that CraneMap.v maps to C++ gives, on numbers at and past the machine's widths, what vm_compute finds for it (CraneSelfTest.v, selftest.cpp);
• nanofil-backend-cppcompile and compile-promoted print what nanofilcompile and nanofilcompile-promoted print, byte for byte, and refuse what they refuse (rocq/backend/tests/compile.sh), on the IR fixtures; the files not taken are those rocq/backend/tests/compile/none.txt names;
• nanofil-backend-cppcompile-allocated prints what the OCaml build's compile-allocated prints, byte for byte, and exits as it does (rocq/backend/crane/tests/same.sh), on the same fixtures and those of rocq/backend/tests/regs; Prolog has no such command, and tests/regs.sh holds the OCaml build's output to how the programs behave (nix/backend.nix);
• parse.sh reads every sentence of the Crane files back (web/rocq).

No Fil-C toolchain: the fixtures are IR text.