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.

A call changes memory along an effects path of 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 (ExternalCalls.v): local_effect segments, which write bytes and 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 only where the call has write_authority and change an object only by freeing a live heap object it may release or allocated itself, and allocations at a fresh base, which join the call's born objects. The program logic owns pieces of memory (agrees with a ghost heap h), and asks what of them survives the call.

The premise is separation by address, not by identity: no address of a contract's writable roots lies in a live object that owns a piece of h (roots_apart), and the contract releases none of h's identities (ids_apart). Then the call's born objects are not the program's, it writes nothing the program owns, and after the whole path h still agrees with memory and live objects are still apart (Logic.v's effects_agrees, prefix_agrees and invoke_agrees, over the language's own call relations). A world's new roots that a call delegates from its old roots and born objects stay apart as well (delegates_apart).

A call may also write blocks the program hands it, such as mbrtowc's output, state and errno cells. Then its roots touch the program's objects only at the addresses of those blocks (roots_out), and every piece but the handed-over ones keeps agreeing (agrees_except, local_agrees_out; Logic.v's effects_agrees_out and prefix_agrees_out).

Byte and aux pieces of an object that is not live need only stay registered, and an aux piece of a live one is known up to aux_holds; regions of old identities change only by being freed, so a freed capability stays freed and one that traps as freed keeps trapping (freed_in_step, traps_as_freed_step). Released or not, no piece but a life token needs its object kept live; a life token does, which is what ids_apart of the releases gives.