crdt example: property-based law checks over the executable merge

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). |

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)))

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 +)")