fix: guarantee sequential consistency across recovery

[Tech-Matt]

Summary

main did not guarantee the sequential consistency required by specs/ds1_project_2026_v1.pdf: reads were unimplemented there, the update and election protocols were still separate, update identities were not stable, and coordinator recovery could fork or lose the committed prefix.

This PR:

• integrates the exact live heads of feat: Implement ReadTransaction class and integrate with Client and Replica #83 (14b243b), Feat: UpdateTransaction #86 (73052d2), and Implement ring-based ElectionTransaction FSM and coordinator recovery #97 (d1222a2);
• makes the coordinator the sole allocator of unique, stable EpochPair values;
• carries the same pair through UPDATE -> ACK -> WRITEOK -> apply -> history -> WriteFinish;
• starts recovery from update-phase timeouts and permits a broadcast to stop at the configured crash point;
• prevents overlapping election initiator windows from electing different coordinators for the same failed term;
• retries only writes that definitely never reached UPDATE, and separates heartbeat, ordinary, and election transaction-ID namespaces;
• adds focused concurrency, client-order, identity, and partial-WRITEOK recovery tests;
• documents the requirement, failure traces, invariants, proof, assumptions, and limitations in the sequential-consistency report.

Correctness argument

1. Client serializes each client's operations through one current transaction and a FIFO queue.
2. The coordinator actor reserves update pairs in mailbox order.
3. Per-channel FIFO ensures each participant receives update A before B and returns ACK A before ACK B.
4. Therefore B cannot obtain a strict-majority quorum before A obtains the same quorum, so the coordinator sends WRITEOK A before WRITEOK B.
5. Coordinator-to-replica FIFO makes every correct replica apply a prefix of that same order.
6. After coordinator failure, election selects the longest applied EpochPair, synchronizes one common prefix, and only then continues in a higher epoch.

The report gives the complete proof and explicitly separates this safety result from assumptions about bounded delay, strict-majority availability, and reasonable client timeouts.

Validation

Run with an isolated Gradle home because the machine's default Gradle home could not load its native platform library:

GRADLE_USER_HOME=/tmp/coredump-gradle-home gradle compileJava compileTestJava --no-daemon
GRADLE_USER_HOME=/tmp/coredump-gradle-home gradle test --tests it.unitn.ds.TestSequentialConsistency --no-daemon
GRADLE_USER_HOME=/tmp/coredump-gradle-home gradle regression --no-daemon
GRADLE_USER_HOME=/tmp/coredump-gradle-home gradle test --no-daemon
GRADLE_USER_HOME=/tmp/coredump-gradle-home gradle staticAnalysis --no-daemon
git diff --check origin/main...HEAD

Results:

• compilation: passed;
• focused sequential-consistency tests: 4/4 passed;
• regression task: passed;
• complete test suite: 80/80 passed;
• static-analysis task: BUILD SUCCESSFUL with 0 errors, 42 warnings, 2 informational findings, 2 duplication findings, and 0 formatting findings;
• full PR diff check: passed.

The non-error static-analysis findings are principally in the integrated election implementation and do not block the build. Reports are generated under build/reports/.

Integration note

Because main did not yet contain the read, update, or election state machines needed to establish this end-to-end property, this PR includes the live work from #83, #86, and #97. Those PRs should not be merged independently without reconciling their history with this branch.