Xavier Denis

Meeting proposal: State of formal methods tools in Rust

2

# Meeting proposal info - **Title:** The state of formal methods tools in Rust - **Type:** technical # Summary There is a nascent community of formal methods tool developers for...

Adds a specification for `[T]::iter_mut` and the associated `IterMut` type. One quirk is that where in RustHornBelt we modeled mutable iterators a sa sequence of borrows, I used a borrow...

`creusot-contracts` should be tested in CI

1

We should actually generate the MLCFG and prove all the obligations in `creusot-contracts`. At the moment everything is `#[trusted]` but we should still check.

Thanks to @jhjourdan's #376 we can actually replay complex sessions in CI, but this is still rather unfinished business. There are a few further improvements we could make which would...

Program translation IR

1

I'm introducing an IR in the translation of program code which is non-why3 specific. It serves a few purposes: - Isolating the rest of Creusot from rustc's changes - Making...

- Adds `insertion_sort` - Adds "Hillel challenge" - Adds a basic BST (too hard?)

There's a hygiene issue in the way that trait implementations declare their generics: if they overlap with the parent trait at all it can cause errors.

I just encountered an annoying error in why3 because of 'open' mutual recursion: If we define an instance of `Model` for `Box` (which makes sense to do), then the following...

Support `SizeOf` and `AlignOf` MIR instructions

4

The `SizeOf` and `AlignOf` `Rvalues` are used in the MIR generated by `vec!` having some basic support for those operations would be greatly beneficial. Specifically, we need to support the...

Currently, the default derivations for traits like `PartialEq` and `Hash` can crash creusot. We should - [ ] Provide custom derives which prove the specifications - [ ] Ensure the...