feat(C3 partial): OR-Set semilattice property tests (3 more)#1423
Merged
feat(C3 partial): OR-Set semilattice property tests (3 more)#1423
Conversation
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
1 task
There was a problem hiding this comment.
Pull request overview
Adds FsCheck semilattice-law property tests for OrSet in the math invariants test suite, aligning coverage with the existing CRDT property-testing pattern used for counters while comparing on the externally observable element set.
Changes:
- Added FsCheck properties asserting commutativity, idempotence, and associativity of
OrSet.Mergeon the observableValueset. - Introduced helpers to build OR-sets from generated inputs and compare OR-set observable values via
Set.ofSeq.
Three FsCheck properties for OrSet, mirroring the G-Counter / PN-Counter pattern: - OR-set merge value is commutative - OR-set merge value is idempotent - OR-set merge value is associative Compares on the OBSERVABLE element-set (Set.ofSeq orset.Value), not on internal entry weights — OrSet.Merge is ZSet.add, so weights can vary by merge order but the externally-visible CRDT set must be invariant under semilattice laws. Math-proofs assessment matrix C3 row: closes 3 more after PN-Counter's 3 (running total: 6 of ~15 target). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
force-pushed
the
otto/c3-orset-semilattice-properties-2026-05-03
branch
from
a228fe5 to
1fdf0bf
Compare
Reviewer-flagged P1 on #1423: buildOrSet used OrSet.Add which calls Guid.NewGuid() per step, making FsCheck shrinking non-replayable and taking O(N^2) work via repeated linear merges. Fix: build Entries directly via ZSet.ofSeq with index-derived Guid tags. Deterministic across runs (same input list → same Entries), O(N log N) construction, and FsCheck can now shrink reproducibly. P2 (rename to "merge VALUE is...") was already addressed in the original commit's property names — no rename needed. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Comment on lines
+112
to
+149
| // 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) = | ||
| let a = buildOrSet xs | ||
| let b = buildOrSet ys | ||
| let c = buildOrSet zs |
Comment on lines
+107
to
+110
| // 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. |
This was referenced May 3, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Three FsCheck properties for
OrSet, mirroring the G-Counter / PN-Counter pattern:Compares on the observable element-set (
Set.ofSeq orset.Value), not on internal entry weights — OrSet.Merge isZSet.add, so weights can vary by merge order but the externally-visible CRDT set must be invariant under semilattice laws.Math-proofs assessment matrix C3 row: closes 3 more after PN-Counter's 3 (PR #1420). Running total: 6 of ~15 target.
Test plan
dotnet test --filter "FullyQualifiedName~OR-set"→ 3 passed in 160ms.dotnet buildclean.🤖 Generated with Claude Code