nanofil's formal model, read as Rocq

rocq/backend/

Abi.v674 lines

Fil-C ABI lowering (filc_abi.pl's lower_function/4 and lower_thunks/2): the plan of a checked function, before any register or frame offset is chosen.

Asm.v274 lines

x86-64 assembly as the backend builds it, and its printer as GNU as (AT&T) text: asm.pl's line terms as inductives, and asm.pl's grammar as functions.

AsmTerm.v190 lines

Asm.v's lines from the terms asm.pl prints them from: the decoder of what nanofilasm − termsFILE writes, one line term each.

Compile.v184 lines

# From an unchecked module to its lines

Copy.v385 lines

# Copy propagation

Emit.v649 lines

The code of a function from its plan: filc_amd64.pl's function//2 with every temporary in its stack slot, which is what --registers=stack selects there.

EmitData.v519 lines

# Data objects, thread-local data, table entries and aliases

EmitInst.v797 lines

# Instructions

EmitModule.v55 lines

# The lines of a module

EmitObject.v418 lines

# Function objects

EmitOps.v2416 lines

The scalar instruction selection of the stack-homed emission: amd64.pl's compute_op//4 with all it calls, its store_insn/3 and load_insn/3, and filc_amd64.pl's x87 instructions for long double.

EmitThunk.v381 lines

# Weak thunks

Escape.v370 lines

# Escape classification of allocs

Extract.v90 lines

Extraction of the backend to OCaml, for the driver (extraction/main.ml), which holds each part to the Prolog compiler's output:

FrameSlots.v210 lines

Stack slots for temporaries (frame_slots.pl's temp_slots/7, with shared pools): each temporary gets a slot of its pool, and two whose live intervals are strictly disjoint may share one.

Fuse.v304 lines

Fusion, the first step of the Fil-C backend (filc_amd64.pl's fused_blocks/5): each check of the checked IR and the raw access after it, which reads the check's proof, become one instruction at one index, the access now at the checked pointer itself.

IrTerm.v583 lines

The checkedchecked IR nanofilThe two stages of the IR. Unchecked IR leaves Fil-C's checks implicit in every load and store at a p address; checked IR states every check, every raw access and the proof it uses, so the validator can see that each access is covered. A module's stage is read off its vocabulary, never a flag (ir:module_stage/2). IR back as Prolog terms: the encoders of the syntax of Syntax.v, the inverse of Transport.v's decoders, so that the backend can print an instruction as the very term the Prolog compiler printed it as (nanofilabi − termsFILE).

IrText.v875 lines

A reader of IR text (src/ir_text.pl): a module written as Prolog clauses, one func/5, data/4, alias/3 or context/2 term per item, which the Prolog compiler reads with read_term/3.

Layout.v404 lines

Where a function's plan lives below %rbp, and the names its code uses: filc_amd64.pl's layout/4, its function context, its labels and abi_symbol/3, with the short ways to write a line that the emission (Emit.v and the files it calls) is built from.

Liveness.v166 lines

Liveness of temporaries over fused blocks (cfg.pl's temp_liveness/3): the temporaries live on entry to and on exit from each block, reachable or not, the least solution of

Nfb.v109 lines

NFB (docs/nfb.md) for the modules of Syntax.v: encode writes a module's words and decode reads them back, in place of the term the Prolog compiler prints and Transport.v's decode_module reads.

NfbProof.v81 lines · 5 lemmas

What NFB's Gallina reader and writer (NfbTerm.v, Nfb.v) are proved to do (docs/nfb.md, Relation to the term form and the Rocq model).

NfbRead.v2996 lines · 148 lemmas · 4 axioms

NFB's term reader gives back what its writer wrote (NfbTerm.v, docs/nfb.md): for every module term t that encode_term writes with NAMES, read_term reads the words back as t itself, says whether they had NAMES, and those are words encode_term writes for t with that answer, which module_words keeps whole (read_encode_term).

NfbTerm.v1767 lines

NFB, the bytecode of a nanofil module (docs/nfb.md), read and written at the level of Prolog terms: the Gallina twin of src/nfb.pl, which must write the very same words.

NfbTotal.v390 lines · 25 lemmas

NFB's Gallina reader is total and its fuel never runs out (docs/nfb.md, Relation to the term form and the Rocq model).

NfbTransport.v532 lines · 47 lemmas

The term half of NFB's round trip (docs/nfb.md): a module that Transport.v's decode_module reads from any term is read back from the term Nfb.v's enc_module writes for it (decode_enc_module), and no item of that term is a context item (enc_module_no_context).

Order.v231 lines

Prolog's standard order of terms, and the sorted lists the Prolog compiler makes with it: sort/2, msort/2 and the ordsets of library(ordsets).

Pizlonate.v738 lines

# Pizlonation

Plan.v285 lines

The ABI plan of a function, as filc_abi.pl's abi_function/10 states it before any register or frame offset is chosen: a frame of named slots, entry actions, blocks whose calls, getters and returns are lists of ABI actions, and the function's public object.

PlanTerm.v264 lines

A plan as the term the Prolog compiler writes for it (filc_abi.pl's abi_function/10), and a module's thunks as its thunks(List).

Promote.v780 lines

# Promotion of memory slots to temporaries

Regs.v3234 lines

# Whole-function register allocation and selection

RegsProof.v764 lines · 32 lemmas

# Soundness proofs for Regs.v

TermCfg.v411 lines

# The control-flow graph of an unchecked function

Text.v69 lines

Text as the backend builds it: a list of parts, each a string, which the driver writes one after another.

rocq/backend/crane/

CraneExtract.v23 lines

# The backend's compiler, extracted to C++ by Crane

CraneMap.v135 lines

# How Crane writes the stdlib's numbers and strings in C++

CraneSelfTest.v176 lines

# The C++ mappings against vm_compute

rocq/glibc/

GlibcLogic.v154 lines · 2 lemmas

What the proofs of programs linked with user glibc's IR share (docs/glibc-ir.md): a raw load through a read-only capability, Iris adequacyadequacy nanofilAdequacy is the one theorem that ties a program logic to the machine: if a program's proof in the logic can be derived, then no state any of its runs reaches fails. It is proved once; after it, proving a program never panics is deriving its proof, with no reasoning about runs. for a program that starts owning pieces of its initial memory, and tactics that take a step whose values are all known by computing it.

LenCode.v114 lines

The checked module nanofil -O makes of rocq/glibc/len.c with user glibc's string/strlen.os, linked by rocq/link.pl, as a term.

LenLogic.v225 lines · 12 lemmas

rocq/glibc/len.c, linked with nanofil's IR of user glibc's string/strlen.c, through the program logic of Logic.v (docs/glibc-ir.md).

SayCode.v123 lines

The checked module nanofil -O makes of rocq/glibc/say.c with user glibc's string/strlen.os io/write.os, linked by rocq/link.pl, as a term.

SayLogic.v245 lines · 10 lemmas

rocq/glibc/say.c, linked with nanofil's IR of user glibc's string/strlen.c and io/write.c, through the program logic of Logic.v (docs/glibc-ir.md).

StrlenBits.v440 lines · 37 lemmas

The bit facts glibc's word-at-a-time strlen rests on (StrlenLogic.v, docs/glibc-ir.md).

StrlenLogic.v357 lines · 8 lemmas

A triple for glibc's own __strlen, as nanofil compiles user glibc's string/strlen.c (docs/glibc-ir.md): for any string, not one literal, over any registry and world, so a program linked with glibc's strlen uses it as a rule at its call.

ZsysWrite.v261 lines · 5 lemmas

A contract at libpizlo's boundary: zsys_write, the pizlonated write(2) that user glibc's write calls (docs/zsys.md, docs/glibc-ir.md).

rocq/spikes/

IrisHeap.v351 lines · 14 lemmas

Spike: a ghost heap of pieces for the Iris instantiation of nanofil's machine (IrisLang.v), and the generic proof rules a program proof applies at each step.

IrisLang.v175 lines · 6 lemmas

Spike: nanofil's core machine as an Iris language, and Iris adequacy as a proof of never_panics.

IrisListSum.v483 lines · 18 lemmas

Spike: spikes/listsum.c proved never to panic through Iris, with the ghost heap and rules of IrisHeap.v, the same theorem the hand-rolled spike proves.

ListSum.v86 lines · 6 lemmas

The program both logic spikes prove, shared by them: spikes/listsum.c, which builds a linked list of n nodes on the collected heap (__builtin_alloca, which Fil-C places there), then calls sum, which walks it and adds each node's value.

ListSumCode.v64 lines

The checked module nanofil -O makes of rocq/spikes/listsum.c, as a term.

ListSumLogic.v430 lines · 23 lemmas

Spike: spikes/listsum.c through the program logic of Logic.v.

Sep.v935 lines · 88 lemmas

A small separation logic over the model's memory, hand-rolled: the first of the two spikes of docs/logic.md.

SepListSum.v620 lines · 21 lemmas

The listsum spike proved with the hand-rolled separation logic of Sep.v (docs/logic.md): spikes/listsum.c never panics, with no premise, under any runtime, the interpreter's among them.

rocq/theories/

Ahead.v280 lines · 11 lemmas · 1 axiom

Campaign 3's scheduled checkscheck_ahead nanofilcheck_ahead(Lo, Hi, Rights, Align, AHi) is a check of [Lo, Hi) whose own access needs only [Lo, AHi): the bytes [AHi, Hi) are checked early for later accesses through the same base, as filcc's check scheduler does. It may trap earlier than the reference program, but only on runs that would trap later anyway.: what the validator's backward pass for check_ahead computes, point by point (formal.md, Campaign 3; rocq.md, Facts ahead; schedule.md).

Buffer.v333 lines · 9 lemmas

A program with a heap object, proved never to panic: rocq/programs/buffer.c, which allocates a buffer of four longs (__builtin_alloca, which Fil-C places in the collected heap), fills it, then sums p[i % 4] for i from 0 while i < n, for every int n (BufferCode.v, checked current by rocq/programs.sh).

BufferCode.v56 lines

The checked module nanofil -O makes of rocq/programs/buffer.c, as a term.

BufferLogic.v311 lines · 14 lemmas

rocq/programs/buffer.c through the program logic of Logic.v.

CallbackLogic.v258 lines · 9 lemmas

Exact-state adequacyadequacy nanofilAdequacy is the one theorem that ties a program logic to the machine: if a program's proof in the logic can be derived, then no state any of its runs reaches fails. It is proved once; after it, proving a program never panics is deriving its proof, with no reasoning about runs. for retained void callbacks.

Cfg.v246 lines

The control-flow graph (CFG) of a function and its dominatorsdominance nanofilBlock A dominates block B when every path from the entry to B passes through A. The validator decides it with the dominator tree's preorder intervals: each label gets the numbers of its subtree, and A dominates B when B's number lies in A's interval., transcribed from cfg.pl: func_cfg/2, cfg_idoms/2 (Cooper, Harvey and Kennedy, "A Simple, Fast Dominance Algorithm"), dom_children/3, dom_intervals/3 and dominates_by_interval/3.

Chain.v622 lines · 27 lemmas · 5 axioms

Campaign 3's reuse formsreuse nanofilReuse is using earlier evidence instead of a new check. --checks=reuse deletes a check whose access an earlier live proof already covers, so the access reads that proof; it works across plain edges and for related pointers at a constant offset (check_reuse:reuse_checks/2, m7.md, round 3). A reuse form is any op that trusts evidence other than a check just before it: renew, renew_hull, half_check, renew_if, check_limit and check_ahead., part one: what a frame may read off the single definitionssingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point. that dominatedominance nanofilBlock A dominates block B when every path from the entry to B passes through A. The validator decides it with the dominator tree's preorder intervals: each label gets the numbers of its subtree, and A dominates B when B's number lies in A's interval. its point (formal.md, Campaign 3; rocq.md, Reading single definitions).

Composition.v363 lines · 13 lemmas

A trusted puts contract with one continuous logical stdout and registration inventory.

ContractFrame.v284 lines · 13 lemmas · 1 axiom

The program logic's frame for external callsexternal call nanofilAn external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the runtime and is stuck at every other. A contract is Campaign 4's trusted description of one external function: its ABI, the caller's premises, the roots it may write, what it may release or allocate, its observations and its endings. (Logic.v, docs/logic.md): what a call through a contract leaves of the ghost heap of Heap.v.

CountCode.v47 lines

The checked module nanofil -O makes of rocq/programs/count.c, as a term.

CountLogic.v301 lines · 15 lemmas

rocq/programs/count.c through the program logic of Logic.v: a helper with its own specification, called in a loop, with memory read after each call.

Coverage.v254 lines · 13 lemmas

Campaign 3's coverage lemma (docs/formal.md, Campaign 3; docs/rocq.md, The coverage lemma): a raw accessraw access nanofilA raw access is a checked-stage memory access that does no checking of its own and names the proof that covers it: raw_load, raw_store, raw_load_pointer, raw_store_pointer, raw_cas and raw_call (ir:covered_access/6). that a passed checkcheck Fil-CAn access check: check(Lo, Hi, Rights, Align) of a pointer P traps unless P's capability permits Rights on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a proof of class a. check_local does the same for a named local, and check_function yields a function proof of class f (ir:op_kind/2, pizlonate:checked_access/4). covers, as ir.pl's covered_access/6 says, does not give uncheckedunchecked nanofilunchecked(Why) is the outcome of a raw access its capability does not allow, or of a reuse form whose trust was false: a check was missing or too weak, which only a broken pass produces. It is neither undefined behaviour nor a trap, so it refines nothing (interp:raw_res/2)..

Cycle.v277 lines · 8 lemmas

A loop whose trip count is the input, proved never to panic: rocq/programs/cycle.c, the sum of n longs read in turn from a read-only global array of four, xs[i % 4] for i from 0 while i < n, for every int n (CycleCode.v, checked current by rocq/programs.sh).

CycleCode.v43 lines

The checked module nanofil -O makes of rocq/programs/cycle.c, as a term.

Diagnostics.v203 lines · 8 lemmas

GNU error has two different continuations: status zero returns void; nonzero requests soft exit after the diagnostic.

Dominance.v1615 lines · 81 lemmas · 4 axioms

What the dominator intervalsdominance nanofilBlock A dominates block B when every path from the entry to B passes through A. The validator decides it with the dominator tree's preorder intervals: each label gets the numbers of its subtree, and A dominates B when B's number lies in A's interval. of Cfg.v mean (formal.md, Campaign 3; rocq.md, Dominance).

Doomed.v1649 lines · 61 lemmas · 5 axioms

Campaign 3's scheduled checkscheck_ahead nanofilcheck_ahead(Lo, Hi, Rights, Align, AHi) is a check of [Lo, Hi) whose own access needs only [Lo, AHi): the bytes [AHi, Hi) are checked early for later accesses through the same base, as filcc's check scheduler does. It may trap earlier than the reference program, but only on runs that would trap later anyway. along runs: a doomed framedoomed frame nanofilA frame is doomed after a check_ahead whose early bytes failed: the check yields its pointer anyway and the frame records the failure, because the validator promised that the frame will reach an access that fails on those bytes before anything observable happens. never runs to uncheckedunchecked nanofilunchecked(Why) is the outcome of a raw access its capability does not allow, or of a reuse form whose trust was false: a check was missing or too weak, which only a broken pass produces. It is neither undefined behaviour nor a trap, so it refines nothing (interp:raw_res/2). (formal.md, Campaign 3; rocq.md, The doomed frame; schedule.md).

Ending.v418 lines · 9 lemmas

Exit requests precede terminal external dispatch.

Evidence.v779 lines · 41 lemmas

Campaign 3's evidenceevidence nanofilEvidence is whatever discharges an access's requirement, the authority over the bytes it touches. Today it is a check immediately before the access, an earlier heap check whose live fact still holds, or a reuse form's trust: for renew a dominating check, for renew_if a guard's span test. invariant, at one instruction (docs/formal.md, Campaign 3, Proof persistence; docs/rocq.md, The evidence invariant, instruction by instruction).

ExitMemory.v1153 lines · 39 lemmas

A selected memory view of user-glibc's exit registry, not an executor or proof of native satisfaction.

ExternalCalls.v5562 lines · 145 lemmas

Campaigncampaign nanofilA 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. 4's trusted external callexternal call nanofilAn external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the runtime and is stuck at every other. A contract is Campaign 4's trusted description of one external function: its ABI, the caller's premises, the roots it may write, what it may release or allocate, its observations and its endings. boundary (libc-contracts.md, milestone 1).

ExternalMachine.v901 lines · 21 lemmas

Campaigncampaign nanofilA 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. 4's guarded, labelled extension of Machine.v (milestone 2): a machinemachine nanofilThe machine of a runtime R, MachineR, is what one thread's program sees run under R: Semantics.v's steps, plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs. whose steps carry the external callexternal call nanofilAn external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the runtime and is stuck at every other. A contract is Campaign 4's trusted description of one external function: its ABI, the caller's premises, the roots it may write, what it may release or allocate, its observations and its endings. events of ExternalCalls.v.

Extract.v31 lines

Extractionextraction nanofilExtraction compiles the Rocq model to OCaml so that it can be run beside the Prolog on the same inputs. judge is the extracted function that reads one run line nanofil printed, runs it in the model, and answers agree, disagree, outside or stuck_both. of the model to OCaml: the decoder (decode_module), 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.'s instance of the semantics, and judge, which the driver (extraction/main.ml) applies to every line nanofiloutcomes prints, and judge_valid, which it applies to rocq/mutants.pl's 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. verdicts (Transport.v), and the validator itself: Validate.v's valid_items and valid_func, and ValidFast.v's valid_items_fast, valid_func_fast and valid_fast, which answer as they and valid do.

Formatting.v454 lines · 3 lemmas

Hello's reached plain formatting calls, not the older fortified-symbol census.

Getopt.v589 lines · 9 lemmas

Trusted getopt_long boundary.

GetoptLogic.v188 lines · 8 lemmas

A program reads optarg and optind straight from libc's cells, which getopt rewrites at every call.

Guard.v463 lines · 12 lemmas · 5 axioms

Campaign 3's reuse formsreuse nanofilReuse is using earlier evidence instead of a new check. --checks=reuse deletes a check whose access an earlier live proof already covers, so the access reads that proof; it works across plain edges and for related pointers at a constant offset (check_reuse:reuse_checks/2, m7.md, round 3). A reuse form is any op that trusts evidence other than a check just before it: renew, renew_hull, half_check, renew_if, check_limit and check_ahead., part three: renew_ifrenew_if nanofilA renew whose bounds come from a guard: renew_if(Lo, Hi, Rights, Align) of [P, G] is exactly a check of P, but where the span test G passed it natively tests only the flags and alignment, and where G failed it runs the full check out of line. The validator accepts it through ir:guard_covers/5, following P's guard chain (ir:guard_chain/3). and check_limit (formal.md, Campaign 3; rocq.md, Guards and limits).

Heap.v543 lines · 34 lemmas

The ghost heap of the program logic (Logic.v): what each piece of memory holds, when a ghost heap of pieces agrees with the memory, and the ownership of a list of pieces in Iris's gen_heap.

HelloClose.v736 lines · 18 lemmas

GNU Hello's closeout helpers through the separation logicseparation logic IrisSeparation logic is Hoare logic whose assertions describe the part of memory a piece of code owns. ℓ ↦ v owns one cell, P ∗ Q holds of memory that splits into a part where P holds and a disjoint part where Q holds, and the frame rule lets code proved on what it owns run inside any larger memory, which it leaves alone. Aliasing is ruled out by the assertions, not by side conditions..

HelloCode.v3538 lines

The checked module nanofil -O makes of GNU Hello 2.12.3 (nanofil-hello-O), linked by rocq/link.pl, as a term.

HelloConv.v1140 lines · 14 lemmas

GNU Hello's conversion of its greeting through the program logic of Logic.v (docs/logic.md): libc's mbrtowc, and gnulib's rpl_mbrtowc and rpl_mbsrtowcs around it, which main calls to turn the greeting into wide characters.

HelloConvDefs.v371 lines · 26 lemmas

The definitions and lemmas of HelloConv that do not need the program logic: memory read as lists, spans of live objects, a block after a call, libc's private state, and the IR of gnulib's rpl_mbrtowc and rpl_mbsrtowcs.

HelloDiagnosticChecks.v535 lines · 16 lemmas

Logical controls for Hello's four-argument diagnostic binding.

HelloJoin.v804 lines · 10 lemmas

HelloMain proves main from its entry up to the greeting at iw_1.join (main_to_join).

HelloLeaf.v379 lines · 22 lemmas

GNU Hello's leaf functions through the program logic of Logic.v (docs/logic.md, "GNU Hello through the logic", milestone 2).

HelloLocale.v521 lines · 26 lemmas

GNU Hello's locale helpers through the program logic of Logic.v (docs/logic.md): gnulib's hard_locale and the setlocale_null_r chain beneath it, which rpl_mbrtowc calls to decide whether a byte may stand for itself.

HelloMain.v2360 lines · 60 lemmas

Main's proof calls the triples of every Hello layer, so it applies each layer's functor to one Logic instance: two applications of Logic have distinct expressions, and their triples could not be combined.

HelloModule.v82 lines · 3 lemmas

GNU Hello as the model sees it: one checked module, linked from the objects nanofil compiles for nanofil − hello − O (Campaigncampaign nanofilA 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. 7, docs/logic.md).

HelloName.v381 lines · 16 lemmas

GNU Hello's set_program_name through the program logic of Logic.v (docs/logic.md, "GNU Hello through the logic", milestone 2).

HelloProgName.v311 lines · 6 lemmas

set_program_name preserves strings, not just capabilities.

HelloReach.v243 lines · 12 lemmas

Reference closure of the linked GNU Hello image, including function addresses passed as callbacks and symbols stored in data.

HelloStdio.v1566 lines · 49 lemmas

Admission of Hello's actual version/footer literals.

HelloVersion.v1566 lines · 48 lemmas

GNU Hello's version and help helpers through the program logic.

HelloWorld.v656 lines · 24 lemmas

One fixed-launch Hello world.

Hi.v586 lines · 29 lemmas · 1 axiom

The source-shaped body of tests/c/prog/hi.c at the trusted libc boundary.

HiArtifact.v126 lines · 5 lemmas

The application proof describes the checked module actually generated from hi.c.

HiCode.v26 lines

The checked module nanofil -O makes of tests/c/prog/hi.c, as a term.

HiLogic.v229 lines · 9 lemmas · 1 axiom

tests/c/prog/hi.c through the program logic of Logic.v, with puts called through Campaigncampaign nanofilA 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. 4's contract (puts_contract).

Identity.v420 lines · 30 lemmas

Objects last: what a run of Machine R, the machinemachine nanofilThe machine of a runtime R, MachineR, is what one thread's program sees run under R: Semantics.v's steps, plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs. over a 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. R, leaves of the objects it finds (docs/formal.md, Campaign 3; docs/rocq.md, Identities persist).

Ieee.v336 lines

IEEE 754 arithmetic with integers only, transcribed from ieee.pl: binary32 (s), binary64 (d) and the x87 80-bit extended format (x), rounding to nearest, ties to even.

Interval.v700 lines · 22 lemmas · 1 axiom

What ir.pl's offset intervalsoffset interval nanofilAn offset interval bounds the values an integer name can hold, derived through its single definitions, so that a flight's offset from its base is known to lie in [Lo, Hi]. At class w it bounds the signed word itself; at l it bounds some integer congruent to the value modulo 2^64, which is all address arithmetic needs. derive, and that they hold (Campaign 3; docs/rocq.md).

Invariant.v720 lines · 34 lemmas

Campaign 3's run-level evidenceevidence nanofilEvidence is whatever discharges an access's requirement, the authority over the bytes it touches. Today it is a check immediately before the access, an earlier heap check whose live fact still holds, or a reuse form's trust: for renew a dominating check, for renew_if a guard's span test. invariant, stated (docs/rocq.md, The evidence invariant over runs): what holds at each point of a frameframe nanofilA configuration is the whole state of a run in the model: the running frame, the suspended callers (each with how it will read its callee's result), memory, and the fuel left. A frame is one invocation: its function, its temporaries, its named locals, whether it is doomed, and its point. of Machine R (Machine.v), and the lemmas each kind of step needs.

Language.v1107 lines · 49 lemmas

Nanofil's machinemachine nanofilThe machine of a runtime R, MachineR, is what one thread's program sees run under R: Semantics.v's steps, plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs., with the external callsexternal call nanofilAn external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the runtime and is stuck at every other. A contract is Campaign 4's trusted description of one external function: its ABI, the caller's premises, the roots it may write, what it may release or allocate, its observations and its endings. of a contract registry, as an Iris language whose evaluation context is the stack of callers, and Iris adequacyadequacy nanofilAdequacy is the one theorem that ties a program logic to the machine: if a program's proof in the logic can be derived, then no state any of its runs reaches fails. It is proved once; after it, proving a program never panics is deriving its proof, with no reasoning about runs. as a proof of never_panics and of the labelled machine's safety.

LentLogic.v549 lines · 18 lemmas · 1 axiom

Strings the world lends, in the program logic of Logic.v (docs/logic.md).

Libc.v1353 lines · 28 lemmas

Hello's composite trusted libc boundary.

LibcDiagnosticLogic.v582 lines · 10 lemmas

Returning diagnostics on the consumer's same libc world and machine.

LibcErrnoLogic.v481 lines · 18 lemmas

Selected FILE calls with program-owned errno bytes.

LibcExit.v207 lines · 7 lemmas

Hard exit as a trusted nonreturning external-call summary over the consumer's exact machine.

LibcStreamAdapter.v1225 lines · 36 lemmas

World-owned callback snapshots, separate from locale string names.

LibcStreamLogic.v199 lines · 9 lemmas

Program-memory and selected-FILE world frames over the logic's exact machine.

LibcStreamTokens.v289 lines · 11 lemmas

Callback stream tokens retain native handle lives but do not own private FILE bytes.

LibcStreams.v687 lines · 24 lemmas

Composite stdout/stderr contracts.

Libio.v706 lines · 15 lemmas

A capabilitycapability Fil-CA capability is the authority half of a Fil-C pointer: which object, if any, its address may be used to access. In the model a capability is an identity, never bounds; the object's current bounds live in its region, so freeing through one alias empties what every alias sees.-backed memory view of the pinned byte stdout (milestone 3c).

Linked.v360 lines · 6 lemmas

Retained void callbacks at the labelled program boundary.

Locale.v793 lines · 17 lemmas

Trusted setlocale boundary for the selected glibc categories.

LocaleLogic.v390 lines · 17 lemmas

The locale world in the program logic of Logic.v (docs/logic.md, "Strings the world lends"): locale_wi, the world interpretation of a program that calls setlocale, over Campaigncampaign nanofilA 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. 4's locale_world (Locale.v), and what it gives the triples of LentLogic.v and HelloLocale.v.

Logic.v1383 lines · 52 lemmas

The program logic of nanofil's core machinemachine nanofilThe machine of a runtime R, MachineR, is what one thread's program sees run under R: Semantics.v's steps, plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs. on the language of Language.v, whose evaluation context is the stack of callers: a ghost heap of pieces as Iris's state interpretation, a small assertion vocabulary over it, and one weakest-precondition rule per instruction form, each the lifted reading of its rule in StepRules.v.

Machine.v634 lines · 39 lemmas

Campaign 3's machinemachine nanofilThe machine of a runtime R, MachineR, is what one thread's program sees run under R: Semantics.v's steps, plus R's allocations and R's actions at safepoints. mstep is its step relation and mreachable its runs.: Semantics.v's steps run over a Runtime (Runtime.v), and the first invariant of every run, that the runtime stays readyready nanofilA runtime is ready in a memory when its own state and that memory agree well enough that its next allocation is fresh. Readiness is the runtime's invariant: the axioms about allocation and the address space are stated only for ready states. to allocate (formal.md, Campaign 3; rocq.md).

Maps.v202 lines · 8 lemmas

Finite maps keyed by names, the model's counterpart of library(assoc), which ir.pl and cfg.pl use for every table indexed by a blockblock nanofilA block is a labelled straight line of a function: phis, then instructions, then one jump (goto, branch, ret, rets, ret, unreachable). The first block is the entry and has no phis; its label is the name edges use. label or a temporarytemporary nanofilA temporary is a function-local IR name, tmp(N), holding one word of one class. Parameters, phis and instructions define temporaries; operands read them. Names are ground terms, compared only for equality: no logic variable appears in IR..

MemLogic.v1269 lines · 45 lemmas

Blocks of memory in the program logic of Logic.v, and the triples of libc's memory calls derived from Campaigncampaign nanofilA 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. 4's contracts.

Memory.v321 lines

Memory and Fil-C's access check, transcribed from interp.pl's Memory section.

Ops.v591 lines

Integer arithmetic and the evaluation of ops, transcribed from interp.pl's Operations section: alu/4, additive_res/4 and kind_res/8 for the core subset.

Panics.v171 lines · 3 lemmas

Campaign 7's property, never_panics: no runrun nanofilA run is the execution of one function of a module from its initial memory, step after step, to an outcome or forever. The theorems quantify over every state a run reaches, not over its outcome, so a run that never ends is covered too. of a program from any admissible input ever reaches a failure (formal.md, Campaign 7).

Persistence.v453 lines · 21 lemmas

Campaign 3's evidenceevidence nanofilEvidence is whatever discharges an access's requirement, the authority over the bytes it touches. Today it is a check immediately before the access, an earlier heap check whose live fact still holds, or a reuse form's trust: for renew a dominating check, for renew_if a guard's span test. invariant over whole runs (docs/formal.md, Campaign 3, Proof persistence; docs/rocq.md, The evidence invariant over runs).

Pieces.v217 lines · 13 lemmas

The resource model of the program logic (Logic.v, docs/logic.md), shared with the logic spikes: the pieces of memory an assertion may own, keyed by identityidentity nanofilAn object's identity is its base, the number its capabilities name; it outlives the object's bounds, so a freed object keeps its identity. One memory persists from another when every object of the first is in the second as it was, or freed: no identity is lost, moved or given to a new object., and the facts about the whole memory that make owning them mean something.

Program.v1015 lines · 41 lemmas · 1 axiom

Application execution over the coupled libc world.

Renew.v943 lines · 30 lemmas · 10 axioms

Campaign 3's reuse formsreuse nanofilReuse is using earlier evidence instead of a new check. --checks=reuse deletes a check whose access an earlier live proof already covers, so the access reads that proof; it works across plain edges and for related pointers at a constant offset (check_reuse:reuse_checks/2, m7.md, round 3). A reuse form is any op that trusts evidence other than a check just before it: renew, renew_hull, half_check, renew_if, check_limit and check_ahead., part two: renewrenew nanofilA renew reuses an earlier check's bounds: renew(Lo, Hi, Rights, Align) of [Q1, P] trusts the dominating check that made Q1 for P's bounds and tests again only what a free changes, that the object is not freed (and, for a write, not read-only). It is the −O default (check_reuse:renew_checks/2, m7.md, round 4)., renew over a hullrenew_hull nanofilThe hull of several passed checks of one object is the interval from the least lower end to the greatest upper end of their spans; since an object is one interval, every byte of the hull is in it. renew_hull(Lo, Hi, Rights, Align) of [QL, QH, P] is a renew whose bounds two such checks give: QL's from at or below P+Lo, QH's to at or above P+Hi. and half checkhalf_check nanofilhalf_check(Bound, Lo, Hi, Rights, Align) of [Q1, P] is exactly a check of [Lo, Hi) at P that natively tests only one bound, upper or lower; the other end is known from Q1's earlier check of the same object, P being at a known distance from Q1's pointer. (formal.md, Campaign 3; rocq.md, Renew and the half check).

Run.v199 lines

Running a function of a module as interp:run/5 does: prepare the module's initial memory, call the function, and take stepsstep nanofilA step moves a configuration on by one thing: entering a block (its phis, one unit of fuel), one instruction, or one jump. step answers Next with the next configuration, Done with an outcome, Fresh for an allocation that waits for a base, or Stuck. until an outcomeoutcome nanofilAn outcome is how a run ends: a return, unreachable, undefined behaviour, a trap, unchecked, or running out of fuel. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares., choosing each allocation's base as a 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. does.

Runtime.v612 lines · 23 lemmas · 14 axioms

The runtime as axiomsruntime 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.: Campaign 2's module type Runtime, and 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.'s instance of it (formal.md, runtime-axioms.md, which gives each axiom's source in the runtime).

ScanCode.v38 lines

The checked module nanofil -O makes of rocq/programs/scan.c, as a term.

ScanLogic.v248 lines · 11 lemmas · 1 axiom

rocq/programs/scan.c through the program logic of Logic.v, with strlen, strchr and puts called through Campaigncampaign nanofilA 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. 4's contracts.

Selected.v697 lines · 14 lemmas

Selected libc lifecycle segments, over the existing external-call effect discipline.

Semantics.v877 lines

The small-stepstep nanofilA step moves a configuration on by one thing: entering a block (its phis, one unit of fuel), one instruction, or one jump. step answers Next with the next configuration, Done with an outcome, Fresh for an allocation that waits for a base, or Stuck. semantics of the core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside. of the checked IRchecked IR nanofilThe two stages of the IR. Unchecked IR leaves Fil-C's checks implicit in every load and store at a p address; checked IR states every check, every raw access and the proof it uses, so the validator can see that each access is covered. A module's stage is read off its vocabulary, never a flag (ir:module_stage/2)., transcribed from 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.'s run/5 (interp.pl).

Shutdown.v412 lines · 19 lemmas

Serialized shutdown of the selected user-glibc: callbacks, stdout obligations and a soft or hard host-exit handoff.

Single.v962 lines · 51 lemmas

Campaign 3's single-definition invariantsingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point. over runs (docs/formal.md, Campaign 3; docs/rocq.md, The single-definition invariant).

Sites.v369 lines · 17 lemmas

Where a name is defined, and what definitions_dominate/3 says of its uses (formal.md, Campaign 3; rocq.md, Where a name is defined).

SlotCode.v78 lines

The checked module nanofil -O makes of rocq/programs/slot.c, as a term.

SlotLogic.v567 lines · 24 lemmas

rocq/programs/slot.c through the program logic of Logic.v: a callee that owns memory across calls, in the shape of gnulib's quotearg.

Soundness.v312 lines · 10 lemmas

Campaign 3's theorem, valid_no_unchecked: if the validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked. accepts a module, no runrun nanofilA run is the execution of one function of a module from its initial memory, step after step, to an outcome or forever. The theorems quantify over every state a run reaches, not over its outcome, so a run that never ends is covered too. of it that starts readyready nanofilA runtime is ready in a memory when its own state and that memory agree well enough that its next allocation is fresh. Readiness is the runtime's invariant: the axioms about allocation and the address space are stated only for ready states. ever steps to uncheckedunchecked nanofilunchecked(Why) is the outcome of a raw access its capability does not allow, or of a reuse form whose trust was false: a check was missing or too weak, which only a broken pass produces. It is neither undefined behaviour nor a trap, so it refines nothing (interp:raw_res/2). (formal.md, Campaign 3; rocq.md, No run is unchecked).

Startup.v1204 lines · 40 lemmas

The Fil-C launcher's entry contract, before libc calls main (milestone 3a).

Stdio.v324 lines · 7 lemmas

A logical stdout protocol, not a native FILE representation (milestone 3b).

StepRules.v503 lines · 33 lemmas

What one stepstep nanofilA step moves a configuration on by one thing: entering a block (its phis, one unit of fuel), one instruction, or one jump. step answers Next with the next configuration, Done with an outcome, Fresh for an allocation that waits for a base, or Stuck. gives, rule by rule: for each instruction form of the core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside. and each jump, the configuration step reaches from a frame at it, under premises small enough to compute on their own.

Steps.v298 lines · 22 lemmas

What one stepstep nanofilA step moves a configuration on by one thing: entering a block (its phis, one unit of fuel), one instruction, or one jump. step answers Next with the next configuration, Done with an outcome, Fresh for an allocation that waits for a base, or Stuck. of Semantics.v's step does to the running frameframe nanofilA configuration is the whole state of a run in the model: the running frame, the suspended callers (each with how it will read its callee's result), memory, and the fuel left. A frame is one invocation: its function, its temporaries, its named locals, whether it is doomed, and its point., as Campaign 3's run-level invariant (Persistence.v) reads it.

Streams.v332 lines · 6 lemmas

Selected stream queries and close, over explicit projections of the application's libc world.

StringLogic.v624 lines · 28 lemmas

C strings in the program logic of Logic.v, and the triples of the libc string calls derived from Campaigncampaign nanofilA 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. 4's contracts.

Sum.v258 lines · 16 lemmas

The first program proved never to panic: rocq/programs/sum.c, a loop that sums a read-only global array of four longs, as nanofil -O compiles it (SumCode.v, checked current by rocq/programs.sh).

SumCode.v42 lines

The checked module nanofil -O makes of rocq/programs/sum.c, as a term.

Symbolic.v412 lines · 4 lemmas

Symbolic execution of the model's stepstep nanofilA step moves a configuration on by one thing: entering a block (its phis, one unit of fuel), one instruction, or one jump. step answers Next with the next configuration, Done with an outcome, Fresh for an allocation that waits for a base, or Stuck., for proofs that a program never panics from assertions at its points (Cycle.v).

Syntax.v519 lines

The core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside. of the checked IRchecked IR nanofilThe two stages of the IR. Unchecked IR leaves Fil-C's checks implicit in every load and store at a p address; checked IR states every check, every raw access and the proof it uses, so the validator can see that each access is covered. A module's stage is read off its vocabulary, never a flag (ir:module_stage/2)., transcribed from ir.pl: its grammar as inductive types, one constructor per functor of the intermediate representation (IR), and the small tables of facts the semantics reads.

Term.v108 lines · 2 lemmas

Ground Prolog terms, the shape every nanofil product has before it means anything: an integer, an atom, a compound of a name and arguments, or a proper list.

Transport.v629 lines

Transporttransport nanofilTransport is the crossing between Prolog terms and the model: decoding a checked module that nanofil printed into Syntax.v's syntax, and encoding the model's outcome back as the term interp:run/5 would give, so that the two can be compared with ==. between Prolog terms and the model: decoding a checkedchecked IR nanofilThe two stages of the IR. Unchecked IR leaves Fil-C's checks implicit in every load and store at a p address; checked IR states every check, every raw access and the proof it uses, so the validator can see that each access is covered. A module's stage is read off its vocabulary, never a flag (ir:module_stage/2). module that nanofil printed (nanofiloutcomes FILE, main.pl's outcomes/3) into the syntax of Syntax.v, and encoding the model's outcomeoutcome nanofilAn outcome is how a run ends: a return, unreachable, undefined behaviour, a trap, unchecked, or running out of fuel. interp.pl and the model give the same outcomes term for term, which is what the outcome gate compares. as the term interp:run/5 would give, so the two can be compared with ==.

ValidFast.v204 lines · 8 lemmas

The validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked. with its single definitionssingle definition nanofilA single definition is a temporary with exactly one definition in its function: a parameter, a phi or an instruction. The reuse forms read relations only between such names (a flight and its base, a proof and the pointer it checked, a span test or limit and its pointer), and the single-definition invariant says those relations hold at run time wherever the definition dominates the running point. found through a name mapname map nanofilA name map is a finite map keyed by IR names, the model's counterpart of SWI-Prolog's library(assoc), which ir.pl and cfg.pl use for every table indexed by a label or a temporary: the single-definition map, the evidence indexes, dominator intervals., and the proof that it answers as Validate.v's valid does.

Validate.v2085 lines

The validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked. of checked IRchecked IR nanofilThe two stages of the IR. Unchecked IR leaves Fil-C's checks implicit in every load and store at a p address; checked IR states every check, every raw access and the proof it uses, so the validator can see that each access is covered. A module's stage is read off its vocabulary, never a flag (ir:module_stage/2)., transcribed from ir.pl's valid_module/1 for the core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals, touch, variadics and setjmp, which is validated as ir.pl does while its step is stuck, as the interpreter refuses it. A function that uses anything else decodes to IOutside.: valid_funcmd f is true exactly when ir.pl accepts the function f of the module md, checked stage, filc modemode nanofilA module's mode is plain or filc: filc if it uses anything Fil-C-specific (a p, a call to an external function, ...), plain otherwise, read off its contents (ir:module_mode/2).; valid_data and valid_alias do the same for the module's data objects and aliases.

Values.v85 lines

Run-time values, transcribed from interp.pl: capabilitiescapability Fil-CA capability is the authority half of a Fil-C pointer: which object, if any, its address may be used to access. In the model a capability is an identity, never bounds; the object's current bounds live in its region, so freeing through one alias empties what every alias sees., pointers and the wordsword nanofilA word is the value a temporary holds at run time: an integer, a pointer (an address with its capability), or a limit's opaque snapshot. The temporary's class says how it is read. a temporarytemporary nanofilA temporary is a function-local IR name, tmp(N), holding one word of one class. Parameters, phis and instructions define temporaries; operands read them. Names are ground terms, compared only for equality: no logic variable appears in IR. holds.

Walk.v558 lines · 35 lemmas

The evidence passevidence pass nanofilThe evidence pass is the validator's forward walk over a checked function: it tracks live facts and accepts each raw access only where its own check, a live fact or a reuse rule covers it. It visits the blocks once, in order; a block's entry facts are the meet over its incoming edges, with nothing carried over a poll edge or from a block not yet visited. read back for Campaign 3's run-level invariant (Persistence.v; rocq.md, The evidence invariant over runs).