aeneas
aeneas copied to clipboard
AeneasVerif
A verification toolchain for Rust programs
MWE: ```rust fn bar(a: &mut bool) { } fn foo(s: &mut bool) { let mut a = *s; while 0 < 0 { bar(&mut a); } *s = a; }...
When defining a `usize` constant in Rust initialized by a constant expression, `eval_global` fails to prove that the computation doesn't fail. MWE: ```rust const W: usize = 0 + 0;...
On an unmodified Lean environment, the following `foo.rs` extracts, but the definitions run into `maximum depth exceeded problems. foo.rs const W: [u64; 162] = [ 0xfdf43de1ad133931, 0x7b3072a3b39b6df8, 0x413d1ffe14269cb3, 0x34c891c87128c954, 0x2ede7218bb0023d3,...
The following example works. ```lean @[simp_lists_simps] theorem foo[Inhabited α](ls: List α)(i_idx: 0 < ls.length) : ls[0]! = ls.head! := by cases ls simp example[Inhabited α](ls: List α)(i: Nat)(i_idx: i <...
We need to update `PureTypeCheck` so that it is more complete. Also, if we set `Config.type_check_pure_code` to `true` the type checker detects type checking errors in the tests.
Since we're currently using `Aesop`'s `addTryThisTacticSeqSuggestion` function, the prompt makes it seem like the suggestion is coming from the Aesop tactic. https://github.com/AeneasVerif/aeneas/blob/0c87ae52b7963acabb8d487bd55e573ff56a94f6/backends/lean/Aeneas/Progress/ProgressStar.lean#L365-L369 
Consider the following code ```rust fn example(a: bool, b: bool) -> bool{ a & &b } ``` This code is extracted to ```lean -- THIS FILE WAS AUTOMATICALLY GENERATED BY...
Lean complains about some functions using definitions marked as `axiom`s by Aeneas, since they are not marked as `noncomputable`. ___ Consider the following snippet ```rust // foo.rs fn foo (){...
Minmimzed example: ```rust fn example() { let _ = vec![()]; } ``` Error generated: ``` [Error] Invalid input for unop Source: '/rustc/library/alloc/src/macros.rs', lines 54:12-54:46 ```