cryspen · karthikbhargavan · Jul 23, 2024 · Jul 23, 2024 · Jul 29, 2024 · Jul 29, 2024
diff --git a/.docker/c/Dockerfile b/.docker/c/Dockerfile
@@ -23,6 +23,8 @@ COPY --chown=$USER:$USER . $HOME/$USER
 # Setup & install.
 ADD install.sh /tmp/install.sh
 RUN bash /tmp/install.sh
+ADD ext-tools.sh /tmp/ext-tools.sh
+RUN bash /tmp/ext-tools.sh
 
 ENV FSTAR_HOME=$HOME/fstar
 ENV HACL_HOME=$HOME/hacl-star

diff --git a/.docker/c/ext-tools.sh b/.docker/c/ext-tools.sh
@@ -0,0 +1,47 @@
+#!/usr/bin/env bash
+
+set -v -e -x
+
+source $HOME/.profile
+
+curl -L https://github.com/AeneasVerif/charon/archive/28d543bfacc902ba9cc2a734b76baae9583892a4.zip \
+ --output charon.zip
+unzip charon.zip
+rm -rf charon.zip
+mv charon-28d543bfacc902ba9cc2a734b76baae9583892a4/ charon
+
+curl -L https://github.com/FStarLang/karamel/archive/15d4bce74a2d43e34a64f48f8311b7d9bcb0e152.zip \
+ --output karamel.zip
+unzip karamel.zip
+rm -rf karamel.zip
+mv karamel-15d4bce74a2d43e34a64f48f8311b7d9bcb0e152/ karamel
+
+curl -L https://github.com/AeneasVerif/eurydice/archive/1a65dbf3758fe310833718c645a64266294a29ac.zip \
+ --output eurydice.zip
+unzip eurydice.zip
+rm -rf eurydice.zip
+mv eurydice-1a65dbf3758fe310833718c645a64266294a29ac/ eurydice
+
+echo "export KRML_HOME=$HOME/karamel" >>$HOME/.profile
+echo "export EURYDICE_HOME=$HOME/eurydice" >>$HOME/.profile
+echo "export CHARON_HOME=$HOME/charon" >>$HOME/.profile
+
+source $HOME/.profile
+
+# 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 ../
diff --git a/.docker/c/install.sh b/.docker/c/install.sh
@@ -9,7 +9,7 @@ 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 \
+curl -L https://github.com/FStarLang/FStar/releases/download/v2024.09.05/fstar_2024.09.05_Linux_x86_64.tar.gz \
  --output Fstar.tar.gz
 tar --extract --file Fstar.tar.gz
 rm -f Fstar.tar.gz
@@ -25,52 +25,12 @@ unzip hacl-star.zip
 rm -rf hacl-star.zip
 mv hacl-star-2a8b61343a1a7232611cb763b0dc3e4dff84d656/ hacl-star
 
-curl -L https://github.com/AeneasVerif/charon/archive/3f6d1c304e0e5bef1e9e2ea65aec703661b05f39.zip \
- --output charon.zip
-unzip charon.zip
-rm -rf charon.zip
-mv charon-3f6d1c304e0e5bef1e9e2ea65aec703661b05f39/ charon
-
-
-curl -L https://github.com/FStarLang/karamel/archive/fc56fce6a58754766809845f88fc62063b2c6b92.zip \
- --output karamel.zip
-unzip karamel.zip
-rm -rf karamel.zip
-mv karamel-fc56fce6a58754766809845f88fc62063b2c6b92/ karamel
-
-curl -L https://github.com/AeneasVerif/eurydice/archive/392674166bac86e60f5fffa861181a398fdc3896.zip \
- --output eurydice.zip
-unzip eurydice.zip
-rm -rf eurydice.zip
-mv eurydice-392674166bac86e60f5fffa861181a398fdc3896/ 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 core_unix 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 ../
diff --git a/.github/workflows/hax.yml b/.github/workflows/hax.yml
@@ -65,3 +65,7 @@ jobs:
  HAX_HOME=${{ github.workspace }}/hax \
  PATH="${PATH}:${{ github.workspace }}/fstar/bin" \
  ./hax.py prove --admit
