Replace height intrinsic with is_smaller_than and make height a partial order

[Chris-Hawblitzel]

This pull request allows decreases that go through Seq, Map, FnSpec, and user-defined abstract datatypes. For example:

        struct S {
            x: Seq<Box<S>>,
        }

        spec fn f(s: S) -> int
            decreases s
        {
            if s.x.len() > 0 {
                f(*s.x[0])
            } else {
                0
            }
        }

The new is_smaller_than(a, b) intrinsic expresses that b can decrease to a in a decreases clause:

#[verifier(external_body)]
#[verifier(broadcast_forall)]
pub proof fn axiom_seq_index_height<A>(s: Seq<A>, i: int)
    requires
        0 <= i < s.len(),
    ensures
        #[trigger] is_smaller_than(s[i], s),
{
}

is_smaller_than also works on lexicographic tuples, which can be useful for debugging termination failures:

assert(is_smaller_than((i, j - 1), (i, j)));

is_smaller_than replaces the previous height intrinsic. height is still used in the SMT encoding, but heights are no longer integers, and are instead Z3 partial orders. This allows the SMT encoding to express the heights of infinite maps and FnSpec functions.

Partial orders are a new feature in Z3, so this pull request requires upgrading to the latest Z3 release (4.12.2).

[tjhance]

I'm a little confused about how tuples work. Is the lexicographic ordering of tuples consistent with the height-ordering of tuples?

If I write is_smaller_than((a, b), (c, d)) then it looks like rust_to_vir_expr lexicographic ordering, but we can also talk about the partial-order on tuple objects themselves:

let x = (a, b);
let y = (c, d);
is_smaller_than(x, y)

Is this equivalent to is_smaller_than((a, b), (c, d))?

[tjhance]

this could use some documentation

[tjhance]

same - what's the u64 for?

[Chris-Hawblitzel]

I'm a little confused about how tuples work. Is the lexicographic ordering of tuples consistent with the height-ordering of tuples?

If I write is_smaller_than((a, b), (c, d)) then it looks like rust_to_vir_expr lexicographic ordering, but we can also talk about the partial-order on tuple objects themselves:

let x = (a, b);
let y = (c, d);
is_smaller_than(x, y)

Is this equivalent to is_smaller_than((a, b), (c, d))?

It's not equivalent. Maybe the larger question is what the syntax for is_smaller_than should be. Right now, the tuples are just a way to transport the various expressions through Rust's syntax and type checker. But we could have some dedicated syntax that doesn't overload tuples like this. I'm not convinced that is_smaller_than is important enough to deserve its own operator in the Verus syntax macro (along the lines of F*'s << operator). But would it be better to have an ordinary ! macro for it? Like is_smaller_than!(a, b; c, d) or is_smaller_than!(a, b => c, d) or decreases_to!(c, d => a, b)?

[tjhance]

Perhaps we should just have is_smaller_than and is_smaller_than_lexicographic (and the latter can just expect syntactic tuples)

[utaal]

FYI, I made this change to help smoothen the transition to z3 4.12.2 (and for future version updates): 6f5342c (adds a message that points the user to tools/get-z3.(ps1|sh)).

[utaal]

Can you please extract this conversion into a separate function?

[utaal]

Thank you! Having is_smaller_than(_lexicographic) will hopefully make debugging failing termination proof easier.

Looks good to me, modulo @tjhance's and my review comments.

[Chris-Hawblitzel]

I added a restriction similar to FStarLang/FStar#2954 . I think this should be ready to merge into main now.