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.
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 CompileSimilarly, 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.
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.
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.
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
}
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.