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).

Hi.v proves hi's body safe by hand: an invariant over the labelled machine's states with a case for each of main's four points, and a lemma for each kind of labelled step at each. This file proves the same body in Iris, by one rule per instruction and StringLogic.v's triple for puts (wp_puts):

• the program owns its literal str.10 as a string: its life and its six bytes (lit_ps);
• the world interpretation is stdio_wi: puts's rep and stdio_ready, and the world's writable roots apart from the program's live objects; a safepoint keeps it under Hi.v's premise that it keeps rep and readiness;
• main enters, copies the literal, calls puts and returns 0 (main_spec), 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. for the labelled machine (heap_labelled_safe) makes that hi_logic_safe.

The theorem's premises beyond Hi.v's hi_before_call are the logic's own: the runtime 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., the live objects apart, and the world's roots apart from the literal (literal_apart). Its conclusion is the logic's: no run stops with a failure_ending, and main returns 0; Hi.v's hi_ending lists the stops that remain by name. docs/logic.md compares the two proofs.