code refs, additional specs

spec/modules/README.md

@@ -52,6 +52,21 @@ Things that would surprise a competent Haskell developer reading the code for th
 - Alternatives considered and rejected
 - Known limitations and their justification
 
+## Non-obvious threshold
+
+The guiding principle: **non-obvious state machines and flows require documentation; standard things don't.**
+
+Document:
+- Multi-step protocols and negotiation flows (e.g., KEM propose/accept round-trips)
+- Monotonic or irreversible state transitions (e.g., PQ support can only be enabled, never disabled)
+- Silent error behaviors (e.g., `verify` returns `False` on algorithm mismatch instead of an error)
+- Design rationale for non-standard choices (e.g., why byte-reverse a nonce, why hash-then-encrypt for authenticators)
+
+Do NOT document:
+- Standard algorithm properties (e.g., Ed25519 public key derivable from private key)
+- Well-known protocol mechanics (e.g., HKDF usage per RFC 5869, deterministic nonce derivation in double ratchet)
+- Implementation details that follow directly from the type signatures
+
 ## What NOT to include
 
 - **Type signatures** — the code has them
@@ -107,6 +122,14 @@ This is valuable — it confirms someone looked and found nothing to document.
 
 ## Linking conventions
 
+### Module doc → protocol docs
+When a module implements or is governed by a protocol specification in `protocol/`, link to it near the top of the module doc (after the overview). Do not duplicate protocol content — just reference it:
+```markdown
+**Protocol spec**: [`protocol/pqdr.md`](../../../../protocol/pqdr.md) — Post-quantum resistant augmented double ratchet algorithm.
+```
+
+This is especially important for modules in transport, protocol, client, server, and agent layers where behavior is defined by the protocol spec rather than being self-evident from the code.
+
 ### Module doc → other module docs
 Use fully qualified names as link text:
 ```markdown

spec/modules/Simplex/Messaging/Crypto.md

@@ -55,10 +55,6 @@ Both apply `pad`/`unPad` by default. The `NoPad` variants skip padding.
 
 The XSalsa20 implementation splits the 24-byte nonce into two 8-byte halves. The first half initializes the cipher state (prepended with 16 zero bytes), the second derives a subkey. The first 32 bytes of output become the Poly1305 one-time key (`rs`), then the rest encrypts the message. This is the standard NaCl construction.
 
-## CbAuthenticator
-
-An authentication scheme that encrypts the SHA-512 hash of the message using crypto_box, rather than the message itself. The result is 80 bytes (64 hash + 16 auth tag). Used for authenticating messages where the content is transmitted separately from the authentication proof.
-
 ## Secret box chains (sbcInit / sbcHkdf)
 
 HKDF-based key chains for deriving sequential key+nonce pairs:
@@ -77,6 +73,22 @@ All keys are encoded as ASN.1 DER (X.509 SubjectPublicKeyInfo for public, PKCS#8
 
 `GCMIV` constructor is not exported — only `gcmIV :: ByteString -> Either CryptoError GCMIV` is available, which validates that the input is exactly 12 bytes. This prevents construction of invalid IVs.
 
+## verify silently returns False on algorithm mismatch
+
+`verify :: APublicVerifyKey -> ASignature -> ByteString -> Bool` uses `testEquality` on the algorithm singletons. If the key is Ed25519 but the signature is Ed448 (or vice versa), `testEquality` fails and `verify` returns `False` — no error, no indication of a type mismatch. A correctly-formed signature can "fail" simply because the wrong algorithm key was passed.
+
+## dh' returns raw DH output — no key derivation
+
+`dh'` returns the raw X25519/X448 shared point with no hashing or HKDF. Callers must apply their own KDF: [SNTRUP761](./Crypto/SNTRUP761.md) hashes with SHA3-256, the [ratchet](./Crypto/Ratchet.md#kdf-functions) uses HKDF-SHA512. Not all DH libraries behave this way — some hash the output automatically.
+
+## reverseNonce
+
+`reverseNonce` creates a "reply" nonce by byte-reversing the original 24-byte nonce. Used for bidirectional communication where both sides need distinct nonces derived from the same starting value. The two nonces are guaranteed distinct unless the original is a byte palindrome, which is astronomically unlikely for random 24-byte values.
+
+## CbAuthenticator
+
+An authentication scheme that encrypts the SHA-512 hash of the message using crypto_box, rather than the message itself. The result is 80 bytes (64 hash + 16 auth tag). This is the djb-recommended authenticator scheme: it proves knowledge of the shared secret and the message content, without requiring the message to fit in a single crypto_box, and without revealing message content even to someone who compromises the shared key after verification.
+
 ## generateKeyPair is STM
 
 Key generation uses `TVar ChaChaDRG` and runs in `STM`, not `IO`. This allows key generation inside `atomically` blocks, which is used extensively in handshake and ratchet initialization code.

spec/modules/Simplex/Messaging/Crypto/Ratchet.md

@@ -12,6 +12,8 @@ Implements the Signal double ratchet protocol extended with:
 
 The ratchet uses X448 (not X25519) for DH operations — `type RatchetX448 = Ratchet 'X448`.
 
