rocq/theories/Values.v

Run-time values, transcribed from interp.pl: capabilities, pointers and the words a temporary holds.

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
`obj(Base)`	`Obj`	a writable object
`ro(Base)`	`Ro`	a read-only object
`fn(F)`	`Fn`	a function of the module
`ext(N)`	`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 pointerflight pointer Fil-CA flight pointer is a pointer held in a variable or register rather than in memory. It has two words: its intval, the address the C program sees, prints and computes with, which nothing trusts; and its lower, the capability, which only an allocation creates and the program can neither see nor forge. Stored to memory it becomes a pointer at rest: the intval goes in the object's bytes and the lower in the object's aux allocation, where no capability reaches. That invisibility gives InvisiCaps their name, and it keeps sizeof(void*) at 8., ptr(Addr, Cap) in interp.pl, ptr in Values.v. Natively the capability is the lowerlower 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 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.

Words

Values are a sum type over classes (formal.md's decision): well classedness is a boolean fact about a word, not an index of its type.

Gallina	interp.pl	Classes
`WIntn`	an integer	`w`, `l`; also `p`, an integer argument with no pointer term
`WPtrp`	`ptr(Addr, Cap)`	`p`, `a`, `f`
`WLimitc size`	`limit(Cap, Size)`	`l`: a limit's opaque snapshot

The integer at class p is interp.pl's defaulty case for main.pl's canonical arguments (class_arg/2): the model keeps it, and every operation that needs a pointer is stuck on it, as the interpreter fails there.

From Stdlib Require Import String ZArith List Bool

From Nanofil Require Import Term Syntax

Import ListNotations

Open Scope Z_scope

A capability, what a pointer carries beside its address: which object, if any, it may access. An object's is its identity, the base of its region, and holds no bounds of its own.

32Inductive cap: Type ≔

\|	CNone		`none`: no object, a null or forged pointer
\|	Obj	base : Z	`obj(Base)`: the writable object of identity base
\|	Ro	base : Z	`ro(Base)`: the read-only object of identity base
\|	Fn	f : name	`fn(F)`: the function f of the module
\|	External	n : name	`ext(N)`: the symbol n, defined outside the module

Equality of capabilities.

40Definition cap_eqbc c′ : cap : bool ≔

match c, c′ with

CNone, CNone

⇒

true

Objb, Objb′ | Rob, Rob′

⇒

Z.eqbb b′

Fnf, Fnf′ | Externalf, Externalf′

⇒

name_eqbf f′

_, _

⇒

false

As ptr(Addr, Cap): a pointer, an address and its capability, which move together as one indivisible pair, the pair a flight builds.

51Record ptr: Type ≔ mkPtr

ptr_addr	: Z
ptr_cap	: cap

A word, the value a temporary holds at run time; the table at the top of the page gives the classes each form is at.

55Inductive word: Type ≔

\|	WInt	n : Z	an integer, or a float's bit pattern
\|	WPtr	p : ptr	a pointer, or a proof of class `a` or `f`
\|	WLimit	c : cap size : Z	`limit(Cap, Size)`: a limit's opaque snapshot

As word_at_class(K, X0, X): the word x taken at class k. An integer is cut to the low 32, 64 or 80 bits of the class (a float word is its bit pattern, an integer); a pointer or proof word is itself, and a limit stays a limit at l. Any other mismatch is the interpreter's type error, here no word.