Skip to main content

SpecMapper

vest_lib::combinators::mapped::spec

Trait SpecMapper 

Source 
pub trait SpecMapper {
    type In;
    type Out;

    // Required methods
    spec fn spec_map(&self, i: Self::In) -> Self::Out;
    spec fn spec_map_rev(&self, o: Self::Out) -> Self::In;

    // Provided methods
    open spec fn wf_in(&self, i: Self::In) -> bool { ... }
    fn wf_out(&self, o: Self::Out) -> bool { ... }
}
Expand description

A bidirectional mapping between two types (forward for parsing, reverse for serialization). For roundtrip guarantees, implement and prove LossyMapper or LosslessMapper as appropriate.

Required Associated Types§

Source

type In

The input type.

Source

type Out

The output type.

Required Methods§

Source

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

Forward mapping (used during parsing).

Source

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

Reverse mapping (used during serialization).

Provided Methods§

Source

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

{ true }

Optional refinement predicates on the input type.

This is the precondition for LosslessMapper::lemma_lossless_mapper.

Source

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

{ true }

Optional refinement predicates on the output type.

This is the precondition for LossyMapper::lemma_sound_mapper.

Implementors§