diff --git a/content/posts/this-month-in-hax/2024-10.md b/content/posts/this-month-in-hax/2024-10.md new file mode 100644 index 0000000..9602395 --- /dev/null +++ b/content/posts/this-month-in-hax/2024-10.md @@ -0,0 +1,103 @@ +--- +author: "Maxime Buyse" +title: "This month in hax: October 2024" +date: "2024-11-04" +tags: ["this-month-in-hax"] +ShowToc: false +ShowBreadCrumbs: false +--- + +In October, we merged 70 PRs! 🎉 + +Thanks to a huge work from [Nadrieril](https://github.com/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](https://github.com/W95Psp), we now produce JSON without errors for more than 99% of Rust's top 800 crates! + +[W95Psp](https://github.com/W95Psp) worked on a new data representation for communication between the frontend and the engine. This removes redundancy and gives great performance gains. + +A new generic printer has been developed by [W95Psp](https://github.com/W95Psp) and is now available for backend development. The coq backend is the first to use it thanks to the migration work from [cmester0](https://github.com/cmester0). + +I have worked on eliminating circular dependencies between the modules we generate. And also on allowing control flow (`return`, `break` and `continue`) inside loops. + +Last but not least, the effort to release v0.1.0 is almost finished. This comes with documentation and tooling improvements. For example, [jschneider-bensch](https://github.com/jschneider-bensch) added a simple PSK based protocol as an example for the ProVerif backend. + +# Merged Pull Requests +* #1087: [Fix two query panics](https://github.com/hacspec/hax/pull/1087) +* #1084: [fix(engine/simplify_question_marks): fix type arguments on `from`](https://github.com/hacspec/hax/pull/1084) +* #1079: [Include defaulted items in `FullDefKind::TraitImpl`](https://github.com/hacspec/hax/pull/1079) +* #1077: [fix(engine) Keep late_skip attributes in bundles](https://github.com/hacspec/hax/pull/1077) +* #1074: [feat(engine): profile each phase (mem usage, time, number of items)](https://github.com/hacspec/hax/pull/1074) +* #1071: [count_ones and bool->int](https://github.com/hacspec/hax/pull/1071) +* #1069: [Add `ImplExpr` information to associated types in an impl block](https://github.com/hacspec/hax/pull/1069) +* #1067: [feat(book): allow F* extraction + TC from within the book](https://github.com/hacspec/hax/pull/1067) +* #1063: [Add module information to `FullDef`](https://github.com/hacspec/hax/pull/1063) +* #1062: [fix(engine) Remove attributes on bundle aliases and filter out NotImplementedYet.](https://github.com/hacspec/hax/pull/1062) +* #1061: [feat(frontend/consts): float lits: use strings not bits, more support](https://github.com/hacspec/hax/pull/1061) +* #1057: [fix(exporter/constants): support usize casted to raw pointers constants](https://github.com/hacspec/hax/pull/1057) +* #1056: [fix(engine) Avoid wrapping return in a tuple.](https://github.com/hacspec/hax/pull/1056) +* #1055: [Include bodies in `FullDef`](https://github.com/hacspec/hax/pull/1055) +* #1054: [Intern `DefId`s](https://github.com/hacspec/hax/pull/1054) +* #1053: [Avoid a panic in `FullDef`](https://github.com/hacspec/hax/pull/1053) +* #1052: [fix(exporter/thir): fix #1048](https://github.com/hacspec/hax/pull/1052) +* #1050: [Fix #1042](https://github.com/hacspec/hax/pull/1050) +* #1049: [fix(engine) Move variant constructors in recursive bundling.](https://github.com/hacspec/hax/pull/1049) +* #1041: [fix: rustc_private](https://github.com/hacspec/hax/pull/1041) +* #1039: [Fix 914](https://github.com/hacspec/hax/pull/1039) +* #1037: [Machine int constructors and conversions](https://github.com/hacspec/hax/pull/1037) +* #1036: [Upgrade rustc](https://github.com/hacspec/hax/pull/1036) +* #1035: [feat: check licenses](https://github.com/hacspec/hax/pull/1035) +* #1031: [Improve trait resolution](https://github.com/hacspec/hax/pull/1031) +* #1030: [Avoid bundling use items.](https://github.com/hacspec/hax/pull/1030) +* #1029: [feat: deduplicate types in haxmeta and JSON](https://github.com/hacspec/hax/pull/1029) +* #1027: [fix(frontend): this was reverted by mistake](https://github.com/hacspec/hax/pull/1027) +* #1024: [Reorganize `frontend/exporter/types`](https://github.com/hacspec/hax/pull/1024) +* #1023: [PV backend example: Simple PSK based protocol](https://github.com/hacspec/hax/pull/1023) +* #1022: [some fixes for iterators.f_next and update_at_usize](https://github.com/hacspec/hax/pull/1022) +* #1020: [Quote items track replace](https://github.com/hacspec/hax/pull/1020) +* #1018: [fix(engine/import_thir): never drop bodies of constants](https://github.com/hacspec/hax/pull/1018) +* #1015: [fix(frontend): issue #1014](https://github.com/hacspec/hax/pull/1015) +* #1012: [fix: justfile](https://github.com/hacspec/hax/pull/1012) +* #1011: [fix(engine): also rename concrete idents within a projector.](https://github.com/hacspec/hax/pull/1011) +* #1008: [Support `impl Trait` in trait resolution](https://github.com/hacspec/hax/pull/1008) +* #1007: [feat(cli): better version information](https://github.com/hacspec/hax/pull/1007) +* #1006: [Support more features](https://github.com/hacspec/hax/pull/1006) +* #1002: [Fix bug with recursive bundles depending on items from original modules.](https://github.com/hacspec/hax/pull/1002) +* #1000: [Cache `FullDef` translation and add more information to it](https://github.com/hacspec/hax/pull/1000) +* #999: [Exporter get variant information works on unions](https://github.com/hacspec/hax/pull/999) +* #996: [Cache many things](https://github.com/hacspec/hax/pull/996) +* #994: [fix: DEV.md debug engine](https://github.com/hacspec/hax/pull/994) +* #990: [Remove workaround in trait resolution for associated items](https://github.com/hacspec/hax/pull/990) +* #989: [fix(engine): make consts fun. calls of arity 0 when there is an impl expr](https://github.com/hacspec/hax/pull/989) +* #988: [feat(engine) Rewrite control flow inside loops.](https://github.com/hacspec/hax/pull/988) +* #987: [Coq generic printer](https://github.com/hacspec/hax/pull/987) +* #984: [feat: just use `just`](https://github.com/hacspec/hax/pull/984) +* #981: [Make options extensible](https://github.com/hacspec/hax/pull/981) +* #977: [More improvements to trait resolution](https://github.com/hacspec/hax/pull/977) +* #970: [Rework trait resolution to support GATs](https://github.com/hacspec/hax/pull/970) +* #969: [Release `0.1.0-alpha.1`](https://github.com/hacspec/hax/pull/969) +* #964: [feat(contributing): add a `regressions` section](https://github.com/hacspec/hax/pull/964) +* #961: [Update README.md](https://github.com/hacspec/hax/pull/961) +* #960: [feat(engine): add `ast_destruct` module](https://github.com/hacspec/hax/pull/960) +* #959: [Prefer `try_normalize_erasing_regions`](https://github.com/hacspec/hax/pull/959) +* #958: [feat(engine): add module `ast_builder`](https://github.com/hacspec/hax/pull/958) +* #957: [Ignore structs in variants renaming for bundling.](https://github.com/hacspec/hax/pull/957) +* #956: [Run `cargo clippy --fix`](https://github.com/hacspec/hax/pull/956) +* #955: [feat(frontend): collect regular comments](https://github.com/hacspec/hax/pull/955) +* #952: [feat(doc): add `CONTRIBUTING.md`](https://github.com/hacspec/hax/pull/952) +* #950: [feat(nix/utils): intro. `check-unimlemented-issue-coherency`](https://github.com/hacspec/hax/pull/950) +* #949: [fix(engine): change issue id](https://github.com/hacspec/hax/pull/949) +* #948: [fix(engine/f*): convert an unimplemented to an assertion failure](https://github.com/hacspec/hax/pull/948) +* #947: [fix(exporter+engine): drop default parameters on traits](https://github.com/hacspec/hax/pull/947) +* #945: [feat(engine/f*): allow unsafe code](https://github.com/hacspec/hax/pull/945) +* #935: [Handle cyclic module dependencies](https://github.com/hacspec/hax/pull/935) +* #851: [fix(engine): expose type of local_ident.id](https://github.com/hacspec/hax/pull/851) +* #533: [more principled generic printer](https://github.com/hacspec/hax/pull/533) + +### Contributors +* [@cmester0](https://github.com/cmester0) +* [@W95Psp](https://github.com/W95Psp) +* [@jschneider-bensch](https://github.com/jschneider-bensch) +* [@spitters](https://github.com/spitters) +* [@franziskuskiefer](https://github.com/franziskuskiefer) +* [@Nadrieril](https://github.com/Nadrieril) +* [@karthikbhargavan](https://github.com/karthikbhargavan) +* [@maximebuyse](https://github.com/maximebuyse) +* [@paulmure](https://github.com/paulmure)