A campaign is one numbered stage of nanofil's formal plan in formal.md, from Campaign 0 (measure which checks survive) to Campaign 7 (prove one program never panics). Each ends with a note in docs/ saying what it found.
| Campaign | Goal | Note |
|---|
| 0 | measure the residual checks | residual.md |
| 1 | the core model in Rocq, agreeing with the interpreterinterpreter nanofilThe interpreter is interp.pl, nanofil's executable meaning of the IR: a relation from a module, a function, arguments and fuel to an outcome, with CLP(Z) integers so that it runs in every direction. The Rocq model transcribes it, and the outcome gate checks that the two agree on every run line of the corpus. | rocq.md |
| 2 | the runtimeruntime Fil-CThe runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGC: where a new object goes, what free does, and what the collector may change while the program waits at a safepoint. The model does not define it; it states it as one page of axioms, Module Type Runtime (Runtime), each with a native test in tests/c/prog/axiom-*.c. as axioms | runtime-axioms.md |
| 3 | [[soundness | soundness of checking]], valid_no_unchecked | rocq.md |
| 4 | observations, refinement, libc [[external-call | contracts]] | libc-contracts.md |
| 5 | static discharge by certificate | not started |
| 6 | integration with Filnix | not started |
| 7 | trap-freedom of one pinned program | trap-census.md |
The word has two other meanings nearby. campaign.md is "the campaign": nanofil's foundation as an executable account of Fil-C's capability semantics, which formal.md extends. And "the full campaign" is the opt-in Rocq check with every mutantmutant nanofilA mutant is a checked module with one item changed, inserted or deleted: a check deleted or moved, its bounds, rights or alignment changed, a raw access's offset moved by one, a free inserted between evidence and its use, a reuse form given another proof, a poll edge removed, or a data object's or alias's linkage, target or name changed. Prolog's and Rocq's validators judge each, and must agree.. Filnix's port campaign is unrelated.
See formal.md, The campaigns at a glance.