version bumps, MAX_RECV_SEEN patch, FIPS interop, doc updates

Abstract.md

@@ -646,14 +646,11 @@ recv_seen, prev_recv_seen, local_fp, remote_fp, epoch)
 - (d) s = 0 ∧ sk_s set is unreachable.
 - (e) s = 0 ∧ pending = ⊥ ∧ pk_r set ∧ sk_s unset is unreachable.
 - (f) prev_ek_r is set iff prev_pk_r is set (co-presence).
-- (g) |recv_seen| ≤ MAX_RECV_SEEN; |prev_recv_seen| ≤ MAX_RECV_SEEN. Note: the
-  runtime bound allows recv_seen to reach exactly MAX_RECV_SEEN entries (the
-  check-before-insert pattern at §5.4 Step 6 passes at MAX_RECV_SEEN − 1, then
-  the insert produces MAX_RECV_SEEN). However, a state with MAX_RECV_SEEN
-  entries cannot be serialized — serialization rejects at |recv_seen| ≥
-  MAX_RECV_SEEN. The serialization invariant is therefore |recv_seen| <
-  MAX_RECV_SEEN. Models reasoning about serialization should use the strict
-  bound.
+- (g) |recv_seen| < MAX_RECV_SEEN; |prev_recv_seen| < MAX_RECV_SEEN. The
+  runtime check (§5.4 Step 6) rejects when a successful insert would push the
+  set to MAX_RECV_SEEN entries, so the live invariant matches the serialization
+  invariant: no reachable live state has MAX_RECV_SEEN or more entries, and
+  every live state is serializable on this dimension.
 - (h) local_fp ≠ remote_fp (self-messaging rejected at construction).
   Additionally, local_fp ≠ 0³² and remote_fp ≠ 0³² (all-zero fingerprint
   rejected at construction; constant-time check). Under SHA3-256 modeled as a
@@ -910,7 +907,7 @@ symmetric rollback for both operations produces an incorrect model.
    replaying a legitimate ciphertext; AEAD succeeds but the plaintext is
    discarded). These must be modeled as separate failure branches with different
    adversary capabilities.
