test: validate recorded engine runs against the TLA+ model

[rgamba]

Stacked on #35.

Summary

#35 model-checks a TLA+ spec of how the engine drives a workflow. That shows properties hold in the model, but nothing tied the model to the code. This PR adds trace validation:

• record what the real engine does during the end-to-end test suites;
• check each recorded run against the spec;
• fail when the code takes a step the spec says it can't.

That catches spec drift, and it catches engine changes that break the protocol even while the tests stay green.

Design

• Recording (testutils/.../trace). -PskipperTraceDir=<dir> makes TestRuntime and WorkflowTest wrap the store and scheduler in tracing decorators. Without the property, nothing changes.

  • Every write is logged as one JSON line, under one lock, so the file order is the commit order.
  • A line holds the operation, the engine call site (from the stack), and a snapshot of everything the model tracks for that workflow, read back after the write.
  • Three reads are logged too, because the model treats them as steps: the handler loading its instance, the handler loading its timers, and a signal loading its instance.
  • Only the stock SQLite and MySQL backends are wrapped. Tests that inject their own store or scheduler steer interleavings by blocking inside calls, and the lock would change what they test.
  • No production code changes. The SkipperRuntime backend checks pass wrapping factories.

• Conversion (formal/tla/trace/trace_to_tla.py). Splits each trace by workflow, maps each write to its model action by operation and call site, and reduces state to model values.

  • Checkpoint and persisted-signal writes are dropped, because the model doesn't track those rows.
  • Workflows using unmodelled features (compensation, execution timeout, cancel, rewind) are reported as skipped, not silently passed.

• Checking (SkipperTrace.tla). A step either consumes the next event (takes its action and must land exactly on its snapshot) or is silent (changes no durable state).

  • Silent steps stand for what the code does without writing: time passing, a lease lapsing, a run's body.
  • The workflow body is left free, constrained only to what waitUntil allows, so the check covers the engine's protocol for any workflow code.

• Bounded checks. Each trace gets a time budget (TRACE_BUDGET, default 300 s). A trace TLC can't decide in time is reported as inconclusive, with a CI warning, instead of stalling the job. Only rejections fail it.

• Keeping the search small. TLC has to guess whatever the trace doesn't pin down. Several measures cut that down, and each can only make the checker reject more, never accept a wrong run:

  • log the three reads the model treats as steps, instead of guessing when they happened;
  • run the workflow body's waits in order;
  • require a body's outcome to match an upcoming recorded persist;
  • treat workers as interchangeable;
  • drop counters that only record history;
  • let time move a row only when the next event needs it.

  The details are in formal/tla/trace/README.md.

• Self-test (mutants.py). A checker loose enough to accept anything would also be green. --self-test corrupts every accepted trace in five ways (versions, statuses, dropped writes, swapped writes), and every mutant must be rejected.

• CI. A new trace-validation job in formal.yml records traces from the end-to-end suites (record_traces.sh) and runs check_traces.sh --self-test.

  • Both formal jobs now also trigger on src/main/** and testutils/**, since engine changes are exactly what trace validation is for.
  • Neither job is required.

What it has found so far

The spec was wrong in these places, and they're now fixed:

The code	The spec had
createWorkflow inserts RUNNING	CREATED. This also corrects finding 1 in #35's README: the stuck workflow is RUNNING.
A persist moves timers only as Timer.Status.canTransitionTo allows	any transition
A retry with a zero delay is due at once	retries always backed off
A terminal workflow that runs again is persisted again, which bumps its version	the run was skipped
Signals take the in-memory path when FORCE_SIGNAL_WORKFLOW_EXEC_IN_SCHEDULER is off	always the scheduler
Callers invoke the method again	one start call
In-memory copies run on the instance they were queued with	a fresh read
The handler's instance read and timer read are separate steps	one step

All of #35's model configs still give their expected verdicts: the four open bugs are still found, and #12 still reproduces with its gate off.

Testing

• Tracing doesn't change test outcomes. record_traces.sh runs these with tracing on, and they all pass: the SQLite integration suite, the coroutine, factory, service, scheduler-manager, SQLite-scheduler, lease-renewal and timer-handler tests, and skipper-testutils. That writes 121 trace files. Tracing initially broke two tests; both are fixed:
  • SqliteSchedulerTest failed because my decorator rejected the null partition callers pass to mean no filtering.
  • LostSignalOnHonoredLeaseTest failed because the lock stalled its blocking scheduler wrapper; custom backends are no longer traced.
• Trace validation on those traces:
  • 90 of 90 in-scope workflow runs accepted, 0 inconclusive.
  • 113 skipped: 95 tests that write to the store directly, 14 compensation, 2 execution timeout, 1 cancellation, 1 rewind.
  • The self-test rejected 442 of 442 mutants.
  • About 7 minutes locally with 8 parallel checks. The longest trace (104 events) takes 23 seconds; before the search-size work it didn't finish within 10 minutes.
• It catches an engine change the end-to-end tests miss. I temporarily changed TimerTaskHandler to schedule the workflow before expiring its timer:
  • the end-to-end suites stayed green, and one unit test caught it;
  • trace validation rejected 8 workflow runs, each at exactly the reordered step;
  • the change was reverted and isn't part of this PR.
• Model suite. formal/tla/check.sh gives all 10 verdicts as expected.
• Format. spotlessCheck is clean, and actionlint passes on the workflow.