Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Reference Card
参考卡片

Quick-reference for all 14+ correct-by-construction patterns with selection flowchart, pattern catalogue, composition rules, crate mapping, and types-as-guarantees cheat sheet.
这是一张 14+ 种构造即正确模式的速查卡,包括选择流程图、模式目录、组合规则、crate 映射,以及“类型即保证”速查表。

Cross-references: Every chapter — this is the lookup table for the entire book.
交叉阅读: 全书所有章节。这个文件本身就是整本书的索引表和速查表。

Quick Reference: Correct-by-Construction Patterns
速查:构造即正确模式

Pattern Selection Guide
模式选择指南

Is the bug catastrophic if missed?
├── Yes → Can it be encoded in types?
│         ├── Yes → USE CORRECT-BY-CONSTRUCTION
│         └── No  → Runtime check + extensive testing
└── No  → Runtime check is fine

这个 bug 一旦漏掉,后果会不会很严重?
├── 会 → 能不能编码进类型系统?
│      ├── 能 → 用构造即正确
│      └── 不能 → 运行时检查 + 大量测试
└── 不会 → 运行时检查通常就够

Pattern Catalogue
模式目录

#Pattern
模式
Key Trait/Type
关键 Trait/类型
Prevents
防止什么
Runtime Cost
运行时成本
Chapter
章节
1Typed Commands
类型化命令
trait IpmiCmd { type Response; }Wrong response type
响应类型错误
Zero
ch02
2Single-Use Types
单次使用类型
struct Nonce (not Clone/Copy)Nonce/key reuse
nonce/密钥复用
Zero
ch03
3Capability Tokens
能力令牌
struct AdminToken { _private: () }Unauthorised access
未授权访问
Zero
ch04
4Type-State
类型状态
Session<Active>Protocol violations
协议违规
Zero
ch05
5Dimensional Types
量纲类型
struct Celsius(f64)Unit confusion
单位混淆
Zero
ch06
6Validated Boundaries
已验证边界
struct ValidFru (via TryFrom)Unvalidated data use
未验证数据直接使用
Parse once
解析一次
ch07
7Capability Mixins
能力混入
trait FanDiagMixin: HasSpi + HasI2cMissing bus access
缺失总线能力
Zero
ch08
8Phantom Types
Phantom 类型
Register<Width16>Width/direction mismatch
宽度或方向错配
Zero
ch09
9Sentinel → Option
哨兵值转 Option
Option<u8> (not 0xFF)Sentinel-as-value bugs
把哨兵值当正常值用
Zero
ch11
10Sealed Traits
封闭 trait
trait Cmd: private::SealedUnsound external impls
外部不安全实现
Zero
ch11
11Non-Exhaustive Enums
非穷尽枚举
#[non_exhaustive] enum SkuSilent match fallthrough
静默遗漏分支
Zero
ch11
12Typestate Builder
类型状态 Builder
DerBuilder<Set, Missing>Incomplete construction
构造不完整对象
Zero
ch11
13FromStr Validation
FromStr 校验
impl FromStr for DiagLevelUnvalidated string input
未验证字符串输入
Parse once
解析一次
ch11
14Const-Generic Size
常量泛型尺寸
RegisterBank<const N: usize>Buffer size mismatch
缓冲区尺寸错配
Zero
ch11
15Safe unsafe Wrapper
安全的 unsafe 包装器
MmioRegion::read_u32()Unchecked MMIO/FFI
未约束的 MMIO/FFI
Zero
ch11
16Async Type-State
异步类型状态
AsyncSession<Active>Async protocol violations
异步协议违规
Zero
ch11
17Const Assertions
常量断言
SdrSensorId<const N: u8>Invalid compile-time IDs
非法编译期 ID
Zero
ch11
18Session Types
会话类型
Chan<SendRequest>Out-of-order channel ops
乱序通道操作
Zero
ch11
19Pin Self-Referential
Pin 自引用结构
Pin<Box<StreamParser>>Dangling intra-struct pointer
结构体内部悬垂指针
Zero
ch11
20RAII / Drop
RAII / Drop
impl Drop for SessionResource leak on any exit path
任意退出路径上的资源泄漏
Zero
ch11
21Error Type Hierarchy
错误类型层级
#[derive(Error)] enum DiagErrorSilent error swallowing
静默吞错
Zero
ch11
22#[must_use]#[must_use] struct TokenSilently dropped values
值被悄悄丢掉
Zero
ch11

