Function prepare_slice 

pub exec fn prepare_slice<Inner, T>(
    fmt: &Inner,
    values: &[T],
) -> checked : Result<usize, PreSerializeError>
where
    Inner: Prepare<T>,
    T: DeepView,

requires

fmt.exec_inv(),

ensures

checked matches Ok(
    len,
) ==> {
    &&& (super::Star(*fmt)).consistent(values.deep_view())
    &&& len == (super::Star(*fmt)).byte_len(values.deep_view())

},