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.)