Add support for binding sub-arrays using slice patterns

[zhassan-aws]

Requested feature: Add full support for Rust slice patterns. Currently, only binding sub-slices is supported (see #357). Binding sub-arrays panics.
Use case: Slice patterns
Link to relevant documentation (Rust reference, Nomicon, RFC): https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
Is this a breaking change? No

Test case:

let [x, y @ .., z] = [1, 2, 3, 4]; // `y: [i32, 2] = [2, 3]

[zhassan-aws]

We currently don't handle the head/tail pattern fully. Add an appropriate error message and add to the limitations section of the docs, then we can remove the "MLP - Must Have" and change it from a bug to a feature.

[zhassan-aws]

With #1066, this no longer crashes, and instead we codegen assert/assume false that will cause verification to fail if the array subslice pattern is reachable. Removing the "MLP - Must Have" label.

[matthiaskrgr]

fn array() -> [(String, String); 3] {
    Default::default()
}

#[kani::proof]
fn move_out_by_const_subslice_and_index_field() {
    let a = array();
    let [_, _y @ ..] = a;
    let [(ref _x, _), _, _] = a;
}

#[kani::proof]
fn move_out_by_const_subslice_and_end_index_field() {
    let a = array();
    let [_y @ .., _] = a;
    let [.., (ref _x, _)] = a;
}

// Slice + Slice
#[kani::proof]
fn move_out_by_subslice_and_subslice() {
    let a = array();
    let [x @ .., _, _] = a;
    let [_, ref _y @ ..] = a;
}

with mir-opt-level=3: Failed Checks: Sub-array binding is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/707