Struct CborFmt 

pub struct CborFmt<const DET: bool, const LIMIT: usize = MAX_RECURSION_DEPTH>;

A complete generic CBOR data item with bounded nesting.

Trait Implementations

impl<'i, const DET: bool, const LIMIT: usize> ByteLen<CborValue<'i>> for CborFmt<DET, LIMIT>

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

fn exec_inv(&self) -> bool

impl<const DET: bool, const LIMIT: usize> Clone for CborFmt<DET, LIMIT>

fn clone(&self) -> CborFmt<DET, LIMIT>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<const DET: bool, const LIMIT: usize> Consistency for CborFmt<DET, LIMIT>

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

{ cbor_fmt::<DET, LIMIT>().consistent(value) }

type Val = CborValueSpec

The type of values whose consistency is being checked.

impl<const DET: bool, const LIMIT: usize> EquivSerializers for CborFmt<DET, LIMIT>

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

fn equiv_inv(&self) -> bool

impl<const DET: bool, const LIMIT: usize> EquivSerializersGeneral for CborFmt<DET, LIMIT>

proof fn lemma_serialize_equiv(&self, value: Self::SVal, out: Seq<u8>)

fn equiv_general_inv(&self) -> bool

impl<const DET: bool, const LIMIT: usize> GoodSerializer for CborFmt<DET, LIMIT>

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

fn serialize_inv(&self) -> bool

impl<const LIMIT: usize> NonMalleable for CborFmt<true, LIMIT>

proof fn lemma_parse_non_malleable(&self, left: Seq<u8>, right: Seq<u8>)

fn nonmal_inv(&self) -> bool

impl<const DET: bool, const LIMIT: usize> NonTailFmt for CborFmt<DET, LIMIT>

proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, out: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, value: Self::SValue, out: Seq<u8>)

fn serialize_dps_inv(&self) -> bool

impl<'i, const DET: bool, const LIMIT: usize> Parser<&'i [u8]> for CborFmt<DET, LIMIT>

where CborRecBody<DET>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<DET>> + ParserRecBody<&'i [u8], EP = (), O = CborValue<'i>>, <CborRecBody<DET> as SpecRecBody>::Body: Productive,

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

type PT = CborValue<'i>

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<'i, const DET: bool, const LIMIT: usize> Prepare<CborValue<'i>> for CborFmt<DET, LIMIT>

where CborRecBody<DET>: SpecRecBody<Param = (), T = CborValueSpec, Body = CborBodyFmt<DET>> + PrepareRecBody<CborValue<'i>, EP = ()>,

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

fn exec_inv(&self) -> bool

impl<const DET: bool, const LIMIT: usize> Productive for CborFmt<DET, LIMIT>

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

fn productive_inv(&self) -> bool

impl<const DET: bool, const LIMIT: usize> SPRoundTripDps for CborFmt<DET, LIMIT>

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

fn unambiguous(&self) -> bool

impl<const DET: bool, const LIMIT: usize> SafeParser for CborFmt<DET, LIMIT>

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

fn safe_inv(&self) -> bool

impl<'i, Output: OutputBuf, const DET: bool, const LIMIT: usize> Serializer<Output, CborValue<'i>> for CborFmt<DET, LIMIT>

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

fn exec_inv(&self) -> bool

impl<const LIMIT: usize> SoundParser for CborFmt<true, LIMIT>

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

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

fn sound_inv(&self) -> bool

impl<const DET: bool, const LIMIT: usize> SpecByteLen for CborFmt<DET, LIMIT>

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

{ cbor_fmt::<DET, LIMIT>().byte_len(value) }

type T = CborValueSpec

The type of values whose byte length is being computed.

impl<const DET: bool, const LIMIT: usize> SpecParser for CborFmt<DET, LIMIT>

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

{ cbor_fmt::<DET, LIMIT>().spec_parse(input) }

type PVal = CborValueSpec

The type of parsed values.

impl<const DET: bool, const LIMIT: usize> SpecSerializer for CborFmt<DET, LIMIT>

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

{ cbor_fmt::<DET, LIMIT>().spec_serialize(value) }

type SVal = CborValueSpec

The type of values to be serialized.

impl<const DET: bool, const LIMIT: usize> SpecSerializerDps for CborFmt<DET, LIMIT>

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

{ cbor_fmt::<DET, LIMIT>().spec_serialize_dps(value, out) }

type SValue = CborValueSpec

The type of values to be serialized.

impl<const DET: bool, const LIMIT: usize> Copy for CborFmt<DET, LIMIT>