# 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 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.

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.