creusot
creusot copied to clipboard
creusot-rs
Creusot helps you prove your code is correct in an automated fashion.
Triggers
It would probably be useful to allow uses to manually specify triggers for laws and quantifiers to help avoid matching loops. Note: Why3 already supports this https://why3.lri.fr/doc/syntaxref.html#grammar-token-triggers
Essential for leftpad verification. I guess it makes sense to interpret it as an integer from 0 to 0x10FFFF. This allows for char ranges, for example.
Right now it's impossible to compile code that parametrize on `Model`
- 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...
The following code produces a mismatched types error: ```rust fn foo() { let mut c: Ghost = ghost! { 0 }; c = ghost! { *c + 1 }; //...
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...
The intrinsic `discriminant_value` is used inside the proc macro for `Hash`, and causes it to crash. I haven't thought about why it crashes or the proper way to fix it...
Metadata
Owner
Metadata
Creusot helps you prove your code is correct in an automated fashion.