This Month in Hax: April 2025
In April, we successfully merged 38 pull requests!
Thanks @Nadrieril, for pinning a more recent nightly version of the Rust compiler (#1391). Nadrieril also continued making the frontend more robust and complete with work on constants #1402 and item's children (#1412).
@W95Psp worked on hax-lib
with improved support for writing f* lemmas in rust (#1428), and fstar post-processing with tactics (#1437).
I worked on while loops which now support invariants and variants (to prove termination) in #1375
We also worked on various improvements like removing deprecated dependencies used by hax-lib (#1385 and #1394), some ProVerif backend workarounds by @jschneider-bensch (#1360, #1401 and #1406), and multiple f* core lib additions.
Stay tuned for more updates next month!
Full list of PRs
- #1437: feat(hax_lib/macros): F*: add
postprocess_with
- #1436: Silence unused inputs in lemmas
- #1435: Add
t_Debug
instance foru128
- #1432: Add Instances of
Core.Fmt.t_Debug
forPrims.bool
and pairs - #1430: Fix range loops for empty ranges.
- #1429: Translate evaluated closure constants
- #1428: feat(hax-lib&backend): F*: support for SMT patterns
- #1427: feat(proof-libs): add
impl_i32__wrapping_sub
- #1422: Barrett example tutorial
- #1420: Add a fake
DefId
for promoted constants - #1417: Add
arg_count
to MIR bodies - #1416: fix(engine) Fix name clashes for functions defined in impl methods.
- #1415: fix(proof-libs): give a computable definition to
>>
- #1414: Use
ConstantExprKind::Todo
more - #1413: feat(justfile):
just expand
: always use nightly - #1412: full_def: Add helper to explore an item's children
- #1410: Typeclass for
BitAnd
; Instantiations forPrims.bool
- #1409: Libs needed for Bertie
- #1408: feat(fstar/proof-libs): add a lemma for simplifying double casts
- #1406: [ProVerif] Match arm type error workaround
- #1404: feat(backends/fstar): make
unfold
the opaque proxy functions - #1402: Improve support for getting constant bodies
- #1401: [ProVerif] Match arm type workaround
- #1395: Put macro_metavar_expr_concat feature under hax cfg.
- #1394: Replace
paste
bywith_builtin_macros
. - #1393: Tell crane to keep references to the rust toolchain
- #1391: Update the rustc pin
- #1390: Revert #1377
- #1389: Cut ASTs printed in errors when they are too long.
- #1388: Remove AST printing in import_thir errors.
- #1385: Switch to proc-macro-error2 because original is unmaintained.
- #1384: Remove deprecated macro parsing infrastructure
- #1381: feat(docs/blog): this month in hax 03 2025
- #1375: Add invariants for while loops.
- #1368: feat(blog): add blog post about the rework of names
- #1360: [PV] Generate consistent field accessor names
- #1340: Add logor_disjoint to Rust_primitives.Integers
- #808: Fix dependencies bounded integers