The runtime `lca()` helper used a `heapless::Vec<u16,32>` ancestry-set
with a linear `contains()` per node — O(H²) and capped at H ≤ 32. The
codegened `__DEPTH` table already had everything needed for an O(H)
depth-walk with no allocation and no hierarchy ceiling. Switch to that.
Also adds an iai-callgrind dispatch bench harness (Linux-only dev-dep)
so future optimizations can be measured deterministically by instruction
count. Seven benches cover: cold start, lateral H=2/4/8, up, self, and a
self-emit chain. Baseline numbers checked in at `hsmc/benches/baseline.txt`.
The latency analysis (`docs/003. latency-analysis.md`) is rounded out
with event-entry-point and cooperative-driving audits — three new
sections documenting the four event injection paths, the run-loop's
cooperative shape, and three correctness invariants (sticky overflow
flag, biased-select trap, cancel-safety on durings).
Bench deltas (cargo bench --bench dispatch -- --baseline=pre_lca_fix):
h2_cold_start -1.9% / -0.3% (priming step, no lca() — noise)
h2_warm_lateral -22.8% / -22.1%
h4_cross_tree -25.9% / -10.6%
h4_up +1.0% / +0.4% (up-transition, no lca() — noise)
h4_self -21.5% / -11.7%
h8_cross_tree -46.2% / -41.0% ← headline: deepest LCA stress
chain_self_emit -15.4% / -10.4%
Improvement scales with hierarchy depth, exactly as the O(H²) → O(H)
algorithmic change would predict.
All tests pass under --no-default-features, --features tokio, and
--features embassy.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The codegen now emits one `__chart_observe!` invocation per observable
atom. The macro fans out at compile time to whichever sinks are enabled:
the in-memory journal (`feature = "journal"`), `defmt` (`trace-defmt`),
`log` (`trace-log`), and/or `tracing` (`trace-tracing`). Trace and
journal share the same vocabulary by construction — they cannot
diverge. With no sink feature on, every site expands to `()` (zero
overhead). Multiple trace backends now compose; previously they were
mutually exclusive.
Trace lines use a logfmt-style format with a `[statechart:Name]` prefix
and `key=value` pairs, machine-parseable and greppable. Twenty verbs
cover every observable atom — entries/exits with begin/end pairs,
actions with kind, durings, transitions with the reason that triggered
them, event lifecycle (received/delivered/dropped/queued/failed),
timers, and termination.
BREAKING CHANGES (chart syntax unchanged; observability surface only):
- `TraceEvent::TransitionFired` now carries `reason: TransitionReason`
showing whether the transition was driven by an event, a timer, or
internal logic.
- New `TraceEvent` variants for phase pairing: `EnterBegan`, `ExitBegan`,
`TransitionComplete`, `EventReceived`.
- Trace prefix changed from `[Name]` to `[statechart:Name]`.
- The chart-level `trace;` keyword is parsed for backwards compatibility
but no longer gates emission.
- `__chart_trace!` / `__chart_journal!` macros removed (doc-hidden).
Verification: 159 integration tests pass, 0 missed mutants, miri 68
tests clean, Creusot 14/14 VCs discharged. Zero overhead confirmed via
`cargo expand` — every observation site expands to `{}` with no sinks
enabled.
Phase 1 — semantics doc
docs/002. hsmc-semantics-formal.md
Phase 2 — deterministic execution journal
hsmc/src/journal.rs (TraceEvent, JournalSink, ActionKind)
hsmc-macros: __chart_journal! emission at every observable site
(entry/exit/action/transition/timer arm-cancel-fire/during/emit/
event delivery/terminate). Per-state during count helpers, stable
chart-hash via FNV-1a. Action observation moved out of run_action
and into call sites so ActionKind is accurate.
Public API on the generated machine: journal(), take_journal(),
clear_journal(), CHART_HASH.
Phase 3 — verification crate (Creusot scaffolding)
verification/{Cargo.toml,mise.toml,requirements.txt,INVARIANTS.md}
verification/src/{event_queue.rs,timer_table.rs} — Pearlite
contracts on simplified mirrors of the runtime types. cargo
creusot generates Coma IR cleanly; VCs not yet discharged.
Correspondence tests drive the verified mirror and the runtime
type with the same op sequences and assert observable parity.
Tests — 113 deterministic-flow tests across 22 files. Each compares a
hand-built expected journal byte-for-byte against actual, anchored
to a spec section: initial entry, lateral/self/up transitions,
bubbling, timers, emit, ordering, durings, step/dispatch
equivalence, root-targeting, current_state, termination.
Tooling — mise.toml (root): stable Rust + cargo subcommands.
verification/mise.toml: pinned nightly-2025-11-13 + opam + python
venv + uv. just verify is fully self-installing.
Bug fix — root state targetable by the chart's own name (e.g.
`on(Trig) => ChartName;`) per spec §"How transitions work".
CHART_HASH — stable FNV-1a fingerprint over the chart's structural
definition; mismatch on replay = different chart.
A transition whose target is already active (an ancestor of the
innermost active state) now unwinds only the subtree strictly below
the target. The target's entry/exit actions do not fire and its
default() does not re-descend — you cannot re-enter a state you never
left. The old behavior could loop infinitely when a child transitioned
to its own parent.
Self-transitions (target == innermost) and lateral transitions are
unchanged. See spec §2.6 and tests §T2.8 / T2.8b / T2.8c.
Also in this release:
* Full workspace justfile (check, test, coverage, mutants, pre-release)
* Unit tests covering all __private internals; `cargo mutants` now exits
clean (38 caught, 178 unviable, 0 missed, 0 timeouts).
* .config/nextest.toml with slow-timeout/terminate-after so hung tests
fail fast rather than wedging cargo-mutants runs.
BREAKING CHANGE: transition-to-ancestor semantics. Machines that relied
on the old re-entry behavior of up-transitions will observe different
exit/entry action sequences.
Hierarchical statechart codegen for Rust with:
- during: activities for state-scoped concurrent I/O
- field-list borrowing (split-borrow inside the run loop)
- embassy-first async with tokio support
- STATE_CHART const for tooling/inspection
- examples: microwave, microwave_tui, embassy_full, during_radio
swaitsandClaude Opus 4.7