Adopt Why3Find

[xldenis]

trafficstars

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:

• [x] 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?

[Lysxia]

Commands to run why3find on all the tests (the long flag is just to turn off warnings to make the logs are more readable):

why3find config --detect --why3-warn-off unused_variable,axiom_abstract -j 8
why3find prove creusot/tests

There was a wrinkle with an old test file, which is fixed by #1147.

Ignoring the tests whose proofs we don't care about, the following test cases could not be verified by why3find prove:

why3find prove creusot/tests/should_succeed/iterators/04_skip.coma
why3find prove creusot/tests/should_succeed/iterators/05_map.coma
why3find prove creusot/tests/should_succeed/iterators/06_map_precond.coma
why3find prove creusot/tests/should_succeed/iterators/12_zip.coma
why3find prove creusot/tests/should_succeed/iterators/15_enumerate.coma
why3find prove creusot/tests/should_succeed/iterators/16_take.coma
why3find prove creusot/tests/should_succeed/iterators/17_filter.coma
why3find prove creusot/tests/should_succeed/sparse_array.coma
why3find prove creusot/tests/should_succeed/syntax/derive_macros/mixed.coma  # fixed (I don't remember why/how)

why3find prove creusot/tests/should_succeed/vector/06_knights_tour.coma # fixed in #1150 (iterator shenanigans)

why3find prove creusot/tests/should_succeed/list_reversal_lasso.coma  # fixed with longer timeout and option  --tactic +inline_goal,+split_all_full
why3find prove creusot/tests/should_succeed/sum.coma  # fixed with longer timeout and option --tactic +inline_goal

why3find prove creusot/tests/should_succeed/bdd.coma # fixed by a longer timeout
why3find prove creusot/tests/should_succeed/hashmap.coma # fixed by a longer timeout
why3find prove creusot/tests/should_succeed/heapsort_generic.coma # fixed by adding cvc
why3find prove creusot/tests/should_succeed/iterators/03_std_iterators.coma # fixed by adding cvc
why3find prove creusot/tests/should_succeed/iterators/10_once.coma  # fixed by a longer timeout
why3find prove creusot/tests/should_succeed/red_black_tree.coma # fixed by adding cvc
why3find prove creusot/tests/should_succeed/selection_sort_generic.coma   # fixed by a longer timeout
why3find prove creusot/tests/should_succeed/vector/08_haystack.coma # fixed by adding cvc

[Lysxia]

Closed by #1205 and #1255