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 or asm_fixed. 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:

M6 met all three, and its record under Milestones says how each was settled.

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 was such code. Since M4 the standalone compiler reads IR text with IrText.v, and the OCaml reader serves only the gates that take Prolog's terms. Three character primitives of IrText.v have OCaml definitions. At M6 they needed no C++ twins of their own: Crane's mappings of nat_of_ascii, ascii_of_nat and string_of_list_ascii cover them.

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. M5 measured it on the experiment's nine benchmark patterns: 2.7 to 16 times slower than -O code, 6.2 times in the geometric mean, and still 1.5 to 3.5 times faster than PCRE2's interpreter. The regex compiler keeps a node's choice state in alloc slots, and without promotion every use of one is a checked load or store. Promotion, copy propagation and the selection of branches bring the code to 2.1 times -O's, which is all that -O gives with stack homes; registers are the other 2 times. Simplification, inlining, the check passes and the inline memcpy change nothing for this code. M5b ported the first three, before Crane and before the allocator, and rxc now runs nanofil-backend compile-promoted: the measured figure is 2.10.
  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 is nearly all the module read as terms, which a reader of NFB words would not build.

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.

The profile, at the end of M3. The same tool on nanofil-backend module, which reads SQLite's module, lowers it, emits it and prints it in 8.8 s. As shares of that time:

Inside the instructions' lines no one form stands out. The leaves are string concatenation (17%), the hash and comparison of a name (about 40% with the maps' lookups), and list append (10%). So the emission's own cost is names again: a slot is found by the term of its temporary, and a label is built from strings at each use. Numbered temporaries remove the first, and a label kept as parts until it is printed removes the second.

The measurements of M5. On the standalone compiler, which compiles SQLite's IR text in 41 s where nanofil compile takes 70.

The validator is the cost. The model's valid is 18 to 20 s of the 41, where Prolog's own validator takes 14. It grows with the square of a function's definitions: two thirds of it is in three functions of 6,000 to 14,800 definitions.

The validator is the model's, and nine proof files of the program logic read single_definitions, so the repair is not this campaign's to make alone. Decision 6 below is about it.

The first repair. theories/ValidFast.v counts every definition in one pass into a map, and its valid_fast is valid with the single definitions taken from that count. valid_fast_eq proves valid_fast md = valid md for every module, so valid stays the definition the proofs and the gates read, and the compiler runs valid_fast. On SQLite, pizlonation and validation went from 24.8 s to 17.2 s and the whole compile from 41 s to 33 s, with the same text printed. The two lookups are next; the blocks' own rules are 4.0 s of what is left and the reuse forms' stage about 5.

Numbered temporaries gain nothing. A pass that numbered a function's temporaries and gave the plans integer names was written and measured: the validator and the plans took the same time. What they pay for is the walk along a list, not the comparison of two names at each step. So the repair is maps in place of the lists, with whatever names, and the pass is not in the tree.

pcre2 through rxc. With NANOFIL_BACKEND set, rxc and the experiment's run.sh compile the IR with nanofil-backend compile, and no Prolog runs after the regex compiler. The experiment's checks pass: the module of 36 functions is Prolog's plain compile byte for byte, bench agrees with PCRE2 on every pattern, and hook compiles its 39 patterns and agrees on all of them.

Compile time, on an orb:

So the 10 ms target is missed by two to four times, and validation is again the largest part. A miss is now bounded as the target wanted, by the regex compiler in SWI-Prolog and three process starts, at about a tenth of a second.

With M5b's passes. rxc and run.sh now run nanofil-backend compile-promoted. For the module of 36 it prints 45,702 lines, nanofil compile-promoted's byte for byte, in 0.35 s, against 1.4 s for that command and 6.2 s for nanofil -O compile; the first version's text is 99,256 lines, and -O's 28,580. Per call, on the nine benchmark patterns and as a multiple of -O's time, the code takes 2.10 in the geometric mean (1.56 to 2.91), where the first version's takes 6.0 (2.8 to 16): the figure the Prolog selection measured below. That is 3.0 to 11.8 times faster than PCRE2's interpreter. A cold cache of 39 patterns through the hook takes 4.1 s, 106 ms a miss, against 4.5 to 4.7 s with the first version. bench and hook agree with PCRE2 on every pattern.

