Fix: Parse slice range indexing (e.g. buffer[..n], buffer[..=n])

[Copilot]

verusfmt failed to parse range-indexed slices like &buffer[..n] because the PEG grammar had no expr_inner production for prefix range expressions (..n, .., ..=n). A secondary bug caused ..= to be tokenized as .. + = (formatted as x.. = y) due to wrong alternation ordering.

Changes

src/verus.pest

• Fix ..= operator ordering: swap (dot_dot_str | dot_dot_eq_str) → (dot_dot_eq_str | dot_dot_str) in expr_outer and expr_outer_no_struct so the longer token wins
• Add two silent rules range_expr_inner / range_expr_inner_no_struct to represent prefix range expressions; insert into expr_inner / expr_inner_no_struct
• Fix record_expr_field: change from attr* ~ (name ~ colon_str)? ~ expr to attr* ~ (name ~ colon_str ~ expr | !".." ~ expr) — prevents a leading-.. shorthand field from consuming the struct update base (..base), while still allowing named fields with range-to values (x: ..5)

src/lib.rs

• Add Rule::range_expr_inner / Rule::range_expr_inner_no_struct to the exhaustive match (silent rules never create Pair nodes at runtime, but Rust requires all Rule variants to be covered)

tests/verus-consistency.rs

• Add verus_range_index_expr covering [..n], [..], [..=n], [n..], [n..n]

verus! {
    fn slice_stuff(buffer: &[u8; 1024], n: usize) {
        foo(&buffer[..n]);   // previously: Failed to parse
        foo(&buffer[..]);
        foo(&buffer[..=n]);  // previously: formatted as `.. = n`
    }
}

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

[bsdinis]

@jaybosamiya-ms i tested this out and it does work. Thank you

[jaybosamiya]

The fix that the agent came up with is (at least at first glance) not the best, and might cause maintenance troubles in the future, so I'd like to write a cleaner one before merging; until then, if this is a blocker, as a workaround I think you can use let x = (..n); buffer[x] as a workaround in the code.