← Back to AILP Home

Handle lifetimes (ARIA-032)

A handle is only valid as long as the arena that minted it lives. Within a single function body, the borrow checker enforces this statically: derefing or freeing a handle whose arena was destroyed earlier in the same function is a compile error tagged ARIA-032.

The rule

use "handle.npk".*;

func:bad = int32() {
    int64:a            = raw HandleArena.create();
    Handle<int32>:h    = raw HandleArena.alloc(a, 4i64);
    raw HandleArena.destroy(a);              // arena gone
    int64:p = raw HandleArena.deref(h);      // [ARIA-032]
    exit 0;
};

error[ARIA-032]: Handle 'h' outlives its arena 'a'. The arena was
destroyed earlier in this function; the handle is no longer valid.
See ARIA-032 and guide/memory/handles.md.

free of a stale handle is also rejected:

raw HandleArena.destroy(a);
raw HandleArena.free(h);                     // [ARIA-032]

What the rule catches

The borrow checker records two things per function:

HandleArena.deref(h) and HandleArena.free(h) look up h's bound arena; if it is in the destroyed set, the rule fires.

The rule does not false-positive on correct teardown:

int64:a         = raw HandleArena.create();
Handle<int32>:h = raw HandleArena.alloc(a, 4i64);
int64:p         = raw HandleArena.deref(h);    // OK — a still alive
raw HandleArena.free(h);                       // OK — a still alive
raw HandleArena.destroy(a);                    // last
exit 0;

bug263_handle_destroy_after_use_pass.npk is the regression test.

Sibling arenas are independent:

int64:a            = raw HandleArena.create();
int64:b            = raw HandleArena.create();
Handle<int32>:hb   = raw HandleArena.alloc(b, 4i64);
raw HandleArena.destroy(a);                    // destroy a
int64:p = raw HandleArena.deref(hb);           // OK — hb is bound to b, not a

bug262_handle_other_arena_alive_pass.npk covers this.

What the rule does not catch (intentional)

The v0.28.x slices extended the rule across function boundaries for the common shapes:

What still bypasses the static rule (by design, for now):

Closed in v0.30.x. Transitive cross-function flow (destroy-via-helper-via-helper) closed in v0.30.1 via a per-module fixpoint over function summaries. The dual escape case (return-of-handle-bound-to-callee-arena) closed in v0.30.2. Imported externs are no longer a blind spot: v0.30.3 seeds summaries from every module loaded via use, and v0.30.4 added the #[destroys_arena(<param>)] attribute so externs without an Nitpick body can still participate. The cross-module and transitive cases ship as warnings for one cycle (IPC-DEC-004); intra-function stays an error. See cross_module.md for the full story.

In all of the remaining bypass cases the runtime generation check still catches the misuse: deref returns 0i64. The static rule is a strict superset of safety — it never accepts code the runtime would reject; it just refuses some code earlier.

Interaction with raw / drop / nodrop

The borrow checker peeks through raw(...), drop(...), and nodrop(...) wrappers on the initializer expression — Handle<T>:h = raw HandleArena.alloc(...) is recognised the same as Handle<T>:h = HandleArena.alloc(...). The same peeling applies to the per-Handle<T> RAII recognizer introduced in v0.31.5.x.

There are two distinct opt-outs with different semantics:

Since v0.29.5, importing drop.npk opts arena bindings into auto-destroy: int64:a = HandleArena.create(); auto-emits npk_handle_arena_destroy(a) at scope end. Since v0.31.5.x, the same import also auto-emits npk_handle_free(h) for every Handle<T>:h = HandleArena.alloc(...); binding at its scope's end. The outlives rule still applies — bindings whose handles escape from a RAII-managed arena trigger ARIA-032 the same way, and a pass h move out of the originating frame skips the auto-free (HANDLE-DEC-006). An explicit HandleArena.free(h) on a RAII-managed binding raises ARIA-022 (hard error in v0.31.6.4, NODROP-DEC-013 — promoted from the v0.31.5.3 ARIA-051 warning since nodrop now provides a precise per-binding opt-out). See the guide/drop/ cookbook (especially regions.md for the recognizer rules and pitfalls.md for the manual + auto collision trap).

Validation

See also