The code's speed, and which passes it needs. nanofil compile on the module with one selection of -O's parts at a time, then bench. The figure is the geometric mean over the nine benchmark patterns of the time per call, as a multiple of full -O's:

Four things follow:

The C++ build, measured at M6. The target was within 2× of the OCaml build, and it is missed: Crane's C++ takes 5 to 7.5 times the OCaml build's time and up to 4 times its memory, and it is slower than Prolog. Wall time and peak memory on an orb, IR text to assembly, for the regex module rx.ir (36 functions) and for Lua's lvm.c as IR; each build prints the same bytes:

Where the time goes, by perf record on the C++ build:

Set Crane Arena was tried and is worse: slower, and ten times the memory. So no switch closes the gap, and what would is more patches to what Crane emits for values, matches and calls. That work is proposed for M8, where the same C++ is built by filcc and its speed first matters to a user; until then the OCaml build is the fast one.

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.

So far: every list of every module, and whole modules. The command is nanofil emit-terms FILE, which prints the checked module and then the reference emission's lines as terms: a list for each item, for each weak thunk and for the end of the file. Layout.v has a function's context and the loads and stores of homes. EmitOps.v is amd64.pl's scalar selection, with SSE2 and x87. EmitInst.v emits one instruction of a plan: lets, span tests, flights, fused and reused accesses, pointer effects, named locals, calls and the ABI's actions. EmitObject.v emits a function's getter, generic entry, variadic adapter and object, and Emit.v the function. EmitData.v emits a data object with its relocation table, a thread-local object, an init entry, a weak declaration and an alias's getter. EmitThunk.v emits a weak thunk, and EmitModule.v puts the lists in the file's order.

rocq/backend/tests/emit.sh is the gate. It emits each list again from the module and compares it, as text, with the reference's. Then, without -O, it compares what nanofil-backend module prints for the module with what nanofil compile prints for the file. For a preprocessed .i file the text is nanofil cc's, which is what nanofil-cc runs on a package's translation units. Emission is total: a form that is not ported gives a todo line, and the gate counts such a list as partial. None is left. The todos that remain in the code stand where Prolog itself fails or throws.

What it showed:

What remains of M3:

M4. Pizlonation and a standalone compiler. 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. Done.

Pizlonation is done. Pizlonate.v's pizlonate_module takes a module's term and gives the term pizlonate.pl gives: every access with its check, the flight forms, a poll on each edge to a block at or before its source, the loc markers of an unchecked module dropped, and the context items dropped. It gives nothing where Prolog fails or throws.

The standalone compiler is done. nanofil-backend compile FILE.ir reads the text with IrText.v and compiles the module with Compile.v: pizlonate, read into Syntax.v's types, the model's valid, lower, emit, print. It exits 1 for a module it refuses and 3 for one it does not take: a plain module, whose backend (amd64.pl) is not ported, or one with a function outside the subset.

The driver's input stays text. An NFB reader is proved (Nfb.decode), but its checked decoding of SQLite's two stages took 17 s, where the text reader takes 9.6 s for the first and the driver's OCaml reader of Prolog's terms about a second. It becomes the input when it is the faster one. The NFB work now aims at decoding straight into M5's numbered form: Syntax.v's own types with a temporary named by an integer term, symbols keeping their names, and a function outside the subset kept as a term.

The full check (nanofil-backend-full, about an hour) runs only when asked, by workflow_dispatch; the quick one runs on pushes that touch the backend's paths or the seven Prolog files it must match (ir_text.pl, pizlonate.pl, promote.pl, copy.pl, filc_abi.pl, filc_amd64.pl and asm.pl), and on no others.

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.

Measured, and half done. The numbers are under Performance targets.

M5b. The middle end pcre2's code needs. Promotion and what it stands on: the CFG and dominators of cfg.pl, escape.pl, promote.pl and copy.pl, about 2,100 lines of Prolog. They run before pizlonation, on the unchecked module, and their result is in the first version's forms, so nothing after them changes. With them comes the selection of branches in the emission (compare_branch and selected_jump in filc_amd64.pl, under 100 lines): a branch reads the flags of the comparison before it, and an edge to the next block falls through. simplify.pl, inlining and local storage are left out: M5's list says regex code does not need the first two, and local storage changes nothing in the regex module. Gate: byte identity on the corpus with the Prolog compiler run with those parts alone (opt.pl's passes([promote, copy]), which leaves local storage off, with --registers=stack --branches=selected --memcpy=call --checks=reference), and the regex experiment's patterns at the 2.1 times of full -O that this selection measures in Prolog. This is the first point where the rxc route is worth switching on.

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.

