41 Proofs about bounds — intervals, relations, row-major addresses

41.1 Computing with intervals#

The compiler computes with intervals [lo, hi] instead of single values to decide overflow and bounds.

a ∈ [0, 100],  b ∈ [0, 100]
a + b ∈ [0, 200]        lo+lo, hi+hi
a − b ∈ [−100, 100]     lo−hi, hi−lo   subtraction flips --- a common place for mistakes
a × b ∈ [0, 10000]      with mixed signs, min and max of four products

module sum_contract .
rem run: small_sum 100 100
rem ir

fn small_sum input a u8 . input b u8 . output u16 .
  requires le a 100 .
  requires le b 100 .
do
  return add (widen u16 a) (widen u16 b) .
end

$ lowentc --run small_sum sum_contract.low 100 100
small_sum(100, 100) = 200
$ lowentc --ir sum_contract.low
-- runtime checks (interval analysis: overflow · division · narrowing) --
   2 / 2 removed  (100%)

The contract bounds both inputs to 100 or less, so the sum does not exceed 200 and does not overflow u16. Every check disappears. With the same shape but unbounded inputs, the checks remain.

module product_bare .
rem run: product 1000 1000
rem ir

fn product input a u64 . input b u64 . output u64 .
do
  return mul a b .
end

$ lowentc --run product product_bare.low 1000 1000
product(1000, 1000) = 1000000
$ lowentc --ir product_bare.low
-- runtime checks (interval analysis: overflow · division · narrowing) --
   0 / 1 removed  (0%)

1000 × 1000 does not overflow, but the analysis does not know how large a and b can get. So it keeps the check and confirms no overflow only when actual values arrive.

The theorems all point one way. “Places said to be safe really are safe.” The converse — safe but not said to be — is not guaranteed. That is only a performance loss.

analysis goes wide    →  checks remain     →  slow (safe)
analysis goes narrow  →  checks disappear  →  wrong memory access (dangerous)

So every time a rule is added, the question is the same — “can this rule be narrower than reality?”

41.2 Relations — what intervals cannot do#

Intervals look at variables separately. Knowing i ∈ [0, 100] and n ∈ [0, 100] does not tell whether i < n. Yet that is exactly the fact array safety needs. So one-slot relations sit beside the intervals.

lenlt[i] = s     local i is less than len(local s)
lerel[i] = n     local i is less than local n

These facts come from branch conditions. Inside the body of while lt i n, i < n is true, and on the branch where the condition is false, i ≥ n is true. One slot is used instead of heavy relational domains (octagons, polyhedra) because of the shape of real code. Code walking an array is almost always shaped while lt i (len s), and capturing the shape of real code exactly is worth more than sophisticated theory.

The rules for facts have three parts.

1. Obtain. Plant the fact on the branch where the condition is true.
2. Carry. Follow assignments — in var x be j, if j < cap then x < cap. At merges, keep a fact only if both paths agree. What holds on one side only is not a fact.
3. Kill. When a related variable changes, kill the fact in both directions. When a slice is rebound, every fact about its length dies.

The third is the core of safety. Keeping a fact alive too long is exactly wrong check removal, so killing is always the more aggressive side.

41.3 Four stages#

Here are the shapes in which bounds checks vanish, in order of increasing strength. --emit-proof lists each check removed by proof on one line — op name, instruction position, operation, rule used, and the ranges the rule used.

module bound_stages .
rem run: direct [1,2,3]
rem run: stored [1,2,3]
rem run: capacity [1,2,3,4] 3
rem run: grid [1,2,3,4] 2
rem proof

rem 1 --- the loop condition looks at len directly
fn direct input s slice u8 . output u64 . do
  var t u64 be 0 .
  var i u64 be 0 .
  while lt i (len s) . do
    set t (wrap_add t (widen u64 (index s i))) .
    set i (add i 1) .
  end
  return t .
end

