From 72be892850134c996d53a2e478caaf790e9499fe Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 12:37:30 +0200
Subject: [PATCH 01/15] ci: cargo check workspace, public items are documented

---
 .github/workflows/workspace-checks.yml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.github/workflows/workspace-checks.yml b/.github/workflows/workspace-checks.yml
index 0a7a1b052..ae56ee347 100644
--- a/.github/workflows/workspace-checks.yml
+++ b/.github/workflows/workspace-checks.yml
@@ -26,6 +26,11 @@ jobs:
       - name: 🧹 Cargo fmt
         run: cargo fmt --all -- --check
 
+      - name: 🧐 Cargo check
+        env:
+          RUSTFLAGS: "-D missing_docs"
+        run: cargo check --workspace
+
   fmt-status:
     if: ${{ always() }}
     needs: [fmt]

From 4e83bd047cf1a5fd0b36ab393c60dfcda85f6627 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 16:34:35 +0200
Subject: [PATCH 02/15] document secrets crate

---
 secrets/src/int.rs                 | 11 +++++++++++
 secrets/src/int/public_integers.rs | 10 ++++++++++
 secrets/src/traits.rs              | 21 +++++++++++++++++++++
 3 files changed, 42 insertions(+)

diff --git a/secrets/src/int.rs b/secrets/src/int.rs
index 5da4a01c1..515665d2d 100644
--- a/secrets/src/int.rs
+++ b/secrets/src/int.rs
@@ -19,6 +19,7 @@ pub use public_integers::*;
 // A macro defining const constructors for secret/public integers
 macro_rules! impl_new {
     ($name:ident, $t:ty, $st:ty) => {
+        /// Creates a new secret/public integer from a primitive value
         #[allow(non_snake_case)]
         #[inline(always)]
         pub const fn $name(v: $t) -> $st {
@@ -44,18 +45,28 @@ impl_new!(I128, i128, I128);
 
 /// A trait defining cast operations for secret/public integers
 pub trait CastOps {
+    /// Cast to U8
     fn as_u8(self) -> U8;
+    /// Cast to I8
     fn as_i8(self) -> I8;
+    /// Cast to U16
     fn as_u16(self) -> U16;
+    /// Cast to I16
     fn as_i16(self) -> I16;
+    /// Cast to U32
     fn as_u32(self) -> U32;
+    /// Cast to I32
     fn as_i32(self) -> I32;
+    /// Cast to U64
     fn as_u64(self) -> U64;
+    /// Cast to I64
     fn as_i64(self) -> I64;
 
     #[cfg(not(eurydice))]
+    /// Cast to U128
     fn as_u128(self) -> U128;
     #[cfg(not(eurydice))]
+    /// Cast to I128
     fn as_i128(self) -> I128;
 }
 
diff --git a/secrets/src/int/public_integers.rs b/secrets/src/int/public_integers.rs
index 8a0a22bf0..663ad847f 100644
--- a/secrets/src/int/public_integers.rs
+++ b/secrets/src/int/public_integers.rs
@@ -1,17 +1,27 @@
 /// This crate defines classification and declassification over public integers
 /// All functions and types here are transparent (identities) and have no performance impact
 use crate::traits::*;
+/// Public 8-bit signed integer type
 pub type I8 = i8;
+/// Public 8-bit unsigned integer type
 pub type U8 = u8;
+/// Public 16-bit signed integer type
 pub type I16 = i16;
+/// Public 16-bit unsigned integer type
 pub type U16 = u16;
+/// Public 32-bit signed integer type
 pub type I32 = i32;
+/// Public 32-bit unsigned integer type
 pub type U32 = u32;
+/// Public 64-bit signed integer type
 pub type I64 = i64;
+/// Public 64-bit unsigned integer type
 pub type U64 = u64;
 #[cfg(not(eurydice))]
+/// Public 128-bit signed integer type
 pub type I128 = i128;
 #[cfg(not(eurydice))]
+/// Public 128-bit unsigned integer type
 pub type U128 = u128;
 
 /// Construct a public integer (identity)
diff --git a/secrets/src/traits.rs b/secrets/src/traits.rs
index b65b6a5fd..b322d3b6d 100644
--- a/secrets/src/traits.rs
+++ b/secrets/src/traits.rs
@@ -1,36 +1,48 @@
 /// A trait for public types that can be classified into secret types
 pub trait Classify {
+    /// The secret type that this public type can be classified into
     type Classified;
+    /// Convert this public value into a secret value
     fn classify(self) -> Self::Classified;
 }
 
 /// A trait for classifying immutable references to public types
 pub trait ClassifyRef {
+    /// The secret reference type that this public reference can be classified into
     type ClassifiedRef;
+    /// Convert this public reference into a secret reference
     fn classify_ref(self) -> Self::ClassifiedRef;
 }
 
 /// A trait for declassifying secret types into public types
 pub trait Declassify {
+    /// The public type that this secret type can be declassified into
     type Declassified;
+    /// Convert this secret value into a public value
     fn declassify(self) -> Self::Declassified;
 }
 
 /// A trait for declassifying references to secret types
 pub trait DeclassifyRef {
+    /// The public reference type that this secret reference can be declassified into
     type DeclassifiedRef;
+    /// Convert this secret reference into a public reference
     fn declassify_ref(self) -> Self::DeclassifiedRef;
 }
 
 /// A trait for classifying mutable references to public types
 pub trait ClassifyRefMut {
+    /// The secret mutable reference type that this public mutable reference can be classified into
     type ClassifiedRefMut;
+    /// Convert this public mutable reference into a secret mutable reference
     fn classify_ref_mut(self) -> Self::ClassifiedRefMut;
 }
 
 /// A trait for declassifying mutable references to secret types
 pub trait DeclassifyRefMut {
+    /// The public mutable reference type that this secret mutable reference can be declassified into
     type DeclassifiedRefMut;
+    /// Convert this secret mutable reference into a public mutable reference
     fn declassify_ref_mut(self) -> Self::DeclassifiedRefMut;
 }
 
@@ -56,19 +68,28 @@ pub trait IntOps
 where
     Self: Sized,
 {
+    /// Addition with wrapping overflow behavior
     fn wrapping_add<T: Into<Self>>(self, rhs: T) -> Self;
+    /// Subtraction with wrapping overflow behavior
     fn wrapping_sub<T: Into<Self>>(self, rhs: T) -> Self;
+    /// Multiplication with wrapping overflow behavior
     fn wrapping_mul<T: Into<Self>>(self, rhs: T) -> Self;
+    /// Rotate the bits of the integer to the left
     fn rotate_left(self, rhs: u32) -> Self;
+    /// Rotate the bits of the integer to the right
     fn rotate_right(self, rhs: u32) -> Self;
 }
 
 /// A trait for byte conversion operations provided by Rust for machine integers
 pub trait EncodeOps<T, const N: usize> {
+    /// Convert to little-endian byte array
     fn to_le_bytes(&self) -> [T; N];
+    /// Convert to big-endian byte array
     fn to_be_bytes(&self) -> [T; N];
 
+    /// Create from little-endian byte array
     fn from_le_bytes(x: [T; N]) -> Self;
+    /// Create from big-endian byte array
     fn from_be_bytes(x: [T; N]) -> Self;
 }
 

From a6f12fc4f3be59510b13f15d068dcedc276a2964 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 17:15:28 +0200
Subject: [PATCH 03/15] Add build script module docs

---
 benchmarks/build.rs         | 4 ++++
 libcrux-intrinsics/build.rs | 6 ++++++
 libcrux-ml-dsa/build.rs     | 6 ++++++
 libcrux-ml-kem/build.rs     | 6 ++++++
 libcrux-sha3/build.rs       | 6 ++++++
 sys/lib25519/build.rs       | 4 ++++
 sys/libjade/build.rs        | 6 ++++++
 7 files changed, 38 insertions(+)

diff --git a/benchmarks/build.rs b/benchmarks/build.rs
index 6468edce0..9d4a49a0d 100644
--- a/benchmarks/build.rs
+++ b/benchmarks/build.rs
@@ -1,3 +1,7 @@
+//! Build script for benchmarks crate.
+//!
+//! This script configures linking to lib25519 if available for benchmark comparisons.
+
 use std::{env, path::Path};
 
 fn main() {
diff --git a/libcrux-intrinsics/build.rs b/libcrux-intrinsics/build.rs
index 91a6fae70..3e04df931 100644
--- a/libcrux-intrinsics/build.rs
+++ b/libcrux-intrinsics/build.rs
@@ -1,3 +1,9 @@
+//! Build script for libcrux-intrinsics crate.
+//!
+//! This script configures SIMD features based on the target architecture and environment variables.
+//! It enables simd128 on aarch64 targets and simd256 on x86_64 targets, with override options
+//! available through environment variables.
+
 use std::env;
 
 fn main() {
diff --git a/libcrux-ml-dsa/build.rs b/libcrux-ml-dsa/build.rs
index dce0fe33d..a333ee8c6 100644
--- a/libcrux-ml-dsa/build.rs
+++ b/libcrux-ml-dsa/build.rs
@@ -1,3 +1,9 @@
+//! Build script for libcrux-ml-dsa crate.
+//!
+//! This script configures SIMD features based on the target architecture and environment variables.
+//! It enables simd128 on aarch64 targets and simd256 on x86_64 targets, with override options
+//! available through environment variables.
+
 use std::env;
 
 fn main() {
diff --git a/libcrux-ml-kem/build.rs b/libcrux-ml-kem/build.rs
index 91a6fae70..ce362ed83 100644
--- a/libcrux-ml-kem/build.rs
+++ b/libcrux-ml-kem/build.rs
@@ -1,3 +1,9 @@
+//! Build script for libcrux-ml-kem crate.
+//!
+//! This script configures SIMD features based on the target architecture and environment variables.
+//! It enables simd128 on aarch64 targets and simd256 on x86_64 targets, with override options
+//! available through environment variables.
+
 use std::env;
 
 fn main() {
diff --git a/libcrux-sha3/build.rs b/libcrux-sha3/build.rs
index 91a6fae70..4570f69d9 100644
--- a/libcrux-sha3/build.rs
+++ b/libcrux-sha3/build.rs
@@ -1,3 +1,9 @@
+//! Build script for libcrux-sha3 crate.
+//!
+//! This script configures SIMD features based on the target architecture and environment variables.
+//! It enables simd128 on aarch64 targets and simd256 on x86_64 targets, with override options
+//! available through environment variables.
+
 use std::env;
 
 fn main() {
diff --git a/sys/lib25519/build.rs b/sys/lib25519/build.rs
index c2245b2a8..376d6f9f8 100644
--- a/sys/lib25519/build.rs
+++ b/sys/lib25519/build.rs
@@ -1,3 +1,7 @@
+//! Build script for lib25519 FFI bindings.
+//!
+//! This script configures linking to the lib25519 C library and its dependencies.
+
 use std::env;
 
 fn main() {
diff --git a/sys/libjade/build.rs b/sys/libjade/build.rs
index d0d07cd27..07e045bfa 100644
--- a/sys/libjade/build.rs
+++ b/sys/libjade/build.rs
@@ -1,3 +1,8 @@
+//! Build script for libjade FFI bindings.
+//!
+//! This script configures compilation and binding generation for the libjade library,
+//! a collection of high-assurance cryptographic software components.
+
 use std::{env, path::Path};
 
 macro_rules! svec {
@@ -128,6 +133,7 @@ struct Platform {
     simd256: bool,
 }
 
+/// Main build script entry point
 pub fn main() {
     // Get ENV variables
     let home_dir = env::var("CARGO_MANIFEST_DIR").unwrap();

From a5433113104ab19dc3c102e9adacae7d93fd9609 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 17:16:49 +0200
Subject: [PATCH 04/15] ci: make workspace check separate job

---
 .github/workflows/workspace-checks.yml | 17 ++++++++++++-----
 1 file changed, 12 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/workspace-checks.yml b/.github/workflows/workspace-checks.yml
index ae56ee347..5dc12b145 100644
--- a/.github/workflows/workspace-checks.yml
+++ b/.github/workflows/workspace-checks.yml
@@ -16,24 +16,31 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  fmt:
+  check:
     if: ${{ github.event_name != 'merge_group' }}
     runs-on: ubuntu-latest
 
     steps:
       - uses: actions/checkout@v5
 
-      - name: 🧹 Cargo fmt
-        run: cargo fmt --all -- --check
-
       - name: 🧐 Cargo check
         env:
           RUSTFLAGS: "-D missing_docs"
         run: cargo check --workspace
 
+  fmt:
+    if: ${{ github.event_name != 'merge_group' }}
+    runs-on: ubuntu-latest
+
+    steps:
+      - uses: actions/checkout@v5
+
+      - name: 🧹 Cargo fmt
+        run: cargo fmt --all -- --check
+
   fmt-status:
     if: ${{ always() }}
-    needs: [fmt]
+    needs: [fmt, check]
     runs-on: ubuntu-latest
     steps:
       - name: Successful

From d7849f37d78cdaf2e095e99c5fc9eb464df6c0b7 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 17:38:13 +0200
Subject: [PATCH 05/15] Add libcrux-platforms doc comments

---
 sys/platform/src/lib.rs | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/sys/platform/src/lib.rs b/sys/platform/src/lib.rs
index f66b9479e..3b5cffa78 100644
--- a/sys/platform/src/lib.rs
+++ b/sys/platform/src/lib.rs
@@ -56,6 +56,7 @@ mod platform {
     use super::x86::{self as cpu_id, Feature};
 
     // TODO: Check for z14 or z15
+    /// Check whether 128-bit SIMD support is available
     pub fn simd128_support() -> bool {
         #[cfg(all(target_arch = "aarch64", target_os = "macos"))]
         {
@@ -87,6 +88,7 @@ mod platform {
         }
     }
 
+    /// Check whether 256-bit SIMD support is available
     pub fn simd256_support() -> bool {
         #[cfg(any(target_arch = "x86", target_arch = "x86_64"))]
         return cpu_id::supported(Feature::avx2);
@@ -95,6 +97,7 @@ mod platform {
         false
     }
 
+    /// Check whether CPU features required for X25519 are supported
     pub fn x25519_support() -> bool {
         #[cfg(any(target_arch = "x86", target_arch = "x86_64"))]
         return cpu_id::supported(Feature::bmi2) && cpu_id::supported(Feature::adx);
@@ -103,6 +106,7 @@ mod platform {
         false
     }
 
+    /// Check whether BMI2 and ADX CPU features are supported
     pub fn bmi2_adx_support() -> bool {
         #[cfg(any(target_arch = "x86", target_arch = "x86_64"))]
         return cpu_id::supported(Feature::bmi2) && cpu_id::supported(Feature::adx);

From db69422d24e5efeff7705517e0d325aa31cc1720 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 17:40:15 +0200
Subject: [PATCH 06/15] Add libcrux-macros doc comment

---
 macros/src/lib.rs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/macros/src/lib.rs b/macros/src/lib.rs
index 6c8eae249..b18a918d2 100644
--- a/macros/src/lib.rs
+++ b/macros/src/lib.rs
@@ -22,6 +22,7 @@ fn brace(ts: TokenStream) -> TokenTree {
     TokenTree::Group(proc_macro::Group::new(Delimiter::Brace, ts))
 }
 
+/// A procedural macro that unrolls a for loop at compile time.
 #[proc_macro]
 pub fn unroll_for(ts: TokenStream) -> TokenStream {
     let mut i = ts.into_iter();

From b772df3a35907415ec9e28b31ed5c0e916ef8318 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 17:41:03 +0200
Subject: [PATCH 07/15] Add libcrux-intrinsics doc comments

---
 libcrux-intrinsics/src/avx2.rs | 88 ++++++++++++++++++++++++++++++++++
 libcrux-intrinsics/src/lib.rs  |  6 +++
 2 files changed, 94 insertions(+)

diff --git a/libcrux-intrinsics/src/avx2.rs b/libcrux-intrinsics/src/avx2.rs
index 9acb73ddb..22190bf35 100644
--- a/libcrux-intrinsics/src/avx2.rs
+++ b/libcrux-intrinsics/src/avx2.rs
@@ -8,10 +8,14 @@ pub use core::arch::x86_64::*;
 #[cfg(hax)]
 pub use core_models::arch::x86::*;
 
+/// 256-bit SIMD vector of integers
 pub type Vec256 = __m256i;
+/// 128-bit SIMD vector of integers
 pub type Vec128 = __m128i;
+/// 256-bit SIMD vector of floats
 pub type Vec256Float = __m256;
 
+/// Store a 256-bit integer vector to an unaligned u8 array
 #[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_storeu_si256_u8(output: &mut [u8], vector: Vec256) {
@@ -27,6 +31,7 @@ pub fn mm256_storeu_si256_u8(output: &mut [u8], vector: Vec256) {
     }
 }
 
+/// Store a 256-bit integer vector to an unaligned i16 array
 #[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_storeu_si256_i16(output: &mut [i16], vector: Vec256) {
@@ -37,6 +42,7 @@ pub fn mm256_storeu_si256_i16(output: &mut [i16], vector: Vec256) {
     }
 }
 
+/// Store a 256-bit integer vector to an unaligned i32 array
 #[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_storeu_si256_i32(output: &mut [i32], vector: Vec256) {
@@ -47,6 +53,7 @@ pub fn mm256_storeu_si256_i32(output: &mut [i32], vector: Vec256) {
     }
 }
 
+/// Store a 128-bit integer vector to an unaligned i16 array
 #[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_storeu_si128(output: &mut [i16], vector: Vec128) {
@@ -57,6 +64,7 @@ pub fn mm_storeu_si128(output: &mut [i16], vector: Vec128) {
     }
 }
 
+/// Store a 128-bit integer vector to an unaligned i32 array
 #[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_storeu_si128_i32(output: &mut [i32], vector: Vec128) {
@@ -67,6 +75,7 @@ pub fn mm_storeu_si128_i32(output: &mut [i32], vector: Vec128) {
     }
 }
 
+/// Store a 128-bit integer vector to an unaligned u8 array
 #[hax_lib::opaque]
 #[hax_lib::ensures(|_r| future(output).len() == output.len())]
 #[inline(always)]
@@ -78,6 +87,7 @@ pub fn mm_storeu_bytes_si128(output: &mut [u8], vector: Vec128) {
     }
 }
 
+/// Load a 128-bit integer vector from an unaligned u8 array
 #[hax_lib::opaque]
 #[inline(always)]
 pub fn mm_loadu_si128(input: &[u8]) -> Vec128 {
@@ -86,6 +96,7 @@ pub fn mm_loadu_si128(input: &[u8]) -> Vec128 {
     unsafe { _mm_loadu_si128(input.as_ptr() as *const Vec128) }
 }
 
+/// Load a 256-bit integer vector from an unaligned u8 array
 #[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_loadu_si256_u8(input: &[u8]) -> Vec256 {
@@ -94,6 +105,7 @@ pub fn mm256_loadu_si256_u8(input: &[u8]) -> Vec256 {
     unsafe { _mm256_loadu_si256(input.as_ptr() as *const Vec256) }
 }
 
+/// Load a 256-bit integer vector from an unaligned i16 array
 #[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_loadu_si256_i16(input: &[i16]) -> Vec256 {
@@ -102,6 +114,7 @@ pub fn mm256_loadu_si256_i16(input: &[i16]) -> Vec256 {
     unsafe { _mm256_loadu_si256(input.as_ptr() as *const Vec256) }
 }
 
+/// Load a 256-bit integer vector from an unaligned i32 array
 #[hax_lib::opaque]
 #[inline(always)]
 pub fn mm256_loadu_si256_i32(input: &[i32]) -> Vec256 {
@@ -110,16 +123,19 @@ pub fn mm256_loadu_si256_i32(input: &[i32]) -> Vec256 {
     unsafe { _mm256_loadu_si256(input.as_ptr() as *const Vec256) }
 }
 
+/// Create a 256-bit vector with all elements set to zero
 #[inline(always)]
 pub fn mm256_setzero_si256() -> Vec256 {
     unsafe { _mm256_setzero_si256() }
 }
 
+/// Create a 256-bit vector by combining two 128-bit vectors (high and low)
 #[inline(always)]
 pub fn mm256_set_m128i(hi: Vec128, lo: Vec128) -> Vec256 {
     unsafe { _mm256_set_m128i(hi, lo) }
 }
 
+/// Create a 128-bit vector from 16 individual i8 values
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_set_epi8(
@@ -148,6 +164,7 @@ pub fn mm_set_epi8(
     }
 }
 
+/// Create a 256-bit vector from 32 individual i8 values
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_set_epi8(
@@ -193,12 +210,14 @@ pub fn mm256_set_epi8(
     }
 }
 
+/// Create a 256-bit vector with all i16 elements set to the same value
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_set1_epi16(constant: i16) -> Vec256 {
     unsafe { _mm256_set1_epi16(constant) }
 }
 
+/// Create a 256-bit vector from 16 individual i16 values
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_set_epi16(
@@ -227,24 +246,28 @@ pub fn mm256_set_epi16(
     }
 }
 
+/// Create a 128-bit vector with all i16 elements set to the same value
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_set1_epi16(constant: i16) -> Vec128 {
     unsafe { _mm_set1_epi16(constant) }
 }
 
+/// Create a 256-bit vector with all i32 elements set to the same value
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_set1_epi32(constant: i32) -> Vec256 {
     unsafe { _mm256_set1_epi32(constant) }
 }
 
+/// Create a 128-bit vector from 4 individual i32 values
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_set_epi32(input3: i32, input2: i32, input1: i32, input0: i32) -> Vec128 {
     unsafe { _mm_set_epi32(input3, input2, input1, input0) }
 }
 
+/// Create a 256-bit vector from 8 individual i32 values
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_set_epi32(
@@ -264,162 +287,189 @@ pub fn mm256_set_epi32(
     }
 }
 
+/// Add packed 16-bit integers in two 128-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_add_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 {
     unsafe { _mm_add_epi16(lhs, rhs) }
 }
 
+/// Add packed 16-bit integers in two 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_add_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_add_epi16(lhs, rhs) }
 }
 
+/// Multiply packed 16-bit integers, add adjacent pairs and store as 32-bit integers
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_madd_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_madd_epi16(lhs, rhs) }
 }
 
+/// Add packed 32-bit integers in two 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_add_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_add_epi32(lhs, rhs) }
 }
 
+/// Add packed 64-bit integers in two 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_add_epi64(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_add_epi64(lhs, rhs) }
 }
 
+/// Compute absolute value of packed 32-bit integers
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_abs_epi32(a: Vec256) -> Vec256 {
     unsafe { _mm256_abs_epi32(a) }
 }
 
+/// Subtract packed 16-bit integers in two 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_sub_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_sub_epi16(lhs, rhs) }
 }
 
+/// Subtract packed 32-bit integers in two 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_sub_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_sub_epi32(lhs, rhs) }
 }
 
+/// Subtract packed 16-bit integers in two 128-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_sub_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 {
     unsafe { _mm_sub_epi16(lhs, rhs) }
 }
 
+/// Multiply packed 16-bit integers and store low 16 bits of results
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_mullo_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_mullo_epi16(lhs, rhs) }
 }
 
+/// Multiply packed 16-bit integers and store low 16 bits of results
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_mullo_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 {
     unsafe { _mm_mullo_epi16(lhs, rhs) }
 }
 
+/// Compare packed 16-bit integers for greater than
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_cmpgt_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_cmpgt_epi16(lhs, rhs) }
 }
 
