A program logic for never_panics

November 2026. The brief for the campaign after formal.md's Campaign 7 proofs of single programs (formal.md, Campaign 7). It records a proposal mbrock received from another Fable instance, what the model already has that the proposal builds on, where the proposal misreads the model, what it would cost, and a recommendation. Beyond what "What exists" lists, only the two list-sum spikes are built, off the main path. The choice of Iris, and whether to start at all, is mbrock's. iris.md explains Iris itself, its history and model, and reads the Iris spike.

The proposal in one paragraph

Campaign 3 is already a program logic, with one fixed assertion language (the validator's facts), facts derived automatically, and adequacy proved once (valid_no_unchecked). never_panics needs that assertion language opened so each program brings its own facts, while keeping one adequacy theorem. The facts that keep a check from failing are about the heap's shape (this field points to a live 16-byte object; this string has a NUL), and they are global, so they should travel with ownership: separation logic, with a frame rule carrying everything a function does not touch across a call. The logic's weakest precondition is defined from the machine's step, with a panic counted as stuck and a refusal, an exit or the end of fuel as final, so that adequacy is never_panics itself. Its resources are keyed by object identity: a persistent meta fact, a live token that free consumes, and points-to cells with their aux capabilities. A check then splits into a spatial part (arithmetic over persistent facts) and a temporal part (live b), and raw accesses need no rule because Campaign 3 covers them. The runtime's freedom to free a live heap object at a safepoint becomes a premise on the runtime instance, not an axiom. Blocks get Floyd assertions (SSA temporaries are logical constants), functions get specs in a table with the frame rule and Löb induction for recursion, libc gets triples derived from ExternalCalls.v's contracts, and each object file is proved against its imports' specs. It recommends Iris (Cerise as prior art) and a first spike on gc.ir's list sum. Above the logic sits a ladder: validator facts, Campaign 5's certificates, RefinedC-style ownership types, then hand proofs, each a fragment of the one below, so Campaigns 5 and 7 merge.

What exists

So the degenerate logic and its adequacy exist, and three programs are proved with it. What does not exist is any separation: one invariant names everything the program holds, and a second function or a second object means rewriting it.

Where the proposal is right

• One adequacy theorem, an open assertion language. This is the right shape, and never_panics_by_invariant shows the adequacy end is cheap here: the machine already has the safety notion, so adequacy is an induction on mreachable. The open question is only how rich the assertions are.

• Ownership keyed by identity. Fil-C's memory is already that: regions by identity (region), bounds that change only at free, identities never reused in the model (free_keeps_ids), freed bytes retained (retention), capabilities in the aux. A meta fact is persistent because nothing after allocation changes what was allocated, and live is exactly what free changes. Buffer.v needed precisely these two facts and nothing about bytes.

• The spatial and temporal split. A check's bounds part is arithmetic over meta and the pointer's offset; its flag part is live. That matches Campaign 0's census categories and lets Campaign 5's certificates stay purely arithmetic.

• Raw accesses need no rule. Cycle.v and Buffer.v re-prove every raw load in bounds by symbolic execution, which valid_no_unchecked already guarantees for a valid module. A logic that takes Campaign 3's run invariant as a given only needs rules at the obligation sites and value rules for what a load returns. This would cut most of the per-program arithmetic.

• The safepoint premise belongs to the instance. Under Runtime.v as first written, a safepoint could free any live heap object (safepoint_lifetime), so never_panics was false for a program that holds one across a poll or a call. Buffer.v stated the premise as an antecedent, safepoint_keeps_live, which the interpreter meets; Hi.v's stdio_stable is the same kind of premise for stdio's objects. The safepoint axiom is now the collector's alone, collector_live (no region changes at a safepoint), which makes safepoint_keeps_live a lemma for every runtime, so the premise is gone.

• The ladder, and Campaign 5 as a fragment. A certificate checker that emits derivations in the logic is sound by adequacy, with no separate soundness proof against the machine.

Where it misreads the model

• "Raw accesses need no rule" has hypotheses. valid_no_unchecked needs the module valid and the run started ready (it no longer takes spares, which every runtime meets, by spares_any), and in the core machine an external call other than free is stuck, so it says nothing past one. For hi.c or Hello it must hold on Campaign 4's labelled machine (ExternalMachine.v preserves Campaign 3's invariants across calls, so this is near) and be combined with the logic's invariant: adequacy is then "the logic's state interpretation and Campaign 3's run invariant together are preserved", not the logic's alone.

• The safepoint rely is simpler than "handlers respect ownership". The model has no threads and no handlers: a safepoint is the runtime R's collector acting, and Runtime.v's collector_live says it changes no region, so no program states a rely at all. A signal handler or another thread is program code. In the model installing a handler (signal, sigaction) or starting a thread (pthread_create) is a call to an external with no contract, which ends the run as a failure, and the run is the program's whole execution after the trusted entry, with no handler installed and no other thread when it starts. That covers Hello, which installs no handler. The ownership-respecting rely returns when a handler is verified as program code, with an invariant that it frees only what it was handed, and in the concurrency inquiry. Its stability proof uses non_moving (bytes), aux_round_trip (stored capabilities) and collector_live (regions and identities, with rooting now a lemma from it), as the proposal says.

• Shared libc state is not Iris-shaped here. libc is not code in the model; it is trusted contracts over an abstract world with a rep relation to memory. The program does not touch a FILE's fields, so stdout is a first-order resource the program owns and lends to each call's contract, not a shared invariant between two pieces of code.

• The function pointers on the roadmap have known targets. Campaign 4 represents the exit registry as pinned and in memory (ExitMemory.v); close_stdout and the like are a case split on Fnf, first-order, as the proposal concedes.

• Recursion has fuel. The machine spends one unit of fuel per block entry, shared by the whole stack, and OutOfFuel is not a failure. An induction on fuel therefore gives Löb's rule for recursive functions without step-indexing; but not for a safepoint, which spends none (see the spikes below).

