ml kem crate and simd setup

Cargo.toml

@@ -7,6 +7,9 @@ members = [
     "sys/lib25519",
     "benchmarks",
     "fuzz",
+    "libcrux-ml-kem",
+    "libcrux-simd",
+    "libcrux-sha3",
 ]
 
 [workspace.package]

libcrux-ml-kem/.gitignore

@@ -0,0 +1 @@
+Cargo.lock

libcrux-ml-kem/Cargo.toml

@@ -0,0 +1,35 @@
+[package]
+name = "libcrux-ml-kem"
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+homepage.workspace = true
+edition.workspace = true
+repository.workspace = true
+readme.workspace = true
+exclude = ["/tests", "/implementation_notes.pdf"]
+
+[dependencies]
+rand_core = { version = "0.6" }
+libcrux-platform = { version = "0.0.2-pre.2", path = "../sys/platform" }
+libcrux-sha3 = { version = "0.0.2-pre.2", path = "../libcrux-sha3" }
+
+# This is only required for verification.
+# The hax config is set by the hax toolchain.
+[target.'cfg(hax)'.dependencies]
+hax-lib = { git = "https://github.com/hacspec/hax/" }
+
+[features]
+simd128 = []
+simd256 = []
+
+[dev-dependencies]
+rand = { version = "0.8" }
+serde_json = { version = "1.0" }
+serde = { version = "1.0", features = ["derive"] }
+hex = { version = "0.4.3", features = ["serde"] }
+criterion = "0.5"
+
+[[bench]]
+name = "ml-kem"
+harness = false

libcrux-ml-kem/benches/ml-kem.rs

