Struct SetOfFmt 

pub struct SetOfFmt<C>(pub C);

DER SET OF contents whose elements are encoded by C.

C must encode a complete DER element, including its tag and length. The parsed value is a Vec<C::PT> in canonical DER order. Duplicate encodings are permitted.

Tuple Fields

0: C

Implementations

impl<C: SpecParser> SetOfFmt<C>

pub open spec fn parse_ordered( &self, ibuf: Seq<u8>, previous: Seq<Seq<u8>>, ) -> Option<Seq<C::PVal>>

{
    if !der_encodings_sorted(previous) {
        None
    } else if ibuf.len() == 0 {
        Some(Seq::empty())
    } else {
        match self.0.spec_parse(ibuf) {
            Some(
                (n, v),
            ) if 0 < n <= ibuf.len()
                && der_encodings_sorted(previous.push(ibuf.take(n))) => {
                match self.parse_ordered(ibuf.skip(n), previous.push(ibuf.take(n))) {
                    Some(values) => Some(seq![v] + values),
                    None => None,
                }
            }
            _ => None,
        }
    }
}

Parses all remaining elements while maintaining a canonically sorted encoding prefix.

Trait Implementations

impl<C, Elem> ByteLen<[Elem]> for SetOfFmt<C>

where C: SpecByteLen<T = <Elem as DeepView>::V> + ByteLen<Elem> + Copy, Elem: DeepView,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn length(&self, v: &[Elem]) -> len : usize

impl<C, Elem> ByteLen<Vec<Elem>> for SetOfFmt<C>

where C: SpecByteLen<T = <Elem as DeepView>::V> + ByteLen<Elem> + Copy, Elem: DeepView,

Available on crate feature alloc only.

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn length(&self, values: &Vec<Elem>) -> len : usize

impl<C: Clone> Clone for SetOfFmt<C>

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

ensures

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

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

Performs copy-assignment from source.

impl<C> Consistency for SetOfFmt<C>

where C: Consistency + SpecSerializer<SVal = C::Val>,

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

{
    &&& Star(self.0).consistent(values)
    &&& set_of_values_sorted(self.0, values)

}

type Val = Seq<<C as Consistency>::Val>

The type of values whose consistency is being checked.

impl<A, T> DerOrd<Vec<T>> for SetOfFmt<A>

where T: DeepView, A: DerOrd<T> + Copy,

Available on crate feature alloc only.

proof fn lemma_der_serialize_len(&self, values: Seq<T::V>)

open spec fn der_remaining( &self, values: Seq<T::V>, state: StarDerState<A::State>, ) -> Seq<u8>

{ Star(self.0).der_remaining(values, state) }

open spec fn der_state_valid( &self, values: Seq<T::V>, state: StarDerState<A::State>, ) -> bool

{ Star(self.0).der_state_valid(values, state) }

exec fn der_start(&self, v: &Vec<T>) -> state : StarDerState<A::State>

exec fn der_next(&self, v: &Vec<T>, state: &mut StarDerState<A::State>) -> next : Option<u8>

fn der_leq(&self, left: &T, right: &T) -> bool

impl<A: DerState> DerState for SetOfFmt<A>

Available on crate feature alloc only.

type State = StarDerState<<A as DerState>::State>

impl<C: EquivSerializersGeneral> EquivSerializers for SetOfFmt<C>

open spec fn equiv_inv(&self) -> bool

{ self.0.equiv_general_inv() }

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

impl<C: GoodSerializer> GoodSerializer for SetOfFmt<C>

open spec fn serialize_inv(&self) -> bool

{ self.0.serialize_inv() }

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

impl<C: NonMalleable> NonMalleable for SetOfFmt<C>

open spec fn nonmal_inv(&self) -> bool

{ self.0.nonmal_inv() && self.0.safe_inv() }

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

impl<'i, C> Parser<&'i [u8]> for SetOfFmt<C>

where C: Parser<&'i [u8]> + SafeParser + Productive + Copy,

