Skip to main content

LosslessMapper

vest_lib::combinators::mapped::spec

Trait LosslessMapper 

Source 
pub trait LosslessMapper: LossyMapper {
    // Required methods
    proof fn lemma_lossless_mapper(&self, i: Self::In);
    proof fn lemma_mapper_wf_in_out(&self, i: Self::In);
}
Expand description

A SpecMapper that is lossless (i.e., non-malleable).

Required Methods§

Source

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

requires
self.wf_in(i),
ensures
self.spec_map_rev(self.spec_map(i)) == i,

A lossless mapper should satisfy spec_map_rev(spec_map(i)) == i for all well-formed i. That is, spec_map should be injective on well-formed Self::In values, and spec_map_rev should be its inverse.

Source

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

requires
self.wf_in(i),
ensures
self.wf_out(self.spec_map(i)),

For well-formed i, spec_map(i) should also be well-formed.

Implementors§