An external call is a call to a symbol the module does not define, in practice libc. The core model sends only free to the 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. 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.

• Core: Semantics.v's external_call and free_name, which run the global environmentglobal environment nanofilThe global environment is what every step of a run reads but never changes: the module, each global's pointer, and the free that a call of libc's free runs.'s ge_free; interp.pl's external callvoid, globalfree, argp, P, which module-defined functions take precedence over.

• ExternalCalls.v: contract, effects, invoke, puts_contract. ExternalMachine.v: external_site (direct calls only, never in a doomeddoomed 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. frame), no_violation, and run_preserve, which carries readiness, identities and both invariants through labelled runs. The extracted driver is unchanged.

The subtlety: a failed premise is an unmet caller obligationobligation nanofilAn obligation is something a proof leaves to be shown or trusted elsewhere, named rather than assumed away. A realization obligation is the trusted claim that native code realizes a logical model: that pinned libc's FILE, buffering and dispatch behave as Stdio.v's protocol and Libio.v's memory view say., a ContractViolation ending, not a claim that native libc traps. Within its contract a call may return, exit or exhaust resources, but never 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). or a capability panic.

The table of contracts is libc-contracts.md; see formal.md, Campaign 4, milestone 1.