Merge branch 'main' into prop-predicates

cryspen · Feb 19, 2025 · 908f653 · 908f653
2 parents 927c221 + ce2ea4b
commit 908f653
Show file tree

Hide file tree

Showing 26 changed files with 1,812 additions and 298 deletions.
diff --git a/docs/blog/posts/this-month-in-hax/2025-01.md 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)
diff --git a/docs/index.md b/docs/index.md
@@ -1,6 +1,18 @@
-# Welcome to hax
+# hax
 
 hax is a tool for high assurance translations of a large subset of
 Rust into formal languages such as [F\*](https://www.fstar-lang.org/) or [Rocq](https://rocq-prover.org/).
 
-Head over to the [Manual](./manual/index.md) to get started!
+Head over to the [Manual](./manual/index.md) or the [playground](https://hax-playground.cryspen.com)
+to get started!
+
+![hax overview](static/img/overview.png)
+
+## Playground
+Try out hax in the browser on the [playground](https://hax-playground.cryspen.com).
+
+[![Playground screenshot](static/img/playground.png)](https://hax-playground.cryspen.com)
+
+## Community
+
+Join the hax community on our [Zulip chat](https://hacspec.zulipchat.com).
diff --git a/docs/javascripts/hax_playground.js b/docs/javascripts/hax_playground.js
@@ -1,5 +1,13 @@
+const PLAYGROUND_URL = 'https://hax-playground.cryspen.com';
+
+// Fetches the commit hash for latest `main` of hax
+async function get_latest_hax_main() {
+    let commits = await (await fetch(PLAYGROUND_URL + '/git-refs')).text();
+    return commits.match(/(.*);refs\/remotes\/origin\/main;/).pop();
+}
+
 // Call into the API of the hax playground
-function call_playground(result_block, query, text) {
+async function call_playground(result_block, query, text) {
     let raw_query = async (API_URL, hax_version, query, files, on_line_received) => {
         let response = await fetch(`${API_URL}/query/${hax_version}/${query}`, {
             method: "POST",
@@ -24,14 +32,13 @@ function call_playground(result_block, query, text) {
                 on_line_received(line);
         }
     };
-    let hax_version = '5ca1c13023200dee0cca6237901a3b5a69ad345a';
-    let playground_url = 'https://hax-playground.cryspen.com';
     let ansi_up = new AnsiUp();
     let first = true;
     let logs = document.createElement('div');
     logs.style = 'font-size: 80%; background: #00000010; padding: 3px;';
+    let hax_version = await get_latest_hax_main();
     raw_query(
-        playground_url,
+        PLAYGROUND_URL,
         hax_version,
         query,
         [['src/lib.rs', text]],
@@ -75,7 +82,7 @@ function call_playground(result_block, query, text) {
                     result_block.innerHTML += '<div style="float: left; padding: 3px; padding-top: 8px; position: relative; top: 6px;"><span style="color: gray;">Status: </span><span style="color: green">✓ F* successfully typechecked!</span></div>';
                 }
                 hljs.highlightBlock(result);
-                result_block.innerHTML += `<br/><a style="float:right; font-family: 'Open Sans', sans-serif; font-size: 70%; cursor: pointer; color: gray; text-transform: uppercase; position: relative; top: -10px;" href='${playground_url}/#fstar/${hax_version}/${LZString.compressToEncodedURIComponent(text)}'>Open in hax playground ↗</a>`;
+                result_block.innerHTML += `<br/><a style="float:right; font-family: 'Open Sans', sans-serif; font-size: 70%; cursor: pointer; color: gray; text-transform: uppercase; position: relative; top: -10px;" href='${PLAYGROUND_URL}/#fstar/${hax_version}/${LZString.compressToEncodedURIComponent(text)}'>Open in hax playground ↗</a>`;
             }
         },
     );

diff --git a/docs/publications.md b/docs/publications.md
@@ -2,15 +2,22 @@
 weight: 5
 ---
 
+To cite hax, please use
+
+<center>
+[**hax: Verifying Security-Critical Rust Software using Multiple Provers**](https://eprint.iacr.org/2025/142).
+</center>
+
 # Publications
 
-* [📕 hacspec Tech report](https://hal.inria.fr/hal-03176482)
-* [📕 HACSpec: A gateway to high-assurance cryptography](https://github.com/hacspec/hacspec/blob/master/rwc2023-abstract.pdf)
-* [📕 Original hacspec paper](https://www.franziskuskiefer.de/publications/hacspec-ssr18-paper.pdf)
+* [hax: Verifying Security-Critical Rust Software using Multiple Provers](https://eprint.iacr.org/2025/142)
+* [hacspec Tech report](https://hal.inria.fr/hal-03176482)
+* [HACSpec: A gateway to high-assurance cryptography](https://github.com/hacspec/hacspec/blob/master/rwc2023-abstract.pdf)
+* [Original hacspec paper](https://www.franziskuskiefer.de/publications/hacspec-ssr18-paper.pdf)
 
 ### Secondary literature, using hacspec & hax:
-* [📕 Last yard](https://eprint.iacr.org/2023/185)
-* [📕 A Verified Pipeline from a Specification Language to Optimized, Safe Rust](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl22-final61.pdf) at [CoqPL'22](https://popl22.sigplan.org/details/CoqPL-2022-papers/5/A-Verified-Pipeline-from-a-Specification-Language-to-Optimized-Safe-Rust)
-* [📕 Hax - Enabling High Assurance Cryptographic Software](https://github.com/hacspec/hacspec.github.io/blob/master/RustVerify24.pdf) at [RustVerify24](https://sites.google.com/view/rustverify2024)
-* [📕 A formal security analysis of Blockchain voting](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl24-paper8-2.pdf) at [CoqPL'24](https://popl24.sigplan.org/details/CoqPL-2024-papers/8/A-formal-security-analysis-of-Blockchain-voting)
-* [📕 Specifying Smart Contract with Hax and ConCert](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl24-paper9-13.pdf) at [CoqPL'24](https://popl24.sigplan.org/details/CoqPL-2024-papers/9/Specifying-Smart-Contract-with-Hax-and-ConCert)
+* [Last yard](https://eprint.iacr.org/2023/185)
+* [A Verified Pipeline from a Specification Language to Optimized, Safe Rust](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl22-final61.pdf) at [CoqPL'22](https://popl22.sigplan.org/details/CoqPL-2022-papers/5/A-Verified-Pipeline-from-a-Specification-Language-to-Optimized-Safe-Rust)
+* [Hax - Enabling High Assurance Cryptographic Software](https://github.com/hacspec/hacspec.github.io/blob/master/RustVerify24.pdf) at [RustVerify24](https://sites.google.com/view/rustverify2024)
+* [A formal security analysis of Blockchain voting](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl24-paper8-2.pdf) at [CoqPL'24](https://popl24.sigplan.org/details/CoqPL-2024-papers/8/A-formal-security-analysis-of-Blockchain-voting)
+* [Specifying Smart Contract with Hax and ConCert](https://github.com/hacspec/hacspec.github.io/blob/master/coqpl24-paper9-13.pdf) at [CoqPL'24](https://popl24.sigplan.org/details/CoqPL-2024-papers/9/Specifying-Smart-Contract-with-Hax-and-ConCert)
diff --git a/docs/static/img/overview.png b/docs/static/img/overview.png
diff --git a/docs/static/img/playground.png b/docs/static/img/playground.png
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
@@ -109,8 +109,8 @@ module Make (F : Features.T) = struct
 
     let deref_mut_app = concrete_app1 Core__ops__deref__DerefMut__deref_mut
 
-    let local_var (e : expr) : expr option =
-      match e.e with LocalVar _ -> Some e | _ -> None
+    let local_var (e : expr) : local_ident option =
+      match e.e with LocalVar v -> Some v | _ -> None
 
     let arrow (typ : ty) : (ty list * ty) option =
       match typ with

diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
@@ -37,6 +37,7 @@ end
 
 module U = Ast_utils.Make (Features.Rust)
 module W = Features.On
+module Ast_builder = Ast_builder.Make (Features.Rust)
 open Ast
 
 let def_id ~value (def_id : Thir.def_id) : global_ident =
@@ -724,18 +725,32 @@ end) : EXPR = struct
                        typ = TInt { size = S8; signedness = Unsigned };
                      })
                    l))
-      | NamedConst { def_id = id; impl; args; _ } -> (
+      | NamedConst { def_id = id; impl; args; _ } ->
           let f = GlobalVar (def_id ~value:true id) in
-          match impl with
-          | Some impl ->
-              let trait =
-                Some
-                  ( c_impl_expr e.span impl,
-                    List.map ~f:(c_generic_value e.span) args )
-              in
-              let f = { e = f; span; typ = TArrow ([], typ) } in
-              App { f; trait; args = []; generic_args = []; bounds_impls = [] }
-          | _ -> f)
+          let args = List.map ~f:(c_generic_value e.span) args in
+          let const_args =
+            List.filter_map args ~f:(function GConst e -> Some e | _ -> None)
+          in
+          if List.is_empty const_args && Option.is_none impl then f
+          else
+            let f =
+              {
+                e = f;
+                span;
+                typ = TArrow (List.map const_args ~f:(fun e -> e.typ), typ);
+              }
+            in
+            let trait =
+              Option.map impl ~f:(c_impl_expr e.span &&& Fn.const args)
+            in
+            App
+              {
+                f;
+                trait;
+                args = const_args;
+                generic_args = [];
+                bounds_impls = [];
+              }
       | Closure { body; params; upvars; _ } ->
           let params =
             List.filter_map ~f:(fun p -> Option.map ~f:c_pat p.pat) params
@@ -1358,95 +1373,60 @@ let generic_param_to_value ({ ident; kind; span; _ } : generic_param) :
   | GPType -> GType (TParam ident)
   | GPConst { typ } -> GConst { e = LocalVar ident; typ; span }
 
-type discriminant_expr =
-  | Lit of Int64.t
-  | Exp of expr  (** Helper type for [cast_of_enum]. *)
-
 (** Generate a cast function from an inductive to its represantant type. *)
 let cast_of_enum typ_name generics typ thir_span
     (variants : (variant * Types.variant_for__decorated_for__expr_kind) list) :
     item =
+  let span = Span.of_thir thir_span in
+  let (module M) = Ast_builder.make span in
   let self =
-    TApp
-      {
-        ident = `Concrete typ_name;
-        args = List.map ~f:generic_param_to_value generics.params;
-      }
+    let args = List.map ~f:generic_param_to_value generics.params in
+    TApp { ident = `Concrete typ_name; args }
   in
-  let span = Span.of_thir thir_span in
-  let init = Lit (Int64.of_int 0) in
-  let to_expr (n : Int64.t) : expr =
-    match typ with
-    | TInt kind ->
-        let value = Int64.to_string n in
-        {
-          e = Literal (Int { value; negative = Int64.is_negative n; kind });
-          span;
-          typ;
-        }
-    | typ ->
-        assertion_failure [ thir_span ]
-        @@ "disc_literal_to_expr: got repr type "
-        ^ [%show: ty] typ
+  let expr_of_int (n : Int64.t) : expr =
+    let kind =
+      match typ with
+      | TInt kind -> kind
+      | typ ->
+          assertion_failure [ thir_span ]
+            ("cast_of_enum: expected in type, got " ^ [%show: ty] typ)
+    in
+    let value = Int64.to_string n in
+    M.expr_Literal ~typ (Int { value; negative = Int64.is_negative n; kind })
   in
   let arms =
-    List.folding_map variants ~init ~f:(fun acc (variant, thir_variant) ->
+    (* Each variant comes with a [rustc_middle::ty::VariantDiscr]. Some variant have [Explicit] discr (i.e. an expression)
+       while other have [Relative] discr (the distance to the previous last explicit discr). *)
+    List.folding_map variants ~init:None
+      ~f:(fun previous_explicit_discriminator (variant, { discr; _ }) ->
         let pat =
-          PConstruct
-            {
-              is_record = variant.is_record;
-              is_struct = false;
-              fields =
-                List.map
-                  ~f:(fun (cid, typ, _) ->
-                    { field = `Concrete cid; pat = { p = PWild; typ; span } })
-                  variant.arguments;
-              constructor = `Concrete variant.name;
-            }
+          let mk_wild_field (cid, typ, _) =
+            { field = `Concrete cid; pat = M.pat_PWild ~typ }
+          in
+          M.pat_PConstruct ~constructor:(`Concrete variant.name)
+            ~is_struct:false ~typ ~is_record:variant.is_record
+            ~fields:(List.map ~f:mk_wild_field variant.arguments)
         in
-        let pat = { p = pat; typ = self; span } in
-        match (acc, thir_variant.discr) with
-        | Lit n, Relative m ->
-            let acc = Lit Int64.(n + m) in
-            (acc, (pat, acc))
+        match (previous_explicit_discriminator, discr) with
+        | None, Relative m -> (None, (pat, expr_of_int m))
         | _, Explicit did ->
-            let acc =
-              Exp { e = GlobalVar (def_id ~value:true did); span; typ }
-            in
-            (acc, (pat, acc))
-        | Exp e, Relative n ->
-            let acc =
-              Exp (U.call Core__ops__arith__Add__add [ e; to_expr n ] span typ)
-            in
-            (Exp e, (pat, acc)))
-    |> List.map ~f:(Fn.id *** function Exp e -> e | Lit n -> to_expr n)
-    |> List.map ~f:(fun (arm_pat, body) ->
-           { arm = { arm_pat; body; guard = None }; span })
-  in
-  let scrutinee_var =
-    Local_ident.{ name = "x"; id = Local_ident.mk_id Expr (-1) }
+            let e = M.expr_GlobalVar ~typ (def_id ~value:true did) in
+            (Some e, (pat, e))
+        | Some e, Relative n ->
+            let n = expr_of_int n in
+            let e = U.call Core__ops__arith__Add__add [ e; n ] span typ in
+            (previous_explicit_discriminator, (pat, e)))
+    |> List.map ~f:(fun (p, e) -> M.arm p e)
   in
-  let scrutinee = { e = LocalVar scrutinee_var; typ = self; span } in
+  let scrutinee_var = Local_ident.{ name = "x"; id = mk_id Expr (-1) } in
+  let scrutinee = M.expr_LocalVar ~typ:self scrutinee_var in
   let ident = cast_name_for_type typ_name in
-  let v =
-    Fn
-      {
-        name = ident;
-        generics;
-        body = { e = Match { scrutinee; arms }; typ; span };
-        params =
-          [
-            {
-              pat = U.make_var_pat scrutinee_var self span;
-              typ = self;
-              typ_span = None;
-              attrs = [];
-            };
-          ];
-        safety = Safe;
-      }
+  let params =
+    let pat = U.make_var_pat scrutinee_var self span in
+    [ { pat; typ = self; typ_span = None; attrs = [] } ]
   in
-  { v; span; ident; attrs = [] }
+  let body = M.expr_Match ~typ ~scrutinee ~arms in
+  M.item_Fn ~ident ~attrs:[] ~name:ident ~generics ~params ~safety:Safe ~body
 
 let rec c_item ~ident ~type_only (item : Thir.item) : item list =
   try

diff --git a/engine/lib/phases/phase_drop_return_break_continue.ml b/engine/lib/phases/phase_drop_return_break_continue.ml
@@ -101,6 +101,9 @@ module%inlined_contents Make (F : Features.T) = struct
               Some ({ return_type; break_type }, _) ) ->
               UA.M.expr_Constructor_CF ~return_type ~span ~break_type ~e ~acc
                 `Break
+          | ( Continue { acc = Some (acc, _); _ },
+              Some ({ return_type = None; break_type = None }, _) ) ->
+              acc
           | ( Continue { acc = Some (acc, _); _ },
               Some ({ return_type; break_type }, _) ) ->
               UA.M.expr_Constructor_CF ~return_type ~span ~break_type ~acc