This first blog post inaugurates our series named “This Month in hax”: a series of short highlights of what happened in the development of hax and it’s ecosystem in the month.
In June, 23 PRs have been merged 🎉! The detail is available below.
On the Rust side, we have updated the Rust compiler to a very recent
nightly thanks to @Nadrieril! We also
added support for more Rust features in the frontend (dyn Trait
), more disciminant
informations on ADTs, fixed
various bugs, and improved the general experience of using hax.
We pushed many fixes for the F* backend in the engine and improved the F* proof library. We also improved the bounded integer library and it’s F* integration.
Merged Pull Requests
- Translate
dyn Trait
information - fix(engine/fstar): use
Base.String.hash
instead ofString.hash
- feat: add LICENSE
- Update rustc all at once
- refactor(engine/fstar-ast): get rid of
zarith
and GMP - Update rustc
- fix(engine/fstar): fix implicit discrepancies in traits
- feat(nix): reduce closure size for hax-engine
- Generalize bounded ints
- Don’t use strings to represent paths
- Update rustc
- fix(backends/fstar): no
__marker_trait
if parent bounds - feat(proof-libs): add
t_Default
- feat(hax): logging: enable tracing in release, add trait-related logs
- fix(exporter): disable impl expr resolution under type aliases
- fix: rename action for extracting ml-kem
- feat: isolate
DefId
: faster build times - fix(README): always begin relative path with
./
, rewrite in action - fix(ci): newer version of
ppx_deriving
(6.0.2) loops indefinitely - Update to OCaml 5
- Export discriminant values in
AdtDef
- Update README.md
- Bump rustc version