Composition Rules
组合规则

Capability Token + Type-State = Authorised state transitions
Typed Command + Dimensional Type = Physically-typed responses
Validated Boundary + Phantom Type = Typed register access on validated config
Capability Mixin + Typed Command = Bus-aware typed operations
Single-Use Type + Type-State = Consume-on-transition protocols
Sealed Trait + Typed Command = Closed, sound command set
Sentinel → Option + Validated Boundary = Clean parse-once pipeline
Typestate Builder + Capability Token = Proof-of-complete construction
FromStr + #[non_exhaustive] = Evolvable, fail-fast enum parsing
Const-Generic Size + Validated Boundary = Sized, validated protocol buffers
Safe unsafe Wrapper + Phantom Type = Typed, safe MMIO access
Async Type-State + Capability Token = Authorised async transitions
Session Types + Typed Command = Fully-typed request-response channels
Pin + Type-State = Self-referential state machines that can't move
RAII (Drop) + Type-State = State-dependent cleanup guarantees
Error Hierarchy + Validated Boundary = Typed parse errors with exhaustive handling
#[must_use] + Single-Use Type = Hard-to-ignore, hard-to-reuse tokens

能力令牌 + 类型状态 = 带权限控制的状态迁移
类型化命令 + 量纲类型 = 带物理单位的响应
已验证边界 + Phantom 类型 = 在已验证配置上的类型化寄存器访问
能力混入 + 类型化命令 = 面向总线能力的类型化操作
单次使用类型 + 类型状态 = 迁移时消费的协议
Sealed Trait + 类型化命令 = 封闭且健全的命令集合
哨兵值转 Option + 已验证边界 = 干净的“解析一次”流水线
Typestate Builder + 能力令牌 = “构造完整”的证明
FromStr + #[non_exhaustive] = 可演进、失败即报的枚举解析
常量泛型尺寸 + 已验证边界 = 带尺寸保证的协议缓冲区
安全 `unsafe` 包装器 + Phantom 类型 = 类型化、可审计的 MMIO 访问
异步类型状态 + 能力令牌 = 带权限约束的异步状态迁移
会话类型 + 类型化命令 = 全类型化的请求响应通道
Pin + 类型状态 = 不能移动的自引用状态机
RAII(Drop)+ 类型状态 = 带状态约束的清理保证
错误类型层级 + 已验证边界 = 带类型信息的解析错误处理
#[must_use] + 单次使用类型 = 不容易忽略,也不容易复用的令牌

Anti-Patterns to Avoid
该避开的反模式

