Prove stronger stepping frame rule
Right now, we have a "stepping frame rule" that looks as follows:
{ P } e { Q } e is not a value
------------------------------------
{ \later R * P } e { R * Q }Essentially, this allows us to step away a later when framing around any non-value. (We also sometimes call this the "atomic frame rule", since atomic expressions are never values. But the one above is just as valid, and obviously stronger.)
However, I think I will need for my Rust stuff a stronger version of this rule, that allows me to strip away a later inside an invariant from any non-value. This comes up because I have non-atomic reads and writes that are, well, non-atomic, and I still want to strip away a later from something that is located inside an invariant[1]. This rule is rather awkward to write down in terms of Hoare triples and view shifts:
R0 E1^==>^E2 \later R1 R1 E2^==>^E1 R2 { P } e { Q }_E1
e is not a value E2 <= E1
------------------------------------------------------------------
{ R0 * P } e { R2 * Q }_E1It looks nicer in terms of primitive view shifts and weakest-pre:
wp_E1 e Q * vs_E1^E2(\later vs_E2^E1(R))
e is not a value E2 <= E1
-------------------------------------
wp_E1 e (Q * R)When we re-do the weakest-pre proofs for V2.0, I think this is the rule we should show. (And derive the old one, of course.)
[1] If you are curious: The invariant has two states "vs(P)" and "P", with an STS making sure that one can only go from the 1st state to the 2nd. The rule I need allows me to open this invariant alongside the non-atomic access, obtain "\later (vs(P) / P)", strip away the later, view shift to "P", and put that back into the invariant; taking out the witness that the view shift has been performed. I do not need any resource from the invariant to justify the memory access, so it's fine for that one to be non-atomic. But I do need to perform this view shift, because immediately after the access I will want to open the invariant again and know I get "\later P", without any more skips.