Struct ExactLen 

pub struct ExactLen<Inner, Len = u8>(pub Len, pub Inner);

Wraps an inner combinator, constraining it to consume/produce exactly self.0 bytes.

Implemented as AndThen(Varied(self.0), self.1).

Consistency

A value of type Inner::Val is consistent w.r.t ExactLen iff it is consistent w.r.t Inner and its byte length given by Inner equals self.0.

Tuple Fields

0: Len

1: Inner

Implementations

impl<Inner: SpecByteLen, Len: AsLen> ExactLen<Inner, Len>

pub open spec fn byte_len(inner: Inner, v: <Self as SpecByteLen>::T) -> nat

{ inner.byte_len(v) }

Trait Implementations

impl<Len, Inner, InnerST> ByteLen<InnerST> for ExactLen<Inner, Len>

where Len: AsLen, InnerST: DeepView + ?Sized, Inner: ByteLen<InnerST>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

exec fn length(&self, v: &InnerST) -> len : usize

impl<Inner: Clone, Len: Clone> Clone for ExactLen<Inner, Len>

exec fn clone(&self) -> cloned : Self

ensures

call_ensures(Len::clone, (&self.0,), cloned.0),

call_ensures(Inner::clone, (&self.1,), cloned.1),

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<Inner: Consistency + SpecByteLen<T = Inner::Val>, Len: AsLen> Consistency for ExactLen<Inner, Len>

open spec fn consistent(&self, v: Self::Val) -> bool

{
    &&& self.1.consistent(v)
    &&& self.0.as_nat() == self.1.byte_len(v)

}

type Val = <Inner as Consistency>::Val

The type of values whose consistency is being checked.

impl<Inner: EquivSerializers, Len: AsLen> EquivSerializers for ExactLen<Inner, Len>

open spec fn equiv_inv(&self) -> bool

{ super::AndThen(super::Varied(self.0), self.1).equiv_inv() }

proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal)

impl<Inner: EquivSerializers, Len: AsLen> EquivSerializersGeneral for ExactLen<Inner, Len>

open spec fn equiv_general_inv(&self) -> bool

{ super::AndThen(super::Varied(self.0), self.1).equiv_general_inv() }

proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>)

impl<Inner: GoodSerializer, Len: AsLen> GoodSerializer for ExactLen<Inner, Len>

open spec fn serialize_inv(&self) -> bool

{ super::AndThen(super::Varied(self.0), self.1).serialize_inv() }

proof fn lemma_serialize_len(&self, v: Self::SVal)

impl<Inner, Len> MinMaxByteLen for ExactLen<Inner, Len>

where Inner: SpecByteLen + Consistency<Val = Inner::T>, Len: AsLen,

open spec fn min(&self) -> nat

{ self.0.as_nat() }

open spec fn max(&self) -> nat

{ self.0.as_nat() }

proof fn lemma_min_max_byte_len(&self, v: Self::T)

impl<Inner: SafeParser, Len: AsLen> NoLookAhead for ExactLen<Inner, Len>

open spec fn no_lookahead_inv(&self) -> bool

{ super::AndThen(super::Varied(self.0), self.1).no_lookahead_inv() }

proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)

fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)

impl<Inner: NonMalleable, Len: AsLen> NonMalleable for ExactLen<Inner, Len>

open spec fn nonmal_inv(&self) -> bool

{ super::AndThen(super::Varied(self.0), self.1).nonmal_inv() }

proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)

impl<Inner, Len> NonTailFmt for ExactLen<Inner, Len>

where Inner: GoodSerializer + EquivSerializers, Len: AsLen,

open spec fn serialize_dps_inv(&self) -> bool

{ super::AndThen(super::Varied(self.0), self.1).serialize_dps_inv() }

proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>)

impl<I, Len, Inner> Parser<I> for ExactLen<Inner, Len>

where I: InputBuf, Len: AsLen, Inner: Parser<I>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

exec fn parse(&self, ibuf: &I) -> PResult<Self::PT>

type PT = <Inner as Parser<I>>::PT

Executable value returned by this parser.

impl<Len, Inner, InnerST> Prepare<InnerST> for ExactLen<Inner, Len>

where Len: AsLen, InnerST: DeepView + ?Sized, Inner: Prepare<InnerST>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

exec fn prepare(&self, v: &InnerST) -> checked : Result<usize, PreSerializeError>

impl<Inner, Len> Productive for ExactLen<Inner, Len>

where Inner: SafeParser, Len: AsLen,

open spec fn productive_inv(&self) -> bool

{ super::AndThen(super::Varied(self.0), self.1).productive_inv() }

proof fn lemma_productive(&self, s: Seq<u8>)

impl<Inner, Len> SPRoundTripDps for ExactLen<Inner, Len>

where Inner: EquivSerializers + GoodSerializer + SPRoundTrip, Len: AsLen,

open spec fn unambiguous(&self) -> bool

{
    &&& self.1.serialize_inv()
    &&& self.1.equiv_inv()
    &&& self.1.sp_roundtrip_inv()

}

proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>)

impl<Inner: SafeParser, Len: AsLen> SafeParser for ExactLen<Inner, Len>

open spec fn safe_inv(&self) -> bool

{ super::AndThen(super::Varied(self.0), self.1).safe_inv() }

proof fn lemma_parse_safe(&self, ibuf: Seq<u8>)

impl<Output: OutputBuf, Len, Inner, T> Serializer<Output, T> for ExactLen<Inner, Len>

where Len: AsLen, T: DeepView + ?Sized, Inner: Serializer<Output, T> + SpecByteLen<T = T::V>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

exec fn serialize_into(&self, v: &T, obuf: &mut Output)

impl<Inner: SoundParser, Len: AsLen> SoundParser for ExactLen<Inner, Len>

open spec fn sound_inv(&self) -> bool

{ super::AndThen(super::Varied(self.0), self.1).sound_inv() }

proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>)

proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>)

impl<Inner: SpecByteLen, Len: AsLen> SpecByteLen for ExactLen<Inner, Len>

open spec fn byte_len(&self, v: Self::T) -> nat

{ super::AndThen(super::Varied(self.0), self.1).byte_len(v) }

type T = <Inner as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<Inner: SpecParser, Len: AsLen> SpecParser for ExactLen<Inner, Len>

open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)>

{ super::AndThen(super::Varied(self.0), self.1).spec_parse(ibuf) }

type PVal = <Inner as SpecParser>::PVal

The type of parsed values.

impl<Inner: SpecSerializer, Len: AsLen> SpecSerializer for ExactLen<Inner, Len>

open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8>

{ super::AndThen(super::Varied(self.0), self.1).spec_serialize(v) }

type SVal = <Inner as SpecSerializer>::SVal

The type of values to be serialized.

impl<Inner: SpecSerializerDps, Len: AsLen> SpecSerializerDps for ExactLen<Inner, Len>

open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8>

{ super::AndThen(super::Varied(self.0), self.1).spec_serialize_dps(v, obuf) }

type SValue = <Inner as SpecSerializerDps>::SValue

The type of values to be serialized.

impl<Inner: ValueByteLen, Len: AsLen> ValueByteLen for ExactLen<Inner, Len>

open spec fn value_byte_len(v: Self::T) -> nat

{ Inner::value_byte_len(v) }

proof fn lemma_value_len_matches_byte_len(&self, v: Self::T)

impl<Inner: Copy, Len: Copy> Copy for ExactLen<Inner, Len>