Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
50 changes: 50 additions & 0 deletions tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Comment on lines +107 to +110
//
// 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<int> =
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<byte> 16
(System.BitConverter.GetBytes i).CopyTo(bytes, 0)
(x, System.Guid bytes), 1L)
{ Entries = ZSet.ofSeq entries }

[<Property>]
let ``OR-set merge value is commutative`` (xs: int list) (ys: int list) =
let a = buildOrSet xs
let b = buildOrSet ys
orSetValueEqual (OrSet<int>.Merge a b) (OrSet<int>.Merge b a)

[<Property>]
let ``OR-set merge value is idempotent`` (xs: int list) =
let a = buildOrSet xs
orSetValueEqual (OrSet<int>.Merge a a) a

[<Property>]
let ``OR-set merge value is associative`` (xs: int list) (ys: int list) (zs: int list) =
Comment thread
AceHack marked this conversation as resolved.
let a = buildOrSet xs
let b = buildOrSet ys
let c = buildOrSet zs
Comment on lines +112 to +149
let lhs = OrSet<int>.Merge (OrSet<int>.Merge a b) c
let rhs = OrSet<int>.Merge a (OrSet<int>.Merge b c)
orSetValueEqual lhs rhs


// ─── HyperMinHash — Jaccard monotonicity ───────────────────────────
// Reference: Yu & Weber arXiv:1710.08436.

Expand Down
Loading