add hacl-rs hashing code, make libcrux use hacl-rs impl for sha2

Cargo.toml

@@ -1,23 +1,23 @@
 [workspace]
 members = [
-    "sys/hacl",
-    "sys/libjade",
-    "sys/platform",
-    "sys/pqclean",
-    "sys/lib25519",
-    "benchmarks",
-    "fuzz",
-    "libcrux-ml-kem",
-    "libcrux-sha3",
-    "libcrux-ml-dsa",
-    "libcrux-intrinsics",
-    "libcrux-kem",
-    "libcrux-hmac",
-    "libcrux-hkdf",
-    "libcrux-ecdh",
-    "libcrux-psq",
-    "cavp",
+  "sys/hacl",
+  "sys/libjade",
+  "sys/platform",
+  "sys/pqclean",
+  "sys/lib25519",
+  "benchmarks",
+  "fuzz",
+  "libcrux-ml-kem",
+  "libcrux-sha3",
+  "libcrux-ml-dsa",
+  "libcrux-intrinsics",
+  "libcrux-kem",
+  "libcrux-hmac",
+  "libcrux-hkdf",
+  "libcrux-ecdh",
+  "libcrux-psq",
   "libcrux-hacl-rs-krml",
+  "cavp",
 ]
 
 [workspace.package]
@@ -44,15 +44,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]
@@ -63,6 +63,7 @@ bench = false                               # so libtest doesn't eat the argumen
 libcrux-platform = { version = "=0.0.2-beta.2", path = "sys/platform" }
 
 [dependencies]
+krml = { package = "libcrux-hacl-rs-krml", path = "libcrux-hacl-rs-krml" }
 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" }
@@ -113,11 +114,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)',
 ] }

src/digest.rs

@@ -291,10 +291,52 @@ macro_rules! impl_streaming {
     };
 }
 impl_streaming!(Sha2_224, Sha224, Sha2_224Digest);
-impl_streaming!(Sha2_256, Sha256, Sha2_256Digest);
 impl_streaming!(Sha2_384, Sha384, Sha2_384Digest);
 impl_streaming!(Sha2_512, Sha512, Sha2_512Digest);
 
+// Streaming API - This is the recommended one.
+// For implementations based on hacl_rs (over hacl-c)
+macro_rules! impl_streaming_hacl_rs {
+    ($name:ident, $state:ty, $result:ty) => {
+        #[derive(Clone)]
+        pub struct $name {
+            state: $state,
+        }
+        impl $name {
+            /// Initialize a new digest state.
+            pub fn new() -> Self {
+                Self {
+                    state: <$state>::new(),
+                }
+            }
+
+            /// Add the `payload` to the digest.
+            pub fn update(&mut self, payload: &[u8]) {
+                self.state.update(payload);
+            }
+
+            /// Get the digest.
+            ///
+            /// Note that the digest state can be continued to be used, to extend the
+            /// digest.
+            pub fn finish(&self, digest: &mut $result) {
+                self.state.finish(digest)
+            }
+        }
+
+        impl Default for $name {
+            fn default() -> Self {
+                Self::new()
+            }
+        }
+    };
+}
+
+impl_streaming_hacl_rs!(
+    Sha2_256,
+    crate::hacl_rs::hash_sha2::HaclRs_Sha2_Sha256,
+    Sha2_256Digest
+);
 // SHAKE messages from SHA 3
 
 #[cfg(simd256)]

src/hacl_rs/fstar.rs

@@ -0,0 +1,5 @@
+pub mod uint128;
+pub mod uint16;
+pub mod uint32;
+pub mod uint64;
+pub mod uint8;

src/hacl_rs/fstar/uint128.rs

@@ -0,0 +1,79 @@
+#![allow(non_camel_case_types)]
+
+pub type uint128 = u128;
+
+pub fn add(x: uint128, y: uint128) -> uint128 {
+    x.wrapping_add(y)
+}
+pub fn add_mod(x: uint128, y: uint128) -> uint128 {
+    x.wrapping_add(y)
+}
+pub fn sub(x: uint128, y: uint128) -> uint128 {
+    x.wrapping_sub(y)
+}
+pub fn sub_mod(x: uint128, y: uint128) -> uint128 {
+    x.wrapping_sub(y)
+}
+pub fn logand(x: uint128, y: uint128) -> uint128 {
+    x & y
+}
+pub fn logxor(x: uint128, y: uint128) -> uint128 {
+    x ^ y
+}
+pub fn logor(x: uint128, y: uint128) -> uint128 {
+    x | y
+}
+pub fn lognot(x: uint128) -> uint128 {
+    !x
+}
+pub fn shift_left(x: uint128, y: u32) -> uint128 {
+    x.wrapping_shl(y)
+}
+pub fn shift_right(x: uint128, y: u32) -> uint128 {
+    x.wrapping_shr(y)
+}
+pub fn eq(x: uint128, y: uint128) -> bool {
+    x == y
+}
+pub fn gt(x: uint128, y: uint128) -> bool {
+    x > y
+}
+pub fn lt(x: uint128, y: uint128) -> bool {
+    x < y
+}
+pub fn gte(x: uint128, y: uint128) -> bool {
+    x >= y
+}
+pub fn lte(x: uint128, y: uint128) -> bool {
+    x <= y
+}
+pub fn eq_mask(a: uint128, b: uint128) -> uint128 {
+    let x = a ^ b;
+    let minus_x = (!x).wrapping_add(1u128);
+    let x_or_minus_x = x | minus_x;
+    let xnx = x_or_minus_x.wrapping_shr(127);
+    xnx.wrapping_sub(1u128)
+}
+pub fn gte_mask(a: uint128, b: uint128) -> uint128 {
+    let x = a;
+    let y = b;
+    let x_xor_y = x ^ y;
+    let x_sub_y = x.wrapping_sub(y);
+    let x_sub_y_xor_y = x_sub_y ^ y;
+    let q = x_xor_y | x_sub_y_xor_y;
+    let x_xor_q = x ^ q;
+    let x_xor_q_ = x_xor_q.wrapping_shr(127);
+    x_xor_q_.wrapping_sub(1u128)
+}
+pub fn uint64_to_uint128(x: u64) -> uint128 {
+    x as u128
+}
+pub fn uint128_to_uint64(x: uint128) -> u64 {
+    x as u64
+}
+pub fn mul32(x: u64, y: u32) -> uint128 {
+    (x as u128) * (y as u128)
+}
+pub fn mul_wide(x: u64, y: u64) -> uint128 {
+    (x as u128) * (y as u128)
+}

