pub trait MinMaxByteLen: SpecByteLen + Consistency<Val = Self::T> {
// Required methods
spec fn min(&self) -> nat;
spec fn max(&self) -> nat;
proof fn lemma_min_max_byte_len(&self, v: Self::T);
}Expand description
Denotes the min/max byte length of a value w.r.t. a combinator’s format spec.
Combinators that do not implement MinMaxByteLen
- Unbounded Sequence/Tail Combinators:
Tail(consumes the remaining buffer)Star<A>(zero or more repetitions)Repeat<A, B>(zero or moreAs followed by terminatorB)RepeatTillEnd<A>(sugar forRepeat<A, Eof>)
- Dependent and Recursive Combinators:
Bind<A, B>(the suffix parserBis constructed dynamically from the parsed value ofA)Implicit<Head, Tail>(similar toBind)FixWith<LIMIT, Body, Param>(recursive fixpoint)
Required Methods§
Sourceproof fn lemma_min_max_byte_len(&self, v: Self::T)
proof fn lemma_min_max_byte_len(&self, v: Self::T)
requires
self.consistent(v),self.min() <= self.byte_len(v) <= self.max(),