hax & hacspec

This is the last post of this series for 2024. During this somewhat brief December, as many take time off for the holidays, we merged 21 PRs. The focus this month was largely on bug fixes, improvements, and general cleanups, with most of the work concentrated on the engine. However, a few frontend updates made their way in as well. A notable contribution from @maximebuyse introduces more consistent support for marking Rust items as opaque, establishing a unified approach to opaqueness across nearly all types of Rust items. ...

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. We also pushed various enhancements (visitors for the internal AST are generated again, we propagate some more trait generics arguments…) and bug fixes. ...