rem 2 --- the length is stored in a local
fn stored input s slice u8 . output u64 . do
  let n u64 be len s .
  var t u64 be 0 .
  var i u64 be 0 .
  while lt i n . do
    set t (wrap_add t (widen u64 (index s i))) .
    set i (add i 1) .
  end
  return t .
end

rem 3 --- a contract states the capacity
fn capacity input s slice u8 . input cap u64 . output u64 .
  requires ge (len s) cap .
do
  var t u64 be 0 .
  var j u64 be 0 .
  while lt j cap . do
    set t (wrap_add t (widen u64 (index s j))) .
    set j (add j 1) .
  end
  return t .
end

rem 4 --- row-major address i·n + k
fn grid input a slice u8 . input n u64 . output u64 .
  requires le n 1000 .
  requires ge (len a) (mul n n) .
do
  var t u64 be 0 .
  var i u64 be 0 .
  while lt i n . do
    var k u64 be 0 .
    while lt k n . do
      set t (wrap_add t (widen u64 (index a (add (mul i n) k)))) .
      set k (add k 1) .
    end
    set i (add i 1) .
  end
  return t .
end

$ lowentc --run direct bound_stages.low [1,2,3]
direct([1,2,3]) = 6
  arg0 (written) = [1,2,3]
$ lowentc --run stored bound_stages.low [1,2,3]
stored([1,2,3]) = 6
  arg0 (written) = [1,2,3]
$ lowentc --run capacity bound_stages.low [1,2,3,4] 3
capacity([1,2,3,4], 3) = 6
  arg0 (written) = [1,2,3,4]
$ lowentc --run grid bound_stages.low [1,2,3,4] 2
grid([1,2,3,4], 2) = 10
  arg0 (written) = [1,2,3,4]
$ lowentc --emit-proof bound_stages.low
# proven 12 certified 12
direct 12 index R-IDX-LENLT 0 281474976710655
direct 18 add.i64 R-ADD-LENLT 0 281474976710655 1 1 64 0
stored 14 index R-IDX-LENLT 0 281474976710655
stored 20 add.i64 R-ADD-LEREL 0 281474976710655 1 1 64 0
capacity 16 index R-IDX-LENLT 0 281474976710655
capacity 22 add.i64 R-ADD-LEREL 0 281474976710655 1 1 64 0
grid 8 mul.i64 R-MUL-CAP 0 1000 0 1000 64 0
grid 29 mul.i64 R-MUL-CAP 0 999 0 1000 64 0
grid 31 add.i64 R-ROW-CAP 0 999000 0 999 64 0
grid 32 index R-IDX-ROWMAJOR 0 999999
grid 38 add.i64 R-ADD-LEREL 0 999 1 1 64 0
grid 43 add.i64 R-ADD-LEREL 0 999 1 1 64 0

• 1 · Direct. In direct the loop condition looks at len s directly. index was removed by R-IDX-LENLT.
• 2 · Length stored in a local. stored puts the length in a local with let n be len s. It is a very common idiom. At one time the fact “this value is len s” was a property of a stack value that vanished the moment it was stored in a local, and this loop’s check stayed. Since the fact is now carried by locals too, it is removed just like stage 1. This was a performance fix, not a safety fix — the check was there, so it was safe all along.
• 3 · Capacity from a contract. In capacity the array size and loop bound are different variables. j < cap (loop condition) and len s ≥ cap (contract), so j < len s.
• 4 · Row-major address. grid uses a computed index, index a (add (mul i n) k). Neither intervals nor one-slot relations handle products, yet it was removed by R-IDX-ROWMAJOR. The product and sum of the address were proven along with it, by R-MUL-CAP and R-ROW-CAP.

The additions incrementing i and j vanished too, via R-ADD-LENLT and R-ADD-LEREL, thanks to the same relations. If i < n then i + 1 ≤ n, so it does not overflow.

41.4 The row-major proof#

High-school mathematics, but drop any premise and it collapses.

The last line is the subtlest.

module grid_wrap .
rem run: grid [1,2,3,4] 2
rem proof

