Verus misreports an automatically selected trigger within a macro

[matthias-brun]

It's possible that this bug is specific to bitvector reasoning. I didn't try to reproduce with different queries.

use vstd::prelude::*;

verus!{

fn main() { }

macro_rules! bitmask_inc {
    ($low:expr,$high:expr) => {
        (!(!0u64 << (($high+1u64)-$low))) << $low
    }
}

macro_rules! bit {
    ($v:expr) => {
        1u64 << $v
    }
}

proof fn foo(a: u64, b: u64) {
    assume(a & !bitmask_inc!(9u64,11u64) == b & !bitmask_inc!(9u64,11u64));
    assert(forall|i:u64| 11u64 < i < 64u64 ==> a & (1u64 << i) == b & bit!(i)) by (bit_vector)
        requires a & !bitmask_inc!(9u64,11u64) == b & !bitmask_inc!(9u64,11u64);
    assert(forall|i:u64| 11u64 < i < 64u64 ==> a & bit!(i) == b & bit!(i)) by (bit_vector)
        requires a & !bitmask_inc!(9u64,11u64) == b & !bitmask_inc!(9u64,11u64);
}

}

The two bitvector queries are identical except that I inlined the bit! macro in the first one. Verus prints a note about the triggers that are chosen automatically. For both queries 1u64 << i is chosen as the trigger (I checked the air file) but for the query using the bit! macro the chosen trigger is incorrectly reported as just 1u64:

note: automatically chose triggers for this expression:
  --> /st/verus/test.rs:21:12
   |
21 |     assert(forall|i:u64| 11u64 < i < 64u64 ==> a & (1u64 << i) == b & bit!(i)) by (bit_vector)
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

note:   trigger 1 of 1:
  --> /st/verus/test.rs:21:52
   |
21 |     assert(forall|i:u64| 11u64 < i < 64u64 ==> a & (1u64 << i) == b & bit!(i)) by (bit_vector)
   |                                                    ^^^^^^^^^^^

note: automatically chose triggers for this expression:
  --> /st/verus/test.rs:23:12
   |
23 |     assert(forall|i:u64| 11u64 < i < 64u64 ==> a & bit!(i) == b & bit!(i)) by (bit_vector)
   |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

note:   trigger 1 of 1:
  --> /st/verus/test.rs:15:9
   |
15 |         1u64 << $v
   |         ^^^^
...
23 |     assert(forall|i:u64| 11u64 < i < 64u64 ==> a & bit!(i) == b & bit!(i)) by (bit_vector)
   |                                                    ------- in this macro invocation
   |
   = note: this note originates in the macro `bit` (in Nightly builds, run with -Z macro-backtrace for more info)

[...]