Struct TermByteFromToNat 

pub struct TermByteFromToNat;

Trait Implementations

impl LosslessMapper for TermByteFromToNat

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

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

impl LossyMapper for TermByteFromToNat

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

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

impl SpecMapper for TermByteFromToNat

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

{ i < CONTINUATION_BIT }

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

{ o < CONTINUATION_BIT }

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

{ i as nat }

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

{ o as u8 }

type In = u8

The input type.

type Out = nat

The output type.