Function vstd::storage_protocol::exchanges_nondeterministic

source ·

pub open spec fn exchanges_nondeterministic<K, V, P: Protocol<K, V>>(
    p1: P,
    s1: Map<K, V>,
    new_values: Set<(P, Map<K, V>)>
) -> bool

Expand description

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