Personalization Correctness Verification

Problem Statement

tidalDB's core value proposition is the personalization loop: a signal is written (view, like, share, completion), its effect decays over time, and subsequent ranking queries reflect the updated signal state within milliseconds. If any link in this chain is mathematically wrong or stale, the entire product thesis falls apart.

Today the loop is implemented and exercised by milestone UAT tests, but there is no dedicated verification suite that:

Proves the mathematical correctness of exponential decay (hot tier), windowed counting (warm tier), velocity computation, and preference vector EMA updates against known analytical solutions.
Proves ranking reactivity — that a signal write is reflected in the next ranking query within a bounded latency (target: < 100ms end-to-end from signal() return to retrieve() observing the change).
Proves score monotonicity and ordering invariants — that the ranking pipeline preserves the expected ordering when signal weights, decay parameters, and boost configurations change.

Scope

In Scope

Decay correctness tests: Given a known signal history (timestamps, weights, lambda), assert that HotSignalState::current_score() matches the analytical closed-form S(t) = sum_i(w_i * exp(-lambda * (t - t_i))) within IEEE 754 f64 tolerance (< 1e-10 relative error).
Out-of-order event correctness: Verify that out-of-order signal ingestion produces the same final score as in-order ingestion (modulo f64 ordering differences bounded by < 1e-10).
Windowed count correctness: Verify that BucketedCounter returns accurate counts for 1h window (minute-bucket granularity), and that 24h/7d windows degrade predictably for sparse event streams (documented in MEMORY.md).
Velocity correctness: Verify that read_velocity() returns windowed_count / window_duration_seconds for non-AllTime windows and 0.0 for AllTime.
Preference vector EMA correctness: Verify that PreferenceVectors::update() computes the EMA correctly: v_new = (1 - alpha) * v_old + alpha * embedding, with adaptive learning rate alpha = base / (1 + ln(count + 1)).
Ranking reactivity test: Write a signal via db.signal(), immediately call db.retrieve() with a profile that uses the signal, and assert the signal is reflected — total wall-clock time < 100ms.
Score ordering invariants: Verify that for the for_you profile, higher engagement (more likes, more views) produces higher ranking scores. Verify that the interaction boost (INTERACTION_BOOST_WEIGHT = 0.3) is additive and monotonic.
Boost/penalty linearity: Verify that profile boosts are additive (score += weight * agg) and penalties are subtractive (score -= weight * agg), and that neither can produce NaN or infinity.
Gate filtering correctness: Verify that candidates below a gate threshold are excluded, and candidates at or above the threshold pass.
Diversity post-condition: Verify that after diversity enforcement, no creator exceeds max_per_creator items in the result set.

Out of Scope

Baseline comparison (covered by pg1-baseline-comparison).
Metrics instrumentation (covered by pg1-instrumented-metrics).
Distributed/replicated correctness (covered by M8 CRDT reconciliation tests).
Community policy enforcement (covered by M10 tests).
Performance benchmarking beyond the 100ms reactivity assertion.

Success Criteria

Criterion	Measurement	Target
Decay accuracy	Relative error vs. analytical closed-form	< 1e-10
Out-of-order convergence	Final score difference (in-order vs out-of-order)	< 1e-10
Windowed count accuracy (1h)	Exact match for minute-granularity events	0 error
Velocity formula	Exact match: count / window_seconds	0 error
Preference EMA	Relative error vs. manual EMA computation	< 1e-6 (f32)
Ranking reactivity	Wall-clock from signal() return to retrieve() observing change	< 100ms
Score monotonicity	Higher engagement => higher score for for_you profile	Boolean pass
Boost/penalty linearity	Additive/subtractive; no NaN/Inf	Boolean pass
Gate filtering	Below-threshold excluded, at-threshold included	Boolean pass
Diversity post-condition	max_per_creator never exceeded	Boolean pass

Technical Approach

All verification tests will be placed in a new integration test file tidal/tests/pg1_personalization_correctness.rs. Tests use TidalDb::builder().ephemeral() with a controlled schema to avoid filesystem dependencies.

Decay Verification Strategy

The analytical reference is computed independently in the test using the recurrence:

S(0) = 0
For each event (t_i, w_i) in chronological order:
  S(t_i) = S(t_{i-1}) * exp(-lambda * (t_i - t_{i-1})) + w_i
At query time t_q:
  S(t_q) = S(t_last) * exp(-lambda * (t_q - t_last))

This is compared against db.read_decay_score() which internally calls HotSignalState::current_score().

Reactivity Verification Strategy

A tight loop: write signal, then immediately retrieve. Measure wall-clock time. The signal write path is synchronous (WAL-first, then in-memory hot/warm update), so the score is available on the next read without any async propagation delay. The 100ms budget includes WAL append, hot-tier CAS, and full retrieve pipeline execution.

Dependencies

None. This feature uses only existing public API methods.

Risks

Risk	Mitigation
f64 precision differences across platforms	Use relative error bounds (1e-10) rather than exact equality
Warm-tier 24h/7d inaccuracy for sparse streams	Document as known limitation; test only 1h window for exact correctness
Test flakiness from wall-clock timing	Use `Instant::elapsed()` with generous margin (100ms is 10x expected latency)

5.8 KiB Raw Blame History