Done, but for the speed target. Crane at commit c2aadd9, with a patch of ours, extracts the reader of IR text, compile, compile_promoted and M7's compile_allocated to 36,106 lines of C++23. clang builds them with a driver of 127 lines as nanofil-backend-cpp, which prints what Prolog and the OCaml build print, byte for byte. It takes 5 to 7.5 times the OCaml build's time, so the 2× target is missed; the figures and the profile are under Performance targets. CertiRocq was not needed.

What stopped Crane, in the order of the remedies:

Three of those (the default branch, the numerals and the assignment) made C++ that compiled and computed something else. That is the argument for keeping the gates on every change to the backend: Crane is an alpha, as its site says, and its output is trusted only as far as it is compared. The patch is ours to maintain; none of it has been offered upstream yet.

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.

Done. Regs.v (nanofil-backend compile-allocated) numbers each function's temporaries into nat identifiers, recognizes adjacent single-use flight + check accesses and integer let + cmp + branch sequences so ephemeral values stay in %rax without taking a register home, builds closed sub-intervals per block from CFG liveness, and colors integer (w, l) temporaries and pointer (p) address words in descending 4^depth natural-loop weight order over %r10, %r11, %rbx and %r12–%r15, preferring a colored phi partner's register first so loop induction updates coalesce in place. Capability lowers stay in their lowers[] frame roots, and any temporary live across a call, helper call (AStorePointer, ADispatch, alloc, getters, va_arg) or poll edge takes only callee-saved %rbx or %r12–%r15, saved after the stack check and restored before every leave. Phi edges compile via a parallel-move scheduler using %rax and cycle-breaker %rcx with no shadow slots, and scalar operations select directly into assigned registers with three-address lea, imm32 operands and narrow loads and stores.

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 rest of the middle end and the check passes in Gallina, each replacing a *_refines run-time check with a theorem. 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 (M4). It turned out to need no types of its own.
  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, and M5 measured what each part is worth on the nine benchmark patterns. Promotion with copy propagation is 2.3 times, registers 1.7 to 2 times, branch selection 1.1 to 1.6; the check passes, simplification and inlining are nothing. Recommended: port promotion, copy propagation and branch selection (M5b, done) before Crane (M6) and the allocator (M7), and leave the check passes and simplify.pl for later. Two earlier versions of this decision were wrong: the first credited the check passes, and the second took registers to be worth 1.1 to 1.7 times and put simplification in M5b. The other way to the same speed for pcre2 alone is a regex compiler that emits SSA with no alloc slots; the port is preferred because every other producer of IR needs promotion too.
  6. How the validator gets fast. valid is half of a compile and quadratic in a function's size, and it is the model's definition, with proofs that read it. Recommended: this campaign writes, in a file of its own, maps in place of the lists behind single_definitions and the lookup of a definition and of a class, each proved equal to the list it replaces; the model's owner then switches valid_func to them, so valid stays the same function and the proofs rewrite once. The backend takes no unproved replacement at extraction. Proving valid (pizlonate m) = Some true, which removes the run altogether for the first version, stays the later goal. Agreed, with the equality at the top: the campaign's file proves valid_fast md = valid md, the compiler runs valid_fast, and valid_func and its proofs do not change. single_definitions is done; the lookups are not.
  7. What M8 does about the C++ build's speed. M6's C++ prints the right bytes at 5 to 7.5 times the OCaml build's time, against a target of 2. That matters only in M8: on a single function the C++ took 4.4 times the OCaml build's time, and Fil-C's usual 1.5 to 4 times comes on top. By that arithmetic a pattern's 16 to 43 ms in the OCaml build would be 0.1 to 0.8 s in a pizlonated libnanofil, which is slower than starting the OCaml build as a process, as rxc does now. That is an estimate; nothing has been built by filcc yet. Recommended: keep rxc on the OCaml build; begin M8 with a bounded attempt on Crane's output (the destructor's walk, the copies of Term variants, the parameters still passed by value) with 2 times OCaml on rx.ir as the mark; and if that stalls above 3 times, measure CertiRocq's C on the same input before building the library on either. The other choice is to build libnanofil as it is, to learn first what filcc makes of Crane's C++, and take the speed after.