This Month in Hax: June 2025
In June, we successfully merged 21 pull requests!
@Nadrieril and @N1ark continued the improvements on the frontend side with the addition of unchecked arithmetic operators (#1513), regrouping generic and trait arguments in a struct (#1514), support of trait aliases in full_def (#1494), addition of Ty::FnDef (#1487), drop calls resolution (#1467) and more.
@W95Psp, @clementblaudeau and myself worked on adding infrastructure for writing backends and compilation phases for hax in Rust (instead of Ocaml). We now have a Rust version of the hax AST and we can convert back and forth from the Ocaml version (which should allow to incrementally replace Ocaml phases by Rust phases). We also offer utilities for printing this AST when implementing backends. Our plan for the next months is to use this for the new backends we will add, and experiment with Rust phases.
Stay tuned for more updates next month!
Full list of PRs
- #1517: Update charon.yml: add
workflow_dispatch - #1514: Regroup generic and trait arguments in a struct
- #1513: Separate
{Add,Sub,Mul}Unchecked - #1510: Fix following merges changing the frontend AST
- #1507: Rust Engine: rename rust printer to rust engine
- #1506: Rust engine: Add spans to the Rust AST.
- #1505: Rust Engine: OCaml bridge for the AST (OCaml AST -> Rust AST)
- #1504: Rust Engine: transport the Rust AST to OCaml
- #1502: Upstream: Rust engine ast
- #1501: Upstream evit changes up to May 19th
- #1499: docs: Escape "" in "F" from Markdown
- #1494: full_def: support trait aliases
- #1492: sha256 example typecheck in f*
- #1491: This month in hax May 2025.
- #1490: proof-lib/fstar Add an actual instance for ordering of bound integers
- #1487: Add
Ty::FnDef - #1485: Fix detection of trait associated constants
- #1482: Update rustc pin
- #1480: Upstream evit changes up to April 25
- #1470: Add enum coverage test for coq
- #1467: Resolve Drop calls