Trait DerOrd 

pub trait DerOrd<T>:
    DerState
    + SpecSerializer<SVal = T::V>
    + SpecByteLen<T = T::V>
    + Consistency<Val = T::V>
where
    T: DeepView + ?Sized,
{
    // Required methods
    proof fn lemma_der_serialize_len(&self, value: T::V);
    spec fn der_remaining(
        &self,
        value: T::V,
        state: <Self as DerState>::State,
    ) -> Seq<u8>;
    spec fn der_state_valid(
        &self,
        value: T::V,
        state: <Self as DerState>::State,
    ) -> bool;
    exec fn der_start(&self, value: &T) -> state : <Self as DerState>::State;
    exec fn der_next(
        &self,
        value: &T,
        state: &mut <Self as DerState>::State,
    ) -> next : Option<u8>;

    // Provided method
    exec fn der_leq(&self, left: &T, right: &T) -> leq : bool { ... }
}

A format whose executable values can be traversed in serialization order without producing an intermediate byte buffer.

State contains only traversal state; it must not own a serialization of the value.

Required Methods

proof fn lemma_der_serialize_len(&self, value: T::V)

requires

self.consistent(value),

ensures

self.spec_serialize(value).len() == self.byte_len(value),

DER cursors range over the same number of octets as the format’s byte-length model.

Unlike crate::core::spec::GoodSerializer::lemma_serialize_len, this law is unconditional once the value is consistent.

spec fn der_remaining( &self, value: T::V, state: <Self as DerState>::State, ) -> Seq<u8>

The portion of spec_serialize(value) not yet returned by the cursor.

spec fn der_state_valid(&self, value: T::V, state: <Self as DerState>::State) -> bool

The format-specific cursor invariant.

exec fn der_start(&self, value: &T) -> state : <Self as DerState>::State

requires

self.consistent(value.deep_view()),

ensures

self.der_state_valid(value.deep_view(), state),

self.der_remaining(value.deep_view(), state) == self.spec_serialize(value.deep_view()),

Start traversing the encoding of value.

exec fn der_next( &self, value: &T, state: &mut <Self as DerState>::State, ) -> next : Option<u8>

requires

self.consistent(value.deep_view()),

self.der_state_valid(value.deep_view(), *old(state)),

ensures

self.der_state_valid(value.deep_view(), *final(state)),

match next {
    Some(byte) => {
        self.der_remaining(value.deep_view(), *old(state))
            == seq![byte] + self.der_remaining(value.deep_view(), *final(state))
    }
    None => (
        &&& self.der_remaining(value.deep_view(), *old(state)).len() == 0
        &&& self.der_remaining(value.deep_view(), *final(state)).len() == 0

    ),
},

Return the next encoded octet, or None exactly at the end of the encoding.

Provided Methods

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

requires

self.consistent(left.deep_view()),

self.consistent(right.deep_view()),

ensures

leq
    == der_octets_leq(
        self.spec_serialize(left.deep_view()),
        self.spec_serialize(right.deep_view()),
    ),

Compare two values by the complete DER TLV octets produced by this format.

Implementors

impl DerOrd<bool> for BoolFmt<true>

impl DerOrd<i8> for Integer8Fmt

impl DerOrd<i16> for Integer16Fmt

impl DerOrd<u8> for U8

impl DerOrd<u64> for Base128Fmt<true>

impl DerOrd<()> for Empty

impl DerOrd<()> for Eof

impl DerOrd<usize> for LengthFmt<true>

impl DerOrd<BmpString> for BmpStringFmt

Available on crate feature alloc only.

impl DerOrd<ObjectIdentifier> for ObjectIdentifierFmt

Available on crate feature alloc only.

impl DerOrd<Tag> for TagFmt

impl DerOrd<UtcTime> for UtcTimeFmt<true>

impl DerOrd<String> for UniversalStringFmt

Available on crate feature alloc only.

impl DerOrd<[u8]> for Tail

impl<'a> DerOrd<&'a str> for Utf8StringFmt

impl<'a> DerOrd<&'a [u8]> for Tail

impl<'a> DerOrd<Integer<'a>> for EnumeratedFmt

impl<'a> DerOrd<Integer<'a>> for IntegerFmt

impl<'a> DerOrd<Any<'a>> for AnyFmt<true>

impl<'a> DerOrd<BitString<'a>> for BitStringFmt<true>

impl<'a> DerOrd<GeneralizedTime<'a>> for GeneralizedTimeFmt<true>

impl<'a> DerOrd<Ia5String<'a>> for Ia5StringFmt

impl<'a> DerOrd<PrintableString<'a>> for PrintableStringFmt

impl<'a> DerOrd<Real<'a>> for RealFmt<true>

impl<'a> DerOrd<TeletexString<'a>> for TeletexStringFmt

impl<A, B, TA, TB> DerOrd<(Option<TA>, TB)> for Optional<A, B>

where TA: DeepView, TB: DeepView, A: DerOrd<TA>, B: DerOrd<TB>,

impl<A, B, TA, TB> DerOrd<Sum<TA, TB>> for Choice<A, B>

where TA: DeepView, TB: DeepView, A: DerOrd<TA>, B: DerOrd<TB>,

impl<A, B, TA, TB> DerOrd<(TA, TB)> for Pair<A, B>

where TA: DeepView, TB: DeepView, A: DerOrd<TA>, B: DerOrd<TB>,

impl<A, T> DerOrd<Option<T>> for Opt<A>

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

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

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

Available on crate feature alloc only.

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

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

Available on crate feature alloc only.

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

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

Available on crate feature alloc only.

impl<Content, T> DerOrd<T> for ASN1Fmt<Content, true>

where T: DeepView + ?Sized, Content: SpecCombinator<T = T::V> + DerOrd<T>,

impl<F, T> DerOrd<T> for ImplicitlyTaggedFmt<F>

where T: DeepView + ?Sized, F: Retaggable + DerOrd<T>,

impl<Field, Default, Rest, R> DerOrd<(Default, R)> for DefaultedFmt<Field, Default, Rest, true>

where Default: DeepViewIdentity + PartialEq + Structural, R: DeepView, Field: DerOrd<Default>, Rest: DerOrd<R>,

impl<Inner, M, MRev, T> DerOrd<T> for Mapped<Inner, BiMap<M, MRev>>

where T: DeepView, M: SpecMap<Input = MRev::Output, Output = T::V>, MRev: SpecMap<Input = T::V> + for<'x> Map<&'x T>, for<'x> Inner: DerState + DerOrd<<MRev as Map<&'x T>>::O>,

impl<Inner, P, T> DerOrd<T> for Refined<Inner, P>

where T: DeepView, Inner: DerOrd<T>, P: Pred<T>,

impl<Inner, T> DerOrd<&T> for Ref<Inner>

where T: DeepView + ?Sized, Inner: DerOrd<T>,