decreases_to!

The expression decreases_to!(e1, e2, …, en => f1, f2, …, fn) is a bool indicating if the left-hand sequence e1, e2, …, en lexicographically-decreases-to the right-hand sequence f1, f2, …, fn

The lexicographic-decreases-to is used to check the decreases measure for spec functions.

See this tutorial chapter for an introductory discussion of lexicographic-decreases.

Definition

We say that e1, e2, …, en lexicographically-decreases-to f1, f2, …, fn if there exists a k where 1 <= k <= n such that:

• ek decreases-to fk.
• For each i where 1 <= i < k, ei == fi.

The decreases-to relation is a partial order on all values; values of different types are comparable. The relation permits, but is not necessarily limited to:

• If x and y are integers, where x > y >= 0, then x decreases-to y.
• If a is a datatype (struct, tuple, or enum) and f is one of its “potentially recursive” fields, then a decreases-to a.f.
  • For a datatype X, a field is considered “potentially recursive” if it either mentions X or a generic type parameter of X.
• If f is a spec_fn, then f decreases-to f(i).
• If s is a Seq, then s decreases-to s[i].
• If s is a Seq, then s decreases-to s.subrange(i, j) if the given range is strictly smaller than 0 .. s.len().
  • axiom_seq_len_decreases provides a more general axiom; it must be invoked explicitly.
• If v is a Vec, then v decreases-to v@.

These axioms are triggered when the relevant expression (e.g., x.f, x->f, s[i], v@) is used as part of a decreases-to expression.

Notes

1. Tuples are not compared lexicographically; tuples are datatypes, which are compared as explained above, e.g., a decreases_to a.0. Only the “top level” sequences in a decreases_to! expression are compared lexicographically.

2. Sequences are not compared on len() alone. However, you can always use s.len() as a decreases-measure instead of s.

Examples

proof fn example_decreases_to(s: Seq<int>)
    requires s.len() == 5
{
    assert(decreases_to!(8int => 4int));

    // fails: can't decrease to negative number
    // assert(decreases_to!(8 => -2));

    // Comma-separated elements are treated lexicographically:
    assert(decreases_to!(12int, 8int, 1int => 12int, 4int, 50000int));

    // Datatypes decrease-to their fields:
    let x = Some(8int);
    assert(decreases_to!(x => x->0));

    let y = (true, false);
    assert(decreases_to!(y => y.0));

    // fails: tuples are not treated lexicographically
    // assert(decreases_to!((20, 9) => (11, 15)));

    // sequence decreases-to an element of the sequence
    assert(decreases_to!(s => s[2]));

    // sequence decreases-to a subrange of the sequence
    assert(decreases_to!(s => s.subrange(1, 3)));
}