-6. If |seen_set| ≥ MAX_RECV_SEEN: fail (ChainExhausted). seen_set ← seen_set ∪
+6. If |seen_set| + 1 ≥ MAX_RECV_SEEN: fail (ChainExhausted). seen_set ← seen_set ∪
    {n\*}. If epoch is CurrentEpoch or NewEpoch: r ← max(r, n\* + 1).
    (PreviousEpoch messages do not update r — they belong to a prior receive
    epoch, and updating the current-epoch high-water mark would corrupt

CHEATSHEET.md

@@ -294,7 +294,7 @@ Mistakes that compile successfully but produce incorrect or insecure behavior. A
 | `Internal` | -12 | `SOLITON_ERR_INTERNAL` | Structurally unreachable internal invariant violated (bug in soliton) |
 | `NullPointer` | -13 | `SOLITON_ERR_NULL_POINTER` | Null pointer passed for a required argument *(CAPI-only)* |
 | `UnsupportedFlags` | -14 | `SOLITON_ERR_FLAGS` | *(reserved — not currently returned; see footnote)* |
-| `ChainExhausted` | -15 | `SOLITON_ERR_CHAIN_EXHAUSTED` | Counter-space exhausted. Sources: ratchet send/recv counter reaches u32::MAX; call key chain advance limit (2²⁴ = 16,777,216 steps); per-epoch recv_seen set reaches 65536 distinct entries; streaming chunk index reaches u64::MAX |
+| `ChainExhausted` | -15 | `SOLITON_ERR_CHAIN_EXHAUSTED` | Counter-space exhausted. Sources: ratchet send/recv counter reaches u32::MAX; call key chain advance limit (2²⁴ = 16,777,216 steps); per-epoch recv_seen set would grow past 65535 distinct entries; streaming chunk index reaches u64::MAX |
 | `UnsupportedCryptoVersion` | -16 | `SOLITON_ERR_CRYPTO_VERSION` | Peer advertised a crypto version this library does not implement |
 | `InvalidData` | -17 | `SOLITON_ERR_INVALID_DATA` | Structurally invalid content (format error, co-presence violation, implausible values) |
 | `ConcurrentAccess` | -18 | `SOLITON_ERR_CONCURRENT_ACCESS` | Opaque handle is in use by another concurrent operation (reentrancy guard) *(CAPI-only)* |
@@ -420,7 +420,7 @@ All constants have type `&[u8]` (byte-string literals). In Rust, use `b"..."` no
 | `CALL_KEY_B_BYTE` | `&[u8]` | `&[0x05]` | Call key derivation, second call key |
 | `CALL_CHAIN_ADV_BYTE` | `&[u8]` | `&[0x06]` | Call chain key advance |
 | `HKDF_ZERO_SALT` | `[u8; 32]` | `[0u8; 32]` | LO-KEX HKDF salt (§5.4 Step 4) — 32 zero bytes |
-| `MAX_RECV_SEEN` | `u32` | `65536` | recv_seen set cap per epoch; 65536th distinct-counter decrypt succeeds, 65537th returns `ChainExhausted` |
+| `MAX_RECV_SEEN` | `u32` | `65536` | recv_seen set bound per epoch: a live set holds at most 65535 entries (`len < MAX_RECV_SEEN`); the 65536th distinct-counter decrypt returns `ChainExhausted` |
 | `MAX_CALL_ADVANCE` *(internal, not pub)* | `u32` | `16,777,216` (2²⁴) | `CallKeys::advance()` limit; `ChainExhausted` after this many calls. Not in `soliton::constants` — value for reimplementors only. |
 
 ---
@@ -1313,7 +1313,7 @@ pub fn encrypt(&mut self, plaintext: &[u8]) -> Result<EncryptedMessage>
 #[must_use = "decrypted plaintext contains sensitive data that must be consumed or zeroized"]
 pub fn decrypt(&mut self, header: &RatchetHeader, ciphertext: &[u8]) -> Result<Zeroizing<Vec<u8>>>
 // Err(DuplicateMessage) — counter already in recv_seen (state unchanged)
-// Err(ChainExhausted) — counter at u32::MAX, or recv_seen / prev_recv_seen set reached 65536 entries
+// Err(ChainExhausted) — counter at u32::MAX, or recv_seen / prev_recv_seen already holds 65535 entries
 // Err(InvalidData) — ratchet state previously zeroized by reset() or a prior AeadFailed (requires new KEX);
 //   or ratchet step required but no KEM ct in header; or no send secret key
 // Err(DecapsulationFailed) — X-Wing KEM decapsulation failed
@@ -1348,8 +1348,8 @@ pub fn to_bytes(self) -> Result<(Zeroizing<Vec<u8>>, u64)>  // consumes self; re
 // there is no recovery path. Call can_serialize() first; if false, do NOT call to_bytes().
 // Err(ChainExhausted) — send_count, recv_count, prev_send_count == u32::MAX, or epoch == u64::MAX
 // Err(InvalidData) — recv_seen or prev_recv_seen has ≥ 65536 entries (defense-in-depth dead branch:
-//   decrypt's ChainExhausted guard fires at recv_seen.len() == 65536, preventing the set from growing
-//   further, so this InvalidData path is unreachable in normal operation; the global error table lists
+//   decrypt's ChainExhausted guard refuses the insert that would make recv_seen.len() == 65536, so a
+//   live set never exceeds 65535 and this InvalidData path is unreachable in normal operation; the global error table lists
 //   recv_seen exhaustion under ChainExhausted for this reason)
 #[deprecated(note = "Use from_bytes_with_min_epoch for anti-rollback protection")]
 pub fn from_bytes(data: &[u8]) -> Result<Self>  // no rollback protection — always use from_bytes_with_min_epoch

Cargo.toml

@@ -14,7 +14,7 @@ default-members = [
 ]
 
 [workspace.package]
-version = "0.1.3"
+version = "0.1.4"
 edition = "2024"
 rust-version = "1.87"
 license = "AGPL-3.0-only"

REVIEW-2026-09-08.md

@@ -0,0 +1,109 @@
+# libsoliton core review — 2026-09-08 (single-reviewer trial)
+
+## Overall assessment
+
+libsoliton is shippable as reviewed. Across the full primitive stack, the key
+exchange, the double ratchet, streaming/storage AEAD, call keys, auth, and
+verification, I found no defect at medium severity or above. The areas the brief
+flagged as highest-risk are handled correctly and defensively: every AEAD nonce
+is provably unique within its key's lifetime (ratchet counter-mode nonces are a
+strict function of a monotonic `send_count` that aborts at `u32::MAX` before it
+can wrap; the first-message key reuses the epoch key only at counter 0 with a
+random nonce and a distinct AAD; streaming nonces are injective over
+`(index, tag_byte)`; storage uses fresh random nonces). Secret-dependent
+comparisons all use `subtle`/constant-time paths (MAC/token in `auth_verify`,
+all-zero key/secret guards, fingerprint checks against untrusted wire data,
+ratchet-pk epoch identification, shared-secret zero-check in X25519 DH). Key
+material is wrapped in `Zeroizing`/`ZeroizeOnDrop` and every keygen/DH/KEM path
+explicitly zeroizes the `Copy`-type stack staging buffers before returning. The
+double-ratchet state machine is the strongest single piece: `encrypt` is
+atomic-by-ordering (all fallible ops precede any mutation), `decrypt` takes a
+full snapshot and rolls back on any error, duplicate detection is deferred past
+AEAD to avoid a timing oracle, the seen-sets and epoch keys rotate correctly
+across direction changes, and `from_bytes` has an extensive battery of
+structural/co-presence/all-zero guards.
+
+The weakest areas are documentation-vs-code drift and a heavy reliance on
+documented caller obligations, neither of which is a code defect. Two footguns
+that could produce catastrophic nonce reuse — double-`from_bytes` and reusing a
+streaming `(index, is_last)` pair — are real, but both are deprecated/
+`&self`-random-access APIs with explicit in-code warnings and safe alternatives
+(`from_bytes_with_min_epoch`, sequential `encrypt_chunk`), so they fall under the
+brief's "documented decision" exclusion. The one concrete mismatch worth fixing
+is a one-off in the `recv_seen` cap (code is stricter than the docs claim; safe
+direction). I would ship it; the notes below are hygiene, not blockers.
+
+## Findings (medium and above)
+
+None.
+
+## Notes below medium
+
+- **low — `recv_seen`/`prev_recv_seen` cap is off-by-one vs the documentation.**
+  `soliton/src/ratchet/mod.rs:582` (and `:573`) reject with `ChainExhausted` when
+  `self.recv_seen.len() + 1 >= MAX_RECV_SEEN` (65536), i.e. the set can hold at
+  most 65535 entries and the 65536th *distinct*-counter decrypt is rejected. The
+  CHEATSHEET ("the 65536th distinct-counter decrypt succeeds … the 65537th
+  returns `ChainExhausted`") and the `MAX_RECV_SEEN` comment in
+  `soliton/src/constants.rs:83` both state the limit one message higher. The code
+  is the safe/conservative side (it keeps the live set always serializable,
+  matching the `>= MAX_RECV_SEEN` reject in `to_bytes` at `:1060`/`:1074` and
+  `from_bytes` at `:1292`/`:1316`), so this is a doc/reimplementor-guidance error,
+  not a security defect. No test would catch it without a 65k-message epoch.
+
+- **info — contradictory comments about HKDF PRK zeroization.**
+  `soliton/src/primitives/hkdf.rs:19-22` states "The `hkdf` crate's internal PRK
+  is **not** zeroized on drop (`hkdf 0.13.0-rc.5` has no `zeroize` feature)",
+  while `soliton/soliton/Cargo.toml:26-29` explains that `sha3` 0.11-rc + the
+  `hmac` `zeroize` feature were chosen specifically so the keyed SHA3 state used
+  by HMAC/HKDF is `ZeroizeOnDrop`. Since `Hkdf<Sha3_256>` stores its PRK as an
+  `Hmac<Sha3_256>` field, that field's drop should in fact zeroize the PRK. The
+  two comments can't both be right; reconcile them so maintainers don't reason
+  from the pessimistic one. Either way the PRK lifetime is a short-lived local,
+  so the practical exposure is minimal.
+
+- **info — streaming compressed-empty non-final chunk skips the size check.**
+  `soliton/src/streaming.rs:527` gates decompression on
+  `self.compressed && !decrypted.is_empty()`; a compressed *non-final* chunk that
+  AEAD-decrypts to zero bytes would return `(empty, is_last=false)` without the
+  `decompressed.len() != STREAM_CHUNK_SIZE` guard at `:533`. Unreachable in
+  practice: producing a valid AEAD chunk requires the stream key, and the
+  legitimate encryptor never emits an empty non-final chunk (non-final plaintext
+  must be exactly `STREAM_CHUNK_SIZE`, which compresses to non-empty). Latent
+  only.
+
+- **info — `Copy`-typed key material leaves brief stack residue by design.**
+  `random::random_array`, `hmac_sha3_256`, and the various `[u8; 32]` deref-copies
+  documented throughout return `Copy` values the callee can't zeroize. Every
+  in-library use zeroizes the staging copy (e.g. `x25519.rs:62`, `mlkem.rs:162`,
+  `call.rs:312`, `ratchet.rs:174`), and the hazard is called out in the
+  CHEATSHEET for callers. Noted for completeness, not a defect.
+
+- **info — nonce-reuse footguns are deprecated/documented, not defects.**
+  Double-`from_bytes` (`ratchet/mod.rs:1114`, `#[deprecated]`, with an explicit
+  double-deserialization warning and the `from_bytes_with_min_epoch` safe path)
+  and reusing a streaming `(index, is_last)` pair via `encrypt_chunk_at`
+  (`streaming.rs:281`, explicit SECURITY warning) both cause catastrophic nonce
+  reuse if misused, but each ships with a safe alternative and in-code warnings.
+
+## Coverage
+
+Read in full (to the test boundary given in the brief), in dependency order:
+`README.md`; `CHEATSHEET.md` (all 2354 lines); `soliton/Cargo.toml`;
+`src/lib.rs`; `src/error.rs`; `src/constants.rs` (1–163); `src/primitives/mod.rs`;
+`src/primitives/random.rs` (1–34); `src/primitives/sha3_256.rs` (1–28);
+`src/primitives/hmac.rs` (1–40); `src/primitives/hkdf.rs` (1–44);
+`src/primitives/aead.rs` (1–109); `src/primitives/ed25519.rs` (1–58);
+`src/primitives/x25519.rs` (1–105); `src/primitives/mlkem.rs` (1–314);
+`src/primitives/mldsa.rs` (1–436); `src/primitives/xwing.rs` (1–395);
+`src/primitives/argon2.rs` (1–145); `src/identity/mod.rs` (1–349);
+`src/auth/mod.rs` (1–102); `src/kex/mod.rs` (1–924); `src/verification.rs`
+(1–125); `src/ratchet/mod.rs` (1–1606); `src/streaming.rs` (1–549);
+`src/storage/mod.rs` (1–593); `src/call.rs` (1–318). No file was skimmed; every
+allowed source file was read line-by-line. Test modules, `tests/`, `benches/`,
+`fuzz/`, `build.rs`, `Specification.md`, `Abstract.md`, and all non-core crates
+were not opened, per the brief. No build or scratch experiment was needed — the
+notes were settled by reading. Constants in `constants.rs` were cross-checked
+against the standard sizes (ML-KEM-768 1184/2400/1088, ML-DSA-65 1952/3309/32
+seed, X25519/Ed25519 32/64, X-Wing 1216/2432/1120, composite 3200/2496, hybrid
+sig 3373) and against every use site; all agree.

Specification.md

@@ -1416,7 +1416,7 @@ function Decrypt(state, header, ciphertext, sender_fp, recipient_fp):
         if header.n in state.prev_recv_seen:
             restore_recv_state(state, snapshot)
             raise DuplicateMessage
-        if |state.prev_recv_seen| >= MAX_RECV_SEEN:
+        if |state.prev_recv_seen| + 1 >= MAX_RECV_SEEN:
             restore_recv_state(state, snapshot)
             raise ChainExhausted
         state.prev_recv_seen.add(header.n)
@@ -1434,7 +1434,7 @@ function Decrypt(state, header, ciphertext, sender_fp, recipient_fp):
         if header.n in state.recv_seen:
             restore_recv_state(state, snapshot)
             raise DuplicateMessage
-        if |state.recv_seen| >= MAX_RECV_SEEN:
+        if |state.recv_seen| + 1 >= MAX_RECV_SEEN:
             restore_recv_state(state, snapshot)
             raise ChainExhausted
         state.recv_seen.add(header.n)
@@ -1586,7 +1586,7 @@ Ratchet state is serialized for encrypted persistent storage. The caller MUST au
 
 **Serialization buffer zeroization**: The serialization output buffer contains root keys, epoch keys, and ratchet secret keys — all secret material. Implementations SHOULD pre-allocate the buffer to its exact final size before writing any data. If a dynamic array (Vec, list, slice) reallocates during serialization, the abandoned allocation containing partial secret material is freed to the heap allocator without zeroization — only the final allocation is covered by zeroize-on-drop. In Rust, pre-allocation is the actual guarantee; a `debug_assert` on capacity detects underestimates during testing but is compiled out in release builds — if the pre-computed size is wrong, a release binary silently reallocates and the abandoned partial allocation is freed without zeroization. In C/Go/Python, pre-compute the buffer size and allocate once. The output buffer itself MUST be zeroized after the caller has finished with it (e.g., after passing it to storage encryption).
 
-**MAX_RECV_SEEN cap at runtime**: When `recv_seen` or `prev_recv_seen` reaches `MAX_RECV_SEEN` (65536) entries during decrypt, subsequent messages in that epoch return `ChainExhausted`. This is transient — the cap resets on the next KEM ratchet step (which clears `recv_seen`). The cap prevents unbounded memory growth from an authenticated peer sending many messages in a single epoch.
+**MAX_RECV_SEEN cap at runtime**: When `recv_seen` or `prev_recv_seen` reaches `MAX_RECV_SEEN - 1` (65535) entries during decrypt, the next message in that epoch returns `ChainExhausted` — the runtime check rejects when a successful insert would push the set to `MAX_RECV_SEEN`, matching the serialization invariant (`|recv_seen| < MAX_RECV_SEEN`). This is transient — the cap resets on the next KEM ratchet step (which clears `recv_seen`). The cap prevents unbounded memory growth from an authenticated peer sending many messages in a single epoch.
 
 **Which epoch paths can fire this cap**: The `recv_seen` saturation check (`ChainExhausted`) fires only on the **current-epoch path** (messages in the active receive epoch) and the **previous-epoch path** (messages in the prior epoch, checked against `prev_recv_seen`). The **new-epoch path** (which triggers a KEM ratchet step) is immune: it clears `recv_seen` to empty before the duplicate/cap check, so the cap check on that path is structurally unreachable — a new epoch always starts with an empty `recv_seen`. A reimplementer testing `ChainExhausted` from `recv_seen` saturation MUST use the current-epoch or previous-epoch path, not the new-epoch path.
 

soliton/Cargo.toml

@@ -77,7 +77,19 @@ ed25519-dalek = { version = "=2.2.0", default-features = false, features = ["zer
 # stacks are isolated at the type level and never share state.
 ml-kem = { version = "=0.2.3", features = ["zeroize", "deterministic"] }
 kem = "=0.3.0-pre.0"
-ml-dsa = { version = "=0.1.0-rc.7", features = ["zeroize"] }
+# `default-features = false` drops ml-dsa's `pkcs8` and `rand_core` features.
+# soliton uses neither: keys and signatures cross the boundary as raw encodings
+# (B32, EncodedVerifyingKey, EncodedSignature), and keygen seeds `from_seed`
+# with bytes from soliton's own CSPRNG rather than a rand_core Rng.
+#
+# This is load-bearing, not tidiness. ml-dsa 0.1.0-rc.7 requires
+# `pkcs8 = "0.11.0-rc.10"`, which Cargo reads as `>=0.11.0-rc.10, <0.12.0` — so
+# once pkcs8 0.11.0 final shipped it outranked every rc and got selected, and
+# ml-dsa's `pkcs8.rs` stopped compiling (`?` cannot convert into the reshaped
+# `Error`). That broke a fresh `cargo add libsoliton`, since a library's
+# Cargo.lock does not constrain downstream resolution. With the feature off,
+# `pkcs8.rs` is never compiled and the breakage is unreachable.
+ml-dsa = { version = "=0.1.0-rc.7", default-features = false, features = ["zeroize", "alloc"] }
 # rand_core is pulled transitively by ml-kem (0.6) and ml-dsa (0.10).
 # Deterministic/seed-based APIs + getrandom are used to avoid RNG trait issues.
 
@@ -107,7 +119,9 @@ proptest = "=1.10.0"
 rayon = "=1.11.0"
 # ml-dsa is a direct dependency, re-declared here so integration tests can call
 # sign_internal directly to produce deterministic F.27 test vectors (pinned rnd).
-ml-dsa = { version = "=0.1.0-rc.7", features = ["zeroize"] }
+# Feature set must match the [dependencies] entry — see the note there for why
+# default features are off.
+ml-dsa = { version = "=0.1.0-rc.7", default-features = false, features = ["zeroize", "alloc"] }
 
 [[bench]]
 name = "bench"

soliton/fuzz/Cargo.lock

@@ -435,7 +435,7 @@ dependencies = [
 
 [[package]]
 name = "libsoliton"
-version = "0.1.3"
+version = "0.1.4"
 dependencies = [
  "argon2",
  "chacha20poly1305",

soliton/src/constants.rs

@@ -79,10 +79,12 @@ pub const MSG_KEY_DOMAIN_BYTE: u8 = 0x01;
 /// Zero salt for HKDF in LO-KEX (§5.4 Step 4).
 pub const HKDF_ZERO_SALT: [u8; 32] = [0u8; 32];
 
-/// Maximum entries in recv_seen set per epoch (§6.7). Prevents memory
+/// Bound on the recv_seen set per epoch (§6.7): a live set holds fewer than
+/// this many entries (at most 65535); `decrypt` refuses the insert that would
+/// reach it and `to_bytes` rejects a set at or above it. Prevents memory
 /// exhaustion from an adversary sending messages with many distinct counter
-/// values. The set stores only 4-byte counters (not keys), so 65536 entries
-/// is ~256 KB. Resets on each KEM ratchet step.
+/// values. The set stores only 4-byte counters (not keys), so the bound is
+/// ~256 KB. Resets on each KEM ratchet step.
 pub const MAX_RECV_SEEN: u32 = 65536;
 
 /// Ratchet state serialization format version. Checked on deserialization;

soliton/src/primitives/hkdf.rs

@@ -16,10 +16,19 @@ use sha3::Sha3_256;
 /// # Security
 ///
 /// The caller is responsible for zeroizing the `out` buffer when the derived
-/// key material is no longer needed. The `hkdf` crate's internal PRK is
-/// **not** zeroized on drop (`hkdf 0.13.0-rc.5` has no `zeroize` feature).
-/// Mitigation: `Hkdf` is a short-lived local — PRK lifetime is bounded to
-/// this function scope, and `panic = "abort"` prevents unwinding.
+/// key material is no longer needed.
+///
+/// What the dependencies zeroize, verified against the pinned sources
+/// (`hkdf 0.13.0-rc.5`, `hmac 0.13.0-rc.5`, `sha3 0.11.0-rc.7`,
+/// `digest 0.11.0-rc.11`, `block-buffer 0.11.0`, all with their `zeroize`
+/// features resolved on): dropping the `Hkdf` zeroizes the PRK-keyed HMAC
+/// state — both SHA3 cores through `sha3`'s `Drop` and the wrapper's block
+/// buffer through `block-buffer`'s. `hkdf` itself has no `zeroize` feature
+/// and leaves three plain stack copies behind: the raw 32-byte PRK that
+/// `Hkdf::new` extracts and discards, the `key ^ OPAD` block that
+/// `HmacCore::new_from_slice` builds in a local, and the last output block
+/// that `expand` keeps in a local. All three are bounded to this function's
+/// frame, and `panic = "abort"` prevents unwinding past it.
 pub fn hkdf_sha3_256(salt: &[u8], ikm: &[u8], info: &[u8], out: &mut [u8]) -> Result<()> {
     if out.is_empty() {
         return Err(Error::InvalidLength {

soliton/src/primitives/mldsa.rs

@@ -302,6 +302,138 @@ pub fn verify(pk: &PublicKey, message: &[u8], signature: &Signature) -> Result<(
     }
 }
 
+/// Sign with the FIPS 204 §5.2 ML-DSA.Sign envelope (domain separator +
+/// context string).
+///
+/// This is the **standard ML-DSA.Sign** algorithm — equivalent to what
+/// any FIPS 204-compliant implementation produces (rustls/aws-lc-rs,
+/// OpenSSL once they ship PQ, hardware tokens). Use it whenever a
+/// signature must verify under a generic ML-DSA-65 verifier.
+///
+/// Constructs `M' = 0x00 || len(ctx) || ctx || M` per FIPS 204 §5.2,
+/// then signs M' via the underlying primitive. Distinct from
+/// [`sign`], which signs M directly (no prefix) — soliton's
+/// non-standard mode used by intra-Lo signatures that are always
+/// verified by soliton itself.
+///
+/// `ctx` is the FIPS 204 context string. For TLS 1.3 use it MUST be
+/// empty (`b""`) per `draft-ietf-tls-mldsa`. Other protocol-specific
+/// contexts (e.g., `b"lo-session-bind"` for application-level domain
+/// separation) are supported up to 255 bytes.
+///
+/// Hedged signing: 32 bytes of fresh OS entropy mixed into the nonce
+/// derivation, identical to [`sign`]'s hedged behavior.
+///
+/// # Errors
+/// - [`Error::InvalidData`] if `ctx.len() > 255`
+/// - [`Error::InvalidLength`] if the secret-key seed length is wrong
+pub fn sign_with_ctx(sk: &SecretKey, message: &[u8], ctx: &[u8]) -> Result<Signature> {
+    use ml_dsa::{B32, MlDsa65, Seed, SigningKey};
+
+    if ctx.len() > 255 {
+        return Err(Error::InvalidData);
+    }
+    if sk.0.len() != SK_LEN {
+        return Err(Error::InvalidLength {
+            expected: SK_LEN,
+            got: sk.0.len(),
+        });
+    }
+
+    let seed: &Seed = sk.0.as_slice().try_into().map_err(|_| Error::Internal)?;
+    let signing_key = SigningKey::<MlDsa65>::from_seed(seed);
+
+    // Hedged signing: 32 bytes of fresh getrandom entropy. Same
+    // rationale as `sign()` — fault-injection resistance.
+    let mut rnd_bytes = [0u8; 32];
+    super::random::random_bytes(&mut rnd_bytes);
+    let mut rnd: B32 = rnd_bytes.into();
+    rnd_bytes.zeroize();
+
+    // FIPS 204 §5.2 envelope: M' = 0x00 || len(ctx) || ctx || M.
+    // SHAKE's streaming absorb is associative, so passing M' as a
+    // multi-chunk slice (`&[domain_sep, len_byte, ctx, message]`)
+    // produces the same μ as concatenating into one buffer first.
+    // The `MuBuilder::new(tr, ctx).message(M)` path used by the
+    // ml-dsa crate's standard `verify_with_context` absorbs the
+    // same bytes in the same order — so signatures from this
+    // function verify under the standard verify path, AND the
+    // standard sign path verifies under our `verify_with_ctx`.
+    let domain_sep = [0x00u8];
+    let len_byte = [ctx.len() as u8];
+    let sig = signing_key.sign_internal(
+        &[&domain_sep, &len_byte, ctx, message],
+        &rnd,
+    );
+    rnd.zeroize();
+
+    let sig_bytes = sig.encode().to_vec();
+    assert_eq!(
+        sig_bytes.len(),
+        SIG_LEN,
+        "ML-DSA-65 sig size mismatch: got {}, expected {SIG_LEN}",
+        sig_bytes.len()
+    );
+
+    Ok(Signature(sig_bytes))
+}
+
+/// Verify with the FIPS 204 §5.2 ML-DSA.Verify envelope.
+///
+/// Counterpart of [`sign_with_ctx`]. Accepts signatures from any
+/// FIPS 204-compliant ML-DSA-65 implementation (when called with
+/// the same `ctx`).
+///
+/// `ctx` MUST match the context string used by the signer. For TLS
+/// 1.3 use that is `b""`.
+///
+/// Returns `Ok(())` on a valid signature, `Err(VerificationFailed)`
+/// for an invalid one or for `ctx.len() > 255`.
+pub fn verify_with_ctx(
+    pk: &PublicKey,
+    message: &[u8],
+    ctx: &[u8],
+    signature: &Signature,
+) -> Result<()> {
+    use ml_dsa::{EncodedSignature, EncodedVerifyingKey, MlDsa65, VerifyingKey};
+
+    if ctx.len() > 255 {
+        return Err(Error::VerificationFailed);
+    }
+    if pk.0.len() != PK_LEN {
+        return Err(Error::InvalidLength {
+            expected: PK_LEN,
+            got: pk.0.len(),
+        });
+    }
+    if signature.0.len() != SIG_LEN {
+        return Err(Error::InvalidLength {
+            expected: SIG_LEN,
+            got: signature.0.len(),
+        });
+    }
+
+    let vk_enc: &EncodedVerifyingKey<MlDsa65> =
+        pk.0.as_slice().try_into().map_err(|_| Error::Internal)?;
+    let vk = VerifyingKey::<MlDsa65>::decode(vk_enc);
+
+    let sig_enc: &EncodedSignature<MlDsa65> = signature
+        .0
+        .as_slice()
+        .try_into()
+        .map_err(|_| Error::Internal)?;
+    let sig = ml_dsa::Signature::<MlDsa65>::decode(sig_enc).ok_or(Error::VerificationFailed)?;
+
+    // `verify_with_context` applies the FIPS 204 §5.2 envelope
+    // (`0x00 || len(ctx) || ctx || M`) before verifying, matching
+    // the construction in `sign_with_ctx`.
+    if vk.verify_with_context(message, ctx, &sig) {
+        Ok(())
+    } else {
+        Err(Error::VerificationFailed)
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -335,6 +467,98 @@ mod tests {
         assert!(verify(&pk, b"", &sig).is_ok());
     }
 
+    /// `sign_with_ctx` round-trip with empty context (the form used
+    /// for TLS 1.3 cert verify per draft-ietf-tls-mldsa).
+    #[test]
+    fn sign_with_ctx_empty_round_trip() {
+        let (pk, sk) = keygen().unwrap();
+        let sig = sign_with_ctx(&sk, b"hello fips204", b"").unwrap();
+        assert!(verify_with_ctx(&pk, b"hello fips204", b"", &sig).is_ok());
+    }
+
+    /// Round-trip with a non-empty context. Confirms the FIPS 204
+    /// envelope `0x00 || len(ctx) || ctx || M` round-trips through
+    /// the sign/verify pair.
+    #[test]
+    fn sign_with_ctx_nonempty_round_trip() {
+        let (pk, sk) = keygen().unwrap();
+        let sig = sign_with_ctx(&sk, b"payload", b"app-domain-v1").unwrap();
+        assert!(verify_with_ctx(&pk, b"payload", b"app-domain-v1", &sig).is_ok());
+    }
+
+    /// Domain-separation: a signature produced with one context
+    /// MUST NOT verify under a different context. This is the
+    /// security property that makes per-protocol context strings
+    /// useful — a TLS-bound signature can't be replayed to an
+    /// application-layer verifier and vice versa.
+    #[test]
+    fn sign_with_ctx_different_ctx_fails() {
+        let (pk, sk) = keygen().unwrap();
+        let sig = sign_with_ctx(&sk, b"payload", b"ctx-a").unwrap();
+        assert!(matches!(
+            verify_with_ctx(&pk, b"payload", b"ctx-b", &sig),
+            Err(Error::VerificationFailed)
+        ));
+    }
+
+    /// `sign` (no ctx) and `sign_with_ctx` produce DIFFERENT
+    /// signatures, and the signatures don't cross-verify. This is
+    /// the deliberate distinction: `sign` skips the FIPS 204
+    /// envelope, `sign_with_ctx` applies it. If a regression ever
+    /// made them equivalent, soliton's intra-Lo signatures would
+    /// silently become FIPS 204-compatible (or vice versa) — both
+    /// outcomes need to be intentional, not accidental.
+    #[test]
+    fn sign_and_sign_with_ctx_are_distinct() {
+        let (pk, sk) = keygen().unwrap();
+        let sig_internal = sign(&sk, b"payload").unwrap();
+        let sig_standard = sign_with_ctx(&sk, b"payload", b"").unwrap();
+        // Bytes differ (the rnd hedging makes equality unreliable
+        // even for identical inputs, so this isn't a strict check).
+        // The cross-verify check is the load-bearing one:
+        assert!(matches!(
+            verify_with_ctx(&pk, b"payload", b"", &sig_internal),
+            Err(Error::VerificationFailed)
+        ), "internal-mode signature must NOT verify under FIPS 204 verify");
+        assert!(matches!(
+            verify(&pk, b"payload", &sig_standard),
+            Err(Error::VerificationFailed)
+        ), "FIPS 204 signature must NOT verify under internal-mode verify");
+    }
+
+    /// 255-byte context is the spec maximum. Confirm it's accepted.
+    #[test]
+    fn sign_with_ctx_max_length_ok() {
+        let (pk, sk) = keygen().unwrap();
+        let ctx = vec![0xAB; 255];
+        let sig = sign_with_ctx(&sk, b"payload", &ctx).unwrap();
+        assert!(verify_with_ctx(&pk, b"payload", &ctx, &sig).is_ok());
+    }
+
+    /// 256-byte context exceeds the FIPS 204 §5.2 limit and MUST
+    /// be rejected at the API boundary rather than producing an
+    /// invalid signature.
+    #[test]
+    fn sign_with_ctx_oversized_ctx_rejected() {
+        let (_, sk) = keygen().unwrap();
+        let ctx = vec![0u8; 256];
+        assert!(matches!(
+            sign_with_ctx(&sk, b"payload", &ctx),
+            Err(Error::InvalidData)
+        ));
+    }
+
+    #[test]
+    fn verify_with_ctx_oversized_ctx_rejected() {
+        let (pk, sk) = keygen().unwrap();
+        let valid_sig = sign_with_ctx(&sk, b"payload", b"").unwrap();
+        let too_long_ctx = vec![0u8; 256];
+        assert!(matches!(
+            verify_with_ctx(&pk, b"payload", &too_long_ctx, &valid_sig),
+            Err(Error::VerificationFailed)
+        ));
+    }
+
     #[test]
     fn verify_wrong_message() {
         let (pk, sk) = keygen().unwrap();

soliton/src/ratchet/mod.rs

@@ -562,15 +562,15 @@ impl RatchetState {
         // through key derivation + AEAD. Duplicates still succeed AEAD
         // (same key, nonce, ciphertext) but the plaintext is discarded.
         //
-        // Enforce MAX_RECV_SEEN cap at runtime, not just serialization time.
-        // Without this, an authenticated peer sending >65536 messages in one
-        // epoch would grow the set unboundedly and make the state unserializable.
+        // Enforce the serialization invariant (|recv_seen| < MAX_RECV_SEEN,
+        // §6.8) at runtime. The check is on the post-insert size so a successful
+        // decrypt never produces a live state that to_bytes would reject.
         match epoch_type {
             EpochType::PreviousEpoch => {
                 if self.prev_recv_seen.contains(&header.n) {
                     return Err(Error::DuplicateMessage);
                 }
-                if self.prev_recv_seen.len() >= constants::MAX_RECV_SEEN as usize {
+                if self.prev_recv_seen.len() + 1 >= constants::MAX_RECV_SEEN as usize {
                     return Err(Error::ChainExhausted);
                 }
                 self.prev_recv_seen.insert(header.n);
@@ -579,7 +579,7 @@ impl RatchetState {
                 if self.recv_seen.contains(&header.n) {
                     return Err(Error::DuplicateMessage);
                 }
-                if self.recv_seen.len() >= constants::MAX_RECV_SEEN as usize {
+                if self.recv_seen.len() + 1 >= constants::MAX_RECV_SEEN as usize {
                     return Err(Error::ChainExhausted);
                 }
                 self.recv_seen.insert(header.n);
@@ -862,9 +862,10 @@ impl RatchetState {
             // u64::MAX - 1 would write u64::MAX, which from_bytes rejects.
             // u64::MAX is caught by to_bytes' checked_add (returns ChainExhausted).
             && self.epoch < u64::MAX - 1
-            // to_bytes() rejects recv_seen/prev_recv_seen exceeding MAX_RECV_SEEN.
-            // decrypt_inner enforces this cap at runtime, so these checks are
-            // defense-in-depth against a future refactor removing the runtime cap.
+            // to_bytes() rejects recv_seen/prev_recv_seen at MAX_RECV_SEEN or
+            // more. decrypt_inner refuses to grow the set past
+            // MAX_RECV_SEEN - 1 entries, so these checks are defense-in-depth
+            // against a refactor that removes the runtime cap.
             && self.recv_seen.len() < constants::MAX_RECV_SEEN as usize
             && self.prev_recv_seen.len() < constants::MAX_RECV_SEEN as usize
     }
@@ -1054,8 +1055,8 @@ impl RatchetState {
         // recv_seen — sorted for deterministic output.
         let mut sorted_seen: Vec<u32> = self.recv_seen.iter().copied().collect();
         sorted_seen.sort_unstable();
-        // Consistent with decrypt_inner's runtime cap (`>= MAX_RECV_SEEN`):
-        // the set can hold at most MAX_RECV_SEEN - 1 entries (65535).
+        // Mirrors decrypt_inner's runtime cap: a live set holds at most
+        // MAX_RECV_SEEN - 1 entries (65535).
         if sorted_seen.len() >= constants::MAX_RECV_SEEN as usize {
             return Err(Error::InvalidData);
         }
@@ -1069,7 +1070,7 @@ impl RatchetState {
         // prev_recv_seen — sorted for deterministic output.
         let mut sorted_prev_seen: Vec<u32> = self.prev_recv_seen.iter().copied().collect();
         sorted_prev_seen.sort_unstable();
-        // Consistent with decrypt_inner's runtime cap (`>= MAX_RECV_SEEN`).
+        // Mirrors decrypt_inner's runtime cap.
         if sorted_prev_seen.len() >= constants::MAX_RECV_SEEN as usize {
             return Err(Error::InvalidData);
         }
@@ -1286,8 +1287,8 @@ impl RatchetState {
         // recv_seen set.
         let num_seen =
             u32::from_be_bytes(read(&mut pos, 4)?.try_into().map_err(|_| Error::Internal)?);
-        // Consistent with decrypt_inner's runtime cap (`>= MAX_RECV_SEEN`):
-        // the set can hold at most MAX_RECV_SEEN - 1 entries.
+        // Mirrors decrypt_inner's runtime cap: a live set holds at most
+        // MAX_RECV_SEEN - 1 entries.
         if num_seen >= constants::MAX_RECV_SEEN {
             return Err(Error::InvalidData);
         }
@@ -1311,7 +1312,7 @@ impl RatchetState {
         // prev_recv_seen set.
         let num_prev_seen =
             u32::from_be_bytes(read(&mut pos, 4)?.try_into().map_err(|_| Error::Internal)?);
-        // Consistent with decrypt_inner's runtime cap (`>= MAX_RECV_SEEN`).
+        // Mirrors decrypt_inner's runtime cap.
         if num_prev_seen >= constants::MAX_RECV_SEEN {
             return Err(Error::InvalidData);
         }
@@ -3316,11 +3317,12 @@ mod tests {
     #[test]
     fn recv_seen_cap_at_runtime() {
         let (mut alice, mut bob) = make_pair();
-        // Fill recv_seen to capacity with counters that won't collide
-        // with Alice's send_count (which starts at 1).
-        // Use range 100_000..100_000+MAX_RECV_SEEN to avoid collision.
-        bob.recv_seen = (100_000..100_000 + constants::MAX_RECV_SEEN).collect();
-        bob.recv_count = 100_000 + constants::MAX_RECV_SEEN;
+        // Fill recv_seen to the runtime cap (MAX_RECV_SEEN - 1 entries) with
+        // counters that won't collide with Alice's send_count (which starts at
+        // 1). The next decrypt would push the set to MAX_RECV_SEEN, violating
+        // the serialization invariant, so it must be rejected.
+        bob.recv_seen = (100_000..100_000 + constants::MAX_RECV_SEEN - 1).collect();
+        bob.recv_count = 100_000 + constants::MAX_RECV_SEEN - 1;
         // Next decrypt should return ChainExhausted (not DuplicateMessage).
         let enc = alice.encrypt(b"over-cap").unwrap();
         assert!(
@@ -3349,9 +3351,10 @@ mod tests {
         send_a_to_b(&mut alice, &mut bob, b"dir2");
         // enc_old is from Bob's previous recv epoch.
         assert!(bob.prev_recv_epoch_key.is_some());
-        // Fill prev_recv_seen with counters that won't collide with
-        // enc_old's counter (which is 2 — setup=1, will-be-prev=2).
-        bob.prev_recv_seen = (100_000..100_000 + constants::MAX_RECV_SEEN).collect();
+        // Fill prev_recv_seen to the runtime cap (MAX_RECV_SEEN - 1 entries)
+        // with counters that won't collide with enc_old's counter (which is 2 —
+        // setup=1, will-be-prev=2).
+        bob.prev_recv_seen = (100_000..100_000 + constants::MAX_RECV_SEEN - 1).collect();
         // Attempt to decrypt the old-epoch message.
         assert!(
             matches!(
@@ -3435,8 +3438,8 @@ mod tests {
     #[test]
     fn encrypt_works_after_recv_seen_cap() {
         let (mut alice, _) = make_pair();
-        alice.recv_seen = (0..constants::MAX_RECV_SEEN).collect();
-        alice.recv_count = constants::MAX_RECV_SEEN;
+        alice.recv_seen = (0..constants::MAX_RECV_SEEN - 1).collect();
+        alice.recv_count = constants::MAX_RECV_SEEN - 1;
         // Encrypt must still work — recv_seen cap only affects decrypt.
         assert!(alice.encrypt(b"still-works").is_ok());
     }

soliton_capi/fuzz/Cargo.lock

@@ -435,7 +435,7 @@ dependencies = [
 
 [[package]]
 name = "libsoliton"
-version = "0.1.3"
+version = "0.1.4"
 dependencies = [
  "argon2",
  "chacha20poly1305",
@@ -473,7 +473,7 @@ dependencies = [
 
 [[package]]
 name = "libsoliton_capi"
-version = "0.1.3"
+version = "0.1.4"
 dependencies = [
  "libsoliton",
  "zeroize",

soliton_py/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "maturin"
 
 [project]
 name = "soliton-py"
-version = "0.1.3"
+version = "0.1.4"
 description = "Python bindings for libsoliton — post-quantum cryptographic library"
 license = { text = "AGPL-3.0-only" }
 requires-python = ">=3.10"

soliton_wasm/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "soliton-wasm"
-version = "0.1.3"
+version = "0.1.4"
 edition.workspace = true
 license.workspace = true
 repository.workspace = true

soliton_zig/README.md

@@ -24,7 +24,7 @@ Add as a Zig dependency in `build.zig.zon`:
 ```zig
 .dependencies = .{
     .soliton = .{
-        .url = "https://git.lo.sh/lo/libsoliton/archive/v0.1.3.tar.gz",
+        .url = "https://git.lo.sh/lo/libsoliton/archive/v0.1.4.tar.gz",
         .hash = "...",
     },
 },

soliton_zig/build.zig.zon

@@ -1,6 +1,6 @@
 .{
     .name = .soliton_zig,
-    .version = "0.1.3",
+    .version = "0.1.4",
     .fingerprint = 0x333e453f9c21f54c,
     .minimum_zig_version = "0.14.0",
     .paths = .{