aeneas
aeneas copied to clipboard
AeneasVerif
A verification toolchain for Rust programs
The `access_projection` function does not exactly implement the semantics of LLBC when dereferencing a shared borrow. At [this line](https://github.com/AeneasVerif/aeneas/blob/2ad24ac2ec6eefc425250068d7caebba360871f2/compiler/InterpreterPaths.ml#L176) we should dive inside the shared value **only** if the remaining...
This triggers a bug (comes from investigating https://github.com/AeneasVerif/aeneas/issues/270 - it is a different bug): ```rust pub enum List { Cons(T, Box), Nil, } fn foo(h : &u8, mut t: &List)...
This would be more convenient to avoid having to call both Charon and Aeneas, and so that Aeneas can call Charon with the appropriate options.
there's been a bunch of improvements to `grind` lately and i wanted to try it on some aeneas generated code
@R1kM noticed that the following line should be removed: https://github.com/AeneasVerif/aeneas/blob/852977db16ae4a8fecd4597097a2d98f5bd11a18/tests/lean/lakefile.lean#L33 because otherwise `lake build` in `tests/lean` fails (the file `MutuallyRecursiveTraits.lean` is not present, and should not be), and this issue...
It often happens that `bvify` gets stuck because it is non trivial to discharge some precondition. When this happens one has to write by hand the target expression, and prove...
This is valid Rust code: ```rust fn disjoint_borrows_in_slice() { struct Test { a: i32, b: i32, } let inputs: &mut [_] = &mut [Test { a: 0, b: 0 }];...
`scalar_tac` should close automatically the following goal: ```lean example (limbs : Aeneas.Std.Array U64 5#usize) (i : U64) (i_post : i = (↑limbs : List U64)[0]!) (i4 : U64) (i4_post :...
We should keep `+`, `-`, etc. for the operations which do not fail, and that would maybe allow automatic coercions from scalars to int/nat when writing specifications.
Following the install instructions, at the `make setup-charon` step (which I had to amend to `gmake setup-charon` on macos) I get: ``` error[E0554]: `#![feature]` may not be used on the...
