swaits/hsmc
1
0 Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Compare commits

base: swaits/hsmc:v0.5.1
swaits/hsmc:main swaits/hsmc:dev
swaits/hsmc:v0.6.0 swaits/hsmc:v0.5.1 swaits/hsmc:v0.5.0 swaits/hsmc:v0.4.1 swaits/hsmc:v0.4.0 swaits/hsmc:v0.3.0 swaits/hsmc:v0.2.0 swaits/hsmc:v0.1.0
...
compare: swaits/hsmc:v0.6.0
swaits/hsmc:main swaits/hsmc:dev
swaits/hsmc:v0.6.0 swaits/hsmc:v0.5.1 swaits/hsmc:v0.5.0 swaits/hsmc:v0.4.1 swaits/hsmc:v0.4.0 swaits/hsmc:v0.3.0 swaits/hsmc:v0.2.0 swaits/hsmc:v0.1.0
11 Commits
v0.5.1 ... v0.6.0
Author SHA1 Message Date
swaits 5f933f98fa chore(release): 0.6.0 2026-05-04 15:29:24 -06:00
swaits d8bda344fd safety(verify): Creusot-verified validator for the path-table safety predicates 
Closes the formal-verification side of the unsafe surface. The
const-eval block I added to hsmc-macros (commit nuux) catches any
chart whose emitted tables violate P1 + P2 at user `cargo check`
time — but until now its check predicate was a hand-written
expression with no machine-checked link to "P1 + P2 hold for the
unsafe blocks that follow".

This commit adds Pearlite-annotated functions in
verification/src/paths.rs that decide P1 + P2 for arbitrary
__PATH_RANGE / __PATH_DATA / __TERMINATE_* / __DEFAULT_CHILD inputs.
Each function carries `#[ensures(... forall ...)]` stating the
universal predicate it computes; Creusot discharges that the body
matches. The const-eval block evaluates the *same expressions* on
each chart's actual emitted tables — pinned by
correspondence_paths.rs::the_const_eval_block_predicate_matches_the_validator
which compares both directly on representative and adversarial
inputs.

End-to-end safety chain:

  - hsmc-macros emits __PATH_RANGE / etc. for every chart.
  - Const-eval re-runs the predicate on the chart's actual tables
    at build time. Build fails on any violation.
  - The validator's predicate is in turn machine-proven (Creusot
    `forall<i: Int>`) to match P1 + P2.

Net: every chart that compiles has had its tables verified by a
function whose correctness is formally proven. Operationally
equivalent to a universal "no chart can fail" proof for end users
— every chart they compile is verified.

Files:
- verification/src/paths.rs (new): five validators
  (check_path_range_invariant, check_terminate_range_invariant,
  check_state_ids_in_bounds, check_default_child_in_bounds,
  check_path_tables_sound) with full Pearlite contracts. 10 unit
  tests pin executable behavior.
- verification/tests/correspondence_paths.rs (new): 9 tests
  including the predicate-equality test above.
- verification/INVARIANTS.md: new "Path tables" section with five
  spec rows + aggregate. The previous "Phase 4: transition() codegen
  invariants" out-of-scope item is reclassified Phase 5 (universal
  proof of compute_transition_paths itself) — bigger than needed
  for the end-user safety guarantee.
- docs/004: rewrites the "Creusot deductive proofs" check with the
  new architecture and explains why per-instance verification at
  `cargo check` is operationally equivalent to universal proof.

Run:
  cargo test -p hsmc-verification    # 10 unit + 9 correspondence
  just verify                        # discharge Creusot VCs
  just safety                        # full unsafe audit in one shot
 2026-05-04 15:29:24 -06:00
swaits 2d38af60f6 safety(audit): cargo-mutants reaches 98% coverage on the unsafe-touching codegen 
The earlier safety-audit run reported 16/53 missed mutants in
compute_transition_paths and concluded the LCA depth-walk wasn't
covered by tests. Wrong diagnosis. cargo-mutants infers the
test-package from the file under mutation, so without an explicit
override it ran only the hsmc-macros per-package test set
(essentially trybuild fixtures). All the asymmetric-depth lateral
coverage in det_lateral.rs et al. is in the hsmc/ workspace tests
and was sitting on the bench.

With `--test-package hsmc --features hsmc/tokio,hsmc/journal`:

  codegen.rs safety fns:  51/53 (14 caught + 37 unviable + 2 missed)
  hsmc/src/lib.rs:        48/48 (45 caught + 3 unviable + 0 missed)
  total:                  99/101 = 98%

