crdt example: property-based law checks over the executable merge#32
Open
pyrex41 wants to merge 1 commit into
Open
crdt example: property-based law checks over the executable merge#32pyrex41 wants to merge 1 commit into
pyrex41 wants to merge 1 commit into
Conversation
Follow-up to the CRDT example. Tier (b) previously checked the semilattice laws on a handful of hand-picked states — instance checking. This adds property-based checking over 2000 random states each (seeded PRNG, so a failure prints a reproducible counterexample), which is the cheapest way to narrow the model<->code gap the README's tier (c) is honest about not closing: the SHIPPED merges are now exercised on thousands of random inputs, not four. - crdt.shen: add the doc-* semilattice laws (doc-eq? via an order/duplicate- independent effective-field comparison, plus doc-idempotent?/commutative?/ associative?). The LWW-Map is the CRDT the demo actually uses, so proving its merge laws is the highest-value part; previously only gc-* and lww-* had them. - selftest.lua: a "2b. laws by PROPERTY" section generating random G-Counters, registers, and docs over small alphabets (so ids/keys collide and clocks tie — the adversarial corners), running all nine laws over 2000 cases each. 18000 checks; verified the harness can go red (a non-law reports a counterexample). - README: tier (b) reframed as property-based; the honest-scope note now says the property run *narrows* the model<->code gap without claiming a universal proof over the representation. Port suite green (467/467); crdt selftest green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CC5aXvUTaaNgfGHQJjGsvX
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
2 participants
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.
Follow-up to the CRDT example. Its README is honest that tier (c)'s proofs are
about an axiomatized
join, not the shipped merge (the model↔code gap), andtier (b) only checked the laws on a handful of hand-picked states. This PR does
the cheapest thing that narrows that gap: property-based checking of the
executable merge over thousands of random states.
Changes
crdt.shen— add thedoc-*semilattice laws. The LWW-Map (doc) is theCRDT the demo actually uses, but only
gc-*andlww-*had law predicates.Adds
doc-eq?(order- and duplicate-independent, via an effective-fieldcomparison mirroring
gc-eq?) plusdoc-idempotent?/doc-commutative?/doc-associative?. Still loads clean under(tc +).selftest.lua— a new2b. laws by PROPERTYsection. A seeded PRNGgenerates random G-Counters, registers, and docs over small alphabets (so ids
and keys collide and clocks tie — the adversarial corners), then runs all nine
laws over 2000 cases each (18k checks). On failure it prints a reproducible
counterexample. I confirmed the harness can go red (pointing it at a non-law
reports a violation immediately), so the green result is meaningful.
README.md— tier (b) reframed as property-based; the honest-scope notenow says the property run narrows the model↔code gap without claiming a
universal proof over the representation.
Why this and not a full inductive proof
Re-deriving the semilattice axioms from
doc-merge's definition (induction overthe field-list representation) would close the gap, but that's real proof
engineering and out of scope for an example. Property-testing the shipped merge
on thousands of random states is the high-value, low-cost step — and it's the
exact bug class (silent replica divergence on inputs no one hand-picked) these
laws exist to catch.
Port suite green (467/467);
luajit examples/crdt/selftest.luagreen.🤖 Generated with Claude Code
Generated by Claude Code