swaits
ad2aa6e04d
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.
182 lines
8.7 KiB
Markdown
182 lines
8.7 KiB
Markdown
# 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<u16>`
|
||
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 <function-name>` 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.
|