A function that can suspend execution and, when called again later, resume where it left off, in the middle of the function body. See the coroutines note for more details.

Dependent Type

A type that depends on another value. For example, a variable n‘s type might be “the length of s”, for some other slice-typed variable s. Dependent types are a way to implement bounds checking, but they’re not the only way. Wuffs does not use them.


An extension of the type system, applied to functions. Wuffs has three effect categories: pure, impure and coroutine. Pure means that the function has no side effects - it does not change any observable state. The other two categories may have side effects, with coroutines also being able to suspend and resume.

Impure functions are marked with a ! at their definition and at call sites. Coroutines are similarly marked, with a ?. Pure functions have no mark.


A boolean expression (e.g. x > y) that happens to be true at a given point in a program. See the facts note for more details.


A unit of time. One flick (frame-tick) is 1 / 705_600_000 of a second.

Interval Arithmetic

Arithmetic on numerical ranges. See the interval arithmetic note for more details.

Modular Arithmetic

Arithmetic that wraps around at a certain modulus, such as 256 for the base.u8 type. For example, if x is a base.u8 with value 200, then (x + 70) has value 270 and would overflow, but (x ~mod+ 70) has value 14.

Operator Precedence

A ranking of arithmetic operators so that an expression like a + b * c is unambiguous (for the computer), equivalent to exactly one of (a + b) * c or, more conventionally, a + (b * c). While good for brevity, Wuffs does not have operator precedence: the bare a + b * c is an invalid Wuffs expression and the parentheses must be explicit. The ambiguity (for the human) can be a source of bugs in other security-concious file format parsers.

Some binary operators (+, *, &, |, ^, and, or) are also associative: (a + b) + c and a + (b + c) are equivalent, and can be written in Wuffs as a + b + c.

Refinement Type

A basic type further constrained to a subset of its natural range. For example, if x has type base.u8[0 ..= 99] then it is an unsigned 8-bit integer whose value must be less than 100. Without the refinement, x could be as high as 255.

base.u8[0 ..= 99] and base.u32[0 ..= 99] are two different types. They can have different run-time representations.

Non-nullable pointer types can be thought of as a refinement of regular pointer types, where the refined range excludes the nullptr value.

Saturating Arithmetic

Arithmetic that stops at certain bounds, such as 0 and 255 for the base.u8 type. For example, if x is a base.u8 with value 200, then (x + 70) has value 270 and would overflow, but (x ~sat+ 70) has value 255.


The set of facts at a given point in a program.