Fil-C on Nix

Filnix wiki

nanofil/docs/gallina-backend.md

The Gallina backend: a nanofil IR compiler extracted from Rocq

November 2026. A campaign plan, written before any of it is built. It extends the formal campaign, which today scopes "implementation correctness" (native lowering) out of proof. This campaign moves the lowering itself into Rocq, so that claim comes within reach later.

The ambition

nanofil's middle and backend, from the IR to machine code, become Gallina functions in the Rocq development. Extraction turns them into a standalone nanofil IR compiler: first OCaml, then C++ through Bloomberg's Crane, then that C++ built by Fil-C as library code a program can call at run time.

Four things are wanted from it:

Scope: the C frontend stays in Prolog. That is not because it is cheap. Measured at M1, the frontend is about 40% of the plain SQLite compile, and 325 of the 347 s the 281-module test corpus takes, because headers dominate an ordinary translation unit. So a perfect backend barely speeds up everyday C compiles.

The campaign's speed goal serves two other uses:

The scope is mbrock's, and so is the reason: "i excluded the c frontend from the campaign scope mostly because it's big and messy and i am kinda mostly driven to do all this from thinking about jit etc". The frontend is something to reconsider later, outside this campaign.

What exists

The Prolog pipeline after the frontend

Lines are wc -l of nanofil/src today. guide.md walks one function through all of it.

Without -O the path is the reference path: pizlonate, validate, filc_abi:lower_function/5, then filc_amd64 with --registers=stack, where every temporary lives in a frame slot, and asm:print_asm/1. Its other defaults are --checks=reference, --branches=reference and --memcpy=call. About 5,800 lines of Prolog are on it, most of them in filc_amd64.pl.

The Rocq model

In nanofil/rocq/theories, on Rocq 9.1 with stdpp and Iris:

The syntax covers the checked stage only. It has no unchecked load or store, and no vectors, cas and atomics, setjmp, asm_fixed or touch. Of Lua 5.4.7, every function but one decodes into it.

The first version

The first version is the reference path and nothing else:

  1. the asm line terms and their printer;
  2. the frame and ABI plan;
  3. stack-homed emission for the model's core subset;
  4. pizlonation, with the model's valid between it and emission.

It reads IR and writes assembly text for GNU as, the same text the Prolog reference emission prints.

It leaves out:

"The fast simple register mode", as I read it. Prolog has three register modes today: stack, temps and pointers. Only stack is simple, and it is the reference every other mode is checked against, so the first version ports stack. A register allocator that is fast and simple by design (one pass, block-local or linear scan, no translation checker because it is proved instead) is its own later milestone, M7. It is not a port of amd64_regs.pl: that allocator and its checkers are half of -O's compile time.

Reusing the model's definitions

The backend imports the model; it does not copy it.

The new files live in their own project, nanofil/rocq/backend/, with -R ../theories Nanofil and -R . Backend, on the pattern of rocq/spikes. Its Nix check compiles against the model's compiled theories and is not part of the quick nanofil-rocq gate, so that gate does not grow. It touches no file of the program logic or the libc contracts.

Two places need more than the model has, and both go to the model's owner as requests instead of being worked around:

Checking it against the Prolog compiler

The Prolog reference emission is the oracle, and the standard is byte identity.

Byte identity holds until the Gallina backend is the reference. From then on a stage's Prolog twin is retired instead of kept in step, and that is where the mirroring goes away.

The quick subset of these tests runs in the backend's own Nix check. The large programs run in the package checks, which already exist and already run after a push.

Extraction

OCaml first. It is the extraction Rocq ships, the model already uses it, and the driver, zarith and the Nix build are in place. The compiler's entry points are Gallina functions from text to text, so the OCaml driver only reads a file and writes one. Text is built as lists of parts and joined once, as asm.pl does: SQLite's assembly is about 100 MB.

Then Crane. Crane is a Rocq plugin forked from the OCaml extraction. By its README it emits C++23 that needs no runtime system and manages memory with shared_ptr, is LGPL-2.1, installs against Rocq 9.0 and is under active development with parts still experimental. Known risks, each settled in M6 before anything depends on it:

Crane is an alpha, and we expect to patch it. Its site says so, and it will not take all of Gallina. Three rules follow.

The fallback is Gallina to C. If Crane costs more to bend than it saves, CertiRocq (formerly CertiCoq) compiles Gallina to Clight, which any C compiler takes, and brings a small C runtime with its own collector; the Codegen plugin is a second, narrower route to C. Either gives C that filcc can build, so the library and JIT steps below do not depend on Crane. Neither is tried unless M6 fails, and whether CertiRocq's runtime (its tagged values and its collector) is at home under Fil-C is the first thing to find out then.

The Gallina is written with the second extraction in mind from the start: no OCaml-only Extract Constant on a hot path without a C++ twin, and no hand-written OCaml that the compiler's result depends on. The canonical-term reader in main.ml is such code today, and M4 replaces it with a Gallina one.

