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

[pyrex41]

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), and
tier (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 the doc-* semilattice laws. The LWW-Map (doc) is the
  CRDT the demo actually uses, but only gc-* and lww-* had law predicates.
  Adds doc-eq? (order- and duplicate-independent, via an effective-field
  comparison mirroring gc-eq?) plus doc-idempotent? / doc-commutative? /
  doc-associative?. Still loads clean under (tc +).
• selftest.lua — a new 2b. laws by PROPERTY section. A seeded PRNG
  generates 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 note
  now 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 over
the 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.lua green.

🤖 Generated with Claude Code

---

Generated by Claude Code

[pyrex41]

Verified against current main (e47bbfd, 33 commits ahead of this branch's fork point). Merges with zero conflicts; nothing it touches was modified on main since.

Ran on the merged tree (luajit 2.1):

• luajit examples/crdt/selftest.lua — exit 0. Convergence in three sync orders identical; tier (b) hand-picked laws ok; tier (b) property run all nine laws x 2000 random cases ok; tier (c) crdt_laws.shen loads under (tc +) with all three proof terms checking.
• bin/shen -e '(tc +) (load "examples/crdt/crdt_laws.shen")' — loads clean.
• make test — 500 pass, 0 fail across 14 specs.
• make certify — 134 passed, 0 failed, 100%.

One fix pushed on top (833bd10): the property harness's failure path was broken. prop dispatched on arity with an and/or chain, which falls through on a false value — so for arity-1 and arity-2 laws a genuine counterexample skipped the reporting branch and instead applied the predicate to three arguments, aborting the run with an opaque Shen attempt to apply a non-function error and printing nothing. Only arity-3 laws reported correctly. The all-green path was unaffected, which is why it wasn't caught. Now dispatches explicitly; verified by temporarily swapping gc-commutative?'s body for a non-law, which now prints FAIL @ case 1 / a = gc{A:1} / b = gc{A:4,C:3,C:1} and carries on to the remaining laws.