db-18 — Verification

Prerequisites

• Rust ≥ 1.74 with cargo on PATH.
• Go ≥ 1.22 (module declares go 1.22).
• CMake ≥ 3.20 and a C++17 compiler (Apple clang ≥ 14, gcc ≥ 11).
• A POSIX sha256sum is not required — each binary computes its own sha256 in-process.

One command

cd db-18-paxos
bash scripts/verify.sh && bash scripts/cross_test.sh

Green is === verify OK === followed by === ALL OK ===. Anything else is a regression.

What verify.sh does

1. Rust — cargo build --release then cargo test --release. Builds paxos18 lib + paxosctl binary; runs the 12 inline tests in src/rust/src/lib.rs. Expected output ends with test result: ok. 12 passed.
2. Go — go build ./... then go test ./.... Builds cmd/paxosctl + package; runs the 11 tests in src/go/paxos_test.go. Expected output ends with PASS and ok github.com/10xdev/dse/db18.
3. C++ — cmake -DCMAKE_BUILD_TYPE=Release .., make -j, then ./test_db18. Builds db18_lib, paxosctl, test_db18; the test binary prints one line per assertion-group and ends with ALL 11 TESTS PASSED.

If any of these three blocks fails, the script exits non-zero and the rest does not run.

What cross_test.sh does

For each of the six canonical scenarios (A–F), it invokes the three release binaries with identical flags, captures stdout, and asserts rust == go == cpp byte-for-byte. The output prints the matching hash on success; on mismatch it prints all three hashes and exits.

The script does not trust the canonical hashes from this repo to be correct — it only enforces consistency among the three implementations. The "is the hash also the historical fingerprint" check happens by comparing the script's output against docs/observation.md § Expected canonical hashes.

What green guarantees

If both scripts pass:

1. Safety in the modeled environment. For every seed × scenario in the suite, no acceptor stored a decided value that contradicts another node's decided value for the same slot. The unit tests include cases for dueling proposers, partitions, and Phase-1 recovery; the cross-test sweeps the same scenarios across three independent implementations.
2. Determinism. Same inputs ⇒ same canonical dump bytes, across languages and across machines (modulo endianness — all targets are little-endian).
3. Liveness in the modeled environment. Scenarios A, B, D, F all include proposals and run long enough to elect a leader and decide them. Scenarios C and E exist to confirm we don't decide when we shouldn't (C has no proposals; E isolates node 0 so it must not influence the chosen value while {1,2} still carry the load).

What green does not guarantee

• Behavior outside the canonical scenarios. The state space of three-process Multi-Paxos is exponential; six fingerprints are an acceptance test, not a model checker. A real Paxos audit needs TLA+ (see references.md § Background reading).
• Performance. No latency or throughput is checked. Scenario A takes ~150 ticks of simulated time to decide; that is a function of the configured ELECTION_TIMEOUT_MIN, not a wall-clock SLA.
• Snapshotting, membership change, log compaction. None of these exist in this lab; the dump grows unboundedly in accepts and learned. db-23 covers the rest.
• Production safety primitives — leader leases, fsync barriers, on-disk checksums, recovery from torn writes, byzantine actors. All deliberately out of scope.

Invariant assertions in code

Each implementation re-checks the lab's invariants where the cost is near-zero. The most load-bearing assertions are listed below; their firing means the test that triggered them is reporting a symptom of a Phase-1 / Phase-2 bug, not a flaky test.