Function serialize_slice 

pub exec fn serialize_slice<Output, Inner, T>(
    inner: &Inner,
    values: &[T],
    obuf: &mut Output,
)
where
    Output: OutputBuf,
    T: DeepView,
    Inner: Serializer<Output, T>,

requires

inner.exec_inv(),

(super::Star(*inner)).consistent(values.deep_view()),

old(obuf).fits((super::Star(*inner)).byte_len(values.deep_view())),

ensures

final(obuf)@ == old(obuf)@ + spec_serialize_seq(inner, values.deep_view()),

forall |n| {
    old(obuf).fits((super::Star(*inner)).byte_len(values.deep_view()) + n)
        <==> #[trigger] final(obuf).fits(n)
},

old(obuf).same_destination(final(obuf)),