Available on crate feature alloc only.

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.0.safe_inv()
    &&& self.0.productive_inv()

}

exec fn parse(&self, ibuf: &&'i [u8]) -> r : PResult<Self::PT>

type PT = Vec<<C as Parser<&'i [u8]>>::PT>

Executable value returned by this parser.

impl<C, Elem> Prepare<[Elem]> for SetOfFmt<C>

where Elem: DeepView, C: SpecCombinator<T = <Elem as DeepView>::V> + Prepare<Elem> + DerOrd<Elem> + Copy,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn prepare(&self, values: &[Elem]) -> checked : Result<usize, PreSerializeError>

impl<C, Elem> Prepare<Vec<Elem>> for SetOfFmt<C>

where Elem: DeepView, C: SpecCombinator<T = <Elem as DeepView>::V> + Prepare<Elem> + DerOrd<Elem> + Copy,

Available on crate feature alloc only.

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn prepare(&self, values: &Vec<Elem>) -> checked : Result<usize, PreSerializeError>

impl<C: SafeParser> Productive for SetOfFmt<C>

open spec fn productive_inv(&self) -> bool

{ false }

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

impl<C> SPRoundTripDps for SetOfFmt<C>

where C: SPRoundTripDps + NonTailFmt + EquivSerializersGeneral + Productive + SpecSerializer<SVal = C::T>,

open spec fn unambiguous(&self) -> bool

{
    &&& self.0.unambiguous()
    &&& self.0.serialize_dps_inv()
    &&& self.0.equiv_general_inv()
    &&& self.0.safe_inv()
    &&& self.0.productive_inv()

}

proof fn theorem_serialize_dps_parse_roundtrip(&self, values: Self::T, _obuf: Seq<u8>)

impl<C: SafeParser> SafeParser for SetOfFmt<C>

open spec fn safe_inv(&self) -> bool

{ self.0.safe_inv() }

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

impl<Output: OutputBuf, C, Elem> Serializer<Output, [Elem]> for SetOfFmt<C>

where Elem: DeepView, C: SpecCombinator<T = <Elem as DeepView>::V> + Serializer<Output, Elem> + Copy,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn serialize_into(&self, v: &[Elem], obuf: &mut Output)

impl<Output: OutputBuf, C, Elem> Serializer<Output, Vec<Elem>> for SetOfFmt<C>

where Elem: DeepView, C: SpecCombinator<T = <Elem as DeepView>::V> + Serializer<Output, Elem> + Copy,

Available on crate feature alloc only.

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

exec fn serialize_into(&self, values: &Vec<Elem>, obuf: &mut Output)

impl<C: SoundParser + PSRoundTrip> SoundParser for SetOfFmt<C>

open spec fn sound_inv(&self) -> bool

{ self.0.sound_inv() && self.0.ps_roundtrip_inv() }

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

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

impl<C: SpecByteLen> SpecByteLen for SetOfFmt<C>

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

{ Star(self.0).byte_len(v) }

type T = Seq<<C as SpecByteLen>::T>

The type of values whose byte length is being computed.

impl<C: SpecParser> SpecParser for SetOfFmt<C>

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

{
    match self.parse_ordered(ibuf, Seq::empty()) {
        Some(values) => Some((ibuf.len() as int, values)),
        _ => None,
    }
}

type PVal = Seq<<C as SpecParser>::PVal>

The type of parsed values.

impl<C: SpecSerializer> SpecSerializer for SetOfFmt<C>

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

{ Star(self.0).spec_serialize(v) }

type SVal = Seq<<C as SpecSerializer>::SVal>

The type of values to be serialized.

impl<C: SpecSerializerDps> SpecSerializerDps for SetOfFmt<C>

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

{ Star(self.0).spec_serialize_dps(v, Seq::empty()) }

type SValue = Seq<<C as SpecSerializerDps>::SValue>

The type of values to be serialized.

impl<C: Copy> Copy for SetOfFmt<C>