Skip to main content

LossyMapper

vest_lib::combinators::mapped::spec

Trait LossyMapper 

Source 
pub trait LossyMapper: SpecMapper {
    // Required methods
    proof fn lemma_sound_mapper(&self, o: Self::Out);
    proof fn lemma_mapper_wf_out_in(&self, o: Self::Out);
}
Expand description

A SpecMapper that can be lossy (i.e., malleable).

Required Methods§

Source

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

requires
self.wf_out(o),
ensures
self.spec_map(self.spec_map_rev(o)) == o,

A sound mapper should satisfy spec_map(spec_map_rev(o)) == o for all well-formed o. That is, once Self::Out values are mapped to Self::In, spec_map should map them back to the original Self::Out values.

Source

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

requires
self.wf_out(o),
ensures
self.wf_in(self.spec_map_rev(o)),

Implementors§