Function vstd::pcm_lib::validate_4

source ·

pub proof fn validate_4<P: PCM>(tracked 
    r1: &mut Resource<P>,
tracked     r2: &mut Resource<P>,
tracked     r3: &mut Resource<P>,
tracked     r4: &mut Resource<P>
)

Expand description

requires

old(r1).loc() == old(r2).loc() == old(r3).loc() == old(r4).loc(),

ensures

r1.loc() == r2.loc() == r3.loc() == r4.loc() == old(r1).loc(),

r1.value() == old(r1).value(),

r2.value() == old(r2).value(),

r3.value() == old(r3).value(),

r4.value() == old(r4).value(),

P::op(r1.value(), P::op(r2.value(), P::op(r3.value(), r4.value()))).valid(),

Validates that the four given resources have values that combine to form a valid value. Although the inputs r1, r2, r3, and r4 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.)