address PR feedback

Cargo.toml

@@ -1,28 +1,28 @@
 [workspace]
 members = [
-    "sys/hacl",
-    "sys/libjade",
-    "sys/platform",
-    "sys/pqclean",
-    "sys/lib25519",
-    "benchmarks",
-    "fuzz",
-    "libcrux-ml-kem",
-    "libcrux-ml-kem/fuzz",
-    "libcrux-sha3",
-    "libcrux-ml-dsa",
-    "libcrux-intrinsics",
-    "libcrux-kem",
-    "libcrux-hmac",
-    "libcrux-hkdf",
-    "libcrux-ecdh",
-    "libcrux-psq",
-    "libcrux-hacl-rs-krml",
-    "cavp",
-    "libcrux-traits",
-    "libcrux-sha2",
-    "libcrux-ed25519",
-    "libcrux-curve25519",
+  "sys/hacl",
+  "sys/libjade",
+  "sys/platform",
+  "sys/pqclean",
+  "sys/lib25519",
+  "benchmarks",
+  "fuzz",
+  "libcrux-ml-kem",
+  "libcrux-ml-kem/fuzz",
+  "libcrux-sha3",
+  "libcrux-ml-dsa",
+  "libcrux-intrinsics",
+  "libcrux-kem",
+  "libcrux-hmac",
+  "libcrux-hkdf",
+  "libcrux-ecdh",
+  "libcrux-psq",
+  "macros",
+  "cavp",
+  "traits",
+  "sha2",
+  "ed25519",
+  "curve25519",
 ]
 
 [workspace.package]
@@ -49,15 +49,15 @@ readme.workspace = true
 documentation = "https://docs.rs/libcrux/"
 description = "The Formally Verified Cryptography Library"
 exclude = [
-    "/tests",
-    "/specs",
-    "/proofs",
-    "/*.py",
-    "/wasm-demo",
-    "/fuzz",
-    "/git-hooks",
-    "/architecture",
-    "/libcrux.fst.config.json",
+  "/tests",
+  "/specs",
+  "/proofs",
+  "/*.py",
+  "/wasm-demo",
+  "/fuzz",
+  "/git-hooks",
+  "/architecture",
+  "/libcrux.fst.config.json",
 ]
 
 [lib]
@@ -68,14 +68,14 @@ bench = false                               # so libtest doesn't eat the argumen
 libcrux-platform = { version = "=0.0.2-beta.2", path = "sys/platform" }
 
 [dependencies]
-libcrux-traits = { path = "libcrux-traits" }
-libcrux-hacl-rs = { path = "libcrux-hacl-rs" }
+libcrux-traits = { version = "=0.0.2-beta.2", path = "traits" }
+libcrux-hacl-rs = { version = "=0.0.2-beta.2", path = "hacl-rs" }
 libcrux-hacl = { version = "=0.0.2-beta.2", path = "sys/hacl" }
 libcrux-platform = { version = "=0.0.2-beta.2", path = "sys/platform" }
 libcrux-hkdf = { version = "=0.0.2-beta.2", path = "libcrux-hkdf" }
 libcrux-hmac = { version = "=0.0.2-beta.2", path = "libcrux-hmac" }
-libcrux-sha2 = { path = "libcrux-sha2" }
-libcrux-ed25519 = { path = "libcrux-ed25519" }
+libcrux-sha2 = { version = "=0.0.2-beta.2", path = "sha2" }
+libcrux-ed25519 = { version = "=0.0.2-beta.2", path = "ed25519" }
 libcrux-ecdh = { version = "=0.0.2-beta.2", path = "libcrux-ecdh" }
 libcrux-ml-kem = { version = "=0.0.2-beta.2", path = "libcrux-ml-kem" }
 libcrux-kem = { version = "=0.0.2-beta.2", path = "libcrux-kem" }
@@ -123,11 +123,11 @@ panic = "abort"
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = [
-    'cfg(hax)',
-    'cfg(eurydice)',
-    'cfg(doc_cfg)',
-    'cfg(libjade)',
-    'cfg(simd128)',
-    'cfg(simd256)',
-    'cfg(aes_ni)',
+  'cfg(hax)',
+  'cfg(eurydice)',
+  'cfg(doc_cfg)',
+  'cfg(libjade)',
+  'cfg(simd128)',
+  'cfg(simd256)',
+  'cfg(aes_ni)',
 ] }

curve25519/Cargo.toml

