Type Alias KVFormat 

pub type KVFormat<Key, Value, Fmt> = (FnSpec<(Key,), Fmt>, FnSpec<(Value,), Key>);

Dependent family encoded by a pair of pure spec closures (apply, recover).

Trait Implementations

impl<Key, Val, Body> DepCombinator for KVFormat<Key, Val, Body>

where Body: Consistency<Val = Val>,

open spec fn apply(&self, key: Self::Key) -> Self::Body

{ (self.0)(key) }

open spec fn recover(&self, value: Self::Val) -> Self::Key

{ (self.1)(value) }

open spec fn recover_inv(&self) -> bool

{
    forall |key: Key, value: Val| {
        #[trigger] (self.0)(key).consistent(value) ==> (self.1)(value) == key
    }
}

proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val)

type Key = Key

The type of keys parsed by the head combinator/to be recovered during serialization.

type Val = Val

The type of values consumed/produced by the body combinator.

type Body = Body

The type of the body combinator produced by apply.