pub trait DepCombinator {
type Key;
type Val;
type Body: Consistency<Val = Self::Val>;
// Required methods
spec fn apply(&self, key: Self::Key) -> Self::Body;
spec fn recover(&self, value: Self::Val) -> Self::Key;
proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val);
// Provided method
open spec fn recover_inv(&self) -> bool { ... }
}Expand description
A family of dependent combinators indexed by a key type.
Used to constrain the Tail combinator in a Implicit<Head, Tail>.
Required Associated Types§
Sourcetype Body: Consistency<Val = Self::Val>
type Body: Consistency<Val = Self::Val>
The type of the body combinator produced by apply.
Required Methods§
Sourcespec fn apply(&self, key: Self::Key) -> Self::Body
spec fn apply(&self, key: Self::Key) -> Self::Body
Given a key, produce the body combinator for that key.
Sourcespec fn recover(&self, value: Self::Val) -> Self::Key
spec fn recover(&self, value: Self::Val) -> Self::Key
Given a body value, recover the key used to produce the body combinator.
Sourceproof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val)
proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val)
requires
self.recover_inv(),self.apply(key).consistent(value) ==> self.recover(value) == key,Recover must agree with any key that makes the body’s value consistent.
Provided Methods§
Sourceopen spec fn recover_inv(&self) -> bool
open spec fn recover_inv(&self) -> bool
{ true }