Verification — db-23 capstone
Acceptance criteria
| # | Property | Where checked |
|---|---|---|
| 1 | SHA-256 implementation matches NIST vectors. | sha256_vectors test, all 3 langs. |
| 2 | SplitMix64 matches the known value splitmix64(0). | splitmix64_known test, all 3 langs. |
| 3 | Happy-path Put/Del fully replicates and applies on every node. | put_then_del_replicates test, all 3 langs. |
| 4 | After a fault window + catch_up, all three nodes converge. | fault_window_then_catchup_converges test, all 3 langs. |
| 5 | Per-node snapshot layout is exactly 82 bytes for a 1-op cluster. | snapshot_layout_smoke test, all 3 langs. |
| 6 | The normal scenario is deterministic (two runs hash-equal). | workload_is_deterministic test, all 3 langs. |
| 7 | The fault scenario is deterministic. | fault_scenario_is_deterministic test, all 3 langs. |
| 8 | Normal scenario hashes to the frozen golden. | scenario_normal_frozen test, all 3 langs + cross_test.sh. |
| 9 | Fault scenario hashes to the frozen golden. | scenario_fault_frozen test, all 3 langs + cross_test.sh. |
Each language runs its own copy of the 9 tests, so the suite total is
27 assertions of cross-cutting properties plus 6 hash-equality checks
across languages (3 langs × 2 scenarios) in cross_test.sh.
How to run
bash scripts/verify.sh # ends with === OK ===
bash scripts/cross_test.sh # ends with === ALL OK ===
Failure-mode triage
| Symptom | Likely cause |
|---|---|
| Rust passes, Go/C++ fails frozen test | Map iteration order — confirm Go sorts keys, confirm std::map (not std::unordered_map). |
| All three languages disagree on the same scenario | RNG-stream drift — check that step_op draws exactly 3 words regardless of kind. |
| Determinism test fails within one language | Some hidden non-determinism (HashMap, address ordering). Switch to ordered map. |
| Snapshot length wrong | Off-by-one in log_len/kv_len u32, or wrong endian. |
| Fault test fails only in C++ | Probably unsigned char vs char in MAGIC comparison, or signed arithmetic on i64. |
Frozen hashes (locked)
HASH_NORMAL = 5976b45b9f40f440e8249da27fe4fe752e005f606efc3596bdb25ca4e4f99296
HASH_FAULT = d67c36725af65242e985a308db5152af2a3e2525fab33d11ed6e826a252ff792
These constants live in src/rust/src/lib.rs, src/go/db23_test.go, and src/cpp/src/db23.h, and are also hard-coded in scripts/cross_test.sh. Changing any byte of the wire format requires regenerating all five copies in lock-step.