Struct U24BeMapper 

pub struct U24BeMapper;

Trait Implementations

impl LosslessMapper for U24BeMapper

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

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

impl LossyMapper for U24BeMapper

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

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

impl SpecMapper for U24BeMapper

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

{ u24_be_from_bytes(array_from_seq(i)) }

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

{ u24_be_to_bytes(o)@ }

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

{ i.len() == U24_BYTE_LEN }

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

{ o < 0x01000000 }

type In = Seq<u8>

The input type.

type Out = u32

The output type.