This Month in Hax: July 2025
In July, we successfully merged 32 pull requests!
@Nadrieril made sure that we use a recent version of rustc (PR #1534) and made new improvements to trait resolution in the frontend (PR #1522).
We continued efforts to improve the usability of hax with several f* core lib additions, and improvements to the CI.
More importantly, @W95Psp, @clementblaudeau and myself worked on improvements of the new hax engine implemented in Rust (PR #1508, #1518, #1525 and #1526).
Finally, let's celebrate the arrival of our new backend for lean (PR #1509)! @clementblaudeau is taking the lead on this project. This backend is implemented in Rust using our new infrastructure. It is still under active development and many improvements will come in the next couple of months.
Stay tuned for more updates next month!
Full list of PRs
- #1587: Fix inconsistent field naming in marker traits.
- #1583: fix(fstar-backend) Add hint for type class resolution with inheritance
- #1581: Regen code
- #1576: feat(ci/mlkem): make job work with merge queues
- #1575: fix(ci/mlkem): clone twice
- #1574: feat(ci): mlkem job: use specific libcrux revision
- #1572: fix(lib) Fix _super hashes for Cmp traits.
- #1570: Frontend: Fix regression #1566
- #1562: Local hax lib for ml kem ci
- #1561: Check rust formatting with 'cargo fmt'.
- #1558: chore(ci/gh actions):
ubuntu-20.04->ubuntu-22.04 - #1557: Fix typo in properties.md
- #1556: Nix: un-pin ocamlgraph
- #1552: fix Core.Clone
- #1549: Delete .github/workflows/engine_js_build.yml
- #1548: Fix type of u64 rotate left
- #1546: This month in hax June 2025.
- #1545: fix(nix): make
nix runwork on darwin - #1544: fix(setup.sh): install Rust engine
- #1540: chore(rengine/lean): fix warnings
- #1535: Fix typo: frontent -> frontend
- #1534: Update rustc to latest nightly
- #1533: feat(hax-lib):
int!: support hex, octal and binary literals - #1526: Rust Engine: expose common
DefIds in the Rust engine - #1525: Rust Engine: allow multiple backends to implement the
Prettytrait - #1523: Release 0.3.2
- #1522: Don't erase inner binders in trait resolution
- #1520: Addition of integer function implementations in Core.Num.fsti, along with generic functions in Rust_primitives.Integer.fsti to support them.
- #1518: Rust Engine: intro. resugared AST fragment
- #1509: Lean backend [Part 1/3]
- #1508: Rust Engine: turn it into a hax-frontend compatible engine
- #1466: Proof lib/fstar support more rbe