rem the same address computed with a wrapping multiply
fn grid input a slice u8 . input n u64 . output u64 .
  requires le n 1000 .
  requires ge (len a) (mul n n) .
do
  var t u64 be 0 .
  var i u64 be 0 .
  while lt i n . do
    var k u64 be 0 .
    while lt k n . do
      set t (wrap_add t (widen u64 (index a (wrap_add (wrap_mul i n) k)))) .
      set k (add k 1) .
    end
    set i (add i 1) .
  end
  return t .
end

$ lowentc --run grid grid_wrap.low [1,2,3,4] 2
grid([1,2,3,4], 2) = 10
  arg0 (written) = [1,2,3,4]
$ lowentc --emit-proof grid_wrap.low
# proven 5 certified 5
grid 8 mul.i64 R-MUL-CAP 0 1000 0 1000 64 0
grid 29 mul.i64 R-ARITH-RANGE 0 999 0 1000 64 0
grid 31 add.i64 R-ARITH-RANGE 0 999000 0 999 64 0
grid 38 add.i64 R-ADD-LEREL 0 999 1 1 64 0
grid 43 add.i64 R-ADD-LEREL 0 999 1 1 64 0

Same formula, but there is no index line. wrap_mul silently wraps on overflow. A wrapped value can get smaller, so the step i·q ≤ (p − 1)·q breaks. In this example n ≤ 1000 so it never actually wraps, but the rule holds only “for stopping multiplication”. If the operation does not stop, it is not a fact.

Then what if the contract’s product p·q itself overflows? The contract’s product is a stopping product, and contract checks are never removed, so if the body was reached it did not overflow. Where bounds checks were removed, the contract check is the only barrier. That is why contract checks are removed by neither modes nor optimisation.

In the development repository’s measurements, this rule cut the bounds checks of a matrix multiplication benchmark from 6 to 1 (the remaining one is index c 0, where n ≥ 1 is missing from the contract), and those of an LRU benchmark whose contract states capacity from 10 to 4.

41.5 Trust proofs, but back trust with checks#

Theorems say the rules are right, but whether the compiler applied them exactly must be confirmed separately. There are two devices.

Analysis self-accusation. The VM does not remove checks. It runs the places the compiler marked “may be removed”, and if a value is actually out of range, it accuses the compiler right there with E-VM-ANALYSIS: … the interval/relational analysis is UNSOUND (this is a compiler bug). The native build has no checks and is fast, the VM has checks and reports when the mark is false, and the back-end cross-check runs both on the same inputs. This device has actually worked. While adding the row-major rule, requires ge (len a) (mul n n) was believed to be a checked contract, but the processor could not read a contract of that shape, so there was really no check, and exactly this diagnostic appeared. Trust only what is checked.

Certificate recheck. The numbers at the end of each --emit-proof line are the grounds. For every removed check the compiler leaves arithmetic grounds (a Farkas certificate), and checkers written separately from the compiler recompute that arithmetic. The certified count on the first line is how many passed. One checker is extracted into OCaml from the Coq code that proved the rule’s soundness (LowentCert.v, LowentCertExtract.v). Nobody confirms “did I transcribe this arithmetic correctly” for a hand-ported checker, but the extracted one is the very function the theorem talks about. Still, this only makes the rule’s arithmetic trustworthy; “does that fact really hold at that place” is outside the checker’s jurisdiction.

41.6 What is not proven#

Some checks do not go away even with contracts. These are the places measured.

• Widening discards information. It goes wide to reach a fixed point quickly, so checks remain even where safe (chapter 39′s count_up). A loss, not a danger.
• Facts about array contents have no place in this domain. “Every element is less than 10” is closed by no requires. It is the tool’s limit, not the program’s defect, and since the check stays the answer is still right.
• Floating-point intervals are not handled.
• The correspondence between analysis rules and theorems is empirical. Self-accusation, certificate rechecks and back-end cross-checks back it (chapter 50).