Facts are boolean expressions, such as x < (y + z), that are guaranteed to be true at a given point in a program‘s execution (or, informally, at a given line of code). They might not be true at other points, as Wuffs is an imperative language and its variables can change values (but not change types) over a program’s lifetime.
Types (and their refinements) express static constraints (on variables, struct fields and function arguments). Facts express dynamic constraints. They come and go as a program proceeds.
Another difference is that facts can capture the relationships between variables. For example, i < s.length() might be a fact involving the two variables i and s, and therefore s[i] is a valid (in-bounds) index expression (assuming that we also know that 0 <= i, e.g. because i is unsigned). Other programming languages use the type system to express these sorts of concepts, but Wuffs does not have dependent types.
Interval arithmetic and the type system provide much of Wuffs' compile-time bounds checking, but facts are also used to prove bounds checks that the type system alone cannot. For example, a variable x might generally have values in the range [0 ..= 255], but in a specific block of code, x might be temporarily restricted to the range [30 ..= 40] and therefore an expression like a[x - 25] is guaranteed in-bounds when a is an array of length 16.
Guarding against nullptr dereferences is another case of bounds checking. nptr T is the “pointer to T” type that allows nullptr values. The Wuffs compiler will reject any method call on a variable (or function argument) with that type, without the fact that it is not actually a nullptr:
pub func foo.bar!(ic: nptr base.image_config) {
etc
// Cannot call args.ic.set!(etc) here, since the type system doesn't
// rule out args.ic being nullptr.
etc
if args.ic <> nullptr {
// We now know, as a fact, that "args.ic <> nullptr", so that calling a
// method on it is valid. Wuffs spells not-equals as "<>".
args.ic.set!(etc)
}
etc
}
Every fact is true (at its point in the program), but not every truth is a fact. For example, if x < 5 is true then x < 6, x < 7, x < 8, etc are an infinite sequence of truths, but the Wuffs tools only track a finite number of facts at any given point. Some facts are explicitly created and some facts are implicitly created. But all facts are created by specific means.
One way to implicitly create a fact is by assignment. Immediately after the statement a = rhs, the boolean expression a == rhs is a true fact, provided that rhs is an expression with no side effects. That assignment also either removes or updates any other fact involving a.
TODO: specify exactly when and how facts are removed or updated.
As alluded to above, another way to implicitly create a fact is to explicitly check if it is true, using an if or while statement:
// "x < (y + z)" isn't necessarily true here...
if x < (y + z) {
// ...but in here, "x < (y + z)" is a true fact.
w = 3
// It remains so after an assignment to an unrelated variable.
y = 4
// But "x < (y + z)" is no longer necessarily true after one or more of
// that boolean expression's variables (in this case, y) might have
// changed. Still, at this point in the program, the set of facts include
// "w == 3" and "y == 4".
etc
} else {
// At the top of the else branch, and any subsequent branch in the same
// if-else chain, the inverted expression "x >= (y + z)" is a true fact.
etc
}
Facts are also explicitly created by compile-time assertions, discussed in a separate document.
The situation is defined as the set of facts at a given point in a program. Multiple situations have to be reconciled when there are multiple paths to a line of code:
break, continue or return statement) are not considered during reconciliation.continues inside that loop, and the implicit continue at the closing } curly brace.break or if the while condition fails.Reconciliation is simply set intersection: a boolean expression is guaranteed to be true (i.e. it is a fact) at a point in the program only if it is true for every possible code execution path to that point.
Loops are cyclical: the situation at the bottom of the loop depends on the situation at the top of the loop, but the situation at the top depends on the bottom (because of the implicit continue at the bottom). Instead of relying on an SMT solver or automated theorem prover (whose exact behavior is hard to specify, or even reliably reproduce if it can be configured with a timeout) to infer a solution to this self-referential problem, Wuffs simply requires the programmer to write exactly what the situation is, before and after the loop:
while n_bits < n_extra_bits,
inv i < 320,
inv rep_count <= 11,
post n_bits >= n_extra_bits,
{
etc // Loop body.
}
The pre, post and inv keywords introduce loop pre-conditions, post-conditions and invariants (things that are both). The snippet above means that the Wuffs compiler has to verify all three conditions at every place this loop exits: at the implicit break if the expression n_bits < n_extra_bits evaluates to false (which in this case trivially proves the third condition), but also at every explicit break for that loop within its body.
Similarly, it has to verify only the first two conditions at every place this loop repeats (at its initial execution, at every explicit continue and at the loop bottom), before the n_bits < n_extra_bits condition is checked.
As a consequence of explicitly listing those two invariants (which are also pre-condtions), the situation at the top of the loop body (immediately after the { curly brace) is precisely those first two conditions, plus the n_bits < n_extra_bits fact from the while condition evaluation. For example, if the loop body never modifies the i local variable, it is trivial to preserve the fact that i < 320 throughout the loop body but specifically at every exit point, and therefore maintain the invariant.
Note that invariants don't have to hold at every point within the loop, only at every jump for that loop. Such facts can be temporarily lost and later re-established within that loop body, provided that no break or continue for that loop comes in between.
The discussion above focuses on while loops, but also apply to the less common iterate loops.
During development, writing down what part of the situation a programmer needs to preserve across a while loop obviously requires knowing what the situation is. In the future, a Wuffs-aware IDE could provide that information. Until then, inserting an assert false line into a Wuffs program will fail to compile, as the compiler can obviously not prove that false is true, and the compilation error message should include a situation listing.