Struct CborMapper 

pub struct CborMapper<const DET: bool>;

Trait Implementations

impl<const DET: bool> Clone for CborMapper<DET>

fn clone(&self) -> CborMapper<DET>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl LosslessMapper for CborMapper<true>

proof fn lemma_lossless_mapper(&self, wire: Self::In)

proof fn lemma_mapper_wf_in_out(&self, wire: Self::In)

impl<const DET: bool> LossyMapper for CborMapper<DET>

proof fn lemma_sound_mapper(&self, value: Self::Out)

proof fn lemma_mapper_wf_out_in(&self, value: Self::Out)

impl<const DET: bool> SpecMapper for CborMapper<DET>

open spec fn spec_map(&self, wire: Self::In) -> Self::Out

{ decode_cbor_wire(wire) }

open spec fn spec_map_rev(&self, value: Self::Out) -> Self::In

{ encode_cbor_value(value) }

open spec fn wf_in(&self, wire: Self::In) -> bool

{ cbor_wire_valid::<DET>(wire) }

open spec fn wf_out(&self, value: Self::Out) -> bool

{ cbor_value_valid(value) }

type In = (CborHead, Sum<(), Sum<(), Sum<Seq<u8>, Sum<(Seq<Seq<u8>>, u8), Sum<Seq<char>, Sum<(Seq<Seq<char>>, u8), Sum<Seq<CborValueSpec>, Sum<(Seq<CborValueSpec>, u8), Sum<Seq<(CborValueSpec, CborValueSpec)>, Sum<(Seq<(CborValueSpec, CborValueSpec)>, u8), Sum<CborValueSpec, Sum<(), ExecNever>>>>>>>>>>>>)

The input type.

type Out = CborValueSpec

The output type.

impl<const DET: bool> Copy for CborMapper<DET>