Conversation
…-freedom Two FsCheck properties added to existing Merkle.Tests.fs that generalise the per-leaf-edit [<Fact>] check into shrinking-friendly property tests: - MerkleTree root is deterministic for any leaf set - MerkleTree root differs under any single-leaf edit (collision-free in practice; relies on XxHash128's 128-bit hash space making FsCheck-generator-collisions astronomically unlikely) Both properties guard against future regressions: determinism catches accidental reference-equality hashing; collision-freedom catches a regression to a smaller or structural hash. Math-proofs assessment matrix C3 row: closes 2 more after G/PN/OR/LWW counters (running total: 11 of ~15 target). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
Adds FsCheck property-based tests around MerkleTree.Root to broaden the existing example-based [<Fact>] checks, aiming to guard against determinism regressions and practical hash-collision regressions.
Changes:
- Add FsCheck/Xunit property tests for Merkle root determinism across arbitrary leaf sets.
- Add a property asserting the Merkle root changes under a single-leaf replacement (as a practical collision-freedom check).
| // Both trees built from the SAME input must produce equal roots. | ||
| // Treats null arrays as empty (FsCheck can generate null). | ||
| let safe = if isNull leaves then [||] else leaves |> Array.map (fun b -> if isNull b then [||] else b) | ||
| let t1 = MerkleTree safe | ||
| let t2 = MerkleTree safe |
| (NonEmptyArray (leaves: byte array array)) (replacement: byte array) = | ||
| // Replace the first leaf, expect a different root. The 128-bit | ||
| // XxHash makes practical collisions astronomically unlikely for | ||
| // the small inputs FsCheck generates; if the hashing pipeline | ||
| // regresses to <128 bits or to a non-collision-resistant hash, | ||
| // this property starts failing. | ||
| let arr = leaves |> Array.map (fun b -> if isNull b then [||] else b) | ||
| let r = if isNull replacement then [||] else replacement | ||
| if arr.[0] = r then true // skip cases where replacement is identical | ||
| else | ||
| let modified = Array.copy arr | ||
| modified.[0] <- r |
![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: 914b8890b9
ℹ️ 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".
| if arr.[0] = r then true // skip cases where replacement is identical | ||
| else | ||
| let modified = Array.copy arr | ||
| modified.[0] <- r |
There was a problem hiding this comment.
This property always edits arr.[0], so it does not actually validate the stated "any single-leaf edit" behavior across leaf positions. A position-dependent bug in tree construction (e.g., incorrect indexing beyond the first leaf) could still pass this test, which weakens the regression coverage the new property is intended to provide.
Useful? React with 👍 / 👎.
Summary
Two FsCheck properties added to
tests/Tests.FSharp/Storage/Merkle.Tests.fsthat generalise the per-leaf-edit[<Fact>]check into shrinking-friendly property tests:MerkleTree root is deterministic for any leaf setMerkleTree root differs under any single-leaf edit (collision-free in practice)Both properties guard against future regressions:
C3 progress
Math-proofs assessment matrix C3 row: closes 2 more after the CRDT batch (G + PN + OR + LWW each had 3). Running total: ~11 of 15 target after this PR.
Test plan
dotnet test --filter "FullyQualifiedName~MerkleTree"→ 6 passed in 137ms.🤖 Generated with Claude Code