Function length_slice 

pub exec fn length_slice<Inner, T>(fmt: &Inner, values: &[T]) -> len : usize
where
    Inner: ByteLen<T>,
    T: DeepView,

requires

fmt.exec_inv(),

(super::Star(*fmt)).byte_len(values.deep_view()) <= usize::MAX,

ensures

len == (super::Star(*fmt)).byte_len(values.deep_view()),