@@ -0,0 +1,23 @@
+[package]
+name = "libcrux-curve25519"
+description = "Formally verified curve25519 ECDH library"
+
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+homepage.workspace = true
+edition.workspace = true
+repository.workspace = true
+readme.workspace = true
+
+[features]
+default = ["portable_hacl"]
+portable_hacl = ["hacl"]
+hacl = ["dep:libcrux-sha2", "dep:libcrux-hacl-rs", "dep:libcrux-macros"]
+
+[dependencies]
+libcrux-hacl-rs = { version = "=0.0.2-beta.2", path = "../hacl-rs/", optional = true }
+libcrux-sha2 = { version = "=0.0.2-beta.2", path = "../sha2", optional = true, features = [
+  "hacl",
+] }
+libcrux-macros = { version = "=0.0.2-beta.2", path = "../macros", optional = true }

ed25519/Cargo.toml

@@ -0,0 +1,23 @@
+[package]
+name = "libcrux-ed25519"
+description = "Formally verified ed25519 signature library"
+
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+homepage.workspace = true
+edition.workspace = true
+repository.workspace = true
+readme.workspace = true
+
+[features]
+default = ["portable_hacl"]
+portable_hacl = ["hacl"]
+hacl = ["dep:libcrux-sha2", "dep:libcrux-hacl-rs", "dep:libcrux-macros"]
+
+[dependencies]
+libcrux-hacl-rs = { version = "=0.0.2-beta.2", path = "../hacl-rs/", optional = true }
+libcrux-sha2 = { version = "=0.0.2-beta.2", path = "../sha2", optional = true, features = [
+  "hacl",
+] }
+libcrux-macros = { version = "=0.0.2-beta.2", path = "../macros", optional = true }

libcrux-ed25519/src/hacl/ed25519.rs → ed25519/src/hacl/ed25519.rs

@@ -4,6 +4,8 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
+use libcrux_macros as krml;
+
 use libcrux_hacl_rs::bignum;
 use libcrux_hacl_rs::fstar;
 use libcrux_hacl_rs::lowstar;
@@ -1255,70 +1257,6 @@ pub(crate) fn point_negate(p: &[u64], out: &mut [u64]) {
     crate::hacl::ed25519::reduce_513(t1.1)
 }
 
