Skip to main content

validate_5

vstd::resource

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: &Resource<P>,
)
Expand description
requires
old(r1).loc() == r5.loc(),
old(r2).loc() == r5.loc(),
old(r3).loc() == r5.loc(),
old(r4).loc() == r5.loc(),
ensures
r1.loc() == r5.loc(),
r2.loc() == r5.loc(),
r3.loc() == r5.loc(),
r4.loc() == r5.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(), 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 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.)