@@ -0,0 +1,165 @@
+use std::hint::black_box;
+use std::time::Duration;
+
+use criterion::{criterion_group, criterion_main, BatchSize, Criterion};
+use rand_core::OsRng;
+use rand_core::RngCore;
+
+use libcrux_ml_kem::kyber768;
+
+pub fn comparisons_key_generation(c: &mut Criterion) {
+    let mut rng = OsRng;
+    let mut group = c.benchmark_group("Kyber768 Key Generation");
+    group.measurement_time(Duration::from_secs(10));
+
+    group.bench_function("libcrux portable (external random)", |b| {
+        let mut seed = [0; 64];
+        rng.fill_bytes(&mut seed);
+        b.iter(|| {
+            let _kp = kyber768::generate_key_pair(seed);
+        })
+    });
+
+    // group.bench_function("libcrux portable (HACL-DRBG)", |b| {
+    //     b.iter(|| {
+    //         let (_secret_key, _public_key) =
+    //             libcrux::kem::key_gen(Algorithm::MlKem768, &mut drbg).unwrap();
+    //     })
+    // });
+
+    // group.bench_function("libcrux portable (OsRng)", |b| {
+    //     b.iter(|| {
+    //         let (_secret_key, _public_key) =
+    //             libcrux::kem::key_gen(Algorithm::MlKem768, &mut rng).unwrap();
+    //     })
+    // });
+
+    // group.bench_function("pqclean reference implementation", |b| {
+    //     b.iter(|| {
+    //         let (_public_key, _secret_key) = pqcrypto_kyber::kyber768::keypair();
+    //     })
+    // });
+}
+
+pub fn comparisons_pk_validation(c: &mut Criterion) {
+    let mut rng = OsRng;
+    let mut group = c.benchmark_group("Kyber768 PK Validation");
+    group.measurement_time(Duration::from_secs(10));
+
+    group.bench_function("libcrux portable", |b| {
+        let mut seed = [0; 64];
+        rng.fill_bytes(&mut seed);
+        b.iter_batched(
+            || {
+                let keypair = kyber768::generate_key_pair(seed);
+                keypair.public_key().as_slice().into()
+            },
+            |public_key| {
+                let _valid = black_box(kyber768::validate_public_key(public_key));
+            },
+            BatchSize::SmallInput,
+        )
+    });
+}
+
+pub fn comparisons_encapsulation(c: &mut Criterion) {
+    let mut group = c.benchmark_group("Kyber768 Encapsulation");
+    group.measurement_time(Duration::from_secs(10));
+
+    group.bench_function("libcrux portable (external random)", |b| {
+        let mut seed1 = [0; 64];
+        OsRng.fill_bytes(&mut seed1);
+        let mut seed2 = [0; 32];
+        OsRng.fill_bytes(&mut seed2);
+        b.iter_batched(
+            || kyber768::generate_key_pair(seed1),
+            |keypair| {
+                let (_shared_secret, _ciphertext) =
+                    kyber768::encapsulate(keypair.public_key(), seed2);
+            },
+            BatchSize::SmallInput,
+        )
+    });
+
+    // group.bench_function("libcrux portable", |b| {
+    //     b.iter_batched(
+    //         || {
+    //             let mut drbg = Drbg::new(digest::Algorithm::Sha256).unwrap();
+    //             let (_secret_key, public_key) =
+    //                 libcrux::kem::key_gen(Algorithm::MlKem768, &mut drbg).unwrap();
+
+    //             (drbg, public_key)
+    //         },
+    //         |(mut rng, public_key)| {
+    //             let (_shared_secret, _ciphertext) = public_key.encapsulate(&mut rng).unwrap();
+    //         },
+    //         BatchSize::SmallInput,
+    //     )
+    // });
+
+    // group.bench_function("pqclean reference implementation", |b| {
+    //     b.iter_batched(
+    //         || {
+    //             let (public_key, _secret_key) = pqcrypto_kyber::kyber768::keypair();
+
+    //             public_key
+    //         },
+    //         |public_key| {
+    //             let (_shared_secret, _ciphertext) =
+    //                 pqcrypto_kyber::kyber768::encapsulate(&public_key);
+    //         },
+    //         BatchSize::SmallInput,
+    //     )
+    // });
+}
+
+pub fn comparisons_decapsulation(c: &mut Criterion) {
+    let mut group = c.benchmark_group("Kyber768 Decapsulation");
+    group.measurement_time(Duration::from_secs(10));
+
+    group.bench_function("libcrux portable", |b| {
+        let mut seed1 = [0; 64];
+        OsRng.fill_bytes(&mut seed1);
+        let mut seed2 = [0; 32];
+        OsRng.fill_bytes(&mut seed2);
+        b.iter_batched(
+            || {
+                let keypair = kyber768::generate_key_pair(seed1);
+                let (ciphertext, _shared_secret) =
+                    kyber768::encapsulate(keypair.public_key(), seed2);
+                (keypair, ciphertext)
+            },
+            |(keypair, ciphertext)| {
+                let _shared_secret = kyber768::decapsulate(keypair.private_key(), &ciphertext);
+            },
+            BatchSize::SmallInput,
+        )
+    });
+
+    // group.bench_function("pqclean reference implementation", |b| {
+    //     b.iter_batched(
+    //         || {
+    //             let (public_key, secret_key) = pqcrypto_kyber::kyber768::keypair();
+    //             let (_shared_secret, ciphertext) =
+    //                 pqcrypto_kyber::kyber768::encapsulate(&public_key);
+
+    //             (ciphertext, secret_key)
+    //         },
+    //         |(ciphertext, secret_key)| {
+    //             let _shared_secret =
+    //                 pqcrypto_kyber::kyber768::decapsulate(&ciphertext, &secret_key);
+    //         },
+    //         BatchSize::SmallInput,
+    //     )
+    // });
+}
+
+pub fn comparisons(c: &mut Criterion) {
+    comparisons_pk_validation(c);
+    comparisons_key_generation(c);
+    comparisons_encapsulation(c);
+    comparisons_decapsulation(c);
+}
+
+criterion_group!(benches, comparisons);
+criterion_main!(benches);

libcrux-ml-kem/c.sh

