38 Why prove

38.1 Tests show existence, proofs show absence#

module average .
rem run: mean2 10 20
rem trap: mean2 4294967295 1
rem test

fn mean2 input a u32 . input b u32 . output u32 .
do
  return div (add a b) 2 .
end

test small_numbers
do
  expect eq (mean2 10 20) 15 .
  expect eq (mean2 0 0) 0 .
  expect eq (mean2 1000000 3000000) 2000000 .
end

$ lowentc --run mean2 average.low 10 20
mean2(10, 20) = 15
$ lowentc --run mean2 average.low 4294967295 1
== ir diagnostics (1) ==
0:0 E-VM-OVERFLOW: integer overflow at the declared width (use wrap_*/sat_*, or prove the range)
$ lowentc --test average.low
  [PASS] small_numbers
== tests: 1 run, 1 passed, 0 FAILED ==

mean2, which computes the mean of two numbers, passes all three tests. But given 4294967295 and 1, add a b overflows u32 and stops. Write a million more tests, and if the author does not pick large numbers, the defect does not show.

This is the nature of testing. A test can show “it is wrong on this input (∃)” but not “it is wrong on no input (∀)”. Checking a million natural numbers is not checking all natural numbers. No amount of ∃ adds up to ∀. This gap is the one reason proofs are needed.

 inputs of mean2: two u32 values = about 1.8 × 10^19 pairs

 tests          (10,20) (0,0) (10^6,3·10^6)  three points tried → all right
 counterexample (4294967295, 1)              a point never tried → overflows, stops
 proof          ─── every pair ───           speaks about all of them at once

In Lowent this defect is at least not silent. In C the overflowing sum would wrap and give a wrong mean. Here it stops (chapter 4). And the fixed version is written in a shape that cannot overflow.

module average_fixed .
rem run: mean2 4294967295 1
rem ir

fn mean2 input a u32 . input b u32 . output u32 .
do
  let lo u32 be min a b .
  let hi u32 be max a b .
  return add lo (div (sub hi lo) 2) .
end

$ lowentc --run mean2 average_fixed.low 4294967295 1
mean2(4294967295, 1) = 2147483648
$ lowentc --ir average_fixed.low
-- runtime checks (interval analysis: overflow · division · narrowing) --
   1 / 3 removed  (33%)

Adding half the difference of the two numbers to the smaller cannot overflow. --ir says it removed one of three checks. The remaining two stay even though they really cannot overflow, because the interval analysis does not know the relation between min and max. The analysis is wrong only in the safe direction — when it cannot prove, it keeps the check.

38.2 Overlapping three layers#

They are overlapped because the three catch different kinds of mistakes. Drawn as who checks what against what:

 rules of the spec ── modelled ──▶ Coq model ── proof ──▶ every case in the model
                                     ▲
                                     │  exhaustive checking: model vs implementation, small sizes
                                     ▼
 compiler ─┬─ run on the VM ───┐
           └─ emitted as C ────┴─▶ cross-check: different answers = compiler defect

Proofs look at the model, cross-checks look at the implementation, and exhaustive checking ties the two together. In this repository cross-checks caught defects the proofs missed, and proofs caught defects cross-checks missed. And this part does not mix three words. “Proven” means Coq checked every case, “exhaustively checked” means every case of a fixed size was run, and “sketch” means a person argued it but no machine checked.

38.3 What is proven#

The proof files are all in docs/proofs/coq/. This is the scale counted for this edition.

In Coq, Admitted means “assume this is true and move on”, and Axiom means “this is assumed”. If even one such place exists, every theorem in the file relies on that assumption. Both are 0. What is proven and what is not yet is written in docs/proofs/LEDGER.md.

Grouped, it looks like this.

The last chapter (chapter 50) gathers what all of these rely on and what they do not cover.

38.4 Three ways of proving#

You do not need to read proof scripts. But knowing how something was proven gives a sense of how much to trust the theorem.

Invariant preservation. Show that “a property is kept every time the program takes a step”. If it is true at the start (base) and a step carries truth to truth (preservation), it is true however many steps are taken. It is the program version of mathematical induction. The theorems for borrowing rules and loops take this approach.

Reduction to an order structure. Turn the problem into one about an order and answer it with properties of the order. Making “u8 fits safely into u32” into a partial order turns “which type to pick when joining two types” into the well-known notion of a least upper bound. Numeric widening and the weak-memory model take this approach.

Exhaustive checking. Properties not yet proven for all sizes are run for every case within a fixed size. This is not proof, and this part says so.

38.5 Promises this part keeps#

This part keeps three promises.

• It does not mix words. “Proven”, “exhaustively checked” and “sketch” are different strengths. “This language is proven” is often really “a few short cases were run”.
• Every theorem comes with the defect it stops. Theorems whose defect could not be named were left out. A theorem with no value to the reader has no reason to be here.
• This part is not normative. The language is defined by the specification’s clause canon. If this part disagrees with it, this part is wrong.

And the ideas this language rests on, reduced to six lines, are these. All six are either backed by mathematics or written down as not backed — that distinction is the purpose of this part.

1. Make wrong programs impossible to write. Making them inexpressible is cheaper than catching them (chapter 42).
2. Answer “I don’t know” when you don’t know. Failure is a value — option or result — not a hidden exception.
3. Costs must be visible. Allocation, side effects and copies are all written in the source (chapter 44).
4. When in doubt, keep the check. Checks are removed only when there is a proof (chapter 41).
5. Two implementations must give the same answer. If the VM and native code differ, it is a compiler defect (chapter 31).
6. Write down what was not done. Assumptions, limits and what is unproven are recorded (chapter 50).

 theorem ────────────────▶ decides which shapes the compiler must reject
                            e.g. the condition for uN ⊑ iM is N < M (strict)
 a defect the compiler hit ▶ turned into a theorem
                            e.g. laundering a borrow through a function
                            remove that check and the proof breaks