Invariants

invariant clauses attach facts to loops. A loop invariant must hold before the first iteration and after each loop back-edge.

Syntax

func:count_down = int32(int32:x)
    requires x >= 0i32
{
    while (x > 0i32) invariant x >= 0i32 {
        x -= 1i32;
    }
    pass(x);
};

Multiple invariant expressions are comma-separated:

while (i < n) invariant i >= 0i32, sum >= 0i32 {
    sum += i;
    i += 1i32;
}

Entry and back-edge obligations

The compiler checks two points:

Entry: the invariant must hold before the first possible iteration.
Back-edge: after the loop body executes and control jumps back to the condition, the invariant must still hold.

v0.34.4 added Z3 entry obligations and --debug-contracts runtime entry/back-edge checks.

Runtime checking under debug contracts

When a fact is runtime-dependent and --debug-contracts is enabled, the compiler keeps a runtime guard. A failing runtime invariant follows the normal Result/failsafe path used by contract checks in that build mode.

Example from the v0.34.4 regression shape:

func:bad_entry = int32() {
    int32:i = 0i32;
    while (i < 1i32) invariant i == 1i32 {
        i += 1i32;
    }
    pass(i);
};

The invariant is false at entry, so the debug runtime check catches it before the body can repair it.

Purity rules

Invariant clauses must be boolean and solver-friendly. v0.34.4 locks two clear front-end diagnostics:

ARIA-071 / ARIA-INVARIANT-NON-BOOL for non-boolean invariant expressions.
ARIA-072 / ARIA-INVARIANT-IMPURE for calls or recursive expressions inside invariant clauses.

Practical pattern

Start with facts that are already visible at loop entry:

func:sum_to_n = int32(int32:n)
    requires n >= 0i32
{
    int32:i = 0i32;
    int32:sum = 0i32;

    while (i < n) invariant i >= 0i32, sum >= 0i32 {
        sum += i;
        i += 1i32;
    }

    pass(sum);
};