39 The mathematical toolkit

39.1 Six tools#

39.2 Sets and relations#

A set is a collection — {0, 1, 2}. A relation is a list of pairs. The relation “less than” is a collection of ordered pairs such as {(0,1), (0,2), (1,2)}. In talk about programs, a relation “widens safely” is placed over the set of types {u8, u16, u32, u64, i8, …}. That relation is written ⊑ and read “the left fits into the right without changing value”. It resembles ≤, but it speaks not of numeric size but of whether it can be held.

39.3 Partial orders — incomparable pairs#

Numbers are always comparable. Of 3 and 5, one is larger. Types are not. u8 ⊑ u16 ⊑ u32 ⊑ u64 and i8 ⊑ i16 ⊑ i32 ⊑ i64, but neither u32 nor i32 holds all of the other. u32 holds up to four billion and i32 holds negatives. The structure that honestly captures the fact that neither can be called larger is a partial order.

These three must be proven for “safe widening” to mean anything. If transitivity broke, the language would allow u8 → u16 and u16 → u32 but block u8 → u32. Users could never find out why. The three are proven for the real types in chapter 40.

39.4 Lattices and join — what to pick when combining#

When two values go into one operation, the processor must compute in a type holding both. There are several candidates, but the right one is the smallest. That “least common upper bound” is called the join and written ⊔. A partial order where any two elements always have a join is a lattice.

module widening .
rem run: wider 200 60000
rem trap: wider 255 65535

rem adding u8 and u16 computes in the smallest type holding both (u16)
fn wider input a u8 . input b u16 . output u32 . do
  return add a b .
end

$ lowentc --run wider wider.low 200 60000
wider(200, 60000) = 60200
$ lowentc --run wider wider.low 255 65535
== ir diagnostics (1) ==
0:0 E-VM-OVERFLOW: integer overflow at the declared width (use wrap_*/sat_*, or prove the range)

u8 ⊔ u16 = u16. So even though the output type is u32, the addition happens in u16, and 255 + 65535 overflows u16 and stops. The join is decided by the operands, not by the place that receives the result.

With mixed signs it defies intuition. u8 ⊔ i8 is not i8 but i16 — holding both 255 from u8 and −128 from i8 needs a wider type. People get this wrong. Lowent does not pick this widening for you; it makes you write it.

module sign_join .
rem expect: E-TYPE-SIGN

rem the type holding both u8 and i8 is i16. The processor does not pick that widening for you
fn mix input a u8 . input b i8 . output i16 . do
  return add a b .
end

$ lowentc --check sign_join.low
sign_join.low:6:0 E-TYPE-SIGN: sign mismatch: no value-preserving widening exists (widen both to a strictly wider signed type, or bitcast_sign)

The “strictly wider signed type” in the diagnostic is exactly u8 ⊔ i8 = i16. Widening both to i16 explicitly is accepted.

39.5 Monotone functions and fixed points — why analysis stops#

A monotone function is one whose output does not get smaller as its input gets larger. A fixed point is a point where f(x) = x — applying once more changes nothing.

These two ideas do the work when the processor analyses a loop. The analyser does not know a variable’s range on entering the loop. So it starts narrow and widens repeatedly.

after round 1: i ∈ [0, 0]
after round 2: i ∈ [0, 1]
after round 3: i ∈ [0, 2]      … this way it never ends

So it uses widening. After seeing it widen a few times, it decides “this will keep growing” and pushes to the top at once. Combining i ∈ [0, ∞) with the loop condition i < 10 gives i ∈ [0, 9], and one more round still gives [0, 9]. It has reached a fixed point and the analysis ends.

module count_up .
rem run: ten
rem proof

fn ten output u8 . do
  var i u8 be 0 .
  var s u8 be 0 .
  while lt i 10 . do
    set s (add s i) .
    set i (add i 1) .
  end
  return s .
end

$ lowentc --run ten count_up.low
ten() = 45
$ lowentc --emit-proof count_up.low
# proven 1 certified 1
ten 14 add.i64 R-ARITH-RANGE 0 9 1 1 8 0

There is one proof line. add i 1 adds within i ∈ [0, 9], so it is proven not to exceed u8 (R-ARITH-RANGE 0 9). add s i is not proven, because widening threw away the upper end of s. In reality s never exceeds 45, but the analysis does not know that. So the check stays — slow, but never wrong.

• That a fixed point always exists is the guarantee that the analysis stops.
• Widening goes wide. Going larger than reality only fails to remove checks; it never gives wrong answers. This direction is the heart of abstract interpretation.

39.6 Induction and invariants — dominoes#

Mathematical induction goes like this. P(0) is true, and if P(n) is true then P(n+1) is true. Then P(n) is true for every n. In programs, n becomes “steps executed”, and P is called an invariant — a property true throughout execution.

39.7 Abstract interpretation — ranges instead of values#

To learn something about values without running the program, you must handle sets of values instead of single values. Handling sets as they are is too large, so a simple approximation is used. The typical one is the interval [lo, hi].

if x ∈ [0, 5] and y ∈ [10, 20]
x + y ∈ [10, 25]      add the ends
x × y ∈ [0, 100]      with mixed signs, take min and max of four products

There is one rule. The result of an abstract computation must include every value actually possible. If x is always 3 but the analysis answers [0, 5], it loses something but is safe (it cannot remove a check). If x can be 7 but the analysis answers [0, 5], the moment a check is removed on that answer an out-of-range access happens. So every rule of the analysis leans “wide”.

39.8 Table of symbols#

39.9 How the tools interlock#

partial order ⊑           defines "fits safely"                 (numbers)
   │
   ├─ join ⊔              picks the type when combining         (numbers · effects)
   │
monotone functions        loop analysis climbs over them        (bounds)
on a lattice
   │
fixed point               where analysis stops                  (bounds · loops)
   │
soundness of abstract     erring "wide" keeps conclusions safe  (bounds)
interpretation
   │
invariants and induction  show it holds throughout execution    (ownership · loops · races)

It reads bottom to top too. Induction keeps invariants, those invariants come from the soundness of abstract interpretation, abstract interpretation runs on a lattice, and a lattice stands on a partial order. Without the tools design becomes guesswork — a join table written by hand mixes in lines like u8 ⊔ i8 = i8 and turns 255 into −1, loop analysis without widening never ends, and a borrow check without invariants becomes a pile of “allowed here, not there” rules.