+
+ - name: 🏃 Extract ML-DSA crate
+ working-directory: libcrux-ml-dsa
+ run: cargo hax into fstar
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/LICENSE-MIT b/LICENSE-MIT
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2024 Cryspen
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/Readme.md b/Readme.md
@@ -52,6 +52,20 @@ libcrux uses the following configurations for its hardware abstractions
 libcrux provides a DRBG implementation that can be used standalone (`drbg::Drbg`)
 or through the `Rng` traits.
 
+## Verification status
+
+As a quick indicator of overall verification status, subcrates in this workspace include the following badges:
+
+- ![pre-verification] to indicate that most (or all) of the code that is contained in default features of that crate is not (yet) verified.
+- ![verified] to indicate that most (or all) of the code that is contained in the default feature set is verified.
+
+In both cases, please refer to the more detailed notes on verification in each
+sub-crate to learn more about what has (or has not) been verified in the
+particular case.
+
 [architecture]: ./Architecture.md
 [hacspec]: https://hacspec.org
 [formal verification]: ./formal_verification
+
+[verified]: https://img.shields.io/badge/verified-brightgreen.svg?style=for-the-badge&logo=data:image/svg+xml;base64,PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0idXRmLTgiPz48IS0tIFVwbG9hZGVkIHRvOiBTVkcgUmVwbywgd3d3LnN2Z3JlcG8uY29tLCBHZW5lcmF0b3I6IFNWRyBSZXBvIE1peGVyIFRvb2xzIC0tPg0KPHN2ZyB3aWR0aD0iODAwcHgiIGhlaWdodD0iODAwcHgiIHZpZXdCb3g9IjAgMCAyNCAyNCIgZmlsbD0ibm9uZSIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3JnLzIwMDAvc3ZnIj4NCjxwYXRoIGQ9Ik05IDEyTDExIDE0TDE1IDkuOTk5OTlNMjAgMTJDMjAgMTYuNDYxMSAxNC41NCAxOS42OTM3IDEyLjY0MTQgMjAuNjgzQzEyLjQzNjEgMjAuNzkgMTIuMzMzNCAyMC44NDM1IDEyLjE5MSAyMC44NzEyQzEyLjA4IDIwLjg5MjggMTEuOTIgMjAuODkyOCAxMS44MDkgMjAuODcxMkMxMS42NjY2IDIwLjg0MzUgMTEuNTYzOSAyMC43OSAxMS4zNTg2IDIwLjY4M0M5LjQ1OTk2IDE5LjY5MzcgNCAxNi40NjExIDQgMTJWOC4yMTc1OUM0IDcuNDE4MDggNCA3LjAxODMzIDQuMTMwNzYgNi42NzQ3QzQuMjQ2MjcgNi4zNzExMyA0LjQzMzk4IDYuMTAwMjcgNC42Nzc2NiA1Ljg4NTUyQzQuOTUzNSA1LjY0MjQzIDUuMzI3OCA1LjUwMjA3IDYuMDc2NCA1LjIyMTM0TDExLjQzODIgMy4yMTA2N0MxMS42NDYxIDMuMTMyNzEgMTEuNzUgMy4wOTM3MyAxMS44NTcgMy4wNzgyN0MxMS45NTE4IDMuMDY0NTcgMTIuMDQ4MiAzLjA2NDU3IDEyLjE0MyAzLjA3ODI3QzEyLjI1IDMuMDkzNzMgMTIuMzUzOSAzLjEzMjcxIDEyLjU2MTggMy4yMTA2N0wxNy45MjM2IDUuMjIxMzRDMTguNjcyMiA1LjUwMjA3IDE5LjA0NjUgNS42NDI0MyAxOS4zMjIzIDUuODg1NTJDMTkuNTY2IDYuMTAwMjcgMTkuNzUzNyA2LjM3MTEzIDE5Ljg2OTIgNi42NzQ3QzIwIDcuMDE4MzMgMjAgNy40MTgwOCAyMCA4LjIxNzU5VjEyWiIgc3Ryb2tlPSIjMDAwMDAwIiBzdHJva2Utd2lkdGg9IjIiIHN0cm9rZS1saW5lY2FwPSJyb3VuZCIgc3Ryb2tlLWxpbmVqb2luPSJyb3VuZCIvPg0KPC9zdmc+
+[pre-verification]: https://img.shields.io/badge/pre_verification-orange.svg?style=for-the-badge&logo=data:image/svg+xml;base64,PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0idXRmLTgiPz48IS0tIFVwbG9hZGVkIHRvOiBTVkcgUmVwbywgd3d3LnN2Z3JlcG8uY29tLCBHZW5lcmF0b3I6IFNWRyBSZXBvIE1peGVyIFRvb2xzIC0tPg0KPHN2ZyB3aWR0aD0iODAwcHgiIGhlaWdodD0iODAwcHgiIHZpZXdCb3g9IjAgMCAyNCAyNCIgZmlsbD0ibm9uZSIgeG1sbnM9Imh0dHA6Ly93d3cudzMub3JnLzIwMDAvc3ZnIj4NCjxwYXRoIGQ9Ik05IDEySDE1TTIwIDEyQzIwIDE2LjQ2MTEgMTQuNTQgMTkuNjkzNyAxMi42NDE0IDIwLjY4M0MxMi40MzYxIDIwLjc5IDEyLjMzMzQgMjAuODQzNSAxMi4xOTEgMjAuODcxMkMxMi4wOCAyMC44OTI4IDExLjkyIDIwLjg5MjggMTEuODA5IDIwLjg3MTJDMTEuNjY2NiAyMC44NDM1IDExLjU2MzkgMjAuNzkgMTEuMzU4NiAyMC42ODNDOS40NTk5NiAxOS42OTM3IDQgMTYuNDYxMSA0IDEyVjguMjE3NTlDNCA3LjQxODA4IDQgNy4wMTgzMyA0LjEzMDc2IDYuNjc0N0M0LjI0NjI3IDYuMzcxMTMgNC40MzM5OCA2LjEwMDI3IDQuNjc3NjYgNS44ODU1MkM0Ljk1MzUgNS42NDI0MyA1LjMyNzggNS41MDIwNyA2LjA3NjQgNS4yMjEzNEwxMS40MzgyIDMuMjEwNjdDMTEuNjQ2MSAzLjEzMjcxIDExLjc1IDMuMDkzNzMgMTEuODU3IDMuMDc4MjdDMTEuOTUxOCAzLjA2NDU3IDEyLjA0ODIgMy4wNjQ1NyAxMi4xNDMgMy4wNzgyN0MxMi4yNSAzLjA5MzczIDEyLjM1MzkgMy4xMzI3MSAxMi41NjE4IDMuMjEwNjdMMTcuOTIzNiA1LjIyMTM0QzE4LjY3MjIgNS41MDIwNyAxOS4wNDY1IDUuNjQyNDMgMTkuMzIyMyA1Ljg4NTUyQzE5LjU2NiA2LjEwMDI3IDE5Ljc1MzcgNi4zNzExMyAxOS44NjkyIDYuNjc0N0MyMCA3LjAxODMzIDIwIDcuNDE4MDggMjAgOC4yMTc1OVYxMloiIHN0cm9rZT0iIzAwMDAwMCIgc3Ryb2tlLXdpZHRoPSIyIiBzdHJva2UtbGluZWNhcD0icm91bmQiIHN0cm9rZS1saW5lam9pbj0icm91bmQiLz4NCjwvc3ZnPg==
diff --git a/benchmarks/Cargo.toml b/benchmarks/Cargo.toml
@@ -9,13 +9,16 @@ repository.workspace = true
 readme.workspace = true
 publish = false
 
