A trap is a Fil-C check failing, which upstream calls a Fil-C panic or safety error (filc_safety_panic): the run ends trapReason, terminal and uncatchable. Because nothing follows it, a checkcheck Fil-CAn access check: check(Lo, Hi, Rights, Align) of a pointer P traps unless P's capability permits Rights on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a proof of class a. check_local does the same for a named local, and check_function yields a function proof of class f (ir:op_kind/2, pizlonate:checked_access/4). is a pure assertion, which is why a check proved never to fail can be deleted without changing behaviour.

• The reasons: null_capability, out_of_bounds, misaligned, readonly, not_a_function, argument_size, return_size, invalid_free, double_free, too_big, out_of_memory, and earlyWhy for a check_aheadcheck_ahead nanofilcheck_ahead(Lo, Hi, Rights, Align, AHi) is a check of [Lo, Hi) whose own access needs only [Lo, AHi): the bytes [AHi, Hi) are checked early for later accesses through the same base, as filcc's check scheduler does. It may trap earlier than the reference program, but only on runs that would trap later anyway. whose failure came early. The access check tests null, then bounds, then read-only, then alignment (cap_access_res).

• Memory.v's reason is shared with 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)., which adds alias, span, half, limit and aheadWhy: the reuse forms' broken trusts, never traps. res is a partial result: a value, RTrap or RUnchecked.

• interp.pl's reasons are coarse: past the end, below the start, freed and a function object all trap out_of_bounds. The exact native text is compared by progtest and tests/renew-trap.sh.

The subtlety: Campaign 7 does not count every trap as a panic. It counts too_big and out_of_memory as resource endings (formal.md, What counts as a panic).

Defined in Memory.v and interp.pl's header.