Adopt Why3Find

[xldenis]

Why3 Find is finally public: https://git.frama-c.com/pub/why3find. We should integrate this into creusot to ship a complete CLI driven workflow for verification. Once we have this we should also start producing nightly binary builds of a complete creusot install to make setup 100% seamless.

[Armael]

I suggest we focus in this issue on why3find (the binary builds can be a separate issue) :).
In the meeting this morning we discussed the following approach for testing/adopting why3find progressively:

• do some quick testing, check by hand that why3find "works" with creusot at a basic level (done by @xldenis)
• integrate why3find in the creusot repo to run on our testsuite, as an additional test target. The goal is to see which subset of the tests can be solved directly by why3find.
• investigate the tests that are not solved by why3find, try to understand what additional information is needed (by comparing with the session for the test, and possibly discussing with the why3find authors to understand how they solve these kind of issues in their own workflow).
• integrate why3find in a cargo creusot user workflow. We'll probably want to replace the cargo creusot why3 prove subcommand to use why3find.
• migrate all the tests to pass with why3find. This will probably require implementing some additional syntax/features in the proof language/proof annotations used in rust files.

@xldenis could you describe here the rough steps you had to follow to use why3find with creusot, so that we can reproduce it on our side, and work on the integration with the testsuite?