Skip to main content

exchanges

vstd::resource::storage_protocol

Function exchanges 

Source 
pub open spec fn exchanges<K, V, P: Protocol<K, V>>(
    p1: P,
    b1: IMap<K, V>,
    p2: P,
    b2: IMap<K, V>,
) -> bool
Expand description
{
    forall |q: P, t1: IMap<K, V>| {
        P::rel(P::op(p1, q), t1)
            ==> {
                &&& P::rel(P::op(p2, q), t1.union_prefer_right(b1).remove_keys(b2.dom()))
                &&& t1.dom().disjoint(b1.dom())
                &&& b2.submap_of(t1.union_prefer_right(b1))

            }
    }
}