Merge pull request #1330 from cryspen/this-month-in-hax-02-25

This month in hax 02-25 + release 0.2.0

Author: W95Psp

Cargo.lock

@@ -32,7 +32,7 @@ default-members = [
 resolver = "2"
 
 [workspace.package]
-version = "0.1.0"
+version = "0.2.0"
 authors = ["hax Authors"]
 license = "Apache-2.0"
 homepage = "https://github.com/hacspec/hax"
@@ -71,14 +71,14 @@ colored = "2"
 annotate-snippets = "0.11"
 
 # Crates in this repository
-hax-frontend-exporter = { path = "frontend/exporter", version = "=0.1.0", default-features = false }
-hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.1.0" }
-hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.1.0" }
-hax-lib-macros = { path = "hax-lib/macros", version = "=0.1.0" }
-hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.1.0" }
-hax-lib = { path = "hax-lib", version = "=0.1.0" }
-hax-engine-names = { path = "engine/names", version = "=0.1.0" }
-hax-types = { path = "hax-types", version = "=0.1.0" }
+hax-frontend-exporter = { path = "frontend/exporter", version = "=0.2.0", default-features = false }
+hax-adt-into = { path = "frontend/exporter/adt-into", version = "=0.2.0" }
+hax-frontend-exporter-options = { path = "frontend/exporter/options", version = "=0.2.0" }
+hax-lib-macros = { path = "hax-lib/macros", version = "=0.2.0" }
+hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.2.0" }
+hax-lib = { path = "hax-lib", version = "=0.2.0" }
+hax-engine-names = { path = "engine/names", version = "=0.2.0" }
+hax-types = { path = "hax-types", version = "=0.2.0" }
 
 [workspace.metadata.release]
 owners = ["github:hacspec:crates"]

Cargo.toml

@@ -0,0 +1,62 @@
+---
+authors:
+  - lucas
+title: "This Month in Hax: February 2025"
+date: 2025-03-05
+---
+
+In February, we merged **23 pull requests**!
+
+The MIR translation of the frontend was improved by
+[@Nadrieril](https://github.com/Nadrieril): some bugs were fixed, and our
+handling of constants have been improved and is now more robust. 
+
+One of the major updates this month was the introduction of a new
+[`Prop` abstraction](https://github.com/cryspen/hax/pull/1301) in `hax-lib`,
+which enhances expressiveness in property-based reasoning within the Hax
+engine. With `Prop`, it is now possible to write non-computable properties that leverage universal quantifiers.
+
+We also made significant progress in the engine, including fixing issues
+related to [`continue` handling in loops](https://github.com/cryspen/hax/pull/1296) 
+and ensuring proper naming and disambiguation in bundled components 
+([#1280](https://github.com/cryspen/hax/pull/1280), [#1286](https://github.com/cryspen/hax/pull/1286)).
+
+We also tackled improvements in the F\* backend, such as fixing trait
+inheritance in `rand-core` ([#1322](https://github.com/cryspen/hax/pull/1322)) and 
+expanding the core library ([#1292](https://github.com/cryspen/hax/pull/1292)).
+
+Stay tuned for more updates in the coming months!
+
+### Full list of PRs
+
+* \#1325: [mkdocs: add Maxime description](https://github.com/cryspen/hax/pull/1325)
+* \#1322: [Proof libs (F*): fix trait inheritance in rand-core](https://github.com/cryspen/hax/pull/1322)
+* \#1320: ['hax for everyone' blog post.](https://github.com/cryspen/hax/pull/1320)
+* \#1319: [Translate less data in MIR](https://github.com/cryspen/hax/pull/1319)
+* \#1318: [ Not all evaluated MIR constants are byte strings](https://github.com/cryspen/hax/pull/1318)
+* \#1317: [Avoid an ICE by matching on type earlier](https://github.com/cryspen/hax/pull/1317)
+* \#1312: [full_def: no need to normalize clauses eagerly anymore](https://github.com/cryspen/hax/pull/1312)
+* \#1309: [full_def: group generic and predicates into a common struct](https://github.com/cryspen/hax/pull/1309)
+* \#1307: [update website landing page](https://github.com/cryspen/hax/pull/1307)
+* \#1306: [init(docs/blog): this month in hax: January](https://github.com/cryspen/hax/pull/1306)
+* \#1305: [fix(engine) Fix question marks simplification with deref/borrow.](https://github.com/cryspen/hax/pull/1305)
+* \#1304: [feat(manual): hax-playground integration: use latest `main`](https://github.com/cryspen/hax/pull/1304)
+* \#1303: [fix(engine) Fix return inside closure.](https://github.com/cryspen/hax/pull/1303)
+* \#1302: [Engine: fix implicit representation for enums](https://github.com/cryspen/hax/pull/1302)
+* \#1301: [`hax-lib`: introduce a `Prop` abstraction](https://github.com/cryspen/hax/pull/1301)
+* \#1296: [fix(engine) Fix loops with `continue` and no `return`/`break`](https://github.com/cryspen/hax/pull/1296)
+* \#1293: [fix(engine) Add const parameter for assoc const of parametric impl.](https://github.com/cryspen/hax/pull/1293)
+* \#1292: [Additions and corrections in F* core lib.](https://github.com/cryspen/hax/pull/1292)
+* \#1286: [fix(engine) Fix naming bundle regression](https://github.com/cryspen/hax/pull/1286)
+* \#1284: [fix(engine) Make sure origins are renamed in bundles.](https://github.com/cryspen/hax/pull/1284)
+* \#1282: [Update CI dependencies](https://github.com/cryspen/hax/pull/1282)
+* \#1281: [Library additions for ML-DSA verification](https://github.com/cryspen/hax/pull/1281)
+* \#1280: [fix(engine) Add default case for disambiguation of bundle element names](https://github.com/cryspen/hax/pull/1280)
+
+### Contributors
+* [@Nadrieril](https://github.com/Nadrieril)
+* [@W95Psp](https://github.com/W95Psp)
+* [@franziskuskiefer](https://github.com/franziskuskiefer)
+* [@karthikbhargavan](https://github.com/karthikbhargavan)
+* [@maximebuyse](https://github.com/maximebuyse)
+

docs/blog/posts/this-month-in-hax/2025-02.md

@@ -2,7 +2,7 @@
 
 (name hax-engine)
 
-(version 0.1.0)
+(version 0.2.0)
 
 (generate_opam_files true)
 

engine/dune-project

@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "0.1.0"
+version: "0.2.0"
 synopsis: "The engine of hax, a Rust verification tool"
 description:
   "Hax is divided in two: a frontend (written in Rust) and an engine (written in OCaml). This is the engine."