Function vstd::pcm_lib::redistribute

source · 
pub proof fn redistribute<P: PCM>(tracked 
    r1: &mut Resource<P>,
tracked     r2: &mut Resource<P>,
    v1: P,
    v2: P
)
Expand description
requires
old(r1).loc() == old(r2).loc(),
P::op(old(r1).value(), old(r2).value()) == P::op(v1, v2),
ensures
r1.loc() == r2.loc() == old(r1).loc(),
r1.value() == v1,
r2.value() == v2,

Redistribute the values held by resources r1 and r2 such that they have the same combination as before. The new value of r1 will be v1 and the new value of r2 will be v2.