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.
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.
`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>
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.
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
