Struct Real 

pub struct Real<'a, const DER: bool = true> { /* private fields */ }

Borrowed, exact BER/DER REAL contents.

Implementations

impl<'a, const DER: bool> Real<'a, DER>

pub exec fn from_contents(contents: &'a [u8]) -> value : Result<Self, ParseError>

ensures

value matches Ok(v) ==> v.deep_view() == contents.deep_view(),

value is Ok <==> real_bytes_wf::<DER>(contents@),

Validates and borrows REAL contents under this format’s encoding rules.

pub exec fn contents(&self) -> contents : &'a [u8]

ensures

contents.deep_view() == self.deep_view(),

impl<'a> Real<'a, true>

pub exec fn from_der_contents(contents: &'a [u8]) -> value : Result<Self, ParseError>

ensures

value matches Ok(v) ==> v.deep_view() == contents.deep_view(),

value is Ok <==> der_real_bytes_wf(contents@),

Validates and borrows canonical DER REAL contents.

impl<'a> Real<'a, false>

pub exec fn from_ber_contents(contents: &'a [u8]) -> value : Result<Self, ParseError>

ensures

value matches Ok(v) ==> v.deep_view() == contents.deep_view(),

value is Ok <==> ber_real_bytes_wf(contents@),

Validates and borrows any well-formed BER REAL contents.

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<'a, const DER: bool> DeepView for Real<'a, DER>

closed spec fn deep_view(&self) -> Self::V

type V = Seq<u8>

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<'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<'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