pub trait ValueByteLen: SpecByteLen + Consistency<Val = Self::T> {
// Required methods
spec fn value_byte_len(v: Self::T) -> nat;
proof fn lemma_value_len_matches_byte_len(&self, v: Self::T);
}Expand description
Like SpecByteLen, but the byte length can be computed from the value alone, without needing to refer
to the combinator/format’s parameters or internal states (self).
Required Methods§
Sourcespec fn value_byte_len(v: Self::T) -> nat
spec fn value_byte_len(v: Self::T) -> nat
The byte length computed from the value alone.
Sourceproof fn lemma_value_len_matches_byte_len(&self, v: Self::T)
proof fn lemma_value_len_matches_byte_len(&self, v: Self::T)
requires
self.consistent(v),self.byte_len(v) == Self::value_byte_len(v),Bridge between the parameterized byte-length view and the value-based one.
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.