Conversation
Adds three FsCheck properties for PNCounter to Math.Invariants.Tests.fs, mirroring the existing G-Counter pattern: - PN-counter merge is commutative - PN-counter merge is idempotent - PN-counter merge is associative PNCounter merges elementwise (P-side + N-side, each via GCounter.Merge), so semilattice laws inherit from G-counter directly. These properties pin that derivation — any future change to PNCounter that breaks one of the laws trips a property here. Math-proofs assessment matrix C3 row: 3 of 15 closed (the 12 remaining target OR-Set, LWW-Register, DeltaCrdt anti-entropy, Residuated lattice Galois connection, Recursive fixpoint monotonicity, Merkle pair collision-freedom, Watermark monotonicity, KLL ε-bound). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
There was a problem hiding this comment.
Pull request overview
This PR extends the math-invariants property suite with initial FsCheck coverage for PNCounter merge laws and updates the research assessment document to mark part of the C3 proof gap as closed. It fits into the repo’s broader formal-verification effort by adding executable algebraic checks alongside the existing G-counter properties.
Changes:
- Added three FsCheck properties for
PNCounter.Mergein the shared math invariants test suite. - Documented partial C3 progress in the math-proofs honest-assessment matrix.
- Linked the new PN-counter properties to the existing G-counter testing pattern in repo documentation.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs |
Adds commutative, idempotent, and associative property tests for PNCounter merge behavior. |
docs/research/2026-05-03-math-proofs-honest-assessment.md |
Updates the outstanding-work matrix to record partial completion of the C3 FsCheck-property backlog. |
Comment on lines
+83
to
+88
| let ``PN-counter merge is commutative`` (aP: int) (aN: int) (bP: int) (bN: int) = | ||
| // Bound to non-negative for Increment's contract; PN allows | ||
| // both positive (P side) and negative (N side) deltas. | ||
| let a = PNCounter.Empty.Increment("r1", int64 (abs aP)).Increment("r1", -(int64 (abs aN))) | ||
| let b = PNCounter.Empty.Increment("r2", int64 (abs bP)).Increment("r2", -(int64 (abs bN))) | ||
| (PNCounter.Merge a b).Value = (PNCounter.Merge b a).Value |
Comment on lines
+83
to
+99
| let ``PN-counter merge is commutative`` (aP: int) (aN: int) (bP: int) (bN: int) = | ||
| // Bound to non-negative for Increment's contract; PN allows | ||
| // both positive (P side) and negative (N side) deltas. | ||
| let a = PNCounter.Empty.Increment("r1", int64 (abs aP)).Increment("r1", -(int64 (abs aN))) | ||
| let b = PNCounter.Empty.Increment("r2", int64 (abs bP)).Increment("r2", -(int64 (abs bN))) | ||
| (PNCounter.Merge a b).Value = (PNCounter.Merge b a).Value | ||
|
|
||
| [<Property>] | ||
| let ``PN-counter merge is idempotent`` (p: int) (n: int) = | ||
| let a = PNCounter.Empty.Increment("r1", int64 (abs p)).Increment("r1", -(int64 (abs n))) | ||
| (PNCounter.Merge a a).Value = a.Value | ||
|
|
||
| [<Property>] | ||
| let ``PN-counter merge is associative`` (a: int) (b: int) (c: int) = | ||
| let x = PNCounter.Empty.Increment("r1", int64 (abs a)) | ||
| let y = PNCounter.Empty.Increment("r2", int64 (abs b)) | ||
| let z = PNCounter.Empty.Increment("r3", int64 (abs c)) |
Comment on lines
+96
to
+99
| let ``PN-counter merge is associative`` (a: int) (b: int) (c: int) = | ||
| let x = PNCounter.Empty.Increment("r1", int64 (abs a)) | ||
| let y = PNCounter.Empty.Increment("r2", int64 (abs b)) | ||
| let z = PNCounter.Empty.Increment("r3", int64 (abs c)) |
AceHack
added a commit
that referenced
this pull request
May 3, 2026
#1417's stryker-mutation.yml referenced a hallucinated SHA for actions/upload-artifact (9eaf0eba... claimed v5.1.0) which doesn't resolve, causing every workflow run to fail at "Set up job". Replaced with the SHA already in use elsewhere in the repo (scorecard.yml uses 043fb46d... for v7.0.1). Per Otto-364 search-first-authority + the in-repo pattern check, this SHA is verified to resolve and is the version Zeta has standardized on. Surfaced empirically: #1420's CI run (databaseId 25283000236) failed with "Unable to resolve action actions/upload-artifact@9eaf0eba..." on the very first invocation of the new workflow. Author-time discipline (next time): when adding an action SHA, grep the repo first for an existing pin to that action — it's authoritative and tested. Don't make up SHAs. Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
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
tests/Tests.FSharp/Properties/Math.Invariants.Tests.fs: merge commutative + idempotent + associative.proof-tool-coverage.md§5: PN-Counter previously had no property test (only G-Counter did). This closes the simplest gap.Test plan
dotnet test --filter "FullyQualifiedName~PN-counter"→ 3 passed in 333ms.dotnet buildclean.🤖 Generated with Claude Code