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.

A block is owned piece by piece: bytes b o xs, the bytes xs from offset o of the object b, and auxes b o cs, the capabilities cs in its auxaux Fil-CAn object's aux allocation, as large as its payload: where Fil-C keeps the lowers of the pointers stored in the object, slot for slot, while their intvals sit in the object's bytes. The aux word in the object header points at it; it is null for an object no pointer was ever stored into, which the collector then scans as a leaf. A pointer store must *ensure* it exists, which may call the runtime; a pointer load reads it. slots from the same offset. A write by libc into a block needs both: memset clears every pointer slot it touches, a copy moves pointer slots, and a pointer slot is an aux piece.

Each triple is a contract read as a rule, stated at any call site:

• wp_memset, from memset_contract: owning the object's life and a block of n bytes from an 8-aligned offset, with their aux slots, the call fills the bytes with c's low byte and empties every slot that starts in the block (clear_slots);
• wp_memcpy, from memcpy_contract: owning a destination block and a source block in another object, of the same length, both 8-aligned, so in phase, the destination takes the source's bytes, and each of its slots the source's when the copy covers all 8 of its bytes, or empties (copy_slots); the source is handed back;
• wp_malloc, from malloc_contract: the fresh object's pieces (obj); no null case, since the selected malloc refuses with a resource ending, which is not a return;
• wp_strdup, from strdup_contract: owning a string, the call returns a fresh object owning a copy of it as a string.
• wp_string_copy, from string_copy_contract, with wp_strcpy and wp_stpcpy its instances: owning an object's life and bytes, one more than a string's in another object, the call makes them a string holding the copy and binds d to the destination or, for stpcpy, its NUL; it keeps every aux slot, so none is owned, and needs no alignment (copy_string_after);
• wp_memchr and wp_memchr_string, from memchr_contract: a search of an owned block, or a search for the NUL of an owned string with any bound, since memchr reads only through its first match (memchr_input_bounded, nul_found).

The contracts' exact destination frame (memset_frame, shared by the copies) keeps every piece outside the written block (block_frame, through Heap.v's frame_within); for strdup, whose writes lie in its fresh object, frame_other keeps every other object's pieces. The blocks' offsets are 8-aligned so that the slots a write touches start inside them; the contracts also allow unaligned starts, whose first touched slot begins before them.