Struct Preceded 

pub struct Preceded<A, AVal, B, const CHECK: bool = false> {
    pub a: A,
    pub b: B,
    pub a_val: AVal,
}

Parsing semantics: like (A, B), but discards the value parsed by A and returns only the value parsed by B.

Serialization semantics: reuses a_val as the serialized witness for A, then serializes B.

When CHECK is false, parsing is malleable in the discarded prefix unless A admits a unique consistent value. When CHECK is true, parsing additionally checks that the parsed prefix equals a_val.

Fields

a: A

b: B

a_val: AVal

Trait Implementations

impl<A, AVal, B, BVal, const CHECK: bool> ByteLen<BVal> for Preceded<A, AVal, B, CHECK>

where AVal: DeepView<V = AVal>, BVal: DeepView, A: ByteLen<AVal>, B: ByteLen<BVal>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.a.exec_inv()
    &&& self.b.exec_inv()
    &&& forall |v: AVal| v.deep_view() == v

}

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

impl<A: Clone, AVal: Clone, B: Clone, const CHECK: bool> Clone for Preceded<A, AVal, B, CHECK>

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

ensures

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

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

call_ensures(AVal::clone, (&self.a_val,), cloned.a_val),

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

Performs copy-assignment from source.

impl<A, B, const CHECK: bool> Consistency for Preceded<A, A::Val, B, CHECK>

where A: Consistency, B: Consistency,

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

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.consistent(v)
}

type Val = <B as Consistency>::Val

The type of values whose consistency is being checked.

impl<A, B, const CHECK: bool> EquivSerializers for Preceded<A, A::SValue, B, CHECK>

where A: EquivSerializersGeneral + Consistency<Val = A::SVal>, B: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.equiv_inv()
}

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

impl<A, B, const CHECK: bool> EquivSerializersGeneral for Preceded<A, A::SValue, B, CHECK>

where A: EquivSerializersGeneral + Consistency<Val = A::SVal>, B: EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.equiv_general_inv()
}

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

impl<A, B, const CHECK: bool> GoodSerializer for Preceded<A, A::SVal, B, CHECK>

where A: GoodSerializer, B: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.serialize_inv()
}

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

impl<A, B, const CHECK: bool> MinMaxByteLen for Preceded<A, A::T, B, CHECK>

where A: MinMaxByteLen, B: MinMaxByteLen,

open spec fn min(&self) -> nat

{ preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val).min() }

open spec fn max(&self) -> nat

{ preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val).max() }

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

impl<A, B, const CHECK: bool> NoLookAhead for Preceded<A, A::PVal, B, CHECK>

where A: NoLookAhead, B: NoLookAhead,

open spec fn no_lookahead_inv(&self) -> bool

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.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 Preceded<A, A::PVal, B, false>

where A: SoundParser + NonMalleable + AdmitsUniqueVal, B: SoundParser + NonMalleable,

open spec fn nonmal_inv(&self) -> bool

{
    &&& Pair(self.a, self.b).sound_inv()
    &&& Pair(self.a, self.b).nonmal_inv()

}

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

impl<A, B> NonMalleable for Preceded<A, A::PVal, B, true>

where A: SoundParser + NonMalleable, B: SoundParser + NonMalleable,

open spec fn nonmal_inv(&self) -> bool

{
    &&& Pair(self.a, self.b).sound_inv()
    &&& Pair(self.a, self.b).nonmal_inv()

}

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

impl<A, B, const CHECK: bool> NonTailFmt for Preceded<A, A::SValue, B, CHECK>

where A: NonTailFmt, B: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.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, A, AVal, B> Parser<I> for Preceded<A, AVal, B, false>

where I: InputBuf, A: Parser<I, PT = AVal> + SafeParser<PVal = AVal>, B: Parser<I> + SafeParser, AVal: DeepView<V = AVal>,

open spec fn exec_inv(&self) -> bool

{ Pair(&self.a, &self.b).exec_inv() }

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

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

Executable value returned by this parser.

impl<I, A, AVal, B> Parser<I> for Preceded<A, AVal, B, true>

where I: InputBuf, A: Parser<I, PT = AVal> + SafeParser<PVal = AVal>, B: Parser<I> + SafeParser, AVal: DeepView<V = AVal> + PartialEq + Structural,

open spec fn exec_inv(&self) -> bool

