capability
Fil-C also cap, InvisiCaps
Upstream InvisiCaps, filc_runtime.h
A 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.
| interp.pl | Values.v | Names |
|---|---|---|
none | CNone | no object: a null or forged pointer |
objBase | Obj | a writable object |
roBase | Ro | a read-only object |
fnF | Fn | a function of the module |
extN | External | a symbol defined outside the module |
Upstream names the same three kinds: the null capability (none), plain capabilities with bounds (obj and ro, read-only being a flag of the object), and special ones such as a function's, whose upper bound equals its lower so that no data access passes.
A pointer pairs it with an address: a flight pointer, ptrAddr, Cap in interp.pl, ptr in Values.v. Natively the capability is the lower; the model abstracts that to the base, the object's identity, never recovered from address bits. A flight takes its capability from a named donor, independently of its address.
The access check (interp:cap_access_res/7, cap_access_res) tests null, bounds, read-only, then alignment. A function's capability has zero size, so every access through it is out of bounds; an external symbol's is stuck.
Defined in Values.v and interp.pl's header; see guide.md, Address is not authority.
Linked from
- Buffer.v: buffer_module
- Chain.v: cap_access_hull
- Chain.v: offset_rel
- Chain.v: pointer_distance_sound
- Coverage.v: cap_access_covered
- Doomed.v: need_access_fails
- Doomed.v: weak_operands
- ExternalCalls.v: span
- ExternalCalls.v: writable_span
- GIMSO
- Guard.v: lower_chain_sound
- How Fil-C works: Pointers carry capabilities
- Identity.v: ids
- Identity.v: persists_access
- Libio.v: file_capacity
- Machine.v: store_aux_kept
- Renew.v: cap_eqb_refl
- Renew.v: renew_source_def
- Renew.v: reuse_operands
- Run.v: data_cap
- Run.v: item_contents
- Runtime.v: aux_round_trip
- Runtime.v: freed_in
- Semantics.v: flight_cap
- Semantics.v: function_check_res
- Semantics.v: generic_word
- Semantics.v: snapshot_values
- Semantics.v: value_x
- Startup.v: copy_c_bytes
- Startup.v: pointer_slot
- Syntax.v: class
- Transport.v: ecap
- Validate.v: guard_chain
- Validate.v: pointer_distance
- Values.v: cap
- alloc
- aux
- cas
- check
- class
- exact base
- flight
- flight pointer
- getter
- global environment
- identity
- interp.pl: run/5
- launder
- lower
- lower chain
- pointer distance
- region
- rights
- shadow
- word