Lucas Franceschino

Coq backend: handle constructors with bases (aka `{field: expr, ..base}` in rust)

1

For now, the base is just skipped: ```rust struct Foo { a: u8, b: u8, } fn f(x: Foo) -> Foo { Foo { a: 3, ..x } } ```...

Macro inlining: doesn't work in module located in non-root file

1

This makes `merlin` not to extract (related to #28) The bug is that only the surface AST of the root `rs` file is parsed when collecting macro invocations. **Status:** I've...

Inlining of a macro call comming from another macro expansion

1

Consider the following macro [`public_bytes`](https://github.com/hacspec/hacspec/blob/00601ff65cc9a745c5191282986721d0fcb5f4f7/lib/src/array.rs#L955-L959) from the Hacspec lib: ```rust macro_rules! public_bytes { ($name:ident, $l:expr) => { array!($name, $l, u8); }; } ``` This macro is really just a helper...

Remove the linter in favor of something around https://github.com/hacspec/hax/issues/610

Quick feedback without running the whole toolchain, LSP

Currently there is no easy way of grouping recursive items from a backend. However, the feature is already implemented in module `engine/lib/dependencies.ml`. Related to that, there is https://github.com/hacspec/hax/issues/396. But this...

Attributes: introduce them in engine's AST

4

Currently, attributes are translated from the rust compiler to our THIR' JSON file, but we drop them in the module `Import_thir` in the engine. - [x] have attributes on item...

How to distribute proofs with Rust code?

1

- **Extrinsic proofs:** - the assumption here is that in an extrinsic proof model, extractions always typechecks because the program is always wrapped into a monad of exception - separate...

Add a flag `--interface-only` that sets `--interfaces "+!**"`

- [ ] in the book with multiple examples - [ ] in the CLI help (@franziskuskiefer we should look at that together, I think I'm too used to the...