never_panics_by_invariant in Panics.v is the adequacy of the simplest such logic, one invariant of configurations: if it holds at every admissible start, every stepstep nanofilA step moves a configuration on by one thing: entering a block (its phis, one unit of fuel), one instruction, or one jump. step answers Next with the next configuration, Done with an outcome, Fresh for an allocation that waits for a base, or Stuck. from it is safe and lands in it for every freshfresh base nanofilA fresh base is an address where a new object may be placed: positive, aligned, no object's identity (live or freed), overlapping no object's bounds, ending at or below 2^64, and reading as zero with no stored capability, as Fil-C's allocations do. base, and a due safepointpoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1). keeps it, then never_panics holds. Cycle.v and Buffer.v are proved with it.
Campaign 3's valid_no_unchecked is the adequacy of another fixed logic, the validatorvalidator nanofilThe validator decides whether a module is well formed and, in checked IR, whether every access is covered by evidence that still holds. Every producer of checked IR must get its output past it, and Soundness.v proves that a module it accepts never runs to unchecked.'s facts, for one kind of failure, 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)..
IrisIris IrisIris is a higher-order concurrent separation logic framework in Rocq. Its propositions describe owned resources, may quantify over propositions, and are shared through invariants; user-defined ghost state expresses protocols. A language joins it by giving its step relation, and adequacy turns a weakest precondition proved in the logic into a fact about every run. proves adequacy once for every language it is instantiated with, from a weakest preconditionweakest precondition IrisWP e {{ v, Φ v }} says that running e is safe and that, if it ends in a value v, Φ v holds. Iris defines it once for every language by guarded recursion: unless e is a value, given the state interpretation of any state, e can step (when stuckness is NotStuck), and after every step it can take, one later on, the new state's interpretation and the WP of what e became hold. Hoare triples and specifications are wands into it. of the program. The spike IrisLang.v makes the machine an Iris language in which a configuration that fails cannot step, so Iris's adequacy gives never_panics directly (wp_never_panics) (How Iris works).
In the planned logic, assertions describe owned objects by metameta nanofilA meta fact, meta b n k, says that the object of identity b was allocated with extent n bytes and kind k (heap, global data, stack). It is the persistent half of owning an object in the planned program logic: once true it stays true, so it can be copied and shared freely, because nothing after an allocation changes what was allocated. With the pointer's offset from b it decides a check's bounds by arithmetic alone; whether the object is still there is the live token's part. facts, livelive nanofilA live token, live b, is permission to rely on the object of identity b not being freed. It is the temporal half of a check: the bounds come from b's meta fact, and the free flag passes as long as the token is held. Free consumes it, so whoever frees an object must own it, and an object no one else owns cannot be freed behind the owner's back. For a heap object it is exclusive, or split into fractions for readers; for global data, which is never freed, it is persistent. tokens and their cells, and adequacy states that the logic's state interpretation, with Campaign 3's run invariant, holds at every state a run reaches.