Verification — Invariants

scripts/verify.sh runs the language-default binary (Rust by default) through these checks. scripts/cross_test.sh then re-runs the same scenarios in Go and C++ and asserts the behaviorally observable outputs match. The internal layouts are not required to match — only the API behavior.

#InvariantHow verified
V1Skip list round-trip: insert(k, v) then get(k) == v for all kdsbench skiplist roundtrip 10000
V2Skip list iteration is in sorted orderdsbench skiplist iter 1000 piped to sort -c
V3Skip list level distribution is geometric (p=0.5 ± tolerance)histogram chi-square check in unit test
V4Skip list max level stays ≤ MAX_LEVEL even with 100k insertsbench reports max_level_used
V5Hash table round-trip: insert(k, v) then get(k) == v for all kdsbench hashtable roundtrip 10000
V6Hash table max probe distance ≤ 4 × log₂(cap × load) at load ≤ 0.85unit test asserts
V7Hash table resizes at load 0.85, capacity doubles, max-probe dropsunit test
V8Backward-shift deletion never leaves a lookup holeunit test: insert 100, delete random 50, assert remaining 50 still found
V9Insert with same key twice replaces value, len() unchangedunit test
V10Cross-language: insert sequence [5, 1, 3, 8, 2] into skip list, iter output is sorted in all 3 langscross_test.sh
V11Cross-language: hash table after inserting same 1000 keys reports same len()cross_test.sh
V12Cross-language: roundtrip of the same N keys works in all 3 langscross_test.sh

Running

./scripts/verify.sh          # ~5s, runs Rust binary
DSE_BIN=./src/go/bin/dsbench ./scripts/verify.sh
DSE_BIN=./src/cpp/build/dsbench ./scripts/verify.sh

./scripts/cross_test.sh      # builds all 3, runs cross-language checks

What to do when a check fails

FailureMost likely cause
V1, V5Off-by-one in insert path; key not normalized
V2Skip list level 0 chain has out-of-order pointer write
V3RNG broken: same bit pattern reused per call
V4Level cap not enforced
V6Hash table not actually power-of-two; home_slot = hash % cap not masking
V7Load-factor check uses > instead of >=, or len not decremented on delete
V8Tombstones left in array; backward-shift loop terminates too early
V11Hash function differs across langs — must be FNV-1a in all three