diff --git a/AGENTS.md b/AGENTS.md index 4f2b6bf6..db6bb5a5 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -307,6 +307,11 @@ project: - Use dashes (`-`) for list bullets. - Use GitHub-flavoured Markdown footnotes (`[^1]`) for references and footnotes. + - Exception: roadmap-shaped Markdown edited with `mapsplice` (for example + `docs/roadmap.md`) must use inline links instead because the `mapsplice` + roadmap grammar rejects footnote references (`unsupported inline node + footnoteReference`). Cite references inline, either as a parenthetical + `(see [target](path))` or by linking an existing phrase. ## Additional tooling diff --git a/docs/developers-guide.md b/docs/developers-guide.md index 25cdb7e7..602937a3 100644 --- a/docs/developers-guide.md +++ b/docs/developers-guide.md @@ -509,6 +509,35 @@ a fresh handle without explicitly calling the constructor. while holding the logger lock, `new()` recovers the guard via `into_inner()` and drains any buffered log records, so the next test starts from a clean state. +## Roadmap editing with mapsplice + +[The combined roadmap](roadmap.md) is roadmap-shaped Markdown: `mapsplice` +parses it to append, insert, delete, and replace numbered items, so it must +stay within that tool's grammar. Phases are level-2 headings +(`## 9. Phase title`), steps are level-3 headings (`### 9.2. Step title`), and +tasks are numbered checklist items (`- [ ] 9.2.1. Task title`). + +That grammar rejects footnote references, failing with `unsupported inline +node footnoteReference`. Roadmap references must therefore use inline links +instead of the GitHub-flavoured `[^1]` footnotes used elsewhere in the +documentation set: cite a target either as a parenthetical +`(see [target](path))` or by linking an existing phrase. This is a scoped +exception to the footnote rule recorded in the +[documentation style guide](documentation-style-guide.md). + +Keep the visible link text consistent: cite ADRs by number (for example +`ADR 0005`) and design documents by a short descriptive name, rather than by +raw filename. + +`mapsplice` fails closed when the target does not match the supported grammar, +so previewing an edit to stdout doubles as a grammar check: + +```bash +MAPSPLICE_IN_PLACE=false mapsplice append docs/roadmap.md fragment.md >/dev/null +``` + +Run `make fmt` to reformat and rewrap after editing, then `make markdownlint`. + ## Spelling policy The `make spelling` gate enforces en-GB-oxendict spelling across tracked text. diff --git a/docs/documentation-style-guide.md b/docs/documentation-style-guide.md index d4334c3a..d67ab84a 100644 --- a/docs/documentation-style-guide.md +++ b/docs/documentation-style-guide.md @@ -62,6 +62,10 @@ consistent, and easy to maintain across projects. - Do not wrap tables. - Use GitHub-flavoured numeric footnotes referenced as `[^1]`. - Footnotes must be numbered in order of appearance in the document. +- Exception: roadmap-shaped Markdown edited with `mapsplice` (for example + `docs/roadmap.md`) must cite references with inline links instead of + footnotes because the `mapsplice` roadmap grammar rejects footnote + references. - Caption every table, and caption every diagram. ## Standard document types diff --git a/docs/roadmap.md b/docs/roadmap.md index 4df4bd28..6b138a39 100644 --- a/docs/roadmap.md +++ b/docs/roadmap.md @@ -207,10 +207,12 @@ stream. - [x] 6.3.1. Provide a helper (for example `Response::with_channel`) that returns a bounded channel sender alongside a `Response::MultiPacket` so - handlers can opt into streaming ergonomically.[^adr-0001] + handlers can opt into streaming ergonomically (see + [ADR 0001](adr-001-multi-packet-streaming-response-api.md)). - [x] 6.3.2. Update the multi-packet design documentation and user guide with tuple return examples that explain initial-frame handling, back-pressure, and - graceful termination.[^adr-0001] + graceful termination (see + [ADR 0001](adr-001-multi-packet-streaming-response-api.md)). - [x] 6.3.3. Add an example handler (or test fixture) demonstrating spawning a background task that pushes frames through the returned sender while the connection actor manages delivery. @@ -258,7 +260,8 @@ into a single frame, making the process transparent to the application logic. ## 8. Streaming requests and shared message assembly -This phase implements the decisions from ADR 0002,[^adr-0002] adding +This phase implements the decisions from +[ADR 0002](adr-002-streaming-requests-and-shared-message-assembly.md), adding first-class streaming request bodies, a generic message assembly abstraction, and standardized per-connection memory budgets. @@ -371,9 +374,9 @@ integration boundaries. ### 9.2. Fragment adaptor alignment - [x] 9.2.1. Introduce a `FragmentAdapter` trait as described in the - fragmentation design.[^fragmentation-design] Fragmentation behaviour must - explicitly define duplicate handling, out-of-order policies, and ownership of - purge scheduling. + [fragmentation](generic-message-fragmentation-and-re-assembly-design.md) + design. Fragmentation behaviour must explicitly define duplicate handling, + out-of-order policies, and ownership of purge scheduling. - [x] Make fragmentation opt-in by requiring explicit configuration on the `WireframeApp` builder. - [x] Expose a public purge API, so callers can drive timeout eviction. @@ -389,7 +392,8 @@ integration boundaries. ### 9.3. Unified codec handling - [x] 9.3.1. Unify codec handling between the app router and the `Connection` - actor.[^outbound-design] + actor (see + [outbound messaging design](asynchronous-outbound-messaging-design.md)). - [x] Route app-level request and response handling through the `FramePipeline` so fragmentation and metrics apply consistently. - [x] Remove duplicate codec construction in `src/app/inbound_handler.rs`; the @@ -398,8 +402,9 @@ integration boundaries. fragmentation, sequential requests, disabled fragmentation). - [x] Add BDD behavioural tests exercising the unified codec path. - [x] Note: protocol hooks (`before_send`) are deferred to a follow-up - stage because `F::Frame` and `Envelope` types may - differ.[^streaming-design] + stage because `F::Frame` and `Envelope` types may differ; see the + [streaming responses](multi-packet-and-streaming-responses-design.md) + design. ### 9.4. Property-based codec tests @@ -412,12 +417,15 @@ integration boundaries. ### 9.5. Serializer boundaries and protocol metadata - [x] 9.5.1. Decouple message encoding from `bincode`-specific traits to - support alternative serializers.[^router-design][^adr-005] + support alternative serializers (see the + [binary router library design](rust-binary-router-library-design.md) and + [ADR 0005](adr-005-serializer-abstraction.md)). - [x] Introduce a serializer-agnostic message trait or adaptor layer for `Message` types. - [x] Provide optional wire-rs or Serde bridges to reduce manual boilerplate. - [x] Define how frame metadata is exposed to the deserialization context to - enable version negotiation.[^message-versioning] + enable version negotiation (see the + [message versioning design](message-versioning.md)). - [x] Add migration guidance covering existing `bincode` users. ### 9.6. Codec performance benchmarks @@ -436,7 +444,7 @@ integration boundaries. invalid frames, including oversized payloads and correlation metadata. - [x] 9.7.3. Introduce a test observability harness in `wireframe_testing` that captures logs and metrics per test run for asserting codec failures and - recovery policies.[^adr-006] + recovery policies (see [ADR 0006](adr-006-test-observability.md)). - [x] 9.7.4. Add regression tests backed by `wireframe_testing` for the `CodecError` taxonomy and recovery policy behaviours defined in 9.1.2. Requires 9.1.2. @@ -582,19 +590,19 @@ Wireframe's protocol, framing, and message assembly layers. - [x] 15.1.1. Convert the root manifest into a hybrid workspace while keeping the root package as the default member. See - [formal-verification-methods-in-wireframe.md §Root `Cargo.toml` changes](formal-verification-methods-in-wireframe.md#root-cargotoml-changes). + [formal verification guide §Root `Cargo.toml` changes](formal-verification-methods-in-wireframe.md#root-cargotoml-changes). Success criteria: `cargo build` and `cargo test --workspace` pass with the new layout. - [x] 15.1.2. Add `crates/wireframe-verification` as an internal crate for Stateright models and shared verification harnesses. Requires 15.1.1. See - [formal-verification-methods-in-wireframe.md §Why Stateright belongs in a separate verification crate](formal-verification-methods-in-wireframe.md#why-stateright-belongs-in-a-separate-verification-crate) + [formal verification guide §Why Stateright belongs in a separate verification crate](formal-verification-methods-in-wireframe.md#why-stateright-belongs-in-a-separate-verification-crate) and [§Suggested Stateright file layout](formal-verification-methods-in-wireframe.md#suggested-stateright-file-layout). Success criteria: the crate compiles, is included as a workspace member, and contains a placeholder Stateright model that passes `cargo test`. - [x] 15.1.3. Add pinned Kani and Verus tool metadata plus repo-local Makefile install and run entry points. See - [formal-verification-methods-in-wireframe.md §Recommended repository layout](formal-verification-methods-in-wireframe.md#recommended-repository-layout) + [formal verification guide §Recommended repository layout](formal-verification-methods-in-wireframe.md#recommended-repository-layout) and [§Verus should *not* live inside the main build](formal-verification-methods-in-wireframe.md#why-verus-should-not-live-inside-the-main-build). Success criteria: a contributor can run `make install-kani` and @@ -603,56 +611,59 @@ Wireframe's protocol, framing, and message assembly layers. - [ ] 15.1.4. Add `make test-verification`, `make kani`, `make kani-full`, `make verus`, `make formal-pr`, and `make formal-nightly` Makefile targets. Requires 15.1.2 and 15.1.3. See - [formal-verification-methods-in-wireframe.md §Recommended Makefile changes](formal-verification-methods-in-wireframe.md#recommended-makefile-changes). + [formal verification guide §Recommended Makefile changes](formal-verification-methods-in-wireframe.md#recommended-makefile-changes). Success criteria: each target is accepted by `mbake validate Makefile` and returns exit 0 on a clean tree. - [ ] 15.1.5. Add separate CI jobs for Stateright, Kani smoke, and Verus proofs without changing the existing `build-test` coverage flow. See - [formal-verification-methods-in-wireframe.md §Recommended CI changes](formal-verification-methods-in-wireframe.md#recommended-ci-changes). + [formal verification guide §Recommended CI changes](formal-verification-methods-in-wireframe.md#recommended-ci-changes). Success criteria: CI pipelines pass on the default branch with the new jobs visible and green. ### 15.2. Protocol contract decisions +Each decision below is analysed in the +[formal verification guide](formal-verification-methods-in-wireframe.md); the +cited section names the specific question it answers. + - [ ] 15.2.1. Support a determined set of length-prefix widths (either `1`, `2`, `4`, and `8`, or the full `1..=8` range) and enforce them in constructors, conversions, and tests; record the decision in an ADR. Requires - 15.1.1. See the formal verification guide[^fv-guide] §"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.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 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 the formal verification guide[^fv-guide] §"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. 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. - [ ] 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 the formal verification guide[^fv-guide] §"What fairness - guarantee does `ConnectionActor` actually make?". Success criteria: the - design document enumerates each guarantee as a named property that can be - referenced by Stateright model checks. + Requires 15.1.1. See §"What fairness guarantee does `ConnectionActor` + actually make?". Success criteria: the design document enumerates each + guarantee as a named property that can be referenced by Stateright model + checks. ### 15.3. Kani bounded model checks - [ ] 15.3.1. Add smoke harnesses for supported length-prefix round-trips and unsupported-width rejection in `src/frame/*`. See - [formal-verification-methods-in-wireframe.md §Phase 1 smoke harnesses](formal-verification-methods-in-wireframe.md#phase-1-smoke-harnesses). + [formal verification guide §Phase 1 smoke harnesses](formal-verification-methods-in-wireframe.md#phase-1-smoke-harnesses). Requires 15.1.3 and 15.2.1. Success criteria: `make kani` completes with all harnesses verified. - [ ] 15.3.2. Add harnesses for `FragmentSeries`, `Reassembler`, and `MessageSeries` covering duplicates, gaps, completion, and oversize cleanup. See - [formal-verification-methods-in-wireframe.md §Phase 1 smoke harnesses](formal-verification-methods-in-wireframe.md#phase-1-smoke-harnesses) + [formal verification guide §Phase 1 smoke harnesses](formal-verification-methods-in-wireframe.md#phase-1-smoke-harnesses) and [§Phase 2 full harnesses](formal-verification-methods-in-wireframe.md#phase-2-full-harnesses). Requires 15.1.3 and 15.2.2. Success criteria: `make kani-full` completes with all fragment and assembly harnesses verified. - [ ] 15.3.3. Extend existing Proptest coverage for fragment round-trips and mixed actor action traces where Kani bounds would be too small. See - [formal-verification-methods-in-wireframe.md §Second priority: `src/fragment/*`](formal-verification-methods-in-wireframe.md#second-priority-srcfragment) + [formal verification guide §Second priority: `src/fragment/*`](formal-verification-methods-in-wireframe.md#second-priority-srcfragment) and [§How Proptest and Loom fit after these changes](formal-verification-methods-in-wireframe.md#how-proptest-and-loom-fit-after-these-changes). Requires 15.3.1. Success criteria: `make test` includes the new Proptest @@ -663,19 +674,19 @@ Wireframe's protocol, framing, and message assembly layers. - [ ] 15.4.1. Model queue arrivals, active response and multi-packet outputs, shutdown races, fairness state, and terminal markers in `crates/wireframe-verification`. See - [formal-verification-methods-in-wireframe.md §Model scope](formal-verification-methods-in-wireframe.md#model-scope). + [formal verification guide §Model scope](formal-verification-methods-in-wireframe.md#model-scope). Requires 15.1.2 and 15.2.3. Success criteria: the model compiles and a bounded BFS run completes without panics or assertion failures. - [ ] 15.4.2. Add a shared checker harness that separates safety properties from reachability properties and reports both deterministically. See - [formal-verification-methods-in-wireframe.md §Properties to encode](formal-verification-methods-in-wireframe.md#properties-to-encode) + [formal verification guide §Properties to encode](formal-verification-methods-in-wireframe.md#properties-to-encode) and [§Shared checker harness](formal-verification-methods-in-wireframe.md#shared-checker-harness). Requires 15.4.1. Success criteria: `make test-verification` exercises the checker and reports property results. - [ ] 15.4.3. Gate a bounded breadth-first search (BFS) model run in pull request CI and a deeper run in scheduled or manual workflows. See - [formal-verification-methods-in-wireframe.md §Shared checker harness](formal-verification-methods-in-wireframe.md#shared-checker-harness) + [formal verification guide §Shared checker harness](formal-verification-methods-in-wireframe.md#shared-checker-harness) and [§Recommended CI changes](formal-verification-methods-in-wireframe.md#recommended-ci-changes). Requires 15.1.5 and 15.4.2. Success criteria: the PR CI job completes within @@ -685,21 +696,21 @@ Wireframe's protocol, framing, and message assembly layers. - [ ] 15.5.1. Enforce the chosen `total_body_len` contract in runtime code before relying on proofs. See - [formal-verification-methods-in-wireframe.md §"Is `total_body_len` authoritative or advisory?"](formal-verification-methods-in-wireframe.md#2-is-total_body_len-authoritative-or-advisory) + [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. - [ ] 15.5.2. Add proof-only modules under `verus/` for declared-total and buffered-byte accounting invariants. See - [formal-verification-methods-in-wireframe.md §Proof style recommendation](formal-verification-methods-in-wireframe.md#proof-style-recommendation) + [formal verification guide §Proof style recommendation](formal-verification-methods-in-wireframe.md#proof-style-recommendation) and [§Representative proof tree](formal-verification-methods-in-wireframe.md#representative-proof-tree). Requires 15.1.3 and 15.5.1. Success criteria: `make verus` verifies all proof modules without errors. - [ ] 15.5.3. Document proof trigger discipline and contributor expectations for running `make verus`. See - [formal-verification-methods-in-wireframe.md §Trigger discipline](formal-verification-methods-in-wireframe.md#trigger-discipline) + [formal verification guide §Trigger discipline](formal-verification-methods-in-wireframe.md#trigger-discipline) and [§Recommended Makefile changes](formal-verification-methods-in-wireframe.md#recommended-makefile-changes). Requires 15.5.2. Success criteria: a contributor guide section explains @@ -801,7 +812,8 @@ ecosystem. - [ ] 18.2.1. Implement a formal message versioning system to allow for protocol evolution. - [ ] 18.2.2. Ensure version negotiation can consume codec metadata without - leaking framing details into handlers.[^message-versioning] + leaking framing details into handlers (see the + [message versioning design](message-versioning.md)). ### 18.3. Security @@ -832,25 +844,3 @@ and usability. - [ ] 19.4.1. Ensure all public items have clear, useful documentation examples. - [ ] 19.4.2. Publish documentation to `docs.rs`. - -[^adr-0001]: Refer to -[ADR 0001](adr-001-multi-packet-streaming-response-api.md). -[^adr-0002]: Refer to -[ADR 0002](adr-002-streaming-requests-and-shared-message-assembly.md). -[^fragmentation-design]: See - [fragmentation doc](generic-message-fragmentation-and-re-assembly-design.md). -[^outbound-design]: See - [outbound messaging design](asynchronous-outbound-messaging-design.md). -[^streaming-design]: See - [streaming responses design](multi-packet-and-streaming-responses-design.md). -[^router-design]: See -[rust-binary-router-library-design.md](rust-binary-router-library-design.md). -[^message-versioning]: See -[message-versioning.md](message-versioning.md). -[^adr-005]: See -[adr-005-serializer-abstraction.md](adr-005-serializer-abstraction.md). -[^adr-006]: See -[adr-006-test-observability.md](adr-006-test-observability.md). - -[^fv-guide]: See -[formal-verification-methods-in-wireframe.md](formal-verification-methods-in-wireframe.md).