test: model-based (stateful) test of transact/retract/checkpoint/reopen against a reference model #385

Problem

No test runs random sequences of operations against a file-backed database and compares every result with a simple reference model. The storage and index bugs of the last three months only appear after sequences like these:

• selective_fact_fetch drops new assertion when retract+transact share tx_count in WriteTransaction #285, bug: EavtKey and AevtKey missing value bytes causes silent data loss when batching multi-valued facts #287, perf: point query on a bound entity scans the entity's whole version history — O(retract/reassert count), not O(live facts) #323, bug: after a kill during an active run the EAVT index silently loses most entities' entries while AEVT stays intact — entity-bound lookups return [] and no rebuild path exists #370, bug: same-transaction multi-valued facts read back as ONE value, differing between EAVT and AEVT; a batched retract can leave retracted values visible #371
• same-transaction multi-values
• retract and reassert
• several checkpoints
• reopen

Ask

Add a stateful property test, for example with proptest-state-machine. It keeps an in-memory Vec<Fact> as the reference model.

• Operations: transact (including multi-valued batches), retract (including batched retracts), WriteTransaction with several valid-time windows, checkpoint, drop and reopen, and reopen with a small page cache.
• Checks after each step:
  • entity-bound, attribute-bound, value-bound and full-scan queries
  • :as-of N for random N
  • :valid-at T for random T
  • All of these must match the model.
• Backend: file-backed, in a temp dir, so the on-disk B+tree and the packed pages are exercised.
• Nightly job: add it to the property-test job with a high case count, and keep a small case count in normal CI.

The minimized cases this test finds should become regression tests.