From 9ba6fc9b83b773ed4aa0e5a90d9103ecd700323d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 29 May 2024 08:00:37 +0200 Subject: Update the README --- README.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'README.md') diff --git a/README.md b/README.md index 86c1b31e..82f1da55 100644 --- a/README.md +++ b/README.md @@ -94,13 +94,11 @@ design a mechanism to allow using Aeneas in combination with tools targeting uns We have the following limitations, that we plan to address one by one: - **loops**: no nested loops for now. We are working on lifting this limitation. -- **no functions pointers/closures/traits**: ongoing work. We are actively working on this - and plan to have support soon. +- **no functions pointers/closures**: ongoing work. We have support for traits and + will have support for function pointers and closures soon. - **limited type parametricity**: it is not possible for now to instantiate a type parameter with a type containing a borrow. This is mostly an engineering - issue. We intend to quickly address the issue for types (i.e., allow `Option<&mut T>`), - and later address it for functions (i.e., allow `f<&mut T>` - we consider this to - be less urgent). + issue. - **no nested borrows in function signatures**: ongoing work. - **interior mutability**: ongoing work. We are thinking of modeling the effects of interior mutability by using ghost states. @@ -123,4 +121,7 @@ A tutorial for the Lean backend is available [here](./tests/lean/Tutorial.lean). The translation has been formalized and published at ICFP2022: [Aeneas: Rust verification by functional translation](https://dl.acm.org/doi/abs/10.1145/3547647) -([long version](https://arxiv.org/abs/2206.07185)). +([long version](https://arxiv.org/abs/2206.07185)). We also have a proof that +the symbolic execution performed by Aeneas during its translation correctly +implements a borrow checker, and published it in a +[preprint](https://arxiv.org/abs/2404.02680). -- cgit v1.2.3 From 2d8310261ac4d19bd441de271505a0f0004028b8 Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Thu, 18 Apr 2024 14:26:59 +0200 Subject: chore: explain a Nix-powered workflow 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 I do refresh of my files, which can serve as inspiration for a quick start workflow. Signed-off-by: Ryan Lahfa --- README.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'README.md') diff --git a/README.md b/README.md index 82f1da55..76d1720f 100644 --- a/README.md +++ b/README.md @@ -116,6 +116,25 @@ and tactics specialized for monadic programs (see A tutorial for the Lean backend is available [here](./tests/lean/Tutorial.lean). +## Quick start for Nix users + +Assuming Nix is installed, with a support for Flakes (`*`): + +```console +$ # Run Charon with the exact same version required by Aeneas +$ nix run github:aeneasverif/aeneas#charon -L +$ nix run github:aeneasverif/aeneas -L -- -backend your_preferred_backend your_llbc.file +``` + +To regenerate the extraction, just run step 2 and step 3 again. + +`(*)` : Flakes are not necessary, here is an example of how to do similar steps without it: + +```console +$ nix-shell '' -A packages.x86_64-linux.charon --run "charon" -I aeneas=https://github.com/AeneasVerif/aeneas/archive/main.tar.gz +$ nix-shell '' -A packages.x86_64-linux.default --run "aeneas --backend your_preferred_backend your_llbc.file" -I aeneas=https://github.com/AeneasVerif/aeneas/archive/main.tar.gz +``` + ## Formalization The translation has been formalized and published at ICFP2022: [Aeneas: Rust -- cgit v1.2.3