+**Protocol spec**: [`protocol/pqdr.md`](../../../../protocol/pqdr.md) — Post-quantum resistant augmented double ratchet algorithm.
+
 ## PQ X3DH key agreement
 
 `pqX3dhSnd` / `pqX3dhRcv` perform the extended X3DH:
@@ -46,9 +48,13 @@ Each message header carries `msgMaxVersion` (the sender's max supported ratchet
 
 `largeP` detects the length-prefix format by peeking at the first byte: if < 32, it's a 2-byte `Large` prefix (new format); otherwise it's a 1-byte prefix (old format). This allows upgrading the header encoding format in a single message without a version bump.
 
+## maxSkip = 512 — DoS protection
+
+`maxSkip` is a hardcoded constant (not configurable). Messages claiming to be more than 512 positions ahead of the current counter are rejected with `CERatchetTooManySkipped`. This prevents an attacker from forcing the receiver to compute and store an unbounded number of skipped message keys.
+
 ## Skipped message keys
 
-When messages arrive out of order, the ratchet computes and stores the message keys for skipped messages (up to `maxSkip = 512`). Skipped keys are stored in a `Map HeaderKey (Map Word32 MessageKey)` — keyed first by header key, then by message number.
+When messages arrive out of order, the ratchet computes and stores the message keys for skipped messages (up to `maxSkip`). Skipped keys are stored in a `Map HeaderKey (Map Word32 MessageKey)` — keyed first by header key, then by message number.
 
 The `SkippedMsgDiff` type represents changes to the skipped key store as a diff rather than a full replacement — this is persisted to the database, and the full state is loaded for the next message. `applySMDiff` is only used in tests.
 
@@ -61,6 +67,14 @@ Decryption tries three strategies in order:
 
 If strategy 1 decrypts the header but the message number isn't in skipped keys, it checks whether this header key corresponds to the current or next ratchet to decide whether to advance.
 
+### decryptSkipped — linear scan through all stored header keys
+
+`decryptSkipped` iterates through ALL `(HeaderKey, SkippedHdrMsgKeys)` pairs, attempting header decryption with each key. When header decryption succeeds but the message number is NOT in the skipped keys for that header, the result is `SMHeader` — which includes whether the key matches the current ratchet (`rcHKr` → `SameRatchet`) or the next ratchet (`rcNHKr` → `AdvanceRatchet`). This falls through to normal decryption processing rather than producing an error.
+
+### decryptMessage — ratchet advances even on failure
+
+`decryptMessage` returns `Either CryptoError ByteString` inside the `ExceptT` monad — a message decryption failure does NOT abort the ratchet state update. The ratchet counter advances (`rcNr + 1`) and chain key updates (`rcCKr'`) regardless of whether the message body decrypts successfully. This preserves ratchet state consistency for retransmission and error recovery.
+
 ## rcEncryptHeader — separated from rcEncryptMsg
 
 Encryption is split into two steps: `rcEncryptHeader` produces a `MsgEncryptKey` (containing the encrypted header and message key), then `rcEncryptMsg` uses that key to encrypt the message body. This separation allows the ratchet state to be updated (persisted) before the message is encrypted, which is important for crash recovery — if the process crashes after encrypting but before sending, the ratchet state must already reflect the advanced counter.
@@ -80,6 +94,19 @@ Two distinct newtypes with identical structure (`Bool` wrapper):
 - `PQSupport`: whether PQ **can** be used (determines header padding size, cannot be disabled once enabled)
 - `PQEncryption`: whether PQ **is** being used for the current send/receive ratchet
 
+### pqEnableSupport is monotonic
+
+`pqEnableSupport v sup enc = PQSupport $ sup || (v >= pqRatchetE2EEncryptVersion && enc)`. The `||` means once PQ support is `True`, it stays `True` regardless of subsequent messages. PQ encryption (usage) can be toggled per-message; PQ support (capability / header size) only ratchets up. This prevents the larger header format from being downgraded once negotiated.
+
+## replyKEM_ — two-step KEM negotiation
+
+KEM establishment requires two message round-trips, as described in the [PQDR KEM state machine](../../../../protocol/pqdr.md#kem-state-machine):
+
+1. **Propose**: if the sender has no KEM in their header but the replier supports PQ at sufficient version, the replier includes a KEM proposal (`RKParamsProposed` — their encapsulation public key)
+2. **Accept**: if the sender proposed KEM, the replier accepts by encapsulating against the proposed key and including the ciphertext + their own new encapsulation key (`RKParamsAccepted`)
+
+After acceptance, both sides have a shared KEM secret that is folded into the root KDF. Subsequent ratchet steps continue the KEM exchange with fresh keypairs on each side.
+
 ## Error semantics
 
 - `CERatchetEarlierMessage n`: message number is `n` positions before the next expected (already processed or skipped-and-consumed)

src/Simplex/Messaging/Crypto.hs

@@ -1285,11 +1285,13 @@ verify' (PublicKeyEd25519 k) (SignatureEd25519 sig) msg = Ed25519.verify k msg s
 verify' (PublicKeyEd448 k) (SignatureEd448 sig) msg = Ed448.verify k msg sig
 {-# INLINE verify' #-}
 
+-- spec: spec/modules/Simplex/Messaging/Crypto.md#verify-silently-returns-false-on-algorithm-mismatch
 verify :: APublicVerifyKey -> ASignature -> ByteString -> Bool
 verify (APublicVerifyKey a k) (ASignature a' sig) msg = case testEquality a a' of
   Just Refl -> verify' k sig msg
   _ -> False
 
+-- spec: spec/modules/Simplex/Messaging/Crypto.md#dh-returns-raw-dh-output--no-key-derivation
 dh' :: DhAlgorithm a => PublicKey a -> PrivateKey a -> DhSecret a
 dh' (PublicKeyX25519 k) (PrivateKeyX25519 pk) = DhSecretX25519 $ X25519.dh k pk
 dh' (PublicKeyX448 k) (PrivateKeyX448 pk) = DhSecretX448 $ X448.dh k pk
@@ -1418,6 +1420,7 @@ randomCbNonce = fmap CryptoBoxNonce . randomBytes 24
 randomBytes :: Int -> TVar ChaChaDRG -> STM ByteString
 randomBytes n gVar = stateTVar gVar $ randomBytesGenerate n
 
+-- spec: spec/modules/Simplex/Messaging/Crypto.md#reversenonce
 reverseNonce :: CbNonce -> CbNonce
 reverseNonce (CryptoBoxNonce s) = CryptoBoxNonce (B.reverse s)
 

src/Simplex/Messaging/Crypto/Ratchet.hs

@@ -840,9 +840,11 @@ pqEncToSupport (PQEncryption pq) = PQSupport pq
 pqSupportAnd :: PQSupport -> PQSupport -> PQSupport
 pqSupportAnd (PQSupport s1) (PQSupport s2) = PQSupport $ s1 && s2
 
+-- spec: spec/modules/Simplex/Messaging/Crypto/Ratchet.md#pqenablesupport-is-monotonic
 pqEnableSupport :: VersionE2E -> PQSupport -> PQEncryption -> PQSupport
 pqEnableSupport v (PQSupport sup) (PQEncryption enc) = PQSupport $ sup || (v >= pqRatchetE2EEncryptVersion && enc)
 
+-- spec: spec/modules/Simplex/Messaging/Crypto/Ratchet.md#replykem_--two-step-kem-negotiation
 replyKEM_ :: VersionE2E -> Maybe (RKEMParams 'RKSProposed) -> PQSupport -> Maybe AUseKEM
 replyKEM_ v kem_ = \case
   PQSupportOn | v >= pqRatchetE2EEncryptVersion -> Just $ case kem_ of
@@ -994,6 +996,7 @@ data RatchetStep = AdvanceRatchet | SameRatchet
 
 type DecryptResult a = (Either CryptoError ByteString, Ratchet a, SkippedMsgDiff)
 
+-- spec: spec/modules/Simplex/Messaging/Crypto/Ratchet.md#maxskip--512--dos-protection
 maxSkip :: Word32
 maxSkip = 512
 
@@ -1131,6 +1134,7 @@ rcDecrypt g rc@Ratchet {rcRcv, rcAD = Str rcAD, rcVersion} rcMKSkipped msg' = do
       let (ck', mk, iv, _) = chainKdf ck
           mks' = M.insert msgNs (MessageKey mk iv) mks
        in advanceRcvRatchet (n - 1) ck' (msgNs + 1) mks'
+    -- spec: spec/modules/Simplex/Messaging/Crypto/Ratchet.md#decryptskipped--linear-scan-through-all-stored-header-keys
     decryptSkipped :: EncMessageHeader -> EncRatchetMessage -> ExceptT CryptoError IO (SkippedMessage a)
     decryptSkipped encHdr encMsg = tryDecryptSkipped SMNone $ M.assocs rcMKSkipped
       where
@@ -1163,6 +1167,7 @@ rcDecrypt g rc@Ratchet {rcRcv, rcAD = Str rcAD, rcVersion} rcMKSkipped msg' = do
     decryptHeader k EncMessageHeader {ehVersion, ehBody, ehAuthTag, ehIV} = do
       header <- decryptAEAD k ehIV rcAD ehBody ehAuthTag `catchE` \_ -> throwE CERatchetHeader
       parseE' CryptoHeaderError (msgHeaderP ehVersion) header
+    -- spec: spec/modules/Simplex/Messaging/Crypto/Ratchet.md#decryptmessage--ratchet-advances-even-on-failure
     decryptMessage :: MessageKey -> EncRatchetMessage -> ExceptT CryptoError IO (Either CryptoError ByteString)
     decryptMessage (MessageKey mk iv) EncRatchetMessage {emHeader, emBody, emAuthTag} =
       -- DECRYPT(mk, cipher-text, CONCAT(AD, enc_header))