A flight builds a pointer from two independent sources: flightD, Op, Args, Lower computes D's address with copy, add or sub over l values and pointer addresses, and takes its 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. from the pointer Lower names, or none (pizlonate:flight_inst/2pizlonate.plflight_inst+Inst₀, -InstsemidetInst is the flight of the pure pointer operation Inst0: add or sub of an offset, a copy of a temporary or constant, or itop, which has no lower. The address calculation and lower are chosen independently; no new temporary or safepoint separates them. A symbol copy still calls its getter; it is not a pure projection, and stays.). Making the pair proves nothing about access; no check, getter, memory access or safepoint happens inside it.

• Rocq: the instruction Flight; flight_cap reads its capability. A flight is replayable: its capability is its lower donor's (replayreplay nanofilA single definition replays at a point when its name holds what its own instruction's step made, in some earlier frame that agrees with the current one on the instruction's single-definition operands, and the current memory persists from the memory that step left, which lay in the address space.).

• Chains of flights are what the validator follows: guard chainsguard chain nanofilA pointer's guard chain lists its bases with the offset of its address from each: P itself at i(0, 0), then each base B reached through single-definition add, sub and copy flights whose lower donor is their address operand, with an interval for P's address minus B's, modulo 2^64. P has the capability of every base on its chain. and lower chainslower chain nanofilA lower chain from P to B says P carries B's capability: P is B, or a single-definition flight whose lower donor has B's lower, whatever its address..