From 5c8356f9d85397cfb227a3b8b8d368e869bef31c Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 2 Jul 2026 04:46:17 +0000 Subject: [PATCH] crdt example: property-based law checks over the executable merge MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Claude-Session: https://claude.ai/code/session_01CC5aXvUTaaNgfGHQJjGsvX --- examples/crdt/README.md | 30 ++++++++++++-------- examples/crdt/crdt.shen | 51 ++++++++++++++++++++++++++++++++++ examples/crdt/selftest.lua | 57 ++++++++++++++++++++++++++++++++++++++ 3 files changed, 127 insertions(+), 11 deletions(-) diff --git a/examples/crdt/README.md b/examples/crdt/README.md index 1d24207..41ee8dd 100644 --- a/examples/crdt/README.md +++ b/examples/crdt/README.md @@ -42,13 +42,19 @@ datatypes make illegal states unrepresentable and every merge/value/law function is proved well-typed before anything runs. Zero extra work. **(b) Laws by execution — the default.** `gc-commutative?`, -`gc-associative?`, `gc-idempotent?` (and the LWW equivalents) are ordinary Shen -predicates that run the laws over sample states, identically on every port. -This is *instance* checking — and it earns its keep: while building this -example it caught a real bug where `gc-merge` duplicated one replica's keys and -dropped the other's. Types were perfectly happy (both results are well-typed -`gcounter`s); `gc-commutative? = false` is what flagged it. That is the exact -bug class — silent replica divergence — these laws exist to kill. +`gc-associative?`, `gc-idempotent?`, their LWW equivalents, and `doc-*` (the +laws for the CRDT the demo actually uses) are ordinary Shen predicates that run +the laws over states, identically on every port. `selftest.lua` runs them two +ways: on a handful of hand-picked states (including adversarial malformed ones — +duplicate keys, clock ties), and then **property-based** over 2000 random states +each (a seeded PRNG, so a failure prints a reproducible counterexample). This +earns its keep: while building the example it caught a real bug where `gc-merge` +duplicated one replica's keys and dropped the other's. Types were perfectly +happy (both results are well-typed `gcounter`s); `gc-commutative? = false` is +what flagged it. That is the exact bug class — silent replica divergence — these +laws exist to kill. Running over thousands of random states, including the +shipped `doc-merge`, is the cheapest way to narrow the model↔code gap that +tier (c) below is honest about not closing. **(c) Laws by proof — `crdt_laws.shen`.** Universally quantified, no inputs. The three semilattice laws are encoded as a `datatype` (an equational logic: @@ -73,8 +79,10 @@ proposition (Curry–Howard). But be precise about what's proved: satisfy. Tier (c) proves universal *consequences* of them. Tier (b) is what certifies the *executable* `gc-merge` actually satisfies them. - Re-deriving the axioms from `gc-merge`'s definition (induction over the - tally-list representation) would close the model↔code gap, but that is real - proof engineering and is deliberately out of scope. + tally-list representation) would *close* the model↔code gap, but that is real + proof engineering and is deliberately out of scope. Tier (b)'s property run + *narrows* it — the executable merges are checked on thousands of random states + — without claiming a universal proof over the representation. - The trade versus Coq/Agda is **trust, automation, and totality**, not expressiveness: you author the logic's rules (and could make them unsound), there are no tactics, and Shen does not check termination. What you get is a @@ -85,10 +93,10 @@ proposition (Curry–Howard). But be precise about what's proved: | file | what it is | |---|---| -| `crdt.shen` | the typed kernel: G-Counter, LWW-Register, LWW-Map, merges, and the tier-(b) law checks. Pure portable Shen — the same source every port runs. | +| `crdt.shen` | the typed kernel: G-Counter, LWW-Register, LWW-Map, merges, and the tier-(b) law checks (`gc-*`, `lww-*`, `doc-*`). Pure portable Shen — the same source every port runs. | | `crdt_laws.shen` | tier (c): the equational logic + machine-checked proofs of the merge laws. | | `app.lua` | OpenResty glue: marshals the JSON document ↔ the Shen `doc`, calls `doc-merge` as the authoritative convergence point, stores the canonical doc in a `lua_shared_dict`. | | `nginx.conf` | serves the API and the two-replica page; boots Shen once per worker. | -| `selftest.lua` | runs convergence (sync in different orders → identical doc), the tier-(b) laws, and the tier-(c) proof load — no nginx, no network. | +| `selftest.lua` | runs convergence (sync in different orders → identical doc), the tier-(b) laws (hand-picked + property-based over 2000 random states each), and the tier-(c) proof load — no nginx, no network. | | `public/index.html` | two replicas you edit offline and Sync; they converge. | | `json_shim.lua` | a tiny JSON codec for running off-nginx (OpenResty bundles cjson). | diff --git a/examples/crdt/crdt.shen b/examples/crdt/crdt.shen index a63573b..f77cf6d 100644 --- a/examples/crdt/crdt.shen +++ b/examples/crdt/crdt.shen @@ -228,3 +228,54 @@ {(list field) --> (list field) --> (list field)} [] Acc -> Acc [F | Fs] Acc -> (doc-collect Fs (doc-absorb F Acc))) + +(define doc-fields + {doc --> (list field)} + [doc Fs] -> Fs) + +\\ effective register for a field name: lww-merge over EVERY entry that carries +\\ it (so a malformed doc with a duplicated key collapses the same way gc-get +\\ takes the max). [] = the field is absent, [R] = present with register R. +(define doc-lookup + {string --> (list field) --> (list register)} + K Fs -> (doc-lookup-acc K Fs [])) + +(define doc-lookup-acc + {string --> (list field) --> (list register) --> (list register)} + _ [] Acc -> Acc + K [[K R] | Fs] [] -> (doc-lookup-acc K Fs [R]) + K [[K R] | Fs] [R0] -> (doc-lookup-acc K Fs [(lww-merge R R0)]) + K [_ | Fs] Acc -> (doc-lookup-acc K Fs Acc)) + +(define reg-opt-eq? + {(list register) --> (list register) --> boolean} + [] [] -> true + [R1] [R2] -> (lww-eq? R1 R2) + _ _ -> false) + +\\ every field named in Fs resolves to the same effective register in A and B +(define doc-sub? + {(list field) --> doc --> doc --> boolean} + [] _ _ -> true + [[K _] | Fs] A B -> (and (reg-opt-eq? (doc-lookup K (doc-fields A)) (doc-lookup K (doc-fields B))) + (doc-sub? Fs A B))) + +\\ order- and duplicate-independent equality: A and B agree on every field of +\\ either. The right notion for the laws, exactly like gc-eq?. +(define doc-eq? + {doc --> doc --> boolean} + A B -> (and (doc-sub? (doc-fields A) A B) (doc-sub? (doc-fields B) A B))) + +\\ -- the semilattice laws for the DEMOED crdt, as executable checks (tier b) -- +(define doc-idempotent? + {doc --> boolean} + A -> (doc-eq? (doc-merge A A) A)) + +(define doc-commutative? + {doc --> doc --> boolean} + A B -> (doc-eq? (doc-merge A B) (doc-merge B A))) + +(define doc-associative? + {doc --> doc --> doc --> boolean} + A B C -> (doc-eq? (doc-merge A (doc-merge B C)) + (doc-merge (doc-merge A B) C))) diff --git a/examples/crdt/selftest.lua b/examples/crdt/selftest.lua index 0aee496..db8df6c 100644 --- a/examples/crdt/selftest.lua +++ b/examples/crdt/selftest.lua @@ -16,6 +16,8 @@ package.path = root .. "/?.lua;" .. root .. "/examples/crdt/?.lua;" .. package.p local app = require("app") local cjson = app.json local shen = require("shen") +local IO = require("lua_interop") +local sym = IO.sym local fail = 0 local function ok(cond, label) @@ -110,6 +112,61 @@ ok(shen.call("gc-idempotent?", shen.call("gDup")) == true, ok(shen.call("lww-commutative?", shen.call("rX"), shen.call("rY")) == true, "lww-commutative? on same (ts,id), different value") +-- =========================================================================== +print("\n== 2b. laws by PROPERTY: the executable merge over random states ==") +-- Hand-picked cases test the laws on instances someone thought of. This runs +-- them over thousands of RANDOM states — including the shipped `doc-merge` (the +-- CRDT the demo actually uses) — which is the cheapest way to shrink the +-- model<->code gap tier (c) can't yet bridge. The PRNG is seeded, so any +-- failure prints a reproducible counterexample. +local seed = 2463534242 +local function rnd() seed = (seed * 1103515245 + 12345) % 2147483648; return seed / 2147483648 end +local function rint(n) return math.floor(rnd() * n) end +local function pick(t) return t[1 + rint(#t)] end + +-- Small alphabets so ids/keys collide (dup keys) and clocks tie — the adversarial +-- corners. Generators produce a plain-Lua SPEC (for printing) + the Shen value. +local IDS, KEYS, VALS = { "A", "B", "C" }, { "name", "role", "team" }, { "ada", "grace", "x", "y" } +local function gc_spec() local n = rint(4); local s = {}; for i = 1, n do s[i] = { pick(IDS), rint(5) } end; return s end +local function reg_spec() return { pick(VALS), rint(4), pick(IDS) } end +local function doc_spec() local n = rint(4); local s = {}; for i = 1, n do s[i] = { pick(KEYS), reg_spec() } end; return s end + +local function gc_build(s) return { sym("gc"), s } end -- s entries already {id,n} +local function reg_build(s) return { sym("lww"), s[1], s[2], s[3] } end +local function doc_build(s) local fs = {}; for i, f in ipairs(s) do fs[i] = { f[1], reg_build(f[2]) } end; return { sym("doc"), fs } end + +local function reg_str(s) return ("%s@%d/%s"):format(s[1], s[2], s[3]) end +local function gc_str(s) local p = {}; for _, t in ipairs(s) do p[#p+1] = t[1]..":"..t[2] end; return "gc{"..table.concat(p, ",").."}" end +local function doc_str(s) local p = {}; for _, f in ipairs(s) do p[#p+1] = f[1].."="..reg_str(f[2]) end; return "{"..table.concat(p, " ").."}" end + +local N = 2000 +local function prop(label, spec, build, str, pred, arity) + local fn = IO.fn(pred) + for i = 1, N do + local sa, sb, sc = spec(), spec(), spec() + local r = (arity == 1 and fn(build(sa))) + or (arity == 2 and fn(build(sa), build(sb))) + or fn(build(sa), build(sb), build(sc)) + if r ~= true then + print((" %-42s FAIL @ case %d"):format(label, i)) + print(" a = " .. str(sa)); if arity >= 2 then print(" b = " .. str(sb)) end + if arity >= 3 then print(" c = " .. str(sc)) end + fail = fail + 1; return + end + end + ok(true, label .. " (" .. N .. " random cases)") +end + +prop("gc-idempotent?", gc_spec, gc_build, gc_str, "gc-idempotent?", 1) +prop("gc-commutative?", gc_spec, gc_build, gc_str, "gc-commutative?", 2) +prop("gc-associative?", gc_spec, gc_build, gc_str, "gc-associative?", 3) +prop("lww-idempotent?", reg_spec, reg_build, reg_str, "lww-idempotent?", 1) +prop("lww-commutative?",reg_spec, reg_build, reg_str, "lww-commutative?",2) +prop("lww-associative?",reg_spec, reg_build, reg_str, "lww-associative?",3) +prop("doc-idempotent?", doc_spec, doc_build, doc_str, "doc-idempotent?", 1) +prop("doc-commutative?",doc_spec, doc_build, doc_str, "doc-commutative?",2) +prop("doc-associative?",doc_spec, doc_build, doc_str, "doc-associative?",3) + -- =========================================================================== print("\n== 3. universally-quantified proofs, checked by the type system (tier c) ==") shen.eval("(tc +)")