Enforce declared total body length during message assembly (#544)

CHANGELOG.md

@@ -11,6 +11,17 @@ All notable changes to this project will be documented in this file.
   built. See `docs/v0-3-0-to-v0-4-0-migration-guide.md` for migration examples.
   (#642)
 
+- Breaking: `MessageAssemblyState` now enforces
+  `FirstFrameHeader::total_body_len` as an authoritative declaration. A first
+  frame whose body exceeds its declared total is rejected with
+  `DeclaredTotalTooSmall`; a continuation that would overshoot the declaration
+  is rejected with `DeclaredTotalExceeded`; and a completed body whose length
+  differs from the declaration is rejected with `DeclaredTotalMismatch`.
+  Protocol implementations must supply exact totals or leave `total_body_len` as
+  `None`. Downstream exhaustive matches on `MessageAssemblyError` need arms
+  for the three new variants. See
+  [ADR 015](docs/adr-015-declared-total-body-length-contract.md).
+  ([#544](https://github.com/leynos/wireframe/issues/544))
 - Added scheduler and slot poison-recovery coverage, and extracted
   `scheduler_tests.rs` to keep `scheduler.rs` below 400 lines. (#539)
 - Added client-pool lifecycle and slot-rotation coverage that kills the

docs/adr-015-declared-total-body-length-contract.md

@@ -0,0 +1,188 @@
+# Architectural decision record (ADR) 015: declared total body length is authoritative
+
+## Status
+
+Accepted.
+
+`FirstFrameHeader::total_body_len` is authoritative: the assembler rejects a
+declaration it can already contradict, stops a continuation from overshooting
+it, and requires the completed body to match it exactly. The contract is
+implemented by issue [#544](https://github.com/leynos/wireframe/issues/544).
+
+## Date
+
+2026-10-18.
+
+## Context and problem statement
+
+`FirstFrameHeader::total_body_len` lets a protocol declare the size of a
+logical message on its first frame. `MessageSeries` stores the declaration as
+`expected_total`, and `MessageAssemblyState` uses it to reject messages that
+cannot fit the configured size limit.
+
+The declaration was only a budget input. The completion path removed the
+partial assembly and dispatched its body without comparing the accumulated
+length to the declaration, and a single-frame message was returned before any
+comparison at all. A peer could therefore declare any total that passed the
+size check, send a different number of bytes, and have the body dispatched
+unchanged. The name `total_body_len` promised a guarantee the runtime did not
+make, which is a validation weakness (CWE-20) and an inconsistent length
+interpretation (CWE-130).
+
+The formal verification guide frames the choice between an authoritative
+declaration and an advisory hint in its section on
+[whether `total_body_len` is authoritative or advisory](formal-verification-methods-in-wireframe.md#2-is-total_body_len-authoritative-or-advisory).
+
+## Decision drivers
+
+- Every caller in this repository that supplies a total already expects it to
+  be exact.
+- The size limit is only meaningful if the declared value bounds the bytes that
+  are actually buffered and dispatched.
+- The domain, not the inbound adapter, owns message-assembly invariants.
+- An over- or under-declaration must be rejected before an unbounded amount of
+  peer-controlled data is retained.
+
+## Options considered
+
+### Option A: authoritative declaration
+
+Reject any message whose assembled body length differs from the declaration.
+Enforce before buffering as well as at completion.
+
+### Option B: advisory hint
+
+Rename the field and tolerate mismatch.
+
+### Option C: enforce only at completion
+
+Keep buffering unrestricted and compare once the final frame arrives.
+
+| Topic              | Option A                | Option B      | Option C               |
+| ------------------ | ----------------------- | ------------- | ---------------------- |
+| Preserves the name | Yes                     | No (renamed)  | Yes                    |
+| Bounds buffering   | Yes, before each append | No            | No                     |
+| Bypass of limit    | Closed                  | Remains open  | Closed after buffering |
+| Caller impact      | Exact totals required   | Silent change | Exact totals required  |
+
+_Table 1: Trade-offs between the considered options._
+
+## Decision outcome
+
+Option A is adopted. `total_body_len` is a protocol commitment. Four
+enforcement points apply, all in domain code:
+
+| Stage                   | Rejected condition                            | Error                   |
+| ----------------------- | --------------------------------------------- | ----------------------- |
+| First frame             | `total_body_len < body_len`                   | `DeclaredTotalTooSmall` |
+| First frame, final      | `total_body_len != body_len`                  | `DeclaredTotalMismatch` |
+| Continuation            | accumulated body would exceed the declaration | `DeclaredTotalExceeded` |
+| Completing continuation | accumulated body differs from the declaration | `DeclaredTotalMismatch` |
+
+_Table 2: Declared-total enforcement points._
+
+- The first-frame check runs before the size-limit check. A declaration that
+  the first frame already contradicts is rejected as malformed rather than
+  measured against a limit that cannot make it valid.
+- A continuation is checked before its bytes are buffered, so an oversized
+  frame is never retained, even briefly.
+- A rejected continuation or completion removes the partial assembly. The
+  failure is reported through `MessageAssemblyError`, which the inbound adapter
+  maps to `io::ErrorKind::InvalidData` through its existing failure tracker.
+- Protocols that leave `total_body_len` as `None` are unaffected; they retain
+  the previous behaviour with no equality requirement.
+
+For screen readers: the following flow chart traces a first frame through its
+declaration check, a continuation through its admission check, and a completed
+message through the final comparison, showing where each rejection frees the
+partial assembly.
+
+```mermaid
+flowchart TD
+    A[Receive first frame] --> B[validate_first_frame]
+    B -->|declared total smaller than body| E1[Reject: DeclaredTotalTooSmall]
+    B -->|single-frame total differs| E2[Reject: DeclaredTotalMismatch]
+    B -->|valid multi-frame declaration| C[Buffer first-frame body]
+    C --> D[Receive continuation]
+    D --> F[validate_continuation]
+    F -->|would exceed declaration or overflow| E3[Reject: DeclaredTotalExceeded]
+    F -->|within declaration| G[Buffer continuation before completion]
+    G --> H{Message complete?}
+    H -->|no| D
+    H -->|yes| I[validate_completion]
+    I -->|assembled length differs| E4[Reject: DeclaredTotalMismatch]
+    I -->|exact declared length| J[Dispatch assembled message]
+    E1 --> K[Free partial assembly]
+    E2 --> K
+    E3 --> K
+    E4 --> K
+```
+
+_Figure 1: Declared-total enforcement from the first frame to dispatch._
+
+The checks live in `src/message_assembler/validation.rs`, next to the state
+machine that applies them. `PartialAssembly` owns the completion check so the
+buffered length and the declaration are read together.
+
+## Consequences
+
+### Positive
+
+- When the first frame declares a total, the dispatched body length always
+  equals that declaration. A frame that leaves `total_body_len` as `None` opts
+  out, so equality is guaranteed only for declared messages.
+- An under-declared message can no longer bypass an application-configured size
+  limit.
+- Failures are typed per enforcement point, so diagnostics distinguish an
+  unsatisfiable first frame from a completion mismatch.
+
+### Negative
+
+- A protocol that declared an approximate total will now see its messages
+  rejected. No protocol in this repository does so.
+- `MessageAssemblyError` gains three variants. The enum is not
+  `#[non_exhaustive]`, so downstream exhaustive matches need updating.
+
+## Rejected shortcuts
+
+- Do not rename `total_body_len` to make the current behaviour sound: the
+  validation weakness would remain.
+- Do not enforce only in the inbound adapter: another adapter would still see
+  the unsafe domain contract.
+- Do not compare only at completion: a peer could force the runtime to buffer
+  a body up to the configured message-size limit before the mismatch is
+  detected, rather than rejecting the overshooting frame when it arrives.
+- Do not return the mismatched body with a warning: dispatch is the security
+  boundary.
+
+## Migration plan
+
+1. Supply an exact `total_body_len`, or leave it as `None` to opt out of the
+   equality requirement.
+2. Update exhaustive matches on `MessageAssemblyError` with the new variants.
+3. Update behavioural expectations that asserted a mismatched body was
+   dispatched.
+
+## Verification
+
+- Unit tests cover under-declared single-frame totals, over-declared
+  single-frame totals, an over-declared continuation, a final frame short of
+  the declaration, exact equality, and the `None` opt-out.
+- Property tests in `src/message_assembler/declared_total_property_tests.rs`
+  quantify over arbitrary `usize` lengths. They pin acceptance against the
+  remaining room, reject unrepresentable sums near `usize::MAX` as
+  `DeclaredTotalExceeded`, and drive the public state machine across generated
+  multi-frame partitions, asserting that an overshooting frame is never
+  buffered and that only an exact final total dispatches.
+- `tests/ui/message_assembly_error_exhaustive_match.rs` pins the compile-time
+  break caused by the three new variants: a match naming only the pre-change
+  variants fails to compile, as it does for `ClientError`.
+- Behavioural tests in `tests/features/message_assembly.feature` exercise the
+  same paths through the public API.
+- `make check-fmt`, `make lint`, and `make test` pass.
+
+## References
+
+- [Issue #544](https://github.com/leynos/wireframe/issues/544)
+- [ADR 002: streaming requests and shared message assembly](adr-002-streaming-requests-and-shared-message-assembly.md)
+- [Formal verification methods in Wireframe](formal-verification-methods-in-wireframe.md)

docs/contents.md

@@ -65,6 +65,10 @@ reference when navigating the project's design and architecture material.
   client pool.
 - [ADR 014: server shutdown ownership and terminal observation](adr-014-server-shutdown-ownership.md)
   Proposed awaitable server shutdown and supervisor-failure observation.
+- [ADR 015: declared total body length is authoritative][adr-015] Accepted
+  contract for enforcing `total_body_len` during message assembly.
+
+[adr-015]: adr-015-declared-total-body-length-contract.md
 
 ## Execution plans
 

docs/developers-guide.md

@@ -614,6 +614,51 @@ duplicate/gap/out-of-order validation; and `advance_sequence_or_overflow()`
 owns the overflow decision. Each piece is independently testable and the
 decision tree stays flat and readable during future refactors.
 
+### Declared total body length architecture
+
+`FirstFrameHeader::total_body_len` is authoritative, following ADR 015. The
+contract is enforced in domain code so every adapter inherits it, and the work
+is split across four modules in `src/message_assembler/`:
+
+- `validation.rs` holds the pure checks. `validate_first_frame`,
+  `validate_continuation`, and `validate_completion` take lengths and return a
+  `MessageAssemblyError`; they hold no state and perform no I/O, so each
+  boundary is testable without an assembly.
+- `partial.rs` owns an in-flight `PartialAssembly`. It keeps the completion
+  check next to the buffered bytes it compares, so the accumulated length and
+  the declaration are read together.
+- `state.rs` owns admission and routing. It stops growing past its module size
+  budget by delegating the length arithmetic to `validation`.
+- `budget.rs` holds `ContinuationLimits`, which bundles the per-message cap
+  with the aggregate `AggregateBudgets` so a caller cannot pair the cap with
+  the wrong budgets.
+
+The four enforcement points:
+
+| Boundary                | Rejected condition                            | Variant                 |
+| ----------------------- | --------------------------------------------- | ----------------------- |
+| First frame             | declaration smaller than the frame's body     | `DeclaredTotalTooSmall` |
+| First frame, final      | body differs from the declaration             | `DeclaredTotalMismatch` |
+| Continuation            | accumulated body would exceed the declaration | `DeclaredTotalExceeded` |
+| Completing continuation | accumulated body differs from the declaration | `DeclaredTotalMismatch` |
+
+`validate_continuation` runs before the bytes are buffered, so a frame that
+would overshoot is never retained, even briefly. A rejected continuation or
+completion removes the partial assembly, so a failed message cannot linger
+under its key. The inbound adapter in `src/app/frame_handling/assembly.rs`
+translates the resulting `MessageAssemblyError` into
+`io::ErrorKind::InvalidData` through `DeserFailureTracker`; the domain never
+sees `io::Error`.
+
+Overflow is part of the contract, not an incidental guard. The accumulator uses
+`usize::checked_add`, and an unrepresentable sum is reported as
+`DeclaredTotalExceeded` with `attempted: usize::MAX` rather than wrapping to a
+small value that would appear to fit. `declared_total_property_tests.rs` pins
+that boundary over values near `usize::MAX`, and
+`tests/ui/message_assembly_error_exhaustive_match.rs` pins the compile-time
+break caused by the three new variants, matching the existing `ClientError`
+fixture.
+
 ### `fill_buf_with_prefix`
 
 The private helper `fill_buf_with_prefix(buf, prefix, endianness)` in

docs/formal-verification-methods-in-wireframe.md

@@ -131,19 +131,15 @@ This is the best candidate for the **strongest** verification investment.
 `expected_total`, and `MessageAssemblyState` uses the declared total for the
 initial size-limit check.[^22][^23][^24]
 
-However, on completion, the current `accept_continuation_frame_at` path removes
-the partial assembly and returns the assembled message without an explicit
-final equality check between the accumulated body length and
-`expected_total`.[^24]
+The completion path now enforces an explicit final equality check between the
+accumulated body length and `expected_total`, and the first-frame and
+continuation paths reject declarations that cannot be honoured.[^24] The
+contract is recorded as authoritative in
+[ADR 015](adr-015-declared-total-body-length-contract.md), following Position A
+below.
 
-That is either:
-
-- a deliberate design choice, in which case the name `total_body_len`
-  overstates the guarantee, or
-- a missing invariant, in which case it deserves both runtime enforcement and
-  verification.
-
-This is where Verus becomes plausible, but only **after** a contract decision.
+This is where Verus becomes plausible, now that the contract decision is
+settled.
 
 ### Fourth priority: `src/connection/*`
 
@@ -200,18 +196,20 @@ verify, and closer to what the implementation already does.
 
 ### 2. Is `total_body_len` authoritative or advisory?
 
-The current name strongly implies authority, but the completion path does not
-enforce it.[^22][^24]
+**Resolved:** authoritative, recorded in
+[ADR 015](adr-015-declared-total-body-length-contract.md). Completion fails if
+the actual body length differs, and the first-frame and continuation paths
+reject declarations that cannot be honoured.[^22][^24]
 
-Choose one of these positions:
+The alternatives were:
 
 - **Position A:** It is authoritative. Completion must fail if the actual body
   length differs.
 - **Position B:** It is advisory. Rename it accordingly and document that
   mismatch is tolerated.
 
-**Position A** is the stronger choice unless an existing protocol reason
-requires treating it as a hint.
+**Position A** was chosen because no existing protocol requires treating the
+declaration as a hint.
 
 ### 3. What fairness guarantee does `ConnectionActor` actually make?
 

docs/roadmap.md

@@ -655,13 +655,15 @@ cited section names the specific question it answers.
   15.1.1. See §"What widths does Wireframe actually support for length
   prefixes?". Success criteria: an ADR records the decision, constructors
   enforce the chosen set, and existing tests cover rejected widths.
-- [ ] 15.2.2. Treat `total_body_len` as either authoritative or advisory and
+- [x] 15.2.2. Treat `total_body_len` as either authoritative or advisory and
   enforce or rename it consistently across the message assembly path; record
   the decision in an ADR and add tests for both conforming and violating
   inputs. Requires 15.1.1. See §"Is `total_body_len` authoritative or
   advisory?". Success criteria: an ADR records the decision, runtime code
   enforces the chosen semantics, and tests verify both conforming and violating
-  inputs.
+  inputs. See [ADR 015](adr-015-declared-total-body-length-contract.md); issue
+  [#544](https://github.com/leynos/wireframe/issues/544) added conformance and
+  violation coverage.
 - [ ] 15.2.3. Publish named fairness and priority guarantees for
   `ConnectionActor` and encode them as model properties for Stateright checks.
   Requires 15.1.1. See §"What fairness guarantee does `ConnectionActor`
@@ -717,13 +719,14 @@ cited section names the specific question it answers.
 
 ### 15.5. Verus proofs for message assembly
 
-- [ ] 15.5.1. Enforce the chosen `total_body_len` contract in runtime code
+- [x] 15.5.1. Enforce the chosen `total_body_len` contract in runtime code
   before relying on proofs. See
   [formal verification guide §"Is `total_body_len` authoritative or advisory?"](formal-verification-methods-in-wireframe.md#2-is-total_body_len-authoritative-or-advisory)
   and
   [§"What Verus should prove in Wireframe"](formal-verification-methods-in-wireframe.md#what-verus-should-prove-in-wireframe).
   Requires 15.2.2. Success criteria: runtime assertions or checks enforce the
-  contract, and existing tests confirm the enforcement.
+  contract, and existing tests confirm the enforcement. See
+  [ADR 015](adr-015-declared-total-body-length-contract.md).
 - [ ] 15.5.2. Add proof-only modules under `verus/` for declared-total and
   buffered-byte accounting invariants. See
   [formal verification guide §Proof style recommendation](formal-verification-methods-in-wireframe.md#proof-style-recommendation)

docs/users-guide.md

@@ -1282,6 +1282,33 @@ assert!(matches!(
 ));
 ```
 
+#### Declared total body length
+
+`FirstFrameHeader::total_body_len` is an authoritative declaration, not a hint.
+When a protocol supplies it, the assembler enforces it at every boundary:
+
+- a first frame that carries more body bytes than it declares is rejected with
+  `MessageAssemblyError::DeclaredTotalTooSmall`, because its declaration can
+  never be satisfied;
+- a single-frame message whose body differs from its declaration is rejected
+  with `MessageAssemblyError::DeclaredTotalMismatch`;
+- a continuation that would push the accumulated body past the declaration is
+  rejected with `MessageAssemblyError::DeclaredTotalExceeded` before its bytes
+  are buffered; and
+- the frame that completes the message must bring the accumulated body to
+  exactly the declared total, or `MessageAssemblyError::DeclaredTotalMismatch`
+  is returned.
+
+A rejected continuation or a completion mismatch also removes its partial
+assembly, so a mismatched message never remains buffered and is never
+dispatched. A rejected first frame is refused before any assembly exists, so
+there is nothing to remove. Protocols that leave `total_body_len` as `None` opt
+out of the equality requirement and keep the previous behaviour.
+
+The declaration is also used for the size-limit check, so an exact total is the
+cheapest way to fail early on an oversized message. The decision is recorded in
+[ADR 015](adr-015-declared-total-body-length-contract.md).
+
 ### Streaming request body consumption
 
 Handlers can opt into streaming request bodies using the `StreamingBody`