• A configuration is not an expression. Iris's language splits expression from state; a configuration holds the memory (c_mem), and the runtime's state sits beside it in mstate. An Iris instance needs a wrapper: expression the frames, callers and fuel; state the memory and R's state; a safepoint a step that changes only the state; a Done that is not a failure a value, and a failure stuck.

• gc.ir's sum is not a closed program. It takes the list from its caller and calls the external c_gc. never_panics over "any input" cannot say "the argument is a list", so the spike needs a function spec with a precondition, a caller (gc.ir's build, or a fixture that builds then sums), and either a contract for c_gc or a version without it.

What it costs, measured

The proof work in Cycle.v and Buffer.v did not go into the logic. The logic was a 25-line proof rule. It went into computing step, the transcribed interpreter, on abstract states fast enough:

Neither Iris nor a hand-rolled logic removes this. What removes it is a layer of step lemmas, one per instruction form of the core subset (about 25: let of each op class, check and the reuse forms, flight, raw load and store, alloc, the jumps), each proved once over an abstract environment and memory by the same tactics, so that a program proof never reduces step. In a separation logic these are the wp rules of the instructions. This layer is the bulk of the campaign whichever host is chosen.

Iris's own costs, concretely:

• Dependency. The pinned nixpkgs has rocqPackages.iris 4.5.0 and stdpp 1.13.0 beside Rocq 9.1.1, so it is a pin away, not a port; cache.nixos.org has both (measured in the spikes below).

• The literate pipeline. dterm-rocq's grammar (web/rocq, checked by parse.sh) does not yet read let ... in or fresh inside Ltac; Iris proofs are written in its proof mode (iIntros [Hl Hs], intro patterns in strings) with new notation (∗, -∗, ▷, |==>). The renderer and parse.sh would need to learn both before any Iris file is on the site.

• Term size. Iris's tactics are tuned for small expressions; a configuration that carries the function's body is large. The block_fact discipline would be needed there too.

• What it buys. Generic adequacy (here already cheap), invariants and ghost state (needed only for concurrency), Löb (replaceable by fuel), higher-order specs (not needed until a function pointer with an unknown target), and the proof mode, which is the real gain: framing and splitting separating conjunctions by hand is tedious and is where hand-rolled logics usually hurt.

A hand-rolled logic's costs: a heap of identity-keyed heaplets (each meta, live, cells) with disjoint union, a small separating conjunction with its frame lemma, the state interpretation and its stability under alloc, free and a frees-nothing safepoint, and tactics to frame. A first-order version of this is a few thousand lines; VST shows how large it gets when it must also do everything Iris does.

The list-sum spikes

mbrock asked for the spike overnight, both ways. Both are in rocq/spikes, off the main build: nothing in rocq/theories imports them, the quick gate and CI do not build them, and only their own check, nix build .#checks.x86_64-linux.nanofil-logic-spikes (spikes.nix), depends on Iris. Both prove the same statement about the same program, in Panics.v's terms:

Theorem listsum_never_panics :
  P.never_panics ls_module (TAtom "listsum") (fun xs => exists n rest, xs = WInt n :: rest).

The program is listsum.c, closed, so the core machine runs all of it: listsumn allocates n 16-byte nodes on the collected heap, links each with a checked pointer store, and calls sum, which walks the list with a check of each value, a lower half check and an aux pointer load for each next pointer, and a poll on the back edge. gc.ir's sum is the same loop with an external c_gc call in it, which needs Campaign 4's machine. keeps_live (no safepoint frees a live object), once Buffer.v's premise and the spikes', is now a lemma of Pieces.v from Runtime.v's collector_live (a safepoint changes no region), so the theorem holds for every runtime; PrintAssumptions of the interpreter's corollary is closed for both.

