aeneas
aeneas copied to clipboard
AeneasVerif
A verification toolchain for Rust programs
```rust use std::borrow::Borrow; pub enum List { Cons(T, Box), Nil, } fn foo(v: &List) -> Option { if let List::Cons(h, t) = v { let mut t = t.borrow(); let...
Reported by Anders Larsson in the zulip: ```rust pub fn byteToWord (n: u8) -> u16 { n.into() } ``` triggers: ``` [Info ] Generated the partial file (because of errors):...
It would be good to generate warnings (depending on the backend) when: - generating recursive functions for a backend which doesn't support the fixed-point encoding, so that the user is...
The proofs in the Lean backend are a bit slow for my taste. For instance, until recently, the proofs of the hashmap and the AVL took ~200s each, which is...
Consider the following array update: ```rust a[i] = v; ``` It gets extracted to: ```lean let (_, index_mut_back) ← Array.index_mut_usize U32 16#usize a i let a1 ← index_mut_back x ```...
The debugging traces can be hard to parse. In particular, they have no structure meaning there is a lot of noise: it would be good to generate traces which have...
When debugging Aeneas, the current workflow is to manually edit Main.ml to toggle logging in different files before recompiling the project. It would be useful to be able to toggle...
