this month in hax: 09

content/posts/this-month-in-hax/2024-09.md

@@ -0,0 +1,77 @@
+---
+author: "Lucas Franceschino"
+title: "This month in hax: September 2024"
+date: "2024-10-01"
+tags: ["this-month-in-hax"]
+ShowToc: false
+ShowBreadCrumbs: false
+---
+
+In July, we merged 33 PRs! 🎉
+
+On the side of the frontend, [Nadrieril](https://github.com/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](https://github.com/paulmure), we
+now are able to process `unsafe` blocks. Thanks to
+[maximebuyse](https://github.com/maximebuyse), the engine can now
+rewrite more `return` expressions: we are now planning on supporting
+`return` inside loops, along with `break` and `continue`.
+
+We've been improving F* support and F* libraries. Importantly,
+[cmester0](https://github.com/cmester0) is working on a model of
+`core`, in Rust: we aim at replacing our hand-crafted F* model of core
+by an hax extraction of this new core model implemented in Rust. We
+will also be able to extract this model of core in every of our
+backends, enabling a uniform and pain-free `core` multi-backend
+library.
+
+# Merged Pull Requests
+* #934: [chore: assign an issue id for every error in the engine](https://github.com/hacspec/hax/pull/934)
+* #932: [chore: assign an issue for every error in `import_thir`](https://github.com/hacspec/hax/pull/932)
+* #919: [fix #422](https://github.com/hacspec/hax/pull/919)
+* #918: [chore: remove stale `Hax.Lib.fst`](https://github.com/hacspec/hax/pull/918)
+* #917: [doc: disambiguate_local_idents](https://github.com/hacspec/hax/pull/917)
+* #916: [update Cargo.lock](https://github.com/hacspec/hax/pull/916)
+* #909: [Revert "fix(engine/fstar): fix super typeclasses attributes"](https://github.com/hacspec/hax/pull/909)
+* #908: [fix(engine/deps): stop re-computing over and over the set of assoc items](https://github.com/hacspec/hax/pull/908)
+* #907: [Add RewriteControlFlow phase.](https://github.com/hacspec/hax/pull/907)
+* #906: [Cleanup trait resolution](https://github.com/hacspec/hax/pull/906)
+* #902: [fix(engine/fstar): fix super typeclasses attributes](https://github.com/hacspec/hax/pull/902)
+* #901: [Determine emuerate value by index](https://github.com/hacspec/hax/pull/901)
+* #898: [Fix some binder-related crashes](https://github.com/hacspec/hax/pull/898)
+* #895: [Don't eval constants eagerly](https://github.com/hacspec/hax/pull/895)
+* #894: [Detangle trait solving from `SInto`](https://github.com/hacspec/hax/pull/894)
+* #892: [Support other variants of MIR](https://github.com/hacspec/hax/pull/892)
+* #891: [fix: fstar: default trait](https://github.com/hacspec/hax/pull/891)
+* #887: [Initial cleanup of binders-related code](https://github.com/hacspec/hax/pull/887)
+* #885: [docs(book): depend on `hax-lib` only when using hax](https://github.com/hacspec/hax/pull/885)
+* #884: [Fix incorrect line numbers in error messages](https://github.com/hacspec/hax/pull/884)
+* #883: [Fix step boundaries in fold_range_step_by](https://github.com/hacspec/hax/pull/883)
+* #882: [fix(fstar-core): add support for `Option::map`](https://github.com/hacspec/hax/pull/882)
+* #880: [Support float literals](https://github.com/hacspec/hax/pull/880)
+* #877: [Avoid recursing twice on the arguments.](https://github.com/hacspec/hax/pull/877)
+* #876: [Translate additional unsafe MIR operations](https://github.com/hacspec/hax/pull/876)
+* #873: [Small PR to fix circularity in Core.Fmt.fsti](https://github.com/hacspec/hax/pull/873)
+* #872: [Pre post impl blocks](https://github.com/hacspec/hax/pull/872)
+* #870: [count-ones post-condition](https://github.com/hacspec/hax/pull/870)
+* #868: [engine: kill a few `exn` to get useful errors](https://github.com/hacspec/hax/pull/868)
+* #867: [Backend: Import unsafe code as a gated feature](https://github.com/hacspec/hax/pull/867)
+* #860: [fix(engine): make dep. analysis sensible to UID assoc. items](https://github.com/hacspec/hax/pull/860)
+* #827: [Add infos impl](https://github.com/hacspec/hax/pull/827)
+* #819: [Add Rust Core Fstar Definitions.](https://github.com/hacspec/hax/pull/819)
+
+#### Contributors
+ - [Nadrieril](https://github.com/Nadrieril)
+ - [R1kM](https://github.com/R1kM)
+ - [ROMemories](https://github.com/ROMemories)
+ - [W95Psp](https://github.com/W95Psp)
+ - [franziskuskiefer](https://github.com/franziskuskiefer)
+ - [gaetan-sbt](https://github.com/gaetan-sbt)
+ - [karthikbhargavan](https://github.com/karthikbhargavan)
+ - [mamonet](https://github.com/mamonet)
+ - [maximebuyse](https://github.com/maximebuyse)
+ - [paulmure](https://github.com/paulmure)