Support for Pattern Matching in Closure Parameters

[FanelliMarco]

Description:
Currently, Verus does not support pattern matching in closure parameters. When attempting to use pattern matching, such as destructuring a tuple in the parameter list, Verus throws an error:

error: The verifier does not yet support the following Rust feature: only variables are supported here, not general patterns
  --> .\rust_verify\example\guide\test_verus.rs:10:28
   |
10 |         .try_fold((0, 0), |(sum, count), val| {
   |                            ^^^^^^^^^^^^

This limitation restricts the use of idiomatic Rust patterns in Verus-verified code, making it harder to write expressive and readable functional code.

Proposed Solution:
Extend Verus to support pattern matching in closure parameters, particularly for tuple destructuring. This would allow expressions like the following to be verified successfully:

.try_fold((0, 0), |(sum, count), val| {
    val.to_digit(10)
        .map(|num| if count % 2 == 1 { num * 2 } else { num })
        .map(|num| if num > 9 { num - 9 } else { num })
        .map(|num| (num + sum, count + 1))
})

Impact:

• Improves ergonomics and readability of Verus-verified Rust code.
• Reduces the need for workaround solutions, such as manually unpacking tuples inside the closure body.
• Aligns Verus more closely with idiomatic Rust practices.

Additional Context:

• Rust version: 1.85.1
• Verus version: 0.2025.03.24.cee0e29
• Platform: Windows (x86_64-pc-windows-msvc)

[utaal]

Thank you for the feature request. We generally keep track of these (as they may require design) as discussions. I'll move it there.

[wood-ghost]

Hi, has there been any progress on pattern matching in closure parameters since this discussion started?