rewrite(phase7): batch 1 — port LifecycleStateMachine/E2ESafePoint TLA+ specs, add TLC CI job

[SoundMatt]

rewrite(phase7): batch 1 — port LifecycleStateMachine/E2ESafePoint TLA+ specs, add TLC CI job

Part of the v3.0.0 ground-up rewrite (cpp-RCP #129, ROADMAP.md Phase 17),
branch rewrite/v3-from-c-rcp. Phase 7 (formal verification + MC/DC +
release-pipeline hardening), batch 1 of several: TLA+ formal verification
only.

Scope

cpp-RCP had 3 TLA+ specs (WatchdogSafeState, RxSequenceGuard,
CrcSafeStateLatch) but was missing c-RCP's LifecycleStateMachine and
E2ESafePoint specs -- and, a real pre-existing gap discovered during
scoping, none of the 3 existing specs were ever actually run in CI.

Part A -- ported specs (both pass TLC clean)

tla/LifecycleStateMachine.tla (+229) + .cfg (+10): models
rcp::lifecycle::ServerLifecycle::transition()/check_hw_cfg()/
check_rcp_cfg(). TLC: 12 distinct states, depth 5, no error.

tla/E2ESafePoint.tla (+215) + .cfg (+17): models rcp::e2e::RxWatchdog/
apply_watchdog_overflow()/endpoint_in_configured_safe_state()/
may_execute_now(). TLC: 256 distinct states, depth 7, no error.

Both cross-referenced directly against cpp-RCP's include/rcp/lifecycle.hpp
and include/rcp/e2e.hpp against c-RCP's src/lifecycle.c/src/e2e.c --
confirmed field-for-field ports from Phase 2's content-parity pass, so
both are faithful direct ports, not mechanical transliterations. No
implementation bugs found; no C++ source touched.

One known abstraction gap documented (not fixed, correctly out of this
batch's scope): cpp's field_writable() computes FunctionalWStar locking
as a pure function of current ServerState, and transition() supports an
additional RcpConfigured->HwConfigured partial demotion that neither
this spec nor c-RCP's original models. c-RCP's own spec already
abstracts this away (sticky field_lock variable, omits the demotion
transition); this port preserves that same abstraction and flags it in
a "Known abstraction gap" comment block for future re-derivation.

Independently spot-checked against RxSequenceGuard.tla's own
FORMAL_VERIFICATION.md: a separate, genuinely pre-existing gap there
(the spec still models pre-Phase-2 non-wraparound sequence comparison,
not the real RFC 1982 forward-window rule evaluate() implements today)
is confirmed untouched by this batch (byte-identical diff against base)
-- correctly out of scope, a distinct re-derivation task.

Part B -- TLC CI automation (new gap closed for all 5 specs, not just 2)

New formal-verification job in .github/workflows/ci.yml (+44 lines),
following c-RCP's own ci.yml job as a structural reference but written
in cpp-RCP's own job-naming/style conventions: downloads tla2tools.jar
once, then runs TLC against all 5 specs in tla/ (the pre-existing 3 plus
the 2 new ports), each as its own step so a single spec's failure is
individually attributable in the Actions UI. No needs: -- TLC checking
is independent of the C++ build, matching c-RCP's own pattern.

Verification

Independently re-verified: rebuilt tla2tools.jar locally and re-ran TLC
against all 5 specs myself (not trusting the agent's own run) -- all 5
report zero errors/violations/deadlocks (WatchdogSafeState 104 states,
RxSequenceGuard 32, CrcSafeStateLatch 4, LifecycleStateMachine 12,
E2ESafePoint 256). Validated the new ci.yml job's YAML parses cleanly
and has the expected 7-step structure. Directly spot-checked the "Known
abstraction gap" comment's honesty against real lifecycle.hpp behavior,
and confirmed the RxSequenceGuard pre-existing-gap claim via a
byte-identical diff of FORMAL_VERIFICATION.md against the pre-batch
base. Full tree rebuilt from scratch: 0 errors, 0 warnings, 58/58 ctest
suites pass (100%) -- unaffected, since no C++ source was touched.

tla/LifecycleStateMachine.tla: new, +229. tla/LifecycleStateMachine.cfg:
new, +10. tla/E2ESafePoint.tla: new, +215. tla/E2ESafePoint.cfg: new,
+17. .github/workflows/ci.yml: +44 (765 -> 809 lines).

Co-Authored-By: Claude Sonnet 5 noreply@anthropic.com