feat(C3 partial): LWW-Register semilattice property tests (3 more)#1424
Merged
feat(C3 partial): LWW-Register semilattice property tests (3 more)#1424
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: f3867dd42d
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
There was a problem hiding this comment.
Pull request overview
Adds FsCheck semilattice-law properties for LwwRegister to extend the CRDT math-invariants test suite (continuing the C3 “math proofs” coverage work alongside prior PN-Counter and OR-Set additions).
Changes:
- Add FsCheck properties asserting
LwwRegister.Mergeis commutative, idempotent, and associative. - Add a helper equality function for
LwwRegister<int>since the type disables structural equality.
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…ie-break Fact 3 P2 reviewer comments on #1424 surfaced a real issue: LwwRegister.Merge is left-biased on FULL key equality (Timestamp=Timestamp AND Replica=Replica), so commutativity FAILS for that corner. The original property test used independent NonEmptyString-generated replica ids; FsCheck almost never hit the equal-key case, so the property "passed" by chance not by design. Fix: - Constrained the commutative + associative properties to use hard-coded distinct replica ids ("r1", "r2", "r3"). That makes full-key equality impossible, which is the LWW invariant that each (Timestamp, Replica) pair is a unique write-identity. - Renamed properties to "merge is commutative under unique replica ids" + "merge is associative under unique replica ids" so the domain restriction is visible in the test name. - Added [<Fact>] "LWW-register merge tie-breaks left on equal (timestamp, replica)" that exercises the deliberate left-bias contract — the asymmetric corner gets pinned as a unit test (not a property) because it's asymmetric by design. The rationale comment now correctly documents the LWW invariant and the deliberate left-bias on full-key equality. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Three FsCheck properties for LwwRegister, mirroring the G-Counter / PN-Counter / OR-Set pattern: - LWW-register merge is commutative - LWW-register merge is idempotent - LWW-register merge is associative LwwRegister.Merge picks larger timestamp; ties broken by replica-id (lexicographic ordinal) for determinism. The semilattice laws hold because (timestamp, replica) is a total order with deterministic tie-breaking. Math-proofs assessment matrix C3 row: closes 3 more after PN-Counter + OR-Set (running total: 9 of ~15 target). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
AceHack
force-pushed
the
otto/c3-lwwregister-properties-2026-05-03
branch
from
552fdd6 to
d56e677
Compare
Comment on lines
+167
to
+169
| // A separate property below exercises the deliberate tie-breaking | ||
| // (equal timestamps + equal replicas) to lock the deterministic | ||
| // left-bias contract; that one uses lwwEqual on the whole state. |
Comment on lines
+202
to
+204
| // merge is intentionally left-biased — picks the left argument. | ||
| // This is the documented determinism contract; commutativity | ||
| // does NOT hold in this corner. Pinned as a [<Fact>] (not |
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
LwwRegister, completing the third CRDT in the C3 list (after PN-Counter #1420 and OR-Set #1423):LwwRegister.Merge picks larger timestamp; ties broken by replica-id (lexicographic ordinal) for determinism. The semilattice laws hold because (timestamp, replica) is a total order with deterministic tie-breaking.
Math-proofs assessment matrix C3 row: running total 9 of ~15 target after this PR (G-Counter already had 3; +PN-Counter 3 +OR-Set 3 +LWW 3).
Test plan
dotnet test --filter "FullyQualifiedName~LWW-register"→ 3 passed in 97ms.🤖 Generated with Claude Code