The path to a Fil-C library and a JIT

The first JIT needs no encoder and no new way to load code. The regex experiment (its README, pcre2-jit.md) already runs one. Behind pcre2_jit_compile, a patched libpcre2 prints a pattern's bytecode as terms and runs a compiler, rxc, on a cache miss. The experiment's regex compiler, itself Prolog, turns the terms into unchecked nanofil IR, then rxc runs nanofil -O compile, as and ld -shared. The library loads the shared object with dlopen and keeps it in a cache directory. The Fil-C runtime the code calls is already in the loading process, so the trusted runtime does not change.

What that route lacks is a fast compiler. A miss costs 0.15 to 0.8 s per pattern on SWI-Prolog, and nearly all of it is nanofil -O compile: as and the link together take under a tenth of a second even for a module of 36 functions. On Fil-C Trealla, which is what a libpcre2 with its compiler inside would run, the median is 2.4 s. sljit takes 0.1 ms. So the steps are:

  1. The extracted compiler in rxc. nanofil-backend compile takes the place of nanofil -O compile. The regex compiler emits unchecked IR, so this needs pizlonation (M4) and nothing after it. The regex compiler itself stays Prolog for now (0.07 s for 36 patterns).
  2. Code worth running. The first version's code is what Prolog makes without -O, which the experiment measured at 5 to 10 times slower than -O code. That is about the interpreter's speed on some patterns, so the route is not yet worth switching on. With -O's middle end and check passes but stack homes, the code is only 1.1 to 1.7 times slower than full -O. So for pcre2 the check passes matter far more than a register allocator. M5 measures which of them buy the difference on the regex compiler's IR, and those are ported first.
  3. libnanofil, pizlonated. Crane's output is plain C++23, and Fil-C is a C++ compiler (clang 20 with libc++), so the extracted compiler is built with filcc and given a C interface: IR text or a term tree in, assembly text out. libpcre2 links it and calls it in the process; the hook still runs as and ld and loads with dlopen. It is memory-safe against any input, by Fil-C, and checked by the same differential tests as the OCaml build. Crane's README asks for Clang 19 or later; whether Fil-C's libc++ has everything the output uses is found out in M8.

Two further steps are options for later, taken only if measurement asks for them:

The dlopen route trusts the cache directory, as the experiment's README says: what is in it is loaded as code. The validator is the asset on the compiler's side. valid is already Gallina, already extracted and already proved (valid_no_unchecked), so the compiler checks a client's IR after pizlonation and before emitting anything.

Performance targets

These are targets. The figures known before the campaign are perf.md's:

Targets, each measured in perf stat user instructions on the same input and the same stages:

A stage that misses its target gets a profile and a note of where the time goes before the next stage starts.

The baseline, measured at M1. CPU seconds of the plain compile in SWI-Prolog, stage by stage, on one core of an orb (a 2.6 GHz Xeon):

At M1 the extracted printer printed SQLite's lines in 5.0 s, which is 2.5 times Prolog's speed, within 230 MB. Two things follow:

The profile, at the start of M3. perf record with DWARF call graphs, on SQLite, in CPU seconds: an orb has no hardware counters, so instructions are not counted here. The targets for the two parts are a twentieth of Prolog's stages: 0.64 s for printing, and 1.0 s for the plans and the emission together.

The printer went from 5.0 s to 1.1 s:

What remains is a list cell per part and a string per digit.

The plans went from 7.8 s to 2.6 s:

Of what remains, liveness is a third, the first and last touch of each temporary a quarter, the fusing of checks a fifth, and the lowering of instructions a tenth. No one function stands out. About half of all of it is finding and adding names in maps: a name is a term such as tmp(v12), hashed and compared as one at every step. The repair is to number a function's temporaries once and key the maps and sets by number, which changes every pass of M2 and belongs to M5. The gate's 1.4 GB for SQLite, nearly all of it the module read as terms, goes with M4's reader.

Both parts still miss their targets, by less than twice for printing and by more than twice for the plans before any emission. M3's emission is written with this in mind, with no number or list written inside a loop.

Milestones

Each ends with its gate green and a short note of what it found.

M0. The plan and the project. This document. rocq/backend/ with its _RocqProject, a build script, extraction to a nanofil-backend binary and a Nix check outside the quick gate. Gate: the empty project builds, extracts and passes parse.sh.

Done. make -C rocq/backend builds nanofil-backend in two seconds. It compiles only the model files the backend imports, which is Term.v so far, so it does not wait for the model's proofs. The flake checks are nanofil-backend, which takes ten seconds once its inputs are built, and nanofil-backend-full. They have their own workflow, and the quick Rocq gate does not read the directory.

M1. Asm lines and the printer. Asm.v: lines, directives, operands and expressions as inductives, a decoder from terms, and the printer. A Prolog command prints a module's line list as terms. Gate: for the corpus, the printed text equals nanofil compile's, byte for byte; the per-stage baseline is measured and recorded here.

