hax & hacspec

In October, we merged 70 PRs! 🎉 Thanks to a huge work from Nadrieril on trait resolution, the goal of handling all valid Rust code with hax frontend is now almost achieved. With these improvements and some bugfixes from W95Psp, we now produce JSON without errors for more than 99% of Rust’s top 800 crates! W95Psp worked on a new data representation for communication between the frontend and the engine. This removes redundancy and gives great performance gains....

In July, we merged 33 PRs! 🎉 On the side of the frontend, Nadrieril and I worked at making hax handling of binders (e.g. 'a in for<'a> &'a T: PartialEq<i32>) and traits better. This is not finished yet, but we made great progress. Our goal is to make the frontend work on every valid Rust code. In the engine, thanks to paulmure, we now are able to process unsafe blocks. Thanks to maximebuyse, the engine can now rewrite more return expressions: we are now planning on supporting return inside loops, along with break and continue....

In July, we merged 32 PRs! 🎉 On the side of the frontend and CLI, we had a lot of fixes and improvements! The hax command line and rustc driver were refactored, allowing for better scaling and caching. We also improved the general ergonomics: diagnostics can now be output in JSON, we have improved error messages… And we pushed various bug fixes. In the engine, we now resugar asserts properly and support dyn....

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 have been applying hax to verify several Rust pieces of software recently. hax was used to verify Libcrux’s implementation of ML-KEM with F*, but also for smart contracts verification with Coq, and even on protocols with F* and our new ProVerif backend. Meanwhile, we also presented hax at several conferences and workshops. The need for more documentation and guidance was becoming apparent: it was about time to have a tutorial!...