From c50e6c18c534de86163c61ad443eba32a3b17262 Mon Sep 17 00:00:00 2001 From: Aaron Stainback Date: Sun, 3 May 2026 11:38:11 -0400 Subject: [PATCH 1/2] feat(C3 partial): Delta-CRDT anti-entropy property tests (3 more) Three FsCheck properties for DeltaCrdt at the apply layer: - GCounterDelta apply is order-independent (commutativity) - GCounterDelta apply is idempotent on Value - PNCounterDelta apply is order-independent Anti-entropy contract: applying deltas in any order, with duplicates allowed, must converge to the same state. The laws inherit from GCounter / PNCounter semilattice merges (already tested), but pinning them at the delta-apply layer guards against future regressions in DeltaCrdt's apply implementation. Math-proofs assessment matrix C3 row: closes 3 more after CRDT batch + Merkle (running total: ~14 of 15 target). Co-Authored-By: Claude Opus 4.7 --- .../Properties/Math.Invariants.Tests.fs | 41 +++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs b/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs index 5558df479..d483311cf 100644 --- a/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs +++ b/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs @@ -209,6 +209,47 @@ let ``LWW-register merge tie-breaks left on equal (timestamp, replica)`` () = (LwwRegister.Merge b a).Value |> should equal 2 +// ─── Delta-CRDT anti-entropy laws (Almeida et al. 2018) ──────────── +// Delta-state CRDTs ship per-operation deltas instead of full state. +// The anti-entropy contract: applying deltas in ANY order, with +// duplicates allowed, must converge to the same state. The laws +// inherit from GCounter/PNCounter semilattice merges, but pinning +// them at the delta-apply layer guards against future regressions +// in DeltaCrdt's apply implementation (e.g. accidentally using +// addition instead of max-merge under the hood). + +[] +let ``GCounterDelta apply is order-independent`` + (NonNegativeInt d1) (NonNegativeInt d2) = + let initial = GCounter.Empty + let priorDvv = Dvv.Empty + let delta1 = GCounterDelta.increment "r1" (int64 d1) priorDvv + let delta2 = GCounterDelta.increment "r2" (int64 d2) priorDvv + let lhs = GCounterDelta.apply (GCounterDelta.apply initial delta1) delta2 + let rhs = GCounterDelta.apply (GCounterDelta.apply initial delta2) delta1 + lhs.Value = rhs.Value + +[] +let ``GCounterDelta apply is idempotent on Value`` + (NonNegativeInt d) = + let initial = GCounter.Empty + let delta = GCounterDelta.increment "r1" (int64 d) Dvv.Empty + let once = GCounterDelta.apply initial delta + let twice = GCounterDelta.apply once delta + once.Value = twice.Value + +[] +let ``PNCounterDelta apply is order-independent`` + (d1: int) (d2: int) = + let initial = PNCounter.Empty + let priorDvv = Dvv.Empty + let delta1 = PNCounterDelta.increment "r1" (int64 d1) priorDvv + let delta2 = PNCounterDelta.increment "r2" (int64 d2) priorDvv + let lhs = PNCounterDelta.apply (PNCounterDelta.apply initial delta1) delta2 + let rhs = PNCounterDelta.apply (PNCounterDelta.apply initial delta2) delta1 + lhs.Value = rhs.Value + + // ─── HyperMinHash — Jaccard monotonicity ─────────────────────────── // Reference: Yu & Weber arXiv:1710.08436. From 6f60463aab8de7a54a8ca359c3e61b9324e2b964 Mon Sep 17 00:00:00 2001 From: Aaron Stainback Date: Sun, 3 May 2026 11:41:22 -0400 Subject: [PATCH 2/2] review(C3-delta): add PNCounterDelta idempotence + same-replica properties MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reviewer caught two gaps on #1426: P1: PNCounterDelta only had order-independence, no idempotence test — a future regression that double-applies the same delta would still pass. Added "PNCounterDelta apply is idempotent on Value" to cover duplicate-tolerance. P2: PNCounterDelta order-independence used disjoint replica IDs (r1 vs r2) which lands in disjoint GCounter components, so even a broken additive-merge implementation would appear order-independent. Added "PNCounterDelta same-replica deltas converge order-independently" which forces the merge to actually max-fold within a single replica component. Total PNCounterDelta properties now: 3 (order-independent disjoint, same-replica order-independent, idempotent). Plus 2 GCounterDelta (order-independent, idempotent). 5 anti-entropy tests total in this PR after review. Co-Authored-By: Claude Opus 4.7 --- .../Properties/Math.Invariants.Tests.fs | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs b/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs index d483311cf..34b2f785b 100644 --- a/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs +++ b/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs @@ -249,6 +249,35 @@ let ``PNCounterDelta apply is order-independent`` let rhs = PNCounterDelta.apply (PNCounterDelta.apply initial delta2) delta1 lhs.Value = rhs.Value +[] +let ``PNCounterDelta apply is idempotent on Value`` (d: int) = + // Duplicate-tolerance: applying the SAME delta twice must yield + // the same Value as applying it once. Catches a future regression + // that uses additive merge instead of GCounter max-merge — under + // additive merge, double-apply would double the count. + let initial = PNCounter.Empty + let delta = PNCounterDelta.increment "r1" (int64 d) Dvv.Empty + let once = PNCounterDelta.apply initial delta + let twice = PNCounterDelta.apply once delta + once.Value = twice.Value + +[] +let ``PNCounterDelta same-replica deltas converge order-independently`` + (d1: int) (d2: int) = + // Same-replica test exercises the WITHIN-component merge path + // (both deltas land in the same PN P-side or N-side GCounter + // entry under "r1"). The disjoint-replica order-independence + // property above can stay green even under a broken additive + // merge because deltas land in different replicas; this property + // forces the merge to actually max-fold the same component. + let initial = PNCounter.Empty + let priorDvv = Dvv.Empty + let delta1 = PNCounterDelta.increment "r1" (int64 d1) priorDvv + let delta2 = PNCounterDelta.increment "r1" (int64 d2) priorDvv + let lhs = PNCounterDelta.apply (PNCounterDelta.apply initial delta1) delta2 + let rhs = PNCounterDelta.apply (PNCounterDelta.apply initial delta2) delta1 + lhs.Value = rhs.Value + // ─── HyperMinHash — Jaccard monotonicity ─────────────────────────── // Reference: Yu & Weber arXiv:1710.08436.