aeneas
aeneas copied to clipboard
AeneasVerif
A verification toolchain for Rust programs
We can use coercion to go to integers, build a scalar out of an int via unification and let the user clear up bounds or let Lean decide them. Untested...
For now we always use the `Result` type in the output type of the functions we generate. This can make it cumbersome to prove theorems about simple functions. For instance,...
The instructions on running `make test` say: > You can also use make test and make verify to run the tests, and check the generated files. As make test will...
When running the installation instructions, I get the following error when I try to make: ``` $ gmake cd compiler && dune fmt || true Error: Program ocamlformat not found...
To avoid divergence between Charon and Aeneas, we should re-export Charon via our Flake and tell users to use this as a source of truth. Here's an appendix on how...
We should add the following test: ```rust fn foo() { while true { bar() } } ```
Today, when printing spans for external declarations we generated ugly strings, leading to noise in the generated code. For instance: ```lean /- [core::cell::{core::cell::Cell#10}::get]: Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26 Name pattern: core::cell::{core::cell::Cell}::get...
This adds pre-commit hooks for formatting, because I usually just trust whatever people prefer locally :). We could add, e.g. rustfmt, but I prefer @sonmarcho that you tell me what...
https://github.com/RaitoBezarius/avl-verification/commit/117cd1c0afbc50ffc5a90473cb4c01185188711e fails extraction with Aeneas: ``` ❯ nix run github:aeneasverif/aeneas -L -- -backend lean avl_verification.llbc [Info ] Imported: avl_verification.llbc [Info ] Generated the partial file (because of errors): ./AvlVerification.lean [Error]...