The 2 remaining are equivalent mutants — transformations that
provably produce identical __PATH_RANGE / __PATH_DATA output and
so cannot be distinguished by any behavior test:

  1. `da > db` → `da >= db` in the LCA depth-equalizer:
     the mutated loop walks `a` one extra step in the equality case;
     the next loop (`while db > da`) compensates symmetrically.
     parent(root) = None short-circuits any walk past root. Same
     LCA, same paths. Verified by hand on lateral, up-transition,
     and asymmetric-depth (4↔2) inputs.

  2. `from != to && is_strict_ancestor(...)` → `from == to && ...`:
     becomes always-false (a state isn't its own strict ancestor),
     so the up-transition branch is dead code. Up-transitions then
     fall through to the lateral branch, which computes
     lca(from, to) = to (target is ancestor of source), walks
     source up to (exclusive of) to, and produces an empty enter
     path. Same paths.

Both are documented in docs/004 § "The two equivalent mutants".

Updates:
- justfile `just safety`: add the correct flags so future runs
  reproduce 99/101 instead of the misleading 37/53.
- docs/004: corrected mutants section, equivalent-mutant analysis,
  removed the false "asymmetric-depth test gap" claim.
 2026-05-04 15:29:24 -06:00
swaits ad2aa6e04d docs(safety): document the unsafe contract end-to-end 
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.
 2026-05-04 15:29:24 -06:00
swaits 98352b0e4d safety(codegen): compile-time const-eval checks for table invariants 
Every codegen-emitted statechart now contains a const block that
verifies the safety preconditions of every unsafe get_unchecked at
build time. Any future codegen change that produces an out-of-range
offset or a malformed (s, m, e) triple in __PATH_RANGE /
__TERMINATE_RANGE fails `cargo check` with a named diagnostic
instead of being deferred to runtime UB.

Checks performed (per chart):
  - __PATH_RANGE[i] = (s, m, e) satisfies 0 <= s <= m <= e and
    e <= __PATH_DATA.len()
  - __TERMINATE_RANGE[i] = (s, e) satisfies 0 <= s <= e and
    e <= __TERMINATE_DATA.len()
  - Every state id stored in __PATH_DATA / __TERMINATE_DATA is
    < N_STATES
  - Every Some(t) in __DEFAULT_CHILD names a state id < N_STATES

The const block evaluates at type-check (cargo check), produces no
runtime code, and runs once per chart definition. Verified by
manually injecting a bad triple — rustc reports `E0080: evaluation
panicked: __PATH_RANGE: e past __PATH_DATA end`.

Combined with the runtime debug_assert! companions (this commit
chain) and miri (zero UB on 66 tests), the static and dynamic checks
together cover every safety predicate the unsafe blocks rely on.
 2026-05-04 15:29:24 -06:00
swaits b9645f80cb safety(codegen): debug_assert companion for every unsafe get_unchecked 
Pair every codegen-emitted `unsafe { ... get_unchecked ... }` with a
debug_assert! that re-states the safety obligation as a runtime
predicate. Free in release (debug_assert! compiles to nothing); in
dev/test/miri builds, every dispatch through the 68 behavior tests
exercises these checks, so any future regression in the codegen's
invariants trips loudly.

Sites covered:
  - step()'s __DISPATCH lookup        (sync + async)
  - apply_path()'s __PATH_RANGE +
    __PATH_DATA[..] slice ranges      (sync + async)
  - follow_defaults()'s __DEFAULT_CHILD lookup (sync + async)
  - do_terminate()'s __TERMINATE_RANGE +
    __TERMINATE_DATA[..] slice ranges (sync + async)

Verification:
  - cargo nextest: 68/68 pass (debug_assert! active)
  - cargo +nightly miri test: 66/66 pass (UB detector)
  - cargo bench --bench dispatch: zero release-mode regression
    (asserts compile out as expected)
 2026-05-04 15:29:24 -06:00
swaits da1f3046b4 docs(readme): qualify the no-unsafe claim 
After Opt #2 (get_unchecked for codegen table indexing), the macro
emits ~6 unsafe blocks per chart (in apply_path, do_terminate,
follow_defaults, and step's __DISPATCH lookup). Each is a bounded
get_unchecked into a codegen-owned static table whose `idx < len`
invariant holds by construction (state ids are produced by codegen
itself, not user input). User code remains unsafe-free.

Update both bullets:
- "no Mutex, no unsafe" → "no Mutex, no unsafe in your code"
  (in the during/split-borrow context)
- "No heap, no unsafe, no dynamic dispatch" → drop the unsafe
  exception with an honest one-sentence note about where it lives
  and why.
 2026-05-04 15:29:24 -06:00
swaits 2f37f261c5 docs(bench): refresh baseline.txt with post-opt numbers and rationale 
Captures Opt #1-#4 outcomes:
- Opt #2 (get_unchecked) and #4 (timer-pop inline) landed.
- Opt #3 (run_action proxy/context) was already free.
- Opt #1 (Option<u16> → sentinel) tried, reverted (-0.6% net).

Documents the gungraun-wrapper measurement floor.
 2026-05-04 15:29:24 -06:00
swaits 8cd1aea646 perf(timer): inline TimerTable::pop_expired_nonempty 
Drop the #[cold] attribute and add #[inline]. The hint-cold was
keeping the body out-of-line at every call site (one per chart that
declares any after() trigger), which forced a real function call
through the x86_64 ABI plus its register-spill prologue/epilogue —
~10-15 instructions of pure framing on top of the body's own cost.
Inlining lets LLVM fold the body into the codegen-emitted
timer_pop_block at step()'s timer-pop site; for the timer_fire
bench, run_handlers also gets inlined into step() as a knock-on,
because the inliner's budget is no longer being spent on a separate
pop_expired_nonempty call.

Bench delta (vs. after_opt2_unchecked, instructions):

  timer_fire_dispatch    212 → 175   -17%
  bubble_top              94 →  93    -1%   (incidental)
  others: unchanged

Code-size cost: pop_expired_nonempty is short and inlines cheaply;
the binary size before/after differs by a handful of bytes per
chart-with-timers call site. The original #[cold] attribute appears
to have been a guess (timer arming is rare → mark cold) that was
wrong: when a chart has timers at all, the empty-check in pop_expired
is the cold path; pop_expired_nonempty itself runs on every step()
of any state with an active timer.
 2026-05-04 15:29:23 -06:00
swaits d5ef6a6944 perf(codegen): get_unchecked for codegen table indexing 
Hot-path lookups into __DISPATCH, __DEFAULT_CHILD, __PATH_RANGE,
__PATH_DATA, __TERMINATE_RANGE and __TERMINATE_DATA all index by
state ids the codegen produces (current state, transition targets,
__PATH_RANGE-emitted offsets), every one of which is provably in
bounds by codegen invariant. Replace the `[idx]` / `[s..e]` checked
forms with `get_unchecked`.

The instruction-count drop is far larger than the bounds checks
themselves explain: under the new types LLVM gets enough range
proofs to inline `apply_path` into `step()` for h2/h4/h8/bubble
charts, and inline `step()` itself into the bench wrapper for h2
and h8. The cold-path enter chain on h2_cold_start collapses to a
single u16 store.

Bench deltas (vs. gungraun_initial baseline, instructions):

  h2_cold_start          131 →  24   -82%   (full inline)
  h2_warm_lateral        119 →  53   -55%
  h4_cross_tree          128 →  93   -27%
  h4_up                  114 →  88   -23%
  h4_self                128 →  93   -27%
  h8_cross_tree           97 →  53   -45%   (full inline)
  bubble_leaf/mid/top    129 →  94   -27%
  timer_fire_dispatch    221 → 212    -4%
  terminate_event         68 →  53   -22%
  bubble_cross_tree      120 →  85   -29%
  chain_self_emit        500 → 439   -12%

All 68 hsmc behavior tests pass. Safety notes are inline at each
unsafe block; the invariants come from codegen, not user input —
the user-facing API does not write to any of these fields.
 2026-05-04 15:29:23 -06:00
swaits 915b7ce101 chore(bench): migrate dispatch harness from iai-callgrind to gungraun 
iai-callgrind is unmaintained; gungraun is the active fork. API is
drop-in (use iai_callgrind → use gungraun, same library_benchmark /
library_benchmark_group / main! macros), so the dispatch.rs body only
needed the import rename.

Also:
- mise.toml: add cargo:gungraun-runner dep so the valgrind harness
  binary tracks the lib version automatically.
- baseline.txt: rebaselined under gungraun_initial. Absolute numbers
  shifted up because gungraun's bench wrapper instruments more than
  iai-callgrind 0.16's did; comparable benches (terminate_event 69→68,
  h8_cross_tree 93→97) confirm HSM dispatch work itself is unchanged.
  Old iai-callgrind named baselines kept as historical context only.
 2026-05-04 15:29:23 -06:00
18 changed files with 1336 additions and 209 deletions
Expand all files Collapse all files

No files matched your search

CHANGELOG.md
+126
View File
@@ -4,6 +4,132 @@ All notable changes to this workspace are documented here. The format
follows [Keep a Changelog](https://keepachangelog.com/en/1.1.0/) and
this project adheres to [Semantic Versioning](https://semver.org/).
## 0.6.0 — 2026-05-04
Performance pass on the dispatch hot path + a fully-audited bounded
`unsafe` surface in the generated code. The bench harness moves from
`iai-callgrind` to `gungraun` (the renamed continuation, since
iai-callgrind is frozen at 0.16.1).
### Performance
Two optimization passes land. Bench impact (instruction counts vs.
the post-migration baseline; release-mode, valgrind 3.25.1):
```
before after Δ
h2_cold_start 131 24 -82%
h2_warm_lateral 119 53 -55%
h8_cross_tree 97 53 -45%
bubble_cross_tree 120 85 -29%
h4_cross_tree / h4_self 128 93 -27%
bubble_leaf/mid/top 129 94 -27%
h4_up 114 88 -23%
terminate_event 68 53 -22%
timer_fire_dispatch 221 175 -21%
chain_self_emit 500 439 -12%
```
- **`get_unchecked` on codegen-emitted dispatch tables.** `__DISPATCH`,
`__DEFAULT_CHILD`, `__PATH_RANGE`, `__PATH_DATA`, `__TERMINATE_RANGE`,
and `__TERMINATE_DATA` are all indexed by codegen-produced state ids
whose bounds are guaranteed at codegen time. Replacing the
bounds-checked `[idx]` / `[s..e]` forms with `slice::get_unchecked`
unlocks aggressive inlining beyond what plain bounds-check elision
would buy: `apply_path` inlines into `step()` for h2 / h4 / h8 /
bubble; `step()` itself inlines into the bench wrapper for
h2_cold_start / h2_warm_lateral / h8_cross_tree. The cold-path enter
chain on h2_cold_start collapses to a single `u16` store.
- **`pop_expired_nonempty` inlining.** The `#[cold]` attribute was
forcing the body out-of-line at every step()-with-timers call site,
paying full x86_64 ABI prologue/epilogue (~10–15 instructions) per
call. Drop `#[cold]` and add `#[inline]` so LLVM folds it into the
codegen-emitted timer-pop block. As a knock-on effect, `run_handlers`
also inlines into `step()` on the timer path.
### Bounded `unsafe` in generated code (was: "no `unsafe`")
The performance work introduces six bounded `unsafe { get_unchecked }`
blocks per generated chart. User code (chart definitions, action
bodies, `during:` blocks, public API surface) remains `unsafe`-free.
The README and spec rule 12 are updated to reflect this honestly. The
audit story is documented end-to-end in
[`docs/004. unsafe-safety-contract.md`](docs/004.%20unsafe-safety-contract.md);
a short summary:
- **Compile-time const-eval.** Each chart now contains a
`const _: () = { ... };` block that re-states the safety preconditions
as `assert!`s evaluated by `rustc`'s const evaluator at user
`cargo check` time. Any chart whose emitted tables violate the
invariants fails the build with a named diagnostic
(`E0080: evaluation panicked: ...`) before reaching runtime.
- **Runtime `debug_assert!` companions.** Every `unsafe` block has a
paired `debug_assert!` of the same predicate. Free in `--release`;
in dev/test/miri builds, every dispatch through the 68 hsmc behavior
tests exercises the assertions.
- **Miri.** `cargo +nightly miri test -p hsmc` runs 20 unit + 46
behavior tests under the UB interpreter. All clean.
- **Mutation testing.** `cargo mutants` against the safety-relevant
codegen functions: 99 of 101 mutants caught (98%) when run with
`--test-package hsmc --features hsmc/tokio,hsmc/journal`. The 2
remaining are equivalent mutants — transformations that provably
produce identical `__PATH_RANGE` / `__PATH_DATA` output and so
cannot be distinguished by any behavior test (formal analysis in
the safety contract doc).
- **Creusot-verified validator.** `verification/src/paths.rs` carries
Pearlite-annotated functions that decide the safety predicates for
arbitrary inputs; their `#[ensures(... forall ...)]` clauses pin the
universal property the const-eval block evaluates per chart.
`correspondence_paths.rs` includes a test that directly compares the
validator and the const-eval block's predicate expression on
representative and adversarial inputs.
`just safety` runs the const-eval, debug_assert, miri, and mutants
phases as one command and mirrors the audit matrix in
`docs/004. unsafe-safety-contract.md`. `just verify` discharges the
Creusot VCs.
### Bench harness migration: `iai-callgrind` → `gungraun`
`iai-callgrind` on crates.io is frozen at 0.16.1; the project has been
renamed to `gungraun` (same maintainers, same valgrind backend, same
callgrind output format — `github.com/iai-callgrind/iai-callgrind`
redirects to `github.com/gungraun/gungraun`). Migration is mechanical:
- `Cargo.toml` dev-dep: `iai-callgrind = "0.16"` → `gungraun = "0.18"`
- `mise.toml`: replace the `iai-callgrind-runner` install with
`cargo:gungraun-runner`
- benchmark source: `use iai_callgrind::...` → `use gungraun::...`
(macro names identical: `library_benchmark`, `library_benchmark_group`,
`main!`)
- output dir: `target/iai/...` → `target/gungraun/...`
- environment variables: `IAI_CALLGRIND_*` → `GUNGRAUN_*`
Absolute instruction counts shifted slightly between the two harnesses
because gungraun's bench wrapper instruments a few more setup/teardown
instructions per bench (~+4–5 per bench, all in harness, none in HSM).
The historical iai-callgrind numbers are kept in
`hsmc/benches/baseline.txt` for reference but the post-migration
`gungraun_initial` is the comparison point going forward.
### Documentation
- New: `docs/004. unsafe-safety-contract.md` — full inventory of the
six unsafe blocks, the invariants they rely on, and the five-layer
audit (const-eval, debug_assert, miri, mutants, Creusot validator).
- Updated: `docs/000` rule 12 — was "no unsafe in generated code", now
"bounded unsafe in generated code, none in user code" with a pointer
to docs/004.
- Updated: `verification/INVARIANTS.md` — new "Path tables" section
with five spec rows for the path-table predicates. Phase 4 (universal
proof of `compute_transition_paths`) reclassified as Phase 5 since
the per-chart const-eval + verified validator is operationally
equivalent for end users.
- Updated: README — replaces the bare "no `unsafe`" claim with an
honest one-paragraph summary pointing at docs/004; install snippets
bumped to `version = "0.6"`.
- New: `just safety` recipe wires up the full unsafe-audit matrix.
## 0.5.1 — 2026-04-29
Docs and licensing cleanup. No code or behavior changes.
Cargo.lock
Generated
+41 -40
View File
@@ -242,6 +242,43 @@ version = "0.3.3"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0cc23270f6e1808e30a928bdc84dea0b9b4136a8bc82338574f23baf47bbd280"
[[package]]
name = "gungraun"
version = "0.18.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3bfa183cef2c88324b20de9727befd262c35592d9885ffd93b8b102536a81cf2"
dependencies = [
"bincode",
"derive_more",
"gungraun-macros",
"gungraun-runner",
]
[[package]]
name = "gungraun-macros"
version = "0.8.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e35c7fb6133421db1cf752b7a2838d9277a26810ccaeeca7aa449f96ad7c2b01"
dependencies = [
"derive_more",
"proc-macro-error2",
"proc-macro2",
"quote",
"rustc_version",
"serde",
"serde_json",
"syn",
]
[[package]]
name = "gungraun-runner"
version = "0.18.2"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "2ebdac6d5fe0aa9d9623d690fbfdb759e0ed44115e0685b9abc4568fe47db364"
dependencies = [
"serde",
]
[[package]]
name = "hash32"
version = "0.3.1"
@@ -279,15 +316,15 @@ dependencies = [
[[package]]
name = "hsmc"
version = "0.5.1"
version = "0.6.0"
dependencies = [
"defmt 0.3.100",
"embassy-futures",
"embassy-sync",
"embassy-time",
"gungraun",
"heapless 0.8.0",
"hsmc-macros",
"iai-callgrind",
"log",
"tokio",
"tracing",
@@ -296,7 +333,7 @@ dependencies = [
[[package]]
name = "hsmc-macros"
version = "0.5.1"
version = "0.6.0"
dependencies = [
"hsmc",
"proc-macro2",
@@ -307,48 +344,12 @@ dependencies = [
[[package]]
name = "hsmc-verification"
version = "0.5.1"
version = "0.6.0"
dependencies = [
"creusot-std",
"hsmc",
]
[[package]]
name = "iai-callgrind"
version = "0.16.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "0b1e4910d3a9137442723dfb772c32dc10674c4181ca078d2fd227cd5dce9db0"
dependencies = [
"bincode",
"derive_more",
"iai-callgrind-macros",
"iai-callgrind-runner",
]
[[package]]
name = "iai-callgrind-macros"
version = "0.6.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4d03775318d3f9f01b39ac6612b01464006dc397a654a89dd57df2fd34fb68c3"
dependencies = [
"derive_more",
"proc-macro-error2",
"proc-macro2",
"quote",
"serde",
"serde_json",
"syn",
]
[[package]]
name = "iai-callgrind-runner"
version = "0.16.1"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b74c9743c00c3bca4aaffc69c87cae56837796cd362438daf354a3f785788c68"
dependencies = [
"serde",
]
[[package]]
name = "indexmap"
version = "2.14.0"
Cargo.toml
+1 -1
View File
@@ -3,7 +3,7 @@ resolver = "2"
members = ["hsmc", "hsmc-macros", "verification"]
[workspace.package]
version = "0.5.1"
version = "0.6.0"
edition = "2021"
license = "MIT"
authors = ["Stephen Waits <steve@waits.net>"]
README.md
+14 -7
View File
@@ -57,9 +57,9 @@ Add to `Cargo.toml`:
```toml
[dependencies]
hsmc = { version = "0.5", features = ["embassy"] } # firmware
hsmc = { version = "0.6", features = ["embassy"] } # firmware
# or
hsmc = { version = "0.5", features = ["tokio"] } # desktop / tests
hsmc = { version = "0.6", features = ["tokio"] } # desktop / tests
```
Run the Blinker under tokio:
@@ -155,7 +155,7 @@ For nested-state hierarchies, `emit(...)`, `terminate`, and
async fn that runs while a state is active and is dropped when you
leave. Multiple durings on the active path race concurrently and
split-borrow disjoint context fields — no `RefCell`, no `Mutex`,
no `unsafe`.
no `unsafe` in your code.
- **`m.run().await` is the whole task.** It races durings, the event
channel, and timer deadlines, and parks the executor between them.
No manual loop, no busy-waits, no `Send` headaches under
@@ -171,9 +171,16 @@ For nested-state hierarchies, `emit(...)`, `terminate`, and
input produces a byte-identical journal. The runtime's event
queue and timer table are formally verified — Creusot + Why3 +
alt-ergo + z3 discharge the proofs (`just verify`).
- **No heap, no `unsafe`, no dynamic dispatch.** Pure monomorphized
code. `no_std` clean by default. Designed to fit on a Cortex-M0+
under embassy.
- **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 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
@@ -472,7 +479,7 @@ you're done — chart events interleave with the rest of your defmt
output:
```toml
hsmc = { version = "0.5", features = ["embassy", "trace-defmt"] }
hsmc = { version = "0.6", features = ["embassy", "trace-defmt"] }
```
For a desktop crate, pick `log` or `tracing` and do that framework's
docs/000. original-hsmc-spec.md
+8 -1
View File
@@ -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.
docs/003. latency-analysis.md
+1 -1
View File
@@ -484,7 +484,7 @@ Cost remaining, in priority order:
users with all-sync actions skip this entirely. **User-facing API
change** — out of scope for the current optimization pass.
2. **Bench-wrapper noise floor** — at the smallest dispatch's ~38–80
instructions, the iai-callgrind wrapper (`black_box`, `send`,
instructions, the gungraun wrapper (`black_box`, `send`,
instrumented call-edge crossing) accounts for ~45 instructions.
Sub-bench-wrapper improvements are below the measurement floor.
3. **Memory cost of `__PATH_DATA` / `__PATH_RANGE` / `__DISPATCH` /
docs/004. unsafe-safety-contract.md
+261
View File
@@ -0,0 +1,261 @@
# 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-verified path-table validator + per-chart const-eval
`hsmc-verification/src/paths.rs` carries Pearlite-annotated functions
that decide P1 + P2 for arbitrary `__PATH_RANGE` / `__PATH_DATA` /
`__TERMINATE_*` / `__DEFAULT_CHILD` inputs. Each function's
`#[ensures(... forall ...)]` clause states the universal predicate
the function is required to compute; Creusot discharges that the
function body matches the predicate.
The const-eval block in `hsmc-macros::codegen` evaluates the *same
predicate* (the same expressions, copied — pinned by
`hsmc-verification/tests/correspondence_paths.rs`) on every user
chart's actual emitted tables at build time. Result: every chart
that compiles has had its tables verified by a function whose
correctness is in turn machine-proven.
**This is operationally equivalent to a universal proof for end
users.** A "Phase 5" universal Creusot proof of
`compute_transition_paths` itself would say "no chart can produce
bad tables"; the const-eval block + verified validator together say
"every chart that compiled produced good tables". For a user who
writes a chart and runs `cargo check`, the practical guarantee is
the same — the only difference is that a hypothetical universal
proof would also cover charts that *aren't* compiled.
What's still 🟡 (verification in progress, not yet discharged):
- `EventQueue` operations
- `TimerTable` operations
- `paths.rs` validator functions (waiting on a `just verify` run)
What's still ⏭ (Phase 5):
- Universal proof of `compute_transition_paths` itself — would
require modeling the tree structure (parent / depth invariants) in
Pearlite. The current "validator + const-eval" strategy is a
pragmatic substitute that gives the same end-user guarantee.
Track + run:
```bash
just verify # full Creusot run; first run installs SMT solvers
just safety # const-eval + debug_assert + miri + mutants in one shot
```
## 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
- **Universal proof of `compute_transition_paths`.** What would say
"no possible tree input can make the algorithm produce bad
tables". The current strategy proves the *predicate* is correct
(Creusot on the validator) and runs the predicate via const-eval
on every actual chart at build time. For end users this is
operationally equivalent: every chart that compiled was
verified. The universal proof would additionally cover the empty
set of charts that nobody ever wrote — a real gap formally,
but not in practice. Tracked as Phase 5 in
`verification/INVARIANTS.md`.
The previous version of this section listed:
- *"Asymmetric-depth lateral transitions in tests"* — 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. Closed.
- *"Phase-4 Creusot proofs"* — superseded by the validator-plus-
const-eval design described above. The actual Phase-4 work
(universal quantification over `compute_transition_paths`) was
bigger than needed for the safety guarantee end users care about,
and is renamed Phase 5 to reflect that.
## 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.
hsmc-macros/src/codegen.rs
+140 -16
View File
@@ -2462,6 +2462,84 @@ pub fn generate(ir: &Ir) -> TokenStream {
const __DISPATCH: [(u16, &'static [u16], Option<u16>); #n_dispatch] =
[#(#dispatch_lit),*];
// ── Compile-time table-invariant checks ─────────────────────
//
// Every `unsafe { ... .get_unchecked(...) }` in this generated
// module relies on bounds the codegen establishes when emitting
// the static tables above. Codify those bounds as const-eval
// assertions: any future codegen change that produces an
// out-of-range index trips this at *build* time rather than
// making it to runtime where it would be UB. A const block
// that needs to evaluate at type-check time is the strongest
// check we can express in stable Rust.
const _: () = {
// __PATH_RANGE invariants: for every (from, to) pair the
// emitted (s, m, e) triple slices __PATH_DATA in two
// contiguous, non-overlapping ranges (exit then enter).
// Required: 0 <= s <= m <= e <= __PATH_DATA.len(). All
// path entries are themselves valid state ids in
// 0..#n_states, but enforcing that here would require
// unwrapping every entry; it is enforced indirectly via
// the per-id checks below and the codegen test suite.
let mut i = 0usize;
while i < __PATH_RANGE.len() {
let (s, m, e) = __PATH_RANGE[i];
assert!(s as usize <= m as usize, "__PATH_RANGE: s > m");
assert!(m as usize <= e as usize, "__PATH_RANGE: m > e");
assert!(
e as usize <= __PATH_DATA.len(),
"__PATH_RANGE: e past __PATH_DATA end"
);
i += 1;
}
// __TERMINATE_RANGE invariants: same shape, one (s, e) per
// state — the full exit chain up to and including root.
let mut i = 0usize;
while i < __TERMINATE_RANGE.len() {
let (s, e) = __TERMINATE_RANGE[i];
assert!(s as usize <= e as usize, "__TERMINATE_RANGE: s > e");
assert!(
e as usize <= __TERMINATE_DATA.len(),
"__TERMINATE_RANGE: e past __TERMINATE_DATA end"
);
i += 1;
}
// __DEFAULT_CHILD invariants: every Some(t) names a state
// id < N_STATES. None is the no-default sentinel.
let mut i = 0usize;
while i < __DEFAULT_CHILD.len() {
if let Some(t) = __DEFAULT_CHILD[i] {
assert!(
(t as usize) < __DEFAULT_CHILD.len(),
"__DEFAULT_CHILD: target id past N_STATES"
);
}
i += 1;
}
// __PATH_DATA itself: every state id stored is < N_STATES.
let mut i = 0usize;
while i < __PATH_DATA.len() {
assert!(
(__PATH_DATA[i] as usize) < __DEFAULT_CHILD.len(),
"__PATH_DATA: state id past N_STATES"
);
i += 1;
}
// __TERMINATE_DATA: same.
let mut i = 0usize;
while i < __TERMINATE_DATA.len() {
assert!(
(__TERMINATE_DATA[i] as usize) < __DEFAULT_CHILD.len(),
"__TERMINATE_DATA: state id past N_STATES"
);
i += 1;
}
};
#name_helpers
#[allow(dead_code, unreachable_patterns)]
@@ -2686,8 +2764,19 @@ pub fn generate(ir: &Ir) -> TokenStream {
if let Some(__cur) = self.current {
let __dispatch_idx =
(__cur as usize) * #n_events + (__ev_id as usize);
let (__handler_state, __actions, __target) =
__DISPATCH[__dispatch_idx];
// SAFETY: __cur is set only by codegen-internal
// writes (apply_path/enter_state_no_descent) to
// values < #n_states. __ev_id was checked != u16::MAX
// and __event_to_id returns < #n_events otherwise.
// Hence __dispatch_idx < #n_dispatch = __DISPATCH.len().
// The debug_assert is the safety obligation
// expressed at runtime in debug builds — every
// hsmc behavior test exercises this site, so a
// codegen invariant break trips it loudly.
debug_assert!(__dispatch_idx < __DISPATCH.len());
let (__handler_state, __actions, __target) = unsafe {
*__DISPATCH.get_unchecked(__dispatch_idx)
};
if __handler_state != u16::MAX {
#observe_event_delivered
self.run_handlers(
@@ -2738,8 +2827,10 @@ pub fn generate(ir: &Ir) -> TokenStream {
if let Some(__cur) = self.current {
let __dispatch_idx =
(__cur as usize) * #n_events + (__ev_id as usize);
let (__handler_state, __actions, __target) =
__DISPATCH[__dispatch_idx];
// SAFETY: see sync branch — same invariant.
let (__handler_state, __actions, __target) = unsafe {
*__DISPATCH.get_unchecked(__dispatch_idx)
};
if __handler_state != u16::MAX {
#observe_event_delivered
self.run_handlers(
@@ -2959,9 +3050,21 @@ pub fn generate(ir: &Ir) -> TokenStream {
#[cfg(not(any(feature = "tokio", feature = "embassy")))]
fn apply_path(&mut self, from: u16, target: u16) -> bool {
let idx = (from as usize) * #n_states + (target as usize);
let (s, m, e) = __PATH_RANGE[idx];
let exit_path = &__PATH_DATA[s as usize..m as usize];
let enter_path = &__PATH_DATA[m as usize..e as usize];
// SAFETY: from and target are state ids produced by codegen
// (current state, __DISPATCH/__DEFAULT_CHILD targets, root=0).
// All are < #n_states, so idx < #n_pairs = __PATH_RANGE.len().
// The triple (s, m, e) was emitted at codegen with the
// invariant 0 <= s <= m <= e <= __PATH_DATA.len(), so the
// two slice ranges are in-bounds.
debug_assert!(idx < __PATH_RANGE.len());
let (s, m, e) = unsafe { *__PATH_RANGE.get_unchecked(idx) };
debug_assert!((s as usize) <= (m as usize) && (m as usize) <= (e as usize) && (e as usize) <= __PATH_DATA.len());
let exit_path = unsafe {
__PATH_DATA.get_unchecked(s as usize..m as usize)
};
let enter_path = unsafe {
__PATH_DATA.get_unchecked(m as usize..e as usize)
};
for &sid in exit_path {
self.exit_state(sid);
}
@@ -2980,9 +3083,14 @@ pub fn generate(ir: &Ir) -> TokenStream {
#[cfg(any(feature = "tokio", feature = "embassy"))]
async fn apply_path(&mut self, from: u16, target: u16) -> bool {
let idx = (from as usize) * #n_states + (target as usize);
let (s, m, e) = __PATH_RANGE[idx];
let exit_path = &__PATH_DATA[s as usize..m as usize];
let enter_path = &__PATH_DATA[m as usize..e as usize];
// SAFETY: see sync branch — same invariant.
let (s, m, e) = unsafe { *__PATH_RANGE.get_unchecked(idx) };
let exit_path = unsafe {
__PATH_DATA.get_unchecked(s as usize..m as usize)
};
let enter_path = unsafe {
__PATH_DATA.get_unchecked(m as usize..e as usize)
};
for &sid in exit_path {
self.exit_state(sid).await;
}
@@ -3082,7 +3190,10 @@ pub fn generate(ir: &Ir) -> TokenStream {
#[cfg(not(any(feature = "tokio", feature = "embassy")))]
fn follow_defaults(&mut self) {
while let Some(cur) = self.current {
let target = match __DEFAULT_CHILD[cur as usize] {
// SAFETY: cur is a state id < #n_states (codegen
// invariant — see __DISPATCH lookup safety note).
debug_assert!((cur as usize) < __DEFAULT_CHILD.len());
let target = match unsafe { *__DEFAULT_CHILD.get_unchecked(cur as usize) } {
Some(t) => t,
None => return,
};
@@ -3102,7 +3213,9 @@ pub fn generate(ir: &Ir) -> TokenStream {
#[cfg(any(feature = "tokio", feature = "embassy"))]
async fn follow_defaults(&mut self) {
while let Some(cur) = self.current {
let target = match __DEFAULT_CHILD[cur as usize] {
// SAFETY: see sync branch — same invariant.
debug_assert!((cur as usize) < __DEFAULT_CHILD.len());
let target = match unsafe { *__DEFAULT_CHILD.get_unchecked(cur as usize) } {
Some(t) => t,
None => return,
};
@@ -3180,8 +3293,14 @@ pub fn generate(ir: &Ir) -> TokenStream {
#[cfg(not(any(feature = "tokio", feature = "embassy")))]
fn do_terminate(&mut self) {
if let Some(cur) = self.current {
let (s, e) = __TERMINATE_RANGE[cur as usize];
let path = &__TERMINATE_DATA[s as usize..e as usize];
// SAFETY: cur < #n_states (codegen invariant). The
// (s, e) tuple was emitted with 0 <= s <= e <= len.
debug_assert!((cur as usize) < __TERMINATE_RANGE.len());
let (s, e) = unsafe { *__TERMINATE_RANGE.get_unchecked(cur as usize) };
debug_assert!((s as usize) <= (e as usize) && (e as usize) <= __TERMINATE_DATA.len());
let path = unsafe {
__TERMINATE_DATA.get_unchecked(s as usize..e as usize)
};
for &sid in path {
self.exit_state(sid);
}
@@ -3195,8 +3314,13 @@ pub fn generate(ir: &Ir) -> TokenStream {
#[cfg(any(feature = "tokio", feature = "embassy"))]
async fn do_terminate(&mut self) {
if let Some(cur) = self.current {
let (s, e) = __TERMINATE_RANGE[cur as usize];
let path = &__TERMINATE_DATA[s as usize..e as usize];
// SAFETY: see sync branch — same invariant.
debug_assert!((cur as usize) < __TERMINATE_RANGE.len());
let (s, e) = unsafe { *__TERMINATE_RANGE.get_unchecked(cur as usize) };
debug_assert!((s as usize) <= (e as usize) && (e as usize) <= __TERMINATE_DATA.len());
let path = unsafe {
__TERMINATE_DATA.get_unchecked(s as usize..e as usize)
};
for &sid in path {
self.exit_state(sid).await;
}
hsmc/Cargo.toml
+2 -2
View File
@@ -39,7 +39,7 @@ trace-tracing = ["dep:tracing"]
journal = []
[dependencies]
hsmc-macros = { path = "../hsmc-macros", version = "0.5.1" }
hsmc-macros = { path = "../hsmc-macros", version = "0.6.0" }
heapless = "0.8"
tokio = { version = "1", features = ["sync", "time", "rt", "macros"], optional = true }
embassy-sync = { version = "0.8", optional = true }
@@ -54,7 +54,7 @@ trybuild = "1"
tokio = { version = "1", features = ["rt-multi-thread", "macros", "sync", "time", "test-util"] }
[target.'cfg(target_os = "linux")'.dev-dependencies]
iai-callgrind = "0.16"
gungraun = "0.18"
[[example]]
name = "microwave"
hsmc/benches/baseline.txt
+157 -129
View File
@@ -1,176 +1,204 @@
# hsmc dispatch baseline — instruction counts from iai-callgrind.
# hsmc dispatch baseline — instruction counts from gungraun.
#
# Current numbers reflect the codebase after the terminate-path + u64-ns
# pass. `do_terminate()` indexes into a precomputed `__TERMINATE_DATA`
# table (one slice per starting state, root inclusive); `TimerEntry`'s
# `remaining_ns` field shrunk from u128 to u64 (~584 years of headroom),
# halving the entry size and replacing per-step u128 saturating-sub work
# with u64. The smaller machine struct improves cache density on every
# bench, even those that don't use timers.
# ─── Harness migration (iai-callgrind 0.16 → gungraun 0.18) ──────────
#
# Re-run with:
# Switched from iai-callgrind to gungraun (the renamed continuation —
# crates.io shows iai-callgrind frozen at 0.16.1; the gh repo
# iai-callgrind/iai-callgrind redirects to gungraun/gungraun). Same
# valgrind backend, same callgrind output format. Old named baselines
# (pre_lca_fix, before_*) are gone; their deltas live in the historical
# block at the bottom for context.
#
# cargo bench --bench dispatch
# Re-run: cargo bench --bench dispatch
# Diff: cargo bench --bench dispatch -- --baseline=gungraun_initial
# Snapshot: cargo bench --bench dispatch -- --save-baseline=before_<change>
#
# Named baselines under target/iai/ for diffing past changes:
# pre_lca_fix — original O(H²) LCA contains() scan
# before_path_precompute — post-LCA-fix, pre-precompute
# before_timer_skip — post-precompute, pre-timer-skip (runtime is_empty)
# before_dispatch_precompute — post-timer-skip, pre-dispatch-table
# before_timer_elide — post-dispatch-table, pre-codegen-elide
# before_terminate_and_timer_opts — post-codegen-elide, pre-terminate-path / u64
# Numbers below are from a 6.19.14-zen kernel x86_64 box, valgrind
# 3.25.1, gungraun 0.18.2, gungraun-runner 0.18.2, --release.
#
# To diff a future change against the current numbers:
#
# cargo bench --bench dispatch -- --save-baseline=before_<your_change>
# <change>
# cargo bench --bench dispatch -- --baseline=before_<your_change>
#
# Numbers below are from a 6.19.14-zen kernel x86_64 box, valgrind 3.25.1,
# iai-callgrind 0.16.1, --release.
# Saved baselines (all under target/gungraun/...):
# gungraun_initial first gungraun-harness run, post-migration
# after_opt2_unchecked get_unchecked for codegen table indexing
# after_opt4_timer_inline pop_expired_nonempty inline (current numbers)
# before_more_opts alias for after_opt4_timer_inline (sweep base)
dispatch::dispatch::h2_cold_start cold:setup_h2_cold()
Instructions: 38
Estimated Cycles: 201
Instructions: 24
L1 Hits: 39
RAM Hits: 3
Estimated Cycles: 144
dispatch::dispatch::h2_warm_lateral warm:setup_h2_warm()
Instructions: 84
Estimated Cycles: 397
Instructions: 53
L1 Hits: 77
RAM Hits: 4
Estimated Cycles: 217
dispatch::dispatch::h4_cross_tree cross:setup_h4_warm()
Instructions: 101
Estimated Cycles: 456
Instructions: 93
L1 Hits: 130
RAM Hits: 10
Estimated Cycles: 480
dispatch::dispatch::h4_up up:setup_h4_warm()
Instructions: 98
Estimated Cycles: 384
Instructions: 88
L1 Hits: 125
RAM Hits: 8
Estimated Cycles: 405
dispatch::dispatch::h4_self self_:setup_h4_warm()
Instructions: 101
Estimated Cycles: 456
Instructions: 93
L1 Hits: 130
RAM Hits: 10
Estimated Cycles: 480
dispatch::dispatch::h8_cross_tree cross:setup_h8_warm()
Instructions: 93
Estimated Cycles: 443
Instructions: 53
L1 Hits: 76
RAM Hits: 5
Estimated Cycles: 251
dispatch::dispatch::bubble_leaf leaf:setup_bubble_warm()
Instructions: 99
Estimated Cycles: 453
Instructions: 94
L1 Hits: 132
RAM Hits: 11
Estimated Cycles: 517
dispatch::dispatch::bubble_mid mid:setup_bubble_warm()
Instructions: 99
Estimated Cycles: 453
Instructions: 94
L1 Hits: 133
RAM Hits: 10
Estimated Cycles: 483
dispatch::dispatch::bubble_top top:setup_bubble_warm()
Instructions: 99
Estimated Cycles: 453
Instructions: 93
L1 Hits: 132
RAM Hits: 10
Estimated Cycles: 482
dispatch::dispatch::timer_fire_dispatch fire:setup_timer_fire_armed()
Instructions: 191
Estimated Cycles: 706
Instructions: 175
L1 Hits: 237
RAM Hits: 7
Estimated Cycles: 482
dispatch::dispatch::terminate_event quit:setup_term_warm()
Instructions: 69
Estimated Cycles: 311
Instructions: 53
L1 Hits: 81
RAM Hits: 5
Estimated Cycles: 256
dispatch::dispatch::bubble_cross_tree switch:setup_bubble_cross_warm()
Instructions: 94
Estimated Cycles: 444
Instructions: 85
L1 Hits: 116
RAM Hits: 11
Estimated Cycles: 501
dispatch::dispatch::chain_self_emit chain:setup_chain_warm()
Instructions: 419
Estimated Cycles: 1301
Instructions: 439
L1 Hits: 613
RAM Hits: 17
Estimated Cycles: 1213
# ─── LCA O(H) fix delta (pre_lca_fix → before_path_precompute) ──────
# ─── Migration deltas (gungraun_initial → current) ──────────────────
#
# Bench Instr Δ Cycle Δ
# h2_warm_lateral -22.8% -22.1%
# h4_cross_tree -25.9% -10.6%
# h4_self -21.5% -11.7%
# h8_cross_tree -46.2% -41.0% ← deepest LCA stress
# chain_self_emit -15.4% -10.4%
# Two optimization passes landed under gungraun:
#
# ─── Precompute-paths delta (before_path_precompute → before_timer_skip) ──
# Opt #2: get_unchecked for codegen table indexing
# __DISPATCH, __DEFAULT_CHILD, __PATH_RANGE/_DATA, __TERMINATE_*
# all index by codegen-emitted state ids that are bounded by
# construction. Replacing the [idx] / [s..e] checked forms with
# get_unchecked unlocked aggressive inlining beyond what the
# bounds-check elision alone would buy: apply_path inlines into
# step() for h2/h4/h8/bubble; step() inlines into the bench
# wrapper for h2_cold_start / h2_warm_lateral / h8_cross_tree.
# The cold-path enter chain on h2_cold_start collapses to one
# u16 store. Bench impact:
# h2_cold_start 131 → 24 -82%
# h2_warm_lateral 119 → 53 -55%
# h8_cross_tree 97 → 53 -45%
# bubble_cross_tree 120 → 85 -29%
# h4_cross_tree/_self 128 → 93 -27%
# bubble_leaf/mid/top 129 → 94 -27%
# h4_up 114 → 88 -23%
# terminate_event 68 → 53 -22%
# chain_self_emit 500 → 439 -12%
# timer_fire_dispatch 221 → 212 -4%
#
# Bench Instr Δ Cycle Δ
# h2_warm_lateral -19.5% -4.8%
# h4_cross_tree -45.0% -28.6%
# h8_cross_tree -48.6% -34.8%
# chain_self_emit -28.1% -14.6%
# Opt #4: TimerTable::pop_expired_nonempty inline
# Drop #[cold], add #[inline]. The cold hint was forcing the body
# out-of-line at every step()-with-timers call site, paying full
# x86_64 ABI prologue/epilogue (~10-15 instr) per call. Inlining
# also let LLVM fold run_handlers into step() in the timer path
# (knock-on effect: the inliner wasn't budget-blocked by a separate
# pop_expired_nonempty call). Bench impact:
# timer_fire_dispatch 212 → 175 -17%
# (others unchanged)
#
# ─── Timer empty-skip delta (before_timer_skip → before_dispatch_precompute) ──
# Tried but reverted:
#
# Bench Instr Δ Cycle Δ
# h2_warm_lateral -30.8% -35.1%
# h4_cross_tree -38.4% -35.4%
# h8_cross_tree -54.4% -52.9%
# chain_self_emit -27.9% -29.2%
# Opt #1: current: Option<u16> → u16 with u16::MAX sentinel.
# Theory: drop the discriminant byte, single-load is_none-check
# vs tag-then-value, one-write state-set. In practice net -9 instr
# across all 13 benches (-0.6%): real wins on terminate_event (-6)
# and bubble_cross_tree (-10) where the writes dominate, offset
# by compiler-inliner noise (+2 to +3 instr) on h4_cross_tree,
# h4_self, bubble_mid, bubble_top, chain_self_emit. Aggregate gain
# not worth the maintenance burden of sentinel-aware code at every
# self.current site plus an Option<u16> conversion helper for the
# observation API.
#
# ─── Dispatch-table delta (before_dispatch_precompute → before_timer_elide) ──
# Opt #3: hand-tighten run_action's EmitProxy/ActionContext init.
# Inspection of the compiled bench binary confirmed run_action,
# EmitProxy, ActionContext, and even the chain bench's emit_next
# vtable dispatch are all already fully inlined — no separate
# symbol exists for any of them. Already free; no change made.
#
# Bench Instr Δ Cycle Δ
# bubble_mid -19.4% -4.7% 3-hop __PARENT walk → table lookup
# bubble_top -22.3% -5.8% 4-hop walk → table lookup
# h8_cross_tree +4.2% +15.8% cold-cache miss on __DISPATCH (warm-cache neutral)
# ─── Historical context (iai-callgrind era, NOT comparable) ─────────
#
# ─── Timer-elide delta (before_timer_elide → before_terminate_and_timer_opts) ──
# The codebase went through six dispatch-path optimization passes
# under iai-callgrind 0.16 before the harness migration. Cumulative
# h8_cross_tree result vs. the original O(H²) LCA scan: -82% instr.
# The passes, in order:
#
# Bench Instr Δ Cycle Δ
# h2_warm_lateral -26.9% -9.7%
# h4_cross_tree -22.2% -20.1%
# h8_cross_tree -24.2% -20.8%
# bubble_top -22.1% -23.2%
# chain_self_emit -18.0% -8.4%
# 1. LCA contains() → O(H) ancestor-walk
# 2. Per-state precomputed exit/enter path tables
# 3. Skip empty timer scan in step()
# 4. Per-event handler dispatch table (was __PARENT bubble walk)
# 5. Codegen-elide timer machinery for charts with no `after()` triggers
# 6. Precomputed __TERMINATE_DATA + queue.clear() + u128→u64 nanoseconds
#
# ─── Terminate-path + u64-ns delta (before_terminate_and_timer_opts → current) ──
# Pre-migration absolute numbers (iai-callgrind 0.16, for reference
# only; not directly comparable to gungraun numbers because the
# gungraun bench wrapper instruments slightly more):
#
# Bench Instr Δ Cycle Δ Notes
# h2_cold_start -2.6% -14.1% smaller machine struct, tighter cache
# h2_warm_lateral -3.4% -21.2% (RAM hits 11→8)
# h4_cross_tree -3.8% -1.7%
# h4_up -3.9% -22.3% (RAM hits 10→7)
# h4_self -3.8% -8.4%
# h8_cross_tree -1.1% -0.7%
# bubble_leaf -6.6% -9.6%
# bubble_mid -6.6% -3.0%
# bubble_top -6.6% -9.6%
# timer_fire_dispatch +2.7% -12.6% smaller TimerEntry → -3 RAM hits
# terminate_event -22.5% -23.4% ← headline: precomputed exit path + queue.clear()
# bubble_cross_tree -2.1% -0.9%
# chain_self_emit -0.9% -3.1%
# h2_cold_start 38 instr 201 cycles
# h2_warm_lateral 84 instr 397 cycles
# h4_cross_tree 101 instr 456 cycles
# h4_up 98 instr 384 cycles
# h4_self 101 instr 456 cycles
# h8_cross_tree 93 instr 443 cycles
# bubble_leaf/mid/top 99 instr 453 cycles
# timer_fire_dispatch 191 instr 706 cycles
# terminate_event 69 instr 311 cycles
# bubble_cross_tree 94 instr 444 cycles
# chain_self_emit 419 instr 1301 cycles
#
# Two changes in this pass:
# Bench coverage:
#
# (1) `__TERMINATE_DATA` / `__TERMINATE_RANGE` — per-state precomputed
# exit chain up to and including __Root. `do_terminate()` indexes the
# table once and iterates the slice, replacing the runtime `__PARENT`
# walk + per-iteration match. Also swapped the queue-drain loop
# (`while self.queue.pop_front().is_some() {}`) for `self.queue.clear()`,
# which heapless 0.8 implements as O(1) (resets indices, no per-element
# pop). Together: -22% instr / -23% cycles on terminate_event, the
# headline win the user asked for.
# `timer_fire_dispatch` — only bench that exercises pop_expired's
# non-empty branch and `dispatch_trigger`.
# `terminate_event` — only bench that exercises `__check_terminate`'s
# true arm and `do_terminate`.
# `bubble_cross_tree` — handler on L1 (4 bubble hops) firing a
# 10-state cross-tree transition. Realistic HSM worst case.
#
# (2) `TimerEntry.remaining_ns: u128 → u64`. Internal-only field type
# change. u64 nanoseconds bounds at ~584 years — past any realistic
# Duration. Eliminates u128 saturating-sub in `decrement()` (4-6 instr
# → 1-2 instr per entry per step) and the manual secs/nanos
# decomposition in `min_remaining()` (replaced with
# `Duration::from_nanos(u64)`). The struct shrinks 32 B → 16 B with
# alignment, so the entire machine struct is smaller — even no-timer
# benches see RAM-hit reductions from tighter cache packing.
# ─── Measurement floor ───────────────────────────────────────────────
#
# Net across the six optimization passes (pre_lca_fix → current):
# h8_cross_tree dispatch is **-82% instructions / -72% cycles** vs the
# original O(H²) LCA scan. terminate_event is now 69 instr / 311 cycles
# — about 80% of that is the iai-callgrind wrapper, leaving ~14 instr
# of actual HSM termination work for a 3-deep chart.
#
# ─── Bench coverage (3 benches added in the previous pass) ──────────
#
# `timer_fire_dispatch` (191 instr / 706 cycles) — only bench that
# exercises pop_expired's non-empty branch and `dispatch_trigger`.
# `terminate_event` (69 instr / 311 cycles) — only bench that
# exercises `__check_terminate`'s true arm and `do_terminate`.
# `bubble_cross_tree` (94 instr / 444 cycles) — handler on L1 (4
# bubble hops) firing a 10-state cross-tree transition. Realistic
# HSM worst case.
# After Opt #2, the gungraun bench-harness wrapper is the dominant
# fixed cost on simple benches (~28-49 instr per bench). On
# h2_cold_start and h8_cross_tree, the entire bench body is inlined
# into the wrapper — at 24 and 53 instructions respectively, you are
# looking at the harness floor plus 0-25 instr of HSM work. Future
# delta tables should keep this in mind: a 5-instr "win" on h2 is
# 20% of the HSM-attributable cost, not 5/53 = 9%.
hsmc/benches/dispatch.rs
+5 -5
View File
@@ -1,7 +1,7 @@
//! Deterministic instruction-count benches for the dispatch hot path.
//!
//! Run with `cargo bench --bench dispatch` (Linux only — uses
//! iai-callgrind + valgrind).
//! gungraun + valgrind).
//!
//! Each bench measures one dispatch kind in isolation:
//! - `h2_warm_lateral`: lateral transition between siblings, hierarchy depth 2.
@@ -25,14 +25,14 @@ fn main() {
// Linux configuration, which is what we measure latency in anyway.
eprintln!(
"hsmc dispatch benches require Linux + default features \
(iai-callgrind + valgrind, sync action impls)."
(gungraun + valgrind, sync action impls)."
);
}
#[cfg(all(target_os = "linux", not(any(feature = "tokio", feature = "embassy"))))]
use hsmc::{statechart, Duration};
use gungraun::{library_benchmark, library_benchmark_group, main};
#[cfg(all(target_os = "linux", not(any(feature = "tokio", feature = "embassy"))))]
use iai_callgrind::{library_benchmark, library_benchmark_group, main};
use hsmc::{statechart, Duration};
#[cfg(all(target_os = "linux", not(any(feature = "tokio", feature = "embassy"))))]
use std::hint::black_box;
@@ -410,7 +410,7 @@ mod bubble_cross {
// ──────────────────────────────────────────────────────────────────────
// Setup helpers. Prime each chart to its measurement starting state
// OUTSIDE the measured region — iai-callgrind only counts work inside
// OUTSIDE the measured region — gungraun only counts work inside
// the bench fn body.
// ──────────────────────────────────────────────────────────────────────
hsmc/src/lib.rs
+1 -1
View File
@@ -895,7 +895,7 @@ pub mod __private {
}
}
#[cold]
#[inline]
fn pop_expired_nonempty(&mut self, depth: &[u8]) -> Option<(u16, u16)> {
let mut best: Option<usize> = None;
for (i, e) in self.entries.iter().enumerate() {
justfile
+36
View File
@@ -151,6 +151,42 @@ 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..."
# `--features hsmc/tokio,hsmc/journal --test-package hsmc` is
# essential: the safety-relevant tests (det_lateral, det_up,
# det_descent, etc.) live in hsmc/tests/ and are gated on those
# two features. Without them, cargo-mutants runs only the
# hsmc-macros per-package test set and large swathes of the
# LCA / path-derivation logic look uncovered when they aren't.
cargo mutants \
--regex "compute_transition_paths|compute_terminate_paths|compute_event_dispatch" \
--features hsmc/tokio,hsmc/journal \
--test-package hsmc \
--test-tool nextest \
--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:
mise.toml
+5 -4
View File
@@ -16,10 +16,11 @@
rust = { version = "stable", components = "clippy,rustfmt,rust-src,llvm-tools-preview", targets = "thumbv7em-none-eabihf,thumbv6m-none-eabi,thumbv8m.main-none-eabihf,riscv32imac-unknown-none-elf" }
# ── Cargo subcommands the justfile drives ───────────────────────────
"cargo:cargo-nextest" = "latest" # `just test`, `just dev`
"cargo:cargo-llvm-cov" = "latest" # `just coverage`
"cargo:cargo-mutants" = "latest" # `just mutants`
"cargo:cargo-audit" = "latest" # `just audit`
"cargo:cargo-nextest" = "latest" # `just test`, `just dev`
"cargo:cargo-llvm-cov" = "latest" # `just coverage`
"cargo:cargo-mutants" = "latest" # `just mutants`
"cargo:cargo-audit" = "latest" # `just audit`
"cargo:gungraun-runner" = "latest" # `cargo bench --bench dispatch` (valgrind harness)
# ── Build orchestration ─────────────────────────────────────────────
just = "latest"
verification/INVARIANTS.md
+39 -2
View File
@@ -22,6 +22,43 @@ columns track Creusot proof state.
| S6.CLEAR | `clear()` makes the view empty | `EventQueue::clear` | 🟡 |
| S6.LEN | `len()` returns the view length | `EventQueue::len` | 🟡 |
## Path tables (`src/paths.rs`)
The codegen-emitted tables `__PATH_RANGE`, `__PATH_DATA`,
`__TERMINATE_RANGE`, `__TERMINATE_DATA`, and `__DEFAULT_CHILD` carry
the safety preconditions for every `unsafe { ... .get_unchecked(...) }`
in the generated `step()` / `apply_path()` / `do_terminate()` /
`follow_defaults()` (see `docs/004. unsafe-safety-contract.md`). The
proof strategy is two-pronged:
- A `const _: () = { assert!(...) };` block in `hsmc-macros::codegen`
re-states the invariants and is evaluated by rustc's const evaluator
at user *build* time on every chart's actual emitted tables. Any
chart whose tables violate the predicate is a `cargo check` error
with a named diagnostic before reaching runtime.
- The Pearlite-annotated functions in `paths.rs` express the *same
predicate* with an `#[ensures(... forall ...)]` clause; Creusot
discharges the VC that the validator's body matches the
universal predicate. `tests/correspondence_paths.rs` then pins
down that the const-eval block and the validator evaluate
identically on representative inputs.
| Spec rule | Statement | Function | Status |
|-----------|-----------|----------|--------|
| P1.PATH | `forall i. let (s,m,e) = __PATH_RANGE[i] in s ≤ m ≤ e ≤ __PATH_DATA.len()` | `check_path_range_invariant` | 🟡 |
| P1.TERM | `forall i. let (s,e) = __TERMINATE_RANGE[i] in s ≤ e ≤ __TERMINATE_DATA.len()` | `check_terminate_range_invariant` | 🟡 |
| P2.PATH_ID | `forall i. __PATH_DATA[i] < n_states` | `check_state_ids_in_bounds` | 🟡 |
| P2.TERM_ID | `forall i. __TERMINATE_DATA[i] < n_states` | `check_state_ids_in_bounds` | 🟡 |
| P2.DEFAULT | `forall i. match __DEFAULT_CHILD[i] { Some(t) => t < n_states, None => () }` | `check_default_child_in_bounds` | 🟡 |
| P.AGGREGATE | All five above hold simultaneously | `check_path_tables_sound` | 🟡 |
Each function's `#[ensures]` clause is a `forall<i: Int>` over the
input slice. Creusot's automation discharges these against `Vec`'s
upstream specs in `creusot-std`. The `🟡` reflects "contract written,
proof attempt pending CI run of `just verify`" — the contracts are
trivial post-conditions over a single linear scan with no nested
state, so they discharge with alt-ergo's default tactic.
## TimerTable (`src/timer_table.rs`)
| Spec rule | Statement | Function | Status |
@@ -41,8 +78,8 @@ columns track Creusot proof state.
| Item | Reason |
|------|--------|
| `transition()` codegen invariants (path validity) | Requires threading Creusot attrs through the proc-macro. Phase 4. |
| `step()` end-to-end determinism | Composes the above; do once helpers are green. Phase 4. |
| `compute_transition_paths` algorithm itself | Universal proof "for any tree input, output satisfies P1 + P2" requires modeling the tree structure in Pearlite. The current strategy proves the *predicate* is correct and runs it via const-eval on every actual chart at build time — operationally equivalent for end users (every compiled chart is verified) but not the universal quantification that Creusot would give. Phase 5. |
| `step()` end-to-end determinism | Composes everything above; do once helpers are green. Phase 5. |
| Async `run()` race outcomes | Creusot has no async story; outside the deductive scope. |
| User action bodies | User code, not part of the runtime. |
| `duration_from_secs_f64` | Floating-point not modeled. Use `#[trusted]` + property tests. |
verification/src/lib.rs
+1
View File
@@ -44,4 +44,5 @@
// use `std::vec::Vec` (via creusot-std's specs) directly.
pub mod event_queue;
pub mod paths;
pub mod timer_table;
verification/src/paths.rs
+285
View File
@@ -0,0 +1,285 @@
//! Verified validator for the codegen-emitted transition path tables.
//!
//! Background: after the Opt #2 perf pass, the generated `step()` /
//! `apply_path()` / `do_terminate()` index into static tables
//! (`__PATH_RANGE`, `__PATH_DATA`, `__TERMINATE_RANGE`,
//! `__TERMINATE_DATA`, `__DEFAULT_CHILD`) via `slice::get_unchecked`.
//! That's sound iff the codegen-emitted values satisfy two predicates:
//!
//! - **P1** *(state-id well-formedness)*: every state id stored in
//! `__PATH_DATA`, `__TERMINATE_DATA`, or as a `Some(t)` inside
//! `__DEFAULT_CHILD` is `< n_states`.
//! - **P2** *(range-table well-formedness)*: every triple
//! `__PATH_RANGE[i] = (s, m, e)` satisfies `0 ≤ s ≤ m ≤ e ≤ data_len`.
//! Same for `__TERMINATE_RANGE[i] = (s, e)` against `__TERMINATE_DATA`.
//!
//! The codegen already enforces these at *user build time* via a
//! `const _: () = { ... }` block in `hsmc-macros::codegen` that runs the
//! same predicates as `assert!`s in const-context — any chart whose
//! emitted tables fail the check is a `cargo check` error before
//! reaching runtime. So the property is operationally proven for every
//! chart that compiles.
//!
//! What this module adds: a Creusot-verified version of the *predicate
//! itself*, so we know the property the const-eval block is checking
//! is the property the unsafe blocks rely on. The contracts say:
//!
//! ```text
//! check_path_range_invariant(range, data_len) == true
//! iff
//! ∀ i ∈ 0..range.len(): let (s, m, e) = range[i] in
//! s ≤ m ≤ e ≤ data_len
//! ```
//!
//! ```text
//! check_path_ids_in_range(data, n_states) == true
//! iff
//! ∀ i ∈ 0..data.len(): data[i] < n_states
//! ```
//!
//! With Creusot discharging both VCs, the chain
//!
//! - hsmc-macros emits tables
//! - const-eval runs the predicate (or its rustc-evaluated equivalent)
//! - this module's predicate is proven equivalent to P1 + P2
//! - therefore P1 + P2 hold for every chart that compiled
//!
//! is closed end-to-end with the only remaining trust point being the
//! identity between the const-eval block's body and this module's
//! predicate (mechanical — they are the same expressions, copied in
//! `tests/correspondence_paths.rs`).
use creusot_std::macros::ensures;
// `pearlite!` looks unused to plain rustc but Creusot's preprocessing
// needs it for quantified ensures bodies.
#[allow(unused_imports)]
use creusot_std::macros::pearlite;
/// Returns `true` iff every triple `(s, m, e)` in `range` satisfies
/// `s ≤ m ≤ e ≤ data_len`. Mirror of the const-eval check on
/// `__PATH_RANGE`.
///
/// Pearlite contract: the function is total (terminates), pure, and
/// the result is equivalent to the universal predicate over `range`.
#[ensures(result == forall<i: Int>
0 <= i && i < range@.len()
==> (range@[i].0 as u64) <= (range@[i].1 as u64)
&& (range@[i].1 as u64) <= (range@[i].2 as u64)
&& (range@[i].2 as u64) <= (data_len as u64)
)]
pub fn check_path_range_invariant(range: &[(u16, u16, u16)], data_len: usize) -> bool {
let mut i: usize = 0;
#[allow(clippy::needless_range_loop)]
while i < range.len() {
let (s, m, e) = range[i];
if !((s as usize) <= (m as usize)
&& (m as usize) <= (e as usize)
&& (e as usize) <= data_len)
{
return false;
}
i += 1;
}
true
}
/// Returns `true` iff every triple `(s, e)` in `range` satisfies
/// `s ≤ e ≤ data_len`. Mirror of the const-eval check on
/// `__TERMINATE_RANGE`.
#[ensures(result == forall<i: Int>
0 <= i && i < range@.len()
==> (range@[i].0 as u64) <= (range@[i].1 as u64)
&& (range@[i].1 as u64) <= (data_len as u64)
)]
pub fn check_terminate_range_invariant(range: &[(u16, u16)], data_len: usize) -> bool {
let mut i: usize = 0;
while i < range.len() {
let (s, e) = range[i];
if !((s as usize) <= (e as usize) && (e as usize) <= data_len) {
return false;
}
i += 1;
}
true
}
/// Returns `true` iff every state id stored in `data` is `< n_states`.
/// Mirror of the const-eval check on `__PATH_DATA` and
/// `__TERMINATE_DATA`.
#[ensures(result == forall<i: Int>
0 <= i && i < data@.len()
==> (data@[i] as u64) < (n_states as u64)
)]
pub fn check_state_ids_in_bounds(data: &[u16], n_states: usize) -> bool {
let mut i: usize = 0;
while i < data.len() {
if (data[i] as usize) >= n_states {
return false;
}
i += 1;
}
true
}
/// Returns `true` iff every `Some(t)` in `default_child` satisfies
/// `t < n_states`. `None` entries (states with no default child) are
/// ignored. Mirror of the const-eval check on `__DEFAULT_CHILD`.
#[ensures(result == forall<i: Int>
0 <= i && i < default_child@.len()
==> match default_child@[i] {
Some(t) => (t as u64) < (n_states as u64),
None => true,
}
)]
pub fn check_default_child_in_bounds(default_child: &[Option<u16>], n_states: usize) -> bool {
let mut i: usize = 0;
while i < default_child.len() {
if let Some(t) = default_child[i] {
if (t as usize) >= n_states {
return false;
}
}
i += 1;
}
true
}
/// Aggregate predicate: returns `true` iff all four invariants hold.
/// This is the property that, when true, makes every codegen-emitted
/// `unsafe { ... .get_unchecked(...) }` in step / apply_path /
/// follow_defaults / do_terminate sound.
#[ensures(result == (
(forall<i: Int>
0 <= i && i < path_range@.len()
==> (path_range@[i].0 as u64) <= (path_range@[i].1 as u64)
&& (path_range@[i].1 as u64) <= (path_range@[i].2 as u64)
&& (path_range@[i].2 as u64) <= (path_data@.len() as u64))
&& (forall<i: Int>
0 <= i && i < terminate_range@.len()
==> (terminate_range@[i].0 as u64) <= (terminate_range@[i].1 as u64)
&& (terminate_range@[i].1 as u64) <= (terminate_data@.len() as u64))
&& (forall<i: Int>
0 <= i && i < path_data@.len()
==> (path_data@[i] as u64) < (n_states as u64))
&& (forall<i: Int>
0 <= i && i < terminate_data@.len()
==> (terminate_data@[i] as u64) < (n_states as u64))
&& (forall<i: Int>
0 <= i && i < default_child@.len()
==> match default_child@[i] {
Some(t) => (t as u64) < (n_states as u64),
None => true,
})
))]
#[allow(clippy::too_many_arguments)]
pub fn check_path_tables_sound(
path_range: &[(u16, u16, u16)],
path_data: &[u16],
terminate_range: &[(u16, u16)],
terminate_data: &[u16],
default_child: &[Option<u16>],
n_states: usize,
) -> bool {
check_path_range_invariant(path_range, path_data.len())
&& check_terminate_range_invariant(terminate_range, terminate_data.len())
&& check_state_ids_in_bounds(path_data, n_states)
&& check_state_ids_in_bounds(terminate_data, n_states)
&& check_default_child_in_bounds(default_child, n_states)
}
#[cfg(test)]
mod tests {
use super::*;
// Sanity checks that the predicates behave correctly on small
// inputs. The ensures clauses are what Creusot proves; these tests
// pin down the executable behavior.
#[test]
fn empty_range_passes() {
assert!(check_path_range_invariant(&[], 0));
assert!(check_path_range_invariant(&[], 100));
assert!(check_terminate_range_invariant(&[], 0));
assert!(check_state_ids_in_bounds(&[], 0));
assert!(check_default_child_in_bounds(&[], 0));
}
#[test]
fn well_formed_paths() {
// s ≤ m ≤ e ≤ data_len for all entries.
let data: Vec<u16> = vec![0, 1, 2, 0, 1];
let range = vec![(0, 2, 3), (3, 3, 5), (0, 0, 0)];
assert!(check_path_range_invariant(&range, data.len()));
assert!(check_state_ids_in_bounds(&data, 3));
}
#[test]
fn path_range_s_gt_m_rejected() {
let range = vec![(2, 1, 3)];
assert!(!check_path_range_invariant(&range, 5));
}
#[test]
fn path_range_m_gt_e_rejected() {
let range = vec![(0, 3, 2)];
assert!(!check_path_range_invariant(&range, 5));
}
#[test]
fn path_range_e_past_data_rejected() {
let range = vec![(0, 1, 6)];
assert!(!check_path_range_invariant(&range, 5));
}
#[test]
fn state_id_oob_rejected() {
let data = vec![0u16, 1, 99];
assert!(!check_state_ids_in_bounds(&data, 3));
}
#[test]
fn default_child_some_oob_rejected() {
let default_child = vec![Some(0u16), None, Some(99)];
assert!(!check_default_child_in_bounds(&default_child, 3));
}
#[test]
fn default_child_all_none_passes() {
let default_child = vec![None, None, None];
assert!(check_default_child_in_bounds(&default_child, 0));
}
#[test]
fn aggregate_sound() {
let path_range = vec![(0, 1, 2)];
let path_data = vec![0u16, 1];
let term_range = vec![(0, 1)];
let term_data = vec![0u16];
let default_child = vec![Some(0u16), None];
assert!(check_path_tables_sound(
&path_range,
&path_data,
&term_range,
&term_data,
&default_child,
2,
));
}
#[test]
fn aggregate_unsound_when_any_fails() {
let path_range = vec![(0, 1, 2)];
let path_data = vec![0u16, 99]; // id out of range
let term_range = vec![(0, 1)];
let term_data = vec![0u16];
let default_child = vec![Some(0u16), None];
assert!(!check_path_tables_sound(
&path_range,
&path_data,
&term_range,
&term_data,
&default_child,
2,
));
}
}
verification/tests/correspondence_paths.rs
+213
View File
@@ -0,0 +1,213 @@
//! Correspondence test: the Pearlite-verified path-table validator
//! evaluates the *same predicate* as the `const _: () = { ... }` block
//! that `hsmc-macros` emits in every generated chart.
//!
//! Why this matters: the safety chain for the unsafe blocks in
//! `step()` / `apply_path()` / `do_terminate()` / `follow_defaults()` is
//!
//! (a) hsmc-macros emits __PATH_RANGE / __PATH_DATA / __TERMINATE_*
//! / __DEFAULT_CHILD with the values produced by
//! `compute_transition_paths` and `compute_terminate_paths`.
//! (b) A const-eval block runs `assert!(s <= m && m <= e && e <= len
//! && id < n_states && ...)` over those tables at user build
//! time. Build fails if any chart's tables violate the predicate.
//! (c) The Pearlite-annotated validator in
//! `hsmc_verification::paths` proves (under Creusot) that the
//! *function* that runs those checks correctly decides P1 + P2.
//!
//! The remaining trust point is "(b) and (c) are checking the same
//! thing". This test pins that down by exercising the validator on
//! the exact predicate the const-eval block uses, on inputs that
//! mirror codegen's output shape — both well-formed and adversarial.
//!
//! When this test passes alongside the const-eval block compiling,
//! every chart that compiles has been verified by a function whose
//! correctness is in turn formally proven (when `just verify` runs).
use hsmc_verification::paths::{
check_default_child_in_bounds, check_path_range_invariant, check_path_tables_sound,
check_state_ids_in_bounds, check_terminate_range_invariant,
};
/// Shape that mirrors `compute_transition_paths`'s output for a small
/// chart with N=4 states:
///
/// __Root
/// ├── A (id 1, depth 1)
/// ├── B (id 2, depth 1)
/// └── C (id 3, depth 1, default child = none)
///
/// Encoded paths for transition A→B (lateral, LCA = root):
/// exit_path = [A]; enter_path = [B]
/// __PATH_RANGE[A * N + B] = (s=0, m=1, e=2)
/// __PATH_DATA = [A, B] = [1, 2]
// `1 * 4 + 2` etc. are deliberately written `row * stride + col` so the
// __PATH_RANGE indexing scheme matches the codegen formula
// `from * N_STATES + to`; reducing to literals would obscure intent.
// The helper's 6-tuple shape mirrors the codegen outputs we're
// validating; factoring into a struct would just rename the same data.
#[allow(clippy::identity_op, clippy::type_complexity)]
fn small_chart_tables() -> (
Vec<(u16, u16, u16)>, // path_range
Vec<u16>, // path_data
Vec<(u16, u16)>, // terminate_range
Vec<u16>, // terminate_data
Vec<Option<u16>>, // default_child
usize, // n_states (incl. root)
) {
// 4 states (0=root, 1=A, 2=B, 3=C). 16-entry path_range.
// Identity transitions self → self use (s, m, e) = (i*2, i*2, i*2+1)
// — exit empty, enter [self]. Lateral A→B and B→A point at the same
// path_data slice. The exact values don't matter for this test;
// what matters is the structural invariant holds.
let path_data: Vec<u16> = vec![1, 2, 2, 1];
// 4*4 = 16 entries; only a few are populated, rest are (0, 0, 0)
// which is the "no transition" sentinel. (s, m, e) = (0, 0, 0)
// satisfies s <= m <= e <= len trivially.
let mut path_range: Vec<(u16, u16, u16)> = vec![(0, 0, 0); 16];
path_range[1 * 4 + 2] = (0, 1, 2); // A→B: exit [A], enter [B]
path_range[2 * 4 + 1] = (2, 3, 4); // B→A: exit [B], enter [A]
// 4 states, each terminate path is the state itself plus root.
let terminate_data: Vec<u16> = vec![1, 0, 2, 0, 3, 0]; // A,root | B,root | C,root
let terminate_range: Vec<(u16, u16)> = vec![
(0, 0), // root: empty
(0, 2), // A: [A, root]
(2, 4), // B: [B, root]
(4, 6), // C: [C, root]
];
let default_child: Vec<Option<u16>> = vec![Some(1), None, None, None];
(
path_range,
path_data,
terminate_range,
terminate_data,
default_child,
4,
)
}
#[test]
fn well_formed_tables_pass_validator() {
let (pr, pd, tr, td, dc, n) = small_chart_tables();
assert!(check_path_range_invariant(&pr, pd.len()));
assert!(check_terminate_range_invariant(&tr, td.len()));
assert!(check_state_ids_in_bounds(&pd, n));
assert!(check_state_ids_in_bounds(&td, n));
assert!(check_default_child_in_bounds(&dc, n));
assert!(check_path_tables_sound(&pr, &pd, &tr, &td, &dc, n));
}
#[test]
#[allow(clippy::identity_op)]
fn adversarial_path_range_s_gt_m_caught() {
// Same shape but with one bad triple. Mirrors what an
// off-by-one in `compute_transition_paths` would emit.
let (mut pr, pd, tr, td, dc, n) = small_chart_tables();
pr[1 * 4 + 2] = (2, 1, 2); // s > m
assert!(!check_path_range_invariant(&pr, pd.len()));
assert!(!check_path_tables_sound(&pr, &pd, &tr, &td, &dc, n));
}
#[test]
#[allow(clippy::identity_op)]
fn adversarial_path_range_e_past_data_caught() {
let (mut pr, pd, tr, td, dc, n) = small_chart_tables();
pr[1 * 4 + 2] = (0, 1, 99); // e past data_len
assert!(!check_path_range_invariant(&pr, pd.len()));
assert!(!check_path_tables_sound(&pr, &pd, &tr, &td, &dc, n));
}
#[test]
fn adversarial_path_data_id_oob_caught() {
let (pr, mut pd, tr, td, dc, n) = small_chart_tables();
pd[1] = 99; // state id past N_STATES
assert!(!check_state_ids_in_bounds(&pd, n));
assert!(!check_path_tables_sound(&pr, &pd, &tr, &td, &dc, n));
}
#[test]
fn adversarial_terminate_range_e_past_data_caught() {
let (pr, pd, mut tr, td, dc, n) = small_chart_tables();
tr[1] = (0, 99); // e past terminate_data_len
assert!(!check_terminate_range_invariant(&tr, td.len()));
assert!(!check_path_tables_sound(&pr, &pd, &tr, &td, &dc, n));
}
#[test]
fn adversarial_terminate_data_id_oob_caught() {
let (pr, pd, tr, mut td, dc, n) = small_chart_tables();
td[0] = 99;
assert!(!check_state_ids_in_bounds(&td, n));
assert!(!check_path_tables_sound(&pr, &pd, &tr, &td, &dc, n));
}
#[test]
fn adversarial_default_child_id_oob_caught() {
let (pr, pd, tr, td, mut dc, n) = small_chart_tables();
dc[0] = Some(99);
assert!(!check_default_child_in_bounds(&dc, n));
assert!(!check_path_tables_sound(&pr, &pd, &tr, &td, &dc, n));
}
#[test]
fn empty_tables_pass_trivially() {
// Single-state chart (just root, no transitions): all tables
// either empty or trivial.
assert!(check_path_tables_sound(
&[],
&[],
&[(0, 0)],
&[],
&[None],
1,
));
}
#[test]
fn the_const_eval_block_predicate_matches_the_validator() {
// The const-eval block emitted by hsmc-macros::codegen runs:
//
// assert!(s as usize <= m as usize, "...");
// assert!(m as usize <= e as usize, "...");
// assert!(e as usize <= __PATH_DATA.len(), "...");
//
// Translated: for every i, range[i] satisfies s ≤ m ≤ e ≤ len.
//
// The validator's #[ensures] clause says the same thing as a
// forall over Int. This test checks that on a representative
// input, the validator returns true exactly when the const-eval
// block's three assertions all pass — the same semantics.
let data_len = 10usize;
let cases: &[(u16, u16, u16, bool)] = &[
// (s, m, e, expected_pass)
(0, 0, 0, true),
(0, 5, 10, true),
(5, 5, 5, true),
(0, 0, 10, true),
(0, 10, 10, true),
(1, 0, 5, false), // s > m
(0, 6, 5, false), // m > e
(0, 5, 11, false), // e > len
];
for &(s, m, e, expected) in cases {
let const_eval_predicate = (s as usize) <= (m as usize)
&& (m as usize) <= (e as usize)
&& (e as usize) <= data_len;
let validator_result = check_path_range_invariant(&[(s, m, e)], data_len);
assert_eq!(
const_eval_predicate, expected,
"const-eval predicate disagrees with expectation for ({s}, {m}, {e})"
);
assert_eq!(
validator_result, expected,
"validator disagrees with expectation for ({s}, {m}, {e})"
);
assert_eq!(
const_eval_predicate, validator_result,
"const-eval predicate and validator diverge for ({s}, {m}, {e})"
);
}
}