Struct Bind 

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

Sequential composition of formats A and B, where B may depend on the value of A.

Parsing semantics: parses A to get a key, then parses B(key) to get the body value, and returns (key, value). During serialization, the caller must provide both the key and value.

Note on usage

Prefer super::Implicit when the key should be recovered from the body value instead of being carried explicitly through the value type.

Tuple Fields

0: A

1: B

Trait Implementations

impl<A, B, STA, STB> ByteLen<(STA, STB)> for Bind<A, B>

where STA: DeepView, STB: DeepView, A: ByteLen<STA>, B::O: ByteLen<STB>, B: MapRef<STA, Input = STA::V>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& forall |pb: B::O| #[trigger] pb.exec_inv()

}

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

impl<A: Clone, B: Clone> Clone for Bind<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, B> Consistency for Bind<A, B>

where A: Consistency, B: SpecMap<Input = A::Val>, B::Output: Consistency,

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

{
    let (key, val) = value;
    self.0.consistent(key) && self.1.spec_map(key).consistent(val)
}

type Val = (<A as Consistency>::Val, <<B as SpecMap>::Output as Consistency>::Val)

The type of values whose consistency is being checked.

impl<A, B> EquivSerializers for Bind<A, B>

where A: EquivSerializersGeneral, B: SpecMap<Input = A::SVal>, B::Output: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& forall |key: A::SVal| #[trigger] self.1.spec_map(key).equiv_inv()

}

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

impl<A, B> EquivSerializersGeneral for Bind<A, B>

where A: EquivSerializersGeneral, B: SpecMap<Input = A::SVal>, B::Output: EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& forall |key: A::SVal| #[trigger] self.1.spec_map(key).equiv_general_inv()

}

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

impl<A, B> GoodSerializer for Bind<A, B>

where A: GoodSerializer, B: SpecMap<Input = A::SVal>, B::Output: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{
    &&& self.0.serialize_inv()
    &&& forall |key: A::SVal| #[trigger] self.1.spec_map(key).serialize_inv()

}

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

impl<A, B> NoLookAhead for Bind<A, B>

where A: NoLookAhead, B: SpecMap<Input = A::PVal>, B::Output: NoLookAhead,

open spec fn no_lookahead_inv(&self) -> bool

{
    &&& self.0.no_lookahead_inv()
    &&& forall |key: A::PVal| #[trigger] self.1.spec_map(key).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, B> NonMalleable for Bind<A, B>

where A: NonMalleable, B: SpecMap<Input = A::PVal>, B::Output: NonMalleable,

open spec fn nonmal_inv(&self) -> bool

{
    &&& self.0.nonmal_inv()
    &&& self.0.safe_inv()
    &&& forall |key: A::PVal| #[trigger] self.1.spec_map(key).nonmal_inv()
    &&& forall |key: A::PVal| #[trigger] self.1.spec_map(key).safe_inv()

}

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

impl<A, B> NonTailFmt for Bind<A, B>

where A: NonTailFmt, B: SpecMap<Input = A::SValue>, B::Output: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& forall |key: A::SValue| #[trigger] self.1.spec_map(key).serialize_dps_inv()

}

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

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

impl<I, A, B> Parser<I> for Bind<A, B>

where I: InputBuf, A: Parser<I> + SafeParser, B::O: Parser<I> + SafeParser, B: MapRef<A::PT, Input = A::PVal>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.0.safe_inv()
    &&& forall |pb: B::O| #[trigger] pb.exec_inv() && pb.safe_inv()

}

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

type PT = (<A as Parser<I>>::PT, <<B as MapRef<<A as Parser<I>>::PT>>::O as Parser<I>>::PT)

Executable value returned by this parser.

impl<A, B, STA, STB> Prepare<(STA, STB)> for Bind<A, B>

where STA: DeepView, STB: DeepView, A: Prepare<STA>, B::O: Prepare<STB>, B: MapRef<STA, Input = STA::V>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& forall |pb: B::O| #[trigger] pb.exec_inv()

}

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

impl<A, B> Productive for Bind<A, B>

where A: Productive, B: SpecMap<Input = A::PVal>, B::Output: Productive,

