Lucas Franceschino

The traces are super useful for debugging the frontend. But they also are quite verbose and hard to browse. Debugging would be much easier if we had a tool to...

Add automatic invariants for functions with `&mut` inputs

8

When we translate a function with an `&mut` input, some properties can be guaranteed: for instance, mutating a slice will never change the size of the slice. I think this...

`hax_lib::fstar::options!`: accept `interface`/`both`/`impl`

5

`hax_lib::fstar::options!` is less expressive than `hax_lib::fstar::before!` or `hax_lib::fstar::after!`. Those two accept an optional argument to specify where the annotation should go. We need that on `options` (and friends) as well....

Engine: functionalize every kind of loop

4

The AST of the engine defines various kinds of loops. The phase `FunctionalizeLoops` doesn't handle every kind: - [ ] `UnconditionalLoop` - [x] `WhileLoop` - [x] `ForLoop` - [ ]...

Proof libs: `%` is modeled as an euclidian remainder while it's just a remainder

4

Basically, `(-4 % 8)` is `4` in F* but `-4` in Rust. ```rust /// Typechecks in F*. /// If you click `Share` and `Open in Rust playground`, then `Run`, you'll...