Several properties, one library

A project's laws, its properties written as harnesses (The qp command), are proved together, as one suite, from one library of function specifications. A unit is a C file that tools/clight.sh translates on its own. By default every law's program links every library unit of quickproof.conf. With LINK=per-law, each law's program links only the units its harness needs, so laws with very different cones (the code each harness can reach) do not all pay for the largest one.

Which units a law links#

tools/link_units.py quickproof.conf prints them, with the code that new_contract.py uses. It reads clightgen's output (code.v), never the C source, so it sees the program that the theorem is about.

• A unit defines a global when its global_definitions give it a function body (Gfun (Internal _)) or a variable with an initialiser (Gvar with gvar_init <> nil).
• A unit needs a global when it uses it and does not define it. It uses a global when one of its definitions names it: an Evar in a function body (a call, or the address of a function or variable; addressable locals excluded) or an Init_addrof in a variable's initialiser. clightgen also declares exactly the globals that a unit uses (plus __builtin_debug), and the declarations count too.
• A law's units are the closure of its harness under "needs", at unit granularity: whenever a linked unit needs a global, every library unit that defines it is linked, with all its definitions, whose needs are followed too.

Under the closure, every global that the per-law program declares and does not define is one that no unit of the project defines, the same globals as in the program of all units. Stopping at the functions reachable from main would not give this, since a linked unit's unreachable functions could name a global of an unlinked unit.

quickproof.conf may fix a law's units with UNITS_<law>=(src/x src/y ...), using the units' output directories as in UNITS. The list must be closed in the same sense and may add units. A list that leaves out a needed unit is refused with a message that names the global, and no contract is written. The contract records whether its units were computed or fixed.

new_contract.py also refuses a law whose program of all units defines a global twice, differently, since there is then no reference program. Under LINK=per-law it refuses any unit that defines a function of the environment (nondet_*, gp_assert, gp_assume, quickproof_malloc, quickproof_free); argument 2 below says why.

The contract#

Each contract states the law's units in a comment and builds the program from Required unit files (src/units/<Unit>.v), so it compiles only the units it links. After whole_prog comes

Lemma whole_prog_undefined : QuickProof.Link.undefined_globals_are whole_prog
  [ "__builtin_debug"; "fopen"; ... ]%list = true.
Proof. vm_compute. reflexivity. Qed.

QuickProof.Link.undefined_globals whole_prog lists the linked program's external functions (EF_external), except environment functions with the environment's signatures, and its variables without an initialiser. The expected list is computed without the unit set: it holds the globals that the law's units declare and no unit of the project defines. A left-out unit that defines a needed global puts that global in the computed list only, so the contract fails to build (tests/run.sh checks this). The list also shows a reviewer every external outside the environment; in a proved program none of them is ever called (argument 2 below).

