aeneas

aeneas copied to clipboard

This might prove useful: https://github.com/leanprover/lean4-nightly/releases/tag/nightly-2024-03-28

sonmarcho

If `x` is a machine integer (e.g., `U32`), Lean often displays `x` coerced to `Int` as `x.val` instead of `↑x`. This can make the proof states quite difficult to parse,...

sonmarcho

The following code makes Aeneas crash: ```rust pub trait MinimumTraitExample { const CONSTANT: u32 = 10; fn uses_self() -> u32 { Self::CONSTANT } } ``` Error: ``` Uncaught exception: (Failure...

sonmarcho

The following is currently not accepted: ```rust struct S { x : T } ```

sonmarcho

When accessing its fields, do like with tuples and deconstruct the whole structure: ```lean let (x, y, z) = t ... ```

sonmarcho

Add support for closures

1

Filing this tracking issue for closure support. Example program: ```rust fn main() { let r: Result = Ok(3); let _: Result = r.map_err(|_| 4); } ``` ```bash $ charon Compiling...

zhassan-aws

The Aeneas compiler is implemented in CPS because we need to progressively build the execution trace (which is in essence a tree with holes). The way the CPS style is...

sonmarcho

Example: The function below doesn't use its argument: ```lean def take_slice (s : Slice U32) : Result Unit := Result.ret () ``` It would be better to generate: ```lean def...

sonmarcho

sonmarcho

Add support for ADTs with lifetimes

2

Code: ```rust struct Foo

zhassan-aws