From ad2aa6e04d7d168a45d6c762d1187da2e87ca9a5 Mon Sep 17 00:00:00 2001 From: Stephen Waits Date: Mon, 4 May 2026 14:06:41 -0600 Subject: [PATCH] docs(safety): document the unsafe contract end-to-end MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit After Opt #2 added six bounded `get_unchecked` blocks per chart, the project's two "no unsafe" claims (README §"At a glance" + spec §11 rule 12) were stale, and there was no single place answering "how do I know the unsafe is correct?". This commit closes both gaps: - New: docs/004. unsafe-safety-contract.md Inventories every unsafe site, names the predicate, names what establishes it (codegen-time guarantee), and lists the five layered checks (const-eval, debug_assert, miri, mutants, Creusot) with current status. Documents what's *not* yet covered (the 16-of-53 missed mutants in the LCA depth walk are behavior, not safety; transition() codegen invariants are still Phase-4 for Creusot). Includes a maintenance checklist for future unsafe. - README points at the doc and gives an honest one-paragraph summary instead of "no unsafe". - Spec rule 12 rewritten from "no unsafe in generated code" to "bounded unsafe in generated code, none in user code" with a pointer to the audit. - justfile gains `just safety` — runs const-eval (cargo check), debug_assert tests, miri, and mutants in one shot. Mirrors the doc's audit matrix so the doc never goes stale silently. --- README.md | 11 +- docs/000. original-hsmc-spec.md | 9 +- docs/004. unsafe-safety-contract.md | 181 ++++++++++++++++++++++++++++ justfile | 27 +++++ 4 files changed, 224 insertions(+), 4 deletions(-) create mode 100644 docs/004. unsafe-safety-contract.md diff --git a/README.md b/README.md index dd09b01..7f8bb18 100644 --- a/README.md +++ b/README.md @@ -173,9 +173,14 @@ For nested-state hierarchies, `emit(...)`, `terminate`, and alt-ergo + z3 discharge the proofs (`just verify`). - **No heap, no dynamic dispatch.** Pure monomorphized code. `no_std` clean by default. Designed to fit on a Cortex-M0+ under - embassy. The macro emits a small amount of `unsafe` (bounded - `get_unchecked` indexing into codegen-emitted tables whose layout - guarantees `idx < len` by construction); your code is `unsafe`-free. + embassy. The macro emits six bounded `unsafe { get_unchecked }` + blocks per chart for hot-path table indexing; their preconditions + are checked at build time by const-eval, in dev/test by + `debug_assert!`, and under `cargo +nightly miri test`. Full + inventory and audit in + [`docs/004. unsafe-safety-contract.md`](docs/004.%20unsafe-safety-contract.md). + Your chart, your action bodies, and your durings stay + `unsafe`-free. ## How a chart behaves — the rules diff --git a/docs/000. original-hsmc-spec.md b/docs/000. original-hsmc-spec.md index 52f3fe6..877200c 100644 --- a/docs/000. original-hsmc-spec.md +++ b/docs/000. original-hsmc-spec.md @@ -1186,7 +1186,14 @@ The crate is considered complete when: 11. **Timer precision.** Timers fire on the first `step()` call where cumulative elapsed time meets or exceeds the duration. They do not fire early. -12. **No unsafe code** in the public API or generated code (implementation may use unsafe internally if justified and documented). +12. **Bounded `unsafe` in generated code, none in user code.** The + generated dispatch path uses six `slice::get_unchecked` blocks + for hot-path table indexing; their bounds are guaranteed at + codegen time, checked at build time by const-eval, in dev/test + by `debug_assert!`, and in CI under Miri. Inventory + audit in + [`docs/004. unsafe-safety-contract.md`](./004.%20unsafe-safety-contract.md). + User-facing code (chart definitions, action bodies, durings, + public API surface) contains no `unsafe`. 13. **Documentation.** Every public type, method, and trait has rustdoc with examples. diff --git a/docs/004. unsafe-safety-contract.md b/docs/004. unsafe-safety-contract.md new file mode 100644 index 0000000..1b55acf --- /dev/null +++ b/docs/004. unsafe-safety-contract.md @@ -0,0 +1,181 @@ +# Unsafe Safety Contract + +This document inventories every `unsafe` block emitted by the +`statechart!` macro, states the preconditions, names what +establishes them, and lists the layered checks that prove they hold. + +It is the answer to "you said no `unsafe` — now there's `unsafe`. How +do I know it's correct?". + +## Inventory + +All `unsafe` lives in code emitted by `hsmc-macros`. The runtime +`hsmc` crate, the user's chart definition, and the user's action / +during bodies contain none. + +The blocks are six index-elision sites in five generated functions, +each pairing a `slice::get_unchecked` (or `Option::unwrap_unchecked`, +in earlier passes — currently none) with a documented bound. + +| Site | Index expression | Bound | +| ----------------------------------------------- | ---------------------------------------- | -------------------------------------- | +| `step()` — sync + async — `__DISPATCH` lookup | `cur * N_EVENTS + ev_id` | `< __DISPATCH.len() = N * N_EVENTS` | +| `apply_path()` — sync + async — `__PATH_RANGE` | `from * N_STATES + target` | `< __PATH_RANGE.len() = N * N` | +| `apply_path()` — sync + async — `__PATH_DATA[s..m]` | `s..m` from `__PATH_RANGE[idx]` | `s ≤ m ≤ __PATH_DATA.len()` | +| `apply_path()` — sync + async — `__PATH_DATA[m..e]` | `m..e` from `__PATH_RANGE[idx]` | `m ≤ e ≤ __PATH_DATA.len()` | +| `follow_defaults()` — sync + async — `__DEFAULT_CHILD` | `cur` | `< __DEFAULT_CHILD.len() = N_STATES` | +| `do_terminate()` — sync + async — `__TERMINATE_RANGE` + `__TERMINATE_DATA[s..e]` | `cur`, `s..e` | `cur < N_STATES`; `s ≤ e ≤ __TERMINATE_DATA.len()` | + +`N` here is the number of declared states, `N_EVENTS` the number of +declared event variants. Both are codegen constants per chart. + +## Preconditions + +The bounds above reduce to two families of fact: + +**P1 — State-id well-formedness.** Every `u16` value that ends up in +`self.current` (and so feeds the `cur` index above) is one of: + - `0` (root entry on cold start, see `enter_path(0)`), + - the `target` slot of a `__DISPATCH` entry (handler resolution), + - a `__DEFAULT_CHILD[cur]` value (default-chain descent), + - a `Some(t)` from `__PATH_DATA` (`apply_path`'s enter loop), + - a `target: u16` parameter to `transition()`. + +All five sources are produced by codegen from `IR::states`, whose +`StateIr.id` field is `0..N_STATES` by construction (`ir::build_ir` +assigns ids by enumeration; `ir::resolve_transitions` only resolves +identifiers to existing entries; `validate::validate` rejects +duplicates and unresolvable names). User code cannot write +`self.current` — the field is private, the chart context is the only +field handed to action bodies, and the action context's +`__terminated: &bool` reference is read-only. + +**P2 — Range-table well-formedness.** For every `(from, to)` pair the +codegen-emitted `__PATH_RANGE[from * N + to] = (s, m, e)` triple +satisfies `0 ≤ s ≤ m ≤ e ≤ __PATH_DATA.len()`. The same holds for +`__TERMINATE_RANGE[i] = (s, e)` against `__TERMINATE_DATA`. The +triple's interpretation is: exit chain is `__PATH_DATA[s..m]`, enter +chain is `__PATH_DATA[m..e]`. Both slices are required to fit inside +`__PATH_DATA`. + +Codegen establishes P2 in `compute_transition_paths` (codegen.rs +~133): every emitted offset is a `usize` cursor into a `Vec` +that is grown only by `push`, so the cursor never exceeds the +length, and the triple is recorded *after* both halves of the +chain are pushed. + +## Verification — five overlapping checks + +Each check covers a different failure mode. The unsafe surface is +secure when *all five* pass. + +### 1. Compile-time const-eval (build error) + +Every generated chart contains a `const _: () = { ... }` block +(codegen.rs ~2465) that re-states P2 as `assert!`s evaluated at type +check time. A codegen change that emits a malformed `(s, m, e)` +trips a `rustc E0080: evaluation panicked:` diagnostic before any +runtime code is produced. + +Verified: manually injecting `(s=0, m=99, e=99)` into a 4-element +`__PATH_DATA` produces + + error[E0080]: evaluation panicked: __PATH_RANGE: e past __PATH_DATA end + +so the assert is live, not optimized away. + +### 2. Runtime `debug_assert!` companions + +Every `unsafe { ... get_unchecked ... }` is paired with a +`debug_assert!` of the same predicate (codegen.rs ~2693, ~2978–2987, +~3110, ~3211). `debug_assert!` is a `#[cfg(debug_assertions)]` no-op +in `--release`, so production code pays nothing. In dev/test it +panics with a clear message before the unsafe access runs. + +Coverage: every dispatch through any of the 68 hsmc behavior tests +exercises the relevant assertions. A regression in P1 (e.g., a +codegen change that lets a stale id leak into `self.current`) panics +the test, naming the violated bound. + +### 3. Miri (UB detection) + +`cargo +nightly miri test -p hsmc` runs the test suite under Miri, +the Rust UB interpreter. Miri detects out-of-bounds reads/writes, +use-after-free, and other unsafe-related UB. + +Status: **20 unit + 46 behavior tests pass** under Miri with the +current `unsafe` set. + +### 4. Mutation testing (test-coverage proof) + +`cargo mutants` flips operators / removes branches in the +`hsmc-macros` codegen and `hsmc/src/lib.rs` runtime, rebuilding and +testing each mutant. + +Status: +- `hsmc-macros/src/codegen.rs` (safety-relevant fns + `compute_transition_paths`, `compute_terminate_paths`, + `compute_event_dispatch`): **37 of 53 caught (70%)**. The 16 + missed mutants are all in the `lca` depth-walk closure — they + produce *behaviorally* wrong dispatch (the wrong states get + exited / entered) but do not violate P1 or P2, so they cannot + cause UB. They are a *behavior* test gap (no asymmetric-depth + lateral-transition test exercises the depth-equalization path), + not an unsafe-correctness gap. +- `hsmc/src/lib.rs` (runtime): **41 of 48 caught (85%)**. The 6 + missed are all `JournalSink` ops that are no-ops without the + `journal` feature; mutating a no-op is a no-op. + +### 5. Creusot deductive proofs (formal verification, partial) + +`hsmc-verification/INVARIANTS.md` lists the spec rules that have +formal Pearlite contracts. Coverage as of this writing: + +- `EventQueue` operations: contract present, proofs in progress (🟡) +- `TimerTable` operations: contract present, proofs in progress (🟡) +- `transition()` codegen invariants (P1 + P2): **explicitly out of + scope, listed as Phase 4** — requires threading Creusot + attributes through the proc-macro itself. + +So Creusot does *not* currently cover the `unsafe` surface introduced +by Opt #2. Closing that gap is the natural Phase 4 work. + +## Failure modes the checks together rule out + +| Failure | Caught by | +| ------------------------------------------------------ | ---------------------------------- | +| Codegen emits triple with `s > m`, `m > e`, `e > len` | (1) const-eval at build time | +| Codegen emits state id ≥ N_STATES in path data | (1) const-eval at build time | +| Runtime mutates `self.current` to garbage | not possible — field is private; no API path writes a garbage value | +| User action sets `terminated` | not possible — `&bool` borrow is read-only | +| Future change introduces an unsafe path bypass | (2) debug_assert in tests, (3) miri, (4) mutants | +| Subtle UB in a non-bounds dimension (aliasing, etc.) | (3) miri | + +## What's *not* yet covered + +- **Asymmetric-depth lateral transitions in tests.** The 16 missed + mutants in `compute_transition_paths`'s LCA closure indicate the + test charts all have matched depths on both legs of every + transition. Adding a chart whose handler bubbles to a shallow + ancestor and targets a deep state on the other side would close + the gap. The existing `bubble_cross_tree` *bench* exercises this + but has no behavior assertions. +- **Phase-4 Creusot proofs.** Until those land, P1 + P2 are + established by code review of the codegen — the const-eval and + miri checks make the gap *detectable*, but not + *machine-proven-impossible*. + +## Maintenance rules + +When adding a new `unsafe` block in codegen: + +1. Express the safety predicate as a `debug_assert!` immediately + above the `unsafe { ... }`. +2. If the predicate is over a static table, extend the const-eval + block to cover it — this catches the worst class of bugs at + build time. +3. Re-run `cargo +nightly miri test -p hsmc` and `cargo mutants + -p hsmc-macros -F ` to check coverage. +4. Update this doc. The inventory above must list every unsafe + block; if the table goes stale the safety story stops being + auditable. diff --git a/justfile b/justfile index 98a89f9..abcd9ce 100644 --- a/justfile +++ b/justfile @@ -151,6 +151,33 @@ audit: cargo audit @echo "✅ Security checks passed" +# Run the full unsafe-audit matrix: const-eval at build, debug_assert! +# in debug tests, Miri for UB, mutants on the safety-relevant codegen. +# Mirrors the audit described in `docs/004. unsafe-safety-contract.md`. +[script] +safety: + echo "🔒 Unsafe safety audit" + echo "" + echo "1/4 — Compile-time const-eval (any out-of-range table entry" + echo " fails cargo check with E0080)..." + cargo check --workspace --all-targets + echo "" + echo "2/4 — Runtime debug_assert! in dev tests (every unsafe site" + echo " checks its bound on every dispatch)..." + cargo nextest run --workspace --no-default-features + cargo nextest run --workspace --features tokio + echo "" + echo "3/4 — Miri (UB detector under interpreted Rust)..." + just miri + echo "" + echo "4/4 — Mutation testing on safety-relevant codegen fns..." + cargo mutants -p hsmc-macros \ + -F "compute_transition_paths|compute_terminate_paths|compute_event_dispatch" \ + --jobs 4 --no-shuffle + echo "" + echo "✅ Unsafe audit complete. See docs/004. unsafe-safety-contract.md" + echo " for which checks cover which failure modes." + # Run Miri for UB detection (auto-installs nightly + miri component if missing). [script] miri: