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, #1420, #1429) 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_Debuginstance foru128 - #1432: Add Instances of
Core.Fmt.t_DebugforPrims.booland 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
DefIdfor promoted constants - #1417: Add
arg_countto 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::Todomore - #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
unfoldthe 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
pastebywith_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