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.

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors

impl DerOrd<()> for Empty

impl DerOrd<()> for Eof

impl DerOrd<BmpString> for BmpStringFmt

Available on crate feature alloc only.

impl DerOrd<ObjectIdentifier> for ObjectIdentifierFmt

Available on crate feature alloc only.

impl DerOrd<String> for UniversalStringFmt

Available on crate feature alloc only.

impl DerOrd<Tag> for TagFmt

impl DerOrd<UtcTime> for UtcTimeFmt<true>

impl DerOrd<[u8]> for Tail

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<usize> for LengthFmt<true>

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

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

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<Integer<'a>> for EnumeratedFmt

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

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<(TA, TB)> for Pair<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, T> DerOrd<Option<T>> for Opt<A>

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

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<A, T> DerOrd<Vec<T>> for Star<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>,