Update to toolchain 2023-06-29

[floriangru]

Hi Xavier and everyone on the Creusot team!

First of all, props to you all for making this amazing tool; I'm currently using it to verify parts of an embedded OS in rust, so thanks a lot for making Creusot! As a part of a survey/comparison, I'm trying to bring the different verification toolchains I'm using to the same rust version (which might be pointless considering how quickly the compiler is moving), so I'm trying to update Creusot to the ~latest nightly.

For now, I've only picked the low-hanging fruits. Two more are remaining :

• Take MIR dataflow analyses by mutable reference rust-lang/rust#108293 this one may need a modification into the rust compiler as the rustc_mir_dataflow::framework::cursor::AnalysisResults trait is not visible/re-exported and seems to be necessary but I'm not 100% sure;
• Simplify ImplSource candidates a bit rust-lang/rust#112687 rustc_middle::traits::ImplSource doesn't contain the Closure variant anymore, looks doable though.

I'll try to finish at least the ImplSource issue in this PR, but if you can do it more quickly than me (as I'm not familiar with the creusot codebase), don't hesitate of course!

(forgot to add in the commit message that it's patching also:

• Add -Ztrait-solver=next-coherence rust-lang/rust#112122;
• (Vec|LinkedList)::drain_filter feature renamed into (...)::extract_if (tracking issue : Tracking issue for Vec::extract_if and LinkedList::extract_if rust-lang/rust#43244, didn't find the incriminating PR yet))

Cheers

(I'm sorry if this is too verbose, I can trim it down if necessary)

[xldenis]

Hi @floriangru thanks for the contribution and interest. I'll try to take a look at the toolchain update and see what's missing.

Additionally, if you feel like there are missing features (there are many), please let us know so we can see if its something we can easily add.

[floriangru]

Only one issue remaining in creusot/src/extended_location.rs, patched by re-exporting the necessary trait (AnalysisResults) in rust-lang/rust#113089. Should be in the next rollup if I understand correctly.

Additionally, if you feel like there are missing features (there are many), please let us know so we can see if its something we can easily add.

Would do :)

[xldenis]

Seems like it should be possible to bump the nightly and get this merged now!

[floriangru]

Seems like it should be possible to bump the nightly and get this merged now!

Hi, sorry for letting this drag on. It's done now, but I'm not really happy with that since it shuffled a bit the translation and adds a lot of noise. If I bless the updated test cases, that'll modify 1588 lines for nothing (number changed in auto generated ids in the .mlcfg files).
And it appears to break the proof for heapsort_generic. It makes the one for red_black_tree obsolete but at least I managed to fix it; that wasn't the case (at least trivially) for heapsort. I haven't committed these changes to keep this PR readable.

[floriangru]

Also, now targeting toolchain nightly-2023-06-29.

[xldenis]

I've gone ahead and refreshed the sessions fixing the two broken tests. (Just needed to be more thoroughly updated).

[floriangru]

I've gone ahead and refreshed the sessions fixing the two broken tests. (Just needed to be more thoroughly updated).

Hi, thanks Xavier ! I was worried this would cause too much noise in the commits; next time I'll contribute I'll push the generated tests :)