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.
Contracts at the zsys_ boundary: an exploration of libpizlo's pizlonated system calls as the boundary instead of libc, what Hello reaches through user glibc, how much of user glibc nanofil compiles to IR, and Hello running on a glibc whose units it reaches are nanofil's.
A spike: proofs that link user glibc's IR: two programs proved with glibc's own strlen and write in the module, and libpizlo's zsys_write as the one contract.

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.
A guide to nanofil's IR and NFB bytecode (Argon): how the IR and its checked stage work, how NFB encodes a module into words, and how the Prolog and Gallina sides fit together.
The IR and NFB: a guide: the IR (modules, blocks, phis, classes, the unchecked and checked stages) and then NFB for a newcomer, with real encoded words from the corpus.
The nanofil IR and NFB: a newcomer's guide: the IR, its checked stage and NFB's words, written by Meta's Muse Wonderful (muse-wonder-full-1.0).
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