Function vstd::pcm_lib::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.)