Function vstd::storage_protocol::exchanges

source ·

pub open spec fn exchanges<K, V, P: Protocol<K, V>>(
    p1: P,
    b1: Map<K, V>,
    p2: P,
    b2: Map<K, V>
) -> bool

Expand description

{
    forall |q: P, t1: Map<K, V>| {
        P::rel(P::op(p1, q), t1)
            ==> exists |t2: Map<K, V>| {
                P::rel(P::op(p2, q), t2) && t1.dom().disjoint(b1.dom())
                    && t2.dom().disjoint(b2.dom())
                    && t1.union_prefer_right(b1) =~= t2.union_prefer_right(b2)
            }
    }
}