Rights are what an access asks of a capabilitycapability Fil-CA capability is the authority half of a Fil-C pointer: which object, if any, its address may be used to access. In the model a capability is an identity, never bounds; the object's current bounds live in its region, so freeing through one alias empties what every alias sees.: read or write, where write allows reading too. Every check, renew and raw access names the rights it needs.

• ir.pl: the Rights argument of checkLo, Hi, Rights, Align and the reuse forms; ir:rights_allow/2ir.plrights_allow/2not documented. Syntax.v: rights, Read and Write.

• A write through roBase (Ro) traps readonly, tested after bounds and before alignment (cap_access_res). All exposed capabilities of one object have the same rights, so read-only is a property of the object: natively, the READONLY flag in its headerlower Fil-CThe lower is how Fil-C represents a capability natively: the address of the first byte of the object a pointer may access, kept beside the pointer's intval in a flight pointer. The object header sits just below it: the upper bound at lower−16 and the aux word at lower−8, whose low 48 bits point at the aux allocation and whose top 16 bits hold the object's flags (free, read-only, global, ...). A null lower accesses nothing, and free sets upper to lower, so every access through any lower of a freed object fails. filc_abi:lower_function/5 keeps each live one in a root..

The subtlety: a reuse form asks its own rights, not its source's. A renewrenew nanofilA renew reuses an earlier check's bounds: renew(Lo, Hi, Rights, Align) of [Q1, P] trusts the dominating check that made Q1 for P's bounds and tests again only what a free changes, that the object is not freed (and, for a write, not read-only). It is the -O default (check_reuse:renew_checks/2, m7.md, round 4). of a read-only object for a write traps readonly, which interp:renew_res/4interp.plrenew_res+Res₀, +P, +Mem, -ResdetA renew (docs/m7.md, round 4) of P whose access_res/7 is Res0 yields P, proven, or traps as the check it replaced would: a read-only trap stands, and a freed object traps out of bounds. Any other failure means the earlier check's bounds did not cover this access, which a valid renew rules out, so it is unchecked(span), a broken pass. keeps as the program's trap; a hullrenew_hull nanofilThe hull of several passed checks of one object is the interval from the least lower end to the greatest upper end of their spans; since an object is one interval, every byte of the hull is in it. renew_hull(Lo, Hi, Rights, Align) of [QL, QH, P] is a renew whose bounds two such checks give: QL's from at or below P+Lo, QH's to at or above P+Hi. write needs some span with write rights, since a passed write check shows the capability is not read-only.

See rocq.md, Renew and the half check.