Function vstd::pcm_lib::validate_3

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

Validates that the three given resources have values that combine to form a valid value. Although r1 and r2 are mutable, they don’t change. (They change during the function but are restored to the way they were by the time the function returns.)