qp treats src/units/*.v like src/units.v, as frozen contract files that export carries and verify keeps as committed. The program part of a contract that verify and rebuild compare includes whole_prog_undefined.

Soundness: what the theorem says, and why the unit set is not trusted#

The theorem of a law is harness_safe P, where P is its harness linked with its units. Two arguments connect it with F, the harness linked with every library unit, which is what LINK=all proves.

1. With a closed unit set, P and F have the same executions#

F links, so each global has one definition. By closure, every global that P names has the same definition in P as in F, or is undefined in both; main is the harness's in both; and the composite types of P are defined as in F (QPlink checks consistency, and layouts are computed from the members). In CompCert's Clight semantics a program reaches a global only through its name (Genv.find_symbol) or a pointer derived from its address, and integers never become valid pointers. So from main, P and F take the same steps, with memories that differ only by a renaming of blocks and by the blocks of F's extra globals, which P cannot reach. Undefined behaviour does not depend on block numbers: an ordering comparison of pointers into different blocks is undefined in both, and an equality is decided the same way. External calls see the same arguments and memory contents. Hence P has an execution with undefined behaviour exactly when F has one.

This argument about CompCert's semantics is on paper; it is not mechanised in Coq. Neither is the step from semax_prog to "no undefined behaviour" for this environment: VST's adequacy theorem, which makes that step, is not yet instantiated in Coq for it (What a proof means).

2. Even a wrong unit set cannot make a false theorem#

Suppose a unit that defines a global g needed by P were left out. If g is a function, P calls an external g. QuickProof.Link.honest_rejects_foreign (Qed, no axiom) proves that the honest environment HonestEspec gives an external function a witness type, hence a specification a call can satisfy, only when its name and signature are those of an entry of env_specs. Any other external gets VST's NullExtension type, which is empty, so a proved program never calls g, and P and F agree on every execution. If g is a variable, CompCert allocates it as an empty block, so any access is undefined behaviour, and a proved P makes none.

The one way out would be a g that is also a function of the environment, with its name and signature, so that P runs the environment's honest g where F runs the unit's code. Per-law linking closes it off by refusing a unit that defines an environment name, under any signature.

So the unit set is not part of the trusted base. A wrong set makes a contract unprovable or unbuildable; it never makes a theorem false. What is trusted is what What a proof means lists for LINK=all, plus argument 1.

Shared specifications across per-law programs#

Per-law programs differ in their units, hence in their composite types (their compspecs) and in the functions they contain. QuickProof.Assembly (untrusted, no axiom; its header lists the lemmas) makes one body proof per function serve every law:

• Prove each library function's body once, under its unit's compspecs LOGICAL.units.<Unit>.CS, with a context of its callees only (semax_body Vprog Gprog f_x x_spec). A law that links the unit must have every spec of that context in its own G.
• Every law that links the unit contains its composites unchanged, so the body moves to the law's compspecs. semax_body_move takes a body under (cs1, V1, G1) to (cs2, V2, G2); it needs cspecs_sub cs1 cs2, decided by cspecs_sub_by_computation, the variables by find_id and the functions by ctx_sub, which allows funspec_sub. The environment's specs at two compspecs are covered by malloc_spec'_sub, free_spec'_sub and nondet_bytes_spec_cs; the other environment functions do not depend on the compspecs. The tactic entry_shared B turns a body proof B into one entry of a law's G, with every side condition computed. G needs specs only for main, the functions the law reaches and their callees, and the environment functions it calls (harness_safe_of_specs); every other internal function gets VST's vacuous specification automatically, also under LINK=all.
• Prove main against main_spec_std p (the program's global variables and has_ext tt), which is canonical for start_function. semax_body_main_std turns it into harness_safe's main.
• Build the law's compspecs from the program's composites:
  Rocq

  Definition comps := ltac:(let x := eval vm_compute in (prog_composites p) in exact x).
  Definition cprog : Clight.program := Clightdefs.mkprogram comps nil nil 1%positive Logic.I.
  #[export] Instance CS : compspecs. make_compspecs cprog. Defined.

  Calls from main pass data_at at the law's compspecs to a spec at the unit's. Declare #[export] Instance : change_composite_env Unit.CS CS. make_cs_preserve Unit.CS CS. Defined. When forward_call leaves the frame open, rewrite with erewrite (@data_at_change_composite Unit.CS CS _ sh t); [cancel | apply JMeq_refl | reflexivity].

tests/perlaw/, proved by tests/run.sh, is a complete example. Its units are counter.c (with counter_reset, reached by no law and calling log.c), log.c, pair.c and big.c (linked by no law). law_count links counter and log, and law_pair counter, log and pair. proof/Lib.v is the shared library, proof/LawCount.v and proof/LawPair.v are the laws, and proof/Suite.v proves both; Print Assumptions shows only the standard axioms and VST's malloc library. The theorem of law_count reads:

Theorem law_count_proved : harness_safe p.
Proof.
  harness_safe_by_specs CS G main_post_TT.
  - reflexivity.                                                 (* main's spec is G's *)
  - entry_shared (semax_body_main_std _ _ p _ _ body_main eq_refl).
    entry_shared C.body_counter_get.                             (* the shared library's proofs *)
    entry_shared C.body_counter_inc.
    entry_external (@external_ok_u32 CS).                        (* the environment *)
    entry_external (@external_ok_assert CS).
    apply Forall_nil.
Qed.

Choosing#

qp new writes LINK=per-law; use it whenever a project's laws reach different parts of the code. Without a LINK= line the framework keeps LINK=all, so existing contracts do not change (tests/run.sh compares them with golden files). Moving a project to per-law linking changes its contracts, so do it before the proof work starts, in a new proof repository.