+/// Compare packed 32-bit integers for greater than
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_cmpgt_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_cmpgt_epi32(lhs, rhs) }
 }
 
+/// Compare packed 32-bit integers for equality
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_cmpeq_epi32(a: Vec256, b: Vec256) -> Vec256 {
     unsafe { _mm256_cmpeq_epi32(a, b) }
 }
 
+/// Apply sign of packed 32-bit integers in b to packed 32-bit integers in a
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_sign_epi32(a: Vec256, b: Vec256) -> Vec256 {
     unsafe { _mm256_sign_epi32(a, b) }
 }
 
+/// Cast 256-bit integer vector to 256-bit float vector
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_castsi256_ps(a: Vec256) -> Vec256Float {
     unsafe { _mm256_castsi256_ps(a) }
 }
 
+/// Cast 256-bit float vector to 256-bit integer vector
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_castps_si256(a: Vec256Float) -> Vec256 {
     unsafe { _mm256_castps_si256(a) }
 }
 
+/// Extract sign bits from packed single-precision floating-point elements
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_movemask_ps(a: Vec256Float) -> i32 {
     unsafe { _mm256_movemask_ps(a) }
 }
 
+/// Multiply packed 16-bit integers and store high 16 bits of results
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_mulhi_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 {
     unsafe { _mm_mulhi_epi16(lhs, rhs) }
 }
 
