This Month in Hax: February 2025
In February, we merged 23 pull requests!
The MIR translation of the frontend was improved by @Nadrieril: some bugs were fixed, and our handling of constants have been improved and is now more robust.
One of the major updates this month was the introduction of a new
Prop
abstraction in hax-lib
,
which enhances expressiveness in property-based reasoning within the Hax
engine. With Prop
, it is now possible to write non-computable properties that leverage universal quantifiers.
We also made significant progress in the engine, including fixing issues
related to continue
handling in loops
and ensuring proper naming and disambiguation in bundled components
(#1280, #1286).
We also tackled improvements in the F* backend, such as fixing trait
inheritance in rand-core
(#1322) and
expanding the core library (#1292).
Stay tuned for more updates in the coming months!
Full list of PRs
- #1325: mkdocs: add Maxime description
- #1322: Proof libs (F*): fix trait inheritance in rand-core
- #1320: 'hax for everyone' blog post.
- #1319: Translate less data in MIR
- #1318: Not all evaluated MIR constants are byte strings
- #1317: Avoid an ICE by matching on type earlier
- #1312: full_def: no need to normalize clauses eagerly anymore
- #1309: full_def: group generic and predicates into a common struct
- #1307: update website landing page
- #1306: init(docs/blog): this month in hax: January
- #1305: fix(engine) Fix question marks simplification with deref/borrow.
- #1304: feat(manual): hax-playground integration: use latest
main
- #1303: fix(engine) Fix return inside closure.
- #1302: Engine: fix implicit representation for enums
- #1301:
hax-lib
: introduce aProp
abstraction - #1296: fix(engine) Fix loops with
continue
and noreturn
/break
- #1293: fix(engine) Add const parameter for assoc const of parametric impl.
- #1292: Additions and corrections in F* core lib.
- #1286: fix(engine) Fix naming bundle regression
- #1284: fix(engine) Make sure origins are renamed in bundles.
- #1282: Update CI dependencies
- #1281: Library additions for ML-DSA verification
- #1280: fix(engine) Add default case for disambiguation of bundle element names