Add semantic machine testing and causal runtime probes (#85)

* feat: add semantic machine invariants

* feat: add bounded machine exploration

* feat: add causal runtime probes

Author: SandroMaglione

.changeset/fair-laws-check.md

@@ -0,0 +1,5 @@
+---
+"@typeonce/effect-machine": minor
+---
+
+Add state, step, and trace invariants for checking application semantics over planner traces, including machine-inferred builders, conditional observation requirements, structured reports, and property-test assertions. Add bounded breadth-first exploration with state-dependent event representatives, shortest witnesses, explicit truncation frontiers, and fail-closed reachability assertions. Add testing-only runtime probes with acknowledged event delivery so tests can causally inspect ignored, targetless, changing, and failed live macrosteps without adding a production `sendAndAwait` API.

README.md

@@ -21,10 +21,11 @@ require upgrading Effect in lockstep; do not override the peer to another beta.
 import { Machine } from "@typeonce/effect-machine"
 import { ClusterMachine } from "@typeonce/effect-machine/cluster"
 import { AtomMachine } from "@typeonce/effect-machine/reactivity"
+import { MachineTest } from "@typeonce/effect-machine/testing"
 ```
 
 Each ESM entrypoint is independent and tree-shakeable. Importing the root does
-not load the reactivity or cluster adapters.
+not load the reactivity, cluster, or testing modules.
 
 ## First machine
 
@@ -655,6 +656,124 @@ restrictions, checkpoint planning, and delivery guarantees are documented on
 that API. `Machine.resume` is logical resumption, not durable process or cluster
 restoration.
 
+## Property-based semantic invariants
+
+`MachineTest.verify` checks statechart structure and planner lifecycle laws.
+Application semantics belong in invariants that can be reused across generated
+scenarios and, in future, bounded exploration:
+
+```ts
+import { MachineTest } from "@typeonce/effect-machine/testing"
+import { Effect } from "effect"
+
+const invariant = MachineTest.invariants(accountMachine)
+const laws = [
+  invariant.state(
+    "balance is never negative",
+    ({ snapshot }) =>
+      snapshot.value.balance >= 0 ||
+      `negative balance: ${snapshot.value.balance}`
+  ),
+  invariant.step(
+    "withdrawal removes exactly its amount",
+    ({ before, event, after }) =>
+      event._tag !== "Withdraw" ||
+      after.value.balance === before.value.balance - event.amount
+  )
+]
+
+const generated = MachineTest.scenarios(accountMachine, {
+  minEvents: 0,
+  maxEvents: 30
+})
+
+it.effect.prop(
+  "preserves account laws",
+  { scenario: generated.arbitrary },
+  ({ scenario }) =>
+    MachineTest.run(accountMachine, scenario).pipe(
+      Effect.tap((trace) => MachineTest.verify(accountMachine, trace)),
+      Effect.flatMap((trace) => MachineTest.assertInvariants(accountMachine, trace, laws))
+    )
+)
+```
+
+State invariants observe settled startup and public-event states by default.
+Set `observe` to `"microsteps"`, `"all"`, or `"final"` for a different scope.
+Use `when` for conditional laws. A condition with no matches is reported as
+`untested`; add `require: { minObservations: 1 }` when a particular trace must
+exercise it. `checkInvariants` returns this report, while `assertInvariants`
+returns `void` for direct use in property tests. Failures retain the complete
+shrunk trace and precise event, microstep, configuration, and observation
+location.
+
+These APIs inspect planner evidence. Staged action effects, invokes, timing,
+and process scheduling require the runtime command-model APIs instead.
+
+Use bounded exploration when random scenarios should be complemented by a
+systematic search over concrete event representatives:
+
+```ts
+const explored = yield * MachineTest.explore(accountMachine, {
+  events: ({ snapshot }) => [
+    new Deposit({ amount: 1 }),
+    new Withdraw({ amount: snapshot.value.balance }),
+    new Withdraw({ amount: snapshot.value.balance + 1 })
+  ],
+  stateKey: ({ snapshot }) => `${snapshot.value._tag}:${snapshot.value.balance}`,
+  limits: {
+    maxDepth: 20,
+    maxStates: 1_000,
+    maxTransitions: 10_000
+  },
+  invariants: laws
+})
+
+const rejected = yield * MachineTest.assertReachable(
+  explored,
+  "insufficient funds rejection",
+  ({ configuration }) => configuration.includes("Rejected")
+)
+
+console.log(rejected.trace.scenario.events) // shortest witness
+```
+
+Exploration is breadth-first, so each retained node owns its shortest trace.
+It is exhaustive only for the concrete events returned by `events` and the
+equivalence relation defined by `stateKey`. Equal keys intentionally collapse
+snapshots and only the first representative is expanded. Results distinguish
+`Complete` from `Truncated` and retain the depth, state, or transition frontier
+that hit a limit. An unreachability assertion succeeds only for a complete
+result; otherwise it fails as inconclusive. Cycles are retained as graph edges,
+but exploration does not enumerate every cyclic path. Invariants are checked
+on startup and on each planned edge extending a node's shortest trace.
+
+## Causal runtime probes
+
+Pure traces do not execute invokes or the managed runtime. When a test needs to
+prove that one live event has actually left the mailbox, attach a testing-only
+probe to a statechart reference:
+
+```ts
+const ref = yield * Machine.start(machine)
+const probe = yield * MachineTest.probe(machine, ref)
+
+const step = yield * probe.sendAndAwait(new CancelRequested({}))
+
+assert.strictEqual(step.handled, false)
+assert.deepStrictEqual(step.before, step.after)
+```
+
+`sendAndAwait` completes after that event's synchronous macrostep and managed
+commit work. It also completes for ignored events, which publish no snapshot
+and therefore cannot be synchronized by waiting for `ref.changes`.
+
+The step retains the exact runtime plan, before/after logical snapshots, and
+whether the event was handled or changed/reentered the active configuration.
+It does not wait for timers or invoked processes to finish. Production code
+continues to use enqueue-only `ref.send`; probes are exported only from the
+separate testing entry point.
+
 ## Current limits
 
 Declarative first-class guards are not part of the current API. Ordinary

docs/agent-guide.md

@@ -724,6 +724,97 @@ This is not durable runtime restoration. `ClusterMachine` has a separate
 checkpoint/planning contract and process-local restrictions; do not substitute
 `Machine.resume` for cluster recovery.
 
+## Testing machine semantics
+
+Import planner testing tools from the dedicated entrypoint:
+
+```ts
+import { MachineTest } from "@typeonce/effect-machine/testing"
+```
+
+Use three distinct layers:
+
+1. `MachineTest.verify(machine, trace)` checks structural statechart and
+   planner lifecycle laws.
+2. `MachineTest.assertInvariants(machine, trace, laws)` checks application
+   semantics such as conservation, authorization, and exact state updates.
+3. Runtime command models check executed actions, invokes, timing, process
+   publication, and cancellation. Planner traces do not execute this work.
+
+Define semantic laws with a machine-bound builder so the callback receives the
+exact state and event types:
+
+```ts
+const invariant = MachineTest.invariants(machine)
+
+const laws = [
+  invariant.state("balance is never negative", ({ snapshot }) =>
+    snapshot.value.balance >= 0 || "negative balance"),
+  invariant.step("withdrawal is exact", ({ before, event, after }) =>
+    event._tag !== "Withdraw" ||
+    after.value.balance === before.value.balance - event.amount),
+  invariant.trace("all inputs were planned", ({ trace }) =>
+    trace.steps.length === trace.scenario.events.length)
+]
+```
+
+State laws observe settled states by default. Select `"microsteps"`, `"all"`,
+or `"final"` only when the law requires that evidence. A `when` condition with
+no matches is explicitly `untested`; use
+`require: { minObservations: 1 }` when the current trace must exercise it.
+Prefer `assertInvariants` inside FastCheck properties because it succeeds with
+`void`. Use `checkInvariants` when the test needs the per-law report.
+
+For systematic planner exploration, provide a finite abstraction explicitly:
+
+```ts
+const explored = yield * MachineTest.explore(machine, {
+  events: ({ snapshot }) => eventRepresentatives(snapshot),
+  stateKey: ({ snapshot }) => logicalStateKey(snapshot),
+  limits: { maxDepth: 20, maxStates: 1_000 },
+  invariants: laws
+})
+```
+
+The event callback returns concrete representatives, not schemas or
+arbitraries. Include meaningful boundary values based on the current snapshot.
+The key defines which snapshots are treated as equivalent; it must retain every
+piece of data that can change the future behavior being tested. A coarse key
+can make exploration finite but under-approximate behavior.
+
+`assertReachable` returns the shortest witness. `assertUnreachable` succeeds
+only when `explored.completeness` is `Complete`. Never interpret a truncated
+depth, state, or transition frontier as an unreachability proof. The explorer
+retains cycles as graph edges but does not enumerate every path around them;
+use a separate temporal/path model when a law depends on repeated traversal
+rather than logical-state reachability.
+
+Do not encode application invariants as guards merely to make them testable.
+Keep ordinary TypeScript branching in transition handlers unless a choice is
+part of the statechart topology. Invariants independently verify the resulting
+trace without changing production transition selection.
+
+### Live event causality
+
+Use a probe when a test must establish that one event was processed by a
+running statechart rather than merely accepted by its mailbox:
+
+```ts
+const ref = yield * Machine.start(machine)
+const probe = yield * MachineTest.probe(machine, ref)
+const step = yield * probe.sendAndAwait(event)
+```
+
+Inspect `step.before`, `step.after`, `step.plan`, `step.handled`, and
+`step.configurationChanged`. An ignored event has `handled: false` and an
+empty microstep list, but still completes its acknowledgement. A targetless
+handler has `handled: true` even if its before and after snapshots are equal.
+
+Do not use a probe as a substitute for a domain completion event. The
+acknowledgement covers the submitted event's synchronous macrostep, state
+commit, emissions, and invoke startup; it does not wait for an invoke or timer
+to complete. Application code should continue to use `MachineRef.send`.
+
 ## Common compiler errors
 
 ### `initial` is not callable