{
    &&& Pair(&self.a, &self.b).exec_inv()
    &&& forall |v: AVal| v.deep_view() == v

}

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

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

Executable value returned by this parser.

impl<A, AVal, B, BVal, const CHECK: bool> Prepare<BVal> for Preceded<A, AVal, B, CHECK>

where AVal: DeepView<V = AVal>, BVal: DeepView, A: Prepare<AVal>, B: Prepare<BVal>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.a.exec_inv()
    &&& self.b.exec_inv()
    &&& forall |v: AVal| v.deep_view() == v

}

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

impl<A, B> Productive for Preceded<A, A::PVal, B, false>

where A: Productive, B: Productive,

open spec fn productive_inv(&self) -> bool

{ preceded::<_, _, _, _, false>(self.a, self.b, self.a_val).productive_inv() }

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

impl<A, B> Productive for Preceded<A, A::PVal, B, true>

where A: Productive, B: Productive,

open spec fn productive_inv(&self) -> bool

{ preceded::<_, _, _, _, true>(self.a, self.b, self.a_val).productive_inv() }

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

impl<A, B, const CHECK: bool> SPRoundTripDps for Preceded<A, A::SValue, B, CHECK>

where A: SPRoundTripDps + NonTailFmt, B: SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

{ Pair(self.a, self.b).unambiguous() }

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

impl<A, B, const CHECK: bool> SafeParser for Preceded<A, A::PVal, B, CHECK>

where A: SafeParser, B: SafeParser,

open spec fn safe_inv(&self) -> bool

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.safe_inv()
}

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

impl<Output: OutputBuf, A, AVal, B, T, const CHECK: bool> Serializer<Output, T> for Preceded<A, AVal, B, CHECK>

where AVal: DeepView<V = AVal>, T: DeepView, A: Serializer<Output, AVal>, B: Serializer<Output, T>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.a.exec_inv()
    &&& self.b.exec_inv()
    &&& forall |v: AVal| v.deep_view() == v

}

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

impl<A, B> SoundParser for Preceded<A, A::PVal, B, false>

where A: SoundParser + AdmitsUniqueVal, B: SoundParser,

open spec fn sound_inv(&self) -> bool

{
    &&& Pair(self.a, self.b).sound_inv()
    &&& self.a.consistent(self.a_val)

}

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

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

impl<A, B> SoundParser for Preceded<A, A::PVal, B, true>

where A: SoundParser, B: SoundParser,

open spec fn sound_inv(&self) -> bool

{ Pair(self.a, self.b).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, const CHECK: bool> SpecByteLen for Preceded<A, A::T, B, CHECK>

where A: SpecByteLen, B: SpecByteLen,

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

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.byte_len(v)
}

type T = <B as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<A, B, const CHECK: bool> SpecParser for Preceded<A, A::PVal, B, CHECK>

where A: SpecParser, B: SpecParser,

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

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.spec_parse(ibuf)
}

type PVal = <B as SpecParser>::PVal

The type of parsed values.

impl<A, B, const CHECK: bool> SpecSerializer for Preceded<A, A::SVal, B, CHECK>

where A: SpecSerializer, B: SpecSerializer,

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

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.spec_serialize(v)
}

type SVal = <B as SpecSerializer>::SVal

The type of values to be serialized.

impl<A, B, const CHECK: bool> SpecSerializerDps for Preceded<A, A::SValue, B, CHECK>

where A: SpecSerializerDps, B: SpecSerializerDps,

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

{
    let fmt = preceded::<_, _, _, _, CHECK>(self.a, self.b, self.a_val);
    fmt.spec_serialize_dps(v, obuf)
}

type SValue = <B as SpecSerializerDps>::SValue

The type of values to be serialized.

impl<A, B, const CHECK: bool> StaticByteLen for Preceded<A, A::T, B, CHECK>

where A: StaticByteLen, B: StaticByteLen,

open spec fn static_byte_len() -> nat

{ <Pair<A, B> as StaticByteLen>::static_byte_len() }

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

impl<A, B, const CHECK: bool> ValueByteLen for Preceded<A, A::T, B, CHECK>

where A: StaticByteLen, B: ValueByteLen,

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

{ A::static_byte_len() + B::value_byte_len(v) }

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

impl<A: Copy, AVal: Copy, B: Copy, const CHECK: bool> Copy for Preceded<A, AVal, B, CHECK>