Assertions are statements that introduce new compile-time facts. They are not comments, as removing them can prevent the code from compiling, but unlike other programming languages, Wuffs' assertions have no run-time effect at all, not even in a “debug, not release” configuration. Compiling an assert will fail unless it can be proven.
The basic form is assert some_boolean_expression, which creates some_boolean_expression as a fact. That expression must be free of side-effects: any function calls within must be pure.
Arithmetic inside assertions is performed in ideal integer math, working in the integer ring ℤ. An expression like x + y in an assertion never overflows, even if x and y have a realized (non-ideal) integer type like u32.
Some assertions can be proven by the compiler with no further guidance. For example, if x == 1 is already a fact, then x < 5 can be automatically proved. Adding a seemingly redundant fact can be useful when reconciling multiple arms of an if-else chain, as reconciliation requires the facts in each arm's final situation to match exactly:
if x < 5 {
// No further action is required. "x < 5" is a fact in the 'if' arm.
} else {
x = 1
// At this point, "x == 1" is a fact, but "x < 5" is not.
// This assertion creates the "x < 5" fact.
assert x < 5
}
// Here, "x < 5" is still a fact, since the exact boolean expression "x < 5"
// was a fact at the end of every arm of the if-else chain.
TODO: specify what can be proved automatically, without naming an axiom.
Wuffs' assertion system is a proof checker, not an SMT solver or automated theorem prover. It verifies explicit proof targets instead of the more open-ended task of searching for implicit ones. This involves more explicit work by the programmer, but compile times matter, so the Wuffs compiler is fast (and dumb) instead of smart (and slow).
The Wuffs syntax is regular (and unlike C++, does not require a symbol table to parse), so it should be straightforward to transform Wuffs code to and from file formats used by more sophisticated proof engines. Nonetheless, that is out of scope of this respository and the Wuffs compiler per se.
Again for compilation speed, not every inference rule is applied after every line of code. Some assertions require explicit guidance, naming the rule that proves the assertion. These names are simply strings that resemble mathematical statements. They are axiomatic, in that these rules are assumed, not proved, by the Wuffs toolchain. They are typically at a higher level than e.g. Peano axioms, as Wuffs emphasizes practicality over theoretical minimalism. As they are axiomatic, they endeavour to only encode ‘obvious’ mathematical rules.
For example, the axiom named "a < b: a < c; c <= b" is about transitivity: the assertion a < b is proved if both a < c and c <= b are true, for some (pure) expression c. Terms like a, b and c here are all integers in ℤ, they do not encompass floating point concepts like negative zero, NaNs or rounding. The axiom is invoked by extending an assert with the via keyword:
assert n_bits < 12 via "a < b: a < c; c <= b"(c: width)
This proves n_bits < 12 by applying that transitivity axiom, where a is n_bits, b is 12 and c is width. Compiling this assertion requires proving both n_bits < width and width <= 12, from existing facts or from the type system, e.g. width is a base.u32[..= 12].
The trailing (c: width) syntax is deliberately similar to a function call (recall that when calling a Wuffs function, each argument must be named), but the "a < b: a < c; c <= b" named axiom is not a function-typed expression.
The compiler's built-in axioms are listed separately.