Function vstd::bytes::lemma_auto_spec_u16_to_from_le_bytes

source · 
pub proof fn lemma_auto_spec_u16_to_from_le_bytes()
Expand description
ensures
forall |x: u16| {
    &&& #[trigger] spec_u16_to_le_bytes(x).len() == 2
    &&& spec_u16_from_le_bytes(spec_u16_to_le_bytes(x)) == x

},
forall |s: Seq<u8>| {
    s.len() == 2 ==> #[trigger] spec_u16_to_le_bytes(spec_u16_from_le_bytes(s)) == s
},