Function vstd::pcm_lib::update_and_redistribute

source · 
pub proof fn update_and_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(),
frame_preserving_update(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,

Update the values held by resources r1 and r2 such that their values’ combination is updated in a frame-preserving way (i.e., that combination must be updatable in a frame-preserving way to the combination of v1 and v2). The new value of r1 will be v1 and the new value of r2 will be v2.