vstd::storage_protocol

Trait Protocol

Source 
pub trait Protocol<K, V>: Sized {
    // Required methods
    spec fn op(self, other: Self) -> Self;
    spec fn rel(self, s: Map<K, V>) -> bool;
    spec fn unit() -> Self;
    proof fn commutative(a: Self, b: Self);
    proof fn associative(a: Self, b: Self, c: Self);
    proof fn op_unit(a: Self);
}
Expand description

See StorageResource for more information.

Required Methods§

Source

spec fn op(self, other: Self) -> Self

Source

spec fn rel(self, s: Map<K, V>) -> bool

Note that rel, in contrast to PCM::valid, is not necessarily closed under inclusion.

Source

spec fn unit() -> Self

Source

proof fn commutative(a: Self, b: Self)

ensures
Self::op(a, b) == Self::op(b, a),
Source

proof fn associative(a: Self, b: Self, c: Self)

ensures
Self::op(a, Self::op(b, c)) == Self::op(Self::op(a, b), c),
Source

proof fn op_unit(a: Self)

ensures
Self::op(a, Self::unit()) == a,

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§