A value's machine type, one letter: w and l integers (32 and 64 bits), s, d and x floats, p a pointer with 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., and in checked IRchecked IR nanofilThe two stages of the IR. Unchecked IR leaves Fil-C's checks implicit in every load and store at a p address; checked IR states every check, every raw access and the proof it uses, so the validator can see that each access is covered. A module's stage is read off its vocabulary, never a flag (ir:module_stage/2). a (a proven address) and f (a proven function) (ir:class/3ir.plclass?K, ?Kind, ?BitsnondetK is a value class of Kind (int, pointer or float), Bits wide. Every other fact about classes below follows from this table.).

• Rocq: class in Syntax.v, with W, L, P, A, F, Single, Double and Extended; word_at_class (interp:word_at_class/3interp.plword_at_class+K, ?X₀, ?XX is the word X0 taken at class K, its low bits(K) bits; a p word is itself.) says when a wordword nanofilA word is the value a temporary holds at run time: an integer, a pointer (an address with its capability), or a limit's opaque snapshot. The temporary's class says how it is read. is of a class.

• a and f are the proofproof nanofilA proof is a temporary of class a or f, the result of a check: it holds the checked pointer itself and certifies that the check passed. A raw access names the proof it relies on, so evidence is structural (ir:proof_use/6). classes: never parameters, phis, call arguments or stored values.