+/// Multiply packed 32-bit integers and store low 32 bits of results
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_mullo_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_mullo_epi32(lhs, rhs) }
 }
 
+/// Multiply packed 16-bit integers and store high 16 bits of results
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_mulhi_epi16(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_mulhi_epi16(lhs, rhs) }
 }
 
+/// Multiply packed unsigned 32-bit integers and store low 64 bits of results
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_mul_epu32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_mul_epu32(lhs, rhs) }
 }
 
+/// Multiply packed signed 32-bit integers and store low 64 bits of results
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_mul_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_mul_epi32(lhs, rhs) }
 }
 
+/// Perform bitwise AND on 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_and_si256(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_and_si256(lhs, rhs) }
 }
 
+/// Perform bitwise OR on 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_or_si256(a: Vec256, b: Vec256) -> Vec256 {
     unsafe { _mm256_or_si256(a, b) }
 }
 
+/// Test if AND of two 256-bit vectors is zero
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_testz_si256(lhs: Vec256, rhs: Vec256) -> i32 {
     unsafe { _mm256_testz_si256(lhs, rhs) }
 }
 
+/// Perform bitwise XOR on 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_xor_si256(lhs: Vec256, rhs: Vec256) -> Vec256 {
@@ -439,6 +489,7 @@ pub fn mm256_xor_si256(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_xor_si256(lhs, rhs) }
 }
 
+/// Shift packed 16-bit integers right by constant count with sign extension
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_srai_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
@@ -447,6 +498,7 @@ pub fn mm256_srai_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_srai_epi16::<SHIFT_BY>(vector) }
 }
 
+/// Shift packed 32-bit integers right by constant count with sign extension
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_srai_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
@@ -455,6 +507,7 @@ pub fn mm256_srai_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_srai_epi32::<SHIFT_BY>(vector) }
 }
 
+/// Shift packed 16-bit integers right by constant count with zero extension
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_srli_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
@@ -463,6 +516,7 @@ pub fn mm256_srli_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_srli_epi16::<SHIFT_BY>(vector) }
 }
 
+/// Shift packed 32-bit integers right by constant count with zero extension
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_srli_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
@@ -471,6 +525,7 @@ pub fn mm256_srli_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_srli_epi32::<SHIFT_BY>(vector) }
 }
 
+/// Shift packed 64-bit integers right by constant count with zero extension
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_srli_epi64<const SHIFT_BY: i32>(vector: Vec128) -> Vec128 {
@@ -479,6 +534,7 @@ pub fn mm_srli_epi64<const SHIFT_BY: i32>(vector: Vec128) -> Vec128 {
     unsafe { _mm_srli_epi64::<SHIFT_BY>(vector) }
 }
 
+/// Shift packed 64-bit integers right by constant count with zero extension
 #[inline(always)]
 #[hax_lib::requires(SHIFT_BY > 0 && SHIFT_BY < 64)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
@@ -488,6 +544,7 @@ pub fn mm256_srli_epi64<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_srli_epi64::<SHIFT_BY>(vector) }
 }
 
+/// Shift packed 16-bit integers left by constant count
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_slli_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
@@ -496,6 +553,7 @@ pub fn mm256_slli_epi16<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_slli_epi16::<SHIFT_BY>(vector) }
 }
 
+/// Shift packed 32-bit integers left by constant count
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_slli_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
@@ -504,18 +562,21 @@ pub fn mm256_slli_epi32<const SHIFT_BY: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_slli_epi32::<SHIFT_BY>(vector) }
 }
 
+/// Shuffle bytes in 128-bit vector according to control mask
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_shuffle_epi8(vector: Vec128, control: Vec128) -> Vec128 {
     unsafe { _mm_shuffle_epi8(vector, control) }
 }
 
+/// Shuffle bytes in 256-bit vector according to control mask
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_shuffle_epi8(vector: Vec256, control: Vec256) -> Vec256 {
     unsafe { _mm256_shuffle_epi8(vector, control) }
 }
 
+/// Shuffle 32-bit integers in 256-bit vector using constant control
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_shuffle_epi32<const CONTROL: i32>(vector: Vec256) -> Vec256 {
@@ -524,6 +585,7 @@ pub fn mm256_shuffle_epi32<const CONTROL: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_shuffle_epi32::<CONTROL>(vector) }
 }
 
+/// Permute 64-bit integers in 256-bit vector using constant control
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_permute4x64_epi64<const CONTROL: i32>(vector: Vec256) -> Vec256 {
@@ -532,54 +594,63 @@ pub fn mm256_permute4x64_epi64<const CONTROL: i32>(vector: Vec256) -> Vec256 {
     unsafe { _mm256_permute4x64_epi64::<CONTROL>(vector) }
 }
 
+/// Unpack and interleave high 64-bit integers from two 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_unpackhi_epi64(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_unpackhi_epi64(lhs, rhs) }
 }
 
+/// Unpack and interleave low 32-bit integers from two 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_unpacklo_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_unpacklo_epi32(lhs, rhs) }
 }
 
+/// Unpack and interleave high 32-bit integers from two 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_unpackhi_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_unpackhi_epi32(lhs, rhs) }
 }
 
+/// Cast 256-bit integer vector to 128-bit integer vector (extract low 128 bits)
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_castsi256_si128(vector: Vec256) -> Vec128 {
     unsafe { _mm256_castsi256_si128(vector) }
 }
 
+/// Cast 128-bit integer vector to 256-bit integer vector (zero-extend high 128 bits)
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_castsi128_si256(vector: Vec128) -> Vec256 {
     unsafe { _mm256_castsi128_si256(vector) }
 }
 
+/// Convert packed 16-bit integers to 32-bit integers with sign extension
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_cvtepi16_epi32(vector: Vec128) -> Vec256 {
     unsafe { _mm256_cvtepi16_epi32(vector) }
 }
 
+/// Pack signed 16-bit integers to signed 8-bit integers with saturation
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_packs_epi16(lhs: Vec128, rhs: Vec128) -> Vec128 {
     unsafe { _mm_packs_epi16(lhs, rhs) }
 }
 
+/// Pack signed 32-bit integers to signed 16-bit integers with saturation
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_packs_epi32(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_packs_epi32(lhs, rhs) }
 }
 
