c cg fstar refresh

.github/workflows/flake-update.yml

@@ -15,7 +15,7 @@ jobs:
       - uses: actions/checkout@v4
         with:
           ref: ${{ inputs.branch }}
-      - uses: DeterminateSystems/nix-installer-action@v13
+      - uses: DeterminateSystems/nix-installer-action@v16
       - name: update `flake.lock`
         run: nix flake update
       - name: commit

.github/workflows/hax.yml

@@ -11,6 +11,10 @@ on:
     - cron: "0 0 * * *"
 
   workflow_dispatch:
+    inputs:
+      hax_rev:
+        description: 'The hax revision you want this job to use'
+        default: 'main'
   merge_group:
 
 env:
@@ -42,6 +46,7 @@ jobs:
         uses: actions/checkout@v4
         with:
           repository: hacspec/hax
+          ref: ${{ github.event.inputs.hax_rev || 'main' }}
           path: hax
 
       - name: ⤵ Install & confiure Cachix

.github/workflows/nix.yml

@@ -10,7 +10,7 @@ jobs:
   nix:
     runs-on: ubuntu-latest
     steps:
-      - uses: DeterminateSystems/nix-installer-action@v13
+      - uses: DeterminateSystems/nix-installer-action@v16
       - uses: DeterminateSystems/magic-nix-cache-action@v7
       - name: Install & configure Cachix
         shell: bash

.gitignore

@@ -8,6 +8,7 @@ __pycache__
 kyber-crate/
 *.llbc
 .cargo/
+Cargo.lock
 
 # When using sed
 *.bak

CODEOWNERS

@@ -0,0 +1 @@
+* @cryspen/libcrux

Cargo.toml

@@ -116,6 +116,9 @@ lto = "fat"
 codegen-units = 1
 panic = "abort"
 
+[profile.dev.package."libcrux-ml-dsa"]
+opt-level = 1
+
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = [
     'cfg(hax)',

curve25519/src/lib.rs

@@ -1,3 +1,5 @@
+#![no_std]
+
 #[cfg(feature = "hacl")]
 pub use libcrux_hacl_rs::curve25519_51 as hacl;
 

ed25519/src/hacl/ed25519.rs

@@ -6,9 +6,7 @@
 
 use libcrux_macros as krml;
 
-use libcrux_hacl_rs::bignum;
-use libcrux_hacl_rs::fstar;
-use libcrux_hacl_rs::lowstar;
+use libcrux_hacl_rs::prelude::*;
 
 #[inline]
 fn fsum(out: &mut [u64], a: &[u64], b: &[u64]) {

ed25519/src/lib.rs

@@ -1,3 +1,5 @@
+#![no_std]
+
 #[cfg(feature = "hacl")]
 pub mod hacl {
     //! This module contains generated hacl code.

flake.nix

@@ -60,16 +60,17 @@
           FSTAR_REV = inputs.fstar.rev;
         };
 
+        craneLib = inputs.crane.mkLib pkgs;
+
         ml-kem = pkgs.callPackage
-          ({ pkgs
-           , lib
+          ({ lib
            , clang-tools
            , cmake
            , mold-wrapped
            , ninja
            , python3
            , runCommand
-           , crane
+           , craneLib
            , hax
            , googletest
            , benchmark
@@ -80,7 +81,6 @@
            , runBenchmarks ? true
            }:
             let
-              craneLib = crane.mkLib pkgs;
               src = runCommand "libcrux-src" { } ''
                 cp -r ${./.} $out
                 chmod u+w $out
@@ -134,8 +134,7 @@
           {
             inherit
               googletest benchmark json
-              tools-environment;
-            crane = inputs.crane;
+              craneLib tools-environment;
             hax =
               inputs.hax.packages.${system}.default;
           };
@@ -144,15 +143,30 @@
         packages = {
           inherit ml-kem;
         };
-        devShells.default = pkgs.mkShell (tools-environment // {
+        devShells.default = craneLib.devShell (tools-environment // {
           packages = [
             pkgs.clang
             inputs.fstar.packages.${system}.default
           ];
 
-          inputsFrom = [
-            packages.ml-kem
+          # Can't use `inputsFrom` because the `Cargo.lock` is not tracked by git on first evaluation.
+          buildInputs = [
+            pkgs.clang-tools
+            pkgs.cmake
+            pkgs.mold-wrapped
+            pkgs.ninja
+            pkgs.python3
+            inputs.hax.packages.${system}.default
           ];
+
+          shellHook = ''
+            # `Cargo.lock` need to be known to git for the flake to find it.
+            # Note: run `cargo generate-lockfile` to generate a real
+            # `Cargo.lock`. Without that nix builds will error.
+            touch Cargo.lock
+            ${pkgs.git}/bin/git add --intent-to-add --force Cargo.lock
+            ${pkgs.git}/bin/git update-index --assume-unchanged Cargo.lock
+          '';
         });
       }
     );

hacl-rs/src/bignum/base.rs

@@ -5,11 +5,9 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
-use libcrux_macros as krml;
+use crate::prelude::*;
 
-use crate::fstar;
-use crate::lowstar;
-use crate::util as lib;
+use libcrux_macros as krml;
 
 pub(crate) fn bn_karatsuba_mul_uint32(
     aLen: u32,

hacl-rs/src/bignum/bignum256.rs

@@ -4,11 +4,9 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
-use libcrux_macros as krml;
+use crate::prelude::*;
 
-use crate::fstar;
-use crate::lowstar;
-use crate::util as lib;
+use libcrux_macros as krml;
 
 /**
 Write `a + b mod 2^256` in `res`.

hacl-rs/src/bignum/bignum256_32.rs

@@ -4,11 +4,9 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
-use libcrux_macros as krml;
+use crate::prelude::*;
 
-use crate::fstar;
-use crate::lowstar;
-use crate::util as lib;
+use libcrux_macros as krml;
 
 /**
 Write `a + b mod 2^256` in `res`.

hacl-rs/src/bignum/bignum32.rs

@@ -4,9 +4,7 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
-use crate::fstar;
-use crate::lowstar;
-use crate::util as lib;
+use crate::prelude::*;
 
 pub type pbn_mont_ctx_u32<'a> = &'a [super::base::bn_mont_ctx_u32];
 

hacl-rs/src/bignum/bignum4096.rs

@@ -4,11 +4,9 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
-use libcrux_macros as krml;
+use crate::prelude::*;
 
-use crate::fstar;
-use crate::lowstar;
-use crate::util as lib;
+use libcrux_macros as krml;
 
 /**
 Write `a + b mod 2^4096` in `res`.

hacl-rs/src/bignum/bignum4096_32.rs

@@ -4,11 +4,9 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
-use libcrux_macros as krml;
+use crate::prelude::*;
 
-use crate::fstar;
-use crate::lowstar;
-use crate::util as lib;
+use libcrux_macros as krml;
 
 /**
 Write `a + b mod 2^4096` in `res`.

hacl-rs/src/bignum/bignum64.rs

@@ -4,9 +4,7 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
-use crate::fstar;
-use crate::lowstar;
-use crate::util as lib;
+use crate::prelude::*;
 
 pub type pbn_mont_ctx_u64<'a> = &'a [super::base::bn_mont_ctx_u64];
 

hacl-rs/src/bignum/bignum_base.rs

@@ -4,9 +4,7 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
-use crate::fstar;
-use crate::lowstar;
-use crate::util as lib;
+use crate::prelude::*;
 
 #[inline]
 pub(crate) fn mul_wide_add2_u32(a: u32, b: u32, c_in: u32, out: &mut [u32]) -> u32 {