+[lib]
+bench = false # so libtest doesn't eat the arguments for criterion
+
 [dependencies]
+rand = { version = "0.8" }
 
 [dev-dependencies]
 libcrux = { path = "../", features = ["rand", "tests"] }
 libcrux-kem = { path = "../libcrux-kem", features = ["tests"] }
 libcrux-ml-kem = { path = "../libcrux-ml-kem" }
-rand = { version = "0.8" }
 rand_core = { version = "0.6" }
 # Benchmarking "RustCrypto"
 chacha20poly1305 = "0.10"

diff --git a/benchmarks/benches/aead.rs b/benchmarks/benches/aead.rs
@@ -2,10 +2,9 @@ use chacha20poly1305::{AeadCore, AeadInPlace, KeyInit};
 use criterion::{criterion_group, criterion_main, BatchSize, BenchmarkId, Criterion, Throughput};
 use libcrux::{aead::*, digest, drbg};
 
-mod util;
+use benchmarks::util::*;
 use rand_core::OsRng;
 use ring::aead::UnboundKey;
-use util::*;
 
 // Comparing libcrux performance for different payload sizes and other implementations.
 fn comparisons_encrypt(c: &mut Criterion) {

diff --git a/benchmarks/benches/p256.rs b/benchmarks/benches/p256.rs
@@ -1,7 +1,6 @@
 use criterion::{criterion_group, criterion_main, BatchSize, Criterion};
 use libcrux::ecdh;
 
-mod util;
 use rand_core::OsRng;
 
 fn derive(c: &mut Criterion) {

diff --git a/benchmarks/benches/sha2.rs b/benchmarks/benches/sha2.rs
@@ -3,8 +3,7 @@ use criterion::{criterion_group, criterion_main, BatchSize, BenchmarkId, Criteri
 
 use libcrux::digest::{self, *};
 
-mod util;
-use util::*;
+use benchmarks::util::*;
 
 macro_rules! impl_comp {
  ($fun:ident, $libcrux:expr, $ring:expr, $rust_crypto:ty, $openssl:expr) => {

diff --git a/benchmarks/benches/sha3.rs b/benchmarks/benches/sha3.rs
@@ -3,8 +3,7 @@ use criterion::{criterion_group, criterion_main, BatchSize, BenchmarkId, Criteri
 
 use libcrux::digest::{self, *};
 
-mod util;
-use util::*;
+use benchmarks::util::*;
 
 macro_rules! impl_comp {
  ($fun:ident, $libcrux:expr, $rust_crypto:ty, $openssl:expr) => {

diff --git a/benchmarks/benches/util.rs b/benchmarks/benches/util.rs
diff --git a/benchmarks/benches/x25519.rs b/benchmarks/benches/x25519.rs
@@ -1,9 +1,8 @@
 use criterion::{criterion_group, criterion_main, BatchSize, Criterion};
 use libcrux::ecdh;
 
-mod util;
+use benchmarks::util::*;
 use rand::RngCore;
-use util::*;
 
 fn derive(c: &mut Criterion) {
  // Comparing libcrux performance for different payload sizes and other implementations.

diff --git a/benchmarks/src/lib.rs b/benchmarks/src/lib.rs
@@ -1 +1,16 @@
+pub mod util {
+ pub fn randombytes(n: usize) -> Vec<u8> {
+ use rand::rngs::OsRng;
+ use rand::RngCore;
 
+ let mut bytes = vec![0u8; n];
+ OsRng.fill_bytes(&mut bytes);
+ bytes
+ }
+
+ pub fn fmt(x: usize) -> String {
+ let base = (x as f64).log(1024f64).floor() as usize;
+ let suffix = ["", "KB", "MB", "GB"];
+ format!("{} {}", x >> (10 * base), suffix[base])
+ }
+}
diff --git a/cavp/Readme.md b/cavp/Readme.md
@@ -0,0 +1,9 @@
+# Libcrux CAVP Utilities
+
+> The NIST Cryptographic Algorithm Validation Program (CAVP) provides validation testing of Approved (i.e., FIPS-approved and NIST-recommended) cryptographic algorithms and their individual components.
+
+- [NIST: Cryptographic Algorithm Validation
+ Program](https://csrc.nist.gov/projects/cryptographic-algorithm-validation-program)
+
+ This crate provides tooling around parsing and handling of CAVP test
+ vectors for `libcrux` crates.
diff --git a/formal_verification/vale-crypto/README.md b/formal_verification/vale-crypto/README.md
@@ -1,6 +1,6 @@
 # Vale Crypto in libcrux
 
-##Vale: Verified Assembly Language for Everest
+## Vale: Verified Assembly Language for Everest
 
 Vale is a tool for constructing formally verified high-performance assembly language code, with an emphasis on cryptographic code. It uses existing verification frameworks, such as Dafny and F*, for formal verification. It supports multiple architectures, such as x86, x64, and ARM, and multiple platforms, such as Windows, Mac, and Linux. Additional architectures and platforms can be supported with no changes to the Vale tool.
 Each assembly implementation in Vale is verified for:

diff --git a/libcrux-ecdh/Cargo.toml b/libcrux-ecdh/Cargo.toml
@@ -22,3 +22,6 @@ hex = { version = "0.4.3", features = ["serde"] }
 serde_json = { version = "1.0" }
 serde = { version = "1.0", features = ["derive"] }
 pretty_env_logger = "0.5"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(adx)', 'cfg(bmi2)'] }