Merge branch 'main' into pr/sivadeilra/190

.docker/c/Dockerfile

@@ -0,0 +1,32 @@
+# This Dockerfile should be run from this directory
+# `docker build . -t franziskus/libcrux-c`
+
+FROM ubuntu:24.04
+LABEL maintainer="Franziskus Kiefer <[email protected]>"
+
+ENV SHELL /bin/bash
+ENV USER user
+ENV LOGNAME $USER
+ENV HOME /home/$USER
+ENV LANG en_US.UTF-8
+ENV LC_ALL $LANG
+ENV PATH="$HOME/.cargo/bin:${PATH}"
+
+# Install dependencies.
+ADD setup.sh /tmp/setup.sh
+RUN bash /tmp/setup.sh
+
+WORKDIR $HOME
+USER $USER
+COPY --chown=$USER:$USER . $HOME/$USER
+
+# Setup & install.
+ADD install.sh /tmp/install.sh
+RUN bash /tmp/install.sh
+
+ENV FSTAR_HOME $HOME/fstar
+ENV HACL_HOME $HOME/hacl-star
+ENV KRML_HOME $HOME/karamel
+ENV EURYDICE_HOME $HOME/eurydice
+ENV CHARON_HOME $HOME/charon
+ENV PATH "${PATH}:$HOME/fstar/bin:$HOME/z3/bin"

.docker/c/install.sh

@@ -0,0 +1,75 @@
+#!/usr/bin/env bash
+
+set -v -e -x
+
+curl https://sh.rustup.rs -sSf | bash -s -- -y
+
+# Prepare the sources
+opam init --bare --disable-sandboxing --shell-setup --yes
+opam switch create 4.14.1
+
+# Get F*, HACL*, Charon, Karamel, Eurydice for running proofs and extraction
+curl -L https://github.com/FStarLang/FStar/releases/download/v2024.01.13/fstar_2024.01.13_Linux_x86_64.tar.gz \
+    --output Fstar.tar.gz
+tar --extract --file Fstar.tar.gz
+rm -f Fstar.tar.gz
+
+curl -L https://github.com/FStarLang/binaries/raw/master/z3-tested/z3-4.8.5-x64-ubuntu-16.04.zip --output z3.zip
+unzip z3.zip
+rm -rf z3.zip
+mv z3-4.8.5-x64-ubuntu-16.04/ z3
+
+curl -L https://github.com/hacl-star/hacl-star/archive/443aed2deccfbee84f928fadc1f594f729c3aad4.zip \
+    --output hacl-star.zip
+unzip hacl-star.zip
+rm -rf hacl-star.zip
+mv hacl-star-443aed2deccfbee84f928fadc1f594f729c3aad4/ hacl-star
+
+curl -L https://github.com/AeneasVerif/charon/archive/89cecf5d1074fae7e8007be7f6cdf2f38e9782b1.zip \
+    --output charon.zip
+unzip charon.zip
+rm -rf charon.zip
+mv charon-89cecf5d1074fae7e8007be7f6cdf2f38e9782b1/ charon
+
+curl -L https://github.com/FStarLang/karamel/archive/08bfa78ae1df5639446e6c5897b07c9823fbf3b0.zip \
+    --output karamel.zip
+unzip karamel.zip
+rm -rf karamel.zip
+mv karamel-08bfa78ae1df5639446e6c5897b07c9823fbf3b0/ karamel
+
+curl -L https://github.com/AeneasVerif/eurydice/archive/7780d2b4c44c7811d02d7e05789b5611fd497480.zip \
+    --output eurydice.zip
+unzip eurydice.zip
+rm -rf eurydice.zip
+mv eurydice-7780d2b4c44c7811d02d7e05789b5611fd497480/ eurydice
+
+echo "export FSTAR_HOME=$HOME/fstar" >>$HOME/.profile
+echo "export HACL_HOME=$HOME/hacl-star" >>$HOME/.profile
+echo "export KRML_HOME=$HOME/karamel" >>$HOME/.profile
+echo "export EURYDICE_HOME=$HOME/eurydice" >>$HOME/.profile
+echo "export CHARON_HOME=$HOME/charon" >>$HOME/.profile
+echo "export HAX_HOME=$HOME/hax" >>$HOME/.profile
+echo "export PATH=\"${PATH}:$HOME/fstar/bin:$HOME/z3/bin\"" >>$HOME/.profile
+echo "[[ ! -r /home/$USER/.opam/opam-init/init.sh ]] || source /home/$USER/.opam/opam-init/init.sh  > /dev/null 2> /dev/null" >>$HOME/.profile
+
+source $HOME/.profile
+opam install --yes ocamlfind visitors menhir ppx_deriving_yojson sedlex wasm fix process pprint zarith yaml easy_logging terminal
+eval $(opam env)
+
+# Build everything
+cd karamel
+make -j
+cd -
+
+cd charon
+make -j
+cd -
+
+cd eurydice/lib
+rm -f charon
+ln -s $CHARON_HOME/charon-ml charon
+rm -f krml
+ln -s $KRML_HOME/lib krml
+cd ../
+make -j
+cd ../

