From ea2a62ab7e740515ac71546526eb0b246b15ef3f Mon Sep 17 00:00:00 2001 From: "Evgeny @ SimpleX Chat" <259188159+evgeny-simplex@users.noreply.github.com> Date: Wed, 11 Mar 2026 07:32:57 +0000 Subject: [PATCH] more specs --- spec/compression.md | 81 ++++++++++- spec/encoding.md | 341 +++++++++++++++++++++++++++++++++++++++++++- spec/version.md | 194 ++++++++++++++++++++++++- 3 files changed, 609 insertions(+), 7 deletions(-) diff --git a/spec/compression.md b/spec/compression.md index 7e457438b..faa8c275f 100644 --- a/spec/compression.md +++ b/spec/compression.md @@ -1,7 +1,84 @@ # Compression -> Compression support for SimpleX protocols. +> Zstd compression for SimpleX protocol messages. -## Zstd +**Source file**: [`Compression.hs`](../src/Simplex/Messaging/Compression.hs) + +## Overview + +Optional Zstd compression for SMP message bodies. Short messages bypass compression entirely to avoid overhead. The `Compressed` type carries a tag byte indicating whether the payload is compressed or passthrough, making it self-describing on the wire. + +## Types + +### `Compressed` + +**Source**: `Compression.hs:17-22` + +```haskell +data Compressed + = Passthrough ByteString -- short messages, left intact + | Compressed Large -- Zstd-compressed, 2-byte length prefix +``` + +Wire encoding (`Compression.hs:30-38`): + +``` +Passthrough → '0' ++ smpEncode ByteString (1-byte tag + 1-byte length + data) +Compressed → '1' ++ smpEncode Large (1-byte tag + 2-byte length + data) +``` + +Tags are `'0'` (0x30) and `'1'` (0x31) — same ASCII convention as `Maybe` encoding. + +`Passthrough` uses standard `ByteString` encoding (max 255 bytes, 1-byte length prefix). `Compressed` uses `Large` encoding (max 65535 bytes, 2-byte Word16 length prefix), since compressed output can exceed 255 bytes for larger inputs. + +## Constants + +| Constant | Value | Purpose | Source | +|----------|-------|---------|--------| +| `maxLengthPassthrough` | 180 | Messages at or below this length are not compressed | `Compression.hs:24-25` | +| `compressionLevel` | 3 | Zstd compression level | `Compression.hs:27-28` | + +The 180-byte threshold was "sampled from real client data" — messages above this length show rapidly increasing compression ratio. Below 180 bytes, compression overhead (FFI call, dictionary-less Zstd startup) outweighs savings. ## Functions + +### `compress1` + +**Source**: `Compression.hs:40-43` + +```haskell +compress1 :: ByteString -> Compressed +``` + +Compress a message body: +- If `B.length bs <= 180` → `Passthrough bs` +- Otherwise → `Compressed (Large (Z1.compress 3 bs))` + +No context or dictionary — each message is independently compressed ("1" in `compress1` refers to single-shot compression). + +### `decompress1` + +**Source**: `Compression.hs:45-53` + +```haskell +decompress1 :: Int -> Compressed -> Either String ByteString +``` + +Decompress with size limit: +- `Passthrough bs` → `Right bs` (no check needed — already bounded by encoding) +- `Compressed (Large bs)` → check `Z1.decompressedSize bs`: + - If size is known and within `limit` → decompress + - If size unknown or exceeds `limit` → `Left` error + +The size limit check happens **before** decompression, using Zstd's frame header (which includes the decompressed size when the compressor wrote it). This prevents decompression bombs — an attacker cannot cause unbounded memory allocation by sending a small compressed payload that expands to gigabytes. + +The `Z1.decompress` result is pattern-matched for three cases: +- `Z1.Error e` → `Left e` +- `Z1.Skip` → `Right mempty` (zero-length output) +- `Z1.Decompress bs'` → `Right bs'` + +## Security notes + +- **Decompression bomb protection**: `decompress1` requires an explicit size limit and checks `decompressedSize` before allocating. Callers must pass an appropriate limit (typically the SMP block size). +- **No dictionary/context**: Each message is independently compressed. No shared state between messages that could leak information across compression boundaries. +- **Passthrough for short messages**: Messages ≤ 180 bytes are never compressed, avoiding timing side channels from compression ratio differences on short, potentially-predictable messages. diff --git a/spec/encoding.md b/spec/encoding.md index 2b8dded01..3a4fdcd27 100644 --- a/spec/encoding.md +++ b/spec/encoding.md @@ -2,10 +2,345 @@ > Binary and string encoding used across all SimpleX protocols. -## Binary Encoding +**Source files**: [`Encoding.hs`](../src/Simplex/Messaging/Encoding.hs), [`Encoding/String.hs`](../src/Simplex/Messaging/Encoding/String.hs), [`Parsers.hs`](../src/Simplex/Messaging/Parsers.hs) -## String Encoding +## Overview + +Two encoding layers serve different purposes: + +- **`Encoding`** — Binary wire format for SMP protocol transmissions. Compact, no delimiters between fields. Used in all on-the-wire protocol messages. +- **`StrEncoding`** — Human-readable string format for configuration, URIs, logs, and JSON serialization. Uses base64url for binary data, decimal for numbers, comma-separated lists, space-separated tuples. + +Both are typeclasses with `MINIMAL` pragmas requiring `encode` + (`decode` | `parser`), with the missing one derived from the other. + +## Binary Encoding (`Encoding` class) + +**Source**: `Encoding.hs:38-52` + +```haskell +class Encoding a where + smpEncode :: a -> ByteString + smpDecode :: ByteString -> Either String a -- default: parseAll smpP + smpP :: Parser a -- default: smpDecode <$?> smpP +``` + +### Length-prefix conventions + +| Type | Prefix | Max size | Source | +|------|--------|----------|--------| +| `ByteString` | 1-byte length (Word8 as Char) | 255 bytes | `Encoding.hs:102-106` | +| `Large` (newtype) | 2-byte length (Word16 big-endian) | 65535 bytes | `Encoding.hs:135-143` | +| `Tail` (newtype) | None — consumes rest of input | Unlimited | `Encoding.hs:126-132` | +| Lists (`smpEncodeList`) | 1-byte count prefix, then concatenated items | 255 items | `Encoding.hs:155-159` | +| `NonEmpty` | Same as list (fails on count=0) | 255 items | `Encoding.hs:173-178` | + +### Scalar types + +| Type | Encoding | Bytes | Source | +|------|----------|-------|--------| +| `Char` | Raw byte | 1 | `Encoding.hs:54-58` | +| `Bool` | `'T'` / `'F'` (0x54 / 0x46) | 1 | `Encoding.hs:60-70` | +| `Word16` | Big-endian | 2 | `Encoding.hs:72-76` | +| `Word32` | Big-endian | 4 | `Encoding.hs:78-82` | +| `Int64` | Two big-endian Word32s (high then low) | 8 | `Encoding.hs:84-99` | +| `SystemTime` | `systemSeconds` as Int64 (nanoseconds dropped) | 8 | `Encoding.hs:145-149` | +| `Text` | UTF-8 then ByteString encoding (1-byte length prefix) | 1 + len | `Encoding.hs:161-165` | +| `String` | `B.pack` then ByteString encoding | 1 + len | `Encoding.hs:167-171` | + +### `Maybe a` + +**Source**: `Encoding.hs:116-124` + +``` +Nothing → '0' (0x30) +Just x → '1' (0x31) ++ smpEncode x +``` + +Tags are ASCII characters `'0'`/`'1'`, not binary 0x00/0x01. + +### Tuples + +**Source**: `Encoding.hs:180-220` + +Tuples (2 through 8) encode as simple concatenation — no length prefix, no separator. Fields are parsed sequentially using each component's `smpP`. This works because each component's parser knows how many bytes to consume (via its own length prefix or fixed size). + +### Combinators + +| Function | Signature | Purpose | Source | +|----------|-----------|---------|--------| +| `_smpP` | `Parser a` | Space-prefixed parser (`A.space *> smpP`) | `Encoding.hs:151-152` | +| `smpEncodeList` | `[a] -> ByteString` | 1-byte count + concatenated items | `Encoding.hs:155-156` | +| `smpListP` | `Parser [a]` | Parse count then that many items | `Encoding.hs:158-159` | +| `lenEncode` | `Int -> Char` | Int to single-byte length char | `Encoding.hs:108-110` | + +## String Encoding (`StrEncoding` class) + +**Source**: `Encoding/String.hs:56-67` + +```haskell +class StrEncoding a where + strEncode :: a -> ByteString + strDecode :: ByteString -> Either String a -- default: parseAll strP + strP :: Parser a -- default: strDecode <$?> base64urlP +``` + +Key difference from `Encoding`: the default `strP` parses base64url input first, then applies `strDecode`. This means types that only implement `strDecode` will automatically accept base64url-encoded input. + +### Instance conventions + +| Type | Encoding | Source | +|------|----------|--------| +| `ByteString` | base64url (non-empty required) | `String.hs:70-76` | +| `Word16`, `Word32` | Decimal string | `String.hs:114-124` | +| `Int`, `Int64` | Signed decimal | `String.hs:138-148` | +| `Char`, `Bool` | Delegates to `Encoding` (`smpEncode`/`smpP`) | `String.hs:126-136` | +| `Maybe a` | Empty string = `Nothing`, otherwise `strEncode a` | `String.hs:108-112` | +| `Text` | UTF-8 bytes, parsed until space/newline | `String.hs:97-99` | +| `SystemTime` | `systemSeconds` as Int64 (decimal) | `String.hs:150-152` | +| `UTCTime` | ISO 8601 string | `String.hs:154-156` | +| `CertificateChain` | Comma-separated base64url blobs | `String.hs:158-162` | +| `Fingerprint` | base64url of fingerprint bytes | `String.hs:164-168` | + +### Collection encoding + +| Type | Separator | Source | +|------|-----------|--------| +| Lists (`strEncodeList`) | Comma `,` | `String.hs:171-175` | +| `NonEmpty` | Comma (fails on empty) | `String.hs:178-180` | +| `Set a` | Comma | `String.hs:182-184` | +| `IntSet` | Comma | `String.hs:186-188` | +| Tuples (2-6) | Space (` `) | `String.hs:193-221` | + +### `Str` newtype + +**Source**: `String.hs:84-89` + +Raw string (not base64url-encoded). Parses until space, consumes trailing space. Used for string-valued protocol fields that should not be base64-encoded. + +### `TextEncoding` class + +**Source**: `String.hs:51-53` + +```haskell +class TextEncoding a where + textEncode :: a -> Text + textDecode :: Text -> Maybe a +``` + +Separate from `StrEncoding` — operates on `Text` rather than `ByteString`. Used for types that need Text representation (e.g., enum display names). + +### JSON bridge functions + +| Function | Purpose | Source | +|----------|---------|--------| +| `strToJSON` | `StrEncoding a => a -> J.Value` via `decodeLatin1 . strEncode` | `String.hs:229-231` | +| `strToJEncoding` | Same, for Aeson encoding | `String.hs:233-235` | +| `strParseJSON` | `StrEncoding a => String -> J.Value -> JT.Parser a` — parse JSON string via `strP` | `String.hs:237-238` | +| `textToJSON` | `TextEncoding a => a -> J.Value` | `String.hs:240-242` | +| `textToEncoding` | Same, for Aeson encoding | `String.hs:244-246` | +| `textParseJSON` | `TextEncoding a => String -> J.Value -> JT.Parser a` | `String.hs:248-249` | ## Parsers -## Functions +**Source**: [`Parsers.hs`](../src/Simplex/Messaging/Parsers.hs) + +### Core parsing functions + +| Function | Signature | Purpose | Source | +|----------|-----------|---------|--------| +| `parseAll` | `Parser a -> ByteString -> Either String a` | Parse consuming all input (fails if bytes remain) | `Parsers.hs:64-65` | +| `parse` | `Parser a -> e -> ByteString -> Either e a` | `parseAll` with custom error type (discards error string) | `Parsers.hs:61-62` | +| `parseE` | `(String -> e) -> Parser a -> ByteString -> ExceptT e IO a` | `parseAll` lifted into `ExceptT` | `Parsers.hs:67-68` | +| `parseE'` | `(String -> e) -> Parser a -> ByteString -> ExceptT e IO a` | Like `parseE` but allows trailing input | `Parsers.hs:70-71` | +| `parseRead1` | `Read a => Parser a` | Parse a word then `readMaybe` it | `Parsers.hs:76-77` | +| `parseString` | `(ByteString -> Either String a) -> String -> a` | Parse from `String` (errors with `error`) | `Parsers.hs:89-90` | + +### `base64P` + +**Source**: `Parsers.hs:44-53` + +Standard base64 parser (not base64url — uses `+`/`/` alphabet). Takes alphanumeric + `+`/`/` characters, optional `=` padding, then decodes. Contrast with `base64urlP` in `Encoding/String.hs` which uses `-`/`_` alphabet. + +### JSON options helpers + +Platform-conditional JSON encoding for cross-platform compatibility (Haskell ↔ Swift). + +| Function | Purpose | Source | +|----------|---------|--------| +| `enumJSON` | All-nullary constructors as strings, with tag modifier | `Parsers.hs:101-106` | +| `sumTypeJSON` | Platform-conditional: `taggedObjectJSON` on non-Darwin, `singleFieldJSON` on Darwin | `Parsers.hs:109-114` | +| `taggedObjectJSON` | `{"type": "Tag", "data": {...}}` format | `Parsers.hs:119-128` | +| `singleFieldJSON` | `{"Tag": value}` format | `Parsers.hs:137-149` | +| `defaultJSON` | Default options with `omitNothingFields = True` | `Parsers.hs:151-152` | + +Pattern synonyms for JSON field names: +- `TaggedObjectJSONTag = "type"` (`Parsers.hs:131`) +- `TaggedObjectJSONData = "data"` (`Parsers.hs:134`) +- `SingleFieldJSONTag = "_owsf"` (`Parsers.hs:117`) + +### String helpers + +| Function | Purpose | Source | +|----------|---------|--------| +| `fstToLower` | Lowercase first character | `Parsers.hs:92-94` | +| `dropPrefix` | Remove prefix string, lowercase remainder | `Parsers.hs:96-99` | +| `textP` | Parse rest of input as UTF-8 `String` | `Parsers.hs:154-155` | + +## Auxiliary Types and Utilities + +### TMap + +**Source**: [`TMap.hs`](../src/Simplex/Messaging/TMap.hs) + +```haskell +type TMap k a = TVar (Map k a) +``` + +STM-based concurrent map. Wraps `Data.Map.Strict` in a `TVar`. All mutations use `modifyTVar'` (strict) to prevent thunk accumulation. + +| Function | Notes | Source | +|----------|-------|--------| +| `emptyIO` | IO allocation (`newTVarIO`) | `TMap.hs:32-34` | +| `singleton` | STM allocation | `TMap.hs:36-38` | +| `clear` | Reset to empty | `TMap.hs:40-42` | +| `lookup` / `lookupIO` | STM / non-transactional IO read | `TMap.hs:48-54` | +| `member` / `memberIO` | STM / non-transactional IO membership | `TMap.hs:56-62` | +| `insert` / `insertM` | Insert value / insert from STM action | `TMap.hs:64-70` | +| `delete` | Remove key | `TMap.hs:72-74` | +| `lookupInsert` | Atomic lookup-then-insert (returns old value) | `TMap.hs:76-78` | +| `lookupDelete` | Atomic lookup-then-delete | `TMap.hs:80-82` | +| `adjust` / `update` / `alter` / `alterF` | Standard Map operations lifted to STM | `TMap.hs:84-100` | +| `union` | Merge `Map` into `TMap` | `TMap.hs:102-104` | + +`lookupIO`/`memberIO` use `readTVarIO` — single-read outside STM transaction, useful when you need a snapshot without composing with other STM operations. + +### SessionVar + +**Source**: [`Session.hs`](../src/Simplex/Messaging/Session.hs) + +Race-safe session management using TMVar + monotonic ID. + +```haskell +data SessionVar a = SessionVar + { sessionVar :: TMVar a -- result slot + , sessionVarId :: Int -- monotonic ID from TVar counter + , sessionVarTs :: UTCTime -- creation timestamp + } +``` + +| Function | Purpose | Source | +|----------|---------|--------| +| `getSessVar` | Lookup or create session. Returns `Left new` or `Right existing` | `Session.hs:24-33` | +| `removeSessVar` | Delete session only if ID matches (prevents removing a replacement) | `Session.hs:35-39` | +| `tryReadSessVar` | Non-blocking read of session result | `Session.hs:41-42` | + +The ID-match check in `removeSessVar` (`sessionVarId v == sessionVarId v'`) prevents a race where: +1. Thread A creates session #5, starts work +2. Thread B creates session #6 (replacing #5 in TMap) +3. Thread A finishes, tries to remove — ID mismatch, removal blocked + +### ServiceScheme + +**Source**: [`ServiceScheme.hs`](../src/Simplex/Messaging/ServiceScheme.hs) + +```haskell +data ServiceScheme = SSSimplex | SSAppServer SrvLoc +data SrvLoc = SrvLoc HostName ServiceName +``` + +URI scheme for SimpleX service addresses. `SSSimplex` encodes as `"simplex:"`, `SSAppServer` as `"https://host:port"`. + +`simplexChat :: ServiceScheme` is the constant `SSAppServer (SrvLoc "simplex.chat" "")` (`ServiceScheme.hs:38-39`). + +### SystemTime + +**Source**: [`SystemTime.hs`](../src/Simplex/Messaging/SystemTime.hs) + +```haskell +newtype RoundedSystemTime (t :: Nat) = RoundedSystemTime { roundedSeconds :: Int64 } +type SystemDate = RoundedSystemTime 86400 -- day precision +type SystemSeconds = RoundedSystemTime 1 -- second precision +``` + +Phantom-typed time rounding. The `Nat` type parameter specifies rounding granularity in seconds. + +| Function | Purpose | Source | +|----------|---------|--------| +| `getRoundedSystemTime` | Get current time rounded to `t` seconds | `SystemTime.hs:40-43` | +| `getSystemDate` | Alias for day-rounded time | `SystemTime.hs:45-47` | +| `getSystemSeconds` | Second-precision (no rounding needed, just drops nanoseconds) | `SystemTime.hs:49-51` | +| `roundedToUTCTime` | Convert back to `UTCTime` | `SystemTime.hs:53-55` | + +`RoundedSystemTime` derives `FromField`/`ToField` for SQLite storage and `FromJSON`/`ToJSON` for API serialization. + +### Util + +**Source**: [`Util.hs`](../src/Simplex/Messaging/Util.hs) + +Selected utilities used across the codebase: + +**Monadic combinators**: + +| Function | Signature | Purpose | Source | +|----------|-----------|---------|--------| +| `<$?>` | `MonadFail m => (a -> Either String b) -> m a -> m b` | Lift fallible function into parser | `Util.hs:119-121` | +| `$>>=` | `(Monad m, Monad f, Traversable f) => m (f a) -> (a -> m (f b)) -> m (f b)` | Monadic bind through nested monad | `Util.hs:165-167` | +| `ifM` / `whenM` / `unlessM` | Monadic conditionals | `Util.hs:147-157` | +| `anyM` | Short-circuit `any` for monadic predicates (strict) | `Util.hs:159-161` | + +**Error handling**: + +| Function | Purpose | Source | +|----------|---------|--------| +| `tryAllErrors` | Catch all exceptions (including async) into `ExceptT` | `Util.hs:273-275` | +| `catchAllErrors` | Same with handler | `Util.hs:281-283` | +| `tryAllOwnErrors` | Catch only "own" exceptions (re-throws async cancellation) | `Util.hs:322-324` | +| `catchAllOwnErrors` | Same with handler | `Util.hs:330-332` | +| `isOwnException` | `StackOverflow`, `HeapOverflow`, `AllocationLimitExceeded` | `Util.hs:297-304` | +| `isAsyncCancellation` | Any `SomeAsyncException` except own exceptions | `Util.hs:306-310` | +| `catchThrow` | Catch exceptions, wrap in Left | `Util.hs:289-291` | +| `allFinally` | `tryAllErrors` + `final` + `except` (like `finally` for ExceptT) | `Util.hs:293-295` | + +The own-vs-async distinction is critical: `catchOwn`/`tryAllOwnErrors` never swallow async cancellation (`ThreadKilled`, `UserInterrupt`, etc.), only synchronous exceptions and resource exhaustion (`StackOverflow`, `HeapOverflow`, `AllocationLimitExceeded`). + +**STM**: + +| Function | Purpose | Source | +|----------|---------|--------| +| `tryWriteTBQueue` | Non-blocking bounded queue write, returns success | `Util.hs:256-261` | + +**Database result helpers**: + +| Function | Purpose | Source | +|----------|---------|--------| +| `firstRow` | Extract first row with transform, or Left error | `Util.hs:346-347` | +| `maybeFirstRow` | Extract first row as Maybe | `Util.hs:349-350` | +| `firstRow'` | Like `firstRow` but transform can also fail | `Util.hs:355-356` | + +**Collection utilities**: + +| Function | Purpose | Source | +|----------|---------|--------| +| `groupOn` | `groupBy` using equality on projected key | `Util.hs:358-359` | +| `groupAllOn` | `groupOn` after `sortOn` (groups non-adjacent elements) | `Util.hs:372-373` | +| `toChunks` | Split list into `NonEmpty` chunks of size n | `Util.hs:376-380` | +| `packZipWith` | Optimized ByteString zipWith (direct memory access) | `Util.hs:236-254` | + +**Miscellaneous**: + +| Function | Purpose | Source | +|----------|---------|--------| +| `safeDecodeUtf8` | Decode UTF-8 replacing errors with `'?'` | `Util.hs:382-386` | +| `bshow` / `tshow` | `show` to `ByteString` / `Text` | `Util.hs:123-129` | +| `threadDelay'` | `Int64` delay (handles overflow by looping) | `Util.hs:391-399` | +| `diffToMicroseconds` / `diffToMilliseconds` | `NominalDiffTime` conversion | `Util.hs:401-407` | +| `labelMyThread` | Label current thread for debugging | `Util.hs:409-410` | +| `encodeJSON` / `decodeJSON` | `ToJSON a => a -> Text` / `FromJSON a => Text -> Maybe a` | `Util.hs:415-421` | +| `traverseWithKey_` | `Map` traversal discarding results | `Util.hs:423-425` | + +## Security notes + +- **Length prefix overflow**: `ByteString` encoding uses 1-byte length — silently truncates strings > 255 bytes. Callers must ensure size bounds before encoding. `Large` extends to 65535 bytes via Word16 prefix. +- **`Tail` unbounded**: `Tail` consumes all remaining input with no size check. Only safe when total message size is already bounded (e.g., within a padded SMP block). +- **base64 vs base64url**: `Parsers.base64P` uses standard alphabet (`+`/`/`), while `String.base64urlP` uses URL-safe alphabet (`-`/`_`). Mixing them causes silent decode failures. +- **`safeDecodeUtf8`**: Replaces invalid UTF-8 with `'?'` rather than failing. Suitable for logging/display, not for security-critical string comparison. diff --git a/spec/version.md b/spec/version.md index f5b954534..6d9a23c09 100644 --- a/spec/version.md +++ b/spec/version.md @@ -2,8 +2,198 @@ > Version ranges and compatibility checking for protocol evolution. -## Version Ranges +**Source files**: [`Version.hs`](../src/Simplex/Messaging/Version.hs), [`Version/Internal.hs`](../src/Simplex/Messaging/Version/Internal.hs) -## Compatibility +## Overview + +All SimpleX protocols use version negotiation during handshake. Each party advertises a `VersionRange` (min..max supported), and negotiation produces a `Compatible` proof value if the ranges overlap — choosing the highest mutually-supported version. + +The `Compatible` newtype can only be constructed internally (constructor is not exported), so the type system enforces that compatibility was actually checked. + +## Types + +### `Version v` + +**Source**: `Version/Internal.hs:11-12` + +```haskell +newtype Version v = Version Word16 +``` + +Phantom-typed version number. The phantom `v` distinguishes version spaces (e.g., SMP versions vs Agent versions vs XFTP versions) at the type level, preventing accidental comparison across protocols. + +- `Encoding`: 2 bytes big-endian (via Word16 instance) +- `StrEncoding`: decimal string +- JSON: numeric value +- Derives: `Eq`, `Ord`, `Show` + +The constructor is exported from `Version.Internal` but not from `Version`, so application code cannot fabricate versions — they must come from protocol constants or parsing. + +### `VersionRange v` + +**Source**: `Version.hs:46-50` + +```haskell +data VersionRange v = VRange + { minVersion :: Version v + , maxVersion :: Version v + } +``` + +Invariant: `minVersion <= maxVersion` (enforced by smart constructors). + +The `VRange` constructor is not exported — only the pattern synonym `VersionRange` (read-only, `Version.hs:41-44`) is public. + +- `Encoding`: two Word16s concatenated (4 bytes total, `Version.hs:80-84`) +- `StrEncoding`: `"min-max"` or `"v"` if min == max (`Version.hs:86-93`) +- JSON: `{"minVersion": n, "maxVersion": n}` + +### `VersionScope v` + +**Source**: `Version.hs:64` + +```haskell +class VersionScope v +``` + +Empty typeclass used as a constraint on version operations. Each protocol declares its version scope: + +```haskell +instance VersionScope SMP +instance VersionScope Agent +``` + +This prevents accidentally mixing version ranges from different protocols in negotiation functions. + +### `Compatible a` + +**Source**: `Version.hs:117-122` + +```haskell +newtype Compatible a = Compatible_ a + +pattern Compatible :: a -> Compatible a +pattern Compatible a <- Compatible_ a +``` + +Proof that compatibility was checked. The `Compatible_` constructor is not exported — `Compatible` is a read-only pattern synonym. The only way to obtain a `Compatible` value is through `compatibleVersion`, `compatibleVRange`, `proveCompatible`, or the internal `mkCompatibleIf`. + +### `VersionI` / `VersionRangeI` type classes + +**Source**: `Version.hs:95-115` + +Multi-param typeclasses with functional dependencies for generic version/range operations. Allow extension types that wrap `Version` or `VersionRange` to participate in negotiation: + +```haskell +class VersionScope v => VersionI v a | a -> v where + type VersionRangeT v a -- associated type: range form + version :: a -> Version v + toVersionRangeT :: a -> VersionRange v -> VersionRangeT v a + +class VersionScope v => VersionRangeI v a | a -> v where + type VersionT v a -- associated type: version form + versionRange :: a -> VersionRange v + toVersionRange :: a -> VersionRange v -> a + toVersionT :: a -> Version v -> VersionT v a +``` + +Identity instances exist for `Version v` and `VersionRange v` themselves. ## Functions + +### Construction + +| Function | Signature | Purpose | Source | +|----------|-----------|---------|--------| +| `mkVersionRange` | `Version v -> Version v -> VersionRange v` | Construct range, `error` if min > max | `Version.hs:67-70` | +| `safeVersionRange` | `Version v -> Version v -> Maybe (VersionRange v)` | Safe construction, `Nothing` if invalid | `Version.hs:72-75` | +| `versionToRange` | `Version v -> VersionRange v` | Singleton range (min == max) | `Version.hs:77-78` | + +### Compatibility checking + +#### `isCompatible` + +**Source**: `Version.hs:124-125` + +```haskell +isCompatible :: VersionI v a => a -> VersionRange v -> Bool +``` + +Check if a single version falls within a range. + +#### `isCompatibleRange` + +**Source**: `Version.hs:127-130` + +```haskell +isCompatibleRange :: VersionRangeI v a => a -> VersionRange v -> Bool +``` + +Check if two version ranges overlap: `min1 <= max2 && min2 <= max1`. + +#### `proveCompatible` + +**Source**: `Version.hs:132-133` + +```haskell +proveCompatible :: VersionI v a => a -> VersionRange v -> Maybe (Compatible a) +``` + +If version is compatible, wrap in `Compatible` proof. Returns `Nothing` if out of range. + +### Negotiation + +#### `compatibleVersion` + +**Source**: `Version.hs:135-140` + +```haskell +compatibleVersion :: VersionRangeI v a => a -> VersionRange v -> Maybe (Compatible (VersionT v a)) +``` + +Negotiate a single version from two ranges. Returns `min(max1, max2)` — the highest mutually-supported version. Returns `Nothing` if ranges don't overlap. + +#### `compatibleVRange` + +**Source**: `Version.hs:143-148` + +```haskell +compatibleVRange :: VersionRangeI v a => a -> VersionRange v -> Maybe (Compatible a) +``` + +Compute the intersection of two version ranges: `(max(min1,min2), min(max1,max2))`. Returns `Nothing` if the intersection is empty (i.e., ranges don't overlap). + +#### `compatibleVRange'` + +**Source**: `Version.hs:151-156` + +```haskell +compatibleVRange' :: VersionRangeI v a => a -> Version v -> Maybe (Compatible a) +``` + +Cap a version range's maximum at a given version. Returns `Nothing` if the cap is below the range's minimum. + +## Protocol version constants + +Version constants for each protocol are defined in their respective Transport modules. For SMP, key gates include: + +- `currentSMPAgentVersion`, `supportedSMPAgentVRange` — current negotiation range +- `serviceCertsSMPVersion = 16` — service certificate handshake +- `rcvServiceSMPVersion = 19` — service subscription commands + +See [`transport.md`](transport.md) and [`rcv-services.md`](rcv-services.md) for protocol-specific version constants. + +## Negotiation protocol + +During handshake: +1. Client sends its `VersionRange` to server +2. Server computes `compatibleVRange clientRange serverRange` +3. If `Nothing` → reject connection (incompatible) +4. If `Just (Compatible agreedRange)` → use `maxVersion agreedRange` as the effective protocol version + +The `Compatible` proof flows through the connection setup, ensuring all subsequent version-gated code paths have evidence that negotiation occurred. + +## Security notes + +- **No downgrade attack protection in negotiation itself** — an active MITM could modify the version range to force a lower version. Protection comes from the TLS layer (authentication prevents MITM) and from servers setting minimum version floors. +- **`mkVersionRange` uses `error`** — only safe for compile-time constants. Runtime construction must use `safeVersionRange`.