decreases via_fns are unusable

[jonhnet]

Let's make a little recursive spec fn to transform a map into a sequence of pairs:

struct Pair<K,V>{
    key: K, value: V
}

spec fn map_to_pair_seq<K,V>(m: Map<K,V>) -> (out: Seq<Pair<K, V>>)
{
    if m.len() == 0 {
        Seq::empty()
    } else {
        let key = choose |key| m.dom().contains(key);
        map_to_pair_seq(m.remove(key)).push(Pair{key, value: m[key]})
    }
}

Verus reasonably demands a decreases clause, so we add:

decreases m.dom().len()

Verus says "error: could not prove termination". From here, we can go in two directions.

First, we can try to guess how to prove termination. I happen to already know the set library bowels well enough to diagnose that I need trigger axiom_set_remove_len, so I try rewriting the if condition into a statement about m.dom().len().

That doesn't work, but I notice a hint that I haven't satisfied the recommends for choose, so I try rewriting the if condition to !exists.

That doesn't happen to work, either. I tried a few more variations on syntaxes hoping to trigger the axiom, such as rewriting the sub map to be a Map::new closure, but nothing happens to work, and there's no way to diagnose why I've missed the trigger.

So let's try the alternative direction: I try to follow the rather cryptic description of decreases. So I add a signature:

#[via_fn]
proof fn map_to_pair_seq_via<K,V>(m: Map<K,V>)
{
}

decreases m.dom().len() via map_to_pair_seq_via

Verus complains cannot infer type of the type parameter K``, so I change it:

decreases m.dom().len() via map_to_pair_seq_via<K,V>

And now the error is

error: expected curly braces
  --> test.rs:17:50
   |
17 | decreases m.dom().len() via map_to_pair_seq_via<K,V>
   |                                                  ^

This last problem is probably a fixable bug in the via parsing mechanism, and maybe we should fix that because, right now, this code isn't writable even with all the dark magical knowledge I already applied. However, the overall experience is completely inaccessible to a non-insider, and that's before we get to the weird way to actually express the proof inside the #[via_fn], which even I don't actually understand. It's some dark magic where the expressions in the proof fn get pasted inline into the spec fn.

It's worth contrasting this experience with the experience in Dafny: If you need a decreases clause, and it doesn't prove out of the box, you do what you'd do in any other proof text anywhere else in the language: you write asserts and call proof fns from the appropriate branches of the definition until the proof obligation is retired.

I'm not sure what technical challenges stand in the way of accomplishing a more usable approach. Perhaps spec fns with decreases declarations could be parsed in two passes: In one pass, the assert text stripped out, which is the mode we have today that gives the definition of the fn. In a second pass, the text is transformed into a proof fn; requires is inserted based on decreases when, assertions about the decreases clause are inserted at recursive invocations, and asserts and proof fn invocations are left in place to allow the user to explore and complete the proof.

[tjhance]

you need to use the turbofish syntax:

via map_to_pair_seq_via::<K, V>

[tjhance]

you might also find it useful to use m.dom().choose()

[jonhnet]

I very much appreciate the suggestions; they'll unblock my immediate need.

I think the discussion point still stands. "m.dom().choose()" is a dark magic trigger that's unguessable (even by an experienced user). The turbofish syntax will let me declare the via_fn, but the UI for via_fns -- in which you have to construct expressions and imagine how they'll get pasted into the VC -- is still very opaque. The documentation doesn't explain it, and I doubt even proper documentation would make it usable without expert guidance, much less diagnosable.

[parno]

I agree -- it seems like there are a couple of issues here. One is that the automation provided by vstd isn't yet on par with Dafny's proof automation; I don't think anyone has invested in working on it systematically to make examples like this go through (the way Rustan did with Dafny). The equivalent Dafny function goes through fully automatically:

datatype Pair<K, V> = Pair(key: K, value: V)

ghost function map_to_pair_seq<K, V>(m: map<K,V>) : seq<Pair<K,V>> {
    if |m| == 0 then
        []
    else
        var key :| key in m;
        map_to_pair_seq(map k | k in m && k != key :: m[k]) + [Pair(key, m[key])]
}

(and Dafny automatically infers the decreases clause of m; interestingly it fails to prove termination if you manually write |m| instead, so even Dafny has some work to do).

The second issue is that the current documentation of decreases ... via is very minimal. I needed to write a via proof recently, so I looked up the documentation and then gave up and looked through the examples and rust_verify_test directories to find an example instead.

The third issue is that writing a separate via function feels pretty kludgy. We'll likely have the same issue if/when we support ensures clauses for spec functions. I don't think it's impossible to explain, but it does lead to a lot of boilerplate. Writing a separate proof function means you end up writing:

1. A via proof_function_name line on the original spec function
2. A via_fn attribute on your proof function
3. A proof function signature that duplicates all of the arguments from the spec function
4. Replicating at least some of the control-flow of the spec function so that you can focus on the case(s) where you actually make a recursive call in the original spec function. If you make a mistake in this process, you will struggle to understand why your proof is failing to achieve your goal.

Jon offers one suggestion for achieving a more unified, Dafny-like experience, which would eliminate all of this boilerplate. A smaller step in that direction might be to change the syntax so that you can write via { body_of_proof_here}, which would at least eliminate items 2 and 3 above (plus the need to come up with a placeholder name in 1). It would still leave the annoyance of 4, which is probably the largest concern, unfortunately.

[jonhnet]

In the department of funny coincidences, once I was unblocked by Travis' reply, I chased the triggers down and ended up realizing I'd fallen into another finiteness trap (discussion #1512).

But yes, Bryan's breakdown of issues is valuable. Thanks to both of you.

[utaal]

Please note that we (primarily @Chris-Hawblitzel) have refactored VC gen towards allowing asserts in spec fn bodies exactly to address this issue (and spec ensures eventually). We have not pulled that thread through yet, but I'd look at that before making other stop-gap changes.

@jonhnet I suspect you'd be happy if you could just write the termination proof inline, correct?

[jonhnet]

That's fantastic news.

you'd be happy if you could just write the termination proof inline, correct?

Oh absolutely, that would far dominate the via_fn boilerplate and opaque copy-paste-expression semantics.

Hooray!