nanofil

nanofil is a C compiler written in Prolog that emits Fil-C's memory-safe ABI, and an executable account of what that safety consists of: every check is a term in its IR, an interpreter gives the IR a meaning, and a Rocq model proves that a validated module's checks are enough. Every page about it is listed here.

Start

A guide to nanofil: one C function through every stage, the ideas to hold, a map of the modules and where to start a change.
Compile C in the browser: nanofil on SWI-Prolog in WebAssembly, drawing the syntax, IR and assembly it makes.

Explainers

How Fil-C works: capabilities, the collector, safepoints and the libc sandwich, the memory-safe C nanofil targets.
How Iris works: from Hoare logic to Iris, how it is built in Rocq, and nanofil's machine as an Iris language.
Concepts: each term the Prolog, the Rocq and these documents share, explained once.

The formal campaign

The formal campaign: checks removed only where a machine-checked proof says they cannot fire; the plan, campaign by campaign, and what is built.
The model, read as Rocq: the Rocq development drawn as structure, with its proofs' states.
A program logic for never_panics: moving the proofs that programs never panic to Iris, and how far it has come.
Campaign 0: Lua's residual checks: which checks remain after nanofil's own evidence, measured on Lua.
Campaign 1: the core model in Rocq: the model, the validator and the machine, the decisions taken and the gates.
Campaign 2: the runtime as axioms: the facts about Fil-C's runtime the model takes as given, each with a native test.
The Gallina backend: the plan for a nanofil IR compiler written in Gallina and extracted, first to OCaml, then to C++ and a Fil-C library.
Campaign 7: trap-obligation census and native libc contracts: what a whole program (Hello) needs proved, and the libc boundary it relies on.

The compiler

The source, read as Prolog: every module drawn as terms.
The campaign: executable capability semantics: the foundation and its priorities; read it before semantic work.
Pizlonation: the checked stage's contract, its proofs, safepoints and pointer effects.
The explicit-free lifetime oracle: the interpreter's model of free.
Fil-C ABI findings: the ABI as verified against the pinned Fil-C.
Undefined behaviour: what Fil-C and nanofil do with overflow, shifts, aliasing and uninitialized reads.
Nonlocal returns, floating point, fixed-register inline asm and full-width vector access: their contracts.
NFB, a bytecode for nanofil IR: an RFC draft for the IR as little-endian words, with one encoding per module; the numbers the encoder and decoder of nfb.pl assign.
dterm: how these pages draw Prolog and Rocq, and documentation as a relation; its workbench sets the same terms side by side.

Check evidence

M7: reusing access-check evidence: one check's proof covering later accesses, round by round, with the reviews.
Forward facts and half checks: the -O default's evidence, as filcc's forward pass keeps it.
Scheduled checks: earlier traps as filcc's scheduler makes them; an opt-in prototype.
One branch for both bounds: the two bounds tests as one comparison.
Lowers per root: the GC-root contract of a frame.

Measurement

Package survey: how much of filnix's ported C builds with nanofil alone, and what stops the rest.
Code quality: where -O spends its instructions, the benchmark gate and the plan.
Real C corpus and Lua 5.4: whole programs built by nanofil, against filcc.
Upstream Fil-C's test suite: Fil-C's own tests built by nanofil, failures by kind.
One arithmetic, three readings: constant folding against the interpreter and clang.

Milestones

The milestones that are still partly reference; search M4 for a C feature.

PLAN.md: milestones and decisions.
M3: pointer class and Fil-C lowering, M4: C frontend and M5: analyses and promotion.

Filnix wiki