Tags 0/1 are skipped by the exit loop. A reserved slot is not an installed callback; arbitrary unknown flavors are not admitted. Tokens are ghost registration instances, never native slot indices/addresses.

A decoded function capability is not an admitted code specification.

Only the flavor-selected fields matter. In particular free/reserved slots impose no requirements on stale payloads. Cxa's DSO pointer is represented but not dereferenced by ordinary exit. Native pointer mangling is a no-op in this selected source, not in arbitrary glibc.

Flavor, not the public API's spelling, selects the callback form. This pin's atexit stores ef_cxa with null argument and DSO; adapting that to logical AtExit requires a separate calling-convention contract.

Native slots are stored oldest first; exit scans downward, skipping holes.

The slots below idx, not an assertion that idx counts live callbacks.

Full readable containing-object bounds/alignment are independent of pointer-slot decoding. Slots at or above idx are deliberately ignored. Writable spans are NOT inferred from this read-only view.

The actual next-slot value for this finite suffix.

A finite null-terminated chain, linked by decoded pointer capabilities.

Block identities are distinct, not merely the pointers' address bits in next slots. Base capabilities in exit_block_memory tie them together.

Blocks are visited head-first; each block is scanned in reverse slot order.

Callback specifications and retained argument requirements are independent of decoded Fn capabilities. Active evidence is detached from any old slot: idx has already decreased, and cxa may already have cleared it.

Release eligibility AFTER unlinking, not a memory transition. Explicit ownership, an exhausted live Heap base, enough extent, a distinct nonempty successor chain and the updated head are all required. Merely reading a block, finding it live, or observing next != NULL confers no ownership.

A free hole at the next index consumes no pending registration.

Reserved physical slots are skipped too, not treated as installed code.

Popping an installed slot detaches its registration before callback entry. This is a projection lemma, not construction of native write effects.

Decoding a represented slot also supplies checked containing-object access.

Being the last node prevents release even if the caller owns a live heap block.

A readable, writable or live block is still not a release permission.

The array's fixed native capacity rejects idx=33, independently of memory.

Repeated blocks cannot form a selected registry, even if slot bytes look linked.

The native index decrement; older is the prefix left after the pop.

Native cxa removal also clears its flavor, after decrementing idx. Payload bytes and every auxiliary capability remain untouched.

Only idx and, for cxa, the removed flavor need write authority. A readable containing block is not this permission.

The head cell and other block storage must not alias this block. Distinct object identities alone do not establish byte separation.

A byte store preserves all reads disjoint from its actual footprint.

A pointer slot depends on its eight bytes and its own shadow entry.