Renamings

[arnaudgolfouse]

Various renamings to prepare for ghost code with ownership

• Ghost type -> Snapshot
• gh! -> snapshot!
• #[ghost] -> #[logic]
• #[logic] -> #[logic(prophetic)]
• #[predicate] -> #[predicate] and #[predicate(prophetic)]

[xldenis]

#[predicate] -> #[predicate] and #[predicate(prophetic)]

Can you comment on this a bit? Why do we need to introduce this distinction? I thought the purpose of "final borrows" was in part to solve soundness issues with logical definitions and ghost code without having to do this.

cc @jhjourdan

I think if we go this way we should more seriously consider the implications on usability and the overall Pearlite language. If we forbid prophecies in some definitions but not in others, this seems to map to what Dafny calls twostate predicates: would we then be able to rephrase all of pearlite to use old instead of ^? Alternatively, could we use something like what @dewert99 developed with at<'a>?

Secondarily, I would like to remove predicate entirely.

[jhjourdan]

I'm responsible for suggesting this change @arnaudgolfouse is simply implementing it. The motivation is that it is weird to have #[ghost] and ghost! refer to completely unrelated concepts.

Can you comment on this a bit? Why do we need to introduce this distinction? I thought the purpose of "final borrows" was in part to solve soundness issues with logical definitions and ghost code without having to do this.

I don't remember all the discussions we had, but it seems clear to me that if we want to allow snapshots and allow to do something with them (e.g., compare them), then it is necessary to make sure that snapshots are not prophetic. And of course, we need prophecies in specifications. I don't think I've ever promised to lift this distinction.

The improvement of "final borrows" is that we now have a simple syntactic criterion to determine if a logical term is not prophetic: a logical term is not prophetic if it does not have ^ in it and if it does not call prophetic functions. In particular, instantiating a generic logical function cannot make it suddenly prophetic (which was not the case before, becaue of equality).

I think if we go this way we should more seriously consider the implications on usability and the overall Pearlite language.

Our idea was that the "prophetic" qualification would be limited to advanced users. Indeed, in most common cases, mutable borrows are limited to functions parameters, and the prophecy operator don't need to be used outside of specifications. So, in tutorial, we would not teach #[logical(prophetic)], and instead we will have a good error message which explain what is it when the user tries to write a prophetic logical function.

If we forbid prophecies in some definitions but not in others, this seems to map to what Dafny calls twostate predicates: would we then be able to rephrase all of pearlite to use old instead of ^? Alternatively, could we use something like what @dewert99 developed with at<'a>?

I don't see why this would interact with the current proposal. That being said, if we want this, there are clearly lots of discussions to have. First, Dafny's old and twostate predicates seem a bit too restrictive, because if there are more than 1 lifetime, then we would need more than 2 states. @dewert99 's at<'a> is attractive, but we need to make sure that we correctly track lifetimes in pearlite, which I'm not sure we do (e.g., there is a coercion between &mut 'a T and &mut 'b T for any 'a and 'b in pearlite). But all this is a different concern, I think.

[xldenis]

I'm responsible for suggesting this change @arnaudgolfouse is simply implementing it. The motivation is that it is weird to have #[ghost] and ghost! refer to completely unrelated concepts.

This is unambiguously a good cleanup.

I don't remember all the discussions we had, but it seems clear to me that if we want to allow snapshots and allow to do something with them (e.g., compare them), then it is necessary to make sure that snapshots are not prophetic. And of course, we need prophecies in specifications. I don't think I've ever promised to lift this distinction.

I do recall this conversation now that you mention it.

LGTM after explanation.

[dewert99]

My implementation of at<'a> does an extra type checking pass over the pearlite as described in my thesis so if you ever want something like this, let me know