Done. The command is nanofil asm-terms FILE TEXT, which writes the text and prints the lines it is the text of. Asm.v has the types and the printer, AsmTerm.v the decoder, and rocq/backend/tests/asm.sh is the gate. The text is the same for all 280 Fil-C modules of tests/filc, tests/c and tests/c/prog, with and without -O, and for SQLite's 5.52 million lines. Seven files are skipped: six that nanofil refuses without their test's flags, and one plain module. Found:

M2. Frames and the ABI plan. filc_abi.pl and frame_slots.pl: slots, roots, entry and exit actions, call layouts, signatures. Gate: the plan of every corpus function in the subset equals Prolog's, as terms.

Done. The command is nanofil abi-terms FILE, which prints the checked module, the plan of each function and the plans of its weak thunks. Plan.v has the plan's types, whose instructions are Syntax.v's. Fuse.v joins a check to its access, Liveness.v and FrameSlots.v give temporaries their slots, Abi.v builds the plan, and Order.v is Prolog's standard order of terms, which the plans are sorted by. IrTerm.v and PlanTerm.v write a plan as Prolog's term, and rocq/backend/tests/abi.sh is the gate. Only the reference path is compared, without -O.

On the 280 modules of the corpus, the plans of 1089 functions and all 280 lists of thunks are the same terms. The backend refuses no function of the subset. The model keeps 576 functions outside it, and they are passed over: 535 for touch, 12 for asm_fixed, 11 for fence, 9 for setjmp and 9 for raw_cas. On SQLite all 3106 plans and the thunks are the same, with nothing outside. Found:

M3. Stack-homed emission. filc_amd64.pl's reference emission and amd64.pl's scalar selection, in pieces: scalars, compares and jumps first; then checks, flights, raw accesses and polls; then calls, variadics, function objects, data, aliases and TLS. Gate: whole-module byte identity on the corpus, hello, zlib and Lua, with the first performance target.

M4. Pizlonation and a standalone compiler. Unchecked.v, Pizlonate.v and a Gallina reader for IR text. The pipeline is read, pizlonate, valid, lower, emit, print. Gate: the pizlonated module equals Prolog's as a term, and nanofil-backend compile FILE.ir equals nanofil compile FILE.ir with no Prolog in the pipeline.

M5. Speed, and pcre2 through rxc. Profile, fix data structures, record the numbers in perf.md's style. rxc gets a switch that runs nanofil-backend in place of the Prolog compile. Gate: the second performance target; the experiment's checks pass with the extracted compiler; the miss time and the code's speed are recorded, with a list of the -O passes that code needs.

M6. Crane. Build Crane in Nix against our Rocq, extract the same entry points to C++, compile with clang++ and run the same differential tests. Gate: byte identity again, and the C++ target. If Crane cannot extract the development, the note says what stopped it, and the order of remedies is: change the Gallina, use a Crane switch, patch Crane, fall back to CertiRocq.

M7. A fast simple register allocator. Designed for a proof, not ported. Gate: difftests and package checks by behaviour, and a measured run-time gain over stack homes on the benchmark gate.

M8. The Fil-C library. The Crane output built by filcc as libnanofil and called in the process by the pcre2 hook, which still runs as and ld and loads with dlopen. Gate: the pizlonated library passes the differential tests and the experiment's checks.

M9. Hybrid -O. Emission of the reuse forms, so Prolog's middle end and check passes can feed the extracted backend. This is where users of -O first feel the speed.

Later. The middle end and the check passes in Gallina, each replacing a *_refines run-time check with a theorem, the ones pcre2's code needs first. An encoder and a shared-object writer, and installing code in the process, if measurement asks for them.

Outside this campaign. The C frontend. It is where an everyday C compile spends its time, so it is the thing to reconsider once the backend is done, as its own campaign.

M1 to M3 can run in parallel once M1's Asm.v types are fixed, because the plan and the emission pieces own different files.

The proofs it enables

None of these is promised by the milestones above. They are what becomes statable.

Decisions wanted

Each has a recommendation; work proceeds on it unless told otherwise.

  1. What the first version's register mode is. Recommended: stack homes now, a new simple allocator at M7, never a port of amd64_regs.pl.
  2. Where the compiler starts. Recommended: checked IR first (M1 to M3), since that is what Syntax.v describes, then pizlonation on a backend-owned Unchecked.v (M4).
  3. Byte identity as the standard, until the Gallina backend is the reference. Recommended: yes; it is the cheapest strong test there is, and the snapshot gate already works this way.
  4. The first JIT is the regex experiment's route: as, ld -shared and dlopen, with the extracted compiler in rxc from M5. Settled by mbrock. An encoder and installing code in the process are later options; the second is a runtime change and would wait for its own review.
  5. What pcre2 needs after M5. The first version's code has none of -O's check elimination. Recommended: port the check passes M5 finds decisive before the M7 allocator, since the experiment shows they are worth 5 to 10× and registers 1.1 to 1.7×.