aeneas
aeneas copied to clipboard
AeneasVerif
A verification toolchain for Rust programs
In many situations, reasoning about the bounds of `Usize` and `Isize` is very cumbersome (and sometimes, it leads to proof obligations that we don't know how to discharge), while reasoning...
We today have the `scalar_eq_nf` tactic to reason about *some* non-linear arithmetic goals, typically of the shape: ``` c_0 * a_0 ^ n_0 ... + c_n * a_n ^ n_n...
Many proofs are quite mechanical, especially as they follow the structure of the function under scrutinee. For instance, the *structure* of all the proofs in the tutorial could be generated...
I'm using `simp_all` a lot to do what would be given by a "congruence closure" tactic, and it would be good to have such a tactic in our toolbox. There...
We need a tactic to automatically saturate the context by instantiating assumptions of the shape `forall x y, ...` with everything they can find in the context (with maybe a...
We need to have more powerful (and efficient) tactics to simplify the context. For now, I'm relying a lot on `simp_all`, but it is slow (see [this issue](https://github.com/AeneasVerif/aeneas/issues/250) for instance)...
The `scalar_tac` tactic is heavily used as there are a lot of arithmetic proof obligations in the proofs. It can be dramatically improved, both in terms of performance and features....
Hi, the following causes Aeneas to fail ```rust fn doit(x : &mut [usize]) { x[0] += 1; } ``` with error ``` [Error] Can not apply a projection to the...
This micro pass also removes the StorageLive/StorageDead statements following: https://github.com/AeneasVerif/aeneas/pull/505
This PR does the following: - introduce many lemmas about `List`, `Array`, `Vector` and `BitVec` - introduce a new tactic `simp_scalar` to simplify arithmetic expressions - improve `zmodify` to use...