pub proof fn validate_4<P: PCM>(
tracked r1: &mut Resource<P>,
tracked r2: &mut Resource<P>,
tracked r3: &mut Resource<P>,
tracked r4: &Resource<P>,
)Expand description
requires
old(r1).loc() == r4.loc(),old(r2).loc() == r4.loc(),old(r3).loc() == r4.loc(),final(r1).loc() == r4.loc(),final(r2).loc() == r4.loc(),final(r3).loc() == r4.loc(),final(r1).value() == old(r1).value(),final(r2).value() == old(r2).value(),final(r3).value() == old(r3).value(),P::op(final(r1).value(), P::op(final(r2).value(), P::op(final(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 and r3 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.)