vstd::pcm_lib

Function validate_5

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

Validates that the five given resources have values that combine to form a valid value. Although the inputs 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.)