Add Prusti-ish frontend to Creusot

[dewert99]

This PR is an implementation of the Prusti to Creusot translation described in my thesis.

The Prusti style specifications are contained in use creusot_contracts::prusti_prelude, which has its own version of requires, ensures, logic and ghost.

[xldenis]

This is very impressive work, and I think there's value in preserving (and expanding) on your thesis work, but I'm not sure we want to merge things in this current state. My issue is that it's a significant chunk of work that we don't have the expertise to maintain without you, especially as I'm looking to take a step back and allow others to take the lead on Creusot's development.

However, I do have a proposal which may help maintain both objectives: would it be possible to make creusot-prusti a separate frontend for Creusot? If we can split this into two parts of work: API changes to creusot the library and a new frontend I'm hoping we can keep the complexity split cleaner and lower the entanglement.

I hope I don't sound too ungrateful, and I hope that we can find a way to maintain your work without overwhelming the other Creusot developers.

[dewert99]

I've tried to keep the entanglement relatively low, the creusot::prusti module only depends on the rest of creusot for its error type so it would be fairly easy to extract it into its own crate if that would help. creusot::translation::pearlite::prusti depends on the creusot::translation::pearlite::Term type since it is easier to traverse than raw THIR. The changes I made to existing files in creusot mostly exist to improve the ty field of creusot::translation::pearlite::Term function calls to remember lifetimes that were specified by the use (eg. at::<'a>) and whether they used to be references or boxes (and then undoing these changes when lowering the creusot::translation::pearlite::Term). I could try move these changes to a separate PR but I'm not sure how that would help with maintainability.

I could also try to rewrite creusot::translation::pearlite::prusti to operate over THIR instead of creusot::translation::pearlite::Term which would allow me to also move creusot::translation::pearlite::prusti into a separate crate and revert most of the changes I made in creusot::translation::pearlite and creusot::backend:term but this would be more work.

Whatever I end up doing there still will be the maintenance burden caused by updating the rustc version since its API is unstable and my frontend would need to use the same rustc version as the rest of Creusot.

[xldenis]

I've tried to keep the entanglement relatively low, the creusot::prusti module only depends on the rest of creusot for its error type so it would be fairly easy to extract it into its own crate if that would help.

I noticed that and I think that would be a good idea. What I'm imagining is that since we will be moving Creusot to an org, we could make creusot-prusti an alternative binary with its own repo in that organization, using creusot-lib as a dependency. This would allow the two to evolve at different rates: they wouldn't be required to move in strict lockstep.

The changes I made to existing files in creusot mostly exist to improve the ty field of creusot::translation::pearlite::Term function calls to remember lifetimes that were specified by the use (eg. at::<'a>)

I think these can be merged uncontroversially.

Whatever I end up doing there still will be the maintenance burden caused by updating the rustc version since its API is unstable and my frontend would need to use the same rustc version as the rest of Creusot.

That's not really the maintainance burden I was worried about; that's an unchangeable cost, I'm referring more that any changes to Pearlite or Creusot's translation could break the prusti specifications in an unknown manner which no one might have.

Another possible outcome is to ask ourselves: is there a way we could fold some of this work directly into mainline Pearlite? Could we use at as a generalization of ^? Could we use parts of this to build an after_expiry mechanism that works with standard Pearlite? Are there changes to mainline Pearlite we could make which would make building and maintaining a Prusti-style frontend language simpler?

[dewert99]

Another possible outcome is to ask ourselves: is there a way we could fold some of this work directly into mainline Pearlite? Could we use at as a generalization of ^? Could we use parts of this to build an after_expiry mechanism that works with standard Pearlite? Are there changes to mainline Pearlite we could make which would make building and maintaining a Prusti-style frontend language simpler?

The syntax for the Prusti frontend is essentially Pearlite with some builtin functions (like at) and traits that have special semantics. The majority of the work done by the Prusti front-end is deciding which mutable de-references should be replaced with final operators, as well as rejecting programs that do not have well-defined Prusti semantics. Doing this depends on the rust type-checker to eg. find which lifetimes are blocked, check if types are Copy, normalize associated types and type aliases.

That's not really the maintainance burden I was worried about; that's an unchangeable cost, I'm referring more that any changes to Pearlite or Creusot's translation could break the prusti specifications in an unknown manner which no one might have.

I think I understand, unfortunately maintaining a separate front-end has its own difficulties. At least cargo-creusot, creusot-rustc, creusot_contracts and creusot_contracts_proc would all need Prusti front-end versions, and we would need to extract a library out of creusot_contracts_proc since most of the Prusti version would be the same. The Prusti front-end would probably need to use git dependencies to depend on various creusot crates and would need to be updated semi-frequently just to chage the commit of the dependecies (or just pin to main and then risk breaking if Creusot switches its rustc version). Prusti logic functions also have more information in the signatures that Creusot logic functions, so it would be useful to add Prusti specific attributes to some of the logic functions in creusot-contracts although they might seem out of place if the creusot repo otherwise knew nothing about the Prusti frontend.

[dewert99]

@xldenis this is the issue I was referring to in #972

[dewert99]

It is generated from here