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.