hsmc/docs/004. unsafe-safety-contract.md

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. Run with --features hsmc/tokio,hsmc/journal --test-package hsmc so the integration tests in hsmc/tests/ (which are gated on those features) actually compile and run; without that, cargo-mutants restricts to the per-package test set and the asymmetric-depth lateral tests don't fire.

Status (with the correct invocation):

• hsmc-macros/src/codegen.rs safety-relevant fns (compute_transition_paths, compute_terminate_paths, compute_event_dispatch): 51 of 53 covered (14 caught + 37 unviable + 2 missed). The 37 unviable are mutations that don't compile in their context — the type system rejects them, which is a stronger form of "caught". The 2 missed are equivalent mutants analyzed below.
• hsmc/src/lib.rs (runtime): 48 of 48 covered (45 caught + 3 unviable + 0 missed) — full coverage.

Combined: 99 of 101 mutants accounted for (98%). Run with just safety.

The two equivalent mutants

Both produce identical __PATH_RANGE / __PATH_DATA output and therefore cannot be distinguished by any behavior test, however detailed.

Equivalent mutant 1. codegen.rs:140: while da > db { ... } → while da >= db { ... }.

The mutated loop walks a one extra step when da == db. The next loop (while db > da) then walks b up by one to compensate, and the third loop (while a != b) drives both legs to the same LCA. parent(root) = None and the ? operator short-circuit so going "past root" is symmetric on both sides. Result: same LCA, same exit/enter paths. Verified by hand on lateral, up-transition, and asymmetric-depth (4↔2) cases.

Equivalent mutant 2. codegen.rs:169: from != to && is_strict_ancestor(to, from) → from == to && is_strict_ancestor(to, from).

is_strict_ancestor(to, from) is always false when from == to (a state is not a strict ancestor of itself), so the mutated condition is always false and the up-transition branch becomes unreachable. Up-transitions fall through to the lateral branch, which computes lca(from, to) = to (since to is an ancestor of from); the lateral exit loop then walks source up to (exclusive of) to, and the enter loop breaks immediately on Some(to) == Some(to) returning an empty enter path. Result: same exit path, same empty enter path — same (s, m, e) triple.

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

• Phase-4 Creusot proofs. Until those land, P1 + P2 are established by code review of the codegen plus the four runtime checks above. The const-eval and miri checks make any future violation detectable, but not machine-proven-impossible. The Phase-4 work is tracked in verification/INVARIANTS.md under "Out of scope (this phase)".

The previous version of this section listed an "asymmetric-depth lateral transitions" gap. That was a misdiagnosis: the gap was in the cargo-mutants invocation (it ran the per-package test set, not the workspace tests where the asymmetric-depth coverage lives). Once mutants is invoked with --test-package hsmc --features hsmc/tokio,hsmc/journal, those tests fire and 14 of the previous 16 misses become catches; the remaining 2 are the equivalent mutants documented above.

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.