Reading this book

Redoubt is a headless, multi-user operating system for RISC-V, built so that hostile agents can run on it, do real work, and not get out. This book describes the whole system from its code: what each part does, which rule it keeps, which test attacks that rule, and what is still planned. The tenets outrank every other page.

Reading order

1. The tenets: what Redoubt is, the threat model, the guarantees and the walls that hold them, the non-goals.
2. The glossary: the one vocabulary every page uses. Skim it once; come back to it.
3. The kernel: handles, IPC, memory, budgets, scheduling, the timer, processes, devices, boot, and the model that checks them.
4. The servers: trust tiers and labels, then one page per server, from init and the steward to the network path.
5. Userland: what a person, an agent and a developer see.
6. The security register: every security property on one table, with the code that enforces it, the test that attacks it and its residual risks. An auditor starts here.
7. The plan: one page per milestone, then the follow-ups in todo/ and the ideas past the plan in beyond/.
8. The test bench: how every claim in this book is tested.

To build and run Redoubt, see GETTING-STARTED.md. How the work itself is organised, and in what order, is outside this book: AGENTS.md is the way in.

Written as if complete

Every page describes the system as it will be at the end of the plan. Whether a part exists today is said by the status line at the top of its section, never by the prose. A section that is part built and part planned is split in two.

A status with four or more tests folds them away, so the section opens on its claim and not on a list: the status sits in a <summary> with the count of tests, and the tests follow as a bullet list inside the <details>, one per line. The checker holds the count to the list.

<details><summary>Status: built · tested (3)</summary>

- bench:redoubt-ipc
- host:redoubt-sys::every_call_round_trips
- mutation:R2OneCursor

</details>

“Built” means the code exists and its named tests pass. A host test or a build case is not a boot: code built and host-tested is not thereby running in the integrated system, and running there is its own planned section.

A section without its own status line inherits its nearest parent’s. Purpose, Residual risks and Why sections carry none: they say why and what is left, not what is claimed. Status lines appear on the kernel, server and userland pages and on the test bench page; plan, follow-up and idea pages do not use them, and the security register has a status column instead.

A test is named by its kind:

The milestones

A milestone is always written with its name.

Anything past M6 (persist, install, share) is beyond M6: an idea, not a goal, one page each under beyond/.

Rule IDs

Every security property has an ID, defined once by a heading on the page that owns it and cited everywhere else with its short name the first time on a page:

• Rules are one series, R and a number. The kernel’s come first, on the kernel pages, such as R3 (lends and abandoned calls); the server, network and policy rules take the numbers after them, on the server pages, such as R25 (the label check). A letter after the number refines a rule: R4a (open calls).
• Invariants are I and a number, all on invariants, such as I9 (pages W^X, zeroed, lends unmapped). The model checks every one after every step.
• Rule F (trusted verdicts) is the bench’s own: a verdict comes only from a party the attacker cannot impersonate (the test bench).

IDs are cited one at a time, never as ranges, and never reused: a withdrawn rule keeps its heading, marked withdrawn. The security register lists every ID.

Rendering

The pages are plain Markdown and read on GitHub as they are. mdBook renders them as a book with navigation and search:

mdbook build docs      # output in target/book
mdbook serve docs      # the same, served on localhost with live reload

Diagrams are text inside the pages: Mermaid for flows, sequences, state machines and the packet diagrams that draw a record’s words and bits, which GitHub renders too; and memmap blocks for address maps, which the book’s own preprocessor (tools/mdbook-memmap) draws to scale on a log axis, one region per line with its first address, its name and a note per column, and which read as a table on GitHub. Solid lines are built; dashed lines are planned. The book needs the mdbook-mermaid preprocessor and cargo for its own. The docs checker, redoubt-doccheck, holds every page to these rules (the test bench).

The search index

The book’s search index (target/book/searchindex-<hash>.js) is held to a ceiling of 7,000,000 bytes, 30 % under the 10,000,000 at which mdbook warns and the build check fails; the_book_builds fails over the ceiling naming the size and the three largest pages, so the failure says what grew. The index is about three times the pages’ text (3.2× in October 2026: a term’s postings for every section it appears in), and the three largest pages hold a fifth of the text. The ceiling moves only by a stated, measured decision in the same change as the measurement, and never past mdbook’s 10,000,000. Headroom is kept by keeping the pages to their argument: measurements, evidence tables, transcripts and reasoning beyond what a rule or a design needs stay outside the book, in the working notes or a case’s comment, not on the page. A page leaving the book, or splitting, is the owner’s decision, never a way to pass the check. The index needs an mdbook built with elasticlunr-rs 3.1.0 or later (an older indexer doubles every field’s tokens into the next field; scripts/setup.sh installs the right one and the same check reads the version from the binary).