diff --git a/docs/blog/posts/this-month-in-hax/2025-01.md b/docs/blog/posts/this-month-in-hax/2025-01.md new file mode 100644 index 000000000..e369dc161 --- /dev/null +++ b/docs/blog/posts/this-month-in-hax/2025-01.md @@ -0,0 +1,79 @@ +--- +authors: + - lucas +title: "This Month in Hax: January 2025" +date: 2025-02-10 +--- + + +This blog post continues our ongoing series introduced in the [previous blog of +hax](https://hacspec.org/blog/tags/this-month-in-hax/), a monthly collection of +highlights showcasing key developments in hax and its ecosystem. + +This month, we merged **31 pull requests** and celebrated a major milestone by +releasing the first official version of hax: +[v0.1.0](https://github.com/cryspen/hax/releases/tag/cargo-hax-v0.1.0). If you +haven’t already, be sure to check out [our blog post](../announce-v0.1.md) for +more details on this release! + +We tackled a variety of bug fixes and engine improvements. One significant +achievement was resolving a long-standing issue related to the inconsistent +preservation of declaration orders between Rust and the extractions. This +problem [was finally fixed](https://github.com/cryspen/hax/pull/1247). 🎉 + +Additionally, we merged [a comprehensive +overhaul](https://github.com/cryspen/hax/pull/1199) of how identifiers are +treated and represented within the engine. This rework allowed us to fix nearly +ten related issues, making the system more robust and efficient. + +In the F\* backend, we transitioned away from using +[HACL\*](https://github.com/hacl-star/hacl-star) machine integers. Instead, we +now rely on a [thin wrapper](https://github.com/cryspen/hax/pull/1238) over +F\*'s native mathematical integers. Unlike HACL\*'s opaque machine integers, +this new representation allows us to use F\*'s normalizer freely, offering a +cleaner and more lightweight solution. + +Stay tuned for more updates in the coming months! + +### Full list of PRs + +* \#1278: [ci(gha): drop magic-nix-cache action because of EOL](https://github.com/cryspen/hax/pull/1278) +* \#1277: [fix(mkdocs): use codemirror instead of ace, re-setup on page reload](https://github.com/cryspen/hax/pull/1277) +* \#1275: [Create CODEOWNERS](https://github.com/cryspen/hax/pull/1275) +* \#1273: [Various F* core lib additions.](https://github.com/cryspen/hax/pull/1273) +* \#1267: [fix(hax-lib/macros): handle correctly `&mut Self` arguments in `ensures`](https://github.com/cryspen/hax/pull/1267) +* \#1265: [Fix announce-v0.1.md](https://github.com/cryspen/hax/pull/1265) +* \#1263: [updatge readme and docs](https://github.com/cryspen/hax/pull/1263) +* \#1261: [Update website landing page](https://github.com/cryspen/hax/pull/1261) +* \#1260: [chore(deps): bump hashbrown from 0.15.0 to 0.15.2](https://github.com/cryspen/hax/pull/1260) +* \#1259: [changelog: initialize](https://github.com/cryspen/hax/pull/1259) +* \#1258: [Delete frontend/exporter/json-visualizer directory](https://github.com/cryspen/hax/pull/1258) +* \#1247: [Stable topological sort using original order.](https://github.com/cryspen/hax/pull/1247) +* \#1245: [Release hax v0.1.0](https://github.com/cryspen/hax/pull/1245) +* \#1241: [hax v0.1 blog post](https://github.com/cryspen/hax/pull/1241) +* \#1238: [Transparent integers](https://github.com/cryspen/hax/pull/1238) +* \#1237: [Fix order of `Call` trait clauses](https://github.com/cryspen/hax/pull/1237) +* \#1236: [Add more info to `ImplExprAtom::Builtin`](https://github.com/cryspen/hax/pull/1236) +* \#1230: [fix(engine) Propagate return rewrite to avoid crash in side_effect_utils](https://github.com/cryspen/hax/pull/1230) +* \#1229: [fix(engine) Add type arguments for associated constants.](https://github.com/cryspen/hax/pull/1229) +* \#1228: [fix(engine) Use ocamlgraph fork to fix missing rec bug.](https://github.com/cryspen/hax/pull/1228) +* \#1225: [Hax home page using mkdocs](https://github.com/cryspen/hax/pull/1225) +* \#1223: [fix(engine) Attempt to fix double return bug.](https://github.com/cryspen/hax/pull/1223) +* \#1222: [Make predicate handling a bit more consistent](https://github.com/cryspen/hax/pull/1222) +* \#1220: [Visit trait goals to rename impl expr they may contain.](https://github.com/cryspen/hax/pull/1220) +* \#1216: [Update README.md: `unsafe` is OK to use](https://github.com/cryspen/hax/pull/1216) +* \#1215: [Fix generics handling for function calls](https://github.com/cryspen/hax/pull/1215) +* \#1212: [fix(CI) Update F* version to fix mlkem CI job ](https://github.com/cryspen/hax/pull/1212) +* \#1206: [fix(engine) Make sub-parts of `Quote` visited by visitors](https://github.com/cryspen/hax/pull/1206) +* \#1199: [Engine: rework global name representation](https://github.com/cryspen/hax/pull/1199) +* \#1075: [Move trait methods in cyclic dependencies bundling.](https://github.com/cryspen/hax/pull/1075) +* \#1066: [Add EBNF for AST to book](https://github.com/cryspen/hax/pull/1066) + +### Contributors +* [@Nadrieril](https://github.com/Nadrieril) +* [@W95Psp](https://github.com/W95Psp) +* [@app/dependabot](https://github.com/app/dependabot) +* [@cmester0](https://github.com/cmester0) +* [@franziskuskiefer](https://github.com/franziskuskiefer) +* [@karthikbhargavan](https://github.com/karthikbhargavan) +* [@maximebuyse](https://github.com/maximebuyse)