v0.3.5

Changes to the Rust Engine:

• The module names now produces ExplicitDefIds instead of DefIds (#1648)
• Add a resugaring FunctionsToConstants (#1559)
• Drop the tuple nodes of the AST, add resugaring node for tuples (#1662)
• Add support for enums and structs to the Lean backend (type definitions,
  expressions, pattern-matching) (#1623)
• Update name rendering infrastructure in the Lean backend (#1623, #1624)
• Printers now emit proper diagnostics (PR #1669)
• Global identifiers are now interned (#1689)
• Global identifiers are encapsulated properly, and provide easy destructuring as tuple identifiers (#1693)
• Add support for trait and impl in the Lean backend (#1679): trait definitions, trait bounds
  on functions, impl definitions. The typeclass resolution in the generated code is left implicit
  (relies on Lean). Limited support for associated types. No support for default implementations.

Changes to the frontend:

• Add an explicit Self: Trait clause to trait methods and consts (#1559)
• Fix ImplExpr::Builtin that had some type errors (#1559)
• Improve the translation of Drop information (#1559)
• Add variance information to type parameters (#1559)
• Cleanup the State infrastructure a little bit (#1559)
• Add information about the metadata to use in unsize coercions (#1559)
• Resolve dyn Trait predicates (#1559)
• Many improvements to FullDef (#1559)
• Add infrastructure to get a monomorphized FullDef; this is used in charon to monomorphize a crate graph (#1559)
• Fix a regression affecting projection predicates (#1678)

Change to cargo-hax:

• Improve the caching of rustc when using cargo hax commands (#1719)
• Add hidden commands and flags to explicitly manipulate haxmeta files (#1722)

Changes to hax-lib:

• New behavior for hax_lib::include: it now forces inclusion when in contradiction with -i flag.
• hax-lib requires edition 2021 instead of 2024 (#1726)
• Improved VecDeque model in F* proof lib (#1728)

Changes to the Lean backend:

• Improve support for functionalized loops (#1695)

Miscellaneous:

• A lean tutorial has been added to the hax website (#1626)
• Add end-to-end tests for the website (#1690)
• Diagnostics reporting were improved (#1692)

v0.3.4

Changes to the frontend:

• A field visibility was added to HIR items (#1643)

Rust Engine:

• A Lean backend was introduced (#1593, #1591, #1590, #1607)
• The Rust engine was improved (#1624, #1603, #1600, #1585)
• The F* backend has been improved (#1587, #1585)

v0.3.1

Changes to hax-lib:

• Bug fix with PartialOrd in f* lib: #1473
• Move proof-libs into hax-lib to allow dependencies using crates.io

v0.3.0

Main changes to hax-lib:

• Support for SMT patterns in lemmas: #1428
• While loop invariants and termination (loop_decreases): #1375
• Removal of deprecated dependencies: #1385 and #1394
• Support for mathematical integers and logical propositions has been strengthened: #1372, #1352, #1351
• hax_lib::BACKEND::replace_body: #1321
• hax_lib::decreases: #1342

v0.2.0

This release brings various improvements and fixes. On the hax-lib side, the main addition is the Prop abstraction.

Intial release: v0.1.0

We're thrilled to announce that hax is entering a new era of stability and growth with the launch of our new website, a fresh start at Cryspen, and our first official release, v0.1.0!

After an intense period of research and development, hax is transitioning to a more stable phase. To support this evolution, we've moved the repository to its new home within the Cryspen GitHub organization. This change streamlines our processes and clarifies project ownership while maintaining hax's open-source nature. Cryspen is responsible for driving hax forward, but we enthusiastically welcome contributions from the community, and continue working closely with the team of existing contributors!

This move also marks our shift to a release-driven development model, culminating in our first official release, v0.1.0. While we anticipate some breaking changes in the lead-up to v1.0, detailed release notes will clearly outline any backward compatibility issues.

The state of hax

Hax currently boasts three actively used backends: (F*, Rocq and SSProve). While Cryspen primarily focuses on the F* backend, Bas Spitters and his team at the University of Aarhus are actively developing and utilizing the Rocq and SSProve backends. Cryspen also supports an experimental backend for ProVerif.

With this initial release, hax can process a significant subset of Rust code. Both the frontend, which extracts a JSON AST from the Rust compiler, and the engine, which lowers the code to the backends, have undergone major improvements and stabilization throughout 2024.

Our new website provides a central hub for all things hax. Users can explore the manual, experiment with the
interactive hax playground, and delve into a diverse collection of examples showcasing hax's capabilities.

We will work on improving the manual and developer documentation over the next few months.

Hax in Action

Over the past year, hax has proven its versatility in various projects:

• Verifying Bertie: A TLS 1.3 implementation, verified with the ProVerif backend
• Verifying ML-KEM: A post quantum cryptographic algorithm verified with the F* backend
• Verifying Smart Contracts: Leveraging the Rocq backend for enhanced security verification.

The Road Ahead

While hax can handle a substantial portion of Rust code, certain limitations remain. Features like Generic Associated Types (GATs), some Rust nightly features, specific loop and pattern structures, and a range of mutation features are not yet supported.

Detailed list of unsupported features

GATs

Support for Generic Associated Types (GATs) in the frontend is under consideration
(Issue #915)

Rust nightly features

A full list of unsupported Rust nightly features can be found with the unsupported-rust label.

Pattern

Some expressive Rust patterns are not supported yet in the hax engine.
For example, range patterns such as
0..12, as patterns such as x @ Option(_) or array or slice patterns such as [head, ..tail] are not supported.

Mutation

• Mutations inside closures are not supported (Issue #1060)
• Re-borrowing mutable refferences is not allowed (Issue #420)
• Implicit reborrowing of mutable references is not supported (Issue #419)
• User-defined functions cannot return &muts (Issue #418)
• Calling &mut-returning functions is not allowed in general (Issue #418, Issue #494 and Issue #491)
• Enum variants cannot be mutated (Issue #493)

Loops

• Unconditional loops loop {...} (Issue #124)
• While let while let .. = .. {} (Issue #113)
• Loops without side effect (Issue #405)

const inline blocks

Inline const blocks are not supported yet.
Issue #923

Parting Thoughts

This is an exciting time for hax! With our new home at Cryspen, a dedicated release model, and a growing community, we're confident that hax will continue to mature and empower developers to build secure and reliable software.

We encourage you to explore the new hax website, dive into the documentation, and experiment with the playground. Join us on this journey! Contribute to the project, share your feedback, and help us shape the future of Rust verification.

v0.1.0-alpha.1

Initial pre-release