Recommends checking for get_* from #[is_variant] (report warnings when calling get_X_0() without is_X())

[marshtompsxd]

We are using #[is_variant] a lot and often need to write

&&& x.is_X()
&&& x.get_X_0() === yyy

It would be great if Verus can report warnings when we call get_X_0() without ensuring is_X() before that.

[tchajed]

Here's a concrete example where recommends checking isn't solving this problem (does get_X_0() even have a recommends?):

#![allow(unused_imports)]
use builtin::*;
use builtin_macros::*;

verus! {

  #[is_variant]
  enum Foo {
    A(u64),
    B(bool),
  }

  spec fn user_get_A(f: Foo) -> u64
    recommends f.is_A()
  {
    f.get_A_0()
  }

  fn take_a(f: Foo) -> u64
    requires user_get_A(f) == 3
  {
    3
  }

  fn example() {
    let f = Foo::B(false);
    // GOOD: note that recommendation not met
    assert(user_get_A(f) == 3);
    // BAD: nothing about recommendation
    assert(f.get_A_0() == 3);
    // BAD: nothing about recommendation
    take_a(f);
  }

  fn main(){}
}

[utaal]

I don't think we're checking recommends on get_* from #[is_variant] and I agree we probably should. I'll turn this into a discussion where we track feature requests/discussions.

[tchajed]

Thanks for creating the discussion! For this issue though, independently of get_* in the above code take_a(f) doesn't trigger a recommends check on user_get_A(f), even though its recommends is false.

[utaal]

Aha! Now that I've read it more carefully, I see what you're getting at: calling an exec/proof function with a requires that calls a function that carries a recommends doesn't recommend-check that requires; in this case where the recommends is is_A.
We don't perform that recommends check if the requires isn't satisfied at the caller; that recommendation failure would appear if you had a verification failure in the body of take_a:

  fn take_a(f: Foo) -> u64
    requires user_get_A(f) == 3
  {
    assert(false);
    3
  }

This would likely crop up while trying to prove a postcondition for take_a.
Right now I cannot think of a case where checking the recommends of an expression in the requires that fails at the caller would particularly help for functions that are not #[verifier(external_body)] (as it would likely be caught when working on the body of the callee), but I could be convinced otherwise.
To be specific, I think here take_a should have requires f.is_A() && user_get_A(f) == 3, which would be necessary to use the value of f in the body of take_a.

[tjhance]

as it would likely be caught when working on the body of the callee

I'm not sure about this. Is the lemma verifies successfully, the recommends-checking won't be run when proving the body the callee. But a lemma might verify even while its requires might have recommends-checks that would fail.

[utaal]

True, but the user would notice when inspecting the precondition for the failing lemma/function. It may be worth doing this check anyway, but there may be a tradeoff in terms of not doing checks that would not be helpful, not sure.
If we did the check, would we do it when the caller precondition fails? Or would we want something like a requires(checked) that checks recommends on the precondition as part of checking the function definition?

[matthias-brun]

To be specific, I think here take_a should have requires f.is_A() && user_get_A(f) == 3, which would be necessary to use the value of f in the body of take_a.

I don't think that's true. The precondition user_get_A(f) == 3 may be sufficient even for more complex functions/lemmas. E.g. I think I've written some bitvector and/or nonlinear assertions with preconditions like that, deliberately omitting the is_X. (Although that kind of usage indicates that the lemma/assertion could be more general and prove things about 3 directly.)

I think just adding recommends checking for the generated get_A functions might be sufficient. In the take_A example, one would have to explicitly assert the precondition to get the failing recommends check but I think that's preferable to running precondition recommends checks by default. The recommends failures can already cause quite a bit of noise and I suspect that recommends checks on function preconditions are less likely to be helpful than on assertions. Perhaps that's not true, though?