Build fails with `!is` token in spec/proof mode.

[achreto]

Building using cargo build fails related to !is syntax in spec/proof mode.

Verus
  Version: 0.2025.04.03.0f22710
  Profile: release
  Platform: linux_x86_64
  Toolchain: 1.82.0-x86_64-unknown-linux-gnu

Minimal example:

enum Test {
    A,
    B,
    C
}

spec fn is_not_a(t: Test) -> bool {
    t !is A
}

spec fn is_a(t: Test) -> bool {
    t is A
}

output:

error: expected delimiter
   --> src/lib.rs:104:11
    |
104 |     t !is A
    |           ^

[matthias-brun]

The error message indicates a parsing error consistent with the exclamation mark being parsed individually rather than as part of !is. I suspect this happens because the parsing for !is/!has relies on rejoin_tokens in source/builtin_macros/src/syntax.rs and presumably that logic is only used in the verification, while compilation only uses the syn_verus parsing directly. The same parsing error occurs in verus-find, which uses syn_verus.

According to the comments in the code, rejoin_tokens is necessary to correctly parse ==>, &&&, and ||| so this would also mean that external tools that rely on syn_verus currently don't obtain the same AST as Verus does. (Although I wasn't actually able to reproduce that.) Maybe we can move rejoin_tokens into syn_verus?

@Chris-Hawblitzel Do you have thoughts on what the best way to resolve this is?

[rikosellic]

Just a reminder: rejoin_tokens has already been moved into verus_syn. I'm not familiar with Cargo, so maybe someone else could take a look.

Btw, shall we call rejoin_tokens internally within verus_syn APIs, rather than explicitly call it every time we write an external tool?

[matthias-brun]

Yes, to fix the build issue, I think we do need to call it as part of the macro itself, as cargo build doesn't invoke Verus except for the syntax macro. Actually, I'm realizing that the build issue is independent of what you're suggesting. I'm not sure if we can fully take care of the rejoining inside syn_verus but it would certainly be preferable.