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() == r3.loc(),old(r2).loc() == r3.loc(),final(r1).loc() == r3.loc(),final(r2).loc() == r3.loc(),final(r1).value() == old(r1).value(),final(r2).value() == old(r2).value(),P::op(final(r1).value(), P::op(final(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.)