Struct LowBitsMask 

pub struct LowBitsMask;

Trait Implementations

impl LosslessMapper for LowBitsMask

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

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

impl LossyMapper for LowBitsMask

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

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

impl SpecMapper for LowBitsMask

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 - CONTINUATION_BIT) as u8 }

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

{ (o + CONTINUATION_BIT) as u8 }

type In = u8

The input type.

type Out = u8

The output type.