Imprecise trigger report for requires clause #695

jaybosamiya · 2023-07-20T19:32:17Z

Consider the following:

use vstd::prelude::*;

verus! {

exec fn foo(f: impl FnOnce(u32) -> u32) -> (r: u32)
  requires forall |x| f.requires((x,))
{
   f(5)
}

}

fn main() {}

Running Verus on this prints the warning:

$ verus a.rs
note: verifying root module

note: automatically chose triggers for this expression:
 --> a.rs:6:12
  |
6 |   requires forall |x| f.requires((x,))
  |            ^^^^^^

note:   trigger 1 of 1:
 --> a.rs:6:34
  |
6 |   requires forall |x| f.requires((x,))
  |                                  ^^^^

note: Verus printed one or more automatically chosen quantifier triggers
      because it had low confidence in the chosen triggers.
      To suppress these messages, do one of the following:
        (1) manually annotate a single desired trigger using #[trigger]
            (example: forall|i: int, j: int| f(i) && #[trigger] g(i) && #[trigger] h(j)),
        (2) manually annotate multiple desired triggers using #![trigger ...]
            (example: forall|i: int| #![trigger f(i)] #![trigger g(i)] f(i) && g(i)),
        (3) accept the automatically chosen trigger using #![auto]
            (example: forall|i: int, j: int| #![auto] f(i) && g(i) && h(j))
        (4) use the --triggers-silent command-line option to suppress all printing of triggers.
      (Note: triggers are used by the underlying SMT theorem prover to instantiate quantifiers;
      the theorem prover instantiates a quantifier whenever some expression matches the
      pattern specified by one of the quantifier's triggers.)
 --> a.rs:6:12
  |
6 |   requires forall |x| f.requires((x,))
  |            ^^^^^^

verification results:: verified: 2 errors: 0

Notice that running Verus appears to have chosen (x,) as a trigger, but this is not a valid point to annotate as a #[trigger] (and trying to manually put that as a trigger point won't work). Indeed, looking at the smt2 file (after #![auto] to silence the warning), Verus has chosen f.requires((x,) as the full trigger, rather than (x,) as it claims.

Also, this f.requires((x,)) is the only valid point that a trigger can be placed for this expression. In fact, Verus is even kinda aware of this, since it doesn't report a warning if you instead have this (notice rather than (x,), it is just x):

exec fn foo(f: impl FnOnce(u32) -> u32) -> (r: u32)
  requires forall |x| f.requires(x)
  ensures f.ensures((5,), r)
{
   f(5)
}

This succeeds without any warning:

$ verus a.rs
note: verifying root module

verification results:: verified: 2 errors: 0

If we ask if for triggers, it even prints the right thing:

$ verus a.rs --triggers
note: verifying root module

note: automatically chose triggers for this expression:
 --> a.rs:6:12
  |
6 |   requires forall |x| f.requires(x)
  |            ^^^^^^

note:   trigger 1 of 1:
 --> a.rs:6:23
  |
6 |   requires forall |x| f.requires(x)
  |                       ^^^^^^^^^^^^^

verification results:: verified: 2 errors: 0

Tested on:

Verus
  Version: 0.2023.07.20.2dc6a17
  Profile: release
  Platform: macos_aarch64
  Toolchain: 1.68.0-aarch64-apple-darwin

The text was updated successfully, but these errors were encountered:

JoPolzin linked a pull request Jun 28, 2024 that will close this issue

remove tuples from the pool of potential auto triggers #1199

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Imprecise trigger report for requires clause #695

Imprecise trigger report for requires clause #695

jaybosamiya commented Jul 20, 2023

Imprecise trigger report for requires clause #695

Imprecise trigger report for requires clause #695

Comments

jaybosamiya commented Jul 20, 2023