Son HO

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

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

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

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...

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...

The Makefiles are getting bloated in particular when it comes to the test generation, and are probably not the best way of managing a project like Aeneas today. It would...