@@ -0,0 +1,28 @@
+rm -rf c
+
+if [[ -z "$CHARON_HOME" ]]; then
+    echo "Please set CHARON_HOME to the Charon directory" 1>&2
+    exit 1
+fi
+if [[ -z "$EURYDICE_HOME" ]]; then
+    echo "Please set EURYDICE_HOME to the Eurydice directory" 1>&2
+    exit 1
+fi
+
+echo "Running charon ..."
+$CHARON_HOME/bin/charon --errors-as-warnings
+mkdir -p c
+cd c
+
+echo "Running eurydice ..."
+$EURYDICE_HOME/eurydice --config ../c.yaml ../libcrux_kyber.llbc
+cp $EURYDICE_HOME/include/eurydice_glue.h .
+
+if [[ -n "$HACL_PACKAGES_HOME" ]]; then
+    clang-format --style=Mozilla -i libcrux_kyber.c libcrux_kyber.h
+    cp internal/*.h $HACL_PACKAGES_HOME/libcrux/include/internal/
+    cp *.h $HACL_PACKAGES_HOME/libcrux/include
+    cp *.c $HACL_PACKAGES_HOME/libcrux/src
+else
+    echo "Please set HACL_PACKAGES_HOME to the hacl-packages directory to copy the code over" 1>&2
+fi

libcrux-ml-kem/c.yaml

@@ -0,0 +1,19 @@
+files:
+  - name: libcrux_digest
+    api:
+      - [libcrux, digest]
+    include_in_h:
+      - '"libcrux_hacl_glue.h"'
+  - name: libcrux_platform
+    api:
+      - [libcrux_platform]
+  - name: libcrux_kyber
+    api:
+      - [libcrux_kyber, kyber768]
+    private:
+      - [libcrux_kyber, "*"]
+    include_in_c:
+      - '"libcrux_hacl_glue.h"'
+  - name: core
+    private:
+      - [core, "*"]

libcrux-ml-kem/hax.py

@@ -0,0 +1,126 @@
+#! /usr/bin/env python3
+
+import os
+import argparse
+import subprocess
+import sys
+
+
+def shell(command, expect=0, cwd=None, env={}):
+    subprocess_stdout = subprocess.DEVNULL
+
+    print("Env:", env)
+    print("Command: ", end="")
+    for i, word in enumerate(command):
+        if i == 4:
+            print("'{}' ".format(word), end="")
+        else:
+            print("{} ".format(word), end="")
+
+    print("\nDirectory: {}".format(cwd))
+
+    os_env = os.environ
+    os_env.update(env)
+
+    ret = subprocess.run(command, cwd=cwd, env=os_env)
+    if ret.returncode != expect:
+        raise Exception("Error {}. Expected {}.".format(ret, expect))
+
+
+class extractAction(argparse.Action):
+
+    def __call__(self, parser, args, values, option_string=None) -> None:
+        # Extract platform and sha3 interfaces
+        # XXX: This currently is impossible.
+        include_str = "-* +!* -libcrux_sha3::* -libcrux_sha3::x4::internal::*"
+        interface_include = "+* -libcrux_sha3::x4::internal::**"
+        cargo_hax_into = [
+            "cargo",
+            "hax",
+            "into",
+            "-i",
+            include_str,
+            "fstar",
+            "--interfaces",
+            interface_include,
+        ]
+        hax_env = {}
+        shell(
+            cargo_hax_into,
+            cwd="../libcrux-sha3",
+            env=hax_env,
+        )
+
+        # Extract ml-kem
+        include_str = "-libcrux_platform::macos_arm::* +!libcrux_platform::platform::* -libcrux_ml_kem::types::index_impls::**"
+        interface_include = "+* -libcrux::kem::kyber::types +!libcrux_platform::** +!libcrux::digest::**"
+        cargo_hax_into = [
+            "cargo",
+            "hax",
+            "into",
+            "-i",
+            include_str,
+            "fstar",
+            "--interfaces",
+            interface_include,
+        ]
+        hax_env = {}
+        shell(
+            cargo_hax_into,
+            cwd=".",
+            env=hax_env,
+        )
+        return None
+
+
+class proveAction(argparse.Action):
+
+    def __call__(self, parser, args, values, option_string=None) -> None:
+        admit_env = {}
+        if args.admit:
+            admit_env = {"OTHERFLAGS": "--admit_smt_queries true"}
+        shell(["make", "-C", "proofs/fstar/extraction/"], env=admit_env)
+        return None
+
+
+def parse_arguments():
+    parser = argparse.ArgumentParser(
+        description="Libcrux prove script. "
+        + "Make sure to separate sub-command arguments with --."
+    )
+    subparsers = parser.add_subparsers()
+
+    extract_parser = subparsers.add_parser(
+        "extract", help="Extract the F* code for the proofs."
+    )
+    extract_parser.add_argument("extract", nargs="*", action=extractAction)
+
+    prover_parser = subparsers.add_parser(
+        "prove",
+        help="""
+        Run F*.
+
+        This typechecks the extracted code.
+        To lax-typecheck use --admit.
+        """,
+    )
+    prover_parser.add_argument(
+        "--admit",
+        help="Admit all smt queries to lax typecheck.",
+        action="store_true",
+    )
+    prover_parser.add_argument(
+        "prove",
+        nargs="*",
+        action=proveAction,
+    )
+
+    return parser.parse_args()
+
+
+def main():
+    parse_arguments()
+
+
+if __name__ == "__main__":
+    main()