For a slice or array `x`

, an expression like `x[i .. j]`

is invalid unless the compiler can prove that `((0 <= i) and (i <= j) and (j <= x.length()))`

. For example, the expression `x[..]`

is always valid because the implicit `i`

and `j`

values are `0`

and `x.length()`

, and a slice or array cannot have negative length.

Similarly, an expression like `x[i]`

is invalid unless there is a compile-time proof that `i`

is in-bounds: that `((0 <= i) and (i < x.length()))`

. Proofs can involve natural bounds (e.g. if `i`

has type `base.u8`

then `(0 <= i)`

is trivially true since a `base.u8`

is unsigned), refinements (e.g. if `i`

has type `base.u32[..= 100]`

then 100 is an inclusive upper bound for `i`

), facts (e.g. an explicit prior check `if i < x.length()`

) and interval arithmetic (e.g. for an expression like `x[m + n]`

, the upper bound for `m + n`

is the sum of the upper bounds of `m`

and `n`

).

For example, if `a`

is an `array[1024] base.u8`

, and `expr`

is some expression of type `base.u32`

, then `a[expr & 1023]`

is valid (in-bounds). The bitwise-and means that the overall index expression is in the range `[0 ..= 1023]`

, regardless of `expr`

's range.

Arithmetic overflow checking uses the same mechanisms as bounds checking. For example, if `m`

and `n`

both have type `base.u8`

(or a refinement thereof) then the expression `m + n`

also has type `base.u8`

. Proving that `m + n`

evaluates to something inside the `base.u8`

range, `[0 ..= 255]`

, is equivalent to proving that the expression `h[m + n]`

is valid (in-bounds) for a hypothetical `h`

array of length `256`

.

`nullptr`

CheckingGuarding against `nullptr`

dereferences is another case of bounds checking. Like other programming languages, `nptr T`

and `ptr T`

are types: nullable and non-null pointers to some type `T`

. In Wuffs, the latter is effectively a refinement. Assuming that `nullptr`

is equivalent to `0`

, `ptr T`

is conceptually just `(nptr T)[1 ..= UINTPTR_MAX]`

, although that's not actually valid syntax. Similarly, if `expr`

is a pointer-typed expression then checking that `expr`

is not `nullptr`

is equivalent to checking that `expr`

is in the range `[1 ..= UINTPTR_MAX]`

.