`#[verus_spec]` errors when trailing comma is added in `with` clause.

[hiroki-chen]

The following code does not parse:

#[verus_spec(res =>
    with
        Tracked(bar): Tracked<&mut ()>,
    requires
        true,
    ensures
        true,
)]
fn foo() {}

This generates

error: expected `:`
   |
11 |         true,
   |         ^^^^

I mentioned this in #1916 but think another separate issue might be clearer for tracking. It'd be more ergonomic to allow trailing commas though (e.g. for code refactoring, proof-reading.).

[Marsman1996]

This problem is caused by the parser logic here:

verus/dependencies/syn/src/verus.rs

Lines 2441 to 2474 in f592032

	impl parse::Parse for WithSpecOnFn {
	fn parse(input: ParseStream) -> Result<Self> {
	let with = input.parse()?;
	let mut inputs = Punctuated::new();
	while !input.peek(Token![->]) {
	let expr = input.parse()?;
	inputs.push(expr);
	if !input.peek(Token![,]) {
	break;
	}
	let _comma: Token![,] = input.parse()?;
	}
	let outputs = if input.peek(Token![->]) {
	let token = input.parse()?;
	let mut outs = Punctuated::new();
	loop {
	let expr = input.parse()?;
	outs.push(expr);
	if !input.peek(Token![,]) {
	break;
	}
	let _comma: Token![,] = input.parse()?;
	}
	Some((token, outs))
	} else {
	None
	};
	Ok(WithSpecOnFn {
	with,
	inputs,
	outputs,
	})
	}
	}

Not sure if this is by design or an unintended bug.

[hiroki-chen]

If requires and ensures all allow trailing commas then with should be consistent as we may have multiple tracked or ghost variables and it's quite natural to write a trailing comma after the last parameter imo.

[Marsman1996]

#1939 should fix this, you can test it.