hax & hacspec

Despite some team members attending an offsite work week event, we merged 24 PRs this month. Here’s an overview of the work of the month. The frontend remained stable this month, with only a few pull requests focused on small improvements and bug fixes. Our CI now tests the extraction of Rust by Example. cmester0 is working on an annotated core library, which is extractable via hax to multiple backends. The Coq backend now uses this generated core library, and ships with an example....

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....