Address misleading diagnostics in --expand-errors

[utaal]

@jonhnet encountered an --expand-errors diagnostic that pointed to a forall inside a predicate that was assumed to be true.
Here 2023-08-24-09-02-04.zip is the captured error message.

My diagnosis is that this is due to the forall not being provable after --expand-errors split the predicates.
A simplified model of the behavior follows (though this is not exactly faithful, as I forced the split assertion failure with a false predicate):

        use vstd::prelude::*;
        spec fn no(i: int) -> bool {
            false
        }

        spec fn seq_bounded_by_length(s1: Seq<int>) -> bool {
            (forall|i:int| (0 <= i && i < s1.len()) ==> no(i) && (0 <= #[trigger] s1[i] < s1.len()))
        }

        spec fn long_seq(s1: Seq<int>) -> bool {
            s1.len() > 20 // EXPAND-ERRORS
        }

        spec fn seq_is_long_and_bounded_by_length(s1: Seq<int>) -> bool {
            &&& seq_bounded_by_length(s1)
            &&& long_seq(s1) // EXPAND-ERRORS
        }

        proof fn test_expansion_forall()
        {
            let mut ss = Seq::empty();
            ss = ss.push(0);
            ss = ss.push(10);
            assume(seq_bounded_by_length(ss));
            assert(seq_is_long_and_bounded_by_length(ss));  // EXPAND-ERRORS
        }

This results in:

note: split assertion failure
  --> /Users/andreal1/Src/verus/source/target/debug/test_inputs/expand_errors-894260d23f9c5763-test10_expand_forall_assume/test.rs:12:5
   |
12 |     false
   |     ^^^^^
...
16 |     (forall|i:int| (0 <= i && i < s1.len()) ==> no(i) && (0 <= #[trigger] s1[i] < s1.len()))
   |                                                 ----- from this function call
...
24 |     &&& seq_bounded_by_length(s1)
   |         ------------------------- from this function call
...
34 |     assert(seq_is_long_and_bounded_by_length(ss));  // EXPAND-ERRORS
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ from this function call

note: split assertion failure
  --> /Users/andreal1/Src/verus/source/target/debug/test_inputs/expand_errors-894260d23f9c5763-test10_expand_forall_assume/test.rs:20:5
   |
20 |     s1.len() > 20 // EXPAND-ERRORS
   |     ^^^^^^^^^^^^^
...
25 |     &&& long_seq(s1) // EXPAND-ERRORS
   |         ------------ from this function call
...
34 |     assert(seq_is_long_and_bounded_by_length(ss));  // EXPAND-ERRORS
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ from this function call

which is misleading for the user. While the no(i) is indeed not provable, we have assumed seq_bounded_by_length(ss) to be true, which is a typical proof debugging technique, and the failure in the forall is irrelevant for the user at this point.

Note that in this small example I had to write a false predicate to reproduce the error, but in a more complex situation the forall may not be directly provable and may require some manual proof (that a user isn't going to necessarily need for the final proof text).

I propose that we disable splitting the foralls to avoid these situations, and increase the likelihood that the expanded error is not misleading to the user. @jonhnet reports that he has never encountered a misleading expanded error report in dafny, and he values this property.

There is an alternative, I believe: we may be able to collect all the predicates involved in a split and add them as disjunction to the split atoms. This way if any of the split predicates is known to be true, we would not report an error for any of its (recursive) conjuncts / foralls. I don't have the bandwidth to try this right now, but it's worth considering (@chanheec may be interested).

[utaal]

@tjhance suggests:

I think one way to fix this would be to expand one level at a time? e.g.,

• expand seq_is_long_and_bounded_by_length to seq_bounded_by_length(s1) && long_seq(s1)
• observe the first one works, so don't bother expanding it any further
• observe that long_seq(s1) fails, so expand it

@utaal thinks that should work, but believe it will require inspecting the query results to decide what/when to report (instead of emitting all of the messages generated by the expand errors queries as notes, which is what we do now)

[tjhance]

As discussed on slack, this problem isn't restricted just to expanding quantifier expressions:

e.g., if d(a) expands to f(a) && m(a)
and f(a) expands to g(a) && h(a)
If you need f(a) to trigger some forall, but split-errors expands it to
g(a) && h(a) && m(a) then f gets skipped

[utaal]

The current workaround, taking into consideration @tjhance's scenario, is to only expand through one function call or one quantifier. We can remove this restriction when we can expand one layer at a time.

[utaal-b]

Consider adding support to unfold the definition of a lambda: this would be useful for lifted encodings, like the temporal logic for https://github.com/vmware-research/verifiable-controllers

[parno]

@tjhance Has your recent revamp of the expand-errors feature addressed this?

[utaal]

@tjhance bump

[tjhance]

right now we get:

error: assertion failed
  --> texp.rs:39:20
   |
39 |             assert(seq_is_long_and_bounded_by_length(ss));  // EXPAND-ERRORS
   |                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ assertion failed

note: diagnostics via expansion
  --> texp.rs:30:17
   |
30 |             &&& long_seq(s1) // EXPAND-ERRORS
   |                 ^^^^^^^^^^^^

note: seq_is_long_and_bounded_by_length(ss)
|   seq_bounded_by_length(ss) ✔
|   long_seq(ss) ✘
|   |   ss.len() > 20 
|   +---
+---

so I would say yes it's fixed