tidaldb/docs/planning/milestone-8/phase-3/task-06-reconciliation-property-tests.md

Task 06: Reconciliation Property Tests

Delivers

Property tests in tidal/tests/m8p3_crdt.rs verifying: no double-counting after merge, hard negatives never leak, merge is commutative/associative/idempotent across 5 simulated nodes and 100K random operations.

Complexity: M

Dependencies

• Tasks 01-05 complete

Technical Design

// tidal/tests/m8p3_crdt.rs

use proptest::prelude::*;
use tidaldb::replication::crdt::{PNCounter, LWWRegister, HlcTimestamp};

proptest! {
    /// PNCounter merge commutativity.
    #[test]
    fn pn_counter_commutative(
        ops_a in vec((0u16..5, 0u64..1000, bool::arbitrary()), 0..100),
        ops_b in vec((0u16..5, 0u64..1000, bool::arbitrary()), 0..100),
    ) {
        let mut a = PNCounter::new();
        let mut b = PNCounter::new();
        apply_ops(&mut a, &ops_a);
        apply_ops(&mut b, &ops_b);

        let mut merge_ab = a.clone(); merge_ab.merge(&b);
        let mut merge_ba = b.clone(); merge_ba.merge(&a);
        prop_assert_eq!(merge_ab.value(), merge_ba.value());
    }

    /// PNCounter merge idempotency.
    #[test]
    fn pn_counter_idempotent(
        ops in vec((0u16..5, 0u64..1000, bool::arbitrary()), 0..100),
    ) {
        let mut counter = PNCounter::new();
        apply_ops(&mut counter, &ops);
        let original_value = counter.value();

        counter.merge(&counter.clone());
        prop_assert_eq!(counter.value(), original_value);
    }

    /// No double-counting: two nodes with disjoint operations.
    #[test]
    fn pn_counter_no_double_count(
        ops_a in vec((0u64..1000u64), 0..50),
        ops_b in vec((0u64..1000u64), 0..50),
    ) {
        let mut a = PNCounter::new();
        let mut b = PNCounter::new();
        let node_a = ShardId(0);
        let node_b = ShardId(1);

        let expected: u64 = ops_a.iter().sum::<u64>() + ops_b.iter().sum::<u64>();
        for &v in &ops_a { a.increment(node_a, v); }
        for &v in &ops_b { b.increment(node_b, v); }

        a.merge(&b);
        prop_assert_eq!(a.value(), expected);
    }

    /// LWW register commutativity.
    #[test]
    fn lww_register_commutative(
        val_a in 0u8..=1u8,
        wall_a in 0u64..1000,
        logical_a in 0u32..100,
        node_a in 0u16..5,
        val_b in 0u8..=1u8,
        wall_b in 0u64..1000,
        logical_b in 0u32..100,
        node_b in 0u16..5,
    ) {
        let ts_a = HlcTimestamp { wall_ns: wall_a, logical: logical_a, node_id: node_a };
        let ts_b = HlcTimestamp { wall_ns: wall_b, logical: logical_b, node_id: node_b };

        let mut reg_a: LWWRegister<u8> = LWWRegister::empty();
        let mut reg_b: LWWRegister<u8> = LWWRegister::empty();
        reg_a.write(val_a, ts_a);
        reg_b.write(val_b, ts_b);

        let mut merge_ab = reg_a.clone(); merge_ab.merge(&reg_b);
        let mut merge_ba = reg_b.clone(); merge_ba.merge(&reg_a);
        prop_assert_eq!(merge_ab.get(), merge_ba.get());
    }

    /// Hard negatives never leak: hide always wins over unhide when hide has higher HLC.
    #[test]
    fn hard_neg_hide_wins_with_higher_hlc(
        hide_wall in 100u64..1000,
        unhide_wall in 0u64..100,
    ) {
        let ts_hide = HlcTimestamp { wall_ns: hide_wall, logical: 0, node_id: 0 };
        let ts_unhide = HlcTimestamp { wall_ns: unhide_wall, logical: 0, node_id: 1 };

        let mut reg: LWWRegister<HardNegAction> = LWWRegister::empty();
        reg.write(HardNegAction::Hide, ts_hide);
        let mut remote: LWWRegister<HardNegAction> = LWWRegister::empty();
        remote.write(HardNegAction::Unhide, ts_unhide);

        reg.merge(&remote);
        prop_assert_eq!(reg.get(), Some(&HardNegAction::Hide));
    }
}

Acceptance Criteria

• pn_counter_commutative: 10K proptest cases pass
• pn_counter_idempotent: 10K proptest cases pass
• pn_counter_no_double_count: 10K proptest cases pass (sum of distinct increments == merged value)
• lww_register_commutative: 10K proptest cases pass
• hard_neg_hide_wins_with_higher_hlc: 10K proptest cases pass (hide with higher HLC always wins)
• Integration test: two TidalDb instances process 500 overlapping signals during simulated partition; after ReconciliationEngine::plan() + apply(), decay scores match ground truth (single-node replay of all events) to 6 decimal places
• cargo test --test m8p3_crdt passes in < 30 seconds
• cargo clippy -D warnings and cargo fmt pass