pub struct Repeat<C>(pub C);Expand description
A combinator to repeatedly parse/serialize the inner combinator C until the end of the buffer.
If the inner combinator fails before the end of the buffer, Repeat fails
Tuple Fields§
§0: CImplementations§
Trait Implementations§
Source§impl<'x, I, O, C> Combinator<'x, I, O> for Repeat<C>where
I: VestInput,
O: VestOutput<I>,
C: Combinator<'x, I, O, SType = &'x <C as Combinator<'x, I, O>>::Type>,
C::V: SecureSpecCombinator<Type = <C::Type as View>::V>,
<C as Combinator<'x, I, O>>::Type: 'x,
impl<'x, I, O, C> Combinator<'x, I, O> for Repeat<C>where
I: VestInput,
O: VestOutput<I>,
C: Combinator<'x, I, O, SType = &'x <C as Combinator<'x, I, O>>::Type>,
C::V: SecureSpecCombinator<Type = <C::Type as View>::V>,
<C as Combinator<'x, I, O>>::Type: 'x,
Source§open spec fn ex_requires(&self) -> bool
open spec fn ex_requires(&self) -> bool
{ self.0.ex_requires() }Source§exec fn serialize(
&self,
vs: Self::SType,
data: &mut O,
pos: usize,
) -> res : Result<usize, SerializeError>
exec fn serialize( &self, vs: Self::SType, data: &mut O, pos: usize, ) -> res : Result<usize, SerializeError>
Source§type Type = RepeatResult<<C as Combinator<'x, I, O>>::Type>
type Type = RepeatResult<<C as Combinator<'x, I, O>>::Type>
The result type of parsing
Source§type SType = &'x RepeatResult<<C as Combinator<'x, I, O>>::Type>
type SType = &'x RepeatResult<<C as Combinator<'x, I, O>>::Type>
The input type of serialization, often a reference to
Self::Type.
For “structural” formats though (e.g., crate::regular::sequence::Pair and crate::regular::variant::Choice),
this is the tuple/sum of the corresponding Combinator::SType types.Source§impl<C: SecureSpecCombinator> SecureSpecCombinator for Repeat<C>
impl<C: SecureSpecCombinator> SecureSpecCombinator for Repeat<C>
Source§open spec fn is_prefix_secure() -> bool
open spec fn is_prefix_secure() -> bool
{ false }Source§open spec fn is_productive(&self) -> bool
open spec fn is_productive(&self) -> bool
{ false }Source§proof fn theorem_serialize_parse_roundtrip(&self, vs: Self::Type)
proof fn theorem_serialize_parse_roundtrip(&self, vs: Self::Type)
Source§proof fn theorem_parse_serialize_roundtrip(&self, input: Seq<u8>)
proof fn theorem_parse_serialize_roundtrip(&self, input: Seq<u8>)
Source§proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
Source§proof fn lemma_parse_length(&self, s: Seq<u8>)
proof fn lemma_parse_length(&self, s: Seq<u8>)
Source§proof fn lemma_parse_productive(&self, s: Seq<u8>)
proof fn lemma_parse_productive(&self, s: Seq<u8>)
Source§fn corollary_parse_surjective(&self, v: Self::Type)
fn corollary_parse_surjective(&self, v: Self::Type)
Source§fn corollary_serialize_injective_contraposition(
&self,
v1: Self::Type,
v2: Self::Type,
)
fn corollary_serialize_injective_contraposition( &self, v1: Self::Type, v2: Self::Type, )
Source§fn lemma_serialize_productive(&self, v: Self::Type)
fn lemma_serialize_productive(&self, v: Self::Type)
Source§impl<C: SecureSpecCombinator> SpecCombinator for Repeat<C>
impl<C: SecureSpecCombinator> SpecCombinator for Repeat<C>
Source§open spec fn requires(&self) -> bool
open spec fn requires(&self) -> bool
{
&&& self.0.requires()
&&& C::is_prefix_secure()
&&& self.0.is_productive()
}Source§open spec fn wf(&self, vs: Self::Type) -> bool
open spec fn wf(&self, vs: Self::Type) -> bool
{ forall |i: int| 0 <= i < vs.len() ==> #[trigger] self.0.wf(vs[i]) }Source§open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>
{
if s.len() == 0 {
Some((0, seq![]))
} else {
match self.0.spec_parse(s) {
Some((n, v)) => {
if 0 < n <= s.len() {
match self.spec_parse(s.skip(n)) {
Some((_, vs)) => Some((s.len() as int, seq![v] + vs)),
None => None,
}
} else {
None
}
}
None => None,
}
}
}Source§open spec fn spec_serialize(&self, vs: Self::Type) -> Seq<u8>
open spec fn spec_serialize(&self, vs: Self::Type) -> Seq<u8>
{ RepeatN(self.0, vs.len() as usize).spec_serialize(vs) }Source§type Type = Seq<<C as SpecCombinator>::Type>
type Type = Seq<<C as SpecCombinator>::Type>
The view of [
Combinator::Result].Auto Trait Implementations§
impl<C> Freeze for Repeat<C>where
C: Freeze,
impl<C> RefUnwindSafe for Repeat<C>where
C: RefUnwindSafe,
impl<C> Send for Repeat<C>where
C: Send,
impl<C> Sync for Repeat<C>where
C: Sync,
impl<C> Unpin for Repeat<C>where
C: Unpin,
impl<C> UnwindSafe for Repeat<C>where
C: UnwindSafe,
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
§impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: From<T>,
impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: From<T>,
fn obeys_from_spec() -> bool
fn from_spec(v: T) -> VERUS_SPEC__A
§impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: Into<T>,
impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__Awhere
VERUS_SPEC__A: Into<T>,
fn obeys_into_spec() -> bool
fn into_spec(self) -> T
§impl<T, U> IntoSpecImpl<U> for Twhere
U: From<T>,
impl<T, U> IntoSpecImpl<U> for Twhere
U: From<T>,
fn obeys_into_spec() -> bool
fn into_spec(self) -> U
Source§impl<T, U> SpecTryInto<U> for Twhere
U: SpecTryFrom<T>,
impl<T, U> SpecTryInto<U> for Twhere
U: SpecTryFrom<T>,
Source§open spec fn spec_try_into(self) -> Result<U, <U as SpecTryFrom<T>>::Error>
open spec fn spec_try_into(self) -> Result<U, <U as SpecTryFrom<T>>::Error>
{ U::spec_try_from(self) }Source§type Error = <U as SpecTryFrom<T>>::Error
type Error = <U as SpecTryFrom<T>>::Error
The type returned in the event of a conversion error.