pub trait BytesCombinator: SpecByteLen<T = Seq<u8>> {
// Required method
proof fn lemma_byte_len_is_buf_len(&self, buf: Seq<u8>);
}Expand description
Marker for combinators whose corresponding values are raw bytes (Seq<u8>).
Required Methods§
Sourceproof fn lemma_byte_len_is_buf_len(&self, buf: Seq<u8>)
proof fn lemma_byte_len_is_buf_len(&self, buf: Seq<u8>)
ensures
self.byte_len(buf) == buf.len(),Byte length equals buffer length.