diff --git a/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs b/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs index f4985f048..aa2d52e3e 100644 --- a/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs +++ b/tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs @@ -102,6 +102,56 @@ let ``PN-counter merge is associative`` (a: int) (b: int) (c: int) = lhs.Value = rhs.Value +// ─── OR-Set — semilattice laws on observable element set ────────── +// OrSet.Merge is ZSet.add on the (elem, tag) entries. Internal +// weights can vary across merge orderings (Merge a a doubles weights), +// but the *observable* set (elements with ANY weight > 0) is the +// CRDT contract. These properties pin the laws on the observable +// set, which is the layer external code consumes. +// +// Tag derivation: deterministic Guid from list-index so FsCheck +// shrinking is replayable. Naive `OrSet.Empty.Add x` would call +// Guid.NewGuid() on every step, which (a) makes shrinking +// non-replayable and (b) takes O(N^2) work via repeated linear +// merges. Building Entries directly via ZSet.ofSeq is deterministic +// and O(N log N). + +let private orSetValueEqual<'T when 'T : comparison> + (a: OrSet<'T>) (b: OrSet<'T>) = + Set.ofSeq a.Value = Set.ofSeq b.Value + +let private buildOrSet (xs: int list) : OrSet = + let entries = + xs + |> List.mapi (fun i x -> + // Encode list-index into a 16-byte Guid for determinism; + // index is unique per call so no collisions across xs. + let bytes = Array.zeroCreate 16 + (System.BitConverter.GetBytes i).CopyTo(bytes, 0) + (x, System.Guid bytes), 1L) + { Entries = ZSet.ofSeq entries } + +[] +let ``OR-set merge value is commutative`` (xs: int list) (ys: int list) = + let a = buildOrSet xs + let b = buildOrSet ys + orSetValueEqual (OrSet.Merge a b) (OrSet.Merge b a) + +[] +let ``OR-set merge value is idempotent`` (xs: int list) = + let a = buildOrSet xs + orSetValueEqual (OrSet.Merge a a) a + +[] +let ``OR-set merge value is associative`` (xs: int list) (ys: int list) (zs: int list) = + let a = buildOrSet xs + let b = buildOrSet ys + let c = buildOrSet zs + let lhs = OrSet.Merge (OrSet.Merge a b) c + let rhs = OrSet.Merge a (OrSet.Merge b c) + orSetValueEqual lhs rhs + + // ─── HyperMinHash — Jaccard monotonicity ─────────────────────────── // Reference: Yu & Weber arXiv:1710.08436.