Module correctness_testing 

Correctness Testing Framework

Property-based testing and crash-consistency validation for SochDB.

Components

1. Property Tests: Invariant checking with proptest
2. Crash Consistency: Simulate crashes during WAL writes
3. Isolation Testing: Verify SSI guarantees
4. Linearizability: Check single-register linearizability

Design

Uses a combination of:

• Property-based testing (proptest/quickcheck style)
• Model checking for state machines
• Fault injection for crash recovery

Structs

CrashSimulator

Crash simulator for recovery testing

Discrepancy

A discrepancy between model and SUT

KvModel

Model of a key-value store for property testing

LinearOp

A linearizability operation

LinearizabilityChecker

Linearizability checker for single-register operations

TestOracle

Test oracle for comparing model vs implementation

TxnHistory

Transaction history for serializability checking

Enums

CrashPoint

Crash point for fault injection

LinearOpType

Operation type for linearizability

SerializabilityError

Serializability check error

TxnOp

Transaction operation for model checking