Anti-Pattern
反模式
Why It’s Wrong
为什么不对
Correct Alternative
更合适的替代写法
fn read_sensor() -> f64Unitless — could be °C, °F, or RPM
没有单位信息,可能是 °C、°F,也可能是 RPM
fn read_sensor() -> Celsius
fn encrypt(nonce: &[u8; 12])Nonce can be reused (borrow)
nonce 只是借用,完全可能被复用
fn encrypt(nonce: Nonce) (move)
fn admin_op(is_admin: bool)Caller can lie (true)
调用方可以随便传 true 说自己是管理员
fn admin_op(_: &AdminToken)
fn send(session: &Session)No state guarantee
完全没有状态保证
fn send(session: &Session<Active>)
fn process(data: &[u8])Not validated
数据没有验证
fn process(data: &ValidFru)
Clone on ephemeral keysDefeats single-use guarantee
会破坏单次使用保证
Don’t derive Clone
let vendor_id: u16 = 0xFFFFSentinel carried internally
把哨兵值藏在正常类型里
let vendor_id: Option<u16> = None
fn route(level: &str) with fallbackTypos silently default
拼写错了也可能静默回退
let level: DiagLevel = s.parse()?
Builder::new().finish() without fieldsIncomplete object constructed
字段没填全也能构造对象
Typestate builder: finish() gated on Set
let buf: Vec<u8> for fixed-size HW bufferSize only checked at runtime
尺寸只能在运行时检查
RegisterBank<4096> (const generic)
Raw unsafe { ptr::read(...) } scatteredUB risk, unauditable
容易出 UB,也不好审计
MmioRegion::read_u32() safe wrapper
async fn transition(&mut self)Mutable borrows don’t enforce state
可变借用本身并不能证明状态迁移
async fn transition(self) -> NextState
fn cleanup() called manuallyForgotten on early return / panic
早返回或 panic 时很容易忘
impl Drop — compiler inserts call
fn op() -> Result<T, String>Opaque error, no variant matching
错误信息不透明,也不能按变体细分处理
fn op() -> Result<T, DiagError> enum

Mapping to a Diagnostics Codebase
映射到诊断代码库

Module
模块
Applicable Pattern(s)
适用模式
protocol_libTyped commands, type-state sessions
类型化命令、类型状态会话
thermal_diagCapability mixins, dimensional types
能力混入、量纲类型
accel_diagValidated boundaries, phantom registers
已验证边界、phantom 寄存器
network_diagType-state (link training), capability tokens
类型状态(链路训练)、能力令牌
pci_topologyPhantom types (register width), validated config, sentinel → Option
phantom 类型(寄存器宽度)、已验证配置、哨兵值转 Option
event_handlerSingle-use audit tokens, capability tokens, FromStr (Component)
单次使用审计令牌、能力令牌、FromStr(Component)
event_logValidated boundaries (SEL record parsing)
已验证边界(SEL 记录解析)
compute_diagDimensional types (temperature, frequency)
量纲类型(温度、频率)
memory_diagValidated boundaries (SPD data), dimensional types
已验证边界(SPD 数据)、量纲类型
switch_diagType-state (port enumeration), phantom types
类型状态(端口枚举)、phantom 类型
config_loaderFromStr (DiagLevel, FaultStatus, DiagAction)
FromStr(DiagLevel、FaultStatus、DiagAction)
log_analyzerValidated boundaries (CompiledPatterns)
已验证边界(CompiledPatterns)
diag_frameworkTypestate builder (DerBuilder), session types (orchestrator↔worker)
Typestate builder(DerBuilder)、会话类型(orchestrator↔worker)
topology_libConst-generic register banks, safe MMIO wrappers
常量泛型寄存器组、安全 MMIO 包装器

Types as Guarantees — Quick Mapping
类型即保证:快速映射

Guarantee
保证
Rust Equivalent
Rust 对应物
Example
例子
“This proof exists”
“这个证明存在”
A type
一个类型
AdminToken
“I have the proof”
“我手里有这个证明”
A value of that type
该类型的一个值
let tok = authenticate()?;
“A implies B”
“A 蕴含 B”
Function fn(A) -> Bfn activate(AdminToken) -> Session<Active>
“Both A and B”
“A 和 B 同时成立”
Tuple (A, B) or multi-param
元组 (A, B) 或多参数
fn op(a: &AdminToken, b: &LinkTrained)
“Either A or B”
“A 或 B 其一成立”
enum { A(A), B(B) } or Result<A, B>
枚举或 Result<A, B>
Result<Session<Active>, Error>
“Always true”
“永远为真”
() (unit type)Always constructible
永远可构造
“Impossible”
“根本不可能”
! (never type) or enum Void {}Can never be constructed
永远不可构造