.docker/c/setup.sh

@@ -0,0 +1,23 @@
+#!/usr/bin/env bash
+
+set -v -e -x
+
+export DEBIAN_FRONTEND=noninteractive
+
+apt-get -y update
+apt-get install -y \
+    nodejs \
+    build-essential \
+    opam \
+    jq \
+    libgmp-dev \
+    locales \
+    curl
+curl -fsSL https://deb.nodesource.com/setup_21.x | bash -
+apt-get update
+apt-get install -y nodejs
+
+locale-gen $LANG
+DEBIAN_FRONTEND=noninteractive dpkg-reconfigure locales
+useradd -d $HOME -s $SHELL -m $USER
+echo "$USER:$USER" | chpasswd && adduser $USER sudo

.github/workflows/hax.yml

@@ -2,13 +2,13 @@ name: hax
 
 on:
   push:
-    branches: ["dev"]
+    branches: ["dev", "main"]
     paths:
       - 'specs/kyber/src/**'
       - 'src/kem/kyber/**'
 
   pull_request:
-    branches: ["dev"]
+    branches: ["dev", "main"]
     paths:
       - 'specs/kyber/src/**'
       - 'src/kem/kyber/**'
@@ -35,13 +35,8 @@ jobs:
       - uses: DeterminateSystems/nix-installer-action@main
       - uses: DeterminateSystems/magic-nix-cache-action@main
 
-      - name: 🔨 OCaml Setup
-        uses: ocaml/setup-ocaml@v2
-        with:
-          ocaml-compiler: 4.14.1
-
       - name: ⤵ Install FStar
-        run: nix profile install github:FStarLang/FStar/bc622701c668f6b4092760879372968265d4a4e1
+        run: nix profile install github:FStarLang/FStar/v2024.01.13
 
       - name: ⤵ Clone HACL-star repository
         uses: actions/checkout@v4
@@ -55,17 +50,30 @@ jobs:
           repository: hacspec/hacspec-v2
           path: hax
 
-      - name: 🔨 Setup hax
-        working-directory: hax
+      - name: ⤵ Install & confiure Cachix
+        run: |
+          nix profile install nixpkgs#cachix
+          cachix use hax
+
+      - name: ⤵ Install hax
         run: |
-          sudo apt-get update
-          sudo apt-get install --yes nodejs
-          ./setup.sh
+          nix profile install ./hax
 
-      - name: 🏃 Extract and verify the Kyber reference code
+      - name: 🏃 Extract the Kyber reference code
         run: |
           eval $(opam env)
