Struct GeneralizedTimeFmt 

pub struct GeneralizedTimeFmt<const DER: bool = true>;

ASN.1 GeneralizedTime format.

Trait Implementations

impl<'i, const DER: bool> ByteLen<GeneralizedTime<'i>> for GeneralizedTimeFmt<DER>

exec fn length(&self, value: &GeneralizedTime<'i>) -> usize

fn exec_inv(&self) -> bool

impl<const DER: bool> Clone for GeneralizedTimeFmt<DER>

fn clone(&self) -> GeneralizedTimeFmt<DER>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<const DER: bool> Consistency for GeneralizedTimeFmt<DER>

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

{
    (if DER { value.der_wf() } else { value.wf() })
        && generalized_time_len(value) <= usize::MAX
}

type Val = GeneralizedTimeSpec

The type of values whose consistency is being checked.

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

proof fn lemma_der_serialize_len(&self, value: GeneralizedTimeSpec)

open spec fn der_remaining( &self, value: GeneralizedTimeSpec, state: GeneralizedTimeDerState, ) -> Seq<u8>

{ self.spec_serialize(value).skip(state.pos as int) }

open spec fn der_state_valid( &self, value: GeneralizedTimeSpec, state: GeneralizedTimeDerState, ) -> bool

{
    &&& state.pos <= self.spec_serialize(value).len()
    &&& state.prefix@ == crate::asn1::generalizedtime::generalized_time_prefix(value)

}

exec fn der_start(&self, t: &GeneralizedTime<'a>) -> state : GeneralizedTimeDerState

exec fn der_next( &self, t: &GeneralizedTime<'a>, state: &mut GeneralizedTimeDerState, ) -> next : Option<u8>

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

impl DerState for GeneralizedTimeFmt<true>

type State = GeneralizedTimeDerState

impl<const DER: bool> EquivSerializers for GeneralizedTimeFmt<DER>

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

fn equiv_inv(&self) -> bool

impl<const DER: bool> GoodSerializer for GeneralizedTimeFmt<DER>

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

fn serialize_inv(&self) -> bool

impl NonMalleable for GeneralizedTimeFmt<true>

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

fn nonmal_inv(&self) -> bool

impl<'i, const DER: bool> Parser<&'i [u8]> for GeneralizedTimeFmt<DER>

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

type PT = GeneralizedTime<'i>

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<'i, const DER: bool> Prepare<GeneralizedTime<'i>> for GeneralizedTimeFmt<DER>

exec fn prepare( &self, value: &GeneralizedTime<'i>, ) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl<const DER: bool> Productive for GeneralizedTimeFmt<DER>

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

fn productive_inv(&self) -> bool

impl<const DER: bool> SPRoundTripDps for GeneralizedTimeFmt<DER>

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

fn unambiguous(&self) -> bool

impl<const DER: bool> SafeParser for GeneralizedTimeFmt<DER>

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

fn safe_inv(&self) -> bool

impl<'i, Output: OutputBuf, const DER: bool> Serializer<Output, GeneralizedTime<'i>> for GeneralizedTimeFmt<DER>

exec fn serialize_into(&self, value: &GeneralizedTime<'i>, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl SoundParser for GeneralizedTimeFmt<true>

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

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

fn sound_inv(&self) -> bool

impl<const DER: bool> SpecByteLen for GeneralizedTimeFmt<DER>

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

{ generalized_time_len(value) }

type T = GeneralizedTimeSpec

The type of values whose byte length is being computed.

impl<const DER: bool> SpecParser for GeneralizedTimeFmt<DER>

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

{
    if generalized_time_wf::<DER>(ibuf) {
        Some((ibuf.len() as int, generalized_time_value(ibuf).unwrap()))
    } else {
        None
    }
}

type PVal = GeneralizedTimeSpec

The type of parsed values.

impl<const DER: bool> SpecSerializer for GeneralizedTimeFmt<DER>

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

{ generalized_time_bytes(value) }

type SVal = GeneralizedTimeSpec

The type of values to be serialized.

impl<const DER: bool> SpecSerializerDps for GeneralizedTimeFmt<DER>

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

{ generalized_time_bytes(value) }

type SValue = GeneralizedTimeSpec

The type of values to be serialized.

impl<const DER: bool> Copy for GeneralizedTimeFmt<DER>