Struct PrintableString 

pub struct PrintableString<'a> { /* private fields */ }

Implementations

impl<'a> PrintableString<'a>

pub exec fn new(inner: &'a str) -> res : Self

requires

is_valid_printable_string_spec(vstd::utf8::encode_utf8(inner.deep_view())),

ensures

res.deep_view()
    == (PrintableStringSpec {
        inner: inner.deep_view(),
    }),

pub exec fn inner(&self) -> res : &'a str

ensures

res.deep_view() == self.deep_view().inner,

Trait Implementations

impl<'i> ByteLen<PrintableString<'i>> for PrintableStringFmt

exec fn length(&self, v: &PrintableString<'i>) -> usize

fn exec_inv(&self) -> bool

impl<'a> DeepView for PrintableString<'a>

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

type V = PrintableStringSpec

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

proof fn lemma_der_serialize_len(&self, value: PrintableStringSpec)

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

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

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

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

exec fn der_start(&self, s: &PrintableString<'a>) -> state : BytesDerState

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

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

impl<'a> Pred<PrintableString<'a>> for NumericStringChars

exec fn test(&self, value: &PrintableString<'a>) -> ok : bool

impl<'a, const HAS_MIN: bool, const MIN: usize, const HAS_MAX: bool, const MAX: usize> Pred<PrintableString<'a>> for Size<HAS_MIN, MIN, HAS_MAX, MAX>

exec fn test(&self, value: &PrintableString<'a>) -> ok : bool

impl<'i> Prepare<PrintableString<'i>> for PrintableStringFmt

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

fn exec_inv(&self) -> bool

impl<'i, Output: OutputBuf> Serializer<Output, PrintableString<'i>> for PrintableStringFmt

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

fn exec_inv(&self) -> bool