Verification — What to Test and How

Property tests (per language)

#TestPass if
V1crc32_known_vectors"" → 0x00000000; "a" → 0xE8B7BE43; "123456789" → 0xCBF43926
V2roundtrip_smallappend "hello" "world", iter yields exactly those two payloads
V3roundtrip_1000_variableappend 1000 records of pseudo-random sizes 1..1024, iter yields identical sequence
V4truncated_tailopen, append A and B, fsync, write 5 bytes of garbage past EOF, reopen ⇒ iter yields {A,B} only
V5corrupt_payloadflip one bit in the payload of record 2 of 5, iter yields {1} (stops at first bad)
V6corrupt_headeroverwrite len of record 2 with 0xFFFFFFFF, iter yields {1}
V7reopen_truncates_garbagescenario V4 followed by a new append, total iter yields {A,B,C} and file size equals exactly the three records' total bytes
V8append_returns_offsetoffset returned by appendₙ equals sum of (header+payload) for records 0..n-1

Cross-language test

scripts/cross_test.sh performs a six-way matrix: for each writer ∈ {go, rust, cpp} and reader ∈ {go, rust, cpp}, write 500 records of varying sizes with a fixed seed in the writer language, read them in the reader language, assert the payload list matches exactly.

This catches:

  • Endianness mistakes in len/crc.
  • Different CRC polynomials or initial value / final XOR.
  • Off-by-one in header parse.
  • fsync not being called before the reader runs (we close the writer between phases).

Manual smoke

./build/walbench append /tmp/wal 100 64
./build/walbench read /tmp/wal | tail
# expected: OK n=100 bytes=7300
./build/walbench corrupt /tmp/wal 50 0xFF
./build/walbench read /tmp/wal | tail
# expected: stops well before record 100, reports bad record

What "passing" means

  • All 8 property tests green in all three languages.
  • cross_test.sh exits 0 (9 successful writer×reader runs).
  • Manual smoke: corruption stops the reader cleanly, no panic / no segfault, no infinite loop.