rocq/theories/Validate.v
The validator of checked IR, transcribed from ir.pl's valid_module/1 for the core subset: valid_funcmd f is true exactly when ir.pl accepts the function f of the module md, checked stage, filc mode; valid_data and valid_alias do the same for the module's data objects and aliases.
ir.pl's validator throws nanofil_error(Message) at the first problem and fails on a few terms outside the grammar; both are false here. The order of the tests therefore does not matter, and the definitions below follow ir.pl's clause groups, not its order of evaluation. In three places ir.pl's result still depends on how Prolog evaluates, not only on what its clauses say: the memo of offset_interval/8 and the cuts of pointer_distance/4 and op_interval/9; oi, pointer_distance and op_interval follow them.
Parts
| Gallina | ir.pl | Checks |
|---|---|---|
valid_use | valid_use/3 | an operand read at a class its definition allows |
valid_op, op_result_ok | valid_op/1, op_result_ok/3 | an op's parameters and its result class |
valid_inst, valid_jump, valid_phi | the same | each instruction, jump and phi |
definitions_dominate | the same | strict SSA: every use has a dominating definition |
valid_locals | the same | named locals declared once, in the entry block, before use |
stage_func | the same | every access covered by evidence that still holds; a poll on every cycle |
valid_data | valid_item/4 for data | alignment, linkage, item shapes; a table entry names a function, a weak declaration no local definition, no pointer a table entry |
valid_alias | valid_item/4 for aliases | linkage, a name of its own, a target the module defines |
stage_func is the part Campaign 3 is about: the evidence pass, in which a check must be followed at once by an access it covers, a later scalar access may read a proof whose fact is still live, and each reuse form has its own side conditions, stated over the single definitions of the function, the guard chains of flights from a pointer to its bases and the offset intervals.
Names, uses and definitions
Whether the name n is in the list ns.
Whether the operands v and w are the same temporary, the same symbol or the same constant.
The temporaries among the operands vs, in order; constants and symbols are dropped.
As inst_temp_def/3: the temporaries the instruction i defines, each with its class: a let's or a flight's destination, or a call's results.
As cfg:inst_def/2, its first solution: the first temporary the instruction i defines, if it defines one.
The operand of a call argument a.
The class a call argument a is passed at.
As cfg:flight_arg_value/2: the operand of a flight argument, whether it is the address operand or a plain value.
As cfg:inst_uses/2: the temporaries the instruction i reads, a flight's lower donor included.
As cfg:jump_uses/2: the temporaries the jump j reads, a branch's condition or the values it returns.
As jump_edge/2, all its solutions: the edges the jump j may take, both arms of a branch; a return takes none.
The labels of the blocks the jump j may go to, over poll edges too.
Whether the edge t is a poll edge, one that passes a safepoint on the way to its target.
Dominance
Whether the label lists a and b hold the same labels, in any order and number.
As cfg:dominates_by_interval/3: whether block a dominates block b, read off the dominator-tree intervals doms that block_intervals numbers.
Whether the label l is reachable from the entry, that is, has a dominator interval in doms.
As block_sites/1 with the parameters' sites added: each temporary of the function f with every one of its definition sites. A temporary may have several; definitions_dominate asks only that one of them dominate each use.
As site_dominates/4: whether the definition site s comes before position i of block l on every path from the entry. A parameter always does; a site in l itself does when its index is smaller; a site in another block does when that block dominates l.
As dominated_use/4: whether some definition of the temporary n, among its sites in sites, dominates position i of block l.
As definitions_dominate/3, the strict SSA (static single assignment) rule: in every reachable block of the function f, each use of a temporary, by an instruction or the jump, is dominated by one of its definitions. A phi's operand counts as used at the end of the predecessor it comes from, if that predecessor is reachable.
Classes of temporaries
As temp_defs/3: every definition in the function f, as a temporary with its class: the parameters, then each block's phis and instructions.
As check_temp_classes/2: each temporary has one class, that is, each of its definitions in defs has the class of its first one.
As proof_class/1: whether k is a proof class, a for an access proof a check defines or f for the function proof check_function defines.
As valid_use/3: whether the operand v may be read at the class k, given the class of each temporary (classes).
- A proof or float temporary is read only at its own class, and a proof or float class reads only a temporary of that class.
- A
p(pointer) temporary is read only atp, andpreads only aptemporary. - A long (
l) temporary may be read as a word (w), not the reverse. - A float constant is a bit pattern below its class's modulus; no constant is a proof.
- No symbol is read here: in filc mode only a
copyreads one (valid_inst).
Ops
The alignments a check may prove, as valid_op/1 lists them: 1, 2, 4, 8 or 16 bytes.
As alloc_align/1: an alloc's alignment al is a power of two from 4 to 4096.
What valid_op/1 asks of a check's parameters: a nonempty span, lo below hi, at an alignment al that check_align allows.
As local_offset/1: off is a signed 64-bit offset.
The effects a heap raw_store_pointer declares, as pointer_memory_effects/2 lists them for a store: ensure the aux word, the lower barrier, reload the root, then write the lower and the address.
The effects of a pointer store to a proven local object, which has an explicit stack aux: write the lower and the address (pointer_memory_effects/2's local_store).
The effect of an atomic pointer load, which leaves the whole protocol to Fil-C's helper (pointer_memory_effects/2's atomic_load).
The effect of an atomic pointer store, which leaves the whole protocol to Fil-C's helper (pointer_memory_effects/2's atomic_store).
As comparison/2: whether the condition c compares values of the class k. The signed and unsigned orders compare integers, the float conditions floats, and eq and ne both.
As valid_op/1 for the core subset's ops: the parameters an op carries are well formed. A check or reuse form needs check_ok; a check_ahead also an early end ahi strictly inside its span; a span test a nonempty span of signed 64-bit offsets; a limit a size from 1 to 2^31 - 1; a check_local a signed 64-bit offset, a size in that range and a check alignment; a raw pointer load one of the heap, local or atomic effect lists.
As any_class/1: a class a value may have, every class but the proof classes (proof_class).
As op_result_ok/3 in filc mode: the op o may define a temporary of class k. Arithmetic gives an integer or float class as the op allows; conversions give the class they convert to; a check or reuse form gives an access proof (a), check_function a function proof (f), a span test a word and a limit a long.
Signatures
The atom ir.pl writes for the class k, so that a class can be compared with the term of a function outside the core subset.
The term ir.pl writes for the return type r of a function.
What a call site needs of its callee, the function func_named/3 finds: its linkage, its parameters' classes, its return type and whether it is variadic, each as ir.pl writes it.
Whether the term t is a let of va_args, the mark of a variadic function's body.
The sig of a function outside the core subset, read off its term t.
As func_named/3: the sig of the first function the module md defines under the name n, in the core subset or outside it.
Whether the term t is a float class's atom: s, d or x.
As call_result_ok/4: the result r a call binds fits the callee's return type ret. A tuple must match it exactly; one result follows to_result_ok/4 and class_result_ok/4: floats only as the same class, a long result never from a word return, and a pointer result exactly from a pointer return.
Whether the terms ps are a prefix of the terms xs: a variadic callee's fixed parameters, against a call's argument classes.
Instructions, jumps and phis
The labels of the function f's blocks.
As store_value_class/2: the class of the value a raw store of the width w writes. None for a pointer width, which only raw_store_pointer stores.
As not_init_entry/3, negated: whether the symbol s names a constructor or destructor table entry of the module md, which nothing may copy or call.
As valid_inst/2: the instruction i of the module md is well formed, its operands read at the classes given (classes, through valid_use).
- A flight is a
copy,addorsubwith addresses atp, offsets atland a pointer lower donor. - A
copyof a symbol atp(a getter) names no constructor or destructor table entry. - Any other
lethas a valid op (valid_op,op_result_ok) and operands at the classes the op reads;va_argstakes a nonnegative constant. - A raw store writes a value of its width's class through an access proof (
a); a raw pointer store has one of the heap, local or atomic effect lists. - A direct call matches its callee's
sigwhen the module defines it; an indirect call reads a pointer callee, araw_calla function proof (f).
As valid_jump/2: the jump j of the function f is well formed: its targets are labels of f, a branch reads its condition as a word, and a return returns what f's return type says.
As valid_phi/4: the phi ph names exactly the block's predecessors preds, as sets, and each of its values is read at its class.
As valid_block/2: the block b of the function f has valid phis, instructions and jump, and a block with phis has a predecessor.
As proof_class_defs/3: only a check defines a proof in the function f; no parameter, phi, call result or call argument has a proof class.
Whether no name occurs twice in ns.
As valid_locals/3: each local object of the function f is declared once, by a local_alloc in the entry block; there each check_local of it comes after the declaration, and in another block it needs only the declaration.
Evidence
Whether the facts a and b are equal in every field.
As evidence_kill/3 with evidence_names/2: the facts fs without those whose proof or pointer is the temporary d, which is being defined again.
As evidence_after/3: the live facts fs after the instruction i. An instruction that is not evidence_preserving ends them all; otherwise only the facts naming what it defines end.
As evidence_meet/2: the facts in every one of the sets, the evidence a block may assume from all its incoming edges; none for no sets.
Accesses
What a raw access reads or writes, raw_access/5's X: a load type, a store width, or a pointer.
As raw_access/5: the instruction i as a raw access: the proof q it goes through, what it moves, its offset from q's pointer and the rights it needs (read for a load, write for a store).
As access_size_align/3, its first solution: the bytes an access of type x moves, and the alignment its address needs: 8 for a pointer, 8 for an 80-bit float, 1 for the rest.
As rights_allow/2: rights have serve an access that needs need; write rights also allow a read.
As covered_access/6: the instruction i is a raw access through the proof q whose bytes lie from lo up to hi, whose start is aligned as the access needs given q's alignment al, and that the rights r allow: the coverage a proof gives.
Where a raw access goes: the heap or a proven local object.
| | | Heap' | ||
| | | Local' |
As access_storage_effects/2: the access i declares the effects of its storage s. A scalar access always does; a pointer access must declare the heap's, the local's or the atomic effects.
As proof_use/6: the instruction i, right after the check of the proof q, uses it: a heap raw access the proof covers (covered_access).
As reusing_access/2: whether the access i, of type x, may read a live proof that is not its own check's: a scalar access, or a heap pointer load, which reads aux and box words only. A pointer store may exit while ensuring the aux, and keeps its own check.
Single definitions, chains and intervals
A temporary's one definition, an entry of the map Once that single_definitions/3 builds: a parameter, a phi or an instruction.
Every definition of the function f, as a name with what defines it: parameters, phis and instructions.
As single_definitions/3: the temporaries of the function f with exactly one definition, each with it. The reuse forms' rules read only these names: a single definition that dominates a point holds the value it computed there.
Whether the name n has a single definition in once.
As near_offset/1: k is well inside the signed 64-bit range, within 2^62 of 0. Offsets on a guard chain are exact only modulo 2^64; only near ones are the true distance.
As signed_value/3: the constant c taken as a signed integer of the integer class k's width.
As narrow_range/3: the values a narrow type t extends to, for the signed and unsigned bytes and halves; none for the rest.
As interval_fits/3: an offset interval from lo to hi suits the class k. A word (w) interval must lie in the signed 32-bit range, so no word arithmetic wraps; a long (l) one may be anything, since it bounds the value only modulo 2^64.
The memo's answer for the name n at the class k, if it has one.
Whether the operand v is a constant.
As op_interval/9: the offset interval of what the op o computes from args at the class k, with rec the walk of an operand one level deeper and m the memo. Each clause commits once its head matches, as ir.pl's cuts do: an and tries its right operand as the mask before its left one, and a failed ext(sw) does not fall through to a later clause.
As offset_interval/8: the interval from Lo to Hi in which every value the operand v of class k can hold lies (for l, modulo 2^64), walked through the single definitions once, at most 32 deep. It threads ir.pl's memo in the same order: each name's answer is kept, so a name met again deeper than the limit allows still has its interval, but a failed walk keeps nothing it memoised on the way, and only records the name as having none.
As offset_interval/6 from depth 0: the offset interval of the operand v at the class k, if one is derived. Interval.v proves what it answers derived and sound (offset_interval_iv, iv_sound).
As flight_term/5: when the flight op o with args moves the base b, the offset it adds to b and its sign: an add of an offset, a sub of one, or a copy, which adds 0.
The walk of guard_chain, fuel steps at most: the pointer p at the offsets lo to hi from the start, then each base it reaches.
As guard_chain/3: the guard chain of the pointer p. First p at offset 0 from itself, then each base b whose capability p has, through single-definition add, sub and copy flights whose lower donor is their address operand, with the interval of p's offset from b.
A chain element e as an exact base: a single-definition temporary at one known offset, with that offset.
The first answer f gives over the list xs.
As pointer_distance/4: the distance D, modulo 2^64, from the pointer p1 to the pointer p, which has p1's capability: both reach one exact single-definition base on their guard chains, and D is the difference of their offsets from it. Like ir.pl, which cuts after the first, it takes the first base of p's chain that p1's chain shares.
As half_known/6: a half check of the span from lo up to hi of a pointer P may test only its bound bd, when P is d0 bytes from a pointer whose passed check proved the span from lo1 up to hi1 (see docs/half.md). With d0 taken signed modulo 2^64: for upper, P+lo lies at or above the old span's start; for lower, P+hi lies at or below its end; both distances are near (near_offset) and the span is at most 2^62 bytes, so nothing wraps.
As renew_source_op/6 with stage_sources/4's conditions: a renew source, when the instruction i is a single-definition proof q1 of a single-definition pointer p that a later reuse form may lean on (a check, check_ahead, renew_if, check_limit or half_check): q1 with p, its bounds and its alignment.
As hull_renewable/8: a renew_hull of the pointer p over the bytes from lo up to hi, at alignment al, may lean on the two renew sources ql and qh: the span lies between ql's start and qh's end at distances from 0 to 2^62 (pointer_distance), is at most 2^62 bytes, and one of the sources gives the alignment.
As guard_covers/5: the operand g is a single-definition span test of a single-definition pointer n0 whose span contains the bytes from lo up to hi of the pointer p, for every offset p can have from n0 on its guard chain: what a renew_if needs of its guard.
As lower_chain/3: the pointer p has the lower of the base b: p is b, or a single-definition flight whose lower donor has b's lower, whatever its address (a lower chain).
As limit_covers/5: the operand u is a single-definition limit of size bytes of a single-definition pointer n0 whose lower p has (lower_chain), and the access span from lo up to hi is exactly from 0 up to that size: what a check_limit needs.
As hull_covered/7: the instruction i, a raw access through the proof q of the pointer p, lies within the hull of the live facts about p's object: one fact's span starts at or before it and one ends at or after it, measured from p by pointer_distance at near offsets (near_offset). It is aligned as q's proof gives (q's offset lo, alignment al), and a write needs a fact with write rights.
Scheduled checks
The needs at a point of the backward pass of scheduled checks: each base with the offset its bytes are certain to be accessed up to.
The needs fs without the base n's.
As ahead_meet/2: the bases in every one of the need sets fss, each with its least need; none for no sets.
As raise_need/6: the needs fs after an access of size bytes at offset off from the chain element e: when e is an exact base n at offset k, and k and its end are near (near_offset), n's need is raised to at least that end.
As ahead_step/5: the needs fs before the instruction i, given those after it. An instruction that is not ahead-transparent ends every need; one that defines a base ends that base's; a raw access through a proof of ptrs raises the need of each base on its pointer's guard chain (raise_need).
As proof_pointer/3: the pointer that the check or reuse form o with args proves.
As proof_pointers/3: each single-definition access proof of the function f with the pointer it proves.
The proof ahead_insts/8 accepts at the instruction i: a single-definition check_ahead q of the pointer P whose access is followed by the needs next, when some exact base N of P at offset K, with K and K + lo near (near_offset), has a need of at least K + hi there.
As ahead_insts/8: the check_ahead proofs accepted in one block, walking its instructions ris from the last. after are the needs after the current instruction, next those after the one that follows it, its access; js collects the accepted proofs.
The position of the label l in ls, counting from n.
As ahead_edge/5: the needs the edge t carries back to the block at position pos: its target's entry needs if it is a plain edge to a later block, none over a poll edge or an edge to the same or an earlier block.
As phi_ends_need/3, folded over the phis phs: a phi redefines its destination at the block's entry, which ends that base's need.
As ahead_block/6: one block b of the backward pass. Its exit needs are the meet over its jump's edges; its entry needs go into ins and its accepted proofs into js.
Every block's entry needs and the accepted check_ahead proofs, from one pass over the function f's blocks in reverse order.
As ahead_justified/3: the scheduled checks of the function f that are justified: right after its access, its pointer's base needs at least the bytes up to the check's end, so where the check fails early the original program would have trapped later on every path. The needs are computed backward in one pass over the blocks in reverse order; any edge into a later block was walked first.
Getters
The linkage of the first function the module md defines under the name g, in the core subset or outside it.
The linkage of the first data the module md defines under the name g, skipping extern(weak) declarations, which define nothing.
As local_global/2: g is a function or data object the module md defines with local linkage, as the first item of that name says, so its getter is a local symbol only this module calls.
As repeated_getters/4: each single-definition getter copy d of a local symbol g (local_global) that another copy of g dominates, earlier in its block or in a block that strictly dominates it. Such a copy repeats a call of the getter that has already returned, so it reaches no safepoint, frees nothing and stores nothing, and the evidence pass lets the live facts survive it.
The evidence pass
What stage_sources gathers for one function, stage_sources/4's src: the renew sources, the single definitions, the justified scheduled checks and the repeated getters.
| s_renews | ||
| s_once | ||
| s_ahead | : listname | |
| s_getters |
As stage_sources/4: the src of the function f of the module md, with doms its dominator intervals.
The live facts after a check-like instruction i of the proof q over the bytes from lo up to hi and its access: as ir.pl does, evidence_after/3 of the check, then evidence_add/3 of the new fact, then evidence_after/3 of the access.
As checked_inst_rest/7, one step of the evidence pass: None when ir.pl throws; otherwise the instructions left after the instruction i, and the live facts after.
- A check or reuse form (renew, renew_hull, half_check, renew_if,
check_limit, an accepted check_ahead) must be followed at once by an access it covers, which it consumes, and adds its fact. - A
check_localand acheck_functionare used once, right away. - Any other raw access must read a live fact that covers it, directly or by the hull of the live facts (
hull_covered). Araw_callnot right after itscheck_function, an indirect call, and pointer arithmetic,itopor a pointer copy outside a flight are refused. - A repeated getter (
repeated_getters) ends only the facts naming its destination; any other getter ends them all.
As checked_insts/5: the live facts at the end of the instructions is, starting from live, or None when one is refused; fuel bounds the steps.
As incoming_edges/2 for the label l: its incoming edges, each with whether it is a poll edge, one per jump target, the last first (add_edge/3 prepends).
As checked_block/6, folded over the function f's blocks in order (in stage_func/6): the evidence pass. A block's entry evidence is the meet over its incoming edges of the facts each carries, none over a poll edge or from a block not yet walked; a phi ends the facts naming its destination; then each instruction must pass checked_inst_rest.
As limit_reads/2: a limit of the function f is read only as a check_limit's second argument, never by a phi, a jump or another instruction.
The search of polls_every_cycle: blocks with no unpolled edge into what is left of the graph g are removed until none is left (acyclic) or none can be (a cycle without a poll).
As polls_every_cycle/1: every cycle of the function f's control-flow graph, unreachable blocks included, has a poll edge: without them the graph is acyclic.
As stage_func/6 for the checked stage: the function f passes the evidence pass, reads its limits only in check_limit, and polls on every cycle.
The stage
Whether the op o is a word only the checked stage uses: a check, a reuse form, a span test, a limit or a raw load (the let clauses of checked_inst/1).
As checked_inst/1: the instruction i uses a word of the checked stage: a checked op, a raw store, a raw call or a flight.
As checked_jump/1: the jump j takes a poll edge.
checked_op, read off the term t of a function outside the core subset.
checked_inst, read off the term t of an instruction outside the core subset, a touch included.
checked_jump, read off the term t of a jump outside the core subset.
As module_stage/2: the module md is in the checked stage when any function uses a word of it, a check, raw access, flight or poll edge. The stage is read off the vocabulary of the whole module, never stated: a module whose only checked word is one poll edge is unchecked without it, and then needs no poll on its cycles.
Functions and modules
The x rule of valid_item/4 for a function: whether an x (80-bit extended float) value of the function f crosses where it may not: as a parameter, the result, a call's argument or result, or a phi.
As valid_item/4 for a function f of the core subset of the module md, in filc mode: it has blocks and a linkage of export, local or weak, a valid return type, no x crossing (extended_crosses), distinct labels, one class per temporary, no jump to the entry block, proofs defined only by checks, the strict SSA rule, valid locals and valid blocks; in a checked module also stage_func. In the unchecked stage there is no evidence to check, and the core subset then has no memory access at all.
Data
As data_align/1: a data object's alignment a is a power of two from 1 to 4096.
The linkage clauses of valid_item/4 for data: the linkages lk the data of a Fil-C module may have, and what extern(weak) (no items) and init(Kind, Prio) (a constructor or destructor, a priority up to 65535, one pointer item at offset 0) ask of its items its.
What valid_item/4 asks of each data item it: it has one of the header's shapes (data_item_shape/1), a float item's constant is below its class's modulus, a string holds bytes, and a pointer names its symbol by an atom. In a Fil-C module item(l, sym(_, _)), like any other term, decodes to ItemOther and is refused.
As pointer_items_aligned/3: each pointer item of its, counting off bytes into the object, starts at a multiple of 8.
Whether the module md defines a function named n, in the core subset or not (func_named/3).
As data_named/2: the module md defines data named n, that is, data of that name not declared extern(weak).
What data asks of the rest of the module md: a constructor or destructor table entry names a function the module defines; a weak declaration is of no name the module defines with local linkage (local_global/2), whose symbols it would make weak and global; and no pointer item names a table entry, which has no address.
As valid_item/4 for data(Name, Linkage, Align, Items): the data object n of the module md has a valid alignment, linkage and items, its pointer items aligned, and names it may refer to.
Aliases
The first function of each name in the module md, as module_symbols/2 indexes them; seen are the names met so far.
memberchk(call(_, global(Name), _), Is) for some block of the function it: whether it calls the symbol n directly, read off its blocks in the core subset or off its term outside it.
The name of a function item it, in the core subset or not.
As valid_item/4 for alias(Name, Linkage, Target): the alias n of the module md has linkage export or weak, no function or data shares its name, and its target is a function the module defines, or data of a linkage an alias may name (export, local, weak or ro(_)) that no other function calls through the alias.
Modules
As defined_name/2: the name the item it defines; a weak declaration defines none.
As unique_names/1: no two items of the module md define the same name. Functions, data and aliases share one namespace.
No two items of the module md share a name, and each item the model can judge is valid: functions, data and aliases.
As valid_module/1 for a Fil-C module without its contexts: whether the validator accepts the module md, or None when a function is outside the core subset, which the model cannot judge. The context/2 items are provenance's records, which provenance:valid_contexts/1 checks and interp:run/5 never reads; the model has none (docs/rocq.md).