aeneas
aeneas copied to clipboard
AeneasVerif
A verification toolchain for Rust programs
Lean supports automatic derivation of `Repr` and potential other typeclasses, it seems cheap to derive them. Question is: are there situations where a user doesn't want additional typeclasses attached to...
Example: ```rust fn match_u32(x: u32) -> u32 { match x { 0 => 0, 1 => 1, _ => 2, } } ``` gives: ```coq Definition match_u32 (x : u32)...
We need to add a header "THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS" to the copied files
In a coming PR, I will remove a duplicated test that was added to test `-backward-no-state-update`. We should add a test back to make sure we exercise all the codegen...
It's very common for code to contain asserts with custom messages, e.g.: ```rust assert!(x == 0, "must be zero"); ``` This currently leads to a crash in Aeneas, e.g.: ```...
It would make sense to do the same as https://github.com/AeneasVerif/charon/pull/356 for Aeneas
For now the backward functions can fail (they use the `Result` type). The problem comes from enumerations containing mutable borrows. For instance: ```rust fn id Option -- Here we simply...
If a global constant is defined in an implementation, we parameterize it with all the generics of the impl block (see [here](https://github.com/AeneasVerif/aeneas/blob/a5f5bf6dcfa62a4c1eefa339edd424cbfb433ec4/tests/lean/Traits.lean#L543) for instance). We should only parameterize it with...
This is a methodology employed by the Mathlib community to improve the build performance of Mathlib. The idea is to exploit the ImportGraph library which has a command `#min_imports` and...