gate ML‑KEM/ML‑DSA specific SHA3 APIs behind optional features (#1532)

.github/workflows/libcrux-build-test.yml

@@ -115,9 +115,15 @@ jobs:
       - name: 🏃🏻‍♀️ Test
         run: cargo test --verbose $RUST_TARGET_FLAG
 
+      - name: 🏃🏻‍♀️ Test SHA3 Incremental
+        run: cargo test -p libcrux-sha3 --features incremental --verbose $RUST_TARGET_FLAG
+
       - name: 🏃🏻‍♀️ Test Release
         run: cargo test --verbose --release $RUST_TARGET_FLAG
 
+      - name: 🏃🏻‍♀️ Test SHA3 Incremental Release
+        run: cargo test -p libcrux-sha3 --features incremental --verbose --release $RUST_TARGET_FLAG
+
   libcrux-build-test-status:
     if: ${{ always() }}
     needs: [build]

.github/workflows/mlkem-build-test.yml

@@ -104,25 +104,25 @@ jobs:
         working-directory: crates/algorithms/sha3
         run: |
           cargo clean
-          cargo test --verbose $RUST_TARGET_FLAG
+          cargo test --features incremental --verbose $RUST_TARGET_FLAG
 
       - name: 🏃🏻‍♀️ SHA3 Test Release
         working-directory: crates/algorithms/sha3
         run: |
           cargo clean
-          cargo test --release --verbose $RUST_TARGET_FLAG
+          cargo test --features incremental --release --verbose $RUST_TARGET_FLAG
 
       - name: 🏃🏻‍♀️ SHA3 Test Portable
         working-directory: crates/algorithms/sha3
         run: |
           cargo clean
-          LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --verbose $RUST_TARGET_FLAG
+          LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --features incremental --verbose $RUST_TARGET_FLAG
 
       - name: 🏃🏻‍♀️ SHA3 Test Portable Release
         working-directory: crates/algorithms/sha3
         run: |
           cargo clean
-          LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --verbose --release $RUST_TARGET_FLAG
+          LIBCRUX_DISABLE_SIMD128=1 LIBCRUX_DISABLE_SIMD256=1 cargo test --features incremental --verbose --release $RUST_TARGET_FLAG
 
       # Test ...
 

.github/workflows/workspace-test.yml

@@ -33,6 +33,9 @@ jobs:
       - name: Run workspace tests
         run: cargo nextest run --workspace --no-fail-fast -- --skip _mm256_bsrli_epi128
 
+      - name: Run libcrux-sha3 incremental tests
+        run: cargo nextest run -p libcrux-sha3 --features incremental --no-fail-fast
+
       - name: Run workspace doctests
         run: cargo test --doc --workspace --no-fail-fast
 

CHANGELOG.md

@@ -36,6 +36,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Changed
 
+- (libcrux-sha3) [#1532](https://github.com/celabshq/libcrux/issues/1532): Put ML-KEM/ML-DSA specific SHA3 APIs behind optional features
 - [#1534](https://github.com/celabshq/libcrux/pull/XYZ): Update dependencies: `libcrux-blake2`, `libcrux-sha3`, `libcrux-sha2`, `libcrux-curve25519`, `libcrux-aes`, `libcrux-chacha20poly1305`, `libcrux-ml-dsa`, `libcrux-ml-kem`, `libcrux-rsa`, `libcrux-ed25519`, `libcrux-digest`, `libcrux-hmac`, `libcrux-p256`, `libcrux-aead`, `libcrux-hkdf`, `libcrux-ecdsa`, `libcrux-ecdh`, `libcrux-kem`, `libcrux-psq`, `hpke-rs`
 - [#1505](https://github.com/celabshq/libcrux/pull/1505): Update dependency: `hpke-rs`
 - (libcrux-traits, libcrux-sha3, libcrux-sha2, libcrux-blake2) [#1493](https://github.com/celabshq/libcrux/pull/1493): `finish` methods on digest traits consume the hasher

crates/algorithms/kmac/Cargo.toml

@@ -15,7 +15,7 @@ path = "src/kmac.rs"
 
 [dependencies]
 hax-lib.workspace = true
-libcrux-sha3.workspace = true
+libcrux-sha3 = { workspace = true, features = ["incremental"] }
 
 [dev-dependencies]
 libcrux-kats = { workspace = true, features = ["kmac"] }

crates/algorithms/sha3/CHANGELOG.md

@@ -2,6 +2,9 @@
 
 All notable changes to this project will be documented in this file.
 
+## [Unreleased]
+- (libcrux-sha3) [#1532](https://github.com/celabshq/libcrux/issues/1532): Put ML-KEM/ML-DSA specific SHA3 APIs behind optional features
+
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 

crates/algorithms/sha3/Cargo.toml

@@ -22,6 +22,7 @@ hax-lib.workspace = true
 [features]
 simd128 = ["libcrux-intrinsics/simd128"]
 simd256 = ["libcrux-intrinsics/simd256"]
+incremental = []
 
 [[bench]]
 name = "sha3"

crates/algorithms/sha3/benches/sha3.rs

@@ -1,3 +1,4 @@
+#![cfg(feature = "incremental")]
 #![allow(non_snake_case)]
 use criterion::{criterion_group, criterion_main, BatchSize, BenchmarkId, Criterion, Throughput};
 use libcrux_sha3::{portable::incremental::Xof, *};

crates/algorithms/sha3/hax.sh

@@ -23,6 +23,7 @@ function extract_all() {
     # result is a fixed-length `t_Array u8 v_LEN`. An interface would erase that to
     # `t_Slice u8` with a trivial postcondition and the subtyping check fails.
     extract crates/algorithms/sha3 \
+        --features incremental \
         into -i "+**" \
         -i "-**::avx2::**" \
         -i "-**::arm64::**" \

crates/algorithms/sha3/src/avx2.rs

@@ -1,4 +1,5 @@
 /// Performing 4 operations in parallel
+#[cfg(feature = "incremental")]
 pub mod x4 {
     use crate::generic_keccak::simd256::keccak4;
 

crates/algorithms/sha3/src/generic_keccak/xof.rs

@@ -153,14 +153,14 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
 
             // ghost variables for F* proof
             #[cfg(hax)]
-            let self_buf_len = self.buf_len;
+            let _self_buf_len = self.buf_len;
             #[cfg(hax)]
-            let self_squeeze_pos = self.squeeze_pos;
+            let _self_squeeze_pos = self.squeeze_pos;
 
             #[allow(clippy::needless_range_loop)]
             for i in 0..PARALLEL_LANES {
                 hax_lib::loop_invariant!(|_: usize| {
-                    self.buf_len == self_buf_len && self.squeeze_pos == self_squeeze_pos
+                    self.buf_len == _self_buf_len && self.squeeze_pos == _self_squeeze_pos
                 });
 
                 self.buf[i][self.buf_len..].copy_from_slice(&inputs[i][..consumed]);
@@ -218,15 +218,15 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
         let remainder = input_to_consume % RATE;
 
         #[cfg(hax)]
-        let (self_buf_len, self_squeeze_pos, end) = {
+        let (_self_buf_len, _self_squeeze_pos, end) = {
             let end = consumed + num_blocks * RATE;
             hax_lib::assert!(end <= inputs[0].len());
             (self.buf_len, self.squeeze_pos, end)
         };
 
         for i in 0..num_blocks {
             hax_lib::loop_invariant!(
-                |_: usize| self.buf_len == self_buf_len && self.squeeze_pos == self_squeeze_pos
+                |_: usize| self.buf_len == _self_buf_len && self.squeeze_pos == _self_squeeze_pos
             );
             #[cfg(hax)]
             crate::proof_utils::lemma_mul_succ_le(i, num_blocks, RATE);
@@ -278,15 +278,14 @@ impl<const PARALLEL_LANES: usize, const RATE: usize, STATE: KeccakItem<PARALLEL_
             let input_len = inputs[0].len();
 
             #[cfg(hax)]
-            let self_buf_len = self.buf_len;
+            let _self_buf_len = self.buf_len;
             #[cfg(hax)]
-            let self_squeeze_pos = self.squeeze_pos;
+            let _self_squeeze_pos = self.squeeze_pos;
 
             #[allow(clippy::needless_range_loop)]
             for i in 0..PARALLEL_LANES {
-                hax_lib::loop_invariant!(
-                    |_: usize| self.buf_len == self_buf_len && self.squeeze_pos == self_squeeze_pos
-                );
+                hax_lib::loop_invariant!(|_: usize| self.buf_len == _self_buf_len
+                    && self.squeeze_pos == _self_squeeze_pos);
 
                 self.buf[i][self.buf_len..self.buf_len + remainder]
                     .copy_from_slice(&inputs[i][input_len - remainder..input_len]);
@@ -398,15 +397,15 @@ impl<const RATE: usize, STATE: KeccakItem<1>> KeccakXofState<1, RATE, STATE> {
             self.inner.squeeze::<RATE>(out, out_offset, RATE);
 
             #[cfg(hax)]
-            let self_buf_len = self.buf_len;
+            let _self_buf_len = self.buf_len;
             #[cfg(hax)]
-            let self_squeeze_pos = self.squeeze_pos;
+            let _self_squeeze_pos = self.squeeze_pos;
 
             // Apply f then extract for each subsequent full block.
             for i in 1..blocks {
                 hax_lib::loop_invariant!(|_: usize| out.len() == out_len
-                    && self_buf_len == self.buf_len
-                    && self_squeeze_pos == self.squeeze_pos);
+                    && _self_buf_len == self.buf_len
+                    && _self_squeeze_pos == self.squeeze_pos);
                 #[cfg(hax)]
                 hax_lib::assert!(
                     out_offset.to_int() + i.to_int() * RATE.to_int() <= out.len().to_int()

crates/algorithms/sha3/src/neon.rs

@@ -49,6 +49,7 @@ pub fn shake256<const LEN: usize>(digest: &mut [u8; LEN], data: &[u8]) {
 }
 
 /// Performing 2 operations in parallel
+#[cfg(feature = "incremental")]
 pub mod x2 {
     use super::*;
 

crates/algorithms/sha3/src/portable.rs

@@ -48,4 +48,5 @@ pub fn shake256(digest: &mut [u8], data: &[u8]) {
 }
 
 /// An incremental API for SHAKE
+#[cfg(feature = "incremental")]
 pub mod incremental;

crates/algorithms/sha3/src/proof_utils.rs

@@ -12,6 +12,7 @@ pub(crate) fn valid_rate(rate: usize) -> bool {
     rate != 0 && rate <= 200 && rate % 8 == 0 && (rate % 32 == 8 || rate % 32 == 16)
 }
 
+#[allow(unused_imports)]
 pub(crate) use lemmas::{lemma_div_mul_mod, lemma_mul_succ_le};
 
 mod lemmas {
@@ -37,6 +38,7 @@ let lemma_div_mul_mod (a b: usize)
     = ()
 "#
     )]
+    #[allow(dead_code)]
     pub(crate) fn lemma_div_mul_mod(_a: usize, _b: usize) {}
 
     /// Lemma proving multiplication bounds for successive elements.

crates/algorithms/sha3/src/simd/portable.rs

@@ -121,10 +121,10 @@ pub(crate) fn store_block<const RATE: usize>(
     let octets = len / 8;
 
     #[cfg(hax)]
-    let out_len = out.len(); // ghost variable
+    let _out_len = out.len(); // ghost variable
 
     for i in 0..octets {
-        hax_lib::loop_invariant!(|i: usize| out.len() == out_len);
+        hax_lib::loop_invariant!(|i: usize| out.len() == _out_len);
 
         let bytes = get_ij(s, i / 5, i % 5).to_le_bytes();
         let out_pos = start + 8 * i;

crates/algorithms/sha3/tests/avx2.rs

@@ -1,4 +1,4 @@
-#![cfg(feature = "simd256")]
+#![cfg(all(feature = "simd256", feature = "incremental"))]
 
 mod test_vectors;
 

crates/algorithms/sha3/tests/cavp.rs

@@ -137,6 +137,7 @@ shake_vo_test!(
     shake256_ema
 );
 
+#[cfg(feature = "incremental")]
 macro_rules! shake_vo_test_incremental {
     ($name:ident, $kats_fn:path, $shake:ty) => {
         #[test]
@@ -159,11 +160,13 @@ macro_rules! shake_vo_test_incremental {
     };
 }
 
+#[cfg(feature = "incremental")]
 shake_vo_test_incremental!(
     SHAKE128VariableOut_incremental,
     libcrux_kats::sha3::shake128_variable_out,
     libcrux_sha3::portable::incremental::Shake128Xof
 );
+#[cfg(feature = "incremental")]
 shake_vo_test_incremental!(
     SHAKE256VariableOut_incremental,
     libcrux_kats::sha3::shake256_variable_out,
@@ -241,7 +244,7 @@ sha3_neon_test!(
 macro_rules! shake128_neon_test {
     ($test_name:ident, $kats_fn:path) => {
         #[test]
-        #[cfg(feature = "simd128")]
+        #[cfg(all(feature = "simd128", feature = "incremental"))]
         #[allow(non_snake_case)]
         fn $test_name() {
             let _ = pretty_env_logger::try_init();
@@ -270,7 +273,7 @@ shake128_neon_test!(neon_SHAKE128LongMsg, libcrux_kats::sha3::shake128_long);
 macro_rules! shake256_neon_test {
     ($test_name:ident, $kats_fn:path) => {
         #[test]
-        #[cfg(feature = "simd128")]
+        #[cfg(all(feature = "simd128", feature = "incremental"))]
         #[allow(non_snake_case)]
         fn $test_name() {
             let _ = pretty_env_logger::try_init();
@@ -297,7 +300,7 @@ shake256_neon_test!(neon_SHAKE256LongMsg, libcrux_kats::sha3::shake256_long);
 macro_rules! shake256_vo_neon_test {
     ($test_name:ident, $kats_fn:path) => {
         #[test]
-        #[cfg(feature = "simd128")]
+        #[cfg(all(feature = "simd128", feature = "incremental"))]
         #[allow(non_snake_case)]
         fn $test_name() {
             let _ = pretty_env_logger::try_init();
@@ -326,7 +329,7 @@ shake256_vo_neon_test!(
 macro_rules! shake256_avx2_test {
     ($test_name:ident, $kats_fn:path) => {
         #[test]
-        #[cfg(feature = "simd256")]
+        #[cfg(all(feature = "simd256", feature = "incremental"))]
         #[allow(non_snake_case)]
         fn $test_name() {
             let _ = pretty_env_logger::try_init();
@@ -359,7 +362,7 @@ shake256_avx2_test!(avx2_SHAKE256LongMsg, libcrux_kats::sha3::shake256_long);
 macro_rules! shake256_vo_avx2_test {
     ($test_name:ident, $kats_fn:path) => {
         #[test]
-        #[cfg(feature = "simd256")]
+        #[cfg(all(feature = "simd256", feature = "incremental"))]
         #[allow(non_snake_case)]
         fn $test_name() {
             let _ = pretty_env_logger::try_init();

crates/algorithms/sha3/tests/cross_spec.rs

@@ -368,7 +368,7 @@ mod neon_cross_spec {
 // AVX2 (simd256) — cross-spec via x4 incremental API
 // =========================================================================
 
-#[cfg(feature = "simd256")]
+#[cfg(all(feature = "simd256", feature = "incremental"))]
 mod avx2_cross_spec {
     #[test]
     fn avx2_x4_shake256_matches_spec() {

crates/algorithms/sha3/tests/neon.rs

@@ -1,4 +1,4 @@
-#![cfg(feature = "simd128")]
+#![cfg(all(feature = "simd128", feature = "incremental"))]
 
 mod test_vectors;