Proposal: rework the rules for old(self) in preconditions and postconditions

[tchajed]

Edit by @utaal-b: the original title of this by @tchajed is: "Proposal: remove requirement to use old(self) in preconditions". I'm updating it to expand its scope to when new (or similar) will come up for the end of a mutable borrow.

Currently, for any &mut argument a, Verus requires old(a) to be used in preconditions and disallows plain a. I don't know the exact rationale for this, but I believe it was so that old(a) has the same meaning in a precondition and postcondition.

I find that this is unintuitive and mostly results in syntactic overhead when writing preconditions, without adding clarity. In my mind it is consistent for a to always mean the "current" value, which is dependent on whether this is a precondition or postcondition, and this is often what is desired. The current setup makes it possible to make copy-paste errors like old(self).valid() in both pre and postcondition when self.valid() was intended in the postcondition. (I think no matter the design some copy-paste errors are possible.)

One proposal is to go back to the way Dafny works and simply use self in preconditions, and disallow old. As far as I can tell this has little impact on the Verus implementation.

Another option is to instead have new(a), as mypyvy does. In that case a would always refer to the current/old value, and obviously new would only be supported in postconditions. Note that mypvy doesn't have a distinct notion of pre/postconditions since the entire transition is expressed as a predicate over a and new(a), so the design considerations may be different in Verus.

---

Edit by @utaal-b:

@jonhnet and I discussed this offline, and we believe these should be the principles for old/new:

1. the meaning is so often implicit, that you are not allowed to write old/new when the meaning is unambiguous;
2. in the absence of returned mutable references, the only case that's ambiguous is &mut;
3. so the solution in lets is explicitness;
4. so what to do about ensures? They allow both old/new.
5. In requires and ensures you're allowed to omit the modifier for &mut, and the meaning is old for requires, and new for ensures.
6. unadorned is disallowed in lets.

[jaybosamiya]

I support removing the old(a) requirement in preconditions.

I would strongly suggest against new(a) primarily because that'll cause there to be a split between syntax used in the body, and in post-conditions. Also, somewhat importantly, new is already extremely commonly used convention to mean "constructor" in Rust code, so would lead to confusion if it was a keyword at a specific point in the language.

As for old(a) vs a in the pre-condition: I believe we should support both, but have a warning telling people that old(a) is the exact same thing as a in pre-conditions (rather than it being a hard error), since there is literally no other way to interpret old(a) in a pre-condition. This way people can gradually move away from using it, but if they do prefer having the old(a) around for whatever reason (such as being able to quickly copy-pasta pieces into assertions and such while developing the body of the function) then they can do so, and then once they're ready, can remove it to clear out the warning.

[tjhance]

I think whatever approach we take here, it needs to be considered in light of more general &mut support. There's a discussion for that here: #35

[tjhance]

Note that in the proposal I wrote up, there would be something similar to new (name TBD) but it wouldn't be a special case within post-conditions.

[utaal]

I believe it was so that old(a) has the same meaning in a precondition and postcondition.

This was, I believe, my decision, and that's correct. I personally found Dafny's approach of a meaning different things in the pre- and post-condition to be confusing.

In my mind it is consistent for a to always mean the "current" value, which is dependent on whether this is a precondition or postcondition, and this is often what is desired.

As demonstrated by the fact that we have different preferences here, I think it's likely people will have different opinions on what feels consistent. I suspect this is because, by the nature of how we specify pre- and post- conditions, there may not be a perfectly consistent approach. Consider that: (a) in the function body, the value of a changes from its initial to its final value from top to bottom of the body; (b) in the signature, a represents the binding and is associated with "both" the initial and final value. So, in the code structure from top to bottom of a function, we start with a being associated with both initial and final value in the signature, then we move to the pre-state in preconditions and the post-state in postconditions, to then go back to the initial value at the top of the method body.
That gets further complicated by a third state introduced by the support for &mut, as @tjhance mentioned: the value of a when the borrow expires, which is "later" than the end of the current function body, if you will (as it's a program location in the caller).

[jonhnet]

I agree with @utaal 's assessment that every choice has some inconsistency.
Having now used the syntax in anger for a while, I very much agree with @tchajed 's assessment that 'old(a)' in requires is pure clutter. I never want to read it; the only thing it has going for it is that the compiler can accurately scold me that I need to type it. I'd love to see it go away.

[parno]

FWIW, coming from Dafny, I was initially annoyed by it, but I've grown used to it. I think it helps that (a) when you don't add old in the precondition, there's a clear explanation from the compiler on what is wrong and how to fix it, (b) I do see some value in maintaining consistency between how the pre- and post-conditions refer to the same value, especially since this is something I've seen students in my classes struggle with, and (c) I think there have been at least a couple of times when being forced to write old in the precondition made me realize I had messed up a new/old relationship in the post-condition, which is something that's much harder to automatically check.

[tjhance]

My own personal feeling is:

• I don't really care what I write in the precondition. Using *old(a) or *a doesn't make a difference to me. Maybe I mildly prefer *old(a), but this is only for the sake of consistency with the next bullet point.
• I'd prefer to be completely explicit in the post-condition. Like, I'd be happiest if I was forced to write old/new in the postcondition without ever using a naked *a.

[tjhance]

Also, maybe we should consider some totally different syntaxes, like a.old or a.new.

(Though it's unfortunate that new overlaps with a common Rust idiom, as jay pointed out)

[utaal]

The consensus at the [Verus all-hands] was that we'd want to remove the requirement, but we may want to hold off until the syntax to support the prophecy-based encoding has settled.

[tjhance]

This proposal is a little awkward in conjunction with the prophecy encoding.

If you have an input parameter a: &mut T, then in the prophecy-style encoding, there's no "in parameter" and "out parameter", there's just an in-parameter a which is encoded as a pair, a "current" value and an "expiry" value. By this encoding, current(a) always refers to what we think of as the "old" value, even in the postcondition, whereas expiry(a) always refers to what we think of as the "new" value.

So if we want to have *a mean the "old" value in a precondition, while also having *a mean the "new" value in a postcondition, that would mean:

• *a refers to current(a) in the precondition
• *a refers to expiry(a) in the postcondition

I think we'd end up with a picture like this:

	precondition	postcondition	body
*a	current	expiry	current
old(a)	current	current	current (snapshot at start of body)
current(a)	current	current	current
expiry(a)	expiry	expiry	expiry

So current(a) and expiry(a) would basically mean "give me this value out of the encoding", while *a means, "the value pointed to by the reference at this point in time" and old(a) means, "the value pointed to by the reference at the start of the function body".

However, this interpretation of *a doesn't work if the borrow lifetime expires later than the end of the function call (which could happen if the function returns a mutable reference). So maybe *a should be disallowed in the postcondition in that case...?

[utaal]

The design principle should be (from a conversation between @jonhnet and @utaal):

1. the meaning is so often implicit, that you are not allowed to write old/new when the meaning is unambiguous;
2. in the absence of returned mutable references, the only case that's ambiguous is &mut;
3. so the solution in lets is explicitness;
4. so what to do about ensures? They allow both old/new.
5. In requires and ensures you're allowed to omit the modifier for &mut, and the meaning is old for requires, and new for ensures.
6. unadorned is disallowed in lets.