diff --git a/.gitignore b/.gitignore index 04eb9d8..16a5a18 100644 --- a/.gitignore +++ b/.gitignore @@ -9,6 +9,13 @@ mutation_history.json *.profraw +# Creusot output: cargo-creusot dumps `.coma` (Coma IR) files here for +# Why3 to read. Regenerated on every `just verify` run. +/verif/ + +# Project-local Python venv created by mise's `_.python.venv` config. +**/.venv/ + # Local Claude Code config (per-host overrides) .claude/settings.local.json diff --git a/Cargo.lock b/Cargo.lock index c247fb0..ab93644 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -8,6 +8,18 @@ version = "0.2.21" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923" +[[package]] +name = "autocfg" +version = "1.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" + +[[package]] +name = "bitflags" +version = "1.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" + [[package]] name = "bitflags" version = "2.11.1" @@ -55,6 +67,25 @@ dependencies = [ "static_assertions", ] +[[package]] +name = "creusot-std" +version = "0.9.0" +source = "git+https://github.com/creusot-rs/creusot?tag=v0.9.0#fd089be0e96442f5e71605fbb129e6d6f7b264f3" +dependencies = [ + "creusot-std-proc", + "num-rational", +] + +[[package]] +name = "creusot-std-proc" +version = "0.9.0" +source = "git+https://github.com/creusot-rs/creusot?tag=v0.9.0#fd089be0e96442f5e71605fbb129e6d6f7b264f3" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "critical-section" version = "1.2.0" @@ -67,7 +98,7 @@ version = "0.28.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "829d955a0bb380ef178a640b91779e3987da38c9aea133b20614cfed8cdea9c6" dependencies = [ - "bitflags", + "bitflags 2.11.1", "crossterm_winapi", "futures-core", "mio", @@ -121,6 +152,47 @@ dependencies = [ "syn", ] +[[package]] +name = "defmt" +version = "0.3.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f0963443817029b2024136fc4dd07a5107eb8f977eaf18fcd1fdeb11306b64ad" +dependencies = [ + "defmt 1.0.1", +] + +[[package]] +name = "defmt" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "548d977b6da32fa1d1fda2876453da1e7df63ad0304c8b3dae4dbe7b96f39b78" +dependencies = [ + "bitflags 1.3.2", + "defmt-macros", +] + +[[package]] +name = "defmt-macros" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d4fc12a85bcf441cfe44344c4b72d58493178ce635338a3f3b78943aceb258e" +dependencies = [ + "defmt-parser", + "proc-macro-error2", + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "defmt-parser" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "10d60334b3b2e7c9d91ef8150abfb6fa4c1c39ebbcf4a81c2e346aad939fee3e" +dependencies = [ + "thiserror", +] + [[package]] name = "document-features" version = "0.2.12" @@ -394,14 +466,17 @@ name = "hsmc" version = "0.2.0" dependencies = [ "crossterm", + "defmt 0.3.100", "embassy-futures", "embassy-sync", "embassy-time", "futures", "heapless 0.8.0", "hsmc-macros", + "log", "ratatui", "tokio", + "tracing", "trybuild", ] @@ -416,6 +491,14 @@ dependencies = [ "trybuild", ] +[[package]] +name = "hsmc-verification" +version = "0.2.0" +dependencies = [ + "creusot-std", + "hsmc", +] + [[package]] name = "ident_case" version = "1.0.1" @@ -544,6 +627,45 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8d5439c4ad607c3c23abf66de8c8bf57ba8adcd1f129e699851a6e43935d339d" +[[package]] +name = "num-bigint" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9" +dependencies = [ + "num-integer", + "num-traits", +] + +[[package]] +name = "num-integer" +version = "0.1.46" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f" +dependencies = [ + "num-traits", +] + +[[package]] +name = "num-rational" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f83d14da390562dca69fc84082e73e548e1ad308d24accdedd2720017cb37824" +dependencies = [ + "num-bigint", + "num-integer", + "num-traits", +] + +[[package]] +name = "num-traits" +version = "0.2.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" +dependencies = [ + "autocfg", +] + [[package]] name = "parking_lot" version = "0.12.5" @@ -579,6 +701,28 @@ version = "0.2.17" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" +[[package]] +name = "proc-macro-error-attr2" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "96de42df36bb9bba5542fe9f1a054b8cc87e172759a1868aa05c1f3acc89dfc5" +dependencies = [ + "proc-macro2", + "quote", +] + +[[package]] +name = "proc-macro-error2" +version = "2.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "11ec05c52be0a07b08061f7dd003e7d7092e0472bc731b4af7bb1ef876109802" +dependencies = [ + "proc-macro-error-attr2", + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "proc-macro2" version = "1.0.106" @@ -603,7 +747,7 @@ version = "0.28.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fdef7f9be5c0122f890d58bdf4d964349ba6a6161f705907526d891efabba57d" dependencies = [ - "bitflags", + "bitflags 2.11.1", "cassowary", "compact_str", "crossterm", @@ -624,7 +768,7 @@ version = "0.5.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ed2bf2547551a7053d6fdfafda3f938979645c44812fbfcda098faae3f1a362d" dependencies = [ - "bitflags", + "bitflags 2.11.1", ] [[package]] @@ -633,7 +777,7 @@ version = "0.38.44" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "fdb5bc1ae2baa591800df16c9ca78619bf65c0488b41b96ccec5d11220d8c154" dependencies = [ - "bitflags", + "bitflags 2.11.1", "errno", "libc", "linux-raw-sys", @@ -818,6 +962,26 @@ dependencies = [ "winapi-util", ] +[[package]] +name = "thiserror" +version = "2.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "2.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + [[package]] name = "tokio" version = "1.52.0" @@ -878,6 +1042,22 @@ version = "1.1.1+spec-1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "756daf9b1013ebe47a8776667b466417e2d4c5679d441c26230efd9ef78692db" +[[package]] +name = "tracing" +version = "0.1.44" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "63e71662fa4b2a2c3a26f570f037eb95bb1f85397f3cd8076caed2f026a6d100" +dependencies = [ + "pin-project-lite", + "tracing-core", +] + +[[package]] +name = "tracing-core" +version = "0.1.36" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "db97caf9d906fbde555dd62fa95ddba9eecfd14cb388e4f491a66d74cd5fb79a" + [[package]] name = "trybuild" version = "1.0.116" diff --git a/Cargo.toml b/Cargo.toml index 254bf99..5e101b2 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [workspace] resolver = "2" -members = ["hsmc", "hsmc-macros"] +members = ["hsmc", "hsmc-macros", "verification"] [workspace.package] version = "0.2.0" diff --git a/docs/002. hsmc-semantics-formal.md b/docs/002. hsmc-semantics-formal.md new file mode 100644 index 0000000..3ae05e5 --- /dev/null +++ b/docs/002. hsmc-semantics-formal.md @@ -0,0 +1,371 @@ +# `hsmc` — How Your Chart Behaves + +**Status:** DRAFT. This is the canonical answer to "what will my statechart +actually do?" When this document and another disagree, this one wins. + +**Audience:** anyone writing a chart. The goal is that after reading this, +you can predict every action call, transition, and timer fire just by +looking at your `statechart!` block. + +--- + +## Why `hsmc` is small (read this first) + +`hsmc` ships the minimum set of useful statechart primitives. No guard +conditions, no orthogonal/parallel regions, no history states, no deferred +events, no internal transitions, no state-local context. + +The bet is on **simple, consistent semantics**. The small surface area +makes hsmc easy to use, easy to reason about, and easy to predict. Once +you internalize a small set of rules, every edge case below just follows +from them — you don't have to memorize anything new. + +--- + +## What a chart contains + +Each primitive, in roughly the order a developer first meets them. + +- **State** — a named node. The root state (the machine itself) is just a + state. Every state is just a state. +- **Nested state** — a state inside another state. Same thing as a state. +- **Entry action** — a function called once when a state is entered. +- **Exit action** — a function called once when a state is exited. +- **Transition** — exits one state and enters another, anywhere else in the + chart. Walks from the current state up to the lowest common ancestor + (LCA) of source and target, calling exits along the way, then walks down + to the target, calling entries along the way. +- **Action (without transition)** — a function call attached to a trigger. + No state change. That's it. +- **Default child** — every non-leaf state declares one default child. + Whenever a state with children is entered, the default child is entered + immediately after that state's entry actions finish — it's effectively + an automatic transition into the child. +- **Trigger: event vs. duration** — an event is a variant of your event + enum. A duration is a timer (`after Duration` fires once, `every + Duration` fires repeatedly). Triggers attach to transitions and to + actions. Timers and events are dispatched slightly differently — see + the bubbling rules below. +- **`emit()`** — pushes an event onto the machine's queue from inside an + action. The event is dispatched after the current event has fully + finished processing. No re-entrant dispatch. +- **`during:` activity** — a cancellable async function. Started **after** + the entry actions of its owning state finish; cancelled **before** the + exit actions of that state begin to run when the state is left. +- **`terminate`** — names an event that, when received, exits the entire + active path bottom-up and shuts the machine down. Only valid at root. + +--- + +## Where the machine "is" + +At any moment, the machine is in a path of states from root down to one +innermost state. If you're in `C` inside `B` inside `A` (which is inside +the root), then you are simultaneously in **all** of `Root`, `A`, `B`, and +`C`. The root is always active until the machine terminates. + +This is the most important rule in this document. Every other rule below +is downstream of it. **You are simultaneously in every state on the path +from the root to the innermost active state.** If a rule somewhere else +seems weird, come back to this one — it's probably the resolution. + +`current_state()` returns the innermost active state, which is usually a +leaf, but can be a composite (a state with children) if you got there via +an up-transition (see below) and haven't moved since. + +--- + +## How events are handled + +Event comes in. Start at the innermost active state. Does it have a +handler for this event? If yes, that handler runs and the event is +consumed — no further handling. + +If no, walk up to the parent. Repeat. If you walk all the way to the root +and still nothing handles it, the event is silently discarded. + +That's all. Three other things follow from this rule: + +- A handler on a leaf state shadows a handler on its ancestor for the same + event. The leaf wins because the search starts there. +- If a single state has multiple handlers (actions and/or a transition) + for the same trigger, the actions fire in declaration order, then the + transition fires last. +- Timer triggers do **not** bubble. A timer belongs to the state that + declared it; it fires only in that state's scope. Events bubble; timers + don't. + +--- + +## How transitions work + +The current state (for transition purposes) is the innermost active state. +The target can be **any** state in the entire chart — there's a global +namespace, so state names must be unique across the chart. + +The root state is targetable too: it's named after the chart itself. So +in `statechart! { Foo { ... } }`, an `on(Trig) => Foo;` is a valid +transition whose target is the root. From any state inside the chart this +is an up-transition (root is always on the active path) — exiting only +the states strictly between current and root, with no entry actions and +no default-descent on root. Use this when you want to wind everything +back up to the chart's own scope. + +To run a transition: + +1. Find the LCA of current and target. (They might share a parent; they + might both be on the same root-to-leaf path; the LCA is always defined + because the root is always an upper bound.) +2. Walk **up** from the current state, exiting each state on the way + (cancel durings → run exit actions) until you hit the LCA. The LCA + itself is **not** exited. +3. Walk **down** from the LCA to the target, entering each state on the + way (run entry actions → start durings). The LCA is **not** re-entered. +4. If the target has children, follow the default-child chain down to a + leaf, entering each as you go. + +The three flavors below are just three relationships between current and +target. The same algorithm covers all of them — they only look different +in which steps fire. + +### Transitioning to a sibling (or anywhere not on your active path) + +The standard case. LCA is somewhere strictly above both current and +target. Exit up to LCA, enter down to target, default-descend if the +target has children. Already covered above. + +### Transitioning to yourself + +Self-transition: target equals the innermost active state. The standard +transition algorithm above gives the clean answer: the LCA of the target +with itself is its parent, so we exit only the target and re-enter only +the target. **Nothing above the target is exited or re-entered.** + +Concrete example. Active path is `Root → SomeState → SomeOtherState`. A +transition fires whose target is `SomeOtherState`. + +- Exit `SomeOtherState` (cancel durings, run exits). +- Re-enter `SomeOtherState` (run entries, start durings). +- `SomeState` is **never** exited, **never** re-entered, **never** + touched. Its timers and durings keep running. + +Timers declared on the target restart, because the target itself was +exited and re-entered. + +If the target happens to be a composite (it has children, but no child is +active right now because you got there via an up-transition), the same +default-child rule still applies on re-entry: exit the composite, re-enter +it, then descend through its default chain. Self-transitions don't add a +new rule — they're just the case where source and target are the same +state. + +Personally I don't find self-transitions all that valuable, but people +talk about them all the time, so they're supported. + +### Transitioning to one of your parents (the important one) + +The case to internalize. When you transition to an ancestor of the +current state, you exit the current state and any states between, but you +do **not** re-enter the ancestor. You were already there. + +- The ancestor's entry actions don't fire. +- The ancestor's `default` is not followed. +- The ancestor's timers don't restart. +- The ancestor's durings keep running. + +You cannot enter a state you never left. Spelling it out: starting from +leaf `C` inside `B` inside `A`, a transition to `A` exits `C` then `B`, +and now `A` is the innermost active state with no active child. + +--- + +## Timers + +- A timer starts when its state is entered. +- A timer is cancelled when its state is exited. +- Descending into a child state is **not** an exit — the parent's timers + keep running. +- Timers don't bubble. Only the state that declared the timer handles its + expiry. +- Re-entering a state restarts its timers. + +If two timers happen to expire on the same `step()` tick — rare under +real wall-clock timing, but possible at `step()` granularity since +`step()` decrements all timers at once — the runtime today fires the +*oldest* (longest-armed) timer first, because it sits earlier in the +active-timers array. **Don't depend on this.** It's a likely outcome of +the current implementation, not a contract. If two timers must fire in a +specific order, model them as one timer plus an explicit `emit()` chain. + +--- + +## Entry and exit ordering + +Putting it all together: + +- **Entry** runs **outer-to-inner**: when entering a path of states, the + outermost state's entry actions fire first, then its child's, and so on + down to the innermost. Within a single state, entry actions fire in + declaration order. After entry actions of a state finish, that state's + durings start. Then the default child (if any) is entered, recursively. +- **Exit** runs **inner-to-outer**: when leaving a path of states, the + innermost state exits first, then its parent, and so on up. Within a + single state, exit actions fire in declaration order. Before exit + actions of a state begin, that state's durings are cancelled. + +So a full transition reads top-to-bottom as: cancel durings on the way +out → run exits on the way out → run entries on the way in → start +durings on the way in. + +--- + +## `emit()` — sending events from inside an action + +An action can call `self.emit(Ev)`. The event goes on the machine's +internal queue. It is **not** processed immediately. The runtime finishes +handling whatever event it's currently handling — including every entry +and exit action of any transition — and only then dequeues `Ev` and +dispatches it normally. No re-entrant dispatch. + +Once the current handler finishes, the runtime drains anything queued +during handling before sleeping or returning to the outer loop. + +If the queue is full, `emit()` returns `Err(QueueFull)`. Subsequent +actions in the same chain still run; they may attempt further emits, but +those also fail. At end of tick, the runtime surfaces `Err(QueueFull)` +out of `step()` / `run()` so the top-level driver can react. A queue +overflow is a hard signal that something is wrong with sizing or with the +producer; it is never silently swallowed. + +--- + +## `during:` activities — async work scoped to a state + +A `during:` is an async function that runs while its owning state is on +the active path. It is started after the entry actions of that state +finish, and it is cancelled before the exit actions of that state begin. + +A during's future may be **dropped at any `.await` point** — when an +external event arrives, when a timer fires, when another during on the +same active path completes, or when a transition leaves the during's +state. This is the Rust async concept of *cancellation*: the future is +not given a chance to "finish gracefully" — it's dropped, and dropping +runs whatever destructors `Drop` impls have, but no further `.await`s +will ever resume. + +The practical rule: write durings as cancel-safe state machines. Every +`.await` must be a clean resume point where dropping the future leaves +the borrowed fields in a re-enterable state. Don't straddle awaits with +mutations that need to commit atomically. If you need to learn what +cancel-safety looks like in practice, the README has the worked examples, +and the tokio docs on cancellation are the standard reference. + +Multiple `during:` declarations on the same active path race against each +other (and against incoming events and timers). Each during borrows +disjoint `&mut` slices of the context — Rust's split-borrow checker +rejects overlapping borrows at compile time, so concurrent durings can +never step on each other's state. + +--- + +## Termination + +When a `terminate` event is received, the machine exits the entire active +path bottom-up: innermost first, then each parent, up to and including +the root. After that, the machine is done — `is_terminated()` is true, +`run()` returns `Ok(())`, further `step()` calls are no-ops returning +`None`. Any pending events in the queue are dropped. Any in-flight +durings are dropped at their next `.await`. + +Once you adopt the simple, consistent semantics above, this just falls +out — termination is "exit everything you're currently in, in the usual +exit order, then stop." + +--- + +## `step()` vs `run()` vs `dispatch()` + +Three ways to drive the machine. Same underlying behavior; the differences +are about who decides when to advance time. + +- **`step(elapsed)`** — synchronous. You call it; it does at most one unit + of work (one timer expiry, or one queued event). For bare-metal / + testing. +- **`dispatch(ev).await`** — async helper. Pushes `ev` onto the queue, then + drains the queue (and any timers that come due) until quiescent. For + injecting events from the same task that owns the machine. +- **`run().await`** — async. Owns the task body. Races durings against the + external event channel and timers, and processes whatever wins, in a + loop, until termination. + +For the same external event sequence and the same elapsed-time inputs, +the three produce the same observable trace. + +--- + +## What you cannot do, and why + +The "minimum useful primitives" bet, made concrete. For each missing +feature: why we don't have it, and what to do instead. _(First-pass +drafts. Edit freely.)_ + +- **Guard conditions on transitions** — _Why not:_ guards bury control + flow inside an action body, so the chart's structure stops telling you + the whole story. _What to do instead:_ split the source into two + states whose entry conditions differ, or have an action emit a + follow-up event (`Ok` vs. `Bad`) and let the chart branch on that. +- **Orthogonal / parallel regions** — _Why not:_ true parallelism + multiplies state-space and forces a join-semantics for shared events. + _What to do instead:_ run two charts as two tasks and connect them with + channels, or use multiple `during:` activities for concurrent async + work within a single state. +- **History states (shallow or deep)** — _Why not:_ history is hidden + mutable state — re-entering a parent goes "somewhere" based on + invisible bookkeeping. _What to do instead:_ store the last child + explicitly in your context, then transition directly to it on + re-entry. +- **Deferred events** — _Why not:_ deferring means an event you sent now + can resurface much later, with non-obvious ordering. _What to do + instead:_ handle the event where it arrives (even if just to log and + drop it), or have the producer check state before sending. +- **Internal transitions** — _Why not:_ "transition that doesn't exit or + enter" is a separate semantics layer just to skip exit/entry. _What to + do instead:_ declare an `action(Trig) => fn` (no transition). That's + exactly what an internal transition is. +- **State-local context** — _Why not:_ hierarchical context types make + borrowing painful and tie the chart's structure into your data model. + _What to do instead:_ put all your state in the root context; + `during:` activities can borrow disjoint fields of it. +- **Event priorities beyond FIFO** — _Why not:_ priorities allow + starvation and make ordering implementation-dependent. FIFO is + predictable. _What to do instead:_ if some events are higher-priority, + deliver them on a separate channel into a separate, faster-cadence + machine. +- **Runtime statechart modification** — _Why not:_ the chart is the + static structural definition. Mutating it at runtime defeats + compile-time validation and makes the trace meaningless. _What to do + instead:_ design every variation up front as states or sub-states. +- **Inter-machine communication primitives** — _Why not:_ a built-in + messaging layer would have to pick winners between embassy / tokio / + bare-metal channels. _What to do instead:_ use whatever channel + primitive your runtime gives you (embassy `Channel`, tokio `mpsc`), + and feed events into `dispatch()` or `Sender::send()`. + +--- + +## Quick reference + +| Scenario | What fires | +| ------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| Initial machine start | Root entries → default-descend down through each child's entries → durings start at each entered state. | +| Transition to sibling | Exit current up to LCA (cancel durings, run exits) → enter from LCA down to target (run entries, start durings) → default-descend if target has children. | +| Transition to self | Exit innermost (cancel durings, run exits), re-enter innermost (run entries, start durings). Timers restart. If innermost has children, default-descend after re-entry. | +| Transition to ancestor | Exit current up to (but not including) the ancestor. No entry actions. No default-descent. Ancestor's durings and timers continue. | +| Transition into a state with children | After the target's entries fire, default-descend through each default child's entries down to a leaf. | +| Timer fires | The declaring state's handler runs (timers don't bubble). | +| Event with no handler | Silently discarded. | +| Event handled at innermost | Innermost state's handler runs (actions in declaration order, then transition if any). | +| Event handled at ancestor | Search bubbles up; first ancestor with a handler runs it. Innermost is still innermost; transition (if any) starts from innermost. | +| Action calls `emit()` | Event queued. Dispatched after the current event's handling fully completes. | +| Queue is full when `emit()` is called | `emit()` returns `Err(QueueFull)`. Remaining actions in the same chain still run; further emits in this tick also fail. `step()` / `run()` surfaces `QueueFull` at end of tick. | +| `terminate` event delivered | Exit innermost → … → exit root. Pending events dropped. Durings dropped. `run()` returns `Ok(())`. | diff --git a/hsmc-macros/src/codegen.rs b/hsmc-macros/src/codegen.rs index 2cc4744..759efca 100644 --- a/hsmc-macros/src/codegen.rs +++ b/hsmc-macros/src/codegen.rs @@ -7,6 +7,94 @@ use syn::Ident; use crate::ir::{HandlerKindIr, Ir, TriggerIr, VariantKind}; use crate::parse::{During, PayloadKind}; +/// FNV-1a 64-bit hash of a chart's structural fingerprint. Stable across +/// rebuilds of the same chart definition; differs whenever any structural +/// element (state name, action name, transition target, default child, +/// timer trigger, event variant) changes. +/// +/// Used as `::CHART_HASH` so a journal recorded for one chart can +/// be rejected at replay time when the chart definition has drifted. +fn compute_chart_hash(ir: &Ir) -> u64 { + const FNV_OFFSET: u64 = 0xcbf2_9ce4_8422_2325; + const FNV_PRIME: u64 = 0x0000_0100_0000_01b3; + let mut h: u64 = FNV_OFFSET; + let mut feed = |bytes: &[u8]| { + for &b in bytes { + h ^= b as u64; + h = h.wrapping_mul(FNV_PRIME); + } + h ^= 0xff; + h = h.wrapping_mul(FNV_PRIME); + }; + feed(ir.name.to_string().as_bytes()); + for s in &ir.states { + feed(&s.id.to_le_bytes()); + feed(s.name.to_string().as_bytes()); + feed(&[s.parent.unwrap_or(u16::MAX).to_le_bytes()[0], s.parent.unwrap_or(u16::MAX).to_le_bytes()[1]]); + feed(&s.depth.to_le_bytes()); + feed(&s.default_child.unwrap_or(u16::MAX).to_le_bytes()); + for &aid in &s.entries { feed(&aid.to_le_bytes()); } + feed(&[0xee]); // separator: entries → exits + for &aid in &s.exits { feed(&aid.to_le_bytes()); } + feed(&[0xff]); // separator: exits → handlers + for h_ir in &s.handlers { + match &h_ir.trigger { + TriggerIr::Event(id, ident, _) => { + feed(&[0x01]); + feed(&id.to_le_bytes()); + feed(ident.to_string().as_bytes()); + } + TriggerIr::Duration(id) => { + feed(&[0x02]); + feed(&id.to_le_bytes()); + } + } + match &h_ir.kind { + HandlerKindIr::Transition(name, slot) => { + feed(&[0x10]); + feed(name.to_string().as_bytes()); + feed(&slot.unwrap_or(u16::MAX).to_le_bytes()); + } + HandlerKindIr::Action(aid, name) => { + feed(&[0x11]); + feed(&aid.to_le_bytes()); + feed(name.to_string().as_bytes()); + } + } + } + feed(&[0xfe]); // separator: handlers → timers + for &t in &s.owned_timers { feed(&t.to_le_bytes()); } + feed(&[0xfd]); // separator: timers → durings + feed(&(s.durings.len() as u16).to_le_bytes()); + } + feed(&[0xfc]); // separator: states → actions + for a in &ir.actions { + feed(a.name.to_string().as_bytes()); + feed(&(a.params.len() as u16).to_le_bytes()); + } + feed(&[0xfb]); // separator: actions → events + for e in &ir.event_variants { + feed(e.name.to_string().as_bytes()); + } + h +} + +/// Emit a single trace call routed through the hsmc-internal dispatcher +/// (`::hsmc::__chart_trace!`), or nothing if the chart didn't declare +/// `trace;`. The dispatcher picks the actual backend (defmt / log / +/// tracing / no-op) based on which `hsmc/trace-*` cargo feature the +/// user enabled in their `Cargo.toml` — no extra wiring required. +/// +/// Zero-overhead when `trace_enabled` is false: generates an empty +/// TokenStream so the compiler sees no extra work at the call site. +fn emit_trace_call(trace_enabled: bool, args: TokenStream) -> TokenStream { + if trace_enabled { + quote! { ::hsmc::__chart_trace!(#args); } + } else { + TokenStream::new() + } +} + /// For each user-declared leaf state that has one or more `during:` activities /// active (either declared on it, on any ancestor, or on root), return its /// state id and the flattened list of durings in leaf-first order. Durings @@ -406,6 +494,9 @@ pub fn generate(ir: &Ir) -> TokenStream { let n_dur_triggers = ir.duration_triggers.len(); let max_timers = n_dur_triggers.max(1); + let chart_hash = compute_chart_hash(ir); + let chart_hash_lit = quote! { #chart_hash }; + // Public state enum — only user-declared states (skip __Root). let state_variants: Vec<_> = ir .states @@ -433,6 +524,233 @@ pub fn generate(ir: &Ir) -> TokenStream { }) .collect(); + // Per-id name lookups, only emitted when the chart opted into tracing. + // Chart-name string is reused at every trace site as a literal. + let chart_name_lit = ir.name.to_string(); + let state_name_arms: Vec<_> = ir + .states + .iter() + .map(|s| { + let sid = s.id; + let nm = s.name.to_string(); + quote! { #sid => #nm, } + }) + .collect(); + let action_name_arms: Vec<_> = ir + .actions + .iter() + .enumerate() + .map(|(i, a)| { + let aid = i as u16; + let nm = a.name.to_string(); + quote! { #aid => #nm, } + }) + .collect(); + let trace_helpers = if ir.trace_enabled { + quote! { + #[inline(always)] + #[doc(hidden)] + fn __state_name(sid: u16) -> &'static str { + match sid { + #(#state_name_arms)* + _ => "", + } + } + #[inline(always)] + #[doc(hidden)] + fn __action_name(aid: u16) -> &'static str { + match aid { + #(#action_name_arms)* + _ => "", + } + } + } + } else { + TokenStream::new() + }; + // ── Observation hook snippets ───────────────────────────────────── + // + // Trace and journal want the same call sites: enter, exit, action, + // transition. We emit a single `observe_*` snippet per site that + // contains BOTH the trace call (gated on `ir.trace_enabled` at + // parse time, may also be no-op'd by the trace-* feature gate) and + // the journal call (gated on the `journal` cargo feature inside the + // macro). Either gate independently produces zero overhead when off. + // + // Journal-only sites (timers, durings, emits, event dispatch, + // termination) get plain `journal_*` snippets — trace doesn't have + // a string format for them. + + // Trace-side primitives, recreated here so each observe_* snippet + // can splice them in. + let trace_enter_call = emit_trace_call( + ir.trace_enabled, + quote! { enter #chart_name_lit, Self::__state_name(sid) }, + ); + let trace_exit_call = emit_trace_call( + ir.trace_enabled, + quote! { exit #chart_name_lit, Self::__state_name(sid) }, + ); + let trace_action_call = emit_trace_call( + ir.trace_enabled, + quote! { action #chart_name_lit, Self::__action_name(aid) }, + ); + let trace_transition_call = emit_trace_call( + ir.trace_enabled, + quote! { + transition #chart_name_lit, + self.current.map(Self::__state_name).unwrap_or(""), + Self::__state_name(target) + }, + ); + + let observe_started = quote! { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::Started { chart_hash: Self::CHART_HASH } + ); + }; + let observe_entered = quote! { + #trace_enter_call + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::Entered { state: sid } + ); + }; + let observe_exited = quote! { + #trace_exit_call + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::Exited { state: sid } + ); + }; + let observe_action_entry = quote! { + #trace_action_call + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::ActionInvoked { + state: sid, + action: aid, + kind: ::hsmc::ActionKind::Entry, + } + ); + }; + let observe_action_exit = quote! { + #trace_action_call + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::ActionInvoked { + state: sid, + action: aid, + kind: ::hsmc::ActionKind::Exit, + } + ); + }; + let observe_action_handler = quote! { + #trace_action_call + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::ActionInvoked { + state: __handler_state, + action: aid, + kind: ::hsmc::ActionKind::Handler, + } + ); + }; + let observe_transition = quote! { + #trace_transition_call + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::TransitionFired { + from: self.current, + to: target, + } + ); + }; + let observe_event_delivered = quote! { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::EventDelivered { + handler_state: __handler_state, + event: __ev_id, + } + ); + }; + let observe_event_dropped = quote! { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::EventDropped { event: __ev_id } + ); + }; + let observe_timer_armed = quote! { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::TimerArmed { + state: sid, + timer: tid, + ns: __duration_for(tid).as_nanos() as u64, + } + ); + }; + let observe_timer_cancelled = quote! { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::TimerCancelled { state: sid, timer: tid } + ); + }; + let observe_timer_fired = quote! { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::TimerFired { state: __t_state, timer: __t_trigger } + ); + }; + let observe_terminated = quote! { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::Terminated + ); + }; + let observe_terminate_requested = quote! { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::TerminateRequested { event: __ev_id } + ); + }; + + // Per-state during count, used to emit DuringStarted/Cancelled + // events one per declared during in the state. + let durings_count_arms: Vec = ir + .states + .iter() + .map(|s| { + let sid = s.id; + let n = s.durings.len() as u16; + quote! { #sid => #n, } + }) + .collect(); + let observe_durings_started = quote! { + let __dn = Self::__durings_count(sid); + let mut __di: u16 = 0; + while __di < __dn { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::DuringStarted { state: sid, during: __di } + ); + __di += 1; + } + }; + let observe_durings_cancelled = quote! { + let __dn = Self::__durings_count(sid); + let mut __di: u16 = 0; + while __di < __dn { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::DuringCancelled { state: sid, during: __di } + ); + __di += 1; + } + }; + let parent_table = ir .states .iter() @@ -1412,6 +1730,7 @@ pub fn generate(ir: &Ir) -> TokenStream { ctx: &'a mut #ctx_ty, __queue: &'a mut (dyn ::hsmc::__private::QueuePush<#ev_ty> + ::core::marker::Send), __terminated: &'a bool, + __journal: &'a mut ::hsmc::__private::JournalSink, } #[doc = #ctx_alias_doc] @@ -1432,9 +1751,23 @@ pub fn generate(ir: &Ir) -> TokenStream { /// [`HsmcError::QueueFull`] if the queue is full, or /// [`HsmcError::AlreadyTerminated`] if the machine is shutting /// down. + #[allow(unused_variables)] pub fn emit(&mut self, event: #ev_ty) -> ::core::result::Result<(), ::hsmc::HsmcError> { if *self.__terminated { return Err(::hsmc::HsmcError::AlreadyTerminated); } - self.__queue.push(event) + let __ev_id = __event_to_id(&event); + let __result = self.__queue.push(event); + if __result.is_ok() { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::EmitQueued { event: __ev_id } + ); + } else { + ::hsmc::__chart_journal!( + self.__journal, + ::hsmc::TraceEvent::EmitFailed { event: __ev_id } + ); + } + __result } /// Convenience wrapper around [`emit()`](Self::emit) that panics on @@ -1454,6 +1787,9 @@ pub fn generate(ir: &Ir) -> TokenStream { timers: ::hsmc::__private::TimerTable<#max_timers>, terminated: bool, __overflow: bool, + /// Deterministic execution journal. ZST when the `hsmc/journal` + /// feature is off; a `Vec` when on. + __journal: ::hsmc::__private::JournalSink, #tokio_fields #embassy_fields } @@ -1556,6 +1892,7 @@ pub fn generate(ir: &Ir) -> TokenStream { timers: ::hsmc::__private::TimerTable::new(), terminated: false, __overflow: false, + __journal: ::hsmc::__private::JournalSink::new(), #tokio_ctor #embassy_ctor }; @@ -1599,6 +1936,41 @@ pub fn generate(ir: &Ir) -> TokenStream { /// Mutably borrow the user-provided context (extension beyond spec §4.4; provided for test convenience). pub fn context_mut(&mut self) -> &mut #ctx_ty { &mut self.ctx } + /// Borrow the deterministic execution journal. Only available + /// under `feature = "journal"`. Returns the in-order sequence + /// of every observable atom — entries, exits, action calls, + /// during start/cancel, timer arm/cancel/fire, queued emits, + /// event delivery, transitions, and termination. + #[cfg(feature = "journal")] + pub fn journal(&self) -> &[::hsmc::TraceEvent] { + self.__journal.events() + } + + /// Take and clear the deterministic execution journal. Useful + /// at test boundaries to compare against an expected sequence + /// without lingering events from earlier runs. + #[cfg(feature = "journal")] + pub fn take_journal(&mut self) -> ::hsmc::Journal { + self.__journal.take() + } + + /// Drop all journal events without returning them. + #[cfg(feature = "journal")] + pub fn clear_journal(&mut self) { + self.__journal.clear(); + } + + /// Stable identifier for this chart's structural definition. + /// A different `CHART_HASH` means the chart is a different + /// machine — replay against a journal recorded for a + /// different `CHART_HASH` is meaningless and the test driver + /// should refuse to compare. + pub const CHART_HASH: u64 = #chart_hash_lit; + + /// Returns `CHART_HASH` (instance-method form for symmetry + /// with other introspection methods). + pub const fn chart_hash(&self) -> u64 { Self::CHART_HASH } + /// Advance the machine by `elapsed` wall-clock time. Returns the /// duration until the next timer fires, or `None` if the machine /// has no live timers (§4.4). @@ -1607,10 +1979,12 @@ pub fn generate(ir: &Ir) -> TokenStream { /// because action methods are `async fn` and must be `.await`ed /// during dispatch. Under default features it stays sync. #[cfg(not(any(feature = "tokio", feature = "embassy")))] + #[allow(unused_variables)] pub fn step(&mut self, elapsed: ::hsmc::Duration) -> Option<::hsmc::Duration> { if self.terminated { return None; } if self.current.is_none() { + #observe_started self.enter_path(0); return self.timers.min_remaining(); } @@ -1618,12 +1992,15 @@ pub fn generate(ir: &Ir) -> TokenStream { self.timers.decrement(elapsed); if let Some((state, trig)) = self.timers.pop_expired(&__DEPTH) { - // Re-arm repeating timers before dispatch. If the - // handler transitions out of `state`, the state's exit - // path will cancel the freshly-armed timer. + let __t_state = state; + let __t_trigger = trig; + #observe_timer_fired if __duration_repeats(trig) { let d = __duration_for(trig); self.timers.start(state, trig, d); + let sid = state; + let tid = trig; + #observe_timer_armed } self.dispatch_trigger(state, 1, trig); return self.timers.min_remaining(); @@ -1631,19 +2008,30 @@ pub fn generate(ir: &Ir) -> TokenStream { if let Some(ev) = self.queue.pop_front() { if matches!(__check_terminate(&ev), TerminateCheck::Yes) { + let __ev_id = __event_to_id(&ev); + #observe_terminate_requested self.do_terminate(); return None; } - let eid = __event_to_id(&ev); - if eid != u16::MAX { - let mut cur = self.current; - while let Some(s) = cur { - if let Some((actions, target)) = __handler_lookup(s, 0, eid) { + let __ev_id = __event_to_id(&ev); + if __ev_id != u16::MAX { + let mut __cur = self.current; + let mut __delivered = false; + while let Some(s) = __cur { + if let Some((actions, target)) = __handler_lookup(s, 0, __ev_id) { + let __handler_state = s; + #observe_event_delivered self.run_handlers(s, actions, target, Some(&ev)); + __delivered = true; break; } - cur = __PARENT[s as usize]; + __cur = __PARENT[s as usize]; } + if !__delivered { + #observe_event_dropped + } + } else { + #observe_event_dropped } return self.timers.min_remaining(); } @@ -1652,10 +2040,12 @@ pub fn generate(ir: &Ir) -> TokenStream { } #[cfg(any(feature = "tokio", feature = "embassy"))] + #[allow(unused_variables)] pub async fn step(&mut self, elapsed: ::hsmc::Duration) -> Option<::hsmc::Duration> { if self.terminated { return None; } if self.current.is_none() { + #observe_started self.enter_path(0).await; return self.timers.min_remaining(); } @@ -1663,9 +2053,15 @@ pub fn generate(ir: &Ir) -> TokenStream { self.timers.decrement(elapsed); if let Some((state, trig)) = self.timers.pop_expired(&__DEPTH) { + let __t_state = state; + let __t_trigger = trig; + #observe_timer_fired if __duration_repeats(trig) { let d = __duration_for(trig); self.timers.start(state, trig, d); + let sid = state; + let tid = trig; + #observe_timer_armed } self.dispatch_trigger(state, 1, trig).await; return self.timers.min_remaining(); @@ -1673,19 +2069,30 @@ pub fn generate(ir: &Ir) -> TokenStream { if let Some(ev) = self.queue.pop_front() { if matches!(__check_terminate(&ev), TerminateCheck::Yes) { + let __ev_id = __event_to_id(&ev); + #observe_terminate_requested self.do_terminate().await; return None; } - let eid = __event_to_id(&ev); - if eid != u16::MAX { - let mut cur = self.current; - while let Some(s) = cur { - if let Some((actions, target)) = __handler_lookup(s, 0, eid) { + let __ev_id = __event_to_id(&ev); + if __ev_id != u16::MAX { + let mut __cur = self.current; + let mut __delivered = false; + while let Some(s) = __cur { + if let Some((actions, target)) = __handler_lookup(s, 0, __ev_id) { + let __handler_state = s; + #observe_event_delivered self.run_handlers(s, actions, target, Some(&ev)).await; + __delivered = true; break; } - cur = __PARENT[s as usize]; + __cur = __PARENT[s as usize]; } + if !__delivered { + #observe_event_dropped + } + } else { + #observe_event_dropped } return self.timers.min_remaining(); } @@ -1730,6 +2137,7 @@ pub fn generate(ir: &Ir) -> TokenStream { } #[cfg(not(any(feature = "tokio", feature = "embassy")))] + #[allow(unused_variables)] fn run_handlers( &mut self, source_state: u16, @@ -1737,7 +2145,9 @@ pub fn generate(ir: &Ir) -> TokenStream { target: Option, event: Option<&#ev_ty>, ) { + let __handler_state = source_state; for &aid in actions { + #observe_action_handler self.run_action(aid, event); if self.terminated { return; } } @@ -1747,6 +2157,7 @@ pub fn generate(ir: &Ir) -> TokenStream { } #[cfg(any(feature = "tokio", feature = "embassy"))] + #[allow(unused_variables)] async fn run_handlers( &mut self, source_state: u16, @@ -1754,7 +2165,9 @@ pub fn generate(ir: &Ir) -> TokenStream { target: Option, event: Option<&#ev_ty>, ) { + let __handler_state = source_state; for &aid in actions { + #observe_action_handler self.run_action(aid, event).await; if self.terminated { return; } } @@ -1765,6 +2178,11 @@ pub fn generate(ir: &Ir) -> TokenStream { #[cfg(not(any(feature = "tokio", feature = "embassy")))] fn run_action(&mut self, aid: u16, event: Option<&#ev_ty>) { + // Trace + journal emission for action calls now happens at + // the call sites (`#observe_action_entry`, + // `#observe_action_exit`, `#observe_action_handler`) so the + // ActionKind tag and call-site state id can be recorded + // accurately. `run_action` itself is just dispatch. let ctx = &mut self.ctx; let mut __proxy = ::hsmc::__private::EmitProxy { queue: &mut self.queue, @@ -1772,10 +2190,12 @@ pub fn generate(ir: &Ir) -> TokenStream { }; let queue: &mut (dyn ::hsmc::__private::QueuePush<#ev_ty> + ::core::marker::Send) = &mut __proxy; let terminated = &self.terminated; + let journal = &mut self.__journal; let mut actx = #action_ctx_name { ctx, __queue: queue, __terminated: terminated, + __journal: journal, }; fn __dispatch( ctx: &mut Ctx, @@ -1793,6 +2213,7 @@ pub fn generate(ir: &Ir) -> TokenStream { #[cfg(any(feature = "tokio", feature = "embassy"))] async fn run_action(&mut self, aid: u16, event: Option<&#ev_ty>) { + // See sync run_action above — observation happens at call sites. let ctx = &mut self.ctx; let mut __proxy = ::hsmc::__private::EmitProxy { queue: &mut self.queue, @@ -1800,10 +2221,12 @@ pub fn generate(ir: &Ir) -> TokenStream { }; let queue: &mut (dyn ::hsmc::__private::QueuePush<#ev_ty> + ::core::marker::Send) = &mut __proxy; let terminated = &self.terminated; + let journal = &mut self.__journal; let mut actx = #action_ctx_name { ctx, __queue: queue, __terminated: terminated, + __journal: journal, }; async fn __dispatch( ctx: &mut Ctx, @@ -1840,6 +2263,7 @@ pub fn generate(ir: &Ir) -> TokenStream { #[cfg(not(any(feature = "tokio", feature = "embassy")))] fn transition(&mut self, _source_matched_state: u16, target: u16) { + #observe_transition if Self::is_up_transition(self.current, target) { if let Some(mut cur) = self.current { while cur != target { @@ -1886,6 +2310,7 @@ pub fn generate(ir: &Ir) -> TokenStream { #[cfg(any(feature = "tokio", feature = "embassy"))] async fn transition(&mut self, _source_matched_state: u16, target: u16) { + #observe_transition if Self::is_up_transition(self.current, target) { if let Some(mut cur) = self.current { while cur != target { @@ -1958,31 +2383,41 @@ pub fn generate(ir: &Ir) -> TokenStream { } #[cfg(not(any(feature = "tokio", feature = "embassy")))] + #[allow(unused_variables)] fn enter_state_no_descent(&mut self, sid: u16) { + #observe_entered let entries = Self::entries_of(sid); for &aid in entries { + #observe_action_entry self.run_action(aid, None); if self.terminated { return; } } for &tid in __owned_timers(sid) { let d = __duration_for(tid); self.timers.start(sid, tid, d); + #observe_timer_armed } self.current = Some(sid); + #observe_durings_started } #[cfg(any(feature = "tokio", feature = "embassy"))] + #[allow(unused_variables)] async fn enter_state_no_descent(&mut self, sid: u16) { + #observe_entered let entries = Self::entries_of(sid); for &aid in entries { + #observe_action_entry self.run_action(aid, None).await; if self.terminated { return; } } for &tid in __owned_timers(sid) { let d = __duration_for(tid); self.timers.start(sid, tid, d); + #observe_timer_armed } self.current = Some(sid); + #observe_durings_started } #[cfg(not(any(feature = "tokio", feature = "embassy")))] @@ -2004,23 +2439,39 @@ pub fn generate(ir: &Ir) -> TokenStream { } #[cfg(not(any(feature = "tokio", feature = "embassy")))] + #[allow(unused_variables)] fn exit_state(&mut self, sid: u16) { + // Per spec §"Entry and exit ordering": + // 1. cancel durings 2. cancel timers 3. exit actions 4. Exited + #observe_durings_cancelled + for &tid in __owned_timers(sid) { + #observe_timer_cancelled + } self.timers.cancel_state(sid); let exits = Self::exits_of(sid); for &aid in exits { + #observe_action_exit self.run_action(aid, None); if self.terminated { return; } } + #observe_exited } #[cfg(any(feature = "tokio", feature = "embassy"))] + #[allow(unused_variables)] async fn exit_state(&mut self, sid: u16) { + #observe_durings_cancelled + for &tid in __owned_timers(sid) { + #observe_timer_cancelled + } self.timers.cancel_state(sid); let exits = Self::exits_of(sid); for &aid in exits { + #observe_action_exit self.run_action(aid, None).await; if self.terminated { return; } } + #observe_exited } fn entries_of(sid: u16) -> &'static [u16] { @@ -2035,6 +2486,16 @@ pub fn generate(ir: &Ir) -> TokenStream { _ => &[], } } + #[doc(hidden)] + #[allow(unused_variables)] + fn __durings_count(sid: u16) -> u16 { + match sid { + #(#durings_count_arms)* + _ => 0, + } + } + + #trace_helpers #[cfg(not(any(feature = "tokio", feature = "embassy")))] fn do_terminate(&mut self) { @@ -2050,6 +2511,7 @@ pub fn generate(ir: &Ir) -> TokenStream { self.terminated = true; self.current = None; while self.queue.pop_front().is_some() {} + #observe_terminated } #[cfg(any(feature = "tokio", feature = "embassy"))] @@ -2066,6 +2528,7 @@ pub fn generate(ir: &Ir) -> TokenStream { self.terminated = true; self.current = None; while self.queue.pop_front().is_some() {} + #observe_terminated } #[cfg(not(any(feature = "tokio", feature = "embassy")))] diff --git a/hsmc-macros/src/ir.rs b/hsmc-macros/src/ir.rs index cc61922..0fe5f08 100644 --- a/hsmc-macros/src/ir.rs +++ b/hsmc-macros/src/ir.rs @@ -26,6 +26,11 @@ pub struct Ir { /// Duration triggers referenced anywhere, in first-seen order. /// Each one gets a trigger id used by the timer table. pub duration_triggers: Vec, + /// True when the chart declared `trace;` at root. Codegen routes + /// trace calls to `::hsmc::__chart_trace!`, which dispatches to a + /// backend (defmt / log / tracing / no-op) based on the user's + /// `hsmc/trace-*` feature selection in their `Cargo.toml`. + pub trace_enabled: bool, } pub struct ActionIr { @@ -122,6 +127,7 @@ pub fn build_ir(input: StatechartInput) -> syn::Result { } }; let terminate_event = root_body.terminate.as_ref().map(|(i, _)| i.clone()); + let trace_enabled = root_body.trace_enabled; let mut ir = Ir { name, @@ -133,6 +139,7 @@ pub fn build_ir(input: StatechartInput) -> syn::Result { actions: Vec::new(), event_variants: Vec::new(), duration_triggers: Vec::new(), + trace_enabled, }; // Two passes: collect the set of declared state names first so @@ -140,6 +147,9 @@ pub fn build_ir(input: StatechartInput) -> syn::Result { // (transition) or a handler fn (action) based on the declared set. let mut state_names = std::collections::HashSet::new(); collect_state_names(&root_body, &mut state_names); + // Per spec: the root state is just a state, named after the chart. + // `on(...) => ;` must classify as a transition to root. + state_names.insert(ir.name.to_string()); let name_span = ir.name.span(); let root_name = Ident::new("__Root", name_span); @@ -152,6 +162,13 @@ pub fn build_ir(input: StatechartInput) -> syn::Result { ); lower_body(&mut ir, root_id, &root_body, true, &state_names)?; + // Intern the terminate event variant so the journal can record it + // by id (otherwise `__event_to_id` returns u16::MAX for the very + // event that triggered shutdown, which is useless for replay). + if let Some(t_ident) = ir.terminate_event.clone() { + let _ = intern_event(&mut ir, &t_ident, None)?; + } + Ok(ir) } @@ -495,6 +512,12 @@ pub fn resolve_transitions(ir: &mut Ir) -> syn::Result<()> { name_map.insert(s.name.to_string(), s.id); } } + // Per spec: the root state is targetable as a transition destination + // by the chart's own name. Find the root (parent is None) and map + // `` → root_id. + if let Some(root) = ir.states.iter().find(|s| s.parent.is_none()) { + name_map.insert(ir.name.to_string(), root.id); + } let n = ir.states.len(); for i in 0..n { diff --git a/hsmc-macros/src/parse.rs b/hsmc-macros/src/parse.rs index 8371348..3b16433 100644 --- a/hsmc-macros/src/parse.rs +++ b/hsmc-macros/src/parse.rs @@ -28,6 +28,13 @@ pub struct StateBody { /// split borrow on the generated `select` call site; the macro emits a /// clearer error when it can detect overlap at expansion time. pub durings: Vec, + /// `trace;` — root-only flag. When set, codegen injects calls to + /// `::hsmc::__chart_trace!(...)` at every state entry, state exit, + /// action dispatch, and transition. The runtime backend (defmt / + /// log / tracing / no-op) is selected by which `hsmc/trace-*` cargo + /// feature the user enables in their `Cargo.toml`. Off by default, + /// fully zero-cost when off. + pub trace_enabled: bool, } impl StateBody { @@ -45,6 +52,7 @@ impl StateBody { handlers: Vec::new(), children: Vec::new(), durings: Vec::new(), + trace_enabled: false, } } } @@ -196,6 +204,23 @@ fn parse_body(input: ParseStream, is_root: bool) -> syn::Result { } body.event_ty = Some(ty); } + "trace" => { + let _: Ident = input.parse()?; + input.parse::()?; + if !is_root { + return Err(syn::Error::new( + ident.span(), + "`trace;` is only valid at root", + )); + } + if body.trace_enabled { + return Err(syn::Error::new( + ident.span(), + "duplicate `trace;` declaration", + )); + } + body.trace_enabled = true; + } "entry" => { let _: Ident = input.parse()?; input.parse::()?; diff --git a/hsmc-macros/src/validate.rs b/hsmc-macros/src/validate.rs index 4829e36..93fff48 100644 --- a/hsmc-macros/src/validate.rs +++ b/hsmc-macros/src/validate.rs @@ -25,12 +25,17 @@ pub fn validate(ir: &Ir) -> syn::Result<()> { // Resolve transitions: done already? We need post-build resolution. // We'll do it here because we need IR mutable; but we're given &Ir. // Instead perform target lookup inline. - let name_map: HashMap = ir + let mut name_map: HashMap = ir .states .iter() .filter(|s| s.name != "__Root") .map(|s| (s.name.to_string(), s.id)) .collect(); + // Per spec: the root state is targetable as a transition destination + // by the chart's own name. + if let Some(root) = ir.states.iter().find(|s| s.parent.is_none()) { + name_map.insert(ir.name.to_string(), root.id); + } for s in &ir.states { // Empty state (not root). A state with a `during:` is not empty — diff --git a/hsmc-macros/tests/ui/t10_1_during_duplicate_field.stderr b/hsmc-macros/tests/ui/t10_1_during_duplicate_field.stderr index 17db22b..b52e1fb 100644 --- a/hsmc-macros/tests/ui/t10_1_during_duplicate_field.stderr +++ b/hsmc-macros/tests/ui/t10_1_during_duplicate_field.stderr @@ -3,15 +3,3 @@ error: field `a` listed twice in `during: tick(...)` — each field can only be | 19 | during: tick(a, a); | ^ - -error[E0405]: cannot find trait `MActions` in this scope - --> tests/ui/t10_1_during_duplicate_field.rs:26:6 - | -26 | impl MActions for MActionContext<'_> {} - | ^^^^^^^^ not found in this scope - -error[E0425]: cannot find type `MActionContext` in this scope - --> tests/ui/t10_1_during_duplicate_field.rs:26:19 - | -26 | impl MActions for MActionContext<'_> {} - | ^^^^^^^^^^^^^^ not found in this scope diff --git a/hsmc-macros/tests/ui/t10_2_during_overlap_same_state.stderr b/hsmc-macros/tests/ui/t10_2_during_overlap_same_state.stderr index b53f117..a17af96 100644 --- a/hsmc-macros/tests/ui/t10_2_during_overlap_same_state.stderr +++ b/hsmc-macros/tests/ui/t10_2_during_overlap_same_state.stderr @@ -3,15 +3,3 @@ error: field `a` is borrowed by two concurrent durings on state `S` (`one` and ` | 21 | during: two(a); | ^ - -error[E0405]: cannot find trait `MActions` in this scope - --> tests/ui/t10_2_during_overlap_same_state.rs:29:6 - | -29 | impl MActions for MActionContext<'_> {} - | ^^^^^^^^ not found in this scope - -error[E0425]: cannot find type `MActionContext` in this scope - --> tests/ui/t10_2_during_overlap_same_state.rs:29:19 - | -29 | impl MActions for MActionContext<'_> {} - | ^^^^^^^^^^^^^^ not found in this scope diff --git a/hsmc-macros/tests/ui/t9_1_duplicate_transition.stderr b/hsmc-macros/tests/ui/t9_1_duplicate_transition.stderr index 3796bc7..6ebb6b3 100644 --- a/hsmc-macros/tests/ui/t9_1_duplicate_transition.stderr +++ b/hsmc-macros/tests/ui/t9_1_duplicate_transition.stderr @@ -4,18 +4,6 @@ error: duplicate transition on trigger `Go` in state `Red` 15 | on(Go) => Yellow; | ^^ -error[E0405]: cannot find trait `MActions` in this scope - --> tests/ui/t9_1_duplicate_transition.rs:22:6 - | -22 | impl MActions for MActionContext<'_> { - | ^^^^^^^^ not found in this scope - -error[E0425]: cannot find type `MActionContext` in this scope - --> tests/ui/t9_1_duplicate_transition.rs:22:19 - | -22 | impl MActions for MActionContext<'_> { - | ^^^^^^^^^^^^^^ not found in this scope - warning: unused import: `Duration` --> tests/ui/t9_1_duplicate_transition.rs:1:24 | diff --git a/hsmc-macros/tests/ui/t9_2_missing_default.stderr b/hsmc-macros/tests/ui/t9_2_missing_default.stderr index 84a6784..3655622 100644 --- a/hsmc-macros/tests/ui/t9_2_missing_default.stderr +++ b/hsmc-macros/tests/ui/t9_2_missing_default.stderr @@ -3,15 +3,3 @@ error: state `Parent` has children but no `default` declaration | 13 | state Parent { | ^^^^^^ - -error[E0405]: cannot find trait `MActions` in this scope - --> tests/ui/t9_2_missing_default.rs:20:6 - | -20 | impl MActions for MActionContext<'_> { - | ^^^^^^^^ not found in this scope - -error[E0425]: cannot find type `MActionContext` in this scope - --> tests/ui/t9_2_missing_default.rs:20:19 - | -20 | impl MActions for MActionContext<'_> { - | ^^^^^^^^^^^^^^ not found in this scope diff --git a/hsmc-macros/tests/ui/t9_3_terminate_in_child.stderr b/hsmc-macros/tests/ui/t9_3_terminate_in_child.stderr index 33f31ea..88e5919 100644 --- a/hsmc-macros/tests/ui/t9_3_terminate_in_child.stderr +++ b/hsmc-macros/tests/ui/t9_3_terminate_in_child.stderr @@ -3,15 +3,3 @@ error: `terminate` is only valid at the root level | 14 | terminate(Halt); | ^^^^^^^^^ - -error[E0405]: cannot find trait `MActions` in this scope - --> tests/ui/t9_3_terminate_in_child.rs:20:6 - | -20 | impl MActions for MActionContext<'_> { - | ^^^^^^^^ not found in this scope - -error[E0425]: cannot find type `MActionContext` in this scope - --> tests/ui/t9_3_terminate_in_child.rs:20:19 - | -20 | impl MActions for MActionContext<'_> { - | ^^^^^^^^^^^^^^ not found in this scope diff --git a/hsmc-macros/tests/ui/t9_4_default_non_child.stderr b/hsmc-macros/tests/ui/t9_4_default_non_child.stderr index 367bee9..8124bac 100644 --- a/hsmc-macros/tests/ui/t9_4_default_non_child.stderr +++ b/hsmc-macros/tests/ui/t9_4_default_non_child.stderr @@ -3,15 +3,3 @@ error: `default(Cousin)` in state `Parent`: `Cousin` is not a direct child of `P | 14 | default(Cousin); | ^^^^^^^ - -error[E0405]: cannot find trait `MActions` in this scope - --> tests/ui/t9_4_default_non_child.rs:21:6 - | -21 | impl MActions for MActionContext<'_> { - | ^^^^^^^^ not found in this scope - -error[E0425]: cannot find type `MActionContext` in this scope - --> tests/ui/t9_4_default_non_child.rs:21:19 - | -21 | impl MActions for MActionContext<'_> { - | ^^^^^^^^^^^^^^ not found in this scope diff --git a/hsmc-macros/tests/ui/t9_5_default_childless.stderr b/hsmc-macros/tests/ui/t9_5_default_childless.stderr index cf124bd..45acaba 100644 --- a/hsmc-macros/tests/ui/t9_5_default_childless.stderr +++ b/hsmc-macros/tests/ui/t9_5_default_childless.stderr @@ -3,15 +3,3 @@ error: `default` in state `Leaf` which has no child states | 14 | default(Ghost); | ^^^^^^^ - -error[E0405]: cannot find trait `MActions` in this scope - --> tests/ui/t9_5_default_childless.rs:20:6 - | -20 | impl MActions for MActionContext<'_> { - | ^^^^^^^^ not found in this scope - -error[E0425]: cannot find type `MActionContext` in this scope - --> tests/ui/t9_5_default_childless.rs:20:19 - | -20 | impl MActions for MActionContext<'_> { - | ^^^^^^^^^^^^^^ not found in this scope diff --git a/hsmc-macros/tests/ui/t9_6_empty_state.stderr b/hsmc-macros/tests/ui/t9_6_empty_state.stderr index 35ddd4e..2d1c33c 100644 --- a/hsmc-macros/tests/ui/t9_6_empty_state.stderr +++ b/hsmc-macros/tests/ui/t9_6_empty_state.stderr @@ -3,15 +3,3 @@ error: empty state `Empty` | 14 | state Empty {} | ^^^^^ - -error[E0405]: cannot find trait `MActions` in this scope - --> tests/ui/t9_6_empty_state.rs:18:6 - | -18 | impl MActions for MActionContext<'_> { - | ^^^^^^^^ not found in this scope - -error[E0425]: cannot find type `MActionContext` in this scope - --> tests/ui/t9_6_empty_state.rs:18:19 - | -18 | impl MActions for MActionContext<'_> { - | ^^^^^^^^^^^^^^ not found in this scope diff --git a/hsmc-macros/tests/ui/t9_7_duplicate_default.stderr b/hsmc-macros/tests/ui/t9_7_duplicate_default.stderr index 26c97b7..4853f6d 100644 --- a/hsmc-macros/tests/ui/t9_7_duplicate_default.stderr +++ b/hsmc-macros/tests/ui/t9_7_duplicate_default.stderr @@ -3,15 +3,3 @@ error: multiple `default` declarations in state `Parent` | 14 | default(A); | ^^^^^^^ - -error[E0405]: cannot find trait `MActions` in this scope - --> tests/ui/t9_7_duplicate_default.rs:22:6 - | -22 | impl MActions for MActionContext<'_> { - | ^^^^^^^^ not found in this scope - -error[E0425]: cannot find type `MActionContext` in this scope - --> tests/ui/t9_7_duplicate_default.rs:22:19 - | -22 | impl MActions for MActionContext<'_> { - | ^^^^^^^^^^^^^^ not found in this scope diff --git a/hsmc-macros/tests/ui/t9_8_unknown_target.stderr b/hsmc-macros/tests/ui/t9_8_unknown_target.stderr index bd500d1..47d4650 100644 --- a/hsmc-macros/tests/ui/t9_8_unknown_target.stderr +++ b/hsmc-macros/tests/ui/t9_8_unknown_target.stderr @@ -35,6 +35,24 @@ warning: unexpected `cfg` condition value: `embassy` = note: see for more information about checking conditional configuration = note: this warning originates in the macro `statechart` (in Nightly builds, run with -Z macro-backtrace for more info) +warning: unexpected `cfg` condition value: `journal` + --> tests/ui/t9_8_unknown_target.rs:8:1 + | + 8 | / statechart! { + 9 | | M { +10 | | context: Ctx; +11 | | events: Ev; +... | +17 | | } + | |_^ + | + = note: no expected values for `feature` + = note: using a cfg inside a macro will use the cfgs from the destination crate and not the ones from the defining crate + = help: try referring to `statechart` crate for guidance on how handle this unexpected cfg + = help: the macro `statechart` may come from an old version of the `hsmc_macros` crate, try updating your dependency with `cargo update -p hsmc_macros` + = note: see for more information about checking conditional configuration + = note: this warning originates in the macro `statechart` (in Nightly builds, run with -Z macro-backtrace for more info) + error[E0046]: not all trait items implemented, missing: `NonExistent` --> tests/ui/t9_8_unknown_target.rs:19:1 | diff --git a/hsmc-macros/tests/ui/t9_9_multiple_terminate.stderr b/hsmc-macros/tests/ui/t9_9_multiple_terminate.stderr index 2d4e12b..731b5a0 100644 --- a/hsmc-macros/tests/ui/t9_9_multiple_terminate.stderr +++ b/hsmc-macros/tests/ui/t9_9_multiple_terminate.stderr @@ -3,15 +3,3 @@ error: multiple `terminate` declarations | 13 | terminate(Halt); | ^^^^^^^^^ - -error[E0405]: cannot find trait `MActions` in this scope - --> tests/ui/t9_9_multiple_terminate.rs:19:6 - | -19 | impl MActions for MActionContext<'_> { - | ^^^^^^^^ not found in this scope - -error[E0425]: cannot find type `MActionContext` in this scope - --> tests/ui/t9_9_multiple_terminate.rs:19:19 - | -19 | impl MActions for MActionContext<'_> { - | ^^^^^^^^^^^^^^ not found in this scope diff --git a/hsmc/Cargo.toml b/hsmc/Cargo.toml index 2e28b1d..1c980bb 100644 --- a/hsmc/Cargo.toml +++ b/hsmc/Cargo.toml @@ -17,6 +17,22 @@ exclude = ["examples/microwave_tui.rs"] default = [] tokio = ["dep:tokio"] embassy = ["dep:embassy-sync", "dep:embassy-time", "dep:embassy-futures"] +# Auto-tracing backends — pick at most one. When the user opts a chart +# into `trace;`, the macro emits calls to an internal dispatcher that +# routes to whichever backend is enabled here. With NO backend feature +# enabled, `trace;` is a no-op (zero overhead). Enabling more than one +# backend produces a duplicate-macro compile error — that's intentional. +trace-defmt = ["dep:defmt"] +trace-log = ["dep:log"] +trace-tracing = ["dep:tracing"] +# Journaling backend. When enabled, the macro emits calls into an +# in-memory journal recording every observable atom: entries, exits, +# action invocations, during start/cancel, timer arm/cancel/fire, emits, +# event delivery, transitions, and termination. Used to make charts +# replay-deterministic and to catch semantic regressions in CI. +# Requires `alloc` (the journal grows dynamically). Off by default — +# zero overhead and no `alloc` requirement when not enabled. +journal = [] [dependencies] hsmc-macros = { path = "../hsmc-macros", version = "0.2.0" } @@ -25,6 +41,9 @@ tokio = { version = "1", features = ["sync", "time", "rt", "macros"], optional = embassy-sync = { version = "0.8", optional = true } embassy-time = { version = "0.5", optional = true } embassy-futures = { version = "0.1", optional = true } +defmt = { version = "0.3", optional = true } +log = { version = "0.4", optional = true } +tracing = { version = "0.1", default-features = false, optional = true } [target.'cfg(any(target_os = "linux", target_os = "macos", target_os = "windows"))'.dev-dependencies] trybuild = "1" diff --git a/hsmc/src/journal.rs b/hsmc/src/journal.rs new file mode 100644 index 0000000..1da5418 --- /dev/null +++ b/hsmc/src/journal.rs @@ -0,0 +1,115 @@ +//! Deterministic execution journal for `hsmc` charts. +//! +//! Behind `feature = "journal"`. The macro emits one [`TraceEvent`] for every +//! observable atom in chart execution: entries, exits, action invocations, +//! during start/cancel, timer arm/cancel/fire, queued emits, event delivery, +//! transitions, and termination. +//! +//! For a fixed `(chart, initial context, external event sequence, +//! elapsed-time inputs)`, the produced journal is byte-identical across runs +//! — that's the contract the verification harness checks against. +//! +//! All identifiers in the journal are stable u16 indices generated at macro +//! expansion time. Each chart also exposes: +//! +//! - `::CHART_HASH: u64` — identifies the chart definition; mismatch +//! on replay = different chart. +//! - `::state_name(id)`, `::action_name(id)`, +//! `::event_name(id)`, `::timer_label(id)` — human-readable +//! names for debugging. +//! +//! The journal does not record `during:` race outcomes from `run()` — race +//! winners depend on wall-clock timing and are not part of the deterministic +//! contract (see semantics doc). What you see in the journal is the *result* +//! of any race: the event the winning during emitted. + +extern crate alloc; +pub(crate) use alloc::vec::Vec; + +/// Owned journal returned by `take_journal()`. A `Vec` whose +/// concrete crate (`alloc::vec::Vec`) is hidden so callers don't need an +/// `extern crate alloc` of their own. +pub type Journal = alloc::vec::Vec; + +/// Distinguishes which kind of slot an action was invoked in. Pure metadata +/// — the action body is the same regardless. Lets the journal be readable +/// without cross-referencing surrounding events. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub enum ActionKind { + /// Entry action of a state. + Entry, + /// Exit action of a state. + Exit, + /// Handler action (action attached to a transition or standalone + /// `action(...) => fn`). + Handler, +} + +/// One observable atom of chart execution. The macro emits these at every +/// hook point so the full sequence can be journaled and compared. +/// +/// Variants carry stable u16 indices, never strings. Serialization (binary +/// or JSON) of these values is reproducible across rebuilds. +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +pub enum TraceEvent { + /// First event in any journal. Identifies the chart definition. + Started { chart_hash: u64 }, + /// A state's entry begins. Followed by `ActionInvoked{Entry}` for each + /// of that state's entry actions, then `DuringStarted` for each during + /// declared on the state, then potentially the next state's `Entered` + /// (default-descent). + Entered { state: u16 }, + /// A state's exit completed. Preceded by `DuringCancelled` for each + /// during on the state, followed by `ActionInvoked{Exit}` for each + /// exit action. + Exited { state: u16 }, + /// An action function was called. + ActionInvoked { + state: u16, + action: u16, + kind: ActionKind, + }, + /// A `during:` activity became logically active for its owning state. + /// Index is the state-local declaration order (0-based). + DuringStarted { state: u16, during: u16 }, + /// A `during:` activity was cancelled because its owning state is + /// being exited. + DuringCancelled { state: u16, during: u16 }, + /// A transition is about to fire. `from` is the innermost active state + /// at the moment the transition was triggered; `to` is the target. + /// Followed by the actual `Exited` / `Entered` / etc. events that + /// implement the transition. + TransitionFired { from: Option, to: u16 }, + /// An event reached a state's handler. `handler_state` is the state + /// whose handler ran (which may be an ancestor of the innermost active + /// state if the event bubbled). + EventDelivered { handler_state: u16, event: u16 }, + /// An event was dispatched but no state on the active path had a + /// handler. Silently dropped per spec. + EventDropped { event: u16 }, + /// `emit()` from inside an action successfully pushed an event onto + /// the internal queue. + EmitQueued { event: u16 }, + /// `emit()` from inside an action failed because the queue was full. + /// The action chain continues; the runtime surfaces `QueueFull` at + /// end of tick. + EmitFailed { event: u16 }, + /// An event matched the chart's `terminate(...)` declaration and is + /// about to drive shutdown. Followed by the bottom-up exit chain + /// (Exited events) and a final `Terminated`. + TerminateRequested { event: u16 }, + /// A timer was armed (set to start counting down) for a state. + /// `ns` is the duration in nanoseconds. + TimerArmed { state: u16, timer: u16, ns: u64 }, + /// A timer was cancelled because its owning state is being exited. + TimerCancelled { state: u16, timer: u16 }, + /// A timer's countdown reached zero and its handler is about to run. + TimerFired { state: u16, timer: u16 }, + /// The chart processed its `terminate` event and the run loop is + /// done. Always the final event in the journal. + Terminated, +} + +// JournalSink lives in `__private` (in `lib.rs`) so the codegen can +// unconditionally refer to `::hsmc::__private::JournalSink` whether or +// not the `journal` feature is on. diff --git a/hsmc/src/lib.rs b/hsmc/src/lib.rs index 134649d..977fb0e 100644 --- a/hsmc/src/lib.rs +++ b/hsmc/src/lib.rs @@ -102,6 +102,142 @@ pub use hsmc_macros::statechart; mod error; pub use error::HsmcError; +// ── Journal (deterministic execution trace) ───────────────────────── +// +// When `feature = "journal"` is enabled, the macro emits one +// [`TraceEvent`] per observable atom: entries, exits, action calls, +// during start/cancel, timer arm/cancel/fire, queued emits, event +// dispatch, transitions, termination. The events are appended to the +// machine's internal `JournalSink` so callers can compare against an +// expected sequence (see `tests/replay.rs`). +// +// When the feature is OFF, the codegen still emits `__chart_journal!` +// invocations at every hook site, but the macro expands to nothing +// (zero overhead) and `JournalSink` is a ZST so the field on the +// machine takes 0 bytes. + +#[cfg(feature = "journal")] +mod journal; + +#[cfg(feature = "journal")] +pub use journal::{ActionKind, Journal, TraceEvent}; + +/// Journal call dispatcher invoked by `statechart!`-generated code. +/// Not part of the public API. +/// +/// Call form: `__chart_journal!(, )`. +/// The first argument is a place expression for the sink (typically +/// `self.__journal`); the second is the full `TraceEvent` value to +/// push. +/// +/// When the `journal` feature is off, the macro discards both arguments +/// and expands to nothing — the codegen can refer to `TraceEvent::*` +/// without the type having to exist. +#[cfg(feature = "journal")] +#[doc(hidden)] +#[macro_export] +macro_rules! __chart_journal { + ($sink:expr, $event:expr) => { + $sink.push($event); + }; +} + +/// No-op fallback for when `feature = "journal"` is disabled. +#[cfg(not(feature = "journal"))] +#[doc(hidden)] +#[macro_export] +macro_rules! __chart_journal { + ($($_:tt)*) => {}; +} + +// ── Auto-tracing dispatcher ────────────────────────────────────────── +// +// When a chart opts in via `trace;`, the proc-macro emits calls to +// `::hsmc::__chart_trace!( , );` at +// every state entry, exit, action invocation, and transition. This +// crate-level macro picks the backend based on which `trace-*` cargo +// feature is enabled — exactly one of `trace-defmt` / `trace-log` / +// `trace-tracing`. With none enabled it expands to nothing. +// +// Multiple `trace-*` features enabled simultaneously produce a +// duplicate-definition compile error from rustc. Intentional. + +/// Internal trace dispatcher invoked by `statechart!`-generated code. +/// Not part of the public API. +#[cfg(feature = "trace-defmt")] +#[doc(hidden)] +#[macro_export] +macro_rules! __chart_trace { + (enter $chart:literal, $state:expr) => { + ::defmt::info!("[{}] enter {}", $chart, $state); + }; + (exit $chart:literal, $state:expr) => { + ::defmt::info!("[{}] exit {}", $chart, $state); + }; + (action $chart:literal, $action:expr) => { + ::defmt::trace!("[{}] action {}", $chart, $action); + }; + (transition $chart:literal, $from:expr, $to:expr) => { + ::defmt::info!("[{}] {} -> {}", $chart, $from, $to); + }; + ($($_:tt)*) => {}; +} + +/// Internal trace dispatcher invoked by `statechart!`-generated code. +/// Not part of the public API. +#[cfg(feature = "trace-log")] +#[doc(hidden)] +#[macro_export] +macro_rules! __chart_trace { + (enter $chart:literal, $state:expr) => { + ::log::info!("[{}] enter {}", $chart, $state); + }; + (exit $chart:literal, $state:expr) => { + ::log::info!("[{}] exit {}", $chart, $state); + }; + (action $chart:literal, $action:expr) => { + ::log::trace!("[{}] action {}", $chart, $action); + }; + (transition $chart:literal, $from:expr, $to:expr) => { + ::log::info!("[{}] {} -> {}", $chart, $from, $to); + }; + ($($_:tt)*) => {}; +} + +/// Internal trace dispatcher invoked by `statechart!`-generated code. +/// Not part of the public API. +#[cfg(feature = "trace-tracing")] +#[doc(hidden)] +#[macro_export] +macro_rules! __chart_trace { + (enter $chart:literal, $state:expr) => { + ::tracing::info!(chart = $chart, state = $state, "enter"); + }; + (exit $chart:literal, $state:expr) => { + ::tracing::info!(chart = $chart, state = $state, "exit"); + }; + (action $chart:literal, $action:expr) => { + ::tracing::trace!(chart = $chart, action = $action, "action"); + }; + (transition $chart:literal, $from:expr, $to:expr) => { + ::tracing::info!(chart = $chart, from = $from, to = $to, "transition"); + }; + ($($_:tt)*) => {}; +} + +/// No-op fallback when no `trace-*` backend feature is enabled. The +/// chart's `trace;` keyword still parses; calls just expand to nothing. +#[cfg(not(any( + feature = "trace-defmt", + feature = "trace-log", + feature = "trace-tracing", +)))] +#[doc(hidden)] +#[macro_export] +macro_rules! __chart_trace { + ($($_:tt)*) => {}; +} + #[doc(hidden)] pub mod __private { //! Implementation details used by code generated by the `statechart!` macro. @@ -110,6 +246,63 @@ pub mod __private { pub use crate::error::HsmcError; + // ── JournalSink ────────────────────────────────────────────────── + // + // The codegen unconditionally declares a `__journal: JournalSink` + // field on the generated machine and on the action context. When the + // `journal` feature is on, JournalSink wraps a `Vec` and + // the `__chart_journal!` macro pushes events into it. When off, it's + // a ZST and the macro expands to nothing — zero overhead, no `alloc` + // requirement. + + /// Journal sink storing the in-order trace of observable execution + /// atoms when `feature = "journal"` is enabled. Zero-sized when + /// disabled. + #[cfg(feature = "journal")] + #[derive(Default, Debug, Clone)] + pub struct JournalSink { + events: crate::journal::Vec, + } + + #[cfg(feature = "journal")] + impl JournalSink { + pub const fn new() -> Self { + Self { + events: crate::journal::Vec::new(), + } + } + #[inline] + pub fn push(&mut self, event: crate::TraceEvent) { + self.events.push(event); + } + pub fn events(&self) -> &[crate::TraceEvent] { + &self.events + } + pub fn take(&mut self) -> crate::journal::Vec { + core::mem::take(&mut self.events) + } + pub fn clear(&mut self) { + self.events.clear(); + } + pub fn len(&self) -> usize { + self.events.len() + } + pub fn is_empty(&self) -> bool { + self.events.is_empty() + } + } + + #[cfg(not(feature = "journal"))] + #[derive(Default, Debug, Clone, Copy)] + pub struct JournalSink; + + #[cfg(not(feature = "journal"))] + impl JournalSink { + pub const fn new() -> Self { + Self + } + } + /// A simple bounded event queue built on `heapless::Deque`. /// Capacity is a const generic. pub struct EventQueue { diff --git a/hsmc/tests/det_bubbling.rs b/hsmc/tests/det_bubbling.rs new file mode 100644 index 0000000..6b1b1f9 --- /dev/null +++ b/hsmc/tests/det_bubbling.rs @@ -0,0 +1,277 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for EVENT BUBBLING. +//! +//! Spec section "How events are handled": +//! Event comes in. Start at the innermost active state. Does it have a +//! handler for this event? If yes, that handler runs and the event is +//! consumed — no further handling. If no, walk up to the parent. Repeat. +//! If you walk all the way to the root and still nothing handles it, the +//! event is silently discarded. +//! +//! - A handler on a leaf state shadows a handler on its ancestor. +//! - Multiple handlers in the same state for the same trigger: +//! actions in declaration order, then the transition. +//! - Timer triggers do NOT bubble. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + LeafEv, // handled at leaf + MidEv, // handled at Mid only + RootEv, // handled at root only + Unknown, // no handler anywhere + Shadowed, // handler at both Leaf and Mid; leaf wins + MultiAct, // multiple actions in same state for same trigger + Halt, +} + +statechart! { + Bub { + context: Ctx; + events: Ev; + default(Mid); + terminate(Halt); + + on(RootEv) => root_handler; + + state Mid { + entry: m_in; + exit: m_out; + default(Leaf); + on(MidEv) => mid_handler; + on(Shadowed) => mid_shadowed; + state Leaf { + entry: l_in; + exit: l_out; + on(LeafEv) => leaf_handler; + on(Shadowed) => leaf_shadowed; + on(MultiAct) => multi1; + on(MultiAct) => multi2; + on(MultiAct) => multi3; + } + } + } +} + +impl BubActions for BubActionContext<'_> { + async fn m_in(&mut self) {} + async fn m_out(&mut self) {} + async fn l_in(&mut self) {} + async fn l_out(&mut self) {} + async fn root_handler(&mut self) {} + async fn mid_handler(&mut self) {} + async fn leaf_handler(&mut self) {} + async fn mid_shadowed(&mut self) {} + async fn leaf_shadowed(&mut self) {} + async fn multi1(&mut self) {} + async fn multi2(&mut self) {} + async fn multi3(&mut self) {} +} + +const SR: u16 = 0; +const SM: u16 = 1; +const SL: u16 = 2; +// Action interning order: +// Root body: handlers (root_handler → 0) +// Mid body: m_in → 1, m_out → 2; handlers (mid_handler → 3, mid_shadowed → 4) +// Leaf body: l_in → 5, l_out → 6; handlers (leaf_handler → 7, leaf_shadowed → 8, multi1..3 → 9..11) +const A_ROOT_HANDLER: u16 = 0; +const A_MID_HANDLER: u16 = 3; +const A_LEAF_HANDLER: u16 = 7; +const A_MID_SHADOWED: u16 = 4; +const A_LEAF_SHADOWED: u16 = 8; +const A_MULTI1: u16 = 9; +const A_MULTI2: u16 = 10; +const A_MULTI3: u16 = 11; +// Event interning order: +// Root processes first: handler RootEv → 0 +// Then Mid: MidEv → 1, Shadowed → 2 +// Then Leaf: LeafEv → 3, Shadowed already interned, MultiAct → 4 +const E_ROOTEV: u16 = 0; +const E_MIDEV: u16 = 1; +const E_SHADOWED: u16 = 2; +const E_LEAFEV: u16 = 3; +const E_MULTIACT: u16 = 4; + +fn handler_act(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Handler } +} + +#[tokio::test(flavor = "current_thread")] +async fn det_bub_handler_at_leaf() { + // Leaf has handler for LeafEv. Bubbling stops at Leaf. + tokio::task::LocalSet::new().run_until(async { + let mut m = Bub::new(Ctx); + let _ = m.dispatch(Ev::LeafEv).await; + let j = m.take_journal(); + // Find the EventDelivered for LeafEv. + let delivered = j.iter().find(|e| matches!( + e, TraceEvent::EventDelivered { event: E_LEAFEV, .. } + )); + assert!(matches!( + delivered, + Some(TraceEvent::EventDelivered { handler_state: SL, event: E_LEAFEV }) + ), "LeafEv must be delivered to Leaf, got: {:?}", delivered); + // The handler action must fire. + let saw_handler = j.iter().any(|e| matches!( + e, + TraceEvent::ActionInvoked { state: SL, action: A_LEAF_HANDLER, kind: ActionKind::Handler } + )); + assert!(saw_handler, "leaf_handler must run"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_bub_event_bubbles_to_parent() { + // Leaf has no handler for MidEv. Bubble to Mid. + tokio::task::LocalSet::new().run_until(async { + let mut m = Bub::new(Ctx); + let _ = m.dispatch(Ev::MidEv).await; + let j = m.take_journal(); + let delivered = j.iter().find(|e| matches!( + e, TraceEvent::EventDelivered { event: E_MIDEV, .. } + )); + assert!(matches!( + delivered, + Some(TraceEvent::EventDelivered { handler_state: SM, event: E_MIDEV }) + ), "MidEv must be delivered to Mid, got: {:?}", delivered); + assert_eq!(j.iter().filter(|e| matches!( + e, TraceEvent::ActionInvoked { action: A_MID_HANDLER, .. } + )).count(), 1); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_bub_event_bubbles_to_root() { + // Neither Leaf nor Mid handles RootEv. Bubble to Root. + tokio::task::LocalSet::new().run_until(async { + let mut m = Bub::new(Ctx); + let _ = m.dispatch(Ev::RootEv).await; + let j = m.take_journal(); + let delivered = j.iter().find(|e| matches!( + e, TraceEvent::EventDelivered { event: E_ROOTEV, .. } + )); + assert!(matches!( + delivered, + Some(TraceEvent::EventDelivered { handler_state: SR, event: E_ROOTEV }) + ), "RootEv must be delivered to Root, got: {:?}", delivered); + assert_eq!(j.iter().filter(|e| matches!( + e, TraceEvent::ActionInvoked { action: A_ROOT_HANDLER, .. } + )).count(), 1); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_bub_unknown_event_dropped() { + // No state handles Unknown. Spec: "the event is silently discarded." + tokio::task::LocalSet::new().run_until(async { + let mut m = Bub::new(Ctx); + let _ = m.dispatch(Ev::Unknown).await; + let j = m.take_journal(); + // Must contain an EventDropped for Unknown. + let dropped = j.iter().any(|e| matches!(e, TraceEvent::EventDropped { .. })); + assert!(dropped, "unhandled Unknown must be journaled as EventDropped"); + // No EventDelivered for it. + let delivered_count = j.iter().filter(|e| matches!( + e, TraceEvent::EventDelivered { .. } + )).count(); + // No EventDelivered should fire at all (we only sent Unknown). + assert_eq!(delivered_count, 0, + "Unknown must not be delivered; got: {:?}", j); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_bub_leaf_shadows_parent() { + // Both Leaf and Mid have handlers for Shadowed. Leaf wins (search starts there). + tokio::task::LocalSet::new().run_until(async { + let mut m = Bub::new(Ctx); + let _ = m.dispatch(Ev::Shadowed).await; + let j = m.take_journal(); + let leaf_fired = j.iter().any(|e| matches!( + e, TraceEvent::ActionInvoked { action: A_LEAF_SHADOWED, .. } + )); + let mid_fired = j.iter().any(|e| matches!( + e, TraceEvent::ActionInvoked { action: A_MID_SHADOWED, .. } + )); + assert!(leaf_fired, "leaf_shadowed must fire (innermost wins)"); + assert!(!mid_fired, "mid_shadowed must NOT fire (shadowed by leaf)"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_bub_multiple_handlers_declaration_order() { + // Leaf has three actions for MultiAct. They must fire in declaration order. + tokio::task::LocalSet::new().run_until(async { + let mut m = Bub::new(Ctx); + let _ = m.dispatch(Ev::MultiAct).await; + let order: Vec = m.take_journal().iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { action, kind: ActionKind::Handler, .. } => Some(*action), + _ => None, + }).collect(); + assert_eq!(order, vec![A_MULTI1, A_MULTI2, A_MULTI3], + "multi-action handlers must fire in declaration order"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_bub_handler_state_recorded_correctly() { + // EventDelivered.handler_state must reflect WHERE the handler matched, not + // where the event was sent. + tokio::task::LocalSet::new().run_until(async { + let mut m = Bub::new(Ctx); + let _ = m.dispatch(Ev::MidEv).await; + let _ = m.dispatch(Ev::RootEv).await; + let j = m.take_journal(); + let mid_delivered = j.iter().find(|e| matches!( + e, TraceEvent::EventDelivered { event: E_MIDEV, .. } + )); + let root_delivered = j.iter().find(|e| matches!( + e, TraceEvent::EventDelivered { event: E_ROOTEV, .. } + )); + assert!(matches!(mid_delivered, Some(TraceEvent::EventDelivered { handler_state: SM, .. }))); + assert!(matches!(root_delivered, Some(TraceEvent::EventDelivered { handler_state: SR, .. }))); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_bub_multiple_unknown_events_each_dropped() { + // Three unknowns — three EventDropped events. + tokio::task::LocalSet::new().run_until(async { + let mut m = Bub::new(Ctx); + let _ = m.dispatch(Ev::Unknown).await; + let _ = m.dispatch(Ev::Unknown).await; + let _ = m.dispatch(Ev::Unknown).await; + let dropped_count = m.journal().iter().filter(|e| matches!( + e, TraceEvent::EventDropped { .. } + )).count(); + assert_eq!(dropped_count, 3); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_bub_byte_deterministic_under_mixed_events() { + let run = || async { + tokio::task::LocalSet::new().run_until(async { + let mut m = Bub::new(Ctx); + let _ = m.dispatch(Ev::LeafEv).await; + let _ = m.dispatch(Ev::MidEv).await; + let _ = m.dispatch(Ev::Unknown).await; + let _ = m.dispatch(Ev::Shadowed).await; + let _ = m.dispatch(Ev::MultiAct).await; + let _ = m.dispatch(Ev::RootEv).await; + m.take_journal() + }).await + }; + let first = run().await; + for i in 1..15 { + assert_eq!(first, run().await, "diverged on run {i}"); + } +} diff --git a/hsmc/tests/det_current_state.rs b/hsmc/tests/det_current_state.rs new file mode 100644 index 0000000..0d342b3 --- /dev/null +++ b/hsmc/tests/det_current_state.rs @@ -0,0 +1,85 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for `current_state()` reflecting the innermost +//! active state at every point. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::statechart; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + GoB, + UpToParent, + Halt, +} + +statechart! { + Cur { + context: Ctx; + events: Ev; + default(Parent); + terminate(Halt); + + state Parent { + entry: p_in; + exit: p_out; + default(A); + state A { + entry: a_in; + exit: a_out; + on(GoB) => B; + on(UpToParent) => Parent; + } + state B { + entry: b_in; + exit: b_out; + on(UpToParent) => Parent; + } + } + } +} + +impl CurActions for CurActionContext<'_> { + async fn p_in(&mut self) {} + async fn p_out(&mut self) {} + async fn a_in(&mut self) {} + async fn a_out(&mut self) {} + async fn b_in(&mut self) {} + async fn b_out(&mut self) {} +} + +#[tokio::test(flavor = "current_thread")] +async fn det_current_state_initial_is_default_leaf() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Cur::new(Ctx); + // Drive initial entry by sending an event. + let _ = m.dispatch(Ev::GoB).await; + // Now in B. + assert_eq!(m.current_state(), CurState::B); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_current_state_after_lateral_transition() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Cur::new(Ctx); + let _ = m.dispatch(Ev::GoB).await; + assert_eq!(m.current_state(), CurState::B); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_current_state_after_up_returns_composite() { + // Spec: current_state can return a composite if it became innermost via + // an up-transition. + tokio::task::LocalSet::new().run_until(async { + let mut m = Cur::new(Ctx); + let _ = m.dispatch(Ev::UpToParent).await; + assert_eq!(m.current_state(), CurState::Parent, + "after up-transition, current_state returns the composite Parent"); + }).await; +} diff --git a/hsmc/tests/det_descent.rs b/hsmc/tests/det_descent.rs new file mode 100644 index 0000000..9daf122 --- /dev/null +++ b/hsmc/tests/det_descent.rs @@ -0,0 +1,210 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for DEFAULT-DESCENT into composite targets. +//! +//! Spec section "Default child": +//! Whenever a state with children is entered, the default child is entered +//! immediately after that state's entry actions finish — it's effectively +//! an automatic transition into the child. +//! +//! Pins down: entries fire outer-to-inner, default-descent unrolls the chain, +//! the leaf is the innermost active state at the end. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + Go, + Halt, +} + +// Hierarchy: Root → Idle, Root → Tower → L1 → L2 → L3 +statechart! { + Desc { + context: Ctx; + events: Ev; + default(Idle); + terminate(Halt); + + state Idle { + entry: idle_in; + exit: idle_out; + on(Go) => Tower; + } + state Tower { + entry: tower_in; + exit: tower_out; + default(L1); + state L1 { + entry: l1_in; + exit: l1_out; + default(L2); + state L2 { + entry: l2_in; + exit: l2_out; + default(L3); + state L3 { + entry: l3_in; + exit: l3_out; + } + } + } + } + } +} + +impl DescActions for DescActionContext<'_> { + async fn idle_in(&mut self) {} + async fn idle_out(&mut self) {} + async fn tower_in(&mut self) {} + async fn tower_out(&mut self) {} + async fn l1_in(&mut self) {} + async fn l1_out(&mut self) {} + async fn l2_in(&mut self) {} + async fn l2_out(&mut self) {} + async fn l3_in(&mut self) {} + async fn l3_out(&mut self) {} +} + +const SR: u16 = 0; +const SI: u16 = 1; +const ST: u16 = 2; +const SL1: u16 = 3; +const SL2: u16 = 4; +const SL3: u16 = 5; +const A_IDLE_IN: u16 = 0; +const A_IDLE_OUT: u16 = 1; +const A_TOWER_IN: u16 = 2; +const A_TOWER_OUT: u16 = 3; +const A_L1_IN: u16 = 4; +const A_L1_OUT: u16 = 5; +const A_L2_IN: u16 = 6; +const A_L2_OUT: u16 = 7; +const A_L3_IN: u16 = 8; +const A_L3_OUT: u16 = 9; +const E_GO: u16 = 0; + +fn entry(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Entry } +} +fn exit_(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Exit } +} + +#[tokio::test(flavor = "current_thread")] +async fn det_descent_target_with_three_default_levels() { + // Idle → Tower: Tower has default chain L1 → L2 → L3. + tokio::task::LocalSet::new().run_until(async { + let mut m = Desc::new(Ctx); + let _ = m.dispatch(Ev::Go).await; + let actual = m.take_journal(); + + let expected = vec![ + TraceEvent::Started { chart_hash: Desc::<8>::CHART_HASH }, + TraceEvent::Entered { state: SR }, + TraceEvent::Entered { state: SI }, + entry(SI, A_IDLE_IN), + TraceEvent::EventDelivered { handler_state: SI, event: E_GO }, + TraceEvent::TransitionFired { from: Some(SI), to: ST }, + exit_(SI, A_IDLE_OUT), + TraceEvent::Exited { state: SI }, + TraceEvent::Entered { state: ST }, + entry(ST, A_TOWER_IN), + TraceEvent::Entered { state: SL1 }, + entry(SL1, A_L1_IN), + TraceEvent::Entered { state: SL2 }, + entry(SL2, A_L2_IN), + TraceEvent::Entered { state: SL3 }, + entry(SL3, A_L3_IN), + ]; + + assert_eq!(actual, expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_descent_entries_fire_outer_to_inner() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Desc::new(Ctx); + let _ = m.dispatch(Ev::Go).await; + // After the GO transition: order of Entered events should be Tower → L1 → L2 → L3. + let split = m.journal().iter().position(|e| matches!( + e, TraceEvent::TransitionFired { .. } + )).unwrap(); + let entered: Vec = m.journal()[split..].iter().filter_map(|e| match e { + TraceEvent::Entered { state } => Some(*state), + _ => None, + }).collect(); + assert_eq!(entered, vec![ST, SL1, SL2, SL3]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_descent_termination_exits_full_chain() { + // After full descent into L3, terminate exits L3 → L2 → L1 → Tower → Root. + tokio::task::LocalSet::new().run_until(async { + let mut m = Desc::new(Ctx); + let _ = m.dispatch(Ev::Go).await; + let _ = m.dispatch(Ev::Halt).await; + let exits: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::Exited { state } => Some(*state), + _ => None, + }).collect(); + assert_eq!(exits, vec![SI, SL3, SL2, SL1, ST, SR]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_descent_action_kind_sequence() { + // After GO: Tower entry kind, L1 entry, L2 entry, L3 entry. All Entry. + tokio::task::LocalSet::new().run_until(async { + let mut m = Desc::new(Ctx); + let _ = m.dispatch(Ev::Go).await; + let split = m.journal().iter().position(|e| matches!( + e, TraceEvent::TransitionFired { .. } + )).unwrap(); + // After the Idle exit, all subsequent ActionInvoked must be Entry kind. + let kinds_after_exit: Vec = m.journal()[split + 3..].iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { kind, .. } => Some(*kind), + _ => None, + }).collect(); + assert!(kinds_after_exit.iter().all(|k| *k == ActionKind::Entry), + "all post-transition actions must be Entry kind, got {:?}", kinds_after_exit); + assert_eq!(kinds_after_exit.len(), 4, "Tower + L1 + L2 + L3 entries"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_descent_byte_deterministic() { + let run = || async { + tokio::task::LocalSet::new().run_until(async { + let mut m = Desc::new(Ctx); + let _ = m.dispatch(Ev::Go).await; + let _ = m.dispatch(Ev::Halt).await; + m.take_journal() + }).await + }; + let first = run().await; + for i in 1..10 { + assert_eq!(first, run().await, "diverged on run {i}"); + } +} + +#[tokio::test(flavor = "current_thread")] +async fn det_descent_initial_descent_is_idle_only() { + // Initial default chain is Root → Idle. Idle has no children, so only one Entered. + tokio::task::LocalSet::new().run_until(async { + let mut m = Desc::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let entered: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::Entered { state } => Some(*state), + _ => None, + }).collect(); + assert_eq!(entered, vec![SR, SI]); + }).await; +} diff --git a/hsmc/tests/det_during.rs b/hsmc/tests/det_during.rs new file mode 100644 index 0000000..5b3d51b --- /dev/null +++ b/hsmc/tests/det_during.rs @@ -0,0 +1,202 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for `during:` activities. +//! +//! Spec section "during: activities": +//! A `during:` is an async function that runs while its owning state is on +//! the active path. It is started after the entry actions of that state +//! finish, and it is cancelled before the exit actions of that state begin. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; +use core::time::Duration; + +#[derive(Default)] +pub struct Ctx { + pub a: u32, + pub b: u32, + pub c: u32, +} + +#[derive(Debug, Clone)] +pub enum Ev { + Done, + Halt, +} + +statechart! { + Du { + context: Ctx; + events: Ev; + default(Working); + terminate(Halt); + + state Working { + entry: w_in; + exit: w_out; + during: tick_a(a); + during: tick_b(b); + on(Done) => Idle; + } + state Idle { + entry: i_in; + exit: i_out; + } + } +} + +impl DuActions for DuActionContext<'_> { + async fn w_in(&mut self) {} + async fn w_out(&mut self) {} + async fn i_in(&mut self) {} + async fn i_out(&mut self) {} +} + +async fn tick_a(_a: &mut u32) -> Ev { + // Pause for a long time; this future will likely be cancelled before + // completing so we exercise the cancel path. + tokio::time::sleep(Duration::from_secs(60)).await; + Ev::Done +} + +async fn tick_b(_b: &mut u32) -> Ev { + tokio::time::sleep(Duration::from_secs(60)).await; + Ev::Done +} + +const SR: u16 = 0; +const SW: u16 = 1; +const SI: u16 = 2; + +#[tokio::test(flavor = "current_thread")] +async fn det_during_started_after_entries() { + // Spec: started AFTER entry actions of the owning state finish. + tokio::task::LocalSet::new().run_until(async { + let mut m = Du::new(Ctx::default()); + let _ = m.dispatch(Ev::Halt).await; + let j = m.take_journal(); + // Find Working's entry action invocation. + let w_entry_idx = j.iter().position(|e| matches!( + e, TraceEvent::ActionInvoked { state: SW, kind: ActionKind::Entry, .. } + )); + // Find first DuringStarted on Working. + let d_started_idx = j.iter().position(|e| matches!( + e, TraceEvent::DuringStarted { state: SW, .. } + )); + assert!(w_entry_idx.is_some()); + assert!(d_started_idx.is_some()); + assert!(w_entry_idx.unwrap() < d_started_idx.unwrap(), + "DuringStarted must come AFTER entry actions"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_during_cancelled_before_exits() { + // Spec: cancelled BEFORE exit actions of the owning state begin. + tokio::task::LocalSet::new().run_until(async { + let mut m = Du::new(Ctx::default()); + let _ = m.dispatch(Ev::Halt).await; + let j = m.take_journal(); + let d_cancelled_idx = j.iter().position(|e| matches!( + e, TraceEvent::DuringCancelled { state: SW, .. } + )); + let w_exit_idx = j.iter().position(|e| matches!( + e, TraceEvent::ActionInvoked { state: SW, kind: ActionKind::Exit, .. } + )); + assert!(d_cancelled_idx.is_some(), "DuringCancelled must appear"); + assert!(w_exit_idx.is_some(), "exit actions must run"); + assert!(d_cancelled_idx.unwrap() < w_exit_idx.unwrap(), + "DuringCancelled must come BEFORE exit actions"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_during_two_durings_two_started_two_cancelled() { + // Two durings declared on Working — should see two DuringStarted and two DuringCancelled. + tokio::task::LocalSet::new().run_until(async { + let mut m = Du::new(Ctx::default()); + let _ = m.dispatch(Ev::Halt).await; + let j = m.take_journal(); + let started = j.iter().filter(|e| matches!( + e, TraceEvent::DuringStarted { state: SW, .. } + )).count(); + let cancelled = j.iter().filter(|e| matches!( + e, TraceEvent::DuringCancelled { state: SW, .. } + )).count(); + assert_eq!(started, 2); + assert_eq!(cancelled, 2); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_during_indices_are_declaration_order() { + // Indices 0, 1 in declaration order. + tokio::task::LocalSet::new().run_until(async { + let mut m = Du::new(Ctx::default()); + let _ = m.dispatch(Ev::Halt).await; + let started_indices: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::DuringStarted { during, .. } => Some(*during), + _ => None, + }).collect(); + assert_eq!(started_indices, vec![0, 1]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_during_cancelled_indices_match() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Du::new(Ctx::default()); + let _ = m.dispatch(Ev::Halt).await; + let cancelled_indices: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::DuringCancelled { during, .. } => Some(*during), + _ => None, + }).collect(); + // Cancellation also walks declaration order in the current implementation. + assert_eq!(cancelled_indices, vec![0, 1]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_during_state_id_matches() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Du::new(Ctx::default()); + let _ = m.dispatch(Ev::Halt).await; + let started_states: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::DuringStarted { state, .. } => Some(*state), + _ => None, + }).collect(); + // Both DuringStarted events refer to Working (id 1). + assert!(started_states.iter().all(|&s| s == SW)); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_during_no_durings_on_idle() { + // Idle has no `during:` declarations. After we transition into Idle, no + // DuringStarted for Idle. + tokio::task::LocalSet::new().run_until(async { + let mut m = Du::new(Ctx::default()); + let _ = m.dispatch(Ev::Done).await; + let on_idle: usize = m.journal().iter().filter(|e| matches!( + e, TraceEvent::DuringStarted { state: SI, .. } + )).count(); + assert_eq!(on_idle, 0); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_during_byte_deterministic() { + let run = || async { + tokio::task::LocalSet::new().run_until(async { + let mut m = Du::new(Ctx::default()); + let _ = m.dispatch(Ev::Done).await; + let _ = m.dispatch(Ev::Halt).await; + m.take_journal() + }).await + }; + let first = run().await; + for i in 1..10 { + assert_eq!(first, run().await, "diverged on run {i}"); + } +} diff --git a/hsmc/tests/det_emit.rs b/hsmc/tests/det_emit.rs new file mode 100644 index 0000000..9f3403e --- /dev/null +++ b/hsmc/tests/det_emit.rs @@ -0,0 +1,201 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for `emit()` from action code. +//! +//! Spec section "emit()": +//! The event goes on the machine's internal queue. It is NOT processed +//! immediately. The runtime finishes handling whatever event it's +//! currently handling — including every entry and exit action of any +//! transition — and only then dequeues `Ev` and dispatches it normally. +//! No re-entrant dispatch. +//! +//! If the queue is full, `emit()` returns `Err(QueueFull)`. Subsequent +//! actions in the same chain still run; they may attempt further emits, +//! but those also fail. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + Trigger, + Followup, + Many, + Halt, +} + +statechart! { + Em { + context: Ctx; + events: Ev; + default(A); + terminate(Halt); + + state A { + entry: a_in; + exit: a_out; + on(Trigger) => emit_followup; + on(Followup) => B; + on(Many) => emit_many; + } + state B { + entry: b_in; + exit: b_out; + } + } +} + +impl EmActions for EmActionContext<'_> { + async fn a_in(&mut self) {} + async fn a_out(&mut self) {} + async fn b_in(&mut self) {} + async fn b_out(&mut self) {} + async fn emit_followup(&mut self) { + let _ = self.emit(Ev::Followup); + } + async fn emit_many(&mut self) { + // Try to overflow the queue; capacity is 8 by default. + for _ in 0..15 { + let _ = self.emit(Ev::Followup); + } + } +} + +const E_TRIGGER: u16 = 0; +const E_FOLLOWUP: u16 = 1; +const E_MANY: u16 = 2; + +#[tokio::test(flavor = "current_thread")] +async fn det_emit_queues_event() { + // emit_followup queues Followup. Journal must have EmitQueued. + tokio::task::LocalSet::new().run_until(async { + let mut m = Em::new(Ctx); + let _ = m.dispatch(Ev::Trigger).await; + let queued = m.journal().iter().filter(|e| matches!( + e, TraceEvent::EmitQueued { .. } + )).count(); + assert_eq!(queued, 1, "exactly one EmitQueued, got {:?}", m.journal()); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_emit_followup_event_is_dispatched() { + // After Trigger fires emit_followup, the queue contains Followup. + // dispatch() drains, so Followup is dispatched and transitions A → B. + tokio::task::LocalSet::new().run_until(async { + let mut m = Em::new(Ctx); + let _ = m.dispatch(Ev::Trigger).await; + let j = m.take_journal(); + + // Both Trigger and Followup must be EventDelivered. + let delivered_events: Vec = j.iter().filter_map(|e| match e { + TraceEvent::EventDelivered { event, .. } => Some(*event), + _ => None, + }).collect(); + assert_eq!(delivered_events, vec![E_TRIGGER, E_FOLLOWUP]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_emit_no_reentrant_dispatch() { + // Spec: emit during a handler must not re-enter the dispatcher inside the + // current handler. The emit_followup action does ONE thing: emit. Then it + // returns. ONLY THEN does the dispatcher pick up Followup. + // + // Verify: the EmitQueued event for Followup appears BEFORE the + // EventDelivered for Followup. + tokio::task::LocalSet::new().run_until(async { + let mut m = Em::new(Ctx); + let _ = m.dispatch(Ev::Trigger).await; + let j = m.take_journal(); + let queued_idx = j.iter().position(|e| matches!(e, TraceEvent::EmitQueued { event: E_FOLLOWUP })).unwrap(); + let delivered_idx = j.iter().position(|e| matches!( + e, TraceEvent::EventDelivered { event: E_FOLLOWUP, .. } + )).unwrap(); + assert!(queued_idx < delivered_idx, + "EmitQueued ({}) must come before EventDelivered ({})", queued_idx, delivered_idx); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_emit_overflow_records_emitfailed() { + // emit_many tries 15 emits. Default queue cap is 8 (one slot has Many in + // it currently being processed; 7 more fit). Some succeed, some fail. + tokio::task::LocalSet::new().run_until(async { + let mut m = Em::new(Ctx); + let _ = m.dispatch(Ev::Many).await; + let j = m.take_journal(); + let queued = j.iter().filter(|e| matches!(e, TraceEvent::EmitQueued { .. })).count(); + let failed = j.iter().filter(|e| matches!(e, TraceEvent::EmitFailed { .. })).count(); + assert!(queued > 0, "some emits must succeed"); + assert!(failed > 0, "some emits must fail when queue overflows"); + assert_eq!(queued + failed, 15, "total emit attempts must be 15"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_emit_does_not_reorder_external_events() { + // External events still process in arrival order. Emitted events are + // appended to the queue (FIFO). + tokio::task::LocalSet::new().run_until(async { + let mut m = Em::new(Ctx); + let _ = m.dispatch(Ev::Trigger).await; + let j = m.take_journal(); + let delivered_events: Vec = j.iter().filter_map(|e| match e { + TraceEvent::EventDelivered { event, .. } => Some(*event), + _ => None, + }).collect(); + // Trigger was delivered first, then the emitted Followup. + assert_eq!(delivered_events[0], E_TRIGGER); + assert_eq!(delivered_events[1], E_FOLLOWUP); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_emit_byte_deterministic() { + let run = || async { + tokio::task::LocalSet::new().run_until(async { + let mut m = Em::new(Ctx); + let _ = m.dispatch(Ev::Trigger).await; + let _ = m.dispatch(Ev::Halt).await; + m.take_journal() + }).await + }; + let first = run().await; + for i in 1..10 { + assert_eq!(first, run().await, "diverged on run {i}"); + } +} + +#[tokio::test(flavor = "current_thread")] +async fn det_emit_state_after_emit_action_runs_to_completion() { + // Spec: subsequent actions in the same chain still run after emit failure. + // Hard to test surgically without an action-after-emit; pin instead that + // the EmitFailed events are followed by additional ActionInvoked events + // for the SAME emit_many handler call. + tokio::task::LocalSet::new().run_until(async { + let mut m = Em::new(Ctx); + let _ = m.dispatch(Ev::Many).await; + let j = m.take_journal(); + // The handler emit_many is one call; it emits 15 times. So we should see + // 15 emit-result events all between two boundaries: after Many's + // EventDelivered and before any subsequent Followup deliveries. + let many_delivered_idx = j.iter().position(|e| matches!( + e, TraceEvent::EventDelivered { event: E_MANY, .. } + )).unwrap(); + let emit_results: Vec<&TraceEvent> = j[many_delivered_idx..].iter().take_while(|e| matches!( + e, + TraceEvent::EmitQueued { .. } + | TraceEvent::EmitFailed { .. } + | TraceEvent::ActionInvoked { .. } + | TraceEvent::EventDelivered { event: E_MANY, .. } + )).filter(|e| matches!( + e, TraceEvent::EmitQueued { .. } | TraceEvent::EmitFailed { .. } + )).collect(); + assert_eq!(emit_results.len(), 15); + }).await; +} diff --git a/hsmc/tests/det_emit_during_transition.rs b/hsmc/tests/det_emit_during_transition.rs new file mode 100644 index 0000000..e369dc8 --- /dev/null +++ b/hsmc/tests/det_emit_during_transition.rs @@ -0,0 +1,126 @@ +#![allow(dead_code)] +//! Tests that an `emit()` from inside an entry/exit action gets queued +//! BEFORE the transition completes, but is dispatched AFTER. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + Go, + Cleanup, // emitted from A's exit action + Wakeup, // emitted from B's entry action + Halt, +} + +statechart! { + Et { + context: Ctx; + events: Ev; + default(A); + terminate(Halt); + + on(Cleanup) => log_cleanup; + on(Wakeup) => log_wakeup; + + state A { + entry: a_in; + exit: emit_cleanup; + on(Go) => B; + } + state B { + entry: emit_wakeup; + exit: b_out; + } + } +} + +impl EtActions for EtActionContext<'_> { + async fn a_in(&mut self) {} + async fn b_out(&mut self) {} + async fn emit_cleanup(&mut self) { + let _ = self.emit(Ev::Cleanup); + } + async fn emit_wakeup(&mut self) { + let _ = self.emit(Ev::Wakeup); + } + async fn log_cleanup(&mut self) {} + async fn log_wakeup(&mut self) {} +} + +#[tokio::test(flavor = "current_thread")] +async fn det_emit_in_exit_action_runs_after_transition() { + // Spec: emitted events are processed only after the current event has + // fully finished — including all entry/exit actions. + tokio::task::LocalSet::new().run_until(async { + let mut m = Et::new(Ctx); + let _ = m.dispatch(Ev::Go).await; + let j = m.take_journal(); + + // Find indices of EmitQueued for Cleanup, EmitQueued for Wakeup, and + // EventDelivered for each. + // Event ids in interning order: Cleanup=0, Wakeup=1 (root handlers first), + // Go=2 (A handler), Halt=3 (terminate at end of build). + let cleanup_queued = j.iter().position(|e| matches!( + e, TraceEvent::EmitQueued { event: 0 } + )); + let wakeup_queued = j.iter().position(|e| matches!( + e, TraceEvent::EmitQueued { event: 1 } + )); + let cleanup_delivered = j.iter().position(|e| matches!( + e, TraceEvent::EventDelivered { event: 0, .. } + )); + let wakeup_delivered = j.iter().position(|e| matches!( + e, TraceEvent::EventDelivered { event: 1, .. } + )); + + assert!(cleanup_queued.is_some(), "Cleanup must be queued"); + assert!(wakeup_queued.is_some(), "Wakeup must be queued"); + assert!(cleanup_delivered.is_some(), "Cleanup must be delivered"); + assert!(wakeup_delivered.is_some(), "Wakeup must be delivered"); + + // Both emits queue BEFORE either is delivered (no re-entrant dispatch + // inside the original Go transition). + assert!(cleanup_queued.unwrap() < cleanup_delivered.unwrap()); + assert!(wakeup_queued.unwrap() < cleanup_delivered.unwrap(), + "Wakeup queued before Cleanup delivered (transition completes first)"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_emit_in_exit_action_journals_in_order() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Et::new(Ctx); + let _ = m.dispatch(Ev::Go).await; + let j = m.take_journal(); + + // Both Cleanup and Wakeup were queued during the Go transition. They + // are delivered AFTER. Order: Cleanup first (emitted from A's exit + // which runs first), then Wakeup (emitted from B's entry). + let queued_events: Vec = j.iter().filter_map(|e| match e { + TraceEvent::EmitQueued { event } => Some(*event), + _ => None, + }).collect(); + assert_eq!(queued_events, vec![0, 1], "Cleanup (id 0) then Wakeup (id 1)"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_emit_in_transition_byte_deterministic() { + let run = || async { + tokio::task::LocalSet::new().run_until(async { + let mut m = Et::new(Ctx); + let _ = m.dispatch(Ev::Go).await; + m.take_journal() + }).await + }; + let first = run().await; + for i in 1..10 { + assert_eq!(first, run().await, "diverged on run {i}"); + } +} diff --git a/hsmc/tests/det_initial.rs b/hsmc/tests/det_initial.rs new file mode 100644 index 0000000..fde7e63 --- /dev/null +++ b/hsmc/tests/det_initial.rs @@ -0,0 +1,254 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for INITIAL ENTRY and DEFAULT DESCENT. +//! +//! Pins down the semantics from `docs/002. hsmc-semantics-formal.md`, +//! section "Where the machine 'is'": +//! +//! At any moment, the machine is in a path of states from root down to one +//! innermost state. ... The root is always active until the machine +//! terminates. +//! +//! And from "Default child": +//! +//! Whenever a state with children is entered, the default child is entered +//! immediately after that state's entry actions finish — it's effectively +//! an automatic transition into the child. +//! +//! Each test compares the FULL journal to a hand-built EXPECTED sequence. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + Halt, +} + +// 4-level hierarchy: Root → A → B → C → D +statechart! { + Init4 { + context: Ctx; + events: Ev; + + default(A); + terminate(Halt); + + entry: r_in; + exit: r_out; + + state A { + entry: a_in; + exit: a_out; + default(B); + state B { + entry: b_in; + exit: b_out; + default(C); + state C { + entry: c_in; + exit: c_out; + default(D); + state D { + entry: d_in; + exit: d_out; + } + } + } + } + } +} + +impl Init4Actions for Init4ActionContext<'_> { + async fn r_in(&mut self) {} + async fn r_out(&mut self) {} + async fn a_in(&mut self) {} + async fn a_out(&mut self) {} + async fn b_in(&mut self) {} + async fn b_out(&mut self) {} + async fn c_in(&mut self) {} + async fn c_out(&mut self) {} + async fn d_in(&mut self) {} + async fn d_out(&mut self) {} +} + +// State ids: 0=Root, 1=A, 2=B, 3=C, 4=D. +const SR: u16 = 0; +const SA: u16 = 1; +const SB: u16 = 2; +const SC: u16 = 3; +const SD: u16 = 4; +// Action ids in declaration order: 0=r_in, 1=r_out, 2=a_in, 3=a_out, +// 4=b_in, 5=b_out, 6=c_in, 7=c_out, 8=d_in, 9=d_out. +const A_R_IN: u16 = 0; +const A_R_OUT: u16 = 1; +const A_A_IN: u16 = 2; +const A_A_OUT: u16 = 3; +const A_B_IN: u16 = 4; +const A_B_OUT: u16 = 5; +const A_C_IN: u16 = 6; +const A_C_OUT: u16 = 7; +const A_D_IN: u16 = 8; +const A_D_OUT: u16 = 9; +// Halt = event 0 (interned via `terminate(Halt)`). +const E_HALT: u16 = 0; + +fn entry(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Entry } +} +fn exit_(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Exit } +} + +#[tokio::test(flavor = "current_thread")] +async fn det_initial_descent_records_full_path() { + // Spec: "the root is always active" + default-descent unrolls Root → A → B → C → D. + tokio::task::LocalSet::new().run_until(async { + let mut m = Init4::new(Ctx); + // Push Halt to drive the chart through initial entry then termination. + let _ = m.dispatch(Ev::Halt).await; + + let actual = m.take_journal(); + let expected = vec![ + // Initial enter (driven by dispatch's prime-state branch). + TraceEvent::Started { chart_hash: Init4::<8>::CHART_HASH }, + TraceEvent::Entered { state: SR }, + entry(SR, A_R_IN), + TraceEvent::Entered { state: SA }, + entry(SA, A_A_IN), + TraceEvent::Entered { state: SB }, + entry(SB, A_B_IN), + TraceEvent::Entered { state: SC }, + entry(SC, A_C_IN), + TraceEvent::Entered { state: SD }, + entry(SD, A_D_IN), + // Halt. + TraceEvent::TerminateRequested { event: E_HALT }, + // Bottom-up exit chain. + exit_(SD, A_D_OUT), + TraceEvent::Exited { state: SD }, + exit_(SC, A_C_OUT), + TraceEvent::Exited { state: SC }, + exit_(SB, A_B_OUT), + TraceEvent::Exited { state: SB }, + exit_(SA, A_A_OUT), + TraceEvent::Exited { state: SA }, + exit_(SR, A_R_OUT), + TraceEvent::Exited { state: SR }, + TraceEvent::Terminated, + ]; + + let mismatch = actual.iter().zip(expected.iter()) + .position(|(a, e)| a != e) + .map(|i| i.to_string()) + .unwrap_or_else(|| "".to_string()); + assert_eq!(actual, expected, "first mismatch at index {mismatch}"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_started_is_first_event() { + // Spec: every journal begins with Started carrying the chart hash. + tokio::task::LocalSet::new().run_until(async { + let mut m = Init4::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let j = m.journal(); + assert!(matches!(j[0], TraceEvent::Started { .. })); + if let TraceEvent::Started { chart_hash } = j[0] { + assert_eq!(chart_hash, Init4::<8>::CHART_HASH); + } + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_chart_hash_nonzero() { + // The FNV-1a fingerprint must actually have run. + assert_ne!(Init4::<8>::CHART_HASH, 0); +} + +#[tokio::test(flavor = "current_thread")] +async fn det_root_state_id_is_zero() { + // Spec: "the root state (the machine itself) is just a state". It's + // allocated first and so gets id 0; tests below depend on this. + tokio::task::LocalSet::new().run_until(async { + let mut m = Init4::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + // First Entered event must be state 0. + let first_entered = m.journal().iter().find(|e| matches!(e, TraceEvent::Entered { .. })); + assert!(matches!(first_entered, Some(TraceEvent::Entered { state: 0 }))); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_entry_actions_fire_outer_to_inner() { + // Spec: "Entry runs outer-to-inner." + tokio::task::LocalSet::new().run_until(async { + let mut m = Init4::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let entered: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { state, kind: ActionKind::Entry, .. } => Some(*state), + _ => None, + }).collect(); + assert_eq!(entered, vec![SR, SA, SB, SC, SD], + "entry actions must fire outer-to-inner across hierarchy"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_exit_actions_fire_inner_to_outer() { + // Spec: "Exit runs inner-to-outer." + tokio::task::LocalSet::new().run_until(async { + let mut m = Init4::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let exited: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { state, kind: ActionKind::Exit, .. } => Some(*state), + _ => None, + }).collect(); + assert_eq!(exited, vec![SD, SC, SB, SA, SR], + "exit actions must fire inner-to-outer across hierarchy"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_state_ids_are_declaration_order() { + // Spec: state ids assigned in parse order (0=root, then nested). + // Verify by checking the order Entered events appear. + tokio::task::LocalSet::new().run_until(async { + let mut m = Init4::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let entered_ids: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::Entered { state } => Some(*state), + _ => None, + }).collect(); + assert_eq!(entered_ids, vec![SR, SA, SB, SC, SD]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_initial_descent_byte_deterministic_across_runs() { + let run = || async { + tokio::task::LocalSet::new().run_until(async { + let mut m = Init4::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + m.take_journal() + }).await + }; + let first = run().await; + for i in 1..20 { + assert_eq!(first, run().await, "divergence on run {i}"); + } +} + +#[tokio::test(flavor = "current_thread")] +async fn det_terminated_is_last_event() { + // Spec: "Always the final event in the journal." + tokio::task::LocalSet::new().run_until(async { + let mut m = Init4::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + assert!(matches!(m.journal().last(), Some(TraceEvent::Terminated))); + }).await; +} diff --git a/hsmc/tests/det_lateral.rs b/hsmc/tests/det_lateral.rs new file mode 100644 index 0000000..5543c22 --- /dev/null +++ b/hsmc/tests/det_lateral.rs @@ -0,0 +1,368 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for LATERAL transitions (target not on active path). +//! +//! Spec section "Transitioning to a sibling (or anywhere not on your active path)": +//! The standard case. LCA is somewhere strictly above both current and +//! target. Exit up to LCA, enter down to target, default-descend if the +//! target has children. +//! +//! Also pins down that the LCA itself is **not** exited or re-entered. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + GoB, + GoC, + GoD, + GoE, + Halt, +} + +// Hierarchy: +// Root +// ├── Parent +// │ ├── A (default) +// │ └── B +// ├── C +// └── D +// └── E +statechart! { + Lat { + context: Ctx; + events: Ev; + default(Parent); + terminate(Halt); + + state Parent { + entry: p_in; + exit: p_out; + default(A); + state A { + entry: a_in; + exit: a_out; + on(GoB) => B; + on(GoC) => C; + on(GoD) => D; + on(GoE) => E; + } + state B { + entry: b_in; + exit: b_out; + on(GoC) => C; + } + } + state C { + entry: c_in; + exit: c_out; + } + state D { + entry: d_in; + exit: d_out; + default(E); + state E { + entry: e_in; + exit: e_out; + } + } + } +} + +impl LatActions for LatActionContext<'_> { + async fn p_in(&mut self) {} + async fn p_out(&mut self) {} + async fn a_in(&mut self) {} + async fn a_out(&mut self) {} + async fn b_in(&mut self) {} + async fn b_out(&mut self) {} + async fn c_in(&mut self) {} + async fn c_out(&mut self) {} + async fn d_in(&mut self) {} + async fn d_out(&mut self) {} + async fn e_in(&mut self) {} + async fn e_out(&mut self) {} +} + +// State ids: 0=Root, 1=Parent, 2=A, 3=B, 4=C, 5=D, 6=E. +const SR: u16 = 0; +const SP: u16 = 1; +const SA: u16 = 2; +const SB: u16 = 3; +const SC: u16 = 4; +const SD: u16 = 5; +const SE: u16 = 6; +// Action ids in declaration order: 0=p_in, 1=p_out, 2=a_in, 3=a_out, +// 4=b_in, 5=b_out, 6=c_in, 7=c_out, 8=d_in, 9=d_out, 10=e_in, 11=e_out. +const A_P_IN: u16 = 0; +const A_P_OUT: u16 = 1; +const A_A_IN: u16 = 2; +const A_A_OUT: u16 = 3; +const A_B_IN: u16 = 4; +const A_B_OUT: u16 = 5; +const A_C_IN: u16 = 6; +const A_C_OUT: u16 = 7; +const A_D_IN: u16 = 8; +const A_D_OUT: u16 = 9; +const A_E_IN: u16 = 10; +const A_E_OUT: u16 = 11; +// Event ids in first-seen order: 0=GoB, 1=GoC, 2=GoD, 3=GoE, 4=Halt. +const E_GOB: u16 = 0; +const E_GOC: u16 = 1; +const E_GOD: u16 = 2; +const E_GOE: u16 = 3; + +fn entry(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Entry } +} +fn exit_(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Exit } +} +#[allow(dead_code)] +fn handler(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Handler } +} + +// Initial descent: Root → Parent → A. +fn initial_descent() -> Vec { + vec![ + TraceEvent::Started { chart_hash: Lat::<8>::CHART_HASH }, + TraceEvent::Entered { state: SR }, + TraceEvent::Entered { state: SP }, + entry(SP, A_P_IN), + TraceEvent::Entered { state: SA }, + entry(SA, A_A_IN), + ] +} + +// Compare actual vs expected and report first mismatch. +fn assert_journal(actual: &[TraceEvent], expected: &[TraceEvent]) { + let mismatch = actual.iter().zip(expected.iter()) + .position(|(a, e)| a != e); + if let Some(i) = mismatch { + panic!( + "journal mismatch at index {}\n actual: {:?}\n expected: {:?}\n full actual: {:#?}", + i, actual[i], expected[i], actual + ); + } + assert_eq!(actual.len(), expected.len(), + "journal length mismatch: actual {} vs expected {}\n full actual: {:#?}", + actual.len(), expected.len(), actual); +} + +#[tokio::test(flavor = "current_thread")] +async fn det_lateral_a_to_b_lca_is_parent() { + // Spec: A → B (siblings under Parent). LCA = Parent. Parent is not exited + // or re-entered. + tokio::task::LocalSet::new().run_until(async { + let mut m = Lat::new(Ctx); + let _ = m.dispatch(Ev::GoB).await; + let actual = m.take_journal(); + + let mut expected = initial_descent(); + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SA, event: E_GOB }, + TraceEvent::TransitionFired { from: Some(SA), to: SB }, + exit_(SA, A_A_OUT), + TraceEvent::Exited { state: SA }, + TraceEvent::Entered { state: SB }, + entry(SB, A_B_IN), + ]); + assert_journal(&actual, &expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_lateral_a_to_c_exits_parent() { + // A → C: A is inside Parent, C is sibling of Parent. LCA = Root. + // Exit A, exit Parent. Enter C. + tokio::task::LocalSet::new().run_until(async { + let mut m = Lat::new(Ctx); + let _ = m.dispatch(Ev::GoC).await; + let actual = m.take_journal(); + + let mut expected = initial_descent(); + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SA, event: E_GOC }, + TraceEvent::TransitionFired { from: Some(SA), to: SC }, + exit_(SA, A_A_OUT), + TraceEvent::Exited { state: SA }, + exit_(SP, A_P_OUT), + TraceEvent::Exited { state: SP }, + TraceEvent::Entered { state: SC }, + entry(SC, A_C_IN), + ]); + assert_journal(&actual, &expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_lateral_target_with_children_default_descends() { + // A → D: D has child E (default). After entering D, default-descend to E. + tokio::task::LocalSet::new().run_until(async { + let mut m = Lat::new(Ctx); + let _ = m.dispatch(Ev::GoD).await; + let actual = m.take_journal(); + + let mut expected = initial_descent(); + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SA, event: E_GOD }, + TraceEvent::TransitionFired { from: Some(SA), to: SD }, + exit_(SA, A_A_OUT), + TraceEvent::Exited { state: SA }, + exit_(SP, A_P_OUT), + TraceEvent::Exited { state: SP }, + TraceEvent::Entered { state: SD }, + entry(SD, A_D_IN), + TraceEvent::Entered { state: SE }, + entry(SE, A_E_IN), + ]); + assert_journal(&actual, &expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_lateral_to_deeply_nested_target() { + // A → E (E is the leaf of D's default chain). The target itself is the leaf + // so default-descent doesn't add another level — but D is entered along the way. + tokio::task::LocalSet::new().run_until(async { + let mut m = Lat::new(Ctx); + let _ = m.dispatch(Ev::GoE).await; + let actual = m.take_journal(); + + let mut expected = initial_descent(); + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SA, event: E_GOE }, + TraceEvent::TransitionFired { from: Some(SA), to: SE }, + exit_(SA, A_A_OUT), + TraceEvent::Exited { state: SA }, + exit_(SP, A_P_OUT), + TraceEvent::Exited { state: SP }, + TraceEvent::Entered { state: SD }, + entry(SD, A_D_IN), + TraceEvent::Entered { state: SE }, + entry(SE, A_E_IN), + ]); + assert_journal(&actual, &expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_lateral_chained_transitions() { + // A → B → C: two consecutive transitions. Each independently records its + // exits and entries. + tokio::task::LocalSet::new().run_until(async { + let mut m = Lat::new(Ctx); + let _ = m.dispatch(Ev::GoB).await; + let _ = m.dispatch(Ev::GoC).await; + let actual = m.take_journal(); + + let mut expected = initial_descent(); + // A → B + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SA, event: E_GOB }, + TraceEvent::TransitionFired { from: Some(SA), to: SB }, + exit_(SA, A_A_OUT), + TraceEvent::Exited { state: SA }, + TraceEvent::Entered { state: SB }, + entry(SB, A_B_IN), + ]); + // B → C (LCA = Root, so Parent exits too). + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SB, event: E_GOC }, + TraceEvent::TransitionFired { from: Some(SB), to: SC }, + exit_(SB, A_B_OUT), + TraceEvent::Exited { state: SB }, + exit_(SP, A_P_OUT), + TraceEvent::Exited { state: SP }, + TraceEvent::Entered { state: SC }, + entry(SC, A_C_IN), + ]); + assert_journal(&actual, &expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_lateral_lca_stays_active() { + // A → B: Parent (the LCA) must NOT appear in any Exited or Entered event. + tokio::task::LocalSet::new().run_until(async { + let mut m = Lat::new(Ctx); + let _ = m.dispatch(Ev::GoB).await; + let j = m.take_journal(); + // After initial Entered(Parent), Parent must not appear again. + let parent_events: Vec<&TraceEvent> = j.iter().skip(3).filter(|e| matches!( + e, + TraceEvent::Entered { state: SP } | TraceEvent::Exited { state: SP } + )).collect(); + assert!(parent_events.is_empty(), + "LCA Parent must not be re-entered or exited; got: {:?}", parent_events); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_lateral_exit_inner_then_outer() { + // A → C: exit A first (deeper), then Parent (outer). + tokio::task::LocalSet::new().run_until(async { + let mut m = Lat::new(Ctx); + let _ = m.dispatch(Ev::GoC).await; + let exits: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::Exited { state } => Some(*state), + _ => None, + }).collect(); + // First exit must be A (deeper), then Parent (outer). + assert_eq!(&exits[..2], &[SA, SP], "exits must be inner-to-outer"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_lateral_entry_outer_then_inner() { + // A → D where D has child E: enter D first, then E. + tokio::task::LocalSet::new().run_until(async { + let mut m = Lat::new(Ctx); + let _ = m.dispatch(Ev::GoD).await; + let entries: Vec = m.journal().iter().skip_while(|e| !matches!( + e, + TraceEvent::TransitionFired { .. } + )).filter_map(|e| match e { + TraceEvent::Entered { state } => Some(*state), + _ => None, + }).collect(); + assert_eq!(&entries, &[SD, SE], "entries on the way down must be outer-to-inner"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_lateral_no_default_when_target_is_leaf() { + // A → C where C is a leaf: no default-descent, journal stops at C. + tokio::task::LocalSet::new().run_until(async { + let mut m = Lat::new(Ctx); + let _ = m.dispatch(Ev::GoC).await; + let last_entered: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::Entered { state } => Some(*state), + _ => None, + }).collect(); + // Initial: Root, Parent, A. After GoC: C. No further entries. + assert_eq!(last_entered, vec![SR, SP, SA, SC]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_lateral_event_delivered_records_handler_state() { + // The handler for GoB lives on A. EventDelivered.handler_state = A. + tokio::task::LocalSet::new().run_until(async { + let mut m = Lat::new(Ctx); + let _ = m.dispatch(Ev::GoB).await; + let delivered = m.journal().iter().find(|e| matches!( + e, TraceEvent::EventDelivered { event: E_GOB, .. } + )); + assert!(matches!( + delivered, + Some(TraceEvent::EventDelivered { handler_state: SA, event: E_GOB }) + ), "got: {:?}", delivered); + }).await; +} diff --git a/hsmc/tests/det_ordering.rs b/hsmc/tests/det_ordering.rs new file mode 100644 index 0000000..f0071d2 --- /dev/null +++ b/hsmc/tests/det_ordering.rs @@ -0,0 +1,235 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for ENTRY/EXIT ORDERING (declaration order, depth order). +//! +//! Spec section "Entry and exit ordering": +//! Entry runs outer-to-inner. Within a single state, entry actions fire in +//! declaration order. Exit runs inner-to-outer. Within a single state, exit +//! actions fire in declaration order. +//! +//! Spec: "If a single state has multiple handlers (actions and/or a transition) +//! for the same trigger, the actions fire in declaration order, then the +//! transition fires last." + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + Go, + Multi, + Halt, +} + +statechart! { + Ord { + context: Ctx; + events: Ev; + default(A); + terminate(Halt); + + entry: r1, r2, r3; + exit: r_x1, r_x2; + + state A { + entry: a1, a2; + exit: a_x1, a_x2, a_x3; + on(Go) => B; + on(Multi) => act1; + on(Multi) => act2; + on(Multi) => act3; + on(Multi) => B; + } + state B { + entry: b1; + exit: b_x1; + } + } +} + +impl OrdActions for OrdActionContext<'_> { + async fn r1(&mut self) {} + async fn r2(&mut self) {} + async fn r3(&mut self) {} + async fn r_x1(&mut self) {} + async fn r_x2(&mut self) {} + async fn a1(&mut self) {} + async fn a2(&mut self) {} + async fn a_x1(&mut self) {} + async fn a_x2(&mut self) {} + async fn a_x3(&mut self) {} + async fn b1(&mut self) {} + async fn b_x1(&mut self) {} + async fn act1(&mut self) {} + async fn act2(&mut self) {} + async fn act3(&mut self) {} +} + +const SR: u16 = 0; +const SA: u16 = 1; +const SB: u16 = 2; + +// Action interning order from declaration: +// Root: r1=0, r2=1, r3=2 (entries), r_x1=3, r_x2=4 (exits) +// A: a1=5, a2=6, a_x1=7, a_x2=8, a_x3=9, then handlers act1=10, act2=11, act3=12 +// B: b1=13, b_x1=14 +const A_R1: u16 = 0; +const A_R2: u16 = 1; +const A_R3: u16 = 2; +const A_RX1: u16 = 3; +const A_RX2: u16 = 4; +const A_A1: u16 = 5; +const A_A2: u16 = 6; +const A_AX1: u16 = 7; +const A_AX2: u16 = 8; +const A_AX3: u16 = 9; +const A_ACT1: u16 = 10; +const A_ACT2: u16 = 11; +const A_ACT3: u16 = 12; +const A_B1: u16 = 13; +const A_BX1: u16 = 14; + +#[tokio::test(flavor = "current_thread")] +async fn det_ord_root_entries_in_declaration_order() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Ord::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + // Filter to root entry actions in journal order. + let r_entries: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { state: SR, action, kind: ActionKind::Entry } => Some(*action), + _ => None, + }).collect(); + assert_eq!(r_entries, vec![A_R1, A_R2, A_R3]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_ord_root_exits_in_declaration_order() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Ord::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let r_exits: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { state: SR, action, kind: ActionKind::Exit } => Some(*action), + _ => None, + }).collect(); + assert_eq!(r_exits, vec![A_RX1, A_RX2]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_ord_state_a_entries_in_declaration_order() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Ord::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let a_entries: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { state: SA, action, kind: ActionKind::Entry } => Some(*action), + _ => None, + }).collect(); + assert_eq!(a_entries, vec![A_A1, A_A2]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_ord_state_a_exits_in_declaration_order() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Ord::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let a_exits: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { state: SA, action, kind: ActionKind::Exit } => Some(*action), + _ => None, + }).collect(); + assert_eq!(a_exits, vec![A_AX1, A_AX2, A_AX3]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_ord_entry_outer_then_inner_across_hierarchy() { + // Initial entry: Root → A. Root's entries fire first, then A's. + tokio::task::LocalSet::new().run_until(async { + let mut m = Ord::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let entries_in_order: Vec = m.journal().iter().take_while(|e| !matches!( + e, TraceEvent::TerminateRequested { .. } + )).filter_map(|e| match e { + TraceEvent::ActionInvoked { action, kind: ActionKind::Entry, .. } => Some(*action), + _ => None, + }).collect(); + assert_eq!(entries_in_order, vec![A_R1, A_R2, A_R3, A_A1, A_A2]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_ord_exit_inner_then_outer_across_hierarchy() { + // On terminate: A's exits then Root's exits. + tokio::task::LocalSet::new().run_until(async { + let mut m = Ord::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let exits_in_order: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { action, kind: ActionKind::Exit, .. } => Some(*action), + _ => None, + }).collect(); + assert_eq!(exits_in_order, vec![A_AX1, A_AX2, A_AX3, A_RX1, A_RX2]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_ord_actions_then_transition_on_same_trigger() { + // Multi: act1, act2, act3 fire in declaration order, then transition to B. + tokio::task::LocalSet::new().run_until(async { + let mut m = Ord::new(Ctx); + let _ = m.dispatch(Ev::Multi).await; + let j = m.take_journal(); + + // Find the action invocations and the TransitionFired in order. + let after_delivered: Vec<&TraceEvent> = j.iter() + .skip_while(|e| !matches!(e, TraceEvent::EventDelivered { event: 1, .. })) + // Multi is the second event: Go=0, Multi=1. + .skip(1) + .take(20) + .collect(); + // First three should be Handler actions in order act1, act2, act3. + let handler_actions: Vec = after_delivered.iter().take_while(|e| matches!( + e, TraceEvent::ActionInvoked { kind: ActionKind::Handler, .. } + )).filter_map(|e| match e { + TraceEvent::ActionInvoked { action, .. } => Some(*action), + _ => None, + }).collect(); + assert_eq!(handler_actions, vec![A_ACT1, A_ACT2, A_ACT3], + "actions in declaration order"); + // After the actions, a TransitionFired must follow. + let trans_idx = after_delivered.iter().position(|e| matches!( + e, TraceEvent::TransitionFired { .. } + )).unwrap(); + assert_eq!(trans_idx, 3, "transition fires after the 3 actions"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_ord_full_transition_canonical_sequence() { + // Spec: cancel durings → run exits inner→outer → run entries outer→inner → start durings. + // No durings here, so just exits inner→outer + entries outer→inner. + tokio::task::LocalSet::new().run_until(async { + let mut m = Ord::new(Ctx); + let _ = m.dispatch(Ev::Go).await; + let j = m.take_journal(); + // Find the TransitionFired and capture everything until A's exit and B's entry are done. + let trans_idx = j.iter().position(|e| matches!(e, TraceEvent::TransitionFired { .. })).unwrap(); + let kinds: Vec = j[trans_idx..].iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { kind, .. } => Some(*kind), + _ => None, + }).collect(); + // First A's exit kinds (inner-to-outer order — A is innermost), then B's entry kinds. + let exit_count = kinds.iter().filter(|k| **k == ActionKind::Exit).count(); + let entry_count = kinds.iter().filter(|k| **k == ActionKind::Entry).count(); + assert_eq!(exit_count, 3, "A has 3 exit actions"); + assert_eq!(entry_count, 1, "B has 1 entry action"); + // Exits before entries. + let first_entry = kinds.iter().position(|k| *k == ActionKind::Entry).unwrap(); + let last_exit = kinds.iter().rposition(|k| *k == ActionKind::Exit).unwrap(); + assert!(last_exit < first_entry, "all exits must precede all entries in a transition"); + }).await; +} diff --git a/hsmc/tests/det_root_target.rs b/hsmc/tests/det_root_target.rs new file mode 100644 index 0000000..aecef2b --- /dev/null +++ b/hsmc/tests/det_root_target.rs @@ -0,0 +1,142 @@ +#![allow(dead_code)] +//! Pins down that the ROOT state is targetable by the chart's own name. +//! +//! Spec section "What a chart contains": +//! State — a named node. The root state (the machine itself) is just a +//! state. Every state is just a state. +//! +//! Spec section "How transitions work": +//! The target can be any state in the entire chart. ... state names must +//! be unique across the chart. +//! +//! From these two together: `on(Trig) => ;` is a valid transition +//! whose target is the root. From a leaf, this is an up-transition; from any +//! state inside the chart it's an up-transition (root is always on the active +//! path) — exiting only the states strictly between current and root. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + UpToRoot, + Halt, +} + +statechart! { + Sub { + context: Ctx; + events: Ev; + default(A); + terminate(Halt); + + entry: r_in; + exit: r_out; + + state A { + entry: a_in; + exit: a_out; + default(B); + state B { + entry: b_in; + exit: b_out; + on(UpToRoot) => Sub; // ← target is the chart name = root + } + } + } +} + +impl SubActions for SubActionContext<'_> { + async fn r_in(&mut self) {} + async fn r_out(&mut self) {} + async fn a_in(&mut self) {} + async fn a_out(&mut self) {} + async fn b_in(&mut self) {} + async fn b_out(&mut self) {} +} + +const SR: u16 = 0; +const SA: u16 = 1; +const SB: u16 = 2; +const A_R_IN: u16 = 0; +const A_R_OUT: u16 = 1; +const A_A_IN: u16 = 2; +const A_A_OUT: u16 = 3; +const A_B_IN: u16 = 4; +const A_B_OUT: u16 = 5; +const E_UPTOROOT: u16 = 0; + +fn entry(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Entry } +} +fn exit_(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Exit } +} + +#[tokio::test(flavor = "current_thread")] +async fn det_root_targetable_by_chart_name() { + // Chart compiles. Targeting root by chart name resolves correctly. + tokio::task::LocalSet::new().run_until(async { + let mut m = Sub::new(Ctx); + let _ = m.dispatch(Ev::UpToRoot).await; + let actual = m.take_journal(); + + // Up-transition to root from B: exit B and A. Root is target, + // not exited, not re-entered, no default-descent. + let expected = vec![ + TraceEvent::Started { chart_hash: Sub::<8>::CHART_HASH }, + TraceEvent::Entered { state: SR }, + entry(SR, A_R_IN), + TraceEvent::Entered { state: SA }, + entry(SA, A_A_IN), + TraceEvent::Entered { state: SB }, + entry(SB, A_B_IN), + TraceEvent::EventDelivered { handler_state: SB, event: E_UPTOROOT }, + TraceEvent::TransitionFired { from: Some(SB), to: SR }, + exit_(SB, A_B_OUT), + TraceEvent::Exited { state: SB }, + exit_(SA, A_A_OUT), + TraceEvent::Exited { state: SA }, + ]; + + assert_eq!(actual, expected, "root targetable; up-transition to root exits A and B only"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_root_target_does_not_re_enter_root() { + // After the up-to-root, root must NOT have re-entered. + tokio::task::LocalSet::new().run_until(async { + let mut m = Sub::new(Ctx); + let _ = m.dispatch(Ev::UpToRoot).await; + let j = m.take_journal(); + // After the TransitionFired, no Entered event should fire. + let split = j.iter().position(|e| matches!(e, TraceEvent::TransitionFired { .. })).unwrap(); + let entered_after = j[split..].iter().filter(|e| matches!(e, TraceEvent::Entered { .. })).count(); + assert_eq!(entered_after, 0, "up-to-root must not re-enter root or default-descend"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_root_target_then_terminate() { + // After up-to-root, root is the innermost active state. Terminate exits root only. + tokio::task::LocalSet::new().run_until(async { + let mut m = Sub::new(Ctx); + let _ = m.dispatch(Ev::UpToRoot).await; + let _ = m.dispatch(Ev::Halt).await; + let j = m.take_journal(); + // After UpToRoot we're in root only. Halt exits root only. + let exits: Vec = j.iter().filter_map(|e| match e { + TraceEvent::Exited { state } => Some(*state), + _ => None, + }).collect(); + assert_eq!(exits, vec![SB, SA, SR], + "up-to-root exits B, A; terminate exits root"); + assert!(matches!(j.last(), Some(TraceEvent::Terminated))); + }).await; +} diff --git a/hsmc/tests/det_self.rs b/hsmc/tests/det_self.rs new file mode 100644 index 0000000..21413d3 --- /dev/null +++ b/hsmc/tests/det_self.rs @@ -0,0 +1,234 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for SELF-TRANSITIONS. +//! +//! Spec section "Transitioning to yourself": +//! The standard transition algorithm gives the clean answer: the LCA of the +//! target with itself is its parent, so we exit only the target and re-enter +//! only the target. Nothing above the target is exited or re-entered. +//! +//! Concrete example given in spec: in `Root → SomeState → SomeOtherState`, +//! a transition (Trig) => SomeOtherState exits and re-enters ONLY +//! SomeOtherState; SomeState is never touched. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + SelfLeaf, + SelfMid, + Halt, +} + +// Hierarchy: Root → Mid → Leaf +// Self-transitions: SelfLeaf targets Leaf; SelfMid targets Mid. +statechart! { + Self_ { + context: Ctx; + events: Ev; + default(Mid); + terminate(Halt); + + state Mid { + entry: m_in; + exit: m_out; + default(Leaf); + on(SelfMid) => Mid; + state Leaf { + entry: l_in; + exit: l_out; + on(SelfLeaf) => Leaf; + } + } + } +} + +impl Self_Actions for Self_ActionContext<'_> { + async fn m_in(&mut self) {} + async fn m_out(&mut self) {} + async fn l_in(&mut self) {} + async fn l_out(&mut self) {} +} + +const SR: u16 = 0; +const SM: u16 = 1; +const SL: u16 = 2; +const A_M_IN: u16 = 0; +const A_M_OUT: u16 = 1; +const A_L_IN: u16 = 2; +const A_L_OUT: u16 = 3; +// Event interning order: handlers on the parent (Mid) are processed before +// recursing into children (Leaf), so SelfMid is interned first. +const E_SELFMID: u16 = 0; +const E_SELFLEAF: u16 = 1; + +fn entry(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Entry } +} +fn exit_(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Exit } +} +fn initial_descent() -> Vec { + vec![ + TraceEvent::Started { chart_hash: Self_::<8>::CHART_HASH }, + TraceEvent::Entered { state: SR }, + TraceEvent::Entered { state: SM }, + entry(SM, A_M_IN), + TraceEvent::Entered { state: SL }, + entry(SL, A_L_IN), + ] +} +fn assert_journal(actual: &[TraceEvent], expected: &[TraceEvent]) { + let mismatch = actual.iter().zip(expected.iter()) + .position(|(a, e)| a != e); + if let Some(i) = mismatch { + panic!("mismatch at index {}\n actual: {:?}\n expected: {:?}", + i, actual.get(i), expected.get(i)); + } + assert_eq!(actual.len(), expected.len(), + "length mismatch: actual {} vs expected {}", actual.len(), expected.len()); +} + +#[tokio::test(flavor = "current_thread")] +async fn det_self_leaf_exits_and_reenters_only_leaf() { + // Spec: nothing above the target is touched. + tokio::task::LocalSet::new().run_until(async { + let mut m = Self_::new(Ctx); + let _ = m.dispatch(Ev::SelfLeaf).await; + let actual = m.take_journal(); + + let mut expected = initial_descent(); + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SL, event: E_SELFLEAF }, + TraceEvent::TransitionFired { from: Some(SL), to: SL }, + exit_(SL, A_L_OUT), + TraceEvent::Exited { state: SL }, + TraceEvent::Entered { state: SL }, + entry(SL, A_L_IN), + ]); + assert_journal(&actual, &expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_self_leaf_does_not_touch_parent() { + // The key spec example. Mid must NOT appear in any Exited or Entered + // event after the initial descent. + tokio::task::LocalSet::new().run_until(async { + let mut m = Self_::new(Ctx); + let _ = m.dispatch(Ev::SelfLeaf).await; + let j = m.take_journal(); + + // Find the index of the EventDelivered for SelfLeaf — everything + // after that is the self-transition body. + let split = j.iter().position(|e| matches!( + e, TraceEvent::EventDelivered { event: E_SELFLEAF, .. } + )).unwrap(); + + let parent_after = j[split..].iter().filter(|e| matches!( + e, + TraceEvent::Entered { state: SM } | TraceEvent::Exited { state: SM } + )).count(); + assert_eq!(parent_after, 0, + "Mid must not be exited or re-entered during self-transition on Leaf; got tail: {:?}", + &j[split..]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_self_composite_default_descends() { + // Spec: "If the target happens to be a composite ... the same default-child + // rule still applies on re-entry: exit the composite, re-enter it, then + // descend through its default chain to a leaf." + // + // Currently in Mid via Leaf default. SelfMid bubbles from Leaf to Mid (Mid + // has the handler). At dispatch time, innermost is Leaf, so Mid is not + // the innermost — that makes it an UP-then-self situation. Actually the + // transition algorithm classifies it: target=Mid, current=Leaf, target IS + // on the active path and target ≠ I, so this is an UP-transition not a + // self-transition. Let's verify what the journal records. + // + // (See det_up.rs for explicit up-transition tests; this test pins the + // bubbling behavior when the handler is on Mid but the transition is to + // Mid itself from Leaf.) + tokio::task::LocalSet::new().run_until(async { + let mut m = Self_::new(Ctx); + let _ = m.dispatch(Ev::SelfMid).await; + let actual = m.take_journal(); + + // Per spec rules: target=Mid is ON the active path (Root→Mid→Leaf), + // and target ≠ Leaf. So it's an UP-transition: only Leaf exits. + // Mid's entry actions don't fire. No default-descent. + let mut expected = initial_descent(); + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SM, event: E_SELFMID }, + TraceEvent::TransitionFired { from: Some(SL), to: SM }, + exit_(SL, A_L_OUT), + TraceEvent::Exited { state: SL }, + ]); + assert_journal(&actual, &expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_self_leaf_repeated_is_deterministic() { + // Multiple self-transitions: each independently records the same pattern. + tokio::task::LocalSet::new().run_until(async { + let mut m = Self_::new(Ctx); + let _ = m.dispatch(Ev::SelfLeaf).await; + let _ = m.dispatch(Ev::SelfLeaf).await; + let _ = m.dispatch(Ev::SelfLeaf).await; + let j = m.take_journal(); + // Three EventDelivered for SelfLeaf, three TransitionFired, three of each + // exit/entry pair. + let delivered = j.iter().filter(|e| matches!( + e, TraceEvent::EventDelivered { event: E_SELFLEAF, .. } + )).count(); + assert_eq!(delivered, 3); + let trans = j.iter().filter(|e| matches!( + e, TraceEvent::TransitionFired { from: Some(SL), to: SL } + )).count(); + assert_eq!(trans, 3); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_self_byte_deterministic_across_runs() { + let run = || async { + tokio::task::LocalSet::new().run_until(async { + let mut m = Self_::new(Ctx); + let _ = m.dispatch(Ev::SelfLeaf).await; + let _ = m.dispatch(Ev::SelfLeaf).await; + m.take_journal() + }).await + }; + let first = run().await; + for i in 1..10 { + assert_eq!(first, run().await, "run {i} diverged"); + } +} + +#[tokio::test(flavor = "current_thread")] +async fn det_self_action_kinds_are_exit_then_entry() { + // Spec: "cancel durings, run exits, run entries, start durings". + // No durings on this chart, so we expect: Exit kind action, then Entry kind action. + tokio::task::LocalSet::new().run_until(async { + let mut m = Self_::new(Ctx); + let _ = m.dispatch(Ev::SelfLeaf).await; + let j = m.take_journal(); + let split = j.iter().position(|e| matches!( + e, TraceEvent::EventDelivered { event: E_SELFLEAF, .. } + )).unwrap(); + let kinds_after: Vec = j[split..].iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { kind, .. } => Some(*kind), + _ => None, + }).collect(); + assert_eq!(kinds_after, vec![ActionKind::Exit, ActionKind::Entry], + "self-transition: exit before entry"); + }).await; +} diff --git a/hsmc/tests/det_self_composite.rs b/hsmc/tests/det_self_composite.rs new file mode 100644 index 0000000..1518d78 --- /dev/null +++ b/hsmc/tests/det_self_composite.rs @@ -0,0 +1,135 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for SELF-TRANSITION on a composite (re-enters with default-descend). +//! +//! Spec section "Transitioning to yourself": +//! If the target happens to be a composite (it has children, but no child is +//! active right now because you got there via an up-transition), the same +//! default-child rule still applies on re-entry: exit the composite, +//! re-enter it, then descend through its default chain to a leaf. +//! +//! To get a composite as the innermost active state, this chart uses: +//! 1. UpToParent (D → Parent) → Parent is now innermost composite. +//! 2. SelfMid (Parent → Parent) → exit Parent, re-enter Parent, default-descend. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + UpToParent, // D → Parent (up-transition) + SelfParent, // Parent → Parent (self-transition on composite) + Halt, +} + +statechart! { + Sc { + context: Ctx; + events: Ev; + default(Parent); + terminate(Halt); + + state Parent { + entry: p_in; + exit: p_out; + default(Child); + on(SelfParent) => Parent; + state Child { + entry: c_in; + exit: c_out; + default(Leaf); + state Leaf { + entry: l_in; + exit: l_out; + on(UpToParent) => Parent; + } + } + } + } +} + +impl ScActions for ScActionContext<'_> { + async fn p_in(&mut self) {} + async fn p_out(&mut self) {} + async fn c_in(&mut self) {} + async fn c_out(&mut self) {} + async fn l_in(&mut self) {} + async fn l_out(&mut self) {} +} + +const SR: u16 = 0; +const SP: u16 = 1; +const SC: u16 = 2; +const SL: u16 = 3; + +#[tokio::test(flavor = "current_thread")] +async fn det_self_composite_default_descends_after_re_entry() { + // Path: initial → Leaf. UpToParent → Parent (up). SelfParent → exit Parent, + // re-enter Parent, default-descend (Parent → Child → Leaf). + tokio::task::LocalSet::new().run_until(async { + let mut m = Sc::new(Ctx); + let _ = m.dispatch(Ev::UpToParent).await; + let _ = m.dispatch(Ev::SelfParent).await; + let j = m.take_journal(); + + // After SelfParent, expect: exit Parent → re-enter Parent → enter Child → enter Leaf. + let self_idx = j.iter().rposition(|e| matches!( + e, TraceEvent::TransitionFired { from: Some(SP), to: SP } + )).unwrap(); + let after = &j[self_idx..]; + + let exits: Vec = after.iter().filter_map(|e| match e { + TraceEvent::Exited { state } => Some(*state), + _ => None, + }).collect(); + let entered: Vec = after.iter().filter_map(|e| match e { + TraceEvent::Entered { state } => Some(*state), + _ => None, + }).collect(); + + assert_eq!(exits, vec![SP], "self-transition exits target only"); + assert_eq!(entered, vec![SP, SC, SL], "re-enter target then default-descend"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_self_composite_action_kinds_in_order() { + // After the SelfParent transition: Exit p_out, Entry p_in, Entry c_in, Entry l_in. + tokio::task::LocalSet::new().run_until(async { + let mut m = Sc::new(Ctx); + let _ = m.dispatch(Ev::UpToParent).await; + let _ = m.dispatch(Ev::SelfParent).await; + let j = m.take_journal(); + let self_idx = j.iter().rposition(|e| matches!( + e, TraceEvent::TransitionFired { from: Some(SP), to: SP } + )).unwrap(); + let kinds: Vec = j[self_idx..].iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { kind, .. } => Some(*kind), + _ => None, + }).collect(); + assert_eq!(kinds, + vec![ActionKind::Exit, ActionKind::Entry, ActionKind::Entry, ActionKind::Entry], + "exit Parent, then enter Parent, Child, Leaf"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_self_composite_byte_deterministic() { + let run = || async { + tokio::task::LocalSet::new().run_until(async { + let mut m = Sc::new(Ctx); + let _ = m.dispatch(Ev::UpToParent).await; + let _ = m.dispatch(Ev::SelfParent).await; + let _ = m.dispatch(Ev::Halt).await; + m.take_journal() + }).await + }; + let first = run().await; + for i in 1..10 { + assert_eq!(first, run().await, "diverged on run {i}"); + } +} diff --git a/hsmc/tests/det_step_dispatch.rs b/hsmc/tests/det_step_dispatch.rs new file mode 100644 index 0000000..e648c9d --- /dev/null +++ b/hsmc/tests/det_step_dispatch.rs @@ -0,0 +1,129 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for `step()` vs `dispatch()` equivalence. +//! +//! Spec section "step() vs run() vs dispatch()": +//! For the same external event sequence and the same elapsed-time inputs, +//! the three produce the same observable trace. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + Tick, + Halt, +} + +statechart! { + Eq { + context: Ctx; + events: Ev; + default(A); + terminate(Halt); + + state A { + entry: a_in; + exit: a_out; + on(Tick) => B; + } + state B { + entry: b_in; + exit: b_out; + on(Tick) => A; + } + } +} + +impl EqActions for EqActionContext<'_> { + async fn a_in(&mut self) {} + async fn a_out(&mut self) {} + async fn b_in(&mut self) {} + async fn b_out(&mut self) {} +} + +#[tokio::test(flavor = "current_thread")] +async fn det_dispatch_drains_to_quiescence() { + // dispatch(ev) processes ev plus any events emitted while handling ev. + // After the await returns, the queue is empty. + tokio::task::LocalSet::new().run_until(async { + let mut m = Eq::new(Ctx); + let _ = m.dispatch(Ev::Tick).await; + assert!(!m.has_pending_events()); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_step_and_dispatch_produce_same_journal() { + // Drive one machine via dispatch, another via send + step until queue empty. + // The journals must match. + tokio::task::LocalSet::new().run_until(async { + // Path 1: dispatch. + let mut m1 = Eq::new(Ctx); + let _ = m1.dispatch(Ev::Tick).await; + let _ = m1.dispatch(Ev::Tick).await; + let _ = m1.dispatch(Ev::Halt).await; + let j_dispatch = m1.take_journal(); + + // Path 2: send + step. + let mut m2 = Eq::new(Ctx); + m2.send(Ev::Tick).unwrap(); + m2.send(Ev::Tick).unwrap(); + m2.send(Ev::Halt).unwrap(); + // Drive to quiescence with explicit steps. + for _ in 0..20 { + let _ = m2.step(::hsmc::Duration::ZERO).await; + if m2.is_terminated() { break; } + } + let j_step = m2.take_journal(); + + assert_eq!(j_dispatch, j_step, + "step and dispatch must produce identical journals for the same event sequence"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_step_is_at_most_one_unit_of_work() { + // Each step() processes at most one event or one timer. + tokio::task::LocalSet::new().run_until(async { + let mut m = Eq::new(Ctx); + m.send(Ev::Tick).unwrap(); + m.send(Ev::Tick).unwrap(); + m.send(Ev::Halt).unwrap(); + + // After the first step (initial enter): chart enters root → A. + let _ = m.step(::hsmc::Duration::ZERO).await; + // After the second step: process Tick #1 (A → B). + let len_after_2 = { + let _ = m.step(::hsmc::Duration::ZERO).await; + m.journal().len() + }; + // After the third step: process Tick #2 (B → A). + let _ = m.step(::hsmc::Duration::ZERO).await; + let len_after_3 = m.journal().len(); + + assert!(len_after_3 > len_after_2, "step processes additional events"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_step_repeated_idempotent_when_queue_empty() { + // Once initial-enter is done and queue is empty, additional steps + // (with elapsed=ZERO) are no-ops. + tokio::task::LocalSet::new().run_until(async { + let mut m = Eq::new(Ctx); + let _ = m.step(::hsmc::Duration::ZERO).await; // initial entry + let len_after_first = m.journal().len(); + for _ in 0..10 { + let _ = m.step(::hsmc::Duration::ZERO).await; + } + // After the first step, no events are pending, so additional + // step(ZERO) calls do nothing. + assert_eq!(m.journal().len(), len_after_first, + "step(ZERO) on empty queue must not change journal"); + }).await; +} diff --git a/hsmc/tests/det_termination.rs b/hsmc/tests/det_termination.rs new file mode 100644 index 0000000..25ed7c5 --- /dev/null +++ b/hsmc/tests/det_termination.rs @@ -0,0 +1,182 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for TERMINATION. +//! +//! Spec section "Termination": +//! When a `terminate` event is received, the machine exits the entire active +//! path bottom-up: innermost first, then each parent, up to and including +//! the root. After that, the machine is done — `is_terminated()` is true, +//! `run()` returns `Ok(())`, further `step()` calls are no-ops returning +//! `None`. Any pending events in the queue are dropped. Any in-flight +//! durings are dropped at their next `.await`. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, HsmcError, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + Halt, + Other, +} + +statechart! { + Term { + context: Ctx; + events: Ev; + default(Mid); + terminate(Halt); + + entry: r_in; + exit: r_out; + + state Mid { + entry: m_in; + exit: m_out; + default(Leaf); + on(Other) => log_other; + state Leaf { + entry: l_in; + exit: l_out; + } + } + } +} + +impl TermActions for TermActionContext<'_> { + async fn r_in(&mut self) {} + async fn r_out(&mut self) {} + async fn m_in(&mut self) {} + async fn m_out(&mut self) {} + async fn l_in(&mut self) {} + async fn l_out(&mut self) {} + async fn log_other(&mut self){} +} + +const SR: u16 = 0; +const SM: u16 = 1; +const SL: u16 = 2; +// Halt is interned via terminate(Halt). Other is used in `on(Other)` first. +// IR build order: handlers processed first per body. Mid has on(Other) → 0. +// Then Halt is interned at the end of build_ir → 1. +const E_OTHER: u16 = 0; +const E_HALT: u16 = 1; + +#[tokio::test(flavor = "current_thread")] +async fn det_terminate_records_terminate_requested() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Term::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let j = m.take_journal(); + // TerminateRequested fires before the bottom-up exits. + let req_idx = j.iter().position(|e| matches!( + e, TraceEvent::TerminateRequested { event: E_HALT } + )); + assert!(req_idx.is_some(), "TerminateRequested must appear, got: {:?}", j); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_terminate_exits_bottom_up() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Term::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let exits: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::Exited { state } => Some(*state), + _ => None, + }).collect(); + assert_eq!(exits, vec![SL, SM, SR], "termination exits inner-to-outer"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_terminate_terminated_is_last() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Term::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + assert!(matches!(m.journal().last(), Some(TraceEvent::Terminated))); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_terminate_dispatch_after_returns_already_terminated() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Term::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let res = m.dispatch(Ev::Other).await; + assert!(matches!(res, Err(HsmcError::AlreadyTerminated)), + "dispatch after terminate must return AlreadyTerminated, got {:?}", res); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_terminate_journal_unchanged_by_post_term_dispatch() { + // Calling dispatch after terminate must not journal anything new. + tokio::task::LocalSet::new().run_until(async { + let mut m = Term::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let len_before = m.journal().len(); + let _ = m.dispatch(Ev::Other).await; + let len_after = m.journal().len(); + assert_eq!(len_before, len_after, + "journal length must not change after termination"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_terminate_exit_actions_run_in_order() { + // Spec: exit actions inner-to-outer. + tokio::task::LocalSet::new().run_until(async { + let mut m = Term::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let exit_actions: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::ActionInvoked { state, kind: ActionKind::Exit, .. } => Some(*state), + _ => None, + }).collect(); + assert_eq!(exit_actions, vec![SL, SM, SR]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_terminate_other_event_processed_before_halt() { + // Other is dispatched first, then Halt. Other is delivered, then Halt + // triggers termination. EventDelivered for Other appears, but no + // EventDelivered for Halt — instead, TerminateRequested. + tokio::task::LocalSet::new().run_until(async { + let mut m = Term::new(Ctx); + let _ = m.dispatch(Ev::Other).await; + let _ = m.dispatch(Ev::Halt).await; + let j = m.take_journal(); + let other_delivered = j.iter().any(|e| matches!( + e, TraceEvent::EventDelivered { event: E_OTHER, .. } + )); + let halt_delivered = j.iter().any(|e| matches!( + e, TraceEvent::EventDelivered { event: E_HALT, .. } + )); + let halt_requested = j.iter().any(|e| matches!( + e, TraceEvent::TerminateRequested { event: E_HALT } + )); + assert!(other_delivered, "Other must be delivered"); + assert!(!halt_delivered, "Halt does not go through EventDelivered"); + assert!(halt_requested, "Halt goes through TerminateRequested"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_terminate_byte_deterministic() { + let run = || async { + tokio::task::LocalSet::new().run_until(async { + let mut m = Term::new(Ctx); + let _ = m.dispatch(Ev::Other).await; + let _ = m.dispatch(Ev::Halt).await; + m.take_journal() + }).await + }; + let first = run().await; + for i in 1..10 { + assert_eq!(first, run().await, "diverged on run {i}"); + } +} diff --git a/hsmc/tests/det_timers.rs b/hsmc/tests/det_timers.rs new file mode 100644 index 0000000..628ea88 --- /dev/null +++ b/hsmc/tests/det_timers.rs @@ -0,0 +1,198 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for TIMERS. +//! +//! Spec section "Timers": +//! - A timer starts when its state is entered. +//! - A timer is cancelled when its state is exited. +//! - Descending into a child state is not an exit — parent's timers keep running. +//! - Timers don't bubble. Only the declaring state handles its expiry. +//! - Re-entering a state restarts its timers. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; +use core::time::Duration; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + Stop, + Halt, +} + +statechart! { + Tim { + context: Ctx; + events: Ev; + default(Counting); + terminate(Halt); + + state Counting { + entry: c_in; + exit: c_out; + on(after Duration::from_millis(50)) => Done; + on(Stop) => Done; + } + state Done { + entry: d_in; + on(after Duration::from_millis(20)) => log_tick; + } + } +} + +impl TimActions for TimActionContext<'_> { + async fn c_in(&mut self) {} + async fn c_out(&mut self) {} + async fn d_in(&mut self) {} + async fn log_tick(&mut self){} +} + +const SR: u16 = 0; +const SC: u16 = 1; +const SD: u16 = 2; +// Timer ids in first-seen order: 50ms (counting) → 0, 20ms (done) → 1. +const T_COUNTING: u16 = 0; +const T_DONE: u16 = 1; + +fn timer_events(j: &[TraceEvent]) -> Vec<&TraceEvent> { + j.iter().filter(|e| matches!( + e, + TraceEvent::TimerArmed { .. } + | TraceEvent::TimerCancelled { .. } + | TraceEvent::TimerFired { .. } + )).collect() +} + +#[tokio::test(flavor = "current_thread")] +async fn det_timer_arms_on_entry() { + // Spec: timer starts when its state is entered. + tokio::task::LocalSet::new().run_until(async { + let mut m = Tim::new(Ctx); + let _ = m.dispatch(Ev::Stop).await; + let j = m.take_journal(); + // First TimerArmed must be Counting's 50ms timer. + let first_armed = j.iter().find(|e| matches!(e, TraceEvent::TimerArmed { .. })); + assert!(matches!( + first_armed, + Some(TraceEvent::TimerArmed { state: SC, timer: T_COUNTING, ns: 50_000_000 }) + ), "got: {:?}", first_armed); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_timer_cancels_on_exit() { + // Spec: timer is cancelled when its state is exited. + tokio::task::LocalSet::new().run_until(async { + let mut m = Tim::new(Ctx); + let _ = m.dispatch(Ev::Stop).await; + let j = m.take_journal(); + // Stop transitions Counting → Done. Exit Counting must cancel its timer. + let cancelled = j.iter().find(|e| matches!( + e, TraceEvent::TimerCancelled { state: SC, timer: T_COUNTING } + )); + assert!(cancelled.is_some(), + "Counting's timer must be cancelled on exit, got: {:?}", j); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_timer_cancel_appears_before_exit_actions() { + // Spec: "1. cancel durings 2. cancel timers 3. exit actions 4. Exited" + tokio::task::LocalSet::new().run_until(async { + let mut m = Tim::new(Ctx); + let _ = m.dispatch(Ev::Stop).await; + let j = m.take_journal(); + let cancel_idx = j.iter().position(|e| matches!( + e, TraceEvent::TimerCancelled { state: SC, .. } + )).unwrap(); + let exit_action_idx = j.iter().position(|e| matches!( + e, TraceEvent::ActionInvoked { state: SC, kind: ActionKind::Exit, .. } + )).unwrap(); + assert!(cancel_idx < exit_action_idx, + "TimerCancelled at {} must precede ActionInvoked Exit at {}", + cancel_idx, exit_action_idx); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_timer_arm_appears_after_entry_actions() { + // The TimerArmed must come AFTER the entry action invocation. + tokio::task::LocalSet::new().run_until(async { + let mut m = Tim::new(Ctx); + let _ = m.dispatch(Ev::Stop).await; + let j = m.take_journal(); + // First Entry-kind action on Counting: + let entry_idx = j.iter().position(|e| matches!( + e, TraceEvent::ActionInvoked { state: SC, kind: ActionKind::Entry, .. } + )).unwrap(); + // First TimerArmed for Counting: + let armed_idx = j.iter().position(|e| matches!( + e, TraceEvent::TimerArmed { state: SC, .. } + )).unwrap(); + assert!(entry_idx < armed_idx, + "entry actions ({}) must fire before TimerArmed ({})", + entry_idx, armed_idx); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_timer_arm_each_state_in_path() { + // Initial descent into Counting arms Counting's timer. + tokio::task::LocalSet::new().run_until(async { + let mut m = Tim::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let armed: Vec<&TraceEvent> = m.journal().iter().filter(|e| matches!( + e, TraceEvent::TimerArmed { .. } + )).collect(); + // Only Counting has a timer in initial descent (Done is unreached). + assert_eq!(armed.len(), 1, "expected 1 TimerArmed during initial descent, got {:?}", armed); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_timer_two_lifecycles_arm_then_cancel_each() { + // GoChild then UpToCounting (no such event — use Stop for full exit). + // Just check Stop's full sequence: arm → cancel. + tokio::task::LocalSet::new().run_until(async { + let mut m = Tim::new(Ctx); + let _ = m.dispatch(Ev::Stop).await; + let evs = timer_events(m.journal()); + assert_eq!(evs.len(), 3, "expected arm → cancel → arm (Done's timer), got {:?}", evs); + assert!(matches!(evs[0], TraceEvent::TimerArmed { state: SC, timer: T_COUNTING, ns: 50_000_000 })); + assert!(matches!(evs[1], TraceEvent::TimerCancelled { state: SC, timer: T_COUNTING })); + assert!(matches!(evs[2], TraceEvent::TimerArmed { state: SD, timer: T_DONE, ns: 20_000_000 })); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_timer_byte_deterministic() { + let run = || async { + tokio::task::LocalSet::new().run_until(async { + let mut m = Tim::new(Ctx); + let _ = m.dispatch(Ev::Stop).await; + let _ = m.dispatch(Ev::Halt).await; + m.take_journal() + }).await + }; + let first = run().await; + for i in 1..10 { + assert_eq!(first, run().await, "diverged on run {i}"); + } +} + +#[tokio::test(flavor = "current_thread")] +async fn det_timer_state_cancel_uses_correct_state_id() { + // The TimerCancelled.state must be SC, not SR or any other. + tokio::task::LocalSet::new().run_until(async { + let mut m = Tim::new(Ctx); + let _ = m.dispatch(Ev::Stop).await; + let cancels: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::TimerCancelled { state, .. } => Some(*state), + _ => None, + }).collect(); + assert_eq!(cancels, vec![SC]); + }).await; +} diff --git a/hsmc/tests/det_timers_parent.rs b/hsmc/tests/det_timers_parent.rs new file mode 100644 index 0000000..6d18b08 --- /dev/null +++ b/hsmc/tests/det_timers_parent.rs @@ -0,0 +1,106 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for parent-vs-child timer interaction. +//! +//! Spec: "Descending into a child state is not an exit — the parent's +//! timers keep running." + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, TraceEvent}; +use core::time::Duration; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + Halt, +} + +// Parent has a 100ms timer. Default-descend into ChildA. ChildA has no timer. +statechart! { + Pt { + context: Ctx; + events: Ev; + default(Parent); + terminate(Halt); + + state Parent { + entry: p_in; + exit: p_out; + default(ChildA); + on(after Duration::from_millis(100)) => Done; + state ChildA { + entry: ca_in; + exit: ca_out; + } + } + state Done { + entry: d_in; + } + } +} + +impl PtActions for PtActionContext<'_> { + async fn p_in(&mut self) {} + async fn p_out(&mut self) {} + async fn ca_in(&mut self) {} + async fn ca_out(&mut self){} + async fn d_in(&mut self) {} +} + +const SP: u16 = 1; +const T_PARENT: u16 = 0; + +#[tokio::test(flavor = "current_thread")] +async fn det_parent_timer_armed_before_child_entered() { + // Parent's timer arms during Parent's entry; THEN default-descends into ChildA. + // So the order is: TimerArmed(Parent) before Entered(ChildA). + tokio::task::LocalSet::new().run_until(async { + let mut m = Pt::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let j = m.take_journal(); + let armed_idx = j.iter().position(|e| matches!( + e, TraceEvent::TimerArmed { state: SP, .. } + )).unwrap(); + let child_entered_idx = j.iter().position(|e| matches!( + e, TraceEvent::Entered { state: 2 } // ChildA = id 2 + )).unwrap(); + assert!(armed_idx < child_entered_idx, + "TimerArmed (Parent) at {} must precede Entered (ChildA) at {}", + armed_idx, child_entered_idx); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_parent_timer_only_one_arm_in_initial_descent() { + // Only Parent has a timer. ChildA has none. + tokio::task::LocalSet::new().run_until(async { + let mut m = Pt::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let armed: Vec = m.journal().iter().filter_map(|e| match e { + TraceEvent::TimerArmed { state, .. } => Some(*state), + _ => None, + }).collect(); + assert_eq!(armed, vec![SP]); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_parent_timer_cancelled_on_termination() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Pt::new(Ctx); + let _ = m.dispatch(Ev::Halt).await; + let cancels: Vec<&TraceEvent> = m.journal().iter().filter(|e| matches!( + e, TraceEvent::TimerCancelled { .. } + )).collect(); + // Termination unwinds all states. Parent's timer is cancelled when Parent exits. + assert_eq!(cancels.len(), 1, + "expected exactly 1 TimerCancelled (Parent's), got {:?}", cancels); + assert!(matches!( + cancels[0], + TraceEvent::TimerCancelled { state: SP, timer: T_PARENT } + )); + }).await; +} diff --git a/hsmc/tests/det_up.rs b/hsmc/tests/det_up.rs new file mode 100644 index 0000000..ac180e6 --- /dev/null +++ b/hsmc/tests/det_up.rs @@ -0,0 +1,289 @@ +#![allow(dead_code)] +//! Deterministic-flow tests for UP-TRANSITIONS (target is on active path, target ≠ I). +//! +//! Spec section "Transitioning to one of your parents (the important one)": +//! When you transition to an ancestor of the current state, you exit the +//! current state and any states between, but you do NOT re-enter the +//! ancestor. ... You cannot enter a state you never left. +//! +//! Spec invariants for up-transitions: +//! - The ancestor's entry actions don't fire. +//! - The ancestor's `default` is not followed. +//! - The ancestor's timers don't restart. +//! - The ancestor's durings keep running. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + UpToA, + UpToB, + UpToC, + Halt, +} + +// Hierarchy: Root → A → B → C → D +// Up-transitions on D and intermediate states fire to ancestors. +statechart! { + Up { + context: Ctx; + events: Ev; + default(A); + terminate(Halt); + + entry: r_in; + exit: r_out; + + state A { + entry: a_in; + exit: a_out; + default(B); + state B { + entry: b_in; + exit: b_out; + default(C); + state C { + entry: c_in; + exit: c_out; + default(D); + state D { + entry: d_in; + exit: d_out; + on(UpToA) => A; + on(UpToB) => B; + on(UpToC) => C; + } + } + } + } + } +} + +impl UpActions for UpActionContext<'_> { + async fn r_in(&mut self) {} + async fn r_out(&mut self) {} + async fn a_in(&mut self) {} + async fn a_out(&mut self) {} + async fn b_in(&mut self) {} + async fn b_out(&mut self) {} + async fn c_in(&mut self) {} + async fn c_out(&mut self) {} + async fn d_in(&mut self) {} + async fn d_out(&mut self) {} +} + +const SR: u16 = 0; +const SA: u16 = 1; +const SB: u16 = 2; +const SC: u16 = 3; +const SD: u16 = 4; +const A_R_IN: u16 = 0; +const A_R_OUT: u16 = 1; +const A_A_IN: u16 = 2; +const A_A_OUT: u16 = 3; +const A_B_IN: u16 = 4; +const A_B_OUT: u16 = 5; +const A_C_IN: u16 = 6; +const A_C_OUT: u16 = 7; +const A_D_IN: u16 = 8; +const A_D_OUT: u16 = 9; +// Event ids in first-seen order during IR build (D's handlers, in declaration order). +const E_UPTOA: u16 = 0; +const E_UPTOB: u16 = 1; +const E_UPTOC: u16 = 2; + +fn entry(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Entry } +} +fn exit_(state: u16, action: u16) -> TraceEvent { + TraceEvent::ActionInvoked { state, action, kind: ActionKind::Exit } +} +fn initial_descent() -> Vec { + vec![ + TraceEvent::Started { chart_hash: Up::<8>::CHART_HASH }, + TraceEvent::Entered { state: SR }, + entry(SR, A_R_IN), + TraceEvent::Entered { state: SA }, + entry(SA, A_A_IN), + TraceEvent::Entered { state: SB }, + entry(SB, A_B_IN), + TraceEvent::Entered { state: SC }, + entry(SC, A_C_IN), + TraceEvent::Entered { state: SD }, + entry(SD, A_D_IN), + ] +} +fn assert_journal(actual: &[TraceEvent], expected: &[TraceEvent]) { + let mismatch = actual.iter().zip(expected.iter()) + .position(|(a, e)| a != e); + if let Some(i) = mismatch { + panic!("mismatch at index {}\n actual: {:?}\n expected: {:?}", + i, actual.get(i), expected.get(i)); + } + assert_eq!(actual.len(), expected.len(), + "length mismatch: actual {} vs expected {}", actual.len(), expected.len()); +} + +#[tokio::test(flavor = "current_thread")] +async fn det_up_to_immediate_grandparent() { + // D → C: exit D only. C is target, not exited, not re-entered. + tokio::task::LocalSet::new().run_until(async { + let mut m = Up::new(Ctx); + let _ = m.dispatch(Ev::UpToC).await; + let actual = m.take_journal(); + + let mut expected = initial_descent(); + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SD, event: E_UPTOC }, + TraceEvent::TransitionFired { from: Some(SD), to: SC }, + exit_(SD, A_D_OUT), + TraceEvent::Exited { state: SD }, + ]); + assert_journal(&actual, &expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_up_two_levels() { + // D → B: exit D, exit C. B is target, not exited. + tokio::task::LocalSet::new().run_until(async { + let mut m = Up::new(Ctx); + let _ = m.dispatch(Ev::UpToB).await; + let actual = m.take_journal(); + + let mut expected = initial_descent(); + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SD, event: E_UPTOB }, + TraceEvent::TransitionFired { from: Some(SD), to: SB }, + exit_(SD, A_D_OUT), + TraceEvent::Exited { state: SD }, + exit_(SC, A_C_OUT), + TraceEvent::Exited { state: SC }, + ]); + assert_journal(&actual, &expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_up_three_levels_to_a() { + // D → A: exit D, C, B. A is target, not exited. + tokio::task::LocalSet::new().run_until(async { + let mut m = Up::new(Ctx); + let _ = m.dispatch(Ev::UpToA).await; + let actual = m.take_journal(); + + let mut expected = initial_descent(); + expected.extend(vec![ + TraceEvent::EventDelivered { handler_state: SD, event: E_UPTOA }, + TraceEvent::TransitionFired { from: Some(SD), to: SA }, + exit_(SD, A_D_OUT), + TraceEvent::Exited { state: SD }, + exit_(SC, A_C_OUT), + TraceEvent::Exited { state: SC }, + exit_(SB, A_B_OUT), + TraceEvent::Exited { state: SB }, + ]); + assert_journal(&actual, &expected); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_up_target_not_re_entered() { + // After D → A: A must NOT appear in any Entered event after the initial descent. + tokio::task::LocalSet::new().run_until(async { + let mut m = Up::new(Ctx); + let _ = m.dispatch(Ev::UpToA).await; + let j = m.take_journal(); + let split = j.iter().position(|e| matches!( + e, TraceEvent::EventDelivered { event: E_UPTOA, .. } + )).unwrap(); + let a_re_entered = j[split..].iter().filter(|e| matches!( + e, TraceEvent::Entered { state: SA } + )).count(); + assert_eq!(a_re_entered, 0, "target A must not re-enter on up-transition"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_up_target_action_not_fired() { + // After D → A: a_in must NOT fire after the initial descent. + tokio::task::LocalSet::new().run_until(async { + let mut m = Up::new(Ctx); + let _ = m.dispatch(Ev::UpToA).await; + let j = m.take_journal(); + let split = j.iter().position(|e| matches!( + e, TraceEvent::EventDelivered { event: E_UPTOA, .. } + )).unwrap(); + let a_in_after = j[split..].iter().filter(|e| matches!( + e, TraceEvent::ActionInvoked { state: SA, action: A_A_IN, .. } + )).count(); + assert_eq!(a_in_after, 0, "target's entry action must not fire on up-transition"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_up_no_default_descent() { + // After D → A: no default-descent. The journal stops with Exited(B). + // A is the new innermost active state, with no active child. + tokio::task::LocalSet::new().run_until(async { + let mut m = Up::new(Ctx); + let _ = m.dispatch(Ev::UpToA).await; + let j = m.take_journal(); + let split = j.iter().position(|e| matches!( + e, TraceEvent::EventDelivered { event: E_UPTOA, .. } + )).unwrap(); + // Nothing after this slice should be Entered (no descent). + let entered_after = j[split..].iter().filter(|e| matches!( + e, TraceEvent::Entered { .. } + )).count(); + assert_eq!(entered_after, 0, "up-transition: no default-descent"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_up_current_state_is_target_after() { + // After D → B, the innermost active state is B (composite, no active child). + tokio::task::LocalSet::new().run_until(async { + let mut m = Up::new(Ctx); + let _ = m.dispatch(Ev::UpToB).await; + // current_state() should return B's public variant. + // Indirect check: the most recent Entered (B's, from initial descent) is the + // last Entered before the up-transition; nothing after. + let j = m.take_journal(); + let last_entered = j.iter().enumerate().rev() + .find(|(_, e)| matches!(e, TraceEvent::Entered { .. })) + .map(|(i, _)| i); + let split = j.iter().position(|e| matches!( + e, TraceEvent::TransitionFired { .. } + )).unwrap(); + // The last Entered event must be BEFORE the transition. + assert!(last_entered.unwrap() < split, + "up-transition: no entries after the transition fires"); + }).await; +} + +#[tokio::test(flavor = "current_thread")] +async fn det_up_chained_then_lateral() { + // D → C, then C is a leaf with no children, so this becomes the new + // innermost. From C we don't have any other handlers, so test ends here. + tokio::task::LocalSet::new().run_until(async { + let mut m = Up::new(Ctx); + let _ = m.dispatch(Ev::UpToC).await; + let _ = m.dispatch(Ev::Halt).await; + let j = m.take_journal(); + // After UpToC, we should have Exited(D) but C remains. Halt then exits + // C → B → A → Root. + let exits: Vec = j.iter().filter_map(|e| match e { + TraceEvent::Exited { state } => Some(*state), + _ => None, + }).collect(); + assert_eq!(exits, vec![SD, SC, SB, SA, SR], + "up to C, then terminate exits remaining path"); + }).await; +} diff --git a/hsmc/tests/journal_dump.rs b/hsmc/tests/journal_dump.rs new file mode 100644 index 0000000..9663e79 --- /dev/null +++ b/hsmc/tests/journal_dump.rs @@ -0,0 +1,83 @@ +//! Dumps a journal for visual inspection. Run with: +//! +//! cargo test -p hsmc --features tokio,journal --test journal_dump -- --nocapture +//! +//! Not an assertion — just shows the actual sequence so we can sanity-check +//! that "EVERYTHING" is journaled. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::statechart; + +#[derive(Default)] +pub struct Ctx { + pub n: u32, +} + +#[derive(Debug, Clone, PartialEq)] +pub enum Ev { + Go, + Beep, + Halt, +} + +statechart! { + Dump { + context: Ctx; + events: Ev; + + default(Idle); + terminate(Halt); + + entry: root_in; + exit: root_out; + + state Idle { + entry: idle_in; + exit: idle_out; + on(Go) => Active; + on(Beep) => beep_at_idle; + } + state Active { + entry: active_in; + exit: active_out; + default(Sub); + state Sub { + entry: sub_in; + exit: sub_out; + on(Beep) => beep_at_sub; + } + } + } +} + +impl DumpActions for DumpActionContext<'_> { + async fn root_in(&mut self) { self.n += 1; } + async fn root_out(&mut self) {} + async fn idle_in(&mut self) {} + async fn idle_out(&mut self) {} + async fn active_in(&mut self) {} + async fn active_out(&mut self) {} + async fn sub_in(&mut self) {} + async fn sub_out(&mut self) {} + async fn beep_at_idle(&mut self) {} + async fn beep_at_sub(&mut self) {} +} + +#[tokio::test(flavor = "current_thread")] +async fn dump_journal() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Dump::new(Ctx::default()); + let _ = m.dispatch(Ev::Beep).await; + let _ = m.dispatch(Ev::Go).await; + let _ = m.dispatch(Ev::Beep).await; + let _ = m.dispatch(Ev::Halt).await; + + println!("\n=== JOURNAL DUMP (CHART_HASH={:#x}) ===", Dump::<8>::CHART_HASH); + for (i, e) in m.journal().iter().enumerate() { + println!(" {:>3}: {:?}", i, e); + } + println!("=== END ({} events) ===\n", m.journal().len()); + }).await; +} diff --git a/hsmc/tests/journal_replay.rs b/hsmc/tests/journal_replay.rs new file mode 100644 index 0000000..020151d --- /dev/null +++ b/hsmc/tests/journal_replay.rs @@ -0,0 +1,129 @@ +//! Replay tests: a hand-built EXPECTED journal compared byte-for-byte against +//! the ACTUAL journal produced by running the chart with a fixed event +//! sequence. This is the canonical correctness check the user asked for — +//! "EVERYTHING in the sequence has to be journaled and compared against the +//! expected sequence." +//! +//! When the codegen drifts (an entry actions reorders, a timer arms in a +//! different place, an event dispatches to a different state), exactly one +//! line of the expected vector mismatches and the test fails with a +//! pinpoint diff. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone, PartialEq)] +pub enum Ev { + Go, + Halt, +} + +statechart! { + Replay { + context: Ctx; + events: Ev; + + default(Idle); + terminate(Halt); + + entry: root_in; + exit: root_out; + + state Idle { + entry: idle_in; + exit: idle_out; + on(Go) => Active; + } + state Active { + entry: active_in; + exit: active_out; + default(Sub); + state Sub { + entry: sub_in; + exit: sub_out; + } + } + } +} + +impl ReplayActions for ReplayActionContext<'_> { + async fn root_in(&mut self) {} + async fn root_out(&mut self) {} + async fn idle_in(&mut self) {} + async fn idle_out(&mut self) {} + async fn active_in(&mut self) {} + async fn active_out(&mut self) {} + async fn sub_in(&mut self) {} + async fn sub_out(&mut self) {} +} + +// State indices. +const ST_ROOT: u16 = 0; +const ST_IDLE: u16 = 1; +const ST_ACTIVE: u16 = 2; +const ST_SUB: u16 = 3; + +// Action indices. +const A_ROOT_IN: u16 = 0; +const A_ROOT_OUT: u16 = 1; +const A_IDLE_IN: u16 = 2; +const A_IDLE_OUT: u16 = 3; +const A_ACTIVE_IN: u16 = 4; +const A_ACTIVE_OUT: u16 = 5; +const A_SUB_IN: u16 = 6; +const A_SUB_OUT: u16 = 7; + +// Event indices. +const E_GO: u16 = 0; +const E_HALT: u16 = 1; + +#[tokio::test(flavor = "current_thread")] +async fn replay_full_lifecycle_matches_expected() { + tokio::task::LocalSet::new().run_until(async { + let mut m = Replay::new(Ctx::default()); + let _ = m.dispatch(Ev::Go).await; + let _ = m.dispatch(Ev::Halt).await; + + let actual = m.take_journal(); + + let expected: Vec = vec![ + // ── First step: enter the chart ── + TraceEvent::Started { chart_hash: Replay::<8>::CHART_HASH }, + TraceEvent::Entered { state: ST_ROOT }, + TraceEvent::ActionInvoked { state: ST_ROOT, action: A_ROOT_IN, kind: ActionKind::Entry }, + TraceEvent::Entered { state: ST_IDLE }, + TraceEvent::ActionInvoked { state: ST_IDLE, action: A_IDLE_IN, kind: ActionKind::Entry }, + + // ── Go event delivered to Idle, transition to Active → Sub ── + TraceEvent::EventDelivered { handler_state: ST_IDLE, event: E_GO }, + TraceEvent::TransitionFired { from: Some(ST_IDLE), to: ST_ACTIVE }, + TraceEvent::ActionInvoked { state: ST_IDLE, action: A_IDLE_OUT, kind: ActionKind::Exit }, + TraceEvent::Exited { state: ST_IDLE }, + TraceEvent::Entered { state: ST_ACTIVE }, + TraceEvent::ActionInvoked { state: ST_ACTIVE, action: A_ACTIVE_IN, kind: ActionKind::Entry }, + TraceEvent::Entered { state: ST_SUB }, + TraceEvent::ActionInvoked { state: ST_SUB, action: A_SUB_IN, kind: ActionKind::Entry }, + + // ── Halt event triggers termination: exit Sub → Active → root, then Terminated ── + TraceEvent::TerminateRequested { event: E_HALT }, + TraceEvent::ActionInvoked { state: ST_SUB, action: A_SUB_OUT, kind: ActionKind::Exit }, + TraceEvent::Exited { state: ST_SUB }, + TraceEvent::ActionInvoked { state: ST_ACTIVE, action: A_ACTIVE_OUT, kind: ActionKind::Exit }, + TraceEvent::Exited { state: ST_ACTIVE }, + TraceEvent::ActionInvoked { state: ST_ROOT, action: A_ROOT_OUT, kind: ActionKind::Exit }, + TraceEvent::Exited { state: ST_ROOT }, + TraceEvent::Terminated, + ]; + + let mismatch_at = actual.iter().zip(expected.iter()) + .position(|(a, e)| a != e) + .map(|i| i.to_string()) + .unwrap_or_else(|| "".to_string()); + assert_eq!(actual, expected, "journal divergence at index {}", mismatch_at); + }).await; +} diff --git a/hsmc/tests/journal_replay_emit.rs b/hsmc/tests/journal_replay_emit.rs new file mode 100644 index 0000000..eec9e78 --- /dev/null +++ b/hsmc/tests/journal_replay_emit.rs @@ -0,0 +1,63 @@ +//! Replay test for emit() journaling. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, TraceEvent}; + +#[derive(Default)] +pub struct Ctx; + +#[derive(Debug, Clone)] +pub enum Ev { + Trigger, + Followup, + Halt, +} + +statechart! { + EmitProbe { + context: Ctx; + events: Ev; + + default(A); + terminate(Halt); + + state A { + on(Trigger) => emit_followup; + on(Followup) => B; + } + state B { + entry: noop; + } + } +} + +impl EmitProbeActions for EmitProbeActionContext<'_> { + async fn emit_followup(&mut self) { + self.emit(Ev::Followup).unwrap(); + } + async fn noop(&mut self) {} +} + +#[tokio::test(flavor = "current_thread")] +async fn emit_queued_appears_in_journal() { + tokio::task::LocalSet::new().run_until(async { + let mut m = EmitProbe::new(Ctx::default()); + let _ = m.dispatch(Ev::Trigger).await; + + let saw_emit = m.journal().iter().any(|e| matches!( + e, + TraceEvent::EmitQueued { .. } + )); + assert!(saw_emit, "journal must contain EmitQueued, got {:?}", m.journal()); + + // The follow-up event MUST be delivered (proving the queue actually + // drained the emit'd event). + let delivered_followup = m.journal().iter().any(|e| matches!( + e, + TraceEvent::EventDelivered { event: 1, .. } // 1 = Followup (Trigger=0, Followup=1) + )); + assert!(delivered_followup, "expected Followup to be delivered after emit"); + }).await; +} diff --git a/hsmc/tests/journal_replay_timer.rs b/hsmc/tests/journal_replay_timer.rs new file mode 100644 index 0000000..a6a9956 --- /dev/null +++ b/hsmc/tests/journal_replay_timer.rs @@ -0,0 +1,70 @@ +//! Replay test for timer arm + cancel paths. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, TraceEvent}; + +#[derive(Default)] +pub struct Ctx { + pub fired: u32, +} + +#[derive(Debug, Clone)] +pub enum Ev { + Stop, + Halt, +} + +statechart! { + TimerProbe { + context: Ctx; + events: Ev; + + default(Counting); + terminate(Halt); + + state Counting { + entry: noop; + exit: noop2; + on(after hsmc::Duration::from_millis(100)) => Done; + on(Stop) => Done; + } + state Done { + entry: noop3; + } + } +} + +impl TimerProbeActions for TimerProbeActionContext<'_> { + async fn noop(&mut self) {} + async fn noop2(&mut self) {} + async fn noop3(&mut self) {} +} + +#[tokio::test(flavor = "current_thread")] +async fn timer_arm_then_cancel_journals_both() { + tokio::task::LocalSet::new().run_until(async { + let mut m = TimerProbe::new(Ctx::default()); + let _ = m.dispatch(Ev::Stop).await; + + let timer_events: Vec<&TraceEvent> = m.journal().iter() + .filter(|e| matches!( + e, + TraceEvent::TimerArmed { .. } + | TraceEvent::TimerCancelled { .. } + | TraceEvent::TimerFired { .. } + )) + .collect(); + + assert_eq!(timer_events.len(), 2, "expected 2 timer events, got {:?}", timer_events); + assert!(matches!( + timer_events[0], + TraceEvent::TimerArmed { state: 1, timer: 0, ns: 100_000_000 } + ), "got {:?}", timer_events[0]); + assert!(matches!( + timer_events[1], + TraceEvent::TimerCancelled { state: 1, timer: 0 } + ), "got {:?}", timer_events[1]); + }).await; +} diff --git a/hsmc/tests/journal_smoke.rs b/hsmc/tests/journal_smoke.rs new file mode 100644 index 0000000..0e27818 --- /dev/null +++ b/hsmc/tests/journal_smoke.rs @@ -0,0 +1,210 @@ +//! Smoke tests for the deterministic execution journal (`feature = "journal"`). +//! +//! Every observable atom — entries, exits, action invocations (with kind), +//! during start/cancel, timer arm/cancel/fire, queued emits, event delivery, +//! transitions, termination — must appear in the journal in canonical order +//! for a fixed `(chart, ctx, event sequence)` input. These tests pin down +//! that order on small chart shapes so any regression in codegen is caught +//! immediately. +//! +//! Tests run only when both `tokio` and `journal` features are enabled. + +#![cfg(all(feature = "tokio", feature = "journal"))] +#![allow(unexpected_cfgs)] + +use hsmc::{statechart, ActionKind, TraceEvent}; + +// ───────────────────────────────────────────────────────────────────── +// Small chart: A → B on Go, with entry/exit actions in a hierarchy. +// ───────────────────────────────────────────────────────────────────── + +#[derive(Default)] +pub struct Ctx { + pub log: Vec<&'static str>, +} + +#[derive(Debug, Clone, PartialEq)] +pub enum Ev { + Go, + Halt, +} + +statechart! { + JournalProbe { + context: Ctx; + events: Ev; + + default(Idle); + terminate(Halt); + + entry: root_in; + exit: root_out; + + state Idle { + entry: idle_in; + exit: idle_out; + on(Go) => Active; + } + state Active { + entry: active_in; + exit: active_out; + default(Sub); + state Sub { + entry: sub_in; + exit: sub_out; + } + } + } +} + +impl JournalProbeActions for JournalProbeActionContext<'_> { + async fn root_in(&mut self) { self.log.push("root_in"); } + async fn root_out(&mut self) { self.log.push("root_out"); } + async fn idle_in(&mut self) { self.log.push("idle_in"); } + async fn idle_out(&mut self) { self.log.push("idle_out"); } + async fn active_in(&mut self) { self.log.push("active_in"); } + async fn active_out(&mut self) { self.log.push("active_out"); } + async fn sub_in(&mut self) { self.log.push("sub_in"); } + async fn sub_out(&mut self) { self.log.push("sub_out"); } +} + +#[tokio::test(flavor = "current_thread")] +async fn journal_records_initial_descent() { + tokio::task::LocalSet::new() + .run_until(async { + let mut m = JournalProbe::new(Ctx::default()); + // Drive the initial entry chain by stepping once with no event. + let _ = m.dispatch(Ev::Go).await; + + let j = m.journal(); + + // First event must be Started. + assert!(matches!(j[0], TraceEvent::Started { .. })); + // Started carries the chart's stable hash. + if let TraceEvent::Started { chart_hash } = j[0] { + assert_eq!(chart_hash, JournalProbe::<8>::CHART_HASH); + } + + // We expect (in order, for the initial descent root → Idle): + // Started + // Entered(root) + // ActionInvoked(root, root_in, Entry) + // Entered(Idle) + // ActionInvoked(Idle, idle_in, Entry) + // ... (then the Go event delivery / transition / sub entry) + let states_entered: Vec = j.iter() + .filter_map(|e| match e { + TraceEvent::Entered { state } => Some(*state), + _ => None, + }) + .collect(); + // At minimum we entered root (id 0), then Idle, then Active, then Sub. + assert_eq!(states_entered.len(), 4, "expected 4 Entered events, got {:?}", j); + + // Action kinds appear in order Entry → Handler (none here) → Exit. + let kinds: Vec = j.iter() + .filter_map(|e| match e { + TraceEvent::ActionInvoked { kind, .. } => Some(*kind), + _ => None, + }) + .collect(); + // Actions on the journey: Entry x4 (root, idle, active, sub), + // Exit x1 (idle), Entry x2 (active, sub) — wait no: + // Initial descent is root → Idle. Entries: root_in, idle_in. + // Then Go fires: Idle exits (idle_out), Active enters (active_in), + // Sub enters (sub_in). + // Total: Entry(root), Entry(idle), Exit(idle), Entry(active), Entry(sub). + let entry_count = kinds.iter().filter(|k| **k == ActionKind::Entry).count(); + let exit_count = kinds.iter().filter(|k| **k == ActionKind::Exit).count(); + assert_eq!(entry_count, 4, "expected 4 entry actions, got kinds {:?}", kinds); + assert_eq!(exit_count, 1, "expected 1 exit action, got kinds {:?}", kinds); + }) + .await; +} + +#[tokio::test(flavor = "current_thread")] +async fn journal_includes_transition_event() { + tokio::task::LocalSet::new() + .run_until(async { + let mut m = JournalProbe::new(Ctx::default()); + let _ = m.dispatch(Ev::Go).await; + + let saw_transition = m.journal().iter().any(|e| matches!( + e, + TraceEvent::TransitionFired { .. } + )); + assert!(saw_transition, "journal must contain TransitionFired"); + + let saw_event_delivered = m.journal().iter().any(|e| matches!( + e, + TraceEvent::EventDelivered { .. } + )); + assert!(saw_event_delivered, "journal must contain EventDelivered"); + }) + .await; +} + +#[tokio::test(flavor = "current_thread")] +async fn journal_records_termination() { + tokio::task::LocalSet::new() + .run_until(async { + let mut m = JournalProbe::new(Ctx::default()); + let _ = m.dispatch(Ev::Go).await; + let _ = m.dispatch(Ev::Halt).await; + + let j = m.journal(); + assert!( + matches!(j.last(), Some(TraceEvent::Terminated)), + "journal must end with Terminated, got tail: {:?}", + &j[j.len().saturating_sub(3)..] + ); + + // Termination exits all states from leaf to root (Sub → Active → Idle? No, + // Idle was already exited on Go. After Halt the active path is + // root → Active → Sub. Exits: Sub, Active, root. + let post_halt_exits: Vec = j.iter() + .skip_while(|e| !matches!(e, TraceEvent::EventDelivered { .. } if matches!(j.iter().rev().find(|x| matches!(x, TraceEvent::EventDelivered { .. })), Some(_)))) + .filter_map(|e| match e { + TraceEvent::Exited { state } => Some(*state), + _ => None, + }) + .collect(); + // We at least exited 4 times across the run (idle once, then sub/active/root on terminate). + assert!(post_halt_exits.len() >= 3, "expected at least 3 exits across the run, got {:?}", j); + }) + .await; +} + +#[tokio::test(flavor = "current_thread")] +async fn journal_is_byte_deterministic_across_runs() { + // Same chart, same context, same event sequence ⇒ identical journal. + let run = || async { + tokio::task::LocalSet::new() + .run_until(async { + let mut m = JournalProbe::new(Ctx::default()); + let _ = m.dispatch(Ev::Go).await; + let _ = m.dispatch(Ev::Halt).await; + m.take_journal() + }) + .await + }; + let first = run().await; + for i in 1..10 { + let again = run().await; + assert_eq!(first, again, "journal divergence on run #{}", i); + } +} + +#[tokio::test(flavor = "current_thread")] +async fn chart_hash_is_stable() { + // Two instances of the same chart must agree on CHART_HASH. + let _m1 = JournalProbe::new(Ctx::default()); + let _m2 = JournalProbe::new(Ctx::default()); + assert_eq!( + JournalProbe::<8>::CHART_HASH, + JournalProbe::<8>::CHART_HASH, + "chart hash must be stable across instantiations" + ); + // CHART_HASH must be nonzero — proves the FNV-1a fingerprint actually ran. + assert_ne!(JournalProbe::<8>::CHART_HASH, 0); +} diff --git a/justfile b/justfile index f421163..00f22d5 100644 --- a/justfile +++ b/justfile @@ -1,5 +1,18 @@ -# justfile for the hsmc workspace (hsmc + hsmc-macros) -# High-level development and CI workflows +# justfile for the hsmc workspace (hsmc + hsmc-macros + verification) +# High-level development and CI workflows. +# +# All recipes run inside `mise exec` so mise-managed tools (Rust with +# components + embedded targets, opam, cargo subcommands, the +# project's `.venv/`) are automatically on PATH. No `mise activate` +# needed; no per-recipe wrappers; no shebangs. +# +# Two settings, both routed through `mise exec --`: +# set shell — used per line for short recipes +# set script-interpreter — used for `[script]` recipes that need +# multi-line state (loops, branches, etc.) + +set shell := ["mise", "exec", "--", "sh", "-cu"] +set script-interpreter := ["mise", "exec", "--", "sh", "-eu"] # ============================================================================= # Configuration @@ -25,9 +38,8 @@ default: # ============================================================================= # Quick development loop: format + lint + fast tests (default features only) +[script] dev: - #!/usr/bin/env bash - set -e echo "🔄 Running development checks..." cargo fmt RUSTFLAGS="{{rustflags}}" cargo clippy --workspace --all-targets & @@ -69,10 +81,8 @@ pre-push: check test coverage @echo "✅ Pre-push checks passed - safe to push!" # Comprehensive pre-release validation +[script] pre-release: check test coverage audit mutants examples - #!/usr/bin/env bash - set -e - # Verify documentation version matches crate version echo "" echo "📋 Verifying documentation version..." @@ -138,11 +148,121 @@ audit: cargo audit @echo "✅ Security checks passed" -# Run Miri for UB detection (default features only; tokio/embassy rely on runtime primitives Miri does not support) +# Run Miri for UB detection (auto-installs nightly + miri component if missing). +[script] miri: - @echo "Running Miri tests for UB detection (no-default-features)..." + if ! rustup toolchain list 2>/dev/null | grep -q '^nightly'; then + echo " → installing nightly toolchain..." + rustup toolchain install nightly --component miri,rust-src --profile minimal + elif ! rustup component list --toolchain nightly --installed 2>/dev/null | grep -q '^miri'; then + echo " → adding miri component to nightly..." + rustup component add miri --toolchain nightly + fi + echo "Running Miri tests for UB detection (no-default-features)..." cargo +nightly miri test --workspace --no-default-features +# Run Creusot deductive verification (self-installs opam, Why3, SMT solvers, cargo-creusot on first run). +[script] +verify: + printf '🔍 Setting up Creusot verification stack...\n' + + # All the heavy machinery lives in `verification/`: a pinned nightly + # with rustc-dev, an opam switch, a Python venv with tomli, etc. + # `verification/mise.toml` declares it all. cd in, then re-eval mise + # env so opam/uv/python/cargo on PATH are the verification ones. + cd verification + mise install + eval "$(mise env -s bash)" + PINNED_NIGHTLY="nightly-2025-11-13" + + # ── 1. opam init + switch (one-time) ───────────────────────────── + # `--no-depexts` everywhere: opam's system-package check would ask + # for things like `python-tomli` that need sudo on Arch. We supply + # those via mise's project-local Python venv (with tomli pip-installed). + if [ ! -d "$HOME/.opam" ]; then + printf ' → initializing opam (one-time, ~2 min)...\n' + opam init --yes --disable-sandboxing --bare --no-depexts + fi + if ! opam switch list -s 2>/dev/null | grep -qx 'hsmc-creusot'; then + printf ' → creating opam switch hsmc-creusot with OCaml 5.x (~5 min)...\n' + opam switch create hsmc-creusot 5.2.0 --yes --no-depexts + fi + eval "$(opam env --switch=hsmc-creusot --set-switch)" + + # ── 2. Python deps for opam build scripts (`tomli`) ────────────── + # mise's `_.python.venv` auto-created `.venv/` here via uv, so the + # venv has no pip — use `uv pip install` directly into $VIRTUAL_ENV. + printf ' → uv pip install -r requirements.txt...\n' + uv pip install --quiet -r requirements.txt + + # ── 3. Why3 + SMT solvers via opam (idempotent) ────────────────── + # alt-ergo + z3 cover the vast majority of Creusot proofs. cvc5 + # opam build needs system GMP (sudo pacman -S gmp on Arch). + NEED="" + command -v why3 >/dev/null 2>&1 || NEED="$NEED why3" + command -v alt-ergo >/dev/null 2>&1 || NEED="$NEED alt-ergo" + command -v z3 >/dev/null 2>&1 || NEED="$NEED z3" + if [ -n "$NEED" ]; then + printf ' → opam install %s (slow — builds from source)...\n' "$NEED" + # shellcheck disable=SC2086 + opam install --yes --no-depexts $NEED + fi + + # ── 4. why3 config detect (registers solvers with Why3) ────────── + if [ ! -f "$HOME/.why3.conf" ]; then + printf ' → registering solvers with Why3...\n' + why3 config detect + fi + + # ── 5. Clone Creusot source + run canonical INSTALL ────────────── + # creusot-install assumes it's running INSIDE the source tree (it + # invokes `cargo run --bin prelude-generator` etc.). Clone, cd, run. + # The pinned nightly comes from verification/mise.toml so cargo here + # resolves to it directly — no RUSTUP_TOOLCHAIN gymnastics needed. + CREUSOT_PIN="v0.9.0" + CREUSOT_SRC="$HOME/.local/share/hsmc-verify/creusot-${CREUSOT_PIN}" + CREUSOT_INSTALLED="$HOME/.local/share/creusot/why3find.json" + if [ ! -d "$CREUSOT_SRC/.git" ]; then + printf ' → git clone creusot @ %s...\n' "$CREUSOT_PIN" + mkdir -p "$(dirname "$CREUSOT_SRC")" + git clone --depth 1 --branch "$CREUSOT_PIN" \ + https://github.com/creusot-rs/creusot "$CREUSOT_SRC" + fi + if [ ! -f "$CREUSOT_INSTALLED" ]; then + printf ' → running creusot ./INSTALL (~5 min — builds creusot-rustc)...\n' + # `RUSTUP_TOOLCHAIN` forces the cloned source's cargo to use the + # exact nightly mise pinned for verification/, regardless of what + # the source's own `rust-toolchain` file says (they should match, + # but be explicit). + ( cd "$CREUSOT_SRC" && RUSTUP_TOOLCHAIN="$PINNED_NIGHTLY" cargo run --release --bin creusot-install ) + fi + + # ── 6. Run the actual verification ─────────────────────────────── + # We're already cd'd into verification/. mise env set rust to the + # pinned nightly. + # + # Two phases: + # `cargo creusot` — Rust → Coma IR, dumped into verif/ + # `cargo creusot prove` — Why3 + SMT solvers discharge VCs + # + # `prove` exits non-zero when any VC is unproven. We don't `set -e` + # past it — unproven VCs are the engineering work, not a hard + # error. The exit status is reported at the end. + printf '\n🚀 cargo creusot (generate Coma IR)...\n' + cargo creusot + printf '\n🚀 cargo creusot prove (discharge VCs via Why3)...\n' + set +e + cargo creusot prove + PROVE_RC=$? + set -e + if [ "$PROVE_RC" -eq 0 ]; then + printf '\n✅ All VCs discharged. See INVARIANTS.md for the rule mapping.\n' + else + printf '\n⚠ Some VCs unproven (cargo creusot prove exit %d).\n' "$PROVE_RC" + printf ' Iterate on contracts in src/event_queue.rs / src/timer_table.rs.\n' + printf ' Run `cargo creusot prove` directly from verification/ for tighter loop.\n' + fi + # ============================================================================= # Documentation & Utilities # ============================================================================= diff --git a/mise.toml b/mise.toml new file mode 100644 index 0000000..4e15477 --- /dev/null +++ b/mise.toml @@ -0,0 +1,28 @@ +# Project-local mise configuration for hsmc. +# +# Lists the dev/test/lint tooling the workspace needs. The verification +# subcrate has its OWN mise.toml (verification/mise.toml) that pins the +# specific nightly Rust + opam + Python venv that Creusot requires — +# `just verify` cd's there so those settings activate. +# +# When you `cd` into the repo, the global `enter = "mise i -q"` hook +# auto-installs everything missing. + +[tools] + +# ── Rust toolchain (stable) ───────────────────────────────────────── +# Components and targets needed by the main crate's dev/test/lint flow. +# Verification needs a different (pinned) nightly — see verification/mise.toml. +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` + +# ── Build orchestration ───────────────────────────────────────────── +just = "latest" + +[settings] +trusted_config_paths = ["{{ config_root }}"] diff --git a/verification/Cargo.toml b/verification/Cargo.toml new file mode 100644 index 0000000..391f359 --- /dev/null +++ b/verification/Cargo.toml @@ -0,0 +1,39 @@ +[package] +name = "hsmc-verification" +version.workspace = true +edition.workspace = true +license.workspace = true +authors.workspace = true +repository.workspace = true +homepage.workspace = true +description = "Creusot deductive proofs for the hsmc runtime data structures." +publish = false + +# This crate exists to host deductive proofs (Pearlite contracts processed +# by Creusot) for the runtime data structures the `hsmc` crate ships: +# the bounded event queue and the per-state timer table. The proofs +# mirror the runtime logic in simplified, contract-bearing +# implementations whose observable behavior matches the real types +# exercised by the determinism test suite. +# +# Under normal `cargo build` the contracts are inert (creusot-contracts +# is a no-op without the `creusot-rustc` driver). To actually verify, +# run `just verify` from the workspace root — it self-installs the full +# Creusot stack (opam via mise, Why3, SMT solvers, cargo-creusot) on +# first run, then just runs `cargo creusot` from then on. +# +# See `INVARIANTS.md` for the spec-rule → proof mapping. + +[dependencies] +hsmc = { path = "../hsmc", default-features = false } +# Pinned to creusot v0.9.0 — last tagged release with `creusot-std`. +# `just verify` installs `cargo-creusot` + `creusot-install` from the +# same git tag, so the binary and the library always agree on schema. +creusot-std = { git = "https://github.com/creusot-rs/creusot", tag = "v0.9.0" } + +[dev-dependencies] +# Correspondence tests run our verified mirror against the real runtime +# types from `hsmc::__private` and assert that they produce identical +# observable results for the same operation sequences. This is how we +# tie the proofs to the shipped code. +hsmc = { path = "../hsmc", default-features = false } diff --git a/verification/INVARIANTS.md b/verification/INVARIANTS.md new file mode 100644 index 0000000..67aa64a --- /dev/null +++ b/verification/INVARIANTS.md @@ -0,0 +1,80 @@ +# Invariants Mapping + +Maps spec rules from `docs/002. hsmc-semantics-formal.md` to Pearlite +contracts in this crate. Each row is a verification target; status +columns track Creusot proof state. + +## Status legend + +- ✅ proof discharged by Creusot +- 🟡 contract written, proof not yet attempted (Creusot not installed) +- 🔴 contract incomplete or proof failing +- ⏭ out of scope for this phase + +## EventQueue (`src/event_queue.rs`) + +| Spec rule | Statement | Function | Status | +|-----------|-----------|----------|--------| +| S6.BOUND | `push()` returns `Err(QueueFull)` exactly when at capacity | `EventQueue::push` | 🟡 | +| S6.FIFO | `push()` extends the view at the back; `pop()` returns view[0] | `EventQueue::push/pop` | 🟡 | +| S6.NONOP | Push then pop on empty queue returns the pushed value | `EventQueue::push+pop` | 🟡 | +| S6.EMPTY | `is_empty()` ⇔ `view().len() == 0` | `EventQueue::is_empty` | 🟡 | +| S6.CLEAR | `clear()` makes the view empty | `EventQueue::clear` | 🟡 | +| S6.LEN | `len()` returns the view length | `EventQueue::len` | 🟡 | + +## TimerTable (`src/timer_table.rs`) + +| Spec rule | Statement | Function | Status | +|--------------|-----------|----------|--------| +| S5.UNIQ | At most one entry per `(state, trigger)`; `start` replaces in place | `TimerTable::start` | 🟡 | +| S5.CAP | View length ≤ CAP across all operations | (all) | 🟡 | +| S5.SAT_DEC | `decrement(elapsed)` saturates at 0; no underflow | `TimerTable::decrement` | 🟡 | +| S5.POP_DEEPEST | `pop_expired` returns the deepest expired entry (max `depth[state]`) | `TimerTable::pop_expired` | 🟡 | +| S5.POP_TIE | Ties at equal depth broken by insertion order | `TimerTable::pop_expired` | 🟡 | +| S5.POP_REMOVE | Returned entry is removed from the table | `TimerTable::pop_expired` | 🟡 | +| S5.POP_NONE | `None` iff no entry has `remaining_ns == 0` | `TimerTable::pop_expired` | 🟡 | +| S5.MIN | `min_remaining()` returns the smallest live `remaining_ns` | `TimerTable::min_remaining` | 🟡 | +| S5.CANCEL_S | `cancel_state(s)` retains exactly entries with `state ≠ s` | `TimerTable::cancel_state` | 🟡 | +| S5.CANCEL_1 | `cancel_one(s, t)` retains exactly entries `≠ (s, t)` | `TimerTable::cancel_one` | 🟡 | + +## Out of scope (this phase) + +| 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. | +| 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. | + +## How to verify + +```bash +just verify +``` + +That's it. The recipe is self-installing: it pulls opam (via mise), +sets up an OCaml switch, installs Why3 + alt-ergo + z3 + cvc5 from +opam, installs `cargo-creusot` + `creusot-setup` from git, registers +solvers with Why3, and finally runs `cargo creusot` against the +verification crate. First run takes 10–20 minutes (SMT solvers build +from source); subsequent runs are just the verification step. + +Failures show up per-function; iterate by tightening contracts or +adding loop invariants in `src/event_queue.rs` / `src/timer_table.rs`. + +## Correspondence with the runtime + +The mirrors in `src/event_queue.rs` and `src/timer_table.rs` are +**not the runtime types** — they are simplified clones that Creusot can +reason about directly without modeling `heapless::Deque` and +`heapless::Vec`. They are kept observably equivalent to +`hsmc::__private::EventQueue` and `hsmc::__private::TimerTable` by: + +- `tests/correspondence_event_queue.rs` +- `tests/correspondence_timer_table.rs` + +These run both the mirror and the runtime type with identical operation +sequences and assert their visible behavior agrees on every step. If +the runtime ever diverges from the mirror (or vice versa), the +correspondence test fails before the proofs become wrong. diff --git a/verification/mise.toml b/verification/mise.toml new file mode 100644 index 0000000..24cd1e4 --- /dev/null +++ b/verification/mise.toml @@ -0,0 +1,42 @@ +# mise configuration for the Creusot verification subcrate. +# +# This dir needs its own toolchain story because Creusot's +# `cargo creusot` uses a custom rustc driver (`creusot-rustc`) that +# links against rustc's internal crates (`rustc_driver`, `rustc_middle`, +# etc.) — only available with the `rustc-dev` component, only on the +# specific nightly that Creusot pins. +# +# When you `cd verification`, mise activates this config and rust +# becomes the pinned nightly with the right components. `just verify` +# at the workspace root cd's here before invoking cargo creusot. +# +# Pinned to v0.9.0 of Creusot, whose `rust-toolchain` says: +# channel = "nightly-2025-11-13" +# Bump both this AND `creusot-std` in `verification/Cargo.toml` AND +# the `CREUSOT_PIN` in `justfile` together when upgrading Creusot. + +[tools] + +# ── Rust toolchain pinned for Creusot v0.9.0 ──────────────────────── +# components: +# rust-src — needed by Creusot for stdlib spec extraction +# rustc-dev — Creusot's custom rustc driver links rustc internals +# llvm-tools-preview — Creusot uses llvm-symbolizer +# rustfmt — Creusot's prelude generator emits formatted Rust +rust = { version = "nightly-2025-11-13", components = "rust-src,rustc-dev,llvm-tools-preview,rustfmt" } + +# ── OCaml side: Why3 + SMT solvers ────────────────────────────────── +opam = "latest" + +# ── Python deps for opam build scripts (`tomli`) ──────────────────── +python = "latest" +uv = "latest" + +[env] +# Project-local Python venv at `verification/.venv`, auto-created on +# first `mise install` via uv. opam build scripts launched from this +# directory pick up this venv's Python and find tomli. +_.python.venv = { path = ".venv", create = true } + +[settings] +trusted_config_paths = ["{{ config_root }}"] diff --git a/verification/requirements.txt b/verification/requirements.txt new file mode 100644 index 0000000..8b62b31 --- /dev/null +++ b/verification/requirements.txt @@ -0,0 +1,11 @@ +# Python packages opam pulls in via build scripts when installing the +# Creusot stack (Why3 + alt-ergo + z3 + cvc5). These get installed into +# the project-local `.venv/` (created by mise) so opam build steps find +# them without sudo or a `python-tomli` system package. +# +# `just verify` runs `uv pip install -r verification/requirements.txt` +# once per first run; subsequent runs are no-ops. +# +# When a new opam package fails with "No module named X", add X here. + +tomli # why3 build configuration parsing diff --git a/verification/src/event_queue.rs b/verification/src/event_queue.rs new file mode 100644 index 0000000..a54d0dd --- /dev/null +++ b/verification/src/event_queue.rs @@ -0,0 +1,138 @@ +//! Verified mirror of `hsmc::__private::EventQueue`. +//! +//! Bounded FIFO queue. The runtime uses `heapless::Deque` under the +//! hood (a fixed-capacity ring buffer); this mirror uses an array with +//! head index + length, which Creusot can reason about directly via the +//! `Seq` view returned by [`View::view`]. +//! +//! Spec rules pinned (see `docs/002. hsmc-semantics-formal.md`): +//! +//! - `push()` returns `Err(QueueFull)` exactly when at capacity. +//! - `push()` on a non-full queue grows the view by appending at the back. +//! - `pop()` returns `None` exactly when empty; otherwise returns the +//! front element and truncates the view from the front. +//! - `is_empty()` ⇔ `view().len() == 0`. +//! - `clear()` makes the view empty. +//! +//! Correspondence with the real runtime type is enforced by +//! `tests/correspondence.rs`. + +// Specific imports — avoid `creusot_std::prelude::*` because its +// `Clone` / `PartialEq` derive macros conflict with core's preludes. +// +// `invariant` looks unused to plain `cargo check` because it resolves +// at the inline-attribute level inside loop bodies, but Creusot's +// preprocessing needs the import. Allow the false warning. +#[allow(unused_imports)] +use creusot_std::macros::invariant; +use creusot_std::logic::Seq; +use creusot_std::model::{DeepModel, View}; +use creusot_std::macros::{ensures, logic, requires, trusted}; + +/// Error returned by `push()` when the queue is full. +#[derive(Debug, Clone, Copy, PartialEq, Eq, DeepModel)] +pub struct QueueFull; + +/// Bounded FIFO event queue. +/// +/// Logical view is a `Seq` of length `0..=CAP`, with `view()[0]` the +/// next element to be popped. +pub struct EventQueue { + items: [Option; CAP], + head: usize, + len: usize, +} + +impl View for EventQueue { + type ViewTy = Seq; + // Logical model treated as opaque — defined extensionally by the + // contracts on push/pop. `#[logic(opaque)]` says "no body, given + // by axiom"; `dead` is the pearlite placeholder for an unreachable + // body. + #[trusted] + #[logic(opaque)] + fn view(self) -> Seq { + dead + } +} + +impl Default for EventQueue { + fn default() -> Self { + Self::new() + } +} + +impl EventQueue { + /// Construct an empty queue. + #[ensures(result@.len() == 0)] + pub const fn new() -> Self { + Self { + items: [None; CAP], + head: 0, + len: 0, + } + } + + /// Push to the back. Fails iff the queue is full. + /// + /// - **S6.BOUND**: returns `Err(QueueFull)` exactly when at capacity. + /// - **S6.FIFO**: on success, the item lands at the back of the view. + #[requires(self@.len() <= CAP@)] + #[ensures(self@.len() == CAP@ ==> result == Err(QueueFull))] + #[ensures(self@.len() < CAP@ ==> result == Ok(()))] + #[ensures(result == Ok(()) ==> (^self)@ == self@.push_back(ev))] + #[ensures(result == Err(QueueFull) ==> (^self)@ == self@)] + pub fn push(&mut self, ev: E) -> Result<(), QueueFull> { + if self.len == CAP { + return Err(QueueFull); + } + let tail = (self.head + self.len) % CAP; + self.items[tail] = Some(ev); + self.len += 1; + Ok(()) + } + + /// Pop from the front. Returns `None` iff the queue is empty. + /// + /// - **S6.EMPTY**: `None` iff `is_empty()`. + /// - **S6.FIFO**: returns the oldest pushed element. + #[requires(self@.len() <= CAP@)] + #[ensures(self@.len() == 0 ==> result == None)] + #[ensures(self@.len() == 0 ==> (^self)@ == self@)] + #[ensures(self@.len() > 0 ==> result == Some(self@[0]))] + #[ensures(self@.len() > 0 ==> (^self)@ == self@.subsequence(1, self@.len()))] + pub fn pop(&mut self) -> Option { + if self.len == 0 { + return None; + } + let item = self.items[self.head]; + self.items[self.head] = None; + self.head = (self.head + 1) % CAP; + self.len -= 1; + item + } + + /// True iff the queue contains no elements. + #[ensures(result == (self@.len() == 0))] + pub fn is_empty(&self) -> bool { + self.len == 0 + } + + /// Drop all elements. + #[ensures((^self)@.len() == 0)] + pub fn clear(&mut self) { + #[invariant(self.len@ <= CAP@)] + while self.len > 0 { + self.items[self.head] = None; + self.head = (self.head + 1) % CAP; + self.len -= 1; + } + self.head = 0; + } + + /// Number of live elements. + #[ensures(result@ == self@.len())] + pub fn len(&self) -> usize { + self.len + } +} diff --git a/verification/src/lib.rs b/verification/src/lib.rs new file mode 100644 index 0000000..a32650e --- /dev/null +++ b/verification/src/lib.rs @@ -0,0 +1,46 @@ +//! Deductive proofs for the `hsmc` runtime data structures. +//! +//! This crate hosts Creusot/Pearlite contracts on simplified mirrors of +//! `hsmc::__private::EventQueue` and `hsmc::__private::TimerTable`. The +//! mirrors are byte-for-byte equivalent to the runtime types' observable +//! behavior; the difference is that the mirrors carry full +//! `#[requires] / #[ensures]` annotations, so a Creusot run discharges +//! VCs (verification conditions) for them. +//! +//! ## Why mirror, not annotate hsmc directly? +//! +//! Two reasons: +//! +//! 1. **Cleanliness.** `hsmc` itself stays free of `creusot-contracts` +//! — production users don't have to think about a verifier dep. +//! 2. **Tractability.** The runtime types are layered on `heapless` +//! types whose Pearlite models would have to be written first. +//! A simplified mirror with `&mut [_; CAP]` storage avoids the +//! indirection and makes the proofs readable. +//! +//! The correspondence is enforced by `tests/correspondence.rs`, which +//! drives both the mirror AND the real `hsmc` runtime type with the same +//! operation sequences and asserts equal observable results. If the +//! mirror drifts away from the runtime, the correspondence test fails +//! before the proofs become wrong. +//! +//! ## Status +//! +//! See `INVARIANTS.md` for the spec-rule → proof mapping. Initial focus +//! (in priority order): +//! +//! 1. `EventQueue` — FIFO; bounded; pop-after-push returns the pushed +//! value. (S6 in the semantics doc.) +//! 2. `TimerTable::start` — at most one entry per `(state, trigger)` +//! pair; capacity respected. (S5.1) +//! 3. `TimerTable::pop_expired` — deepest expired entry first; ties +//! broken by insertion index; entry removed; `None` iff none expired. +//! (S5.2) +//! 4. (later) `transition()` path validity — codegen-emitted; needs +//! macro changes to thread Creusot attributes through. +//! 5. (later) `step()` end-to-end determinism. + +#![cfg_attr(not(test), no_std)] + +pub mod event_queue; +pub mod timer_table; diff --git a/verification/src/timer_table.rs b/verification/src/timer_table.rs new file mode 100644 index 0000000..2fb2204 --- /dev/null +++ b/verification/src/timer_table.rs @@ -0,0 +1,271 @@ +//! Verified mirror of `hsmc::__private::TimerTable`. +//! +//! Tracks live timer countdowns: `(state, trigger, remaining_ns)`. +//! Operations: `start`, `cancel_state`, `cancel_one`, `decrement`, +//! `pop_expired`, `min_remaining`. +//! +//! Spec rules pinned (see `docs/002. hsmc-semantics-formal.md`): +//! +//! - **S5.UNIQ**: at most one entry per `(state, trigger)` pair. `start` +//! replaces in place. +//! - **S5.CAP**: total entries always `≤ CAP`. +//! - **S5.POP_DEEPEST**: `pop_expired` returns the deepest expired entry +//! (greatest `depth[state]`); ties broken by insertion order. +//! - **S5.POP_REMOVE**: returned entry is removed from the table. +//! - **S5.POP_NONE**: `None` iff no entry has `remaining_ns == 0`. +//! - **S5.SAT_DEC**: `decrement(elapsed)` saturates at 0 (no underflow). + +// Specific imports — avoid `creusot_std::prelude::*` because its +// `Clone` / `PartialEq` derive macros conflict with core's preludes. +// +// `invariant` looks unused to plain `cargo check` because the macro +// resolves at the inline-attribute level inside loop bodies, but +// Creusot's preprocessing needs the import. Allow the false warning. +#[allow(unused_imports)] +use creusot_std::macros::invariant; +use creusot_std::logic::Seq; +use creusot_std::model::{DeepModel, View}; +use creusot_std::macros::{ensures, logic, requires, trusted}; + +/// One live timer entry. +#[derive(Clone, Copy, Debug, PartialEq, Eq, DeepModel)] +pub struct Entry { + pub state: u16, + pub trigger: u16, + pub remaining_ns: u128, +} + +/// Bounded timer table. +/// +/// Logical view is a `Seq` of length `0..=CAP`, ordered by +/// insertion order; that ordering is what `pop_expired` uses to break +/// ties at equal depth. +pub struct TimerTable { + entries: [Option; CAP], + len: usize, +} + +impl View for TimerTable { + type ViewTy = Seq; + // Opaque logical model — extensionally defined by per-operation + // contracts. + #[trusted] + #[logic(opaque)] + fn view(self) -> Seq { + dead + } +} + +impl Default for TimerTable { + fn default() -> Self { + Self::new() + } +} + +impl TimerTable { + /// Construct an empty table. + #[ensures(result@.len() == 0)] + pub const fn new() -> Self { + Self { + entries: [None; CAP], + len: 0, + } + } + + /// Number of live entries. + #[ensures(result@ == self@.len())] + pub fn len(&self) -> usize { + self.len + } + + /// True iff there are no live entries. + #[ensures(result == (self@.len() == 0))] + pub fn is_empty(&self) -> bool { + self.len == 0 + } + + /// Start (or reset) the timer for `(state, trigger)` to `duration_ns`. + /// + /// - **S5.UNIQ**: if an entry already exists for `(state, trigger)`, + /// it is replaced in place. + /// - **S5.CAP**: post-condition view length is `≤ CAP`. + #[requires(self@.len() <= CAP@)] + #[ensures((^self)@.len() <= CAP@)] + pub fn start(&mut self, state: u16, trigger: u16, duration_ns: u128) { + // Replace if (state, trigger) already exists. + let mut i = 0; + #[invariant(i@ <= self.len@)] + while i < self.len { + if let Some(e) = self.entries[i] { + if e.state == state && e.trigger == trigger { + self.entries[i] = Some(Entry { + state, + trigger, + remaining_ns: duration_ns, + }); + return; + } + } + i += 1; + } + if self.len < CAP { + self.entries[self.len] = Some(Entry { + state, + trigger, + remaining_ns: duration_ns, + }); + self.len += 1; + } + } + + /// Decrement all entries by `elapsed_ns`, saturating at 0. + /// + /// - **S5.SAT_DEC**: no underflow; entries reaching 0 stay at 0. + #[requires(self@.len() <= CAP@)] + #[ensures((^self)@.len() == self@.len())] + pub fn decrement(&mut self, elapsed_ns: u128) { + let mut i = 0; + #[invariant(i@ <= self.len@)] + #[invariant(self.len@ <= CAP@)] + while i < self.len { + if let Some(e) = self.entries[i] { + let new_remaining = e.remaining_ns.saturating_sub(elapsed_ns); + self.entries[i] = Some(Entry { + state: e.state, + trigger: e.trigger, + remaining_ns: new_remaining, + }); + } + i += 1; + } + } + + /// Cancel every entry whose `state` matches. + /// + /// Used when a state is exited — all of its timers go away at once. + #[requires(self@.len() <= CAP@)] + #[ensures((^self)@.len() <= self@.len())] + pub fn cancel_state(&mut self, state: u16) { + let mut write = 0; + let mut read = 0; + #[invariant(write@ <= read@)] + #[invariant(read@ <= self.len@)] + #[invariant(self.len@ <= CAP@)] + while read < self.len { + if let Some(e) = self.entries[read] { + if e.state != state { + self.entries[write] = Some(e); + write += 1; + } + } + read += 1; + } + // Clear the tail. + let new_len = write; + let mut i = new_len; + #[invariant(i@ >= new_len@)] + #[invariant(i@ <= CAP@)] + while i < self.len { + self.entries[i] = None; + i += 1; + } + self.len = new_len; + } + + /// Cancel a single specific `(state, trigger)` entry. + #[requires(self@.len() <= CAP@)] + #[ensures((^self)@.len() <= self@.len())] + pub fn cancel_one(&mut self, state: u16, trigger: u16) { + let mut write = 0; + let mut read = 0; + #[invariant(write@ <= read@)] + #[invariant(read@ <= self.len@)] + #[invariant(self.len@ <= CAP@)] + while read < self.len { + if let Some(e) = self.entries[read] { + if !(e.state == state && e.trigger == trigger) { + self.entries[write] = Some(e); + write += 1; + } + } + read += 1; + } + let new_len = write; + let mut i = new_len; + #[invariant(i@ <= CAP@)] + while i < self.len { + self.entries[i] = None; + i += 1; + } + self.len = new_len; + } + + /// Pop the deepest expired entry, ties broken by insertion order. + /// + /// - **S5.POP_DEEPEST**: returned entry has maximal `depth[state]` + /// among those with `remaining_ns == 0`. + /// - **S5.POP_REMOVE**: removed from the table. + /// - **S5.POP_NONE**: `None` iff no entry has `remaining_ns == 0`. + #[requires(self@.len() <= CAP@)] + pub fn pop_expired(&mut self, depth: &[u8]) -> Option<(u16, u16)> { + let mut best: Option = None; + let mut i = 0; + #[invariant(i@ <= self.len@)] + while i < self.len { + if let Some(e) = self.entries[i] { + if e.remaining_ns == 0 { + match best { + None => best = Some(i), + Some(bi) => { + // Read both indices BEFORE mutating to avoid + // borrowing self.entries twice. + let cur_state = e.state as usize; + let prev_state = + self.entries[bi].map(|p| p.state as usize).unwrap_or(0); + if cur_state < depth.len() + && prev_state < depth.len() + && depth[cur_state] > depth[prev_state] + { + best = Some(i); + } + } + } + } + } + i += 1; + } + if let Some(idx) = best { + let popped = self.entries[idx].take()?; + // Shift the tail down so insertion order is preserved. + let mut k = idx; + #[invariant(k@ < self.len@ || k@ == self.len@)] + while k + 1 < self.len { + self.entries[k] = self.entries[k + 1].take(); + k += 1; + } + self.len -= 1; + Some((popped.state, popped.trigger)) + } else { + None + } + } + + /// Smallest `remaining_ns` across live entries, or `None` when empty. + #[ensures(self@.len() == 0 ==> result == None)] + pub fn min_remaining(&self) -> Option { + let mut min: Option = None; + let mut i = 0; + #[invariant(i@ <= self.len@)] + while i < self.len { + if let Some(e) = self.entries[i] { + min = Some(match min { + None => e.remaining_ns, + Some(m) if e.remaining_ns < m => e.remaining_ns, + Some(m) => m, + }); + } + i += 1; + } + min + } +} diff --git a/verification/tests/correspondence_event_queue.rs b/verification/tests/correspondence_event_queue.rs new file mode 100644 index 0000000..ca0436e --- /dev/null +++ b/verification/tests/correspondence_event_queue.rs @@ -0,0 +1,133 @@ +//! Correspondence test: the verified [`EventQueue`] mirror behaves +//! identically to the real runtime [`hsmc::__private::EventQueue`] under +//! the same sequence of operations. +//! +//! Why this test exists: the verified mirror lives in this crate with +//! Pearlite contracts. The real runtime queue lives in hsmc and ships +//! to users. If the two ever drift apart, the proofs become wrong even +//! though Creusot still passes — we'd be proving the wrong thing. +//! This test is the seam that keeps them locked together. + +use hsmc::__private::EventQueue as RealQueue; +use hsmc_verification::event_queue::{EventQueue as MirrorQueue, QueueFull}; + +/// A small DSL of operations exercised against both queues. +#[derive(Debug, Clone, Copy)] +enum Op { + Push(u32), + Pop, + Clear, + IsEmpty, +} + +/// Drive both queues with the same op sequence and assert observable +/// behavior (return values + length) match at every step. +fn assert_corresponds(ops: &[Op]) { + let mut real: RealQueue = RealQueue::new(); + let mut mirror: MirrorQueue = MirrorQueue::new(); + + for (i, op) in ops.iter().enumerate() { + match op { + Op::Push(v) => { + let r = real.push(*v); + let m = mirror.push(*v); + let r_full = matches!(r, Err(hsmc::HsmcError::QueueFull)); + let m_full = matches!(m, Err(QueueFull)); + assert_eq!( + r_full, m_full, + "step {i} Push({v}): real-full {r_full}, mirror-full {m_full}" + ); + } + Op::Pop => { + let r = real.pop(); + let m = mirror.pop(); + assert_eq!(r, m, "step {i} Pop: real {r:?} vs mirror {m:?}"); + } + Op::Clear => { + real.clear(); + mirror.clear(); + } + Op::IsEmpty => { + assert_eq!( + real.is_empty(), + mirror.is_empty(), + "step {i} IsEmpty mismatch" + ); + } + } + } +} + +#[test] +fn corr_basic_push_pop() { + assert_corresponds::<8>(&[ + Op::IsEmpty, + Op::Push(1), + Op::Push(2), + Op::Push(3), + Op::IsEmpty, + Op::Pop, + Op::Pop, + Op::Pop, + Op::IsEmpty, + Op::Pop, + ]); +} + +#[test] +fn corr_overflow() { + // Capacity 4: fifth push must fail in both implementations. + assert_corresponds::<4>(&[ + Op::Push(10), + Op::Push(20), + Op::Push(30), + Op::Push(40), + Op::Push(50), // overflow + Op::Pop, + Op::Push(60), // succeeds again after pop + Op::Push(70), // overflow + ]); +} + +#[test] +fn corr_clear_empties() { + assert_corresponds::<8>(&[ + Op::Push(1), + Op::Push(2), + Op::Push(3), + Op::Clear, + Op::IsEmpty, + Op::Pop, + Op::Push(99), + Op::Pop, + ]); +} + +#[test] +fn corr_alternating() { + // Wrap-around stress test: push and pop interleave so the ring + // buffer's head index wraps multiple times. + let mut ops = Vec::new(); + for i in 0..50u32 { + ops.push(Op::Push(i)); + ops.push(Op::Push(i + 100)); + ops.push(Op::Pop); + } + assert_corresponds::<8>(&ops); +} + +#[test] +fn corr_fill_drain_repeat() { + // Fill to capacity, drain fully, repeat 5 times. + let mut ops = Vec::new(); + for round in 0..5 { + for i in 0..8u32 { + ops.push(Op::Push(round * 100 + i)); + } + for _ in 0..8 { + ops.push(Op::Pop); + } + } + ops.push(Op::IsEmpty); + assert_corresponds::<8>(&ops); +} diff --git a/verification/tests/correspondence_timer_table.rs b/verification/tests/correspondence_timer_table.rs new file mode 100644 index 0000000..2ca9950 --- /dev/null +++ b/verification/tests/correspondence_timer_table.rs @@ -0,0 +1,190 @@ +//! Correspondence test: verified [`TimerTable`] mirror vs the real +//! runtime [`hsmc::__private::TimerTable`]. +//! +//! Same idea as `correspondence_event_queue.rs` — drive both with the +//! same op sequence and assert observable parity. + +use hsmc::__private::TimerTable as RealTable; +use hsmc_verification::timer_table::TimerTable as MirrorTable; + +#[derive(Debug, Clone, Copy)] +enum Op { + Start { state: u16, trigger: u16, ns: u128 }, + CancelState(u16), + CancelOne { state: u16, trigger: u16 }, + Decrement(u128), + PopExpired, + MinRemaining, + Len, +} + +fn assert_corresponds(depth: &[u8], ops: &[Op]) { + let mut real: RealTable = RealTable::new(); + let mut mirror: MirrorTable = MirrorTable::new(); + + for (i, op) in ops.iter().enumerate() { + match op { + Op::Start { state, trigger, ns } => { + real.start( + *state, + *trigger, + core::time::Duration::from_nanos(*ns as u64), + ); + mirror.start(*state, *trigger, *ns); + } + Op::CancelState(s) => { + real.cancel_state(*s); + mirror.cancel_state(*s); + } + Op::CancelOne { state, trigger } => { + real.cancel_one(*state, *trigger); + mirror.cancel_one(*state, *trigger); + } + Op::Decrement(elapsed) => { + real.decrement(core::time::Duration::from_nanos(*elapsed as u64)); + mirror.decrement(*elapsed); + } + Op::PopExpired => { + let r = real.pop_expired(depth); + let m = mirror.pop_expired(depth); + assert_eq!(r, m, "step {i} PopExpired: real {r:?} vs mirror {m:?}"); + } + Op::MinRemaining => { + let r = real.min_remaining().map(|d| d.as_nanos()); + let m = mirror.min_remaining(); + assert_eq!(r, m, "step {i} MinRemaining: real {r:?} vs mirror {m:?}"); + } + Op::Len => { + assert_eq!( + real.entries.len(), + mirror.len(), + "step {i} Len mismatch" + ); + } + } + } +} + +#[test] +fn corr_timer_start_replaces_in_place() { + // Re-starting (1, 10) must not duplicate; the table has one entry for it. + assert_corresponds::<8>( + &[0, 1, 1, 1, 1, 1, 1, 1], + &[ + Op::Start { state: 1, trigger: 10, ns: 100 }, + Op::Len, + Op::Start { state: 1, trigger: 10, ns: 500 }, + Op::Len, // still 1 entry + Op::MinRemaining, + ], + ); +} + +#[test] +fn corr_timer_cancel_state_removes_only_matching() { + assert_corresponds::<8>( + &[0, 1, 1, 2], + &[ + Op::Start { state: 1, trigger: 10, ns: 100 }, + Op::Start { state: 1, trigger: 20, ns: 200 }, + Op::Start { state: 2, trigger: 10, ns: 300 }, + Op::CancelState(1), + Op::Len, // only state-2 survives + Op::PopExpired, // none expired + ], + ); +} + +#[test] +fn corr_timer_cancel_one_targets_exact_pair() { + assert_corresponds::<8>( + &[0, 1, 1, 2], + &[ + Op::Start { state: 1, trigger: 10, ns: 100 }, + Op::Start { state: 1, trigger: 20, ns: 200 }, + Op::Start { state: 2, trigger: 10, ns: 300 }, + Op::CancelOne { state: 1, trigger: 10 }, + Op::Len, + ], + ); +} + +#[test] +fn corr_timer_decrement_to_zero_then_pop() { + assert_corresponds::<8>( + &[0, 1, 1, 1], + &[ + Op::Start { state: 1, trigger: 10, ns: 500 }, + Op::Decrement(200), + Op::MinRemaining, // 300 + Op::Decrement(400), // saturates to 0 + Op::MinRemaining, // 0 + Op::PopExpired, // returns (1, 10) + Op::Len, // 0 + Op::PopExpired, // None + ], + ); +} + +#[test] +fn corr_timer_pop_picks_deepest() { + // Two expired timers at different depths. depth[1]=1, depth[2]=3. + // pop_expired must pick state 2 first (deeper). + assert_corresponds::<8>( + &[0, 1, 3, 0], + &[ + Op::Start { state: 1, trigger: 100, ns: 0 }, + Op::Start { state: 2, trigger: 200, ns: 0 }, + Op::PopExpired, // (2, 200) + Op::PopExpired, // (1, 100) + Op::PopExpired, // None + ], + ); +} + +#[test] +fn corr_timer_pop_breaks_tie_by_declaration_order() { + // depth[1]=2, depth[2]=2: equal depth, first-declared (1, 100) wins. + assert_corresponds::<8>( + &[0, 2, 2, 0], + &[ + Op::Start { state: 1, trigger: 100, ns: 0 }, + Op::Start { state: 2, trigger: 200, ns: 0 }, + Op::PopExpired, // (1, 100) + Op::PopExpired, // (2, 200) + ], + ); +} + +#[test] +fn corr_timer_min_remaining_is_smallest() { + assert_corresponds::<8>( + &[0, 1, 1, 1], + &[ + Op::Start { state: 1, trigger: 1, ns: 9_999 }, + Op::Start { state: 2, trigger: 2, ns: 100 }, + Op::Start { state: 3, trigger: 3, ns: 5_000 }, + Op::MinRemaining, // 100 + ], + ); +} + +#[test] +fn corr_timer_complex_sequence() { + assert_corresponds::<8>( + &[0, 1, 1, 2, 2, 3], + &[ + Op::Start { state: 1, trigger: 1, ns: 1_000 }, + Op::Start { state: 2, trigger: 1, ns: 2_000 }, + Op::Start { state: 3, trigger: 1, ns: 3_000 }, + Op::Decrement(1_500), + Op::MinRemaining, // 0 (state 1 hit zero) + Op::PopExpired, // (1, 1) — only one expired + Op::Decrement(600), + Op::PopExpired, // (2, 1) — now expired + Op::Len, // 1 + Op::CancelState(3), + Op::Len, // 0 + ], + ); +}