support pattern matching in closure parameters

[wood-ghost]

Follow discussion #1540

The PR supports pattern matching in closure parameters, including reference, tuple, struct, and tuple-struct patterns (all covered by regression tests).

• Create pattern_stmts to store destructuring declarations
• Add closure_pat_to_mut_var
  • Preserve the existing path for simple bindings pat_to_mut_var
  • Create a hidden parameter and add its destructuring declaration to pattern_stmts.
• Modify PatKind::Ref branch in pattern_to_vir_unadjusted to handle ordinary reference patterns, respecting rustc’s skipped_ref_pats and continuing to reject pinned reference patterns.
• Wrap each requires and ensures expression, and the closure body, with the generated destructuring declarations so pattern-bound variables are available in each scope.

The implementation preserves VIR’s existing representation of closure parameters as individual variables, along with the original argument types and closure arity.

Assisted-by: GPT-5.6 Sol, GPT-6 Astra

_{By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.}

[tjhance]

Thanks for working on this!

It looks like there are some problems if the pattern contains any ref mut bindings (vir::ast::MutRef). For one thing, you won't be able to lower such patterns in spec code (as you'd need to for the requires and ensures). For another, it needs support in the rustc_mir_build fork.

Specifically, if I try:

fn test() {
    let y = |(x, y): &mut (u64, u64)| {
    };
}

I get a error: Verus Internal Error: setup_verus_ctxt_for_thir_erasure failed, var lookup failed.

IMO, you should just disable this case for now, i.e., check if there are any ByRef::Mut in the Pattern and if so, return a 'not supported' error.

[wood-ghost]

Thanks for working on this!

It looks like there are some problems if the pattern contains any ref mut bindings (vir::ast::MutRef). For one thing, you won't be able to lower such patterns in spec code (as you'd need to for the requires and ensures). For another, it needs support in the rustc_mir_build fork.

Specifically, if I try:

fn test() {
    let y = |(x, y): &mut (u64, u64)| {
    };
}

I get a error: Verus Internal Error: setup_verus_ctxt_for_thir_erasure failed, var lookup failed.

IMO, you should just disable this case for now, i.e., check if there are any ByRef::Mut in the Pattern and if so, return a 'not supported' error.

Thank you so much for the review! Hope that everything is fixed now. I'll be more considerable next time :)

[tjhance]

OK, I pulled your commit to experiment locally and see what's going on with the span ids. I think I found the circumstances that led you add this line, but it's a real mess.

First of all, you shouldn't need to add any mapping ids for "adjusted patterns". This isn't the case for any other patterns (in match expressions or let decls) so it shouldn't be the case here.

The reason it seems like you do is that there are duplicate AstIds. The init expression had the same ID as the pattern, causing the two nodes to get confused.

You need to use spanned_typed_new to get a fresh ID:

-    let init = SpannedTyped::new(&pattern.span, typ, PlaceX::Local(name.clone()));
+    let init = bctx.spanned_typed_new(pat.span, typ, PlaceX::Local(name.clone()));

In rust_to_vir, always use the spanned_typed_new function.

Okay, now there's still the issue that erase.rs expects the id_to_hir mapping to have an entry for every Local node, including the one in your init expression. This is kind of a problem, because there's no HirId that corresponds to this node. IMO, hir_vir_ids really ought to take an Option for this situation, though you could also use a junk HirId (like the HirId of the closure) which will cause it to be ignored later. This is kind of jank, though, and obfuscates the purpose of the mapping.

I think if you make these fixes, everything should be working again. However, there are still a couple of other things I'm worried about:

• pattern_stmts gets cloned (for the requires and ensures), which duplicates the pattern IDs. This seems to work correctly now, but I think this should be fixed. It could result in the modes getting mixed up.
  • Unfortunately, I don't think we have a good function for "clone a node and create fresh ids". There is a similar function, cleanup_span_ids, but it doesn't support patterns.
• There's another SpannedTyped::new when you create the ExprX::Block, which should again be spanned_typed_new.

[wood-ghost]

Thank you for the review! I’ll address the remaining issues as follows:

• Merge the latest main into my working branch.
• Represent generated nodes explicitly
  • Change hir_vir_ids to Vec<(Option<HirId>, AstId)>, using None for generated VIR nodes with no corresponding Rust HIR node
  • Update erasure setup to handle these entries while retaining errors for genuinely missing mappings
• Give the hidden-parameter initializer a fresh ID and register it with None
• Give contract copies independent IDs
  • Support Pattern as fp in source/vir/src/ast_visitor.rs
  • Register the generated contract copies with None so their mode information does not affect erasure of the executable source bindings
  • Use fresh IDs for the generated block expressions
• Testing

[tjhance]

This only applies to statements, but not expressions or patterns. (I'm confused how the temporary test passes, since the test seems to be checking the pattern IDs.)

[wood-ghost]

This only applies to statements, but not expressions or patterns. (I'm confused how the temporary test passes, since the test seems to be checking the pattern IDs.)

Thanks for the comment! I think map_stmt_spans only uses a statement as the entry point and it recursively maps its child nodes. It takes a statement and a span-transforming closure, f_span, which handles new ID here.
The call chain in source/vir/src/ast_visitor.rs is shown below and expressions or patterns are visited.

map_stmt_spans
    ->map_stmt_visitor_env
        -> visit_stmt
            -> visit_stmt_rec
                -> visit_pattern / visit_place / visit_expr

FP is added to MapExprStmtTypVisitor following other type like FE. Its visit_pattern first calls visit_pattern_rec to process nested patterns, then applies fp to the resulting pattern. In map_stmt_spans, the fp closure calls f_span on the pattern’s span, so each visited pattern receives a fresh ID. The expression and place callbacks apply f_span similarly.
That's why I think it passes the test checking pattern IDs.

[wood-ghost]

I'm not sure where to put this helper function. I put it here just because I want to call it conveniently :-(

[wood-ghost]

This only applies to statements, but not expressions or patterns. (I'm confused how the temporary test passes, since the test seems to be checking the pattern IDs.)

Thanks for the comment! I think map_stmt_spans only uses a statement as the entry point and it recursively maps its child nodes. It takes a statement and a span-transforming closure, f_span, which handles new ID here.
The call chain in source/vir/src/ast_visitor.rs is shown below and expressions or patterns are visited.

map_stmt_spans
    ->map_stmt_visitor_env
        -> visit_stmt
            -> visit_stmt_rec
                -> visit_pattern / visit_place / visit_expr

FP is added to MapExprStmtTypVisitor following other type like FE. Its visit_pattern first calls visit_pattern_rec to process nested patterns, then applies fp to the resulting pattern. In map_stmt_spans, the fp closure calls f_span on the pattern’s span, so each visited pattern receives a fresh ID. The expression and place callbacks apply f_span similarly.
That's why I think it passes the test checking pattern IDs.

[tjhance]

Thanks for working on this, and for dealing with the id madness!