Chained conjunction forces spec mode

[jonhnet]

Run this with verus:

use builtin_macros::verus;

verus!{
    exec fn foo(a: usize, b: usize, c: usize) -> usize {
        if a <= b <= c { 1 } else { 2 }
    }
}

You'll get error: condition must have mode exec, which is quite confusing.

A workaround is to replace the condition with a <= b && b <= c, so evidently operator chaining causes the expression to suddenly become a spec expression.

Is there any reason we shouldn't allow chained expressions in exec text and desugar them to a collection of conjuncts?

[tjhance]

Definitely a confusing error message that should be fixed.

I'm not really sure about supporting chained inequalities in exec code though. I think generally it's a good idea to leave exec code as 'normal rust' as much as possible.

[jonhnet]

I think generally it's a good idea to leave exec code as 'normal rust' as much as possible.

While I acknowledge your point, I'd like to also remind us that verus! is a language design problem (opportunity!), and we should be willing to design the language. Chained inequalities don't have a special meaning in spec land, so it's weird that they shouldn't work in either context. I can't see an upside to excluding them other than "now you can't copy-paste exec code into a non-verus! context and have it work without editing", but I'm not very excited about retaining that property at the expense of making the verus! language less usable.

[jaybosamiya]

Given that Rust hasn't had chained comparison in a while (relevant thread that started in 2017: rust-lang/rfcs#2083), and our semantics of chained comparison (e.g., a < b < c == a < b && b < c) seems to be the only possibly reasonable one, and that rustc currently complains with the correct fix on chained comparisons (example below), overall I think us supporting exec-mode chained comparisons would not be too bad.

((Click here for current rustc error message))

$ rustc x.rs
error: comparison operators cannot be chained
 --> x.rs:2:8
  |
2 |   if 1 < 2 < 3 {
  |        ^   ^
  |
help: split the comparison into two
  |
2 |   if 1 < 2 && 2 < 3 {
  |            ++++

error: aborting due to 1 previous error

Important things to keep in mind (esp in exec-mode), if we decide to include this:

• Range::contains exists which solves a lot of common chained-comparison cases, such as (0..n).contains(i) --- imho, this is fairly readable (for saying 0 <= i < n), and also depending on who you ask, might seem more "obviously" correct, without worrying about off-by-ones due to </<= (otoh, we're verifying things, so if we OBO'd, the verifier should likely catch it safely, so maybe less of a concern in a verification language). The particular case in the original message in this thread would use RangeInclusive instead: a <= b <= c == (a..=c).contains(b).
• Side effects (for a < b < c)
  • Double-triggering due to b having side-effects: naïvely rewriting like the above (a < b && b < c) works fine in spec mode where we don't need to worry about side-effects, but in exec-mode, we'd need to ensure that any intermediate is not triggered twice.
  • Short-circuiting because a and c might have side-effects too: we need to make a decision (due to short-circuiting) as to which side effects apply if (say) a < b fails --- does c's side-effect execute in such a case? Personally, I think the easiest to understand behavior is that of no short-circuiting in the middle of a a < b < c chain---specifically, I argue that the expansion should be into three let-bindings into temporaries before doing the comparisons.