+/// Extract 128-bit lane from 256-bit vector
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_extracti128_si256<const CONTROL: i32>(vector: Vec256) -> Vec128 {
@@ -588,6 +659,7 @@ pub fn mm256_extracti128_si256<const CONTROL: i32>(vector: Vec256) -> Vec128 {
     unsafe { _mm256_extracti128_si256::<CONTROL>(vector) }
 }
 
+/// Insert 128-bit value into 256-bit vector at specified lane
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_inserti128_si256<const CONTROL: i32>(vector: Vec256, vector_i128: Vec128) -> Vec256 {
@@ -596,6 +668,7 @@ pub fn mm256_inserti128_si256<const CONTROL: i32>(vector: Vec256, vector_i128: V
     unsafe { _mm256_inserti128_si256::<CONTROL>(vector, vector_i128) }
 }
 
+/// Blend 16-bit integers from two vectors using constant control mask
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_blend_epi16<const CONTROL: i32>(lhs: Vec256, rhs: Vec256) -> Vec256 {
@@ -604,6 +677,7 @@ pub fn mm256_blend_epi16<const CONTROL: i32>(lhs: Vec256, rhs: Vec256) -> Vec256
     unsafe { _mm256_blend_epi16::<CONTROL>(lhs, rhs) }
 }
 
+/// Blend 32-bit integers from two vectors using constant control mask
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_blend_epi32<const CONTROL: i32>(lhs: Vec256, rhs: Vec256) -> Vec256 {
@@ -615,6 +689,7 @@ pub fn mm256_blend_epi32<const CONTROL: i32>(lhs: Vec256, rhs: Vec256) -> Vec256
 // This is essentially _mm256_blendv_ps adapted for use with the Vec256 type.
 // It is not offered by the AVX2 instruction set.
 
+/// Blend 32-bit integers from two vectors using variable mask
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn vec256_blendv_epi32(a: Vec256, b: Vec256, mask: Vec256) -> Vec256 {
@@ -627,48 +702,56 @@ pub fn vec256_blendv_epi32(a: Vec256, b: Vec256, mask: Vec256) -> Vec256 {
     }
 }
 
+/// Extract most significant bit from each 8-bit integer and create mask
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_movemask_epi8(vector: Vec128) -> i32 {
     unsafe { _mm_movemask_epi8(vector) }
 }
 
+/// Permute 32-bit integers in 256-bit vector using variable control
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_permutevar8x32_epi32(vector: Vec256, control: Vec256) -> Vec256 {
     unsafe { _mm256_permutevar8x32_epi32(vector, control) }
 }
 
+/// Shift packed 32-bit integers right by variable counts with zero extension
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_srlv_epi32(vector: Vec256, counts: Vec256) -> Vec256 {
     unsafe { _mm256_srlv_epi32(vector, counts) }
 }
 
+/// Shift packed 64-bit integers right by variable counts with zero extension
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_srlv_epi64(vector: Vec256, counts: Vec256) -> Vec256 {
     unsafe { _mm256_srlv_epi64(vector, counts) }
 }
 
+/// Shift packed 32-bit integers left by variable counts
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm_sllv_epi32(vector: Vec128, counts: Vec128) -> Vec128 {
     unsafe { _mm_sllv_epi32(vector, counts) }
 }
 
+/// Shift packed 32-bit integers left by variable counts
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_sllv_epi32(vector: Vec256, counts: Vec256) -> Vec256 {
     unsafe { _mm256_sllv_epi32(vector, counts) }
 }
 
+/// Shift packed 64-bit integers left by constant count
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_slli_epi64<const LEFT: i32>(x: Vec256) -> Vec256 {
     unsafe { _mm256_slli_epi64::<LEFT>(x) }
 }
 
+/// Shift 128-bit lanes right by constant byte count
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_bsrli_epi128<const SHIFT_BY: i32>(x: Vec256) -> Vec256 {
@@ -677,30 +760,35 @@ pub fn mm256_bsrli_epi128<const SHIFT_BY: i32>(x: Vec256) -> Vec256 {
     unsafe { _mm256_bsrli_epi128::<SHIFT_BY>(x) }
 }
 
+/// Perform bitwise AND NOT operation on 256-bit vectors (NOT a AND b)
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_andnot_si256(a: Vec256, b: Vec256) -> Vec256 {
     unsafe { _mm256_andnot_si256(a, b) }
 }
 
+/// Create a 256-bit vector with all i64 elements set to the same value
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_set1_epi64x(a: i64) -> Vec256 {
     unsafe { _mm256_set1_epi64x(a) }
 }
 
+/// Create a 256-bit vector from 4 individual i64 values
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_set_epi64x(input3: i64, input2: i64, input1: i64, input0: i64) -> Vec256 {
     unsafe { _mm256_set_epi64x(input3, input2, input1, input0) }
 }
 
+/// Unpack and interleave low 64-bit integers from two 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_unpacklo_epi64(lhs: Vec256, rhs: Vec256) -> Vec256 {
     unsafe { _mm256_unpacklo_epi64(lhs, rhs) }
 }
 
+/// Permute 128-bit lanes within and between two 256-bit vectors
 #[inline(always)]
 #[hax_lib::fstar::before(r#"[@@ "opaque_to_smt"]"#)]
 pub fn mm256_permute2x128_si256<const IMM8: i32>(a: Vec256, b: Vec256) -> Vec256 {
diff --git a/libcrux-intrinsics/src/lib.rs b/libcrux-intrinsics/src/lib.rs
index 7c2646ad4..89c980cce 100644
--- a/libcrux-intrinsics/src/lib.rs
+++ b/libcrux-intrinsics/src/lib.rs
@@ -1,7 +1,13 @@
+//! Platform-specific SIMD intrinsics for libcrux.
+//!
+//! This crate provides SIMD intrinsics for ARM64 (128-bit) and x86_64 (256-bit) architectures.
+//! It includes both real implementations for actual hardware and dummy implementations for extraction.
+
 #![no_std]
 #[cfg(all(feature = "simd128", not(hax)))]
 pub mod arm64;
 #[cfg(all(feature = "simd256", not(hax)))]
+/// AVX2 intrinsics for x86_64 256-bit SIMD operations
 pub mod avx2;
 
 // When extracting F* we only want dummy files here.

From 7778ce7305a3feef890c6e717cf749c119b78245 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 17:43:11 +0200
Subject: [PATCH 08/15] Add benchmarks doc comments

---
 benchmarks/src/lib.rs | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/benchmarks/src/lib.rs b/benchmarks/src/lib.rs
index 61c0a28c1..4724c0b99 100644
--- a/benchmarks/src/lib.rs
+++ b/benchmarks/src/lib.rs
@@ -1,4 +1,10 @@
+//! Benchmark utilities for libcrux performance testing.
+//!
+//! This crate provides utility functions for benchmarking cryptographic operations.
+
+/// Utility functions for benchmarking
 pub mod util {
+    /// Generate random bytes for testing
     pub fn randombytes(n: usize) -> Vec<u8> {
         use rand::rngs::OsRng;
         use rand::TryRngCore;
@@ -8,12 +14,14 @@ pub mod util {
         bytes
     }
 
+    /// Format byte count with appropriate units (KB, MB, GB)
     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])
     }
 
+    /// Convert hex string to byte vector
     pub fn hex_str_to_bytes(val: &str) -> Vec<u8> {
         let b: Result<Vec<u8>, std::num::ParseIntError> = (0..val.len())
             .step_by(2)
@@ -22,6 +30,7 @@ pub mod util {
         b.expect("Error parsing hex string")
     }
 
+    /// Convert hex string to fixed-size array
     pub fn hex_str_to_array<A>(val: &str) -> A
     where
         A: Default + AsMut<[u8]>,

From e6055337edc48536555ac02376e4b94793d9db25 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 18:07:53 +0200
Subject: [PATCH 09/15] Add lib25519 doc comments (and exception for generated
 bindings)

---
 sys/lib25519/src/lib.rs | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/sys/lib25519/src/lib.rs b/sys/lib25519/src/lib.rs
index 05d92f297..e7c2c26c0 100644
--- a/sys/lib25519/src/lib.rs
+++ b/sys/lib25519/src/lib.rs
@@ -1,5 +1,11 @@
+//! FFI bindings to lib25519 cryptographic library.
+//!
+//! This crate provides Rust bindings to the lib25519 library, which implements
+//! Curve25519 elliptic curve cryptography operations.
+
 #![allow(non_upper_case_globals)]
 #![allow(non_camel_case_types)]
 #![allow(non_snake_case)]
+#![allow(missing_docs)]
 
 include!("./bindings.rs");

From 698343407d520e3314ec11fa921ed724d9ce2d30 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 18:08:13 +0200
Subject: [PATCH 10/15] Add core-models doc comments

---
 .../core-models/src/abstractions/bit.rs       |  6 ++
 .../core-models/src/abstractions/bitvec.rs    | 10 +++
 .../core-models/src/abstractions/funarr.rs    |  4 +
 .../core-models/src/abstractions/mod.rs       |  1 +
 .../core-models/src/core_arch/x86.rs          | 22 +++++
 .../src/core_arch/x86/interpretations.rs      | 88 +++++++++++++++++++
 fstar-helpers/core-models/src/lib.rs          |  2 +
 7 files changed, 133 insertions(+)

diff --git a/fstar-helpers/core-models/src/abstractions/bit.rs b/fstar-helpers/core-models/src/abstractions/bit.rs
index 46f874be9..15a9d6473 100644
--- a/fstar-helpers/core-models/src/abstractions/bit.rs
+++ b/fstar-helpers/core-models/src/abstractions/bit.rs
@@ -34,7 +34,9 @@
 /// Represent a bit: `0` or `1`.
 #[derive(Copy, Clone, Eq, PartialEq, Debug)]
 pub enum Bit {
+    /// Represents the bit value `0`.
     Zero,
+    /// Represents the bit value `1`.
     One,
 }
 
@@ -111,6 +113,10 @@ impl Bit {
         }
     }
 
+    /// Extracts the `nth` bit from the given integer `x`.
+    ///
+    /// This function treats the integer as a two's complement representation
+    /// and returns the bit at position `nth` (0-indexed from the least significant bit).
     pub fn of_int<T: Into<i128> + MachineInteger>(x: T, nth: u32) -> Bit {
         let x: i128 = x.into();
         if x >= 0 {
diff --git a/fstar-helpers/core-models/src/abstractions/bitvec.rs b/fstar-helpers/core-models/src/abstractions/bitvec.rs
index 3a7da22cf..726071d0b 100644
--- a/fstar-helpers/core-models/src/abstractions/bitvec.rs
+++ b/fstar-helpers/core-models/src/abstractions/bitvec.rs
@@ -102,6 +102,10 @@ const _: () = ();
 macro_rules! impl_pointwise {
     ($n:literal, $($i:literal)*) => {
         impl BitVec<$n> {
+            /// Creates a pointwise copy of the bit vector elements.
+            ///
+            /// This method reconstructs the bit vector by applying an identity function
+            /// to each bit, effectively creating a new bit vector with the same values.
             pub fn pointwise(self) -> Self {
                 Self::from_fn(|i| match i {
                     $($i => self[$i],)*
@@ -241,6 +245,10 @@ pub fn bitvec_postprocess_norm() {}
 
 #[hax_lib::attributes]
 impl<const N: u64> BitVec<N> {
+    /// Performs chunked shift operations on the bit vector.
+    ///
+    /// Divides the bit vector into chunks of size `CHUNK` and applies shift operations
+    /// specified in the `shl` array to each chunk.
     #[hax_lib::requires(CHUNK > 0 && CHUNK.to_int() * SHIFTS.to_int() == N.to_int())]
     pub fn chunked_shift<const CHUNK: u64, const SHIFTS: u64>(
         self,
@@ -355,6 +363,7 @@ pub mod int_vec_interp {
 		     u32x4 [u32; 4], u64x2 [u64; 2], u16x8 [u16; 8]);
 
     impl i64x4 {
+        /// Converts an `i64x4` into an `i32x8` by splitting each 64-bit integer into two 32-bit integers.
         pub fn into_i32x8(self) -> i32x8 {
             i32x8::from_fn(|i| {
                 let value = *self.get(i / 2);
@@ -364,6 +373,7 @@ pub mod int_vec_interp {
     }
 
     impl i32x8 {
+        /// Converts an `i32x8` into an `i64x4` by combining pairs of 32-bit integers into 64-bit integers.
         pub fn into_i64x4(self) -> i64x4 {
             i64x4::from_fn(|i| {
                 let low = *self.get(2 * i) as u32 as u64;
diff --git a/fstar-helpers/core-models/src/abstractions/funarr.rs b/fstar-helpers/core-models/src/abstractions/funarr.rs
index 71e3c9736..25f853059 100644
--- a/fstar-helpers/core-models/src/abstractions/funarr.rs
+++ b/fstar-helpers/core-models/src/abstractions/funarr.rs
@@ -87,6 +87,10 @@ impl<const N: u64, T> FunArray<N, T> {
 macro_rules! impl_pointwise {
     ($n:literal, $($i:literal)*) => {
         impl<T: Copy> FunArray<$n, T> {
+            /// Creates a pointwise copy of the array elements.
+            ///
+            /// This method reconstructs the array by applying an identity function
+            /// to each element, effectively creating a new array with the same values.
             pub fn pointwise(self) -> Self {
                 Self::from_fn(|i| match i {
                     $($i => self[$i],)*
diff --git a/fstar-helpers/core-models/src/abstractions/mod.rs b/fstar-helpers/core-models/src/abstractions/mod.rs
index c67a17bba..f6e435055 100644
--- a/fstar-helpers/core-models/src/abstractions/mod.rs
+++ b/fstar-helpers/core-models/src/abstractions/mod.rs
@@ -22,4 +22,5 @@
 
 pub mod bit;
 pub mod bitvec;
+/// Functional array abstraction with fixed-size arrays and F* integration.
 pub mod funarr;
diff --git a/fstar-helpers/core-models/src/core_arch/x86.rs b/fstar-helpers/core-models/src/core_arch/x86.rs
index aa4740856..8bb7e43e5 100644
--- a/fstar-helpers/core-models/src/core_arch/x86.rs
+++ b/fstar-helpers/core-models/src/core_arch/x86.rs
@@ -76,6 +76,7 @@
 //!
 #![allow(clippy::too_many_arguments)]
 
+/// Interpretations and additional models for x86 SIMD operations.
 pub mod interpretations;
 use crate::abstractions::{bit::*, bitvec::*, funarr::*};
 
@@ -171,8 +172,10 @@ pub type __m128i = BitVec<128>;
 pub type __m256 = __m256i;
 
 pub use ssse3::*;
+/// SSSE3 (Supplemental Streaming SIMD Extensions 3) instruction models.
 pub mod ssse3 {
     use super::*;
+    /// Shuffle bytes in a 128-bit vector according to control bytes in indexes.
     #[hax_lib::opaque]
     pub fn _mm_shuffle_epi8(vector: __m128i, indexes: __m128i) -> __m128i {
         let indexes = indexes.to_vec().try_into().unwrap();
@@ -180,6 +183,7 @@ pub mod ssse3 {
     }
 }
 pub use sse2::*;
+/// SSE2 (Streaming SIMD Extensions 2) instruction models.
 pub mod sse2 {
     /// This intrinsics is not extracted via hax currently since it cannot hanlde raw pointers.
     /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm_loadu_si128&ig_expand=4106)
@@ -195,6 +199,7 @@ pub mod sse2 {
     }
 
     use super::*;
+    /// Set packed 8-bit integers in a 128-bit vector with the supplied values.
     #[hax_lib::opaque]
     pub fn _mm_set_epi8(
         _e15: i8,
@@ -263,6 +268,7 @@ pub mod sse2 {
 }
 
 pub use avx::*;
+/// AVX (Advanced Vector Extensions) instruction models.
 pub mod avx {
     /// This intrinsics is not extracted via hax currently since it cannot hanlde raw pointers.
     /// [Intel Documentation](https://www.intel.com/content/www/us/en/docs/intrinsics-guide/index.html#text=_mm256_storeu_si256)
@@ -332,6 +338,7 @@ pub mod avx {
     }
 
     pub use super::*;
+    /// Cast a 256-bit integer vector to a 128-bit integer vector, extracting the lower 128 bits.
     pub fn _mm256_castsi256_si128(vector: __m256i) -> __m128i {
         BitVec::from_fn(|i| vector[i])
     }
@@ -429,6 +436,7 @@ pub mod avx {
     }
 }
 pub use avx2::*;
+/// AVX2 (Advanced Vector Extensions 2) instruction models.
 pub mod avx2 {
     use super::*;
 
@@ -925,9 +933,11 @@ let ${_rw_mm256_mullo_epi16_shifts} = e___e_rw_mm256_mullo_epi16_shifts'
     }
 };
 
+/// Extra helper functions for SIMD operations not directly corresponding to intrinsics.
 pub mod extra {
     use super::*;
 
+    /// Variable left shift packed 32-bit integers in a 256-bit vector using counts from an array.
     pub fn mm256_sllv_epi32_u32_array(
         vector: BitVec<256>,
         counts: FunArray<8, u32>,
@@ -935,6 +945,7 @@ pub mod extra {
         vector.chunked_shift::<32, 8>(FunArray::from_fn(|i| counts[i] as i128))
     }
 
+    /// Variable left shift packed 32-bit integers in a 256-bit vector using individual shift counts.
     pub fn mm256_sllv_epi32_u32(
         vector: BitVec<256>,
         b7: u32,
@@ -962,6 +973,7 @@ pub mod extra {
         )
     }
 
+    /// Variable right shift packed 32-bit integers in a 256-bit vector using counts from an array.
     pub fn mm256_srlv_epi32_u32_array(
         vector: BitVec<256>,
         counts: FunArray<8, u32>,
@@ -969,6 +981,7 @@ pub mod extra {
         vector.chunked_shift::<32, 8>(FunArray::from_fn(|i| -(counts[i] as i128)))
     }
 
+    /// Variable right shift packed 32-bit integers in a 256-bit vector using individual shift counts.
     pub fn mm256_srlv_epi32_u32(
         vector: BitVec<256>,
         b7: u32,
@@ -996,6 +1009,7 @@ pub mod extra {
         )
     }
 
+    /// Permute packed 32-bit integers in a 256-bit vector using indices from an array.
     pub fn mm256_permutevar8x32_epi32_u32_array(
         a: BitVec<256>,
         b: FunArray<8, u32>,
@@ -1007,6 +1021,7 @@ pub mod extra {
         })
     }
 
+    /// Permute packed 32-bit integers in a 256-bit vector using individual indices.
     pub fn mm256_permutevar8x32_epi32_u32(
         vector: BitVec<256>,
         b7: u32,
@@ -1034,6 +1049,7 @@ pub mod extra {
         )
     }
 
+    /// Shuffle bytes in a 128-bit vector using indices from an array.
     pub fn mm_shuffle_epi8_u8_array(vector: BitVec<128>, indexes: FunArray<16, u8>) -> BitVec<128> {
         BitVec::from_fn(|i| {
             let nth = i / 8;
@@ -1047,6 +1063,7 @@ pub mod extra {
         })
     }
 
+    /// Shuffle bytes in a 128-bit vector using individual byte indices.
     pub fn mm_shuffle_epi8_u8(
         vector: BitVec<128>,
         b15: u8,
@@ -1088,6 +1105,7 @@ pub mod extra {
         mm_shuffle_epi8_u8_array(vector, indexes)
     }
 
+    /// Shuffle bytes in a 256-bit vector using indices from an array.
     pub fn mm256_shuffle_epi8_i8_array(
         vector: BitVec<256>,
         indexes: FunArray<32, i8>,
@@ -1104,6 +1122,7 @@ pub mod extra {
         })
     }
 
+    /// Shuffle bytes in a 256-bit vector using individual byte indices.
     pub fn mm256_shuffle_epi8_i8(
         vector: BitVec<256>,
         byte31: i8,
@@ -1177,6 +1196,7 @@ pub mod extra {
         mm256_shuffle_epi8_i8_array(vector, indexes)
     }
 
+    /// Multiply packed 16-bit integers and shift left by individual shift amounts.
     pub fn mm256_mullo_epi16_shifts(
         vector: __m256i,
         s15: u8,
@@ -1217,6 +1237,7 @@ pub mod extra {
         });
         mm256_mullo_epi16_shifts_array(vector, shifts)
     }
+    /// Multiply packed 16-bit integers and shift left by shift amounts from an array.
     pub fn mm256_mullo_epi16_shifts_array(vector: __m256i, shifts: FunArray<16, u8>) -> __m256i {
         BitVec::from_fn(|i| {
             let nth_bit = i % 16;
@@ -1232,6 +1253,7 @@ pub mod extra {
         })
     }
 
+    /// Store 128-bit integer vector to unaligned byte array.
     #[hax_lib::exclude]
     pub fn mm_storeu_bytes_si128(output: &mut [u8], vector: BitVec<128>) {
         output.copy_from_slice(&vector.to_vec()[..]);
diff --git a/fstar-helpers/core-models/src/core_arch/x86/interpretations.rs b/fstar-helpers/core-models/src/core_arch/x86/interpretations.rs
index 9a8bcba53..332c93569 100644
--- a/fstar-helpers/core-models/src/core_arch/x86/interpretations.rs
+++ b/fstar-helpers/core-models/src/core_arch/x86/interpretations.rs
@@ -9,21 +9,30 @@ pub mod int_vec {
     #[allow(unused)]
     use crate::core_arch::x86;
 
+    /// Broadcast 32-bit integer `x` to all elements of a 256-bit vector
     pub fn _mm256_set1_epi32(x: i32) -> i32x8 {
         i32x8::from_fn(|_| x)
     }
 
+    /// Multiply two 32-bit integers and return the 64-bit result
     pub fn i32_extended64_mul(x: i32, y: i32) -> i64 {
         (x as i64) * (y as i64)
     }
 
+    /// Multiply pairs of 32-bit integers and return 64-bit products
+    ///
+    /// Multiplies the low 32-bit integers from each 64-bit element in x and y
     pub fn _mm256_mul_epi32(x: i32x8, y: i32x8) -> i64x4 {
         i64x4::from_fn(|i| i32_extended64_mul(x[i * 2], y[i * 2]))
     }
+    /// Subtract 32-bit integers in y from corresponding elements in x
     pub fn _mm256_sub_epi32(x: i32x8, y: i32x8) -> i32x8 {
         i32x8::from_fn(|i| x[i].wrapping_sub(y[i]))
     }
 
+    /// Shuffle 32-bit integers within 128-bit lanes using immediate control
+    ///
+    /// CONTROL specifies which elements to select for each position
     pub fn _mm256_shuffle_epi32<const CONTROL: i32>(x: i32x8) -> i32x8 {
         let indexes: FunArray<4, u64> = FunArray::from_fn(|i| ((CONTROL >> i * 2) % 4) as u64);
         i32x8::from_fn(|i| {
@@ -35,25 +44,33 @@ pub mod int_vec {
         })
     }
 
+    /// Blend 32-bit integers from x and y using immediate control mask
+    ///
+    /// CONTROL bits determine whether to select from x (0) or y (1) for each element
     pub fn _mm256_blend_epi32<const CONTROL: i32>(x: i32x8, y: i32x8) -> i32x8 {
         i32x8::from_fn(|i| if (CONTROL >> i) % 2 == 0 { x[i] } else { y[i] })
     }
 
+    /// Return a 256-bit vector with all bits set to zero
     pub fn _mm256_setzero_si256() -> BitVec<256> {
         BitVec::from_fn(|_| Bit::Zero)
     }
+    /// Set 256-bit vector from two 128-bit vectors (hi in upper lane, lo in lower lane)
     pub fn _mm256_set_m128i(hi: BitVec<128>, lo: BitVec<128>) -> BitVec<256> {
         BitVec::from_fn(|i| if i < 128 { lo[i] } else { hi[i - 128] })
     }
 
+    /// Broadcast 16-bit integer to all elements of a 256-bit vector
     pub fn _mm256_set1_epi16(a: i16) -> i16x16 {
         i16x16::from_fn(|_| a)
     }
 
+    /// Broadcast 16-bit integer to all elements of a 128-bit vector
     pub fn _mm_set1_epi16(a: i16) -> i16x8 {
         i16x8::from_fn(|_| a)
     }
 
+    /// Set 128-bit vector from four 32-bit integers (in reverse order)
     pub fn _mm_set_epi32(e3: i32, e2: i32, e1: i32, e0: i32) -> i32x4 {
         i32x4::from_fn(|i| match i {
             0 => e0,
@@ -63,21 +80,28 @@ pub mod int_vec {
             _ => unreachable!(),
         })
     }
+    /// Add 16-bit integers in 128-bit vectors with wrapping
     pub fn _mm_add_epi16(a: i16x8, b: i16x8) -> i16x8 {
         i16x8::from_fn(|i| a[i].wrapping_add(b[i]))
     }
+    /// Add 16-bit integers in 256-bit vectors with wrapping
     pub fn _mm256_add_epi16(a: i16x16, b: i16x16) -> i16x16 {
         i16x16::from_fn(|i| a[i].wrapping_add(b[i]))
     }
 
+    /// Add 32-bit integers in 256-bit vectors with wrapping
     pub fn _mm256_add_epi32(a: i32x8, b: i32x8) -> i32x8 {
         i32x8::from_fn(|i| a[i].wrapping_add(b[i]))
     }
 
+    /// Add 64-bit integers in 256-bit vectors with wrapping
     pub fn _mm256_add_epi64(a: i64x4, b: i64x4) -> i64x4 {
         i64x4::from_fn(|i| a[i].wrapping_add(b[i]))
     }
 
+    /// Compute absolute value of 32-bit integers in 256-bit vector
+    ///
+    /// Special case: i32::MIN returns i32::MIN (unchanged)
     pub fn _mm256_abs_epi32(a: i32x8) -> i32x8 {
         i32x8::from_fn(|i| {
             // See `_mm256_abs_epi32_min`: if the item is `i32::MIN`, the intrinsics returns `i32::MIN`, untouched.
@@ -89,30 +113,46 @@ pub mod int_vec {
         })
     }
 
+    /// Subtract 16-bit integers in 256-bit vectors with wrapping
     pub fn _mm256_sub_epi16(a: i16x16, b: i16x16) -> i16x16 {
         i16x16::from_fn(|i| a[i].wrapping_sub(b[i]))
     }
 
+    /// Subtract 16-bit integers in 128-bit vectors with wrapping
     pub fn _mm_sub_epi16(a: i16x8, b: i16x8) -> i16x8 {
         i16x8::from_fn(|i| a[i].wrapping_sub(b[i]))
     }
 
+    /// Multiply 16-bit integers and return low 16 bits of results
     pub fn _mm_mullo_epi16(a: i16x8, b: i16x8) -> i16x8 {
         i16x8::from_fn(|i| a[i].overflowing_mul(b[i]).0)
     }
 
+    /// Compare 16-bit integers for greater-than and return mask
+    ///
+    /// Returns -1 (all bits set) for true, 0 for false
     pub fn _mm256_cmpgt_epi16(a: i16x16, b: i16x16) -> i16x16 {
         i16x16::from_fn(|i| if a[i] > b[i] { -1 } else { 0 })
     }
 
+    /// Compare 32-bit integers for greater-than and return mask
+    ///
+    /// Returns -1 (all bits set) for true, 0 for false
     pub fn _mm256_cmpgt_epi32(a: i32x8, b: i32x8) -> i32x8 {
         i32x8::from_fn(|i| if a[i] > b[i] { -1 } else { 0 })
     }
 
+    /// Compare 32-bit integers for equality and return mask
+    ///
+    /// Returns -1 (all bits set) for true, 0 for false
     pub fn _mm256_cmpeq_epi32(a: i32x8, b: i32x8) -> i32x8 {
         i32x8::from_fn(|i| if a[i] == b[i] { -1 } else { 0 })
     }
 
+    /// Apply sign of 32-bit integers in b to corresponding elements in a
+    ///
+    /// Returns: -a[i] if b[i] < 0, a[i] if b[i] > 0, 0 if b[i] == 0
+    /// Special case: i32::MIN returns i32::MIN when negated
     pub fn _mm256_sign_epi32(a: i32x8, b: i32x8) -> i32x8 {
         i32x8::from_fn(|i| {
             if b[i] < 0 {
@@ -130,14 +170,23 @@ pub mod int_vec {
         })
     }
 
+    /// Cast 256-bit integer vector to single-precision floating point vector
+    ///
+    /// This is a no-op cast that doesn't change the bit representation
     pub fn _mm256_castsi256_ps(a: BitVec<256>) -> BitVec<256> {
         a
     }
 
+    /// Cast 256-bit single-precision floating point vector to integer vector
+    ///
+    /// This is a no-op cast that doesn't change the bit representation
     pub fn _mm256_castps_si256(a: BitVec<256>) -> BitVec<256> {
         a
     }
 
+    /// Create mask from most significant bits of 32-bit elements
+    ///
+    /// Sets bit i in result if element i has its sign bit set
     pub fn _mm256_movemask_ps(a: i32x8) -> i32 {
         let a0: i32 = if a[0] < 0 { 1 } else { 0 };
         let a1 = if a[1] < 0 { 2 } else { 0 };
@@ -150,24 +199,29 @@ pub mod int_vec {
         a0 + a1 + a2 + a3 + a4 + a5 + a6 + a7
     }
 
+    /// Multiply 16-bit integers and return high 16 bits of results
     #[hax_lib::fstar::options("--z3rlimit 200")]
     pub fn _mm_mulhi_epi16(a: i16x8, b: i16x8) -> i16x8 {
         i16x8::from_fn(|i| ((a[i] as i32) * (b[i] as i32) >> 16) as i16)
     }
 
+    /// Multiply 32-bit integers and return low 32 bits of results
     pub fn _mm256_mullo_epi32(a: i32x8, b: i32x8) -> i32x8 {
         i32x8::from_fn(|i| a[i].overflowing_mul(b[i]).0)
     }
 
+    /// Multiply 16-bit integers and return high 16 bits of results (256-bit version)
     #[hax_lib::fstar::verification_status(lax)]
     pub fn _mm256_mulhi_epi16(a: i16x16, b: i16x16) -> i16x16 {
         i16x16::from_fn(|i| ((a[i] as i32) * (b[i] as i32) >> 16) as i16)
     }
 
+    /// Multiply pairs of unsigned 32-bit integers and return 64-bit products
     pub fn _mm256_mul_epu32(a: u32x8, b: u32x8) -> u64x4 {
         u64x4::from_fn(|i| (a[i * 2] as u64) * (b[i * 2] as u64))
     }
 
+    /// Compute bitwise AND of two 256-bit vectors
     pub fn _mm256_and_si256(a: BitVec<256>, b: BitVec<256>) -> BitVec<256> {
         BitVec::from_fn(|i| match (a[i], b[i]) {
             (Bit::One, Bit::One) => Bit::One,
@@ -175,6 +229,7 @@ pub mod int_vec {
         })
     }
 
+    /// Compute bitwise OR of two 256-bit vectors
     pub fn _mm256_or_si256(a: BitVec<256>, b: BitVec<256>) -> BitVec<256> {
         BitVec::from_fn(|i| match (a[i], b[i]) {
             (Bit::Zero, Bit::Zero) => Bit::Zero,
@@ -182,6 +237,9 @@ pub mod int_vec {
         })
     }
 
+    /// Test whether the bitwise AND of two 256-bit vectors is all zeros
+    ///
+    /// Returns 1 if (a AND b) is all zeros, 0 otherwise
     pub fn _mm256_testz_si256(a: BitVec<256>, b: BitVec<256>) -> i32 {
         let c = BitVec::<256>::from_fn(|i| match (a[i], b[i]) {
             (Bit::One, Bit::One) => Bit::One,
@@ -195,6 +253,7 @@ pub mod int_vec {
         }
     }
 
+    /// Compute bitwise XOR of two 256-bit vectors
     pub fn _mm256_xor_si256(a: BitVec<256>, b: BitVec<256>) -> BitVec<256> {
         BitVec::from_fn(|i| match (a[i], b[i]) {
             (Bit::Zero, Bit::Zero) => Bit::Zero,
@@ -203,6 +262,9 @@ pub mod int_vec {
         })
     }
 
+    /// Shift 16-bit integers right by immediate count with sign extension
+    ///
+    /// If shift count > 15, fills with sign bit
     pub fn _mm256_srai_epi16<const IMM8: i32>(a: i16x16) -> i16x16 {
         i16x16::from_fn(|i| {
             let imm8 = IMM8.rem_euclid(256);
@@ -218,6 +280,7 @@ pub mod int_vec {
         })
     }
 
+    /// Shift right arithmetic packed 32-bit integers by immediate count.
     pub fn _mm256_srai_epi32<const IMM8: i32>(a: i32x8) -> i32x8 {
         i32x8::from_fn(|i| {
             let imm8 = IMM8.rem_euclid(256);
@@ -233,6 +296,7 @@ pub mod int_vec {
         })
     }
 
+    /// Shift right logical packed 16-bit integers by immediate count.
     pub fn _mm256_srli_epi16<const IMM8: i32>(a: i16x16) -> i16x16 {
         i16x16::from_fn(|i| {
             let imm8 = IMM8.rem_euclid(256);
@@ -244,6 +308,7 @@ pub mod int_vec {
         })
     }
 
+    /// Shift right logical packed 32-bit integers by immediate count.
     pub fn _mm256_srli_epi32<const IMM8: i32>(a: i32x8) -> i32x8 {
         i32x8::from_fn(|i| {
             let imm8 = IMM8.rem_euclid(256);
@@ -255,6 +320,7 @@ pub mod int_vec {
         })
     }
 
+    /// Shift right logical packed 64-bit integers by immediate count.
     pub fn _mm_srli_epi64<const IMM8: i32>(a: i64x2) -> i64x2 {
         i64x2::from_fn(|i| {
             let imm8 = IMM8.rem_euclid(256);
@@ -266,6 +332,7 @@ pub mod int_vec {
         })
     }
 
+    /// Shift left logical packed 32-bit integers by immediate count.
     pub fn _mm256_slli_epi32<const IMM8: i32>(a: i32x8) -> i32x8 {
         i32x8::from_fn(|i| {
             let imm8 = IMM8.rem_euclid(256);
@@ -277,11 +344,13 @@ pub mod int_vec {
         })
     }
 
+    /// Permute packed 64-bit integers using immediate control value.
     pub fn _mm256_permute4x64_epi64<const IMM8: i32>(a: i64x4) -> i64x4 {
         let indexes: FunArray<4, u64> = FunArray::from_fn(|i| ((IMM8 >> i * 2) % 4) as u64);
         i64x4::from_fn(|i| a[indexes[i]])
     }
 
+    /// Unpack and interleave high-order 64-bit integers from two vectors.
     pub fn _mm256_unpackhi_epi64(a: i64x4, b: i64x4) -> i64x4 {
         i64x4::from_fn(|i| match i {
             0 => a[1],
@@ -292,6 +361,7 @@ pub mod int_vec {
         })
     }
 
+    /// Unpack and interleave low-order 32-bit integers from two vectors.
     pub fn _mm256_unpacklo_epi32(a: i32x8, b: i32x8) -> i32x8 {
         i32x8::from_fn(|i| match i {
             0 => a[0],
@@ -306,6 +376,7 @@ pub mod int_vec {
         })
     }
 
+    /// Unpack and interleave high-order 32-bit integers from two vectors.
     pub fn _mm256_unpackhi_epi32(a: i32x8, b: i32x8) -> i32x8 {
         i32x8::from_fn(|i| match i {
             0 => a[2],
@@ -320,14 +391,17 @@ pub mod int_vec {
         })
     }
 
+    /// Cast a 128-bit integer vector to a 256-bit integer vector, zeroing the upper 128 bits.
     pub fn _mm256_castsi128_si256(a: BitVec<128>) -> BitVec<256> {
         BitVec::from_fn(|i| if i < 128 { a[i] } else { Bit::Zero })
     }
 
+    /// Convert packed 16-bit integers to packed 32-bit integers with sign extension.
     pub fn _mm256_cvtepi16_epi32(a: i16x8) -> i32x8 {
         i32x8::from_fn(|i| a[i] as i32)
     }
 
+    /// Pack 16-bit integers from two vectors into 8-bit integers with signed saturation.
     pub fn _mm_packs_epi16(a: i16x8, b: i16x8) -> i8x16 {
         i8x16::from_fn(|i| {
             if i < 8 {
@@ -350,6 +424,7 @@ pub mod int_vec {
         })
     }
 
+    /// Pack 32-bit integers from two vectors into 16-bit integers with signed saturation.
     pub fn _mm256_packs_epi32(a: i32x8, b: i32x8) -> i16x16 {
         i16x16::from_fn(|i| {
             if i < 4 {
@@ -388,6 +463,7 @@ pub mod int_vec {
         })
     }
 
+    /// Insert a 128-bit integer into a 256-bit vector at the position specified by immediate.
     pub fn _mm256_inserti128_si256<const IMM8: i32>(a: i128x2, b: i128x1) -> i128x2 {
         i128x2::from_fn(|i| {
             if IMM8 % 2 == 0 {
@@ -406,6 +482,7 @@ pub mod int_vec {
         })
     }
 
+    /// Blend packed 16-bit integers using immediate control mask.
     pub fn _mm256_blend_epi16<const IMM8: i32>(a: i16x16, b: i16x16) -> i16x16 {
         i16x16::from_fn(|i| {
             if (IMM8 >> (i % 8)) % 2 == 0 {
@@ -416,10 +493,12 @@ pub mod int_vec {
         })
     }
 
+    /// Blend packed single-precision floating-point values using mask.
     pub fn _mm256_blendv_ps(a: i32x8, b: i32x8, mask: i32x8) -> i32x8 {
         i32x8::from_fn(|i| if mask[i] < 0 { b[i] } else { a[i] })
     }
 
+    /// Create mask from the most significant bit of each 8-bit element.
     #[hax_lib::fstar::verification_status(lax)]
     pub fn _mm_movemask_epi8(a: i8x16) -> i32 {
         let a0 = if a[0] < 0 { 1 } else { 0 };
@@ -442,6 +521,7 @@ pub mod int_vec {
         a0 + a1 + a2 + a3 + a4 + a5 + a6 + a7 + a8 + a9 + a10 + a11 + a12 + a13 + a14 + a15
     }
 
+    /// Variable right shift packed 64-bit integers.
     pub fn _mm256_srlv_epi64(a: i64x4, b: i64x4) -> i64x4 {
         i64x4::from_fn(|i| {
             if b[i] > 63 || b[i] < 0 {
@@ -452,6 +532,7 @@ pub mod int_vec {
         })
     }
 
+    /// Variable left shift packed 32-bit integers.
     pub fn _mm_sllv_epi32(a: i32x4, b: i32x4) -> i32x4 {
         i32x4::from_fn(|i| {
             if b[i] > 31 || b[i] < 0 {
@@ -462,6 +543,7 @@ pub mod int_vec {
         })
     }
 
+    /// Shift left logical packed 64-bit integers by immediate count.
     pub fn _mm256_slli_epi64<const IMM8: i32>(a: i64x4) -> i64x4 {
         i64x4::from_fn(|i| {
             let imm8 = IMM8 % 256;
@@ -473,6 +555,7 @@ pub mod int_vec {
         })
     }
 
+    /// Shift right logical packed 128-bit integers by immediate count in bytes.
     pub fn _mm256_bsrli_epi128<const IMM8: i32>(a: i128x2) -> i128x2 {
         i128x2::from_fn(|i| {
             let tmp = IMM8 % 256;
@@ -481,6 +564,7 @@ pub mod int_vec {
         })
     }
 
+    /// Compute bitwise AND NOT of two 256-bit vectors.
     pub fn _mm256_andnot_si256(a: BitVec<256>, b: BitVec<256>) -> BitVec<256> {
         BitVec::from_fn(|i| match (a[i], b[i]) {
             (Bit::Zero, Bit::One) => Bit::One,
@@ -488,10 +572,12 @@ pub mod int_vec {
         })
     }
 
+    /// Set packed 64-bit integers with the supplied value.
     pub fn _mm256_set1_epi64x(a: i64) -> i64x4 {
         i64x4::from_fn(|_| a)
     }
 
+    /// Set packed 64-bit integers with the supplied values.
     pub fn _mm256_set_epi64x(e3: i64, e2: i64, e1: i64, e0: i64) -> i64x4 {
         i64x4::from_fn(|i| match i {
             0 => e0,
@@ -502,6 +588,7 @@ pub mod int_vec {
         })
     }
 
+    /// Unpack and interleave low-order 64-bit integers from two vectors.
     pub fn _mm256_unpacklo_epi64(a: i64x4, b: i64x4) -> i64x4 {
         i64x4::from_fn(|i| match i {
             0 => a[0],
@@ -512,6 +599,7 @@ pub mod int_vec {
         })
     }
 
+    /// Permute 128-bit integer lanes using immediate control value.
     pub fn _mm256_permute2x128_si256<const IMM8: i32>(a: i128x2, b: i128x2) -> i128x2 {
         i128x2::from_fn(|i| {
             let control = IMM8 >> (i * 4);
diff --git a/fstar-helpers/core-models/src/lib.rs b/fstar-helpers/core-models/src/lib.rs
index 9fbd0738b..5539999de 100644
--- a/fstar-helpers/core-models/src/lib.rs
+++ b/fstar-helpers/core-models/src/lib.rs
@@ -29,8 +29,10 @@
 // We test functions with const generics, the macro generate a test per possible (const generic) control value.
 #![recursion_limit = "2048"]
 pub mod abstractions;
+/// X86 architecture-specific functions and types modeled in pure Rust.
 pub mod core_arch;
 
 pub use core_arch as arch;
 
+/// Helper functions and utilities for working with core models.
 pub mod helpers;

From c918affcd0b1bed58a8eb049ac12885f79342065 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 18:17:04 +0200
Subject: [PATCH 11/15] Add cavp doc comments

---
 cavp/src/lib.rs | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/cavp/src/lib.rs b/cavp/src/lib.rs
index 1c01db6dc..0cf897418 100644
--- a/cavp/src/lib.rs
+++ b/cavp/src/lib.rs
@@ -1,3 +1,8 @@
+//! CAVP (Cryptographic Algorithm Validation Program) test vector parser.
+//!
+//! This crate provides functionality to read and parse CAVP test vectors
+//! for various cryptographic algorithms including SHA3 and SHAKE.
+
 use core::fmt;
 use std::{
     fs::File,
@@ -19,14 +24,18 @@ pub fn read_string<Ty: Tv>(tv: &str) -> Result<TestVector<Ty>, Error> {
 /// Errors
 #[derive(Debug, Clone, Copy)]
 pub enum Error {
+    /// Failed to open the test vector file
     FileOpen,
+    /// Failed to read or parse test vector data
     Read,
 }
 
 /// A CAVP test vector.
 #[derive(Debug, Clone, Default)]
 pub struct TestVector<TestType: Tv> {
+    /// Header information for the test vector
     pub header: TestType::H,
+    /// Collection of individual test cases
     pub tests: Vec<TestType::T>,
 }
 
@@ -123,7 +132,9 @@ use helper::*;
 pub struct Sha3Test {
     /// Note that `msg_length` is not necessary the same as `msg.len()`
     pub msg_length: usize,
+    /// Input message bytes
     pub msg: Vec<u8>,
+    /// Expected SHA3 digest output
     pub digest: Vec<u8>,
 }
 
@@ -131,6 +142,7 @@ pub struct Sha3Test {
 #[derive(Debug, Clone, Default)]
 pub struct Sha3Header {}
 
+/// SHA3 test vector type
 #[derive(Debug, Clone, Default)]
 pub struct Sha3 {}
 impl Tv for Sha3 {
@@ -181,7 +193,9 @@ impl Test for Sha3Test {
 pub struct ShakeMsgTest {
     /// Note that `msg_length` is not necessary the same as `msg.len()`
     pub msg_length: usize,
+    /// Input message bytes
     pub msg: Vec<u8>,
+    /// Expected SHAKE digest output
     pub digest: Vec<u8>,
 }
 

From ec31d2eaf09fbd6df902c6ea9de72868335699be Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 18:17:21 +0200
Subject: [PATCH 12/15] Ignore missing doc comments in hacl-rs

---
 hacl-rs/src/lib.rs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/hacl-rs/src/lib.rs b/hacl-rs/src/lib.rs
index 205c5a7fa..bbcbd15a8 100644
--- a/hacl-rs/src/lib.rs
+++ b/hacl-rs/src/lib.rs
@@ -4,6 +4,7 @@
 //! hacl-star commit: efbf82f29190e2aecdac8899e4f42c8cb9defc98
 
 #![no_std]
+#![allow(missing_docs)]
 
 // Utility modules. In the generated hacl-rs, these are individual crates.
 pub mod bignum;

From 7ebfa6c9b317dc48e74b7f4065f3fc073259cda5 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 18:17:37 +0200
Subject: [PATCH 13/15] Add libcrux-traits doc comments

---
 traits/src/aead.rs             |  2 ++
 traits/src/aead/tests.rs       |  4 ++++
 traits/src/aead/typed_owned.rs | 18 ++++++++++++++++++
 traits/src/aead/typed_refs.rs  |  4 ++++
 traits/src/ecdh/slice.rs       |  4 ++++
 traits/src/lib.rs              |  7 +++++++
 6 files changed, 39 insertions(+)

diff --git a/traits/src/aead.rs b/traits/src/aead.rs
index 33801749c..09b83106a 100644
--- a/traits/src/aead.rs
+++ b/traits/src/aead.rs
@@ -1,8 +1,10 @@
 pub mod arrayref;
+/// Constants defining AEAD algorithm parameters.
 pub mod consts;
 pub mod owned;
 pub mod secrets;
 pub mod slice;
+/// Test utilities for AEAD implementations.
 pub mod tests;
 
 pub mod typed_owned;
diff --git a/traits/src/aead/tests.rs b/traits/src/aead/tests.rs
index 5a3ec32e0..dd2eab72b 100644
--- a/traits/src/aead/tests.rs
+++ b/traits/src/aead/tests.rs
@@ -1,5 +1,9 @@
 use super::arrayref::*;
 
+/// A simple test function that exercises basic AEAD encrypt/decrypt functionality.
+///
+/// This function performs a round-trip encryption and decryption operation using
+/// the provided AEAD implementation and verifies that the original plaintext is recovered.
 pub fn simple<
     const KEY_LEN: usize,
     const TAG_LEN: usize,
diff --git a/traits/src/aead/typed_owned.rs b/traits/src/aead/typed_owned.rs
index db76d1447..c6c546307 100644
--- a/traits/src/aead/typed_owned.rs
+++ b/traits/src/aead/typed_owned.rs
@@ -12,10 +12,15 @@ use libcrux_secrets::U8;
 // make these associated types. That would mean that we'd have to define them separately for all
 // implementations.
 
+/// A cryptographic key wrapper that ensures type safety for specific AEAD algorithms.
 #[repr(transparent)]
 pub struct Key<Algo: Aead>(Algo::Key);
+
+/// An authentication tag wrapper that ensures type safety for specific AEAD algorithms.
 #[repr(transparent)]
 pub struct Tag<Algo: Aead>(Algo::Tag);
+
+/// A nonce wrapper that ensures type safety for specific AEAD algorithms.
 #[repr(transparent)]
 pub struct Nonce<Algo: Aead>(Algo::Nonce);
 
@@ -26,8 +31,11 @@ pub struct Nonce<Algo: Aead>(Algo::Nonce);
 /// here. Check the documentation of the types implementing this trait to make sure which inputs
 /// are valid.
 pub trait Aead: Sized + AeadConsts {
+    /// The key type used by this AEAD algorithm.
     type Key;
+    /// The authentication tag type used by this AEAD algorithm.
     type Tag;
+    /// The nonce type used by this AEAD algorithm.
     type Nonce;
 
     /// Encrypt a plaintext message, producing a ciphertext and an authentication tag.
@@ -54,6 +62,9 @@ pub trait Aead: Sized + AeadConsts {
 }
 
 impl<Algo: Aead> Key<Algo> {
+    /// Encrypt a plaintext message using this key, producing a ciphertext and authentication tag.
+    ///
+    /// The arguments `plaintext` and `ciphertext` must have the same length.
     pub fn encrypt(
         &self,
         ciphertext: &mut [u8],
@@ -65,6 +76,9 @@ impl<Algo: Aead> Key<Algo> {
         Algo::encrypt(ciphertext, tag, self, nonce, aad, plaintext)
     }
 
+    /// Decrypt a ciphertext using this key, verifying its authenticity and producing the plaintext.
+    ///
+    /// The arguments `plaintext` and `ciphertext` must have the same length.
     pub fn decrypt(
         &self,
         plaintext: &mut [U8],
@@ -77,6 +91,10 @@ impl<Algo: Aead> Key<Algo> {
     }
 }
 
+/// Macro to implement the typed owned AEAD trait for a given type with specified key, tag, and nonce lengths.
+///
+/// This macro generates the necessary trait implementation that bridges between the typed owned
+/// interface and the array reference interface.
 #[macro_export]
 macro_rules! impl_aead_typed_owned {
     ($ty:ty, $keylen:expr, $taglen:expr, $noncelen:expr) => {
diff --git a/traits/src/aead/typed_refs.rs b/traits/src/aead/typed_refs.rs
index 9652dc2d1..5ef3ba804 100644
--- a/traits/src/aead/typed_refs.rs
+++ b/traits/src/aead/typed_refs.rs
@@ -176,8 +176,11 @@ impl<'a, Algo: Aead + core::fmt::Debug> core::fmt::Debug for KeyRef<'a, Algo> {
 /// here. Check the documentation of the types implementing this trait to make sure which inputs
 /// are valid.
 pub trait Aead: Copy + PartialEq {
+    /// Returns the key length in bytes for this AEAD algorithm.
     fn key_len(&self) -> usize;
+    /// Returns the authentication tag length in bytes for this AEAD algorithm.
     fn tag_len(&self) -> usize;
+    /// Returns the nonce length in bytes for this AEAD algorithm.
     fn nonce_len(&self) -> usize;
 
     /// Encrypt a plaintext message, producing a ciphertext and an authentication tag.
@@ -328,6 +331,7 @@ impl<
     }
 }
 
+/// Error indicating that a buffer has the wrong length for the expected algorithm parameters.
 #[derive(Debug, Clone, Copy)]
 pub struct WrongLengthError;
 
diff --git a/traits/src/ecdh/slice.rs b/traits/src/ecdh/slice.rs
index b74bcc5d4..6683d0118 100644
--- a/traits/src/ecdh/slice.rs
+++ b/traits/src/ecdh/slice.rs
@@ -5,6 +5,10 @@
 use super::arrayref;
 use libcrux_secrets::U8;
 
+/// Elliptic Curve Diffie-Hellman (ECDH) operations using slice-based arguments.
+///
+/// This trait provides a slice-based interface for ECDH operations, allowing
+/// for flexible buffer sizes while maintaining type safety through length validation.
 pub trait EcdhSlice {
     /// Generate a Diffie-Hellman secret value.
     /// It is the responsibility of the caller to ensure  that the `rand` argument is actually
diff --git a/traits/src/lib.rs b/traits/src/lib.rs
index 4be2d5489..aa7b3452e 100644
--- a/traits/src/lib.rs
+++ b/traits/src/lib.rs
@@ -1,3 +1,9 @@
+//! libcrux-traits provides cryptographic traits for AEAD, digest, ECDH, and KEM algorithms.
+//!
+//! This crate defines generic interfaces for various cryptographic primitives, allowing
+//! different implementations to be used interchangeably. It includes both low-level array-based
+//! traits and higher-level slice-based traits for easier integration.
+
 #![no_std]
 
 extern crate alloc;
@@ -22,6 +28,7 @@ pub trait Digest<const HASH_LEN: usize> {
     fn reset(&mut self);
 }
 
+/// Authenticated Encryption with Associated Data (AEAD) traits and implementations.
 pub mod aead;
 pub mod digest;
 pub mod ecdh;

From 8b7f6808a52a488dbb14b4861c4369542c5979e7 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Wed, 1 Oct 2025 18:20:06 +0200
Subject: [PATCH 14/15] More docs exceptions for generated hacl code

---
 blake2/src/lib.rs | 1 +
 sha2/src/lib.rs   | 1 +
 2 files changed, 2 insertions(+)

diff --git a/blake2/src/lib.rs b/blake2/src/lib.rs
index d2281e383..bb5d68fd2 100644
--- a/blake2/src/lib.rs
+++ b/blake2/src/lib.rs
@@ -1,5 +1,6 @@
 #![cfg_attr(not(feature = "std"), no_std)]
 
+#[allow(missing_docs)]
 mod hacl {
     //! This module contains generated hacl code.
 
diff --git a/sha2/src/lib.rs b/sha2/src/lib.rs
index 2a29e1cdb..7d1597c26 100644
--- a/sha2/src/lib.rs
+++ b/sha2/src/lib.rs
@@ -18,6 +18,7 @@ mod hacl;
 
 /// The generated hacl code
 #[cfg(feature = "expose-hacl")]
+#[allow(missing_docs)]
 pub mod hacl;
 
 /// The implementation of our types using that hacl code

From cc28e56c883cf5769e3fc1fe70d3845601d9b618 Mon Sep 17 00:00:00 2001
From: "Jan Winkelmann (keks)" <jan@cryspen.com>
Date: Thu, 2 Oct 2025 09:46:58 +0200
Subject: [PATCH 15/15] Add libcrux-sha2 doc comments

---
 sha2/src/impl_hacl.rs | 26 ++++++++++++++++++++------
 sha2/src/lib.rs       | 20 ++++++++++++++++++--
 2 files changed, 38 insertions(+), 8 deletions(-)

diff --git a/sha2/src/impl_hacl.rs b/sha2/src/impl_hacl.rs
index 2e6fe32bb..5c4dbaf66 100644
--- a/sha2/src/impl_hacl.rs
+++ b/sha2/src/impl_hacl.rs
@@ -2,17 +2,21 @@ use super::*;
 use libcrux_hacl_rs::prelude::*;
 use libcrux_traits::Digest;
 
-/// The different Sha2 algorithms.
+/// The different SHA-2 algorithms.
 #[derive(Clone, Copy, Debug)]
 pub enum Algorithm {
+    /// Denotes SHA-224
     Sha224,
+    /// Denotes SHA-256
     Sha256,
+    /// Denotes SHA-384
     Sha384,
+    /// Denotes SHA-512
     Sha512,
 }
 
 impl Algorithm {
-    // The length of the digest by algorithm.
+    /// The length of the digest by algorithm.
     pub const fn hash_len(&self) -> usize {
         match self {
             Algorithm::Sha224 => SHA224_LENGTH,
@@ -37,7 +41,8 @@ impl Algorithm {
     }
 }
 
-/// SHA2 224
+/// Computes the 224-bit SHA-2 hash
+///
 /// Will panic if `payload` is longer than `u32::MAX` to ensure that hacl-rs can
 /// process it.
 #[inline(always)]
@@ -47,7 +52,8 @@ pub fn sha224(payload: &[u8]) -> [u8; SHA224_LENGTH] {
     digest
 }
 
-/// SHA2 256
+/// Computes the 256-bit SHA-2 hash
+///
 /// Will panic if `payload` is longer than `u32::MAX` to ensure that hacl-rs can
 /// process it.
 #[inline(always)]
@@ -57,7 +63,8 @@ pub fn sha256(payload: &[u8]) -> [u8; SHA256_LENGTH] {
     digest
 }
 
-/// SHA2 384
+/// Computes the 384-bit SHA-2 hash
+///
 /// Will panic if `payload` is longer than `u32::MAX` to ensure that hacl-rs can
 /// process it.
 #[inline(always)]
@@ -67,7 +74,8 @@ pub fn sha384(payload: &[u8]) -> [u8; SHA384_LENGTH] {
     digest
 }
 
-/// SHA2 512
+/// Computes the 512-bit SHA-2 hash
+///
 /// Will panic if `payload` is longer than `u32::MAX` to ensure that hacl-rs can
 /// process it.
 #[inline(always)]
@@ -81,6 +89,12 @@ pub fn sha512(payload: &[u8]) -> [u8; SHA512_LENGTH] {
 // For implementations based on hacl_rs (over hacl-c)
 macro_rules! impl_hash {
     ($name:ident, $digest_size:literal, $state:ty, $malloc:expr, $reset:expr, $update:expr, $finish:expr, $copy:expr, $hash:expr) => {
+        #[doc = concat!("A streaming hash digest implementation for ", stringify!($name))]
+        ///
+        ///This struct provides stateful hashing functionality with a digest size of
+        #[doc = concat!( stringify!($digest_size))]
+        /// bytes, allowing data to be processed incrementally through
+        /// multiple `update` calls before finalizing the digest.
         #[allow(non_camel_case_types)]
         pub struct $name {
             state: $state,
diff --git a/sha2/src/lib.rs b/sha2/src/lib.rs
index 7d1597c26..a5998cf70 100644
--- a/sha2/src/lib.rs
+++ b/sha2/src/lib.rs
@@ -1,3 +1,21 @@
+//! # libcrux-sha2
+//!
+//! A pure Rust implementation of the SHA-2 family of cryptographic hash functions.
+//!
+//! This crate provides implementations for SHA-224, SHA-256, SHA-384, and SHA-512
+//! hash algorithms. The implementation is based on verified HACL* code and provides
+//! both a simple functional API and trait-based interfaces.
+//!
+//! ## Examples
+//!
+//! ```rust
+//! use libcrux_sha2::{sha256, SHA256_LENGTH};
+//!
+//! let data = b"hello world";
+//! let hash = sha256(data);
+//! assert_eq!(hash.len(), SHA256_LENGTH);
+//! ```
+
 #![no_std]
 
 /// The length of a SHA224 hash in bytes.
@@ -26,10 +44,8 @@ mod impl_hacl;
 
 mod impl_digest_trait;
 
-/// use it if we want to use hacl
 pub use impl_hacl::*;
 
-/// Re-export the `Digest` trait.
 pub use libcrux_traits::Digest;
 
 pub use impl_digest_trait::*;