The State of Creusot

[xldenis]

I think it would be useful for us to discuss some important changes that need to happen to Creusot over the next few months.
For the moment we can start with a discussion thread, but it may be worthwhile to try and book a meeting with all the key contributors.

In particular there are several points which can cause churn, please voice your opinions on these:

• Organization. Creusot needs to move to a github organization, I think creusot-verif/creusot would be good but I'm open to other ideas.
• User guide. I've set up infrastructure to write a user guide, but we still need to write it!
  • It would be good for people to contribute their respective expertise to it, ie: @dewert99 as your trigger work develops it would be nice to have a few paragraphs about it
  • @voidc, similarly a page on type invariant would be super useful
• Feature flags. Setting a policy on options / flags. This isn't current a concern but I think it would be good to establish guidelines for what can be made an option to avoid a combinatorial explosion.
  I think that a reasonable attitude is that flags can be added for experiments / in development features but they should all (eventually) have a path to stabilization. ie: flags should be treated like nightly features in Rust.
• A new backend. The Why3 developers have been working on a new IVL which could be used to replace MLCFG. It has the huge advantage that we can control where abstraction barriers are inserted (if at all), and it doesn't have to be done at function level. In particular this means: closures would need no contracts, is_some would need no contract, and many contracts could be trimmed. I would like to move creusot to this new backend ASAP.
• Tech Debt. Related churn and tech debt cleanup, the CloneMap 'abstraction' has served us well but is a continual source of pain and bugs. I have a plan to eventually remove it, but that will have to wait until at least after PLDI deadlines.
  Breaking up the clone map would enable us to easily do things like generate multiple sessions from one crate (good for performance / proof stability), and would open up more flexibility in Creusot's encoding into why3, including more easily supporting mutual recursion.

If there are other points you think we should discuss and organize on, please don't hesitate to mention them.

cc @jhjourdan @voidc @dewert99 @arnaudgolfouse

[xldenis]

There's also a discussion to be had about the future direction of Creusot, what are our values, what should distinguish and guide our approach to verification. I have my ideas on this but I would be curious to hear others thoughts.

[jryans]

The Why3 developers have been working on a new IVL which could be used to replace MLCFG.

I am curious to read more about this... Are there any documents that explain this new Why3 IVL? I tried browsing around the Why3 GitLab, but there's a lot going on and I wasn't sure where to look... 😅

[xldenis]

You can look at the the coma module in our Why3 crate, additionally I believe they have submitted (or are soon submitting?) a paper on it. Soon you'll be able to see it in action as #968 transitions creusot to using it, and I can't wait for that to get merged!