src/hacl_rs/fstar/uint16.rs

@@ -0,0 +1,21 @@
+pub fn eq_mask(a: u16, b: u16) -> u16
+{
+  let x = a ^ b;
+  let minus_x = (!x).wrapping_add(1u16);
+  let x_or_minus_x = x | minus_x;
+  let xnx = x_or_minus_x.wrapping_shr(15);
+  xnx.wrapping_sub(1u16)
+}
+
+pub fn gte_mask(a: u16, b: u16) -> u16
+{
+  let x = a;
+  let y = b;
+  let x_xor_y = x ^ y;
+  let x_sub_y = x.wrapping_sub(y);
+  let x_sub_y_xor_y = x_sub_y ^ y;
+  let q = x_xor_y | x_sub_y_xor_y;
+  let x_xor_q = x ^ q;
+  let x_xor_q_ = x_xor_q.wrapping_shr(15);
+  x_xor_q_.wrapping_sub(1u16)
+}

src/hacl_rs/fstar/uint32.rs

@@ -0,0 +1,21 @@
+pub fn eq_mask(a: u32, b: u32) -> u32
+{
+  let x = a ^ b;
+  let minus_x = (!x).wrapping_add(1u32);
+  let x_or_minus_x = x | minus_x;
+  let xnx = x_or_minus_x.wrapping_shr(31);
+  xnx.wrapping_sub(1u32)
+}
+
+pub fn gte_mask(a: u32, b: u32) -> u32
+{
+  let x = a;
+  let y = b;
+  let x_xor_y = x ^ y;
+  let x_sub_y = x.wrapping_sub(y);
+  let x_sub_y_xor_y = x_sub_y ^ y;
+  let q = x_xor_y | x_sub_y_xor_y;
+  let x_xor_q = x ^ q;
+  let x_xor_q_ = x_xor_q.wrapping_shr(31);
+  x_xor_q_.wrapping_sub(1u32)
+}

src/hacl_rs/fstar/uint64.rs

@@ -0,0 +1,21 @@
+pub fn eq_mask(a: u64, b: u64) -> u64
+{
+  let x = a ^ b;
+  let minus_x = (!x).wrapping_add(1u64);
+  let x_or_minus_x = x | minus_x;
+  let xnx = x_or_minus_x.wrapping_shr(63);
+  xnx.wrapping_sub(1u64)
+}
+
+pub fn gte_mask(a: u64, b: u64) -> u64
+{
+  let x = a;
+  let y = b;
+  let x_xor_y = x ^ y;
+  let x_sub_y = x.wrapping_sub(y);
+  let x_sub_y_xor_y = x_sub_y ^ y;
+  let q = x_xor_y | x_sub_y_xor_y;
+  let x_xor_q = x ^ q;
+  let x_xor_q_ = x_xor_q.wrapping_shr(63);
+  x_xor_q_.wrapping_sub(1u64)
+}

src/hacl_rs/fstar/uint8.rs

@@ -0,0 +1,22 @@
+pub fn eq_mask(a: u8, b: u8) -> u8
+{
+  let x = a ^ b;
+  let minus_x = (!x).wrapping_add(1u8);
+  let x_or_minus_x = x | minus_x;
+  let xnx = x_or_minus_x.wrapping_shr(7);
+  xnx.wrapping_sub(1u8)
+}
+
+pub fn gte_mask(a: u8, b: u8) -> u8
+{
+  let x = a;
+  let y = b;
+  let x_xor_y = x ^ y;
+  let x_sub_y = x.wrapping_sub(y);
+  let x_sub_y_xor_y = x_sub_y ^ y;
+  let q = x_xor_y | x_sub_y_xor_y;
+  let x_xor_q = x ^ q;
+  let x_xor_q_ = x_xor_q.wrapping_shr(7);
+  x_xor_q_.wrapping_sub(1u8)
+}
+