Function vstd::storage_protocol::deposits

source ·

pub open spec fn deposits<K, V, P: Protocol<K, V>>(p1: P, b1: Map<K, V>, p2: P) -> 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())
                    && t1.union_prefer_right(b1) =~= t2
            }
    }
}