-pub(crate) fn point_mul(out: &mut [u64], scalar: &[u8], q: &[u64]) {
-    let mut bscalar: [u64; 4] = [0u64; 4usize];
-    krml::unroll_for!(4, "i", 0u32, 1u32, {
-        let bj: (&[u8], &[u8]) = scalar.split_at(i.wrapping_mul(8u32) as usize);
-        let u: u64 = lowstar::endianness::load64_le(bj.1);
-        let r: u64 = u;
-        let x: u64 = r;
-        let os: (&mut [u64], &mut [u64]) = bscalar.split_at_mut(0usize);
-        os.1[i as usize] = x
-    });
-    let mut table: [u64; 320] = [0u64; 320usize];
-    let mut tmp: [u64; 20] = [0u64; 20usize];
-    let t0: (&mut [u64], &mut [u64]) = table.split_at_mut(0usize);
-    let t1: (&mut [u64], &mut [u64]) = t0.1.split_at_mut(20usize);
-    crate::hacl::ed25519::make_point_inf(t1.0);
-    (t1.1[0usize..20usize]).copy_from_slice(&q[0usize..20usize]);
-    lowstar::ignore::ignore::<&[u64]>(&table);
-    krml::unroll_for!(7, "i", 0u32, 1u32, {
-        let t11: (&[u64], &[u64]) =
-            table.split_at(i.wrapping_add(1u32).wrapping_mul(20u32) as usize);
-        let mut p_copy: [u64; 20] = [0u64; 20usize];
-        ((&mut p_copy)[0usize..20usize]).copy_from_slice(&t11.1[0usize..20usize]);
-        crate::hacl::ed25519::point_double(&mut tmp, &p_copy);
-        ((&mut table)[2u32.wrapping_mul(i).wrapping_add(2u32).wrapping_mul(20u32) as usize
-            ..2u32.wrapping_mul(i).wrapping_add(2u32).wrapping_mul(20u32) as usize + 20usize])
-            .copy_from_slice(&(&tmp)[0usize..20usize]);
-        let t2: (&[u64], &[u64]) =
-            table.split_at(2u32.wrapping_mul(i).wrapping_add(2u32).wrapping_mul(20u32) as usize);
-        let mut p_copy0: [u64; 20] = [0u64; 20usize];
-        ((&mut p_copy0)[0usize..20usize]).copy_from_slice(&q[0usize..20usize]);
-        crate::hacl::ed25519::point_add(&mut tmp, &p_copy0, t2.1);
-        ((&mut table)[2u32.wrapping_mul(i).wrapping_add(3u32).wrapping_mul(20u32) as usize
-            ..2u32.wrapping_mul(i).wrapping_add(3u32).wrapping_mul(20u32) as usize + 20usize])
-            .copy_from_slice(&(&tmp)[0usize..20usize])
-    });
-    crate::hacl::ed25519::make_point_inf(out);
-    let mut tmp0: [u64; 20] = [0u64; 20usize];
-    for i in 0u32..64u32 {
-        krml::unroll_for!(4, "_i", 0u32, 1u32, {
-            let mut p_copy: [u64; 20] = [0u64; 20usize];
-            ((&mut p_copy)[0usize..20usize]).copy_from_slice(&out[0usize..20usize]);
-            crate::hacl::ed25519::point_double(out, &p_copy)
-        });
-        let k: u32 = 256u32.wrapping_sub(4u32.wrapping_mul(i)).wrapping_sub(4u32);
-        let bits_l: u64 = bignum::bignum_base::bn_get_bits_u64(4u32, &bscalar, k, 4u32);
-        lowstar::ignore::ignore::<&[u64]>(&table);
-        ((&mut tmp0)[0usize..20usize])
-            .copy_from_slice(&(&(&table)[0usize..] as &[u64])[0usize..20usize]);
-        krml::unroll_for!(15, "i0", 0u32, 1u32, {
-            let c: u64 = fstar::uint64::eq_mask(bits_l, i0.wrapping_add(1u32) as u64);
-            let res_j: (&[u64], &[u64]) =
-                table.split_at(i0.wrapping_add(1u32).wrapping_mul(20u32) as usize);
-            krml::unroll_for!(20, "i1", 0u32, 1u32, {
-                let x: u64 = c & res_j.1[i1 as usize] | !c & (&tmp0)[i1 as usize];
-                let os: (&mut [u64], &mut [u64]) = tmp0.split_at_mut(0usize);
-                os.1[i1 as usize] = x
-            })
-        });
-        let mut p_copy: [u64; 20] = [0u64; 20usize];
-        ((&mut p_copy)[0usize..20usize]).copy_from_slice(&out[0usize..20usize]);
-        crate::hacl::ed25519::point_add(out, &p_copy, &tmp0)
-    }
-}
-
 #[inline]
 fn precomp_get_consttime(table: &[u64], bits_l: u64, tmp: &mut [u64]) {
     (tmp[0usize..20usize]).copy_from_slice(&(&table[0usize..])[0usize..20usize]);

hacl-rs/Cargo.toml

@@ -0,0 +1,18 @@
+[package]
+name = "libcrux-hacl-rs"
+description = "Formally verified Rust code extracted from HACL* - helper library"
+
+version.workspace = true
+authors.workspace = true
+license.workspace = true
+homepage.workspace = true
+edition.workspace = true
+repository.workspace = true
+readme.workspace = true
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+libcrux-macros = { path = "../macros", version = "=0.0.2-beta.2" }
+
+[lib]

libcrux-hacl-rs/src/bignum/bignum.rs → hacl-rs/src/bignum/bignum.rs

@@ -4,6 +4,8 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
+use libcrux_macros as krml;
+
 use crate::fstar;
 use crate::lowstar;
 use crate::util as lib;

libcrux-hacl-rs/src/bignum/bignum256.rs → hacl-rs/src/bignum/bignum256.rs

@@ -4,6 +4,8 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
+use libcrux_macros as krml;
+
 use crate::fstar;
 use crate::lowstar;
 use crate::util as lib;

libcrux-hacl-rs/src/bignum/bignum256_32.rs → hacl-rs/src/bignum/bignum256_32.rs

@@ -4,6 +4,8 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
+use libcrux_macros as krml;
+
 use crate::fstar;
 use crate::lowstar;
 use crate::util as lib;

libcrux-hacl-rs/src/bignum/bignum4096.rs → hacl-rs/src/bignum/bignum4096.rs

@@ -4,6 +4,8 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
+use libcrux_macros as krml;
+
 use crate::fstar;
 use crate::lowstar;
 use crate::util as lib;

libcrux-hacl-rs/src/bignum/bignum4096_32.rs → hacl-rs/src/bignum/bignum4096_32.rs

@@ -4,6 +4,8 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
+use libcrux_macros as krml;
+
 use crate::fstar;
 use crate::lowstar;
 use crate::util as lib;

libcrux-hacl-rs/src/bignum25519_51.rs → hacl-rs/src/bignum25519_51.rs

@@ -4,6 +4,8 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
+use libcrux_macros as krml;
+
 use crate::fstar;
 use crate::lowstar;
 

libcrux-hacl-rs/src/curve25519_51.rs → hacl-rs/src/curve25519_51.rs

@@ -4,6 +4,8 @@
 #![allow(unused_assignments)]
 #![allow(unreachable_patterns)]
 
+use libcrux_macros as krml;
+
 use crate::fstar;
 use crate::lowstar;