They share Pieces.v, the resource model: pieces keyed by identity (an object's life, one byte, one aux slot at an offset), the global fact that live objects are disjoint, and safepoint_shape: a safepoint keeps every region and every byte, and rewrites only aux slots that hold a freed object's capability (from collector_live, non_moving and aux_round_trip). Keying by identity is forced, not chosen: the model's fresh lets a new object take a freed one's addresses.

What each spike taught:

• The step is still the cost. In both, most of the program proof's compile time is computing step on an abstract state, as in Cycle.v and Buffer.v. Iris made it worse, not by itself but because wpc_next leaves the next configuration as an existential variable that the computed step must unify with: Symbolic.v's drop_wraps and decide_compares, which generalise or split, break that unification, so the Iris side wrote non-splitting copies, and the one undecidable comparison is split by hand. The step lemmas of the recommendation below remove this in both and would bring IrisListSum.v under the 35 s line.

• Framing by hand is where the hand-rolled logic hurts, as expected: footprints are predicates, so emp ** P is P only up to "the same pieces" (no extensionality), and the proofs were arranged never to eliminate emp; reassociating four-way stars for a node took explicit lemma chains. Iris's proof mode makes all of this vanish.

• Safepoints are where Iris clearly wins. A safepoint step leaves the expression as it was and changes the state; in Iris that is one Löb induction in the lifting lemma, and every later proof is silent about polls. The hand-rolled logic needs each function's assertions to be sp_stable and a lemma per function to say so. Cheap (0.5 s each, mechanical) but per program. Fuel does not help here, as this document claimed above: a safepoint spends no fuel.

• Calls need a design either way. The Iris language keeps the callers stack inside the expression, so there are no evaluation contexts and no wp_bind; the spike's call rule passes the caller's continuation as a wand. That frames for free but returns nothing to the caller, so a spec that hands the list back needs list segments or an ectx_language with the callers as the context. The hand-rolled spike's frame-generic step lemma is the same idea, first-order.

• Friction with Iris is real but bounded. Importing it swaps in ssreflect's rewrite (no by clause), ++ and + change scope, gen_heap's ↦ is local to its file, and Ltac cannot name a hypothesis that an intro-pattern string introduces. Each was found once.

• Both logics found something. The hand-rolled list predicate first lacked a node's 8-byte alignment, which sum's half check and pointer load test; without it lst p xs ** F admits lists on which sum traps.

• Iris is cheap to have. rocqPackages.iris 4.5.0 and stdpp 1.13.0 come from cache.nixos.org for the pinned Rocq 9.1.1; loading Iris and the compiled model together takes 2.5 s.

Recommendation

Iris, decided on this evidence rather than at a later spike's end as first recommended here. The two spikes are the same size (about 1,550 lines each) and prove the same thing; what separates them is where the next proofs will spend effort. Iris's adequacy into never_panics cost 174 lines; its proof mode removes the framing that dominated the hand-rolled generic layer; safepoints are handled once; and Hello's hardest case, quotearg's lent-out buffer (string ret ∗ (string ret −∗ slots), below), is a wand, which a first-order logic would have to encode. The costs to pay first:

1. Step lemmas, one per instruction form of the core subset, over abstract states, as the rules of the Iris wp. Needed whichever host; they cut both spikes' compile time and remove the existential variable problem. Re-prove Cycle.v and Buffer.v on them as the check. 2. An ectx_language whose context is the callers stack, so calls are wp_bind and a function spec returns its resources to the caller; then sum's spec as a Hoare triple. 3. dterm-rocq learns Iris: the connectives above as notations, WP … {{ }}, and the proof mode's string patterns. parse.sh shows exactly which items fail; the spike files are the test corpus. 4. Iris in the main build once the above works, with spikes/ becoming the campaign's first theories. Persistent meta as ghost_map elements (↪□), which the spike did not need because bounds came from the live token. 5. Then the proposal's path: hi.c through the logic with puts' triple derived from its contract, compared with Hi.v; gc.ir's sum with a c_gc contract on Campaign 4's machine; certificates and ownership types as fragments; Hello.

The hand-rolled spike stays as the record of the alternative and of what the logic must prove about Fil-C's memory, which Pieces.v holds for both. Buffer.v remains the last single-invariant proof; BufferLogic.v proves the same theorem through the program logic.

Progress

mbrock chose Iris (November 2026), in the Iris, RustBelt and Cerise tradition. Steps 1 to 4 above are done, and step 5 is under way:

hi.c, the logic against Hi.v's hand proof. The same body, the same contract, the same fixture:

For hi alone the logic does not pay: as long, five times slower to check, more premises and a weaker conclusion. Hi.v gets away without a frame because main reads nothing after puts, and its invariant has no heap in it; the logic must re-establish its state interpretation after every call, so it needed the frame theorem before it could prove a program with one call. What it bought is where the cost lands: the program-specific proof is six lines and stays a line per instruction, while Hi.v's method adds a constructor and a case analysis per program point and would need the same frame argument as soon as a program reads memory after a call. The test of whether it pays is the next program with a call it reads after: gc.ir's sum with a c_gc contract, or Hello's first string call, with puts's triple generalised from hi's literal to a string p assertion.

scan.c, the read after a call. The next program does read memory after a call, so here the hand method would need the frame too. There is no hand proof of scan; the hand column is an estimate from Hi.v's rate, which is the method's only proof with calls:

This is where the logic starts to pay: scan's own proof is a fifth of the estimate for the hand method, and the triples behind it are already used twice (hi.c now takes wp_puts from StringLogic.v and shrank from 312 to 196 lines). The price is a fixed one, StringLogic.v and the contract machinery in Language.v and Logic.v, and compile time, which stays above the hand method's. The case for the hand method is now only programs with no read after a call.

count.c, a helper with a triple in a loop. The two things Hello needed that scan did not: a callee's specification used by its caller, and a call inside a loop. The hand method has no callee specifications: its invariant covers every configuration, so the callee's points appear once per call site with the caller's frame under them, and the loop needs its invariant at the head as well. Again an estimate from Hi.v's rate:

The callee's triple is what keeps the proof small: each call is one application of next_l_spec, and the caller never sees strchr. Hello's next needs from the table below are memory-writing contracts (Campaign 4 has started with memset), and a callee that owns memory across calls.

slot.c, a callee that owns memory across calls. quotearg's shape: the callee's state lives in static objects between calls, the heap buffer they point to changes identity when it grows, and the caller reads a result it must not keep. Again against Hi.v's rate:

The invariant is what the hand method lacks: the state fill leaves for its next call is a separation-logic assertion, so the second call needs nothing about the first beyond slot_inv, and the caller's reads are safe because it holds the bytes the triple lent. The wand in lent is quotearg's contract with its caller: the buffer is valid until the next call. Writing it needed one fact Runtime.v did not state, that free succeeds on a live heap base and on null (frees_heap). It was a premise of slot_logic_safe until mbrock made it an axiom, free_succeeds, with a native test (axiom-free-succeeds.c).

The premise keeps_live is gone: only a signal handler the program installed, or a thread it started, frees a live object, so Runtime.v's safepoint axiom is now the collector's alone, collector_live, which makes keeps_live a lemma. Handlers are program code, to be verified under an ownership invariant.

What Hello will demand

From the proposal, with what Campaign 4's contracts would need to say for each (the contracts stay relational and trusted; a triple is derived from each once):

GNU Hello through the logic

The target (mbrock, 2026-11-09): never_panics of nanofil-hello-O, proved through the Iris logic as scan, count and slot were. Campaign 4 writes the libc contracts, the entry and exit's callbacks; this campaign writes the triples and the program's proof.

The program. HelloModule.v reads Hello as one checked module, hello_module. Its fixture, HelloCode.v, is what link.pl makes of the 81 checked terms of the real build, regenerated and compared by the flake check nanofil-hello-fixture (rocq/hello-fixture.sh):

• each object's local names become OBJECT#NAME, because objects reuse them (closeout.o and hello.o both have a str.54);

• exported names are shared, and each is defined once;

• only the items a run from main can name, through a globalS operand or a symS, Off data item, are kept: 32 functions and their data, 183 KB of IR. Leaving the rest out changes no run, since no run can name them. This is a claim about the link that no Rocq lemma states yet.

Every object was valid alone, and the link is valid too (hello_valid). That needed one fix to gallina.pl: a byte from 128 to 255 in a string now prints as its two UTF-8 bytes, as Term.v's char_code reads it. Before the fix, gettext_quote's ‘ decoded to an unknown item and the link was Somefalse. HelloCode.v compiles in 9 s, and HelloModule.v in 20 s, of which vm_compute of valid takes 8.5 s.

What it calls. hello_externals_exact lists the 33 libc functions the module calls. They are the plain entries, not the fortified ones: printf, fprintf, wprintf, fputs, atexit, not __printf_chk. Seven of them are called only by quotearg (iswprint, mbrtoc32, __ctype_b_loc, __ctype_get_mb_cur_max, mbsinit, zmemmove, realloc). Quotearg is reached only through close_stdout's diagnostic for a named file, and Hello never names one: closeout's static file_name stays null. A module invariant over that static rules the branch out, so its 414-block function needs no triple. Without it, 21 functions remain (about 200 blocks):

abort has no contract: reaching it is a failure, so the proof must show that rpl_mbsrtowcs and xalloc_die never reach it. xalloc_die is reached only when malloc returns null, which the selected malloc never does.

Decisions (mbrock, 2026-11-09):

• The link keeps what is reachable from main, as above. A later Rocq lemma will show that find_fn agrees with the full link on every reachable name.

• abort stays without a contract, so reaching it is a failure: the proof shows that Hello never calls it.

• Every path is proved, --help, --version and the error paths included, the default path first.

Milestones.

1. Done: the linked module, its gate, hello_valid, and the external list. 2. Done: leaf triples from contracts that exist, then set_program_name. See "Milestone 2" below. 3. Done: the conversion chain, over a locale the world interpretation holds, up to rpl_mbsrtowcs_spec. See "Milestone 3" below. 4. In progress: main and its option loop, from Campaign 4's entry. This needs setlocale, atexit, getopt_long, wprintf and exit. 5. close_stdout as exit's callback, through Campaign 4's Linked.v bridge, which runs an ordinary callback frame. 6. The --help, --version and error paths. 7. never_panics of the linked module from the entry.

Milestone 2. New libc triples:

• StringLogic.v adds wp_strcmp, wp_strncmp and wp_strrchr.

• MemLogic.v adds wp_memcmp and wp_memchr over blocks read through read-write or read-only capabilities (block_readable), and string_window, which lends n bytes of a string as a block.

• Logic.v gains wp_ret_void for void functions.

HelloLeaf.v (12 s, 7 s of which is laying out the module's 115 symbols) proves mbszero_spec, memeq_spec, streq_spec and strnlen1_spec. They hold in any genv that links Hello (hello_linked): its module is hello_module, its symbols include Hello's own, and no libc function Hello calls is a symbol. The registry and the world interpretation are any that hold the contracts, so the same triples serve the whole program over Campaign 4's world. A caller binds them through wp_call_bind at invocation f xs, the frame call_frame makes.

HelloName.v (15 s) proves set_program_name_spec on every path:

• The function owns argv[0] as a string, the two literals "/.libs/" and "lt-", and three cells: Hello's program_name and libc's program_invocation_name and program_invocation_short_name, each its own object, as each Fil-C global is.

• Whatever memcmp and strncmp return, the run is safe. The cells end up holding pointers with argv[0]'s capability, the first two the same one.

• Each store's premise, that it keeps the world interpretation, is store_keeps, which Campaign 4's world must show for the three cells.

The compiled function has no null check of argv[0]. gnulib declares the parameter nonnull, so clang drops the abort branch. The never-panics theorem therefore needs argc ≥ 1, which Startup's startup_at gives.

Two lessons on cost:

• vm_compute of a goal that names hello_module is fast, but cbn or discriminate on one unfolds the whole decoded module (minutes). The proofs only compute module facts through vm_compute (outside_find, hello_outside).

• put on an abstract environment needs gen_env before a lookup through it reduces.

Milestone 3, so far. The locale helpers are proved. Still to come are rpl_mbrtowc and rpl_mbsrtowcs, which wait on Campaign 4's mbrtowc, errno and composite-world contracts. New in the logic:

• Logic.v adds wp_renew and wp_half_check_read. The second is a read half check through a read-only capability, as rpl_mbsrtowcs makes on the greeting literal. MemLogic.v adds wp_raw_store_w, the 4-byte store with which rpl_mbrtowc's fallback writes *pwc. It also adds bytes_app, auxes_app and obj_zero_block, which read a fresh object as a block.

• HelloLeaf.v adds xmalloc_spec: the selected malloc never returns null, so xalloc_die is dead.

• MemLogic.v adds wp_memchr_string, a search for the NUL in an owned string with any bound. Campaign 4's memchr reads only through its first match (25073c1), so the bound may run past the string's object; memchr_input_bounded reads the admission off the string's bounded_length, and the result is nul_found: the NUL if the string is shorter than the bound, else null. On it, strnlen1_spec now returns exactly min(length + 1, n). rpl_mbsrtowcs calls strnlen1p + 4, 12 on the greeting to size its mbrtowc window, and the audited codec profile rules out -2 by that size or its NUL. The milestone 2 version over a whole block, whose result was any int, is gone.

Strings the world lends. setlocale(k, NULL) returns libc's own name for category k. The program does not own that memory, and a weakest precondition cannot remember across steps which string a query returned, because the memory and the world belong to the state, not to the assertion. Pieces.v therefore gains a ghost piece, PNamek, valued VNamep t. It names no memory: mem_piece is false for it, owned_live and ids_apart skip it, and it agrees with every memory. The world interpretation ties it to the world. An Oracle review chose this over a world-indexed state interpretation, which would have changed heap_interp and about 23 proof sites. LentLogic.v (4 s) reads such a string through lent k p t, a persistent token. It carries what holds of the lent value from the moment it is lent: p is not null, t ends before 2^64, and t's bytes are not NUL. It needs one fact of the world interpretation, lent_at: the string is a C string, in an 8-aligned object (Campaign 4's locale_name_aligned, f9a82b6), apart from every object the program owns. On that fact it proves:

• wp_lent_query, for a call that returns the lent pointer and changes nothing, such as setlocale's query;

• wp_strlen_lent;

• wp_memcpy_lent, for a prefix of the name with its NUL, copied into an owned block. The block's aux slots afterwards are whatever the copy left (slots_after), since the source's slots are libc's.

Before a name is lent it is owned whole, as named k p t. The setter setlocale(LC_ALL, "") takes the names it changes: wp_lend renames them in the ghost heap (rename_update) and hands back persistent lent tokens for the new names, whose facts it reads off lent_at in the state after the call. What the call must keep of the state, its frame and wi of the renamed heap, is the triple's premise, for the contract and the world interpretation to discharge.

LocaleLogic.v gives the world interpretation of a program that calls setlocale, locale_wi, over Campaign 4's locale_world:

• the world is locale_ready;

• libc's roots and the objects it may release are apart from the program's pieces, as the frame of an external call needs;

• the object of every read, root and name capability owns no piece of the program (cap_private);

• every ghost name is its category's current name (names_current).

From it, locale_wi_lent is LentLogic's lent_at for every ghost name. A name is a C string in a live object (live because a freed object is empty and a C string is not), and that object is private, so no live object of the program overlaps it. locale_wi_pre and locale_wi_query discharge HelloLocale's premises on setlocale's query. wi_lent now also takes the facts a ready runtime gives: live objects apart, objects in the address space, and freed objects empty.

A setter keeps locale_wi, with every category renamed to its new name (locale_wi_setter). The frame keeps libc's old roots apart from the program; the new roots have write authority only from old roots or born objects, so they stay apart. Campaign 4's private provenance (locale_delegates_private, 4de6b80) makes every new read, root and name capability a born object, which is none of the program's, or an old private one. locale_set_return states this for setlocale(c, p) in the form of wp_lend's premise, and wp_setlocale_set is the setter's triple over the locale world: owning every category's named token and the string argument, the call binds null or c's new name and lends every new name for good.

Two findings went back to Campaign 4:

• The setter contract let a new name carry the setter input's capability, or one loaded from a source's aux slots. A name could then lie in the program's own literal, and no apartness would hold. Campaign 4 restricted new names, reads and roots to born objects or the exact capability of an old read, root or name (4de6b80), which is what the setter's discharge of wp_lend needs.

• LocaleR, LibioR, StartupR and ExitMemoryR each built their own ExternalCallsR, whose invoke is a different inductive from the logic's M.E.invoke, so their theorems could not be applied in the logic. Campaign 4 added exact-machine variants (b03f7ec): LocaleOnR M and its siblings take the machine module itself, and LocaleLogic instantiates LocaleOnR L.M, so locale_wi_query now uses setlocale_query_invocation directly.

HelloLocale.v (17 s) proves setlocale_null_unlocked, setlocale_null_r_unlocked on both of its paths, setlocale_null_r and hard_locale:

• If the name fits in the buffer, it is copied with its NUL and the result is 0.

• Otherwise its first n - 1 bytes are copied, a NUL follows, and the result is ERANGE (snru_result).

• The NULL path, EINVAL, is dead because a lent name is never null.

• hard_locale copies the name into a fresh 257-byte buffer and compares it with "C" and "POSIX". Whatever strcmp answers, the run is safe.

The triples take setlocale's query as premises on its contract spec, so they serve Campaign 4's composite world once its lifted setlocale contract shows them. The same holds for the premises that the world interpretation survives the allocation, the copy and the byte store. The token is persistent, so no triple changes a lent name. Hello's one setter, setlocale(LC_ALL, ""), runs before any query. Its triple, wp_setlocale_set above, takes the names owned whole and turns them into the persistent tokens.

Two more decisions shape the rest of the milestone:

• Hello's conversion theorem carries an explicit premise that the codec is one of the audited C or C.UTF-8 profiles (mbrock, 2026-11-09). It is not derived from locale_ready, from a successful setlocale, or from MB_LEN_MAX. Campaign 4 found that an arbitrary stateful codec does not justify the -2 restrictions that rule out abort.

• __errno_location now has a contract (Campaign 4, ff21058), for rpl_mbsrtowcs's EILSEQ store.

Pieces proved in parallel. From milestone 3 on, helper threads own pieces in their own files and hand them over for integration here. Each is generic in the registry and the world interpretation, and takes as Context premises the contracts that Campaign 4's packages are still landing.

• HelloProgName.v (5a34c2f) strengthens HelloName's set_program_name triple, which only knew capabilities, to bounded suffixes of the owned argv[0] string. set_program_name_string_spec lends the chosen program_name suffix as a string, with a wand that restores argv[0], ready for printing. The one new comparison fact is strncmp_zero_lengths: a zero from strncmp means equal bounded lengths, so comparing with "lt-" for three bytes justifies advancing three without crossing the NUL.

• CallbackLogic.v (9a11a87) connects a handler's weakest precondition to Linked's void-callback endpoint. callback_wp_safe rules out failure endings for every labelled run. callback_wp_return gives the handler's postcondition at the exact memory after invalidate_locals and at the current world, before ReturnCallback. It rests on heap_exact_adequacy, an adequacy that keeps the final state, where heap_labelled_safe forgets it.

• HelloReach.v (c37f796) checks reference closure of the linked image. From main, static reachability follows global addresses and initializer symbols, including callbacks. Every reachable reference is a module function, a module global, one of 33 libc function imports, or one of six libc data imports: stdout, stderr, optarg, optind, program_invocation_name and program_invocation_short_name. hello_genv keeps the module's globals as a prefix, so startup data cannot override a module symbol, and hello_genv_linked proves hello_linked. The proof is about the image we run. That the linker's pruning kept every reachable definition of the original objects is trusted, checked by the linker's own traversal.

• HelloVersion.v (471c501, dac4525) proves proper_name, the identity, and the help footer emit_bug_reporting_address. The footer's literals stay owned by the program; stdout is the world's cell. Its four output calls take premises that line up with Campaign 4's Formatting.v contracts. It also proves the version chain version_etc, version_etc_va and version_etc_arn for the one call main makes (version_main_args): the stream, the package, program and version literals, four author pointers that are proper_name's results, and a null. The other author counts are unreachable, since nothing else calls the chain. version_etc_va derives the count of four by running its loop's five va_arg reads over the snapshot; the count is not a premise. The six output calls keep the program's literals on success, partial and negative output alike. The snapshot's allocation, the stores into the author array and the cursor update are world-frame premises (Kversion_*), and the output contracts are raw premises like the footer's.

• HelloClose.v (2a1f328) proves close_stream and close_stdout. close_stream consumes a usable stream, follows the pending, error and fclose decisions (EBADF included), and returns 0 or EOF, handing back the four errno bytes. close_stdout owns its statics: file_name stays null and ignore_EPIPE zero, so the quotearg_colon branch is dead and no quotearg triple is needed. It closes stdout, then stderr. A stdout failure calls error with status 0, then _exit; a stderr failure calls _exit directly. Wiring it as exit's callback, and _exit over the exact machine, remain integration work.

Conventions the pieces share:

• Module statics and the cells the program reads or writes directly are owned pieces passed into the calls that write them, never facts of wi. That covers file_name, ignore_EPIPE, program_name, errno, optind and optarg.

• A contract enters as raw premises: registry, ABI, admission, and what an invocation keeps. Call-site triples are derived from them with wp_external.

• A rule a piece needs and the core lacks stays in the piece, marked for promotion, until it is reviewed into Logic.v. The candidates so far:

  • wp_strncmp_lengths;

  • heap_exact_adequacy and the Linked transports;

  • rule_va_args and wp_va_args;

  • rule_va_arg, wp_va_arg and wp_va_arg_pointer, the cursor read; rule_snapshot and wp_snapshot, the va snapshot's allocation;

  • wp_raw_load_literal, a pointer load from a read-only literal, which needs an Oracle review of its capability reasoning before promotion;

  • wp_world_let, a load whose value wi fixes;

  • wp_close_errno, wp_close_load_w, wp_close_contract and wp_close_stream_pointer.

The conversion chain, first step. mbrtowc writes three cells the program owns: the wide character, the conversion state and errno. Its roots therefore meet the program's objects, and the external call frame, which needed roots apart from every owned object, did not apply. ContractFrame.v now has a frame for calls into owned blocks (54dc057): agrees_except, roots_out and pieces_off say that the roots touch owned objects only at the addresses the program hands over, and that no other piece lies there. local_agrees_out and Logic.v's effects_agrees_out and prefix_agrees_out keep every other piece agreeing. local_agrees and effects_agrees are now the case where nothing is handed over, with the same statements as before.

HelloConv.v proves wp_mbrtowc over Campaign 4's libc_world, using LibcOnR L.M. The program hands over the three cells as whole blocks (life, bytes and aux slots) and lends the source bytes. The call gives the blocks back holding whatever memory holds afterwards. conv_result reads mbrtowc_result through the owned bytes under the audited codec:

• a NUL converts to 0 and resets the state;

• a character of r bytes, none of them NUL, becomes a nonzero wide character;

• EILSEQ stores 84 in errno and leaves the output alone. Under the C codec it also keeps the state and starts at a byte of 128 or more (mbrtowc_c_error);

• an incomplete sequence is shorter than 16 bytes, with no NUL.

The world interpretation must make libc ready with a fixed errno cell. It keeps libc's private roots, releases and capabilities apart from the program's objects (libc_private), and it must survive the call's writes into the three blocks. The audited codec stays an explicit premise.

The codec is not fixed for the whole run: Hello calls setlocaleLC_ALL, "" before it converts, and that call may select another codec. A conversion therefore learns the codec from a ghost piece. The ghost heap gains a value VCodecc, which, like a name, agrees with every memory, under the key codec_key, which is no category's. locale_wi now also says codec_current: that piece holds the world's codec. wp_lend takes extra ghost pieces that a setter updates in the same step, so wp_setlocale_set takes the codec piece and hands it back holding the codec the setter selected (relocale). wp_mbrtowc takes the piece at any fraction, so after setlocale it can be made persistent and shared by every conversion, and the state stays valid under one codec from call to call.

Two contract gaps went back to Campaign 4, and it fixed both (6e82502):

• Nothing kept the state's bytes in 0 to 255 after a call, so the second call of rpl_mbsrtowcs's loop could not be admitted. The contract now requires mbstate_valid_bytes: valid states hold bytes.

• Under the C codec, hard_locale is false, so rpl_mbrtowc's fallback turns EILSEQ into a one-byte character and the loop calls mbrtowc again with the same state. The EILSEQ state was unspecified, which would have made that call stuck. For the audited C codec only, EILSEQ now keeps the entry state and requires a first byte of 128 or more, so ASCII and NUL never take it.

gnulib's rpl_mbrtowc. Hello never calls mbrtowc directly. It calls gnulib's wrapper, which converts into the caller's pointer or, when that pointer is null, into a fresh four-byte local. After an invalid or incomplete sequence (an answer of 2^64-1 or 2^64-2) it asks hard_localeLC_CTYPE. Outside a hard locale, the first byte stands for itself: the wrapper stores it as the wide character and returns 1. HelloConv.v proves this with two lemmas:

• rpl_tail covers everything from block L11 on: the call through wp_mbrtowc, then HelloLocale.v's hard_locale_spec on the failure path. hard_locale may answer either way, so both branches are proved.

• rpl_mbrtowc_spec enters with an output block the caller owns.

Only rpl_mbsrtowcs's converting loop reaches rpl_mbrtowc from main. Main passes a fresh non-null buffer, so the counting loop, which passes a null pointer, is never reached, and neither is the null entry.

rpl_result states what the caller learns: either mbrtowc's own conv_result, or 1 with the first byte stored, after a failure that left the output alone. The -2 case of conv_result keeps its premise (n below 16, and no NUL in the n bytes), so a caller that counts n through a NUL can rule it out. That is how rpl_mbsrtowcs's abort becomes unreachable even in a hard locale.

rpl_mbsrtowcs's converting loop. For each character, the loop picks a window of n bytes for rpl_mbrtowc. It reads up to four bytes, stopping at the NUL, and then asks strnlen1 for at most twelve more. mbs_window proves that n = min(len + 1, 16) for the string suffix at the cursor, on all five paths.

rpl_step turns one call's rpl_result into what the loop needs. The call is never incomplete, so the abort after -2 is not reached:

• -2 would need n below 16 and no NUL among the n bytes;

• n below 16 means the window reaches the NUL.

EILSEQ stores 84 in errno. The NUL stores a zero character. Anything else consumes 1 to len bytes before the NUL, stores a nonzero character, and leaves the state valid and in its initial shift state (its first four bytes zero).

The fallback after EILSEQ needs the same facts under C.UTF-8. Campaign 4's mbrtowc_initial_error gives them: from a valid initial state, an EILSEQ keeps the state valid and initial, and its first byte is not NUL. conv_result's EILSEQ case now carries that law.

mbs_loop proves the loop from block L28 by Löb induction. Its invariant:

• i characters written from the first j bytes, with i ≤ j ≤ len;

• the written words are nonzero (wide_ok);

• the rest of the destination is owned, word by word;

• the state is valid and initial.

There are three exits:

• EILSEQ in a hard locale: the cursor is stored back through srcp, errno gets 84 (wp_conv_errno, a libc_world copy of HelloClose's rule, for promotion), and the loop returns -1;

• the NUL: null is stored through srcp, and the loop returns i, after i nonzero characters and a zero one (mbs_post);

• otherwise both cursors advance and the loop goes round.

The count left, len - i, never reaches zero before the NUL, because i ≤ j ≤ len. Main reads the result as a wide string with wprintf"%ls", or calls error on -1.

rpl_mbsrtowcs_spec adds the entry, from start to L28, and so proves the whole call as main makes it: dest a fresh buffer of len wide characters, srcp a cell holding the string, len its length with the NUL, and ps main's own state, not null, valid and initial. The entry allocates a local only the counting loop uses, keeps ps, loads the string through srcp, and enters the loop with nothing written. The string may be a read-only literal. Logic.v's wp_raw_load_pointer_in loads any pointer, read-only literals included. It promotes HelloVersion's wp_raw_load_literal after Oracle review:

• the cell may be reached through a read-write or a read-only capability;

• the life of the object the loaded capability names is any (PLive xb, VLive xr) among pieces the caller already owns;

• capabilities for no object, a function or an external need no life.

Its proof rests on Pieces.v's aux_holds_kept: a stored capability whose object is not freed is exactly what the slot holds. wp_raw_load_pointer stays as it is for its callers. In rpl_mbsrtowcs the life of the greeting's object is the head piece of its SL.string, so the load needs no new token.

Stream tokens. The ghost heap gains a value VStreamp pending for Campaign 4's stream adapter. Its key is a name, and pending is Somecount, fifo while the stream is open and None once it is closed. Like a codec, it agrees with every memory, and only the world interpretation reads it. It is not a VName, so lent_current, which constrains every VName in the heap, says nothing about it. A stream's handle keeps its own PLive piece.

One logic for main. Two applications of LogicR have distinct expressions, states and step relations, so triples proved over separate instances cannot be combined. Before this change each Hello file built its own chain from R, and so did LocaleLogicR and CallbackLogicR. Logic.v now has a module type, LogicSig, the signature of one instance. Each layer above it is a functor over one instance, XOnR : Runtime LG0 : LogicSigR:

• StringLogic, MemLogic, LentLogic and LocaleLogic;

• HelloLeaf, HelloLocale, HelloConv, HelloName, HelloProgName, HelloClose and HelloVersion;

• CallbackLogic.

Inside each, Module LG := LG0. keeps the old paths. X itself is XOn over a LogicR of its own, so no statement and no existing user changes. Main's proof applies every …On functor to one instance. Campaign 4's StreamFrameLogic has the same signature, so its …On modules take the same instance.

Main's start block. HelloMain.v applies every …On functor to one LogicR. Its world is libc's, and its world interpretation wi stays abstract. Each section premise is what one call needs of wi, so a concrete interpretation discharges them once:

• Kalloc: an allocation keeps wi;

• Kmemset: zeroing eight owned bytes keeps wi;

• HelloName's cell layout and store premises;

• Hlent, Hset_pre and Kset for setlocale.

wp_main_setlocale is setlocale's triple over libc's contract, libc_setlocale_contract, from LentLogic's wp_lend. It is the libc-world counterpart of LocaleLogic's wp_setlocale_set, whose world is the locale world alone.

main_to_setlocale proves main's start block from the entry up to setlocale's call, and the triples of three files compose in it: 1. two fresh objects, b4 for the greeting's cell and b6 for the conversion state; 2. mbszero on b6 (HelloLeaf); 3. argv[0] loaded through wp_raw_load_pointer_in, its life the head of its string's pieces; 4. set_program_name (HelloProgName); 5. the literal "" copied.

main_start_rest proves the rest of the start block: 1. setlocale(LC_ALL, "") through wp_main_setlocale; 2. the default greeting stored in b4's cell (Kpstore); 3. atexit(close_stdout). Its contract stays abstract: it returns an int and keeps the program's pieces and wi (Katexit), because the registration is libc's own state.

main_start composes the two segments. It goes from main's entry to the option loop's first block, with every resource the loop needs: argv, the name cells, the lent names and the codec, the greeting's cell and the zeroed state.

Next is the option loop. GNU getopt_long may permute argv, and main reads optind and optarg, which are libc's cells, directly. So the loop needs a getopt triple that takes argv's cells and hands them back permuted, and a world-justified read of libc's cells.

Reading getopt's cells. Main owns neither cell, and getopt rewrites both at every call. A ghost value, VGetoptoptarg optind under the name key 64, stands for what getopt last left there. Like the codec and stream tokens, it agrees with every memory. GetoptLogic.v ties it to the world through one premise on wi: the world's getopt state is in memory at the two cells (Campaign 4's getopt_state_at), and the token is current (getopt_current). Logic.v's wp_world_let_with is an instruction whose result wi fixes given pieces the program owns. GetoptLogic derives four rules from it:

• wp_optarg_check, optarg's 8-byte read check;

• wp_optarg_load, the pointer load giving the token's optarg;

• wp_optind_check, optind's 4-byte check at alignment 1;

• wp_optind_load, the signed 32-bit load giving the token's optind.

Campaign 4 added getopt state to libc_world (libc_getopt, viewed by libc_getopt_view) and canonical byte bounds to getopt_slots (1b61cc0). Without that state, any view would be constant, and getopt's post would claim the cells never change. Campaign 4 also confirmed that the registry can be fixed per launch after startup fixes argv, which getopt_contract's input needs.

getopt_long's call. HelloMain.v's wp_main_getopt is the call main makes, with libc_getopt_contract (hello_input av sargs) … in the registry. The run's arguments sargs are strings in objects of their own, as the launcher copies them. hello_input is getopt's input for the whole run: argv, "g:t" and Hello's four long options, every flag null. Main hands over argv the way HelloConv hands mbrtowc its cells: one block (block_ps) of argc + 1 slots. Its bytes are those of the pointers it holds (argv_bytes) and its aux slots their capabilities (argv_caps).

• The admission (getopt_admitted) reads getopt_slots from that block and the arguments' lives. Each slot's capability names a live argument, so it is not freed and its aux piece holds it exactly.

• The return is framed by prefix_agrees_out, whose one block out is argv. The new getopt_slots, with its byte bounds, turns memory back into a block of the same form (argv_of_slots). This is where the bounds are needed: a slot whose bytes are only known to load as a pointer does not fix the bytes the pieces name.

• The triple hands back another permitted order ps', the strings unchanged and the token renamed to the new optarg and optind, with optind in range. hello_code adds that the code is a C int and that a 'g', short or --greeting, comes with a nonnull borrow of an argument.

The premises on wi are call-local:

• Hgetopt_wi: the cells and token are current.

• Htable: the literals are in memory.

• Hgetopt_env: libc's side of admission.

• Hgetopt_apart: roots, cells and releases apart from the program.

• Kgetopt: wi survives with the block and the token rewritten.

The option loop. main_loop is a Löb induction at the entry of iw_1.L8. getopt promises no bound on how often it returns, so the loop may run forever, which never_panics allows. Each round enters a block, and that step guards the induction hypothesis. The code's 32 bits are compared (int32_eq, int32_end), and the cases are:

• 'g': optarg is loaded through the token (GetoptLogic's wp_optarg_check and wp_optarg_load) and stored in the greeting's cell b4, then back round.

• 't': the traditional greeting is stored, then back round.

• Any other code but help and version: back round with pr.2, the "lose" flag, set to 1.

The exits are left to continuations (loop_exit): iw_1.L21 (version), iw_1.L39 (help) and iw_1.L10 (end of options). Each gets the loop's pieces (loop_res): argv's block, the strings, the token, and b4 holding a greeting_ok pointer, which is the default, the traditional greeting, or a nonnull argument borrow. It also gets pr.2 at 0 or 1. Main owns everything else the start block left (b4's tail, b6, the lent names and the codec), and the continuations capture it.

main_to_loop composes main_start with the loop. It takes argv as a block holding the arguments in order (argv_block_split lends its first slot to main_start) and the token at any optind in range. It needs the launcher to give the arguments' strings objects of their own, which Startup.v's copy_slots does, one allocation per string.

Next is the end of options (iw_1.L10: the operand check on optind), then the version and help paths over HelloVersionOn and HelloStdioOn.

Open questions for mbrock

• Start the logic now, or finish Campaign 4's hi.c first?

• Iris, as recommended after the spikes, or the hand-rolled logic?

• Is "frees nothing live at a safepoint" the premise wanted for every single-threaded program, or should Runtime.v gain a single-threaded runtime type that has it as an axiom with a native test? Answered (2026-11-09): neither. There is no premise. Runtime.v's safepoint axiom is the collector's alone, collector_live (no region changes at a safepoint, native test axiom-collector-live.c), for every runtime. A signal handler or a thread is program code, to be verified with an invariant that it frees only what it was handed.

• Should the ladder's middle rungs (types, certificates) be designed before the spike, or only after it shows what a derivation looks like?

See meta, live and adequacy for the three new terms.