Skip to main content

redistribute

vstd::resource

Function 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
final(r1).loc() == old(r1).loc(),
final(r2).loc() == old(r1).loc(),
final(r1).value() == v1,
final(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.