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
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.
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.
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.
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.
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.
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.
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.
`default(...)` is now a transition with the same semantics as any
event-driven transition. It fires immediately after the declaring
state's entries finish and its durings start, applying the standard
exit-to-LCA / enter-to-target algorithm. Three behavioral changes
follow from this unification:
* Optional. A state with children is no longer required to declare a
`default(...)`. When omitted, the state itself is the resting
innermost active state; substates are reachable only via explicit
transitions. This is the "microwave Standby" pattern — Standby
has substates like LowPower that you enter only on demand, and
`=> Standby;` lands at Standby itself with no descent.
* Targets anywhere. The default target may be any state in the chart
— a child (the classic descent case), a sibling, an ancestor,
anywhere. `default(<sibling-or-ancestor>)` exits the just-entered
state as part of the default-fire transition; the same rule fires
whether you wrote it for descent, redirection, or up-bounce.
* Cycle-checked at compile time. The default-edge graph (out-degree
≤ 1 per node) is rejected if it contains any cycle, including
`default(self)`. `state A { default(A); }` and `A → B → A` chains
fail to compile with a pinpoint error message naming the cycle.
This guarantees default chains terminate at runtime.
Implementation:
* `validate.rs`: drop the "must be direct child" and "must have
children" restrictions; add `validate_default_graph` (iterative
three-color cycle detection via chain walk).
* `ir.rs`: keep the unresolved default ident through to
`resolve_transitions` so non-child targets resolve against the
global state-name map (the same map transition targets use).
* `codegen.rs`: precomputed `(from, to)` paths no longer fold default
descent into the enter slice — each path is LCA-relative
`(exit, enter)` ending exactly at the explicit target.
`descend_defaults` (a parent-pointer walk) is replaced by
`follow_defaults`, which fires real transitions through
`apply_path` and emits `TransitionFired{Internal}` /
`TransitionComplete` brackets per link. Up-transitions don't
trigger default-following (nothing was freshly entered, so no
state's default fires).
* `active_durings_per_innermost_state`: predicate widened to include
composites without a default (they can now be the innermost active
state, so any durings they declare must be raced when current).
BREAKING CHANGES:
* Journal format. Default-fires now emit `TransitionFired` (with
`reason: TransitionReason::Internal`) and `TransitionComplete`
brackets around their entry sequence. `Internal` was previously
reserved and never emitted; it is now active. Tests that
hand-build expected journal sequences must include these brackets
around every default-fire.
* Validation. `default(<non-child>)` and `default` on a childless
state previously raised compile-time errors. Both are now valid.
Code relying on these as guard rails must adapt.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Bump workspace version 0.4.0 → 0.4.1.
Patch release: dispatch hot-path performance only. No public API
changes; every chart that compiled against 0.4.0 compiles unchanged
and behaves identically. CHANGELOG.md captures the per-pass writeup
under the 0.4.1 heading.
Headlines (deepest dispatch in the bench suite):
h8_cross_tree -82% instructions / -72% cycles vs pre_lca_fix
bubble_top -22% instructions / -6% cycles vs handler walk
terminate_event -22% instructions / -23% cycles vs PARENT walk
The runtime LCA helper, is_up_transition, the per-call heapless::Vec
ancestry build, the runtime PARENT bubble walk, and (on timer-free
charts) the entire TimerTable machinery are all gone. Callgrind
reports the entire HSM machinery as a single inlined `step` symbol.
Bench suite expanded from 7 to 13 benches: bubble_leaf/mid/top
quantify handler resolution at varying ancestor depths,
timer_fire_dispatch covers the only path that exercises pop_expired's
non-empty branch, terminate_event covers do_terminate, and
bubble_cross_tree covers the realistic HSM worst case (deep bubble +
deep cross-tree transition).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Six codegen-side optimization passes against step() and friends. No
user-facing API changes; all 296 tests pass under no-default, tokio,
embassy, and tokio+journal. Cumulative on h8_cross_tree (deepest
dispatch in the suite): -82% instructions / -72% cycles vs the
pre_lca_fix baseline.
* __PATH_DATA + __PATH_RANGE: per-(from, to) precomputed exit/enter
sequences. Up/self/lateral semantics fold into one indexed lookup;
removes lca() and is_up_transition() runtime helpers and the
per-call heapless::Vec<u16, 16> ancestry build. Hierarchy depth no
longer bounded by Vec capacity.
* __DISPATCH[(state, event)]: precomputed handler resolution. The
runtime __PARENT bubble walk + per-hop __handler_lookup call in
step() collapses to one indexed lookup. Bubble resolution is now
O(1) regardless of depth -- bubble_top (4-hop) is within 3
instructions of bubble_leaf (handler on current).
__handler_lookup retained for timer dispatch.
* __TERMINATE_DATA: per-state precomputed exit chain (root inclusive
-- chart-root entry/exit actions are valid). do_terminate() indexes
the slice instead of walking __PARENT, and uses Deque::clear()
(O(1) in heapless 0.8) instead of pop_front-loop. terminate_event
bench: -22.5% instr / -23.4% cycles.
* TimerTable empty-skip: pop_expired / min_remaining / decrement /
cancel_state each get inlined is_empty() early-out with the
non-empty body marked #[cold].
* Codegen-static timer-machinery elide: when chart has no Duration
triggers, every TimerTable call is omitted from step() and
exit_state(). step() returns None directly. dispatch_trigger and
the timer-fired arms remain but are unreachable; LLVM DCEs them.
* TimerEntry.remaining_ns: u128 -> u64 (~584-year ceiling). Halves
entry size; replaces u128 saturating-sub with u64. The smaller
machine struct improves cache density on every bench, even
timer-free ones.
Bench coverage: four new benches added to cover paths the original
suite missed -- bubble_leaf/mid/top (handler resolution at varying
ancestor depths), timer_fire_dispatch (only bench exercising
pop_expired's non-empty branch and dispatch_trigger), terminate_event
(only bench exercising do_terminate), bubble_cross_tree (deep bubble
+ 10-state cross-tree, the realistic HSM worst case).
See hsmc/benches/baseline.txt for the per-pass delta blocks and
docs/003. latency-analysis.md sections 1, 9, and 12 for the
cost-surface analysis.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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.
Bump workspace version 0.2.0 → 0.3.0.
CHANGELOG: documents the additions in this release —
- `journal` Cargo feature with full TraceEvent enum + machine API
- root state targetable by chart name
- 113 deterministic-flow tests
- verification/ workspace member with mechanical Creusot proofs
- docs/002 formal semantics doc
- README "How a chart behaves" building-block section
- mise + just tooling overhaul (set shell, set script-interpreter)
README: integrates the semantics from docs/002 as eight building-
block rules that build on each other (active path, default-descent,
event bubbling, transitions, up-transition rule, entry/exit
ordering, timer lifecycle, emit / during / termination). Adds an
explicit "what hsmc deliberately does NOT have" table with what to
use instead. New "Verification" section pointing at `just verify`.
No behavior changes for v0.1 / v0.2 charts — every existing chart
compiles unchanged.
Make `just verify` actually invoke Why3 + alt-ergo + z3 against every
Pearlite VC, and fix the mutant + miri pipelines along the way.
Verification crate
- Drop the const-generic CAP types for EventQueue / TimerTable.
Mirror with std::vec::Vec, whose creusot-std specs carry the
proof burden. Capacity behavior is exercised by the runtime's
own unit tests + correspondence tests.
- View impls are #[logic(open)] over a pub field so contracts on
push/pop/etc. can see the link to the inner Vec's @ view.
- 14/14 VCs discharge: EventQueue {new, push, pop, is_empty, len,
clear, Default}; TimerTable {new, len, is_empty, Default};
Entry derives.
- `cargo creusot prove --no-cache` always runs the SMT solvers;
`time` shows ~7s CPU on ~1.2s wall-clock = real parallel work.
Tooling
- verification/mise.toml pins nightly-2025-11-13 + rust-src,
rustc-dev, llvm-tools-preview, rustfmt; declares opam, python,
uv, and the project-local .venv. Inherits root mise.toml's just
+ cargo-* tools.
- just verify clones creusot v0.9.0 to ~/.local/share/hsmc-verify/
and runs the canonical ./INSTALL — that's the only way the
bundled prelude-generator + creusot-rustc actually build.
- just verify --no-cache forces SMT re-runs every time.
- Drop bespoke pin/install of cargo-creusot from mise.toml; the
cargo backend goes through cargo-binstall which can't pin a
multi-bin git workspace at a tag.
Mutants — was missing every JournalSink mutant
- Recipe runs with --features tokio,journal so journal_* and det_*
tests (gated on both) actually execute.
- Add clear_journal_empties_the_journal test in journal_smoke.rs
to kill the JournalSink::clear with-() mutant.
- Remove dead JournalSink::len + is_empty (called nowhere; only
existed as mutation-bait).
Result: 0 missed, 42 caught, 211 unviable (proc-macro emitted
code that mutants can't standalone-compile).
Miri — was hitting the trybuild glob isolation issue
- --exclude hsmc-macros (trybuild ui test isn't UB-relevant)
- --exclude hsmc-verification (different pinned toolchain)
- 66 tests pass under Miri, 0 UB.
Gitignore
- /verif/, /why3find.json, /.why3find/, **/.venv/ — all
regenerated by `just verify`. Repo stays clean of per-machine
prover timings + venv artifacts.
Misc
- Fix root-state targetability: `on(Trig) => <ChartName>;` resolves
to root id 0 in both ir.rs::resolve_transitions and
validate.rs's separate name_map.
- `set shell` and `set script-interpreter` route every justfile
recipe through `mise exec`, so all subshells see the right
Rust + opam + cargo-* tools regardless of how `just` was
invoked. No shebangs anywhere.
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.
Add LICENSE-MIT and LICENSE-APACHE at workspace root and in each member package so the dual MIT OR Apache-2.0 license ships in the published .crate.
Fill in publish metadata (authors, repository, homepage, readme, keywords, categories) across the workspace and both members.
Add CHANGELOG.md with a 0.1.0 initial release entry.
Fix clippy lints: unused enumerate index, collapsible if, Default impls for TimerTable, SimRadio, and Ctx, use RangeInclusive::contains.
Exclude examples/microwave_tui.rs from the published package. The file stays in-tree but has known unawaited async log futures that need a dedicated pass before it ships.
Apply cargo fmt across the workspace.
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
swaits
