Struct RealFmt 

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

ASN.1 REAL contents format.

DER = true accepts only the canonical DER forms. DER = false accepts the additional binary and ISO 6093 decimal forms permitted by BER.

Trait Implementations

impl<'a, const DER: bool> ByteLen<Real<'a, DER>> for RealFmt<DER>

exec fn length(&self, v: &Real<'a, DER>) -> usize

fn exec_inv(&self) -> bool

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

fn clone(&self) -> RealFmt<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 RealFmt<DER>

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

{ real_fmt::<DER>().consistent(v) }

type Val = Seq<u8>

The type of values whose consistency is being checked.

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

proof fn lemma_der_serialize_len(&self, value: Seq<u8>)

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

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

open spec fn der_state_valid(&self, value: Seq<u8>, state: BytesDerState) -> bool

{ state.pos <= self.spec_serialize(value).len() }

exec fn der_start(&self, r: &Real<'a, true>) -> state : BytesDerState

exec fn der_next(&self, r: &Real<'a, true>, state: &mut BytesDerState) -> next : Option<u8>

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

impl DerState for RealFmt<true>

type State = BytesDerState

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

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

fn equiv_inv(&self) -> bool

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

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

fn serialize_inv(&self) -> bool

impl<const DER: bool> NonMalleable for RealFmt<DER>

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

fn nonmal_inv(&self) -> bool

impl<'a, const DER: bool> Parser<&'a [u8]> for RealFmt<DER>

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

type PT = Real<'a, DER>

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<'a, const DER: bool> Prepare<Real<'a, DER>> for RealFmt<DER>

exec fn prepare(&self, v: &Real<'a, DER>) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

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

open spec fn productive_inv(&self) -> bool

{ false }

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

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

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

fn unambiguous(&self) -> bool

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

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

fn safe_inv(&self) -> bool

impl<'a, Output: OutputBuf, const DER: bool> Serializer<Output, Real<'a, DER>> for RealFmt<DER>

exec fn serialize_into(&self, v: &Real<'a, DER>, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl<const DER: bool> SoundParser for RealFmt<DER>

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 RealFmt<DER>

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

{ real_fmt::<DER>().byte_len(v) }

type T = Seq<u8>

The type of values whose byte length is being computed.

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

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

{ real_fmt::<DER>().spec_parse(ibuf) }

type PVal = Seq<u8>

The type of parsed values.

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

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

{ real_fmt::<DER>().spec_serialize(v) }

type SVal = Seq<u8>

The type of values to be serialized.

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

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

{ real_fmt::<DER>().spec_serialize_dps(v, obuf) }

type SValue = Seq<u8>

The type of values to be serialized.

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