Lexicographic decreases clauses

For some recursive functions, it’s difficult to specify a single value that decreases in each recursive call. For example, the Ackermann function has two parameters m and n, and neither m nor n decrease in all 3 of the recursive calls:

spec fn ackermann(m: nat, n: nat) -> nat
    decreases m, n,
{
    if m == 0 {
        n + 1
    } else if n == 0 {
        ackermann((m - 1) as nat, 1)
    } else {
        ackermann((m - 1) as nat, ackermann(m, (n - 1) as nat))
    }
}

proof fn test_ackermann() {
    reveal_with_fuel(ackermann, 12);
    assert(ackermann(3, 2) == 29);
}

For this situation, Verus allows the decreases clause to contain multiple expressions, and it treats these expressions as lexicographically ordered. For example, decreases m, n means that one of the following must be true:

• m stays the same, and n decreases, which happens in the call ackermann(m, (n - 1) as nat)
• m decreases and n may increase or decrease arbitrarily, which happens in the two calls of the form ackermann((m - 1) as nat, ...)

Mutual recursion

Functions may be mutually recursive, as in the following example where is_even calls is_odd recursively and is_odd calls is_even recursively:

spec fn abs(i: int) -> int {
    if i < 0 {
        -i
    } else {
        i
    }
}

spec fn is_even(i: int) -> bool
    decreases abs(i),
{
    if i == 0 {
        true
    } else if i > 0 {
        is_odd(i - 1)
    } else {
        is_odd(i + 1)
    }
}

spec fn is_odd(i: int) -> bool
    decreases abs(i),
{
    if i == 0 {
        false
    } else if i > 0 {
        is_even(i - 1)
    } else {
        is_even(i + 1)
    }
}

proof fn even_odd_mod2(i: int)
    ensures
        is_even(i) <==> i % 2 == 0,
        is_odd(i) <==> i % 2 == 1,
    decreases abs(i),
{
    if i < 0 {
        even_odd_mod2(i + 1);
    }
    if i > 0 {
        even_odd_mod2(i - 1);
    }
}

fn test_even() {
    proof {
        reveal_with_fuel(is_even, 11);
    }
    assert(is_even(10));
}

fn test_odd() {
    proof {
        reveal_with_fuel(is_odd, 11);
    }
    assert(!is_odd(10));
}

The recursion here works for both positive and negative i; in both cases, the recursion decreases abs(i), the absolute value of i.

An alternate way to write this mutual recursion is:

spec fn is_even(i: int) -> bool
    decreases abs(i), 0int,
{
    if i == 0 {
        true
    } else if i > 0 {
        is_odd(i - 1)
    } else {
        is_odd(i + 1)
    }
}

spec fn is_odd(i: int) -> bool
    decreases abs(i), 1int,
{
    !is_even(i)
}

proof fn even_odd_mod2(i: int)
    ensures
        is_even(i) <==> i % 2 == 0,
        is_odd(i) <==> i % 2 == 1,
    decreases abs(i),
{
    reveal_with_fuel(is_odd, 2);
    if i < 0 {
        even_odd_mod2(i + 1);
    }
    if i > 0 {
        even_odd_mod2(i - 1);
    }
}

fn test_even() {
    proof {
        reveal_with_fuel(is_even, 21);
    }
    assert(is_even(10));
}

fn test_odd() {
    proof {
        reveal_with_fuel(is_odd, 22);
    }
    assert(!is_odd(10));
}

In this alternate version, the recursive call !is_even(i) doesn’t decrease abs(i), so we can’t just use abs(i) as the decreases clause by itself. However, we can employ a trick with lexicographic ordering. If we write decreases abs(i), 1, then the call to !is_even(i) keeps the first expression abs(i) the same, but decreases the second expression from 1 to 0, which satisfies the lexicographic requirements for decreasing. The call is_odd(i - 1) also obeys lexicographic ordering, since it decreases the first expression abs(i), which allows the second expression to increase from 0 to 1.