+          (cd proofs/fstar/extraction/ && ./clean.sh)
+          rm -f sys/platform/proofs/fstar/extraction/*.fst*
           ./hax-driver.py --kyber-reference
+
+      - name: 🏃 Regenerate `extraction-*` folders
+        run: ./proofs/fstar/patches.sh apply
+
+      - name: 🏃 Make sure snapshots are up-to-date
+        run: git diff --exit-code
+
+      - name: 🏃 Verify the Kyber reference code
+        run: |
           env FSTAR_HOME=${{ github.workspace }}/fstar \
               HACL_HOME=${{ github.workspace }}/hacl-star \
               HAX_HOME=${{ github.workspace }}/hax \

.github/workflows/rust.yml

@@ -124,7 +124,7 @@ jobs:
 
     steps:
       - uses: actions/checkout@v4
-      - uses: mymindstorm/setup-emsdk@d233ac12b0102f74ca199f5dad7a4e2c13a8a745
+      - uses: mymindstorm/setup-emsdk@6ab9eb1bda2574c4ddb79809fc9247783eaf9021
 
       - name: Setup
         run: |

Cargo.toml

@@ -4,8 +4,8 @@ members = [
     "sys/libjade",
     "sys/platform",
     "sys/pqclean",
-    "fuzz",
     "benchmarks",
+    "fuzz",
 ]
 
 [workspace.package]
@@ -43,22 +43,18 @@ rand = { version = "0.8" }
 log = { version = "0.4", optional = true }
 # WASM API
 wasm-bindgen = { version = "0.2.87", optional = true }
-hax-lib = { git = "https://github.com/hacspec/hax/", branch = "main" }
 
 # When using the hax toolchain, we have more dependencies.
 # This is only required when doing proofs.
 [target.'cfg(hax)'.dependencies]
-hax-lib-macros = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax" }
+hax-lib-macros = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax", branch = "main" }
+hax-lib = { version = "0.1.0-pre.1", git = "https://github.com/hacspec/hax/", branch = "main" }
 
-# WASM needs the js feature on getrandom
-[target.'cfg(target_arch = "wasm32")'.dependencies]
-getrandom = { version = "0.2", features = ["js"] }
-
-[target.'cfg(all(not(target_os = "windows"), target_arch = "x86_64"))'.dependencies]
+[target.'cfg(all(not(target_os = "windows"), target_arch = "x86_64", libjade))'.dependencies]
 libjade-sys = { version = "=0.0.2-pre.2", path = "sys/libjade" }
 
 [dev-dependencies]
-libcrux = { path = ".", features = ["rand"] }
+libcrux = { path = ".", features = ["rand", "tests"] }
 pretty_env_logger = "0.5"
 rand = { version = "0.8" }
 rand_core = { version = "0.6" }
@@ -70,6 +66,7 @@ hex = { version = "0.4.3", features = ["serde"] }
 
 [target.'cfg(target_arch = "wasm32")'.dev-dependencies]
 wasm-bindgen-test = "0.3"
+getrandom = { version = "0.2", features = ["js"] }
 
 [features]
 hacspec = []            # TODO: #7 Use specs instead of efficient implementations
@@ -78,3 +75,5 @@ wasm = ["wasm-bindgen"]
 log = ["dep:log"]
 default = ["std"]
 std = []
+tests = []              # Expose functions for testing.
+experimental = []       # Expose experimental APIs.

add-c-kyber-to-nss.py

@@ -25,7 +25,8 @@ def shell(command, expect=0, cwd=None, env={}):
 
 def add_libcrux_kyber_h(c_extraction_root, freebl_verified_root):
     path_to_header = os.path.join(c_extraction_root, "libcrux_kyber.h")
-    destination = os.path.join(freebl_verified_root, "internal", "Libcrux_Kyber_768.h")
+    destination = os.path.join(freebl_verified_root, "Libcrux_ML_KEM_768.h")
+    shutil.copyfile(path_to_header, destination)
 
     shell(["clang-format", "-i", "-style=Google", destination])
 
@@ -41,7 +42,7 @@ def add_libcrux_kyber_h(c_extraction_root, freebl_verified_root):
 
 def add_libcrux_kyber_c(c_extraction_root, freebl_verified_root):
     path_to_c_file = os.path.join(c_extraction_root, "libcrux_kyber.c")
-    destination = os.path.join(freebl_verified_root, "Libcrux_Kyber_768.c")
+    destination = os.path.join(freebl_verified_root, "Libcrux_ML_KEM_768.c")
     shutil.copyfile(path_to_c_file, destination)
 
     shell(["clang-format", "-i", "-style=Google", destination])
@@ -67,12 +68,12 @@ def add_libcrux_kyber_c(c_extraction_root, freebl_verified_root):
         original = f.read()
         replaced = re.sub(
             '#include "libcrux_kyber.h"',
-            '#include "internal/Libcrux_Kyber_768.h"',
+            '#include "Libcrux_ML_KEM_768.h"',
             original,
         )
         replaced = re.sub(
             '#include "libcrux_hacl_glue.h"',
-            '#include "Libcrux_Kyber_Hash_Functions.h"',
+            '#include "../Libcrux_ML_KEM_Hash_Functions.h"',
             replaced,
         )
         replaced = re.sub("uu____0 = !false", "uu____0 = false", replaced)

benchmarks/Cargo.toml

@@ -7,11 +7,12 @@ homepage.workspace = true
 edition.workspace = true
 repository.workspace = true
 readme.workspace = true
+publish = false
 
 [dependencies]
 
 [dev-dependencies]
-libcrux = { path = "../", features = ["rand"] }
+libcrux = { path = "../", features = ["rand", "tests"] }
 rand = { version = "0.8" }
 rand_core = { version = "0.6" }
 # Benchmarking "RustCrypto"
@@ -26,7 +27,7 @@ ring = "0.17"
 [target.'cfg(not(target_arch = "wasm32"))'.dev-dependencies]
 criterion = "0.5"
 # libcrux-pqclean = { version = "0.0.2-pre.1", path = "sys/pqclean" }
-pqcrypto-kyber = { version = "0.7.6", default-features = false }
+pqcrypto-kyber = { version = "0.8.0", default-features = false }
 
 # Benchmarking "OpenSSL"
 # XXX: We don't do this for Windows or wasm right now.

benchmarks/benches/boringssl/.gitignore

@@ -0,0 +1 @@
+build/

benchmarks/benches/circl/go.mod

@@ -2,9 +2,9 @@ module benchmarks
 
 go 1.20
 
-require github.com/cloudflare/circl v1.3.3
+require github.com/cloudflare/circl v1.3.7
 
 require (
-	golang.org/x/crypto v0.3.1-0.20221117191849-2c476679df9a // indirect
-	golang.org/x/sys v0.3.0 // indirect
+	golang.org/x/crypto v0.17.0 // indirect
+	golang.org/x/sys v0.15.0 // indirect
 )

benchmarks/benches/circl/go.sum

@@ -1,6 +1,6 @@
-github.com/cloudflare/circl v1.3.3 h1:fE/Qz0QdIGqeWfnwq0RE0R7MI51s0M2E4Ga9kq5AEMs=
-github.com/cloudflare/circl v1.3.3/go.mod h1:5XYMA4rFBvNIrhs50XuiBJ15vF2pZn4nnUKZrLbUZFA=
-golang.org/x/crypto v0.3.1-0.20221117191849-2c476679df9a h1:diz9pEYuTIuLMJLs3rGDkeaTsNyRs6duYdFyPAxzE/U=
-golang.org/x/crypto v0.3.1-0.20221117191849-2c476679df9a/go.mod h1:hebNnKkNXi2UzZN1eVRvBB7co0a+JxK6XbPiWVs/3J4=
-golang.org/x/sys v0.3.0 h1:w8ZOecv6NaNa/zC8944JTU3vz4u6Lagfk4RPQxv92NQ=
-golang.org/x/sys v0.3.0/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
+github.com/cloudflare/circl v1.3.7 h1:qlCDlTPz2n9fu58M0Nh1J/JzcFpfgkFHHX3O35r5vcU=
+github.com/cloudflare/circl v1.3.7/go.mod h1:sRTcRWXGLrKw6yIGJ+l7amYJFfAXbZG0kBSc8r4zxgA=
+golang.org/x/crypto v0.17.0 h1:r8bRNjWL3GshPW3gkd+RpvzWrZAwPS49OmTGZ/uhM4k=
+golang.org/x/crypto v0.17.0/go.mod h1:gCAAfMLgwOJRpTjQ2zCCt2OcSfYMTeZVSRtQlPC7Nq4=
+golang.org/x/sys v0.15.0 h1:h48lPFYpsTvQJZF4EKyI4aLHaev3CxivZmv7yZig9pc=
+golang.org/x/sys v0.15.0/go.mod h1:/VUhepiaJMQUp4+oa/7Zr1D23ma6VTLIYjOOTFZPUcA=

benchmarks/benches/drbg.rs

@@ -3,7 +3,7 @@ use libcrux::{digest::Algorithm, drbg::*};
 use ring::rand::Random;
 
 fn init(c: &mut Criterion) {
-    let mut group = c.benchmark_group("x25519 derive");
+    let mut group = c.benchmark_group("Drbg");
 
     group.bench_function("libcrux Sha256", |b| {
         b.iter(|| {
@@ -37,7 +37,7 @@ fn init(c: &mut Criterion) {
 }
 
 fn generate(c: &mut Criterion) {
-    let mut group = c.benchmark_group("x25519 secret to public");
+    let mut group = c.benchmark_group("Drbg");
 
     group.bench_function("libcrux Sha256", |b| {
         b.iter_batched(