Lucas Franceschino

Release `v1~pre` hax

8

We should release a version of hax soon. Karthik and I were thinking about the following release calendar: two weeks after each Rust release (each six weeks). - [x] ~#639~...

CLI: improve `hax into -i '...'`

6

Currently, that `-i` flag is redundant with F*'s `--interfaces` flag. We should have a unified flag that can express a list of queries with modifiers. A query selects some items,...

This requires #145: this crate is very small and could be inlined in another one, but currently the exporter needs those types definitions.

Crates of the hax workspace: publish their doc to docs.rs

1

Currently, the Rust docs are uploaded to https://hacspec.org/hax/ along with the docs for the OCaml engine. In addition when #632 is done, we should: - [ ] have the docs...

#627 introduces a use of `mir_traits::solve_item_traits` in the extraction of types, which are common to THIR and MIR. Thus `solve_item_traits` should move out of `mir_traits.rs`. `solve_item_traits` should anyway be re-written...

Driver: call the frontend once

1

Currently: 1. `cargo-hax` calls `cargo build` with our driver, then for each selected package: a. cargo runs our driver b. the driver runs Rustc with special hooks c. we export...

Hax-lib[-macros]: `cfg(hax)`, `cfg(debug_assert)` and release mode policy

4

hax-lib and hax-lib-macros provide hax-related features that are relevant only when extracting though hax (and maybe in some scenarios in debug mode, but this is not entirely clear yet) The...

Handle `IndexMut` and `UpdateAt` in Rust

2

Currently we don't support user-defined impls of `IndexMut`. We need a way of translating `IndexMut` impls, probably as `UpdateAt` (a hax only construct).

Annotations for loop invariants

3

Requires https://github.com/hacspec/hax/issues/394

Waiting for #607 and #642 ## Links - Related to https://github.com/hacspec/hax/issues/431 - Some work done in https://github.com/hacspec/hax/tree/karthik/secret-integers