open spec fn productive_inv(&self) -> bool

{
    ||| self.0.productive_inv()
    ||| forall |key: A::PVal| #[trigger] self.1.spec_map(key).productive_inv()

}

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

impl<A, B> SPRoundTripDps for Bind<A, B>

where A: SPRoundTripDps + NonTailFmt, B: SpecMap<Input = A::T>, B::Output: SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& self.0.unambiguous()
    &&& forall |key: A::T| #[trigger] self.1.spec_map(key).unambiguous()

}

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

impl<A, B> SafeParser for Bind<A, B>

where A: SafeParser, B: SpecMap<Input = A::PVal>, B::Output: SafeParser,

open spec fn safe_inv(&self) -> bool

{
    &&& self.0.safe_inv()
    &&& forall |key: A::PVal| #[trigger] self.1.spec_map(key).safe_inv()

}

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

impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (TA, TB)> for Bind<A, B>

where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B::O: Serializer<Output, TB>, B: MapRef<TA, Input = TA::V>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& forall |pb: B::O| #[trigger] pb.exec_inv()

}

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

impl<A, B> SoundParser for Bind<A, B>

where A: SoundParser, B: SpecMap<Input = A::PVal>, B::Output: SoundParser,

open spec fn sound_inv(&self) -> bool

{
    &&& self.0.sound_inv()
    &&& forall |key: A::PVal| #[trigger] self.1.spec_map(key).sound_inv()

}

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

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

impl<A, B> SpecByteLen for Bind<A, B>

where A: SpecByteLen, B: SpecMap<Input = A::T>, B::Output: SpecByteLen,

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

{
    let (key, val) = value;
    let next = self.1.spec_map(key);
    self.0.byte_len(key) + next.byte_len(val)
}

type T = (<A as SpecByteLen>::T, <<B as SpecMap>::Output as SpecByteLen>::T)

The type of values whose byte length is being computed.

impl<A, B> SpecParser for Bind<A, B>

where A: SpecParser, B: SpecMap<Input = A::PVal>, B::Output: SpecParser,

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

{
    match self.0.spec_parse(ibuf) {
        Some((n1, key)) => {
            let next = self.1.spec_map(key);
            match next.spec_parse(ibuf.skip(n1)) {
                Some((n2, val)) => Some((n1 + n2, (key, val))),
                None => None,
            }
        }
        None => None,
    }
}

type PVal = (<A as SpecParser>::PVal, <<B as SpecMap>::Output as SpecParser>::PVal)

The type of parsed values.

impl<A, B> SpecSerializer for Bind<A, B>

where A: SpecSerializer, B: SpecMap<Input = A::SVal>, B::Output: SpecSerializer,

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

{
    let (key, val) = v;
    let next = self.1.spec_map(key);
    self.0.spec_serialize(key) + next.spec_serialize(val)
}

type SVal = (<A as SpecSerializer>::SVal, <<B as SpecMap>::Output as SpecSerializer>::SVal)

The type of values to be serialized.

impl<A, B> SpecSerializerDps for Bind<A, B>

where A: SpecSerializerDps, B: SpecMap<Input = A::SValue>, B::Output: SpecSerializerDps,

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

{
    let (key, val) = value;
    let next = self.1.spec_map(key);
    self.0.spec_serialize_dps(key, next.spec_serialize_dps(val, obuf))
}

type SValue = (<A as SpecSerializerDps>::SValue, <<B as SpecMap>::Output as SpecSerializerDps>::SValue)

The type of values to be serialized.

impl<A, B> StaticByteLen for Bind<A, B>

where A: StaticByteLen, B: SpecMap<Input = A::T>, B::Output: StaticByteLen,

open spec fn static_byte_len() -> nat

{ A::static_byte_len() + <B::Output as StaticByteLen>::static_byte_len() }

proof fn lemma_static_len_matches_byte_len(&self, value: Self::T)

impl<A, B> ValueByteLen for Bind<A, B>

where A: ValueByteLen, B: SpecMap<Input = A::T>, B::Output: ValueByteLen,

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

{ A::value_byte_len(value.0) + <B::Output as ValueByteLen>::value_byte_len(value.1) }

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

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