Struct AndThen 

pub struct AndThen<A, B>(pub A, pub B);

Run a bytes combinator A and then re-interpret the entire bytes consumed/produced by A with another combinator B.

Consistency

A value of type B::Val is consistent w.r.t AndThen<A, B> iff there exists a value of type A::Val that is consistent w.r.t A and whose byte length equals the byte length of the B::Val value w.r.t B. Prefer ExactLen over AndThen to avoid the existential reasoning in the consistency condition.

Tuple Fields

0: A

1: B

Trait Implementations

impl<A, Then, ThenST> ByteLen<ThenST> for AndThen<A, Then>

where ThenST: DeepView + ?Sized, Then: ByteLen<ThenST>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<A: Clone, B: Clone> Clone for AndThen<A, B>

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

ensures

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

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

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

Performs copy-assignment from source.

impl<A, Then> Consistency for AndThen<A, Then>

where A: BytesCombinator + Consistency<Val = Seq<u8>>, Then: Consistency + SpecByteLen<T = Then::Val>,

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

{
    &&& self.1.consistent(v)
    &&& exists |chunk: Seq<u8>| {
        self.0.consistent(chunk) && self.0.byte_len(chunk) == self.1.byte_len(v)
    }

}

type Val = <Then as Consistency>::Val

The type of values whose consistency is being checked.

impl<A, Then> EquivSerializers for AndThen<A, Then>

where A: EquivSerializers<SVal = Seq<u8>, SValue = Seq<u8>>, Then: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{
    &&& self.0.equiv_inv()
    &&& self.1.equiv_inv()

}

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

impl<A, Then> EquivSerializersGeneral for AndThen<A, Then>

where A: EquivSerializersGeneral<SVal = Seq<u8>, SValue = Seq<u8>>, Then: EquivSerializers,

open spec fn equiv_general_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& self.1.equiv_inv()

}

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

impl<A, Then> GoodSerializer for AndThen<A, Then>

where A: BytesCombinator + GoodSerializer, Then: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{
    &&& self.0.serialize_inv()
    &&& self.1.serialize_inv()

}

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

impl<A, Then> MinMaxByteLen for AndThen<A, Then>

where A: BytesCombinator + Consistency<Val = Seq<u8>>, Then: MinMaxByteLen,

open spec fn min(&self) -> nat

{ self.1.min() }

open spec fn max(&self) -> nat

{ self.1.max() }

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

impl<A, Then> NoLookAhead for AndThen<A, Then>

where A: BytesCombinator + NoLookAhead<PVal = Seq<u8>>, Then: SafeParser,

open spec fn no_lookahead_inv(&self) -> bool

{ self.0.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<A, Then> NonMalleable for AndThen<A, Then>

where A: BytesCombinator + SoundParser + NonMalleable, Then: NonMalleable,

open spec fn nonmal_inv(&self) -> bool

{
    &&& self.0.nonmal_inv()
    &&& self.0.sound_inv()
    &&& self.1.nonmal_inv()
    &&& self.1.safe_inv()

}

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

impl<A, Then> NonTailFmt for AndThen<A, Then>

where A: BytesCombinator + NonTailFmt, Then: GoodSerializer + EquivSerializers,

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& self.1.serialize_inv()
    &&& self.1.equiv_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: InputBuf, A, Then> Parser<I> for AndThen<A, Then>

where A: Parser<I, PT = I, PVal = Seq<u8>>, Then: Parser<I>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.1.exec_inv()

}

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

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

Executable value returned by this parser.

impl<Then, T> Prepare<T> for AndThen<Tail, Then>

where T: DeepView + ?Sized, Then: Prepare<T>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<A, Then> Productive for AndThen<A, Then>

where A: BytesCombinator + Productive<PVal = Seq<u8>>, Then: SafeParser,

open spec fn productive_inv(&self) -> bool

{ self.0.productive_inv() }

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

impl<Then> SPRoundTripDps for AndThen<Tail, Then>

where Then: EquivSerializers + GoodSerializer + SPRoundTrip,

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<Len, Then> SPRoundTripDps for AndThen<Varied<Len>, Then>

where Then: 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<A, Then> SafeParser for AndThen<A, Then>

where A: BytesCombinator + SafeParser<PVal = Seq<u8>>, Then: SafeParser,

open spec fn safe_inv(&self) -> bool

{ self.0.safe_inv() }

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

impl<Output: OutputBuf, Then, T> Serializer<Output, T> for AndThen<Tail, Then>

where T: DeepView + ?Sized, Then: Serializer<Output, T>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<A, Then> SoundParser for AndThen<A, Then>

where A: BytesCombinator + SoundParser, Then: SoundParser,

open spec fn sound_inv(&self) -> bool

{ self.0.sound_inv() && 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<A, Then: SpecByteLen> SpecByteLen for AndThen<A, Then>

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

{ self.1.byte_len(v) }

type T = <Then as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<A, Then> SpecParser for AndThen<A, Then>

where A: SpecParser<PVal = Seq<u8>>, Then: SpecParser,

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

{
    match self.0.spec_parse(ibuf) {
        None => None,
        Some((len_a, chunk)) => {
            match self.1.spec_parse(chunk) {
                Some((len_b, v)) if len_a == len_b => Some((len_a, v)),
                _ => None,
            }
        }
    }
}

type PVal = <Then as SpecParser>::PVal

The type of parsed values.

impl<A, Then> SpecSerializer for AndThen<A, Then>

where A: SpecSerializer<SVal = Seq<u8>>, Then: SpecSerializer,

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

{
    let inner_bytes = self.1.spec_serialize(v);
    self.0.spec_serialize(inner_bytes)
}

type SVal = <Then as SpecSerializer>::SVal

The type of values to be serialized.

impl<A, Then> SpecSerializerDps for AndThen<A, Then>

where A: SpecSerializerDps<SValue = Seq<u8>>, Then: SpecSerializerDps,

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

{ self.0.spec_serialize_dps(self.1.spec_serialize_dps(v, seq![]), obuf) }

type SValue = <Then as SpecSerializerDps>::SValue

The type of values to be serialized.

impl<A, Then> ValueByteLen for AndThen<A, Then>

where A: BytesCombinator + Consistency<Val = Seq<u8>>, Then: ValueByteLen,

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

{ Then::value_byte_len(v) }

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

impl<A: Copy, B: Copy> Copy for AndThen<A, B>