Skip to main content

withdraws

vstd::resource::storage_protocol

Function withdraws 

Source 
pub open spec fn withdraws<K, V, P: Protocol<K, V>>(p1: P, 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.remove_keys(b2.dom()))
                &&& b2.submap_of(t1)

            }
    }
}