diff --git a/examples/README.md b/examples/README.md
index 4631b5e..2fec0ca 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -1,15 +1,26 @@
 # Examples
 
-Four examples, smallest first (the first three run with plain
-`luajit`/`bin/shen`, no external dependencies, no network):
+Smallest first (everything except the OpenResty web apps runs with plain
+`luajit`/`bin/shen`, no external dependencies, no network; each web app also
+has a `selftest.lua` that runs off-nginx):
 
 | | |
 |---|---|
 | [`hello_embed.lua`](hello_embed.lua) | the smallest useful embedding: boot, define a typed Shen function, call it from Lua, pass lists both ways. `luajit examples/hello_embed.lua` |
 | [`family.shen`](family.shen) | Shen Prolog in twenty lines — facts, rules, yes/no and binding queries. `bin/shen examples/family.shen` |
-| [`config_check.lua`](config_check.lua) | the showcase, walked through below. `luajit examples/config_check.lua` |
+| [`config_check.lua`](config_check.lua) | the interop showcase, walked through below. `luajit examples/config_check.lua` |
+| [`configc/`](configc/) | a typed config **compiler**: one config validates *and* generates a Kubernetes Deployment + nginx server block; a generator type-bug is caught at load. `luajit examples/configc/configc.lua` |
+| [`policy/`](policy/) | a typed **authorization** gateway: one rule set enforced at the OpenResty edge and previewed in the browser, plus authz-as-type-inhabitation (a permission *is* a proof). `luajit examples/policy/selftest.lua` |
+| [`crdt/`](crdt/) | a **CRDT** sync hub: replicas converge via a typed join-semilattice merge whose laws are checked by execution *and* by machine-checked sequent-calculus proof. `luajit examples/crdt/selftest.lua` |
 | [`openresty/`](openresty/) | a complete web app — typed Shen validators + a Shen router on OpenResty (nginx + LuaJIT), with a front end that runs the **same** rules in the browser (Ratatoskr-shaken, ShenScript-compiled). Runs standalone via `luajit examples/openresty/selftest.lua`; see [its README](openresty/README.md) to serve it. |
 
+The last three (`configc/`, `policy/`, `crdt/`) are a themed trio: each extracts
+a correctness-critical kernel into one typed, portable Shen file that runs
+across tiers, and each climbs the same assurance ladder — types make illegal
+states unrepresentable, laws/rules are checked by execution, and the sharpest
+properties are *proved* by Shen's sequent-calculus type checker. See each
+example's README for the walkthrough.
+
 ---
 
 # Lua ⇄ Shen interop: a typed validation layer for Lua config tables
diff --git a/examples/configc/README.md b/examples/configc/README.md
new file mode 100644
index 0000000..5ebf4aa
--- /dev/null
+++ b/examples/configc/README.md
@@ -0,0 +1,57 @@
+# Typed config compiler — validate, then generate
+
+A config compiler that takes one high-level service config and, **only if it
+validates**, emits deployment artifacts — a Kubernetes `Deployment` and an
+nginx server block — from that single source. Validation and generation are one
+typed Shen file (`configc.shen`), loaded under `(tc +)`, so a bug in a
+*generator* is a type error at load, before any config is ever compiled.
+
+```
+luajit examples/configc/configc.lua        # compile good/bad configs on the CLI
+```
+
+Or the live web preview under OpenResty:
+
+```
+mkdir -p examples/configc/logs
+openresty -p "$PWD/examples/configc" -c nginx.conf
+# open http://127.0.0.1:8092/ — edit the config, watch the artifacts regenerate
+```
+
+## What it shows
+
+`compile-config : val --> output` returns **either** the validation errors
+**or** the generated files — a sum type (`[invalid Errs]` / `[compiled Files]`),
+never half of each. So "was it valid?" and "what did it generate?" can't drift
+apart: an invalid config produces no manifest, by construction.
+
+The generators (`emit-k8s`, `emit-nginx`) are **typed over the config's `val`
+structure**. They read fields through typed accessors with defaults and build
+strings with `cn`/`str`. Feed a number where a string is expected and it does
+not compile — see `configc_broken.shen`, whose only sin is `(cn "listen " Port)`
+with `Port` a number. In an untyped templating engine that is a runtime crash
+(or a silently corrupt config file) on first generation; here the CLI run ends
+with:
+
+```
+rejected by the typechecker: type error in rule 1 of bad-listen
+```
+
+Everything is pure, portable Shen (`cn`/`str`/`n->string` only, no host
+bridges), so the identical compiler runs on the CLI, in this OpenResty preview,
+in a CI step, or at a Kubernetes admission webhook (via `shen-go`) — one
+definition of "valid", one definition of "what it generates", everywhere. That
+is the payoff: the config schema and the manifest templates stop being two
+artifacts that drift, and become one typed function.
+
+## Files
+
+| file | what it is |
+|---|---|
+| `configc.shen` | the compiler: the `val`/`output`/`artifact` types, the validators, the k8s + nginx generators, and `compile-config`. |
+| `configc_broken.shen` | the same shape with one planted generator type bug, to show the typechecker rejecting it at load. |
+| `configc.lua` | the CLI: marshals Lua config tables, compiles them, prints artifacts or errors, and proves the broken generator is rejected. |
+| `app.lua` | OpenResty glue: marshals a JSON config and returns generated artifacts (or errors) for the live preview. |
+| `nginx.conf` | serves the `/api/compile` endpoint and the preview page. |
+| `public/index.html` | edit a config, see the generated manifests update live. |
+| `json_shim.lua` | a tiny JSON codec for running off-nginx. |
diff --git a/examples/configc/app.lua b/examples/configc/app.lua
new file mode 100644
index 0000000..315bdd0
--- /dev/null
+++ b/examples/configc/app.lua
@@ -0,0 +1,96 @@
+-- examples/configc/app.lua — the config compiler behind an OpenResty endpoint.
+--
+-- POST a JSON config to /api/compile; it is marshaled into Shen and run through
+-- compile-config (validate; then, if valid, EMIT the artifacts) from
+-- configc.shen, loaded under (tc +). The browser preview calls this to show
+-- the generated Kubernetes/nginx artifacts — or the validation errors — live.
+-- The exact same compiler would run as a CI step or an admission webhook.
+--
+-- Kernel boot + typed load happen ONCE per worker (see nginx.conf).
+
+local APP_DIR = debug.getinfo(1, "S").source:match("^@(.*)[/\\][^/\\]+$") or "."
+
+local shen = require("shen")
+local IO   = require("lua_interop")
+local P    = shen.prims
+
+local cjson
+do
+  local ok, m = pcall(require, "cjson.safe")
+  if not ok then ok, m = pcall(require, "cjson") end
+  cjson = ok and m or assert(loadfile(APP_DIR .. "/json_shim.lua"))()
+end
+
+shen.boot{quiet = true}
+shen.eval("(tc +)")
+P.F["load"](APP_DIR .. "/configc.shen")
+shen.eval("(tc -)")
+
+local compile = IO.fn("compile-config")
+local sym = IO.sym
+
+-- ---- Lua (cjson) value -> Shen `val` ---------------------------------------
+local function to_val(v)
+  local t = type(v)
+  if t == "string"  then return { sym("s"), v } end
+  if t == "number"  then return { sym("n"), v } end
+  if t == "boolean" then return { sym("b"), v } end
+  if t == "table" then
+    if v[1] ~= nil then                       -- has index 1 => a JSON array
+      local a = {}; for i, e in ipairs(v) do a[i] = to_val(e) end
+      return { sym("arr"), a }
+    end
+    -- an empty table is treated as an empty OBJECT here (a config is an object
+    -- at every level), so POST {} yields field errors, not "must be an object".
+    local es, i = {}, 0
+    for k, val in pairs(v) do
+      if type(k) == "string" then i = i + 1; es[i] = { k, to_val(val) } end
+    end
+    return { sym("obj"), es }
+  end
+  return { sym("s"), tostring(v) }
+end
+
+-- ---- compile a decoded config -> a JSON-friendly result --------------------
+-- Shen returns {"compiled", {{"file",name,body}...}} or {"invalid", {errs}}.
+local function compile_config(decoded)
+  local out = compile(to_val(decoded or {}))
+  if out[1] == "compiled" then
+    local files = {}
+    for i, f in ipairs(out[2]) do files[i] = { name = f[2], body = f[3] } end
+    return { ok = true, files = files }
+  end
+  return { ok = false, errors = out[2] }
+end
+
+local function dispatch(method, path, body)
+  if path == "/api/compile" and method == "POST" then
+    return 200, compile_config(body)
+  end
+  return 404, { error = "not found" }
+end
+
+local M = { dispatch = dispatch, compile_config = compile_config, json = cjson }
+
+function M.handle()
+  local method = ngx.req.get_method()
+  local decoded
+  if method == "POST" then
+    ngx.req.read_body()
+    local raw = ngx.req.get_body_data()
+    if raw and raw ~= "" then
+      local d, err = cjson.decode(raw)
+      if d == nil then
+        ngx.status = 400; ngx.header.content_type = "application/json"
+        ngx.say(cjson.encode({ error = "invalid JSON: " .. tostring(err) })); return
+      end
+      decoded = d
+    end
+  end
+  local status, body = dispatch(method, ngx.var.uri, decoded)
+  ngx.status = status
+  ngx.header.content_type = "application/json"
+  ngx.say(cjson.encode(body))
+end
+
+return M
diff --git a/examples/configc/configc.lua b/examples/configc/configc.lua
new file mode 100644
index 0000000..b0ad9a6
--- /dev/null
+++ b/examples/configc/configc.lua
@@ -0,0 +1,84 @@
+-- examples/configc/configc.lua — the typed config compiler as a CLI.
+--
+--   luajit examples/configc/configc.lua          (from the repo root)
+--
+-- Marshals Lua config tables into Shen, compiles each with compile-config
+-- (validate; then, only if valid, EMIT a Kubernetes Deployment + an nginx
+-- server block), and prints the artifacts or the errors. Finally it loads
+-- configc_broken.shen — a generator with one type bug — to show the
+-- typechecker rejecting a bad generator at load, before any config compiles.
+
+local root = arg[0]:match("^(.*)/examples/configc/[^/]+$") or "."
+package.path = root .. "/?.lua;" .. package.path
+require("ffi").cdef[[int chdir(const char *);]]
+require("ffi").C.chdir(root)
+
+local P = require("boot")
+P.load_kernel(false)
+P.initialise()
+local shen = require("lua_interop")   -- the MARSHALING API (Lua table <-> Shen)
+
+-- ---- marshal a nested Lua table into the `val` shape (as config_check.lua) --
+local sym = shen.sym
+local function val(v)
+  local t = type(v)
+  if t == "string"  then return { sym("s"), v } end
+  if t == "number"  then return { sym("n"), v } end
+  if t == "boolean" then return { sym("b"), v } end
+  assert(t == "table", "unsupported config value: " .. t)
+  if v[1] ~= nil or next(v) == nil then
+    local a = {}; for i, e in ipairs(v) do a[i] = val(e) end
+    return { sym("arr"), a }
+  end
+  local keys = {}; for k in pairs(v) do keys[#keys + 1] = k end
+  table.sort(keys)
+  local es = {}; for i, k in ipairs(keys) do es[i] = { k, val(v[k]) } end
+  return { sym("obj"), es }
+end
+
+-- ---- load (and TYPECHECK) the compiler --------------------------------------
+print("== loading examples/configc/configc.shen under (tc +) ==")
+shen.eval("(tc +)")
+P.F["load"]("examples/configc/configc.shen")
+shen.eval("(tc -)")
+
+local compile = shen.fn("compile-config")
+local fail = 0
+
+local function show(name, config)
+  print("\n== compile " .. name .. " ==")
+  local out = compile(val(config))          -- {"compiled", files} | {"invalid", errs}
+  if out[1] == "compiled" then
+    for _, f in ipairs(out[2]) do            -- f = {"file", name, body}
+      print(("--- %s ---"):format(f[2]))
+      print(f[3])
+    end
+  else
+    print("INVALID:")
+    for _, e in ipairs(out[2]) do print("  - " .. e) end
+  end
+  return out[1]
+end
+
+if show("good", {
+  service = "web", port = 8080, replicas = 3,
+  hosts = { "a.example.com", "b.example.com" },
+}) ~= "compiled" then fail = fail + 1; print("  FAIL: expected compiled") end
+
+if show("bad", { service = "", port = 70000 }) ~= "invalid" then
+  fail = fail + 1; print("  FAIL: expected invalid")
+end
+
+-- ---- the typechecker earning its keep on a GENERATOR bug --------------------
+print("\n== loading examples/configc/configc_broken.shen (one generator bug) ==")
+shen.eval("(tc +)")
+local ok, err = pcall(P.F["load"], "examples/configc/configc_broken.shen")
+shen.eval("(tc -)")
+if ok then
+  print("  FAIL: broken generator loaded (expected a type error)"); fail = fail + 1
+else
+  print("  rejected by the typechecker: " .. shen.error_message(err))
+end
+
+if fail == 0 then print("\nOK — all checks passed")
+else print(("\n%d check(s) FAILED"):format(fail)); os.exit(1) end
diff --git a/examples/configc/configc.shen b/examples/configc/configc.shen
new file mode 100644
index 0000000..55cc8e0
--- /dev/null
+++ b/examples/configc/configc.shen
@@ -0,0 +1,195 @@
+\\ configc.shen — a typed configuration COMPILER.
+\\
+\\ examples/config_rules.shen validates a config. This goes one step further:
+\\ it validates AND, only if valid, EMITS deployment artifacts (a Kubernetes
+\\ Deployment and an nginx server block) from the one config. The emit
+\\ functions are typed over the `val` structure, so they cannot run on a config
+\\ that hasn't typechecked, and `compile` returns EITHER the errors OR the
+\\ generated files — never half of each.
+\\
+\\ Pure, portable Shen (cn/str/n->string only): the same source compiles configs
+\\ on a CLI (luajit), at an admission webhook, or in a browser preview — one
+\\ definition of "valid", one definition of "what it generates", everywhere.
+\\ Loaded under (tc +): a bug in a generator (e.g. feeding a number where a
+\\ string is required) is a type error at load, before any config is compiled.
+
+\\ -- the value space of a config (same tagged shape as the other examples) ---
+(datatype val
+  X : string;
+  ============
+  [s X] : val;
+
+  X : number;
+  ============
+  [n X] : val;
+
+  X : boolean;
+  ============
+  [b X] : val;
+
+  Es : (list entry);
+  ==================
+  [obj Es] : val;
+
+  Vs : (list val);
+  ================
+  [arr Vs] : val;)
+
+(datatype entry
+  K : string; V : val;
+  ====================
+  [K V] : entry;)
+
+\\ a compile result: either the validation errors, or the generated files
+(datatype artifact
+  Name : string; Body : string;
+  =============================
+  [file Name Body] : artifact;)
+
+(datatype output
+  Errs : (list string);
+  =====================
+  [invalid Errs] : output;
+
+  Files : (list artifact);
+  ========================
+  [compiled Files] : output;)
+
+\\ -- generic helpers ---------------------------------------------------------
+(define find-val
+  {string --> (list entry) --> (list val)}
+  _ [] -> []
+  K [[K V] | _] -> [V]
+  K [_ | Es] -> (find-val K Es))
+
+(define lines
+  {(list string) --> string}
+  [] -> ""
+  [L] -> L
+  [L | Ls] -> (cn L (cn (n->string 10) (lines Ls))))
+
+(define string-length
+  {string --> number}
+  "" -> 0
+  S -> (+ 1 (string-length (tlstr S))))
+
+\\ typed field readers with defaults (a poor man's "config with defaults")
+(define get-str
+  {string --> (list entry) --> string}
+  K Es -> (str-or "" (find-val K Es)))
+
+(define str-or
+  {string --> (list val) --> string}
+  D []      -> D
+  _ [[s S]] -> S
+  D [_]     -> D)
+
+(define get-num
+  {number --> string --> (list entry) --> number}
+  D K Es -> (num-or D (find-val K Es)))
+
+(define num-or
+  {number --> (list val) --> number}
+  D []      -> D
+  _ [[n N]] -> N
+  D [_]     -> D)
+
+(define get-arr
+  {string --> (list entry) --> (list val)}
+  K Es -> (arr-or (find-val K Es)))
+
+(define arr-or
+  {(list val) --> (list val)}
+  []         -> []
+  [[arr Vs]] -> Vs
+  [_]        -> [])
+
+\\ -- validation (pure Shen; no host bridges, so it ports everywhere) ---------
+(define validate-config
+  {val --> (list string)}
+  [obj Es] -> (append (check-service (find-val "service" Es))
+               (append (check-port (find-val "port" Es))
+                       (check-replicas (find-val "replicas" Es))))
+  _ -> ["config: must be an object"])
+
+(define check-service
+  {(list val) --> (list string)}
+  [[s S]] -> (if (> (string-length S) 0) [] ["service: must be non-empty"])
+  [_]     -> ["service: must be a string"]
+  []      -> ["service: required"])
+
+(define check-port
+  {(list val) --> (list string)}
+  [[n N]] -> (if (and (integer? N) (and (>= N 1) (<= N 65535)))
+                 []
+                 ["port: must be an integer in 1..65535"])
+  [_]     -> ["port: must be a number"]
+  []      -> ["port: required"])
+
+(define check-replicas
+  {(list val) --> (list string)}
+  [[n N]] -> (if (and (integer? N) (>= N 1)) [] ["replicas: must be a positive integer"])
+  [_]     -> ["replicas: must be a number"]
+  []      -> [])                                   \\ optional, defaults to 1
+
+\\ -- the generators (typed over `val`; only reached for a valid config) ------
+(define emit-k8s
+  {val --> artifact}
+  [obj Es] -> [file "deployment.yaml" (k8s-body (get-str "service" Es)
+                                                (get-num 1 "replicas" Es)
+                                                (get-num 80 "port" Es))]
+  _ -> [file "deployment.yaml" ""])
+
+(define k8s-body
+  {string --> number --> number --> string}
+  Service Replicas Port ->
+    (lines ["apiVersion: apps/v1"
+            "kind: Deployment"
+            "metadata:"
+            (cn "  name: " Service)
+            "spec:"
+            (cn "  replicas: " (str Replicas))
+            "  selector:"
+            (cn "    matchLabels: { app: " (cn Service " }"))
+            "  template:"
+            "    metadata:"
+            (cn "      labels: { app: " (cn Service " }"))   \\ must match the selector
+            "    spec:"
+            "      containers:"
+            (cn "        - name: " Service)
+            (cn "          ports: [{ containerPort: " (cn (str Port) " }]"))]))
+
+(define emit-nginx
+  {val --> artifact}
+  [obj Es] -> [file "server.conf" (nginx-body (get-str "service" Es)
+                                              (get-num 80 "port" Es)
+                                              (host-names (get-arr "hosts" Es)))]
+  _ -> [file "server.conf" ""])
+
+(define host-names
+  {(list val) --> string}
+  []           -> "_"
+  [[s H]]      -> H
+  [[s H] | Vs] -> (cn H (cn " " (host-names Vs)))
+  [_ | Vs]     -> (host-names Vs))
+
+(define nginx-body
+  {string --> number --> string --> string}
+  Service Port Hosts ->
+    (lines [(cn "server {  # generated for " Service)
+            (cn "    listen " (cn (str Port) ";"))
+            (cn "    server_name " (cn Hosts ";"))
+            "    location / {"
+            (cn "        proxy_pass http://" (cn Service ";"))
+            "    }"
+            "}"]))
+
+\\ -- the compiler: validate, then (only if clean) generate --------------------
+(define compile-config
+  {val --> output}
+  C -> (compile-config-checked C (validate-config C)))
+
+(define compile-config-checked
+  {val --> (list string) --> output}
+  C []   -> [compiled [(emit-k8s C) (emit-nginx C)]]
+  _ Errs -> [invalid Errs])
diff --git a/examples/configc/configc_broken.shen b/examples/configc/configc_broken.shen
new file mode 100644
index 0000000..bcf99e1
--- /dev/null
+++ b/examples/configc/configc_broken.shen
@@ -0,0 +1,45 @@
+\\ configc_broken.shen — configc with ONE planted generator bug, to show the
+\\ typechecker rejecting it at load (the tier-a guarantee). The bug: the nginx
+\\ generator feeds the numeric Port straight to `cn`, which is
+\\ {string --> string --> string}. In an untyped templating language this is a
+\\ runtime crash (or a silently wrong config file) the first time you generate;
+\\ here `load` under (tc +) refuses the file before any config is compiled.
+
+(datatype val
+  X : string;
+  ============
+  [s X] : val;
+
+  X : number;
+  ============
+  [n X] : val;
+
+  Es : (list entry);
+  ==================
+  [obj Es] : val;)
+
+(datatype entry
+  K : string; V : val;
+  ====================
+  [K V] : entry;)
+
+(define find-val
+  {string --> (list entry) --> (list val)}
+  _ [] -> []
+  K [[K V] | _] -> [V]
+  K [_ | Es] -> (find-val K Es))
+
+(define get-num
+  {number --> string --> (list entry) --> number}
+  D K Es -> (num-or D (find-val K Es)))
+
+(define num-or
+  {number --> (list val) --> number}
+  D []      -> D
+  _ [[n N]] -> N
+  D [_]     -> D)
+
+\\ THE BUG: Port is a number; cn wants a string. (str Port) is the fix.
+(define bad-listen
+  {(list entry) --> string}
+  Es -> (cn "    listen " (get-num 80 "port" Es)))
diff --git a/examples/configc/json_shim.lua b/examples/configc/json_shim.lua
new file mode 100644
index 0000000..0cd6bc6
--- /dev/null
+++ b/examples/configc/json_shim.lua
@@ -0,0 +1,148 @@
+-- examples/openresty/json_shim.lua — a minimal JSON codec.
+--
+-- Used ONLY when the real lua-cjson is unavailable (i.e. running the example
+-- off-nginx under plain luajit, e.g. selftest.lua). OpenResty bundles cjson,
+-- so under the actual server this file is never loaded. It implements just
+-- the surface app.lua uses: decode, encode, and an empty_array sentinel.
+
+local json = {}
+
+-- A unique sentinel so an empty Lua table can be encoded as [] not {}.
+json.empty_array = setmetatable({}, { __tostring = function() return "[]" end })
+
+-- ---- encode ----------------------------------------------------------------
+local escapes = { ['"'] = '\\"', ['\\'] = '\\\\', ['\n'] = '\\n',
+                  ['\r'] = '\\r', ['\t'] = '\\t' }
+local function enc_str(s)
+  return '"' .. s:gsub('[%z\1-\31"\\]', function(c)
+    return escapes[c] or ('\\u%04x'):format(c:byte())
+  end) .. '"'
+end
+
+local encode
+local function enc_table(v, out)
+  if v == json.empty_array then out[#out + 1] = "[]"; return end
+  local n = #v
+  local is_array = n > 0
+  if is_array then
+    out[#out + 1] = "["
+    for i = 1, n do
+      if i > 1 then out[#out + 1] = "," end
+      encode(v[i], out)
+    end
+    out[#out + 1] = "]"
+  else
+    -- object (or empty table -> {})
+    out[#out + 1] = "{"
+    local first = true
+    for k, val in pairs(v) do
+      if not first then out[#out + 1] = "," end
+      first = false
+      out[#out + 1] = enc_str(tostring(k)); out[#out + 1] = ":"
+      encode(val, out)
+    end
+    out[#out + 1] = "}"
+  end
+end
+
+encode = function(v, out)
+  local t = type(v)
+  if t == "string" then out[#out + 1] = enc_str(v)
+  elseif t == "number" then out[#out + 1] = tostring(v)
+  elseif t == "boolean" then out[#out + 1] = v and "true" or "false"
+  elseif t == "nil" then out[#out + 1] = "null"
+  elseif t == "table" then enc_table(v, out)
+  else error("json: cannot encode " .. t) end
+end
+
+function json.encode(v)
+  local out = {}
+  encode(v, out)
+  return table.concat(out)
+end
+
+-- ---- decode (small recursive-descent parser) -------------------------------
+local function decode_error(s, i, msg)
+  error(("json: %s at byte %d"):format(msg, i), 0)
+end
+
+local parse_value
+local function skip_ws(s, i)
+  local _, j = s:find("^[ \t\r\n]*", i)
+  return (j or i - 1) + 1
+end
+
+local function parse_string(s, i)
+  i = i + 1                                   -- skip opening quote
+  local buf = {}
+  while i <= #s do
+    local c = s:sub(i, i)
+    if c == '"' then return table.concat(buf), i + 1
+    elseif c == '\\' then
+      local e = s:sub(i + 1, i + 1)
+      local map = { ['"'] = '"', ['\\'] = '\\', ['/'] = '/', n = '\n',
+                    t = '\t', r = '\r', b = '\b', f = '\f' }
+      if map[e] then buf[#buf + 1] = map[e]; i = i + 2
+      elseif e == 'u' then
+        local hex = s:sub(i + 2, i + 5)
+        buf[#buf + 1] = string.char(tonumber(hex, 16) % 256); i = i + 6
+      else decode_error(s, i, "bad escape") end
+    else buf[#buf + 1] = c; i = i + 1 end
+  end
+  decode_error(s, i, "unterminated string")
+end
+
+local function parse_number(s, i)
+  local j = s:find("[^%d%+%-eE%.]", i) or (#s + 1)
+  local num = tonumber(s:sub(i, j - 1))
+  if not num then decode_error(s, i, "bad number") end
+  return num, j
+end
+
+parse_value = function(s, i)
+  i = skip_ws(s, i)
+  local c = s:sub(i, i)
+  if c == '"' then return parse_string(s, i)
+  elseif c == '{' then
+    local obj = {}
+    i = skip_ws(s, i + 1)
+    if s:sub(i, i) == '}' then return obj, i + 1 end
+    while true do
+      local key; key, i = parse_string(s, skip_ws(s, i))
+      i = skip_ws(s, i)
+      if s:sub(i, i) ~= ':' then decode_error(s, i, "expected ':'") end
+      local val; val, i = parse_value(s, i + 1)
+      obj[key] = val
+      i = skip_ws(s, i)
+      local d = s:sub(i, i)
+      if d == '}' then return obj, i + 1
+      elseif d == ',' then i = skip_ws(s, i + 1)
+      else decode_error(s, i, "expected ',' or '}'") end
+    end
+  elseif c == '[' then
+    local arr = {}
+    i = skip_ws(s, i + 1)
+    if s:sub(i, i) == ']' then return arr, i + 1 end
+    while true do
+      local val; val, i = parse_value(s, i)
+      arr[#arr + 1] = val
+      i = skip_ws(s, i)
+      local d = s:sub(i, i)
+      if d == ']' then return arr, i + 1
+      elseif d == ',' then i = i + 1
+      else decode_error(s, i, "expected ',' or ']'") end
+    end
+  elseif s:sub(i, i + 3) == "true"  then return true, i + 4
+  elseif s:sub(i, i + 4) == "false" then return false, i + 5
+  elseif s:sub(i, i + 3) == "null"  then return nil, i + 4
+  else return parse_number(s, i) end
+end
+
+-- cjson.safe-style: returns nil, errmsg on failure rather than throwing.
+function json.decode(s)
+  local ok, v = pcall(parse_value, s, 1)
+  if not ok then return nil, v end
+  return v
+end
+
+return json
diff --git a/examples/configc/nginx.conf b/examples/configc/nginx.conf
new file mode 100644
index 0000000..eeaabe4
--- /dev/null
+++ b/examples/configc/nginx.conf
@@ -0,0 +1,34 @@
+# examples/configc/nginx.conf — the typed config compiler as a web preview.
+#
+#     mkdir -p examples/configc/logs
+#     openresty -p "$PWD/examples/configc" -c nginx.conf
+#
+# then open http://127.0.0.1:8092/ , edit the config, and watch the generated
+# Kubernetes + nginx artifacts (or the validation errors) update live. The same
+# compile-config runs here, on the CLI (configc.lua), and would run at a CI gate.
+
+daemon off;
+worker_processes 1;
+pid logs/nginx.pid;
+error_log logs/error.log info;
+
+events { worker_connections 256; }
+
+http {
+    access_log logs/access.log;
+    types { text/html html; text/javascript js mjs; application/json json; }
+    default_type application/octet-stream;
+
+    init_by_lua_block {
+        local prefix = ngx.config.prefix()
+        package.path = prefix .. "../../?.lua;" .. prefix .. "?.lua;" .. package.path
+    }
+    init_worker_by_lua_block { require("app") }   -- boot Shen + typed load once
+
+    server {
+        listen 8092;
+        location /api/ { content_by_lua_block { require("app").handle() } }
+        location = /configc.shen { default_type text/plain; alias configc.shen; }
+        location / { root public; index index.html; }
+    }
+}
diff --git a/examples/configc/public/index.html b/examples/configc/public/index.html
new file mode 100644
index 0000000..aea1882
--- /dev/null
+++ b/examples/configc/public/index.html
@@ -0,0 +1,77 @@
+<!DOCTYPE html>
+<!--
+  examples/configc/public/index.html — live typed config compiler.
+
+  Edit the config on the left; the right shows what compile-config in
+  configc.shen (shen-lua, under OpenResty, loaded under (tc +)) generates from
+  it — a Kubernetes Deployment and an nginx server block — or the validation
+  errors. One typed source of "valid" and "what it generates", the same on the
+  CLI, here, and at a CI/admission gate.
+-->
+<html lang="en">
+<head>
+  <meta charset="utf-8">
+  <meta name="viewport" content="width=device-width, initial-scale=1">
+  <title>shen-lua · typed config compiler</title>
+  <style>
+    body { font: 15px/1.5 system-ui, sans-serif; max-width: 60rem; margin: 2rem auto; padding: 0 1rem; color: #1f2937; }
+    h1 { font-size: 1.4rem; } code { background: #f0f0f0; padding: 0 .25em; border-radius: 3px; } a { color: #2563eb; }
+    .cols { display: grid; grid-template-columns: 1fr 1fr; gap: 1rem; margin: 1.5rem 0; }
+    textarea { width: 100%; height: 18rem; font: 13px/1.5 ui-monospace, monospace; padding: .75rem; border: 1px solid #ccc; border-radius: 6px; box-sizing: border-box; }
+    .out { min-height: 18rem; }
+    pre { background: #0f172a; color: #e2e8f0; padding: .75rem 1rem; border-radius: 6px; overflow-x: auto; font-size: 12.5px; line-height: 1.5; margin: 0 0 .75rem; }
+    pre .fname { color: #93c5fd; }
+    .errors { background: #fee2e2; border: 1px solid #fca5a5; color: #991b1b; border-radius: 6px; padding: .75rem 1rem; }
+    .errors li { margin: .15rem 0; }
+    label { font-size: .8rem; color: #6b7280; }
+  </style>
+</head>
+<body>
+  <h1>Typed config compiler <small>— validate &amp; generate, in Shen</small></h1>
+  <p>Edit the config; the artifacts on the right are generated by
+     <a href="/configc.shen" target="_blank"><code>compile-config</code></a>.
+     Break it (blank <code>service</code>, <code>port</code> 70000) and it emits
+     nothing but errors — a config can't compile to a manifest unless it's valid.</p>
+
+  <div class="cols">
+    <div>
+      <label>config (JSON)</label>
+      <textarea id="cfg">{
+  "service": "web",
+  "port": 8080,
+  "replicas": 3,
+  "hosts": ["a.example.com", "b.example.com"]
+}</textarea>
+    </div>
+    <div class="out" id="out"></div>
+  </div>
+
+  <script type="module">
+    const $ = (id) => document.getElementById(id);
+    const esc = (s) => String(s).replace(/[&<>]/g, (c) => ({ "&": "&amp;", "<": "&lt;", ">": "&gt;" }[c]));
+
+    async function recompile() {
+      let cfg;
+      try { cfg = JSON.parse($("cfg").value); }
+      catch (e) { $("out").innerHTML = `<div class="errors">config is not valid JSON: ${esc(e.message)}</div>`; return; }
+      let res;
+      try {
+        res = await (await fetch("/api/compile", {
+          method: "POST", headers: { "Content-Type": "application/json" },
+          body: JSON.stringify(cfg),
+        })).json();
+      } catch (e) { $("out").innerHTML = `<div class="errors">server unreachable</div>`; return; }
+      if (res.ok) {
+        $("out").innerHTML = res.files.map((f) =>
+          `<pre><span class="fname"># ${esc(f.name)}</span>\n${esc(f.body)}</pre>`).join("");
+      } else {
+        $("out").innerHTML = `<div class="errors"><b>will not compile:</b><ul>`
+          + res.errors.map((e) => `<li>${esc(e)}</li>`).join("") + `</ul></div>`;
+      }
+    }
+
+    $("cfg").addEventListener("input", recompile);
+    recompile();
+  </script>
+</body>
+</html>
diff --git a/examples/crdt/README.md b/examples/crdt/README.md
new file mode 100644
index 0000000..1d24207
--- /dev/null
+++ b/examples/crdt/README.md
@@ -0,0 +1,94 @@
+# CRDT sync hub — convergence you can prove
+
+A conflict-free replicated data type (CRDT) lets replicas edit independently
+and merge with **no coordination**, always converging to the same state. The
+correctness rests on three algebraic laws on `merge` — commutativity,
+associativity, idempotence — which are exactly the axioms of a
+**join-semilattice**. This example puts that merge in one typed Shen file and
+shows the laws holding at three increasing levels of assurance.
+
+```
+luajit examples/crdt/selftest.lua          # convergence + laws + proofs, no deps
+```
+
+To serve the two-replica web demo under OpenResty:
+
+```
+mkdir -p examples/crdt/logs
+openresty -p "$PWD/examples/crdt" -c nginx.conf
+# open http://127.0.0.1:8090/ in two tabs, edit each, Sync — they converge
+```
+
+## The data types
+
+| CRDT | what it is | merge (the join) |
+|---|---|---|
+| **G-Counter** | grow-only counter, per-replica tallies | pointwise `max` |
+| **LWW-Register** | a value indivisible from its `(timestamp, id)` clock | greater clock wins |
+| **LWW-Map** (`doc`) | a record: field → `LWW-Register` | per-field, merged independently |
+
+The `doc` is the demoable one: two clients edit the same record offline and it
+converges field by field. The **register's value cannot exist without its
+clock** (it's one datatype), so a merge that "forgets" to compare clocks is not
+expressible — the type rules it out.
+
+## Three tiers of assurance
+
+The whole point of this example is that "frightening correctness" is not one
+thing — it's a ladder, and you pick the rung the stakes justify.
+
+**(a) Structure — free, always on.** `crdt.shen` loads under `(tc +)`. The
+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.
+
+**(c) Laws by proof — `crdt_laws.shen`.** Universally quantified, no inputs.
+The three semilattice laws are encoded as a `datatype` (an equational logic:
+`refl`/`sym`/`trans`/`cong` + the axioms), and Shen's sequent-calculus type
+checker **verifies a proof term** for each theorem — including a real two-step
+derivation of *absorption* (`(join (join a b) b) = (join a b)`: re-merging
+already-merged state is a no-op, a convergence/stability fact). A wrong proof
+is a type error that aborts the load. Run it and watch the proofs check:
+
+```
+bin/shen -e '(tc +) (load "examples/crdt/crdt_laws.shen")'
+```
+
+### Honest scope of tier (c)
+
+This is the answer to "is the sequent calculus enough to *prove* things, not
+just type them?" — **yes**: free variables in a rule are universally quantified,
+`>>` gives hypothetical reasoning, and a proof is a term whose type is the
+proposition (Curry–Howard). But be precise about what's proved:
+
+- The three laws are taken as **axioms** here — what any CRDT merge must
+  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.
+- 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
+  machine-checked derivation a theorem prover would recognize — stronger than
+  tests-on-one-host, short of a verified extraction to the running port.
+
+## Files
+
+| 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_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. |
+| `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/app.lua b/examples/crdt/app.lua
new file mode 100644
index 0000000..d48912e
--- /dev/null
+++ b/examples/crdt/app.lua
@@ -0,0 +1,130 @@
+-- examples/crdt/app.lua — the CRDT sync hub: OpenResty <-> shen-lua glue.
+--
+-- The server is just another replica. It holds one canonical document and,
+-- on every POST, MERGES the client's whole document into it with the SAME
+-- typed `doc-merge` from crdt.shen that the browser runs client-side. Because
+-- merge is a join-semilattice operation (commutative/associative/idempotent —
+-- proved in crdt_laws.shen), it does not matter what order replicas sync in or
+-- how often: everyone converges to the identical document. No locks, no
+-- last-write-stomps, no "who won" coordination.
+--
+-- Kernel boot + the typed load of crdt.shen happen ONCE per worker (see
+-- nginx.conf init_worker_by_lua), never per request.
+
+local APP_DIR = debug.getinfo(1, "S").source:match("^@(.*)[/\\][^/\\]+$") or "."
+
+local shen = require("shen")
+local IO   = require("lua_interop")
+local P    = shen.prims
+
+-- cjson under nginx; the bundled shim off-nginx (selftest under plain luajit).
+local cjson
+do
+  local ok, m = pcall(require, "cjson.safe")
+  if not ok then ok, m = pcall(require, "cjson") end
+  cjson = ok and m or assert(loadfile(APP_DIR .. "/json_shim.lua"))()
+end
+
+-- Canonical document store. Pluggable so selftest can inject an in-memory one;
+-- under nginx M.use_store wires it to a lua_shared_dict (a JSON string).
+local store = { get = function() return nil end, set = function(_) end }
+local function set_store(s) store = s end
+
+shen.boot{quiet = true}
+
+-- crdt.shen is the SAME file the browser loads (via ShenScript). Loaded under
+-- (tc +): every merge/law function is proved well-typed before the first
+-- request, and a type error aborts worker boot.
+shen.eval("(tc +)")
+P.F["load"](APP_DIR .. "/crdt.shen")
+shen.eval("(tc -)")
+
+local doc_merge = IO.fn("doc-merge")
+local sym = IO.sym
+
+-- ---- marshaling: JSON document <-> Shen `doc` ------------------------------
+-- Wire shape:  { "<field>": { "v": <string>, "ts": <number>, "id": <string> }, ... }
+-- Shen shape:  [doc [[<field> [lww V Ts Id]] ...]]
+-- A field whose value isn't a well-formed register is skipped (defensive).
+local function to_doc(obj)
+  local fields = {}
+  if type(obj) == "table" then
+    for k, r in pairs(obj) do
+      if type(k) == "string" and type(r) == "table"
+         and type(r.v) == "string" and type(r.ts) == "number" and type(r.id) == "string" then
+        fields[#fields + 1] = { k, { sym("lww"), r.v, r.ts, r.id } }
+      end
+    end
+  end
+  return { sym("doc"), fields }
+end
+
+-- Shen `doc` (marshaled back to nested Lua arrays, tags as strings) -> JSON obj.
+local function from_doc(d)
+  local out = {}
+  if type(d) == "table" and d[1] == "doc" then
+    for _, field in ipairs(d[2]) do
+      local key, reg = field[1], field[2]
+      if reg and reg[1] == "lww" then
+        out[key] = { v = reg[2], ts = reg[3], id = reg[4] }
+      end
+    end
+  end
+  return out
+end
+
+-- Read the canonical doc as a Lua/JSON value ({} if nothing stored yet).
+local function load_canonical()
+  local raw = store.get()
+  if not raw or raw == "" then return {} end
+  local d = cjson.decode(raw)
+  return d or {}
+end
+
+-- ---- request handling (pure given method/path/body; shared with selftest) --
+-- GET  /api/doc  -> the canonical merged document
+-- POST /api/doc  -> merge the client's document in, return the converged doc
+local function dispatch(method, path, decoded_body)
+  if path ~= "/api/doc" then
+    return 404, { error = "not found" }
+  end
+  if method == "GET" then
+    return 200, load_canonical()
+  end
+  if method == "POST" then
+    local incoming = to_doc(decoded_body or {})
+    local merged   = from_doc(doc_merge(to_doc(load_canonical()), incoming))
+    store.set(cjson.encode(merged))
+    return 200, merged
+  end
+  return 404, { error = "not found" }
+end
+
+local M = { dispatch = dispatch, to_doc = to_doc, from_doc = from_doc,
+            use_store = set_store, json = cjson }
+
+function M.handle()
+  local method = ngx.req.get_method()
+  local path   = ngx.var.uri
+  local decoded
+  if method == "POST" or method == "PUT" then
+    ngx.req.read_body()
+    local raw = ngx.req.get_body_data()
+    if raw and raw ~= "" then
+      local d, err = cjson.decode(raw)
+      if d == nil then
+        ngx.status = 400
+        ngx.header.content_type = "application/json"
+        ngx.say(cjson.encode({ error = "invalid JSON: " .. tostring(err) }))
+        return
+      end
+      decoded = d
+    end
+  end
+  local status, body = dispatch(method, path, decoded)
+  ngx.status = status
+  ngx.header.content_type = "application/json"
+  ngx.say(cjson.encode(body))
+end
+
+return M
diff --git a/examples/crdt/crdt.shen b/examples/crdt/crdt.shen
new file mode 100644
index 0000000..a63573b
--- /dev/null
+++ b/examples/crdt/crdt.shen
@@ -0,0 +1,230 @@
+\\ crdt.shen — conflict-free replicated data types, the SAME typed source loaded
+\\ by every replica: the server (shen-lua under OpenResty), the browser
+\\ (ShenScript), and — unchanged — shen-go / shen-rust. One merge function
+\\ everywhere, so replicas cannot disagree about what "merge" means; that
+\\ agreement is the whole correctness story of a state-based CRDT.
+\\
+\\ Pure, portable Shen: kernel primitives only (cn/str/tlstr/string->n/=), no
+\\ host bridges, exactly like examples/openresty/rules.shen. Loaded under (tc +)
+\\ so every merge/law function is proved well-typed before the first request.
+\\
+\\ A state-based CRDT is a join-semilattice: `merge` is the least-upper-bound
+\\ (join), and Strong Eventual Consistency follows from three algebraic laws on
+\\ merge — commutativity, associativity, idempotence — plus monotonic updates.
+\\ Those three laws ARE the semilattice axioms. We encode them as checkable
+\\ Shen functions (tier b: executable property checks) below; crdt_laws.shen
+\\ takes one of them to tier c (a machine-checked sequent proof).
+
+\\ ===========================================================================
+\\ Shared helpers
+\\ ===========================================================================
+
+(define max-num {number --> number --> number} A B -> (if (> A B) A B))
+
+\\ A deterministic TOTAL order on replica ids (lexicographic by codepoint).
+\\ Ties in a Last-Writer-Wins clock must break identically on every replica or
+\\ they diverge forever — so the tiebreak has to be a genuine total order, and
+\\ it has to be pure/portable. string->n gives the codepoint of the head char.
+(define str-gt?
+  {string --> string --> boolean}
+  "" _ -> false
+  _ "" -> true
+  S1 S2 -> (if (> (string->n S1) (string->n S2))
+               true
+               (if (< (string->n S1) (string->n S2))
+                   false
+                   (str-gt? (tlstr S1) (tlstr S2)))))
+
+\\ ===========================================================================
+\\ G-Counter — the "hello world" of state-based CRDTs.
+\\
+\\ State is a set of per-replica grow-only tallies [Id N]; value is their sum;
+\\ merge is the pointwise MAX. max is commutative/associative/idempotent, so
+\\ the laws hold by construction — this is the cleanest semilattice to see.
+\\ ===========================================================================
+
+(datatype gcounter
+  Id : string; N : number;
+  ========================
+  [Id N] : gtally;
+
+  Ts : (list gtally);
+  ===================
+  [gc Ts] : gcounter;)
+
+\\ this replica's effective count for Id (0 if unseen). Takes the MAX over all
+\\ matching entries, so it is correct even for a malformed counter that carries
+\\ a key more than once — which is what lets the laws below hold for EVERY typed
+\\ gcounter, not only the well-formed (one-entry-per-id) ones gc-inc produces.
+(define gc-get
+  {string --> (list gtally) --> number}
+  _ [] -> 0
+  Id [[Id N] | Ts] -> (max-num N (gc-get Id Ts))
+  Id [_ | Ts] -> (gc-get Id Ts))
+
+\\ the join: canonicalize the union of both counters to one entry per id, each
+\\ the max count seen for that id. Folding with gc-absorb dedups as it goes, so
+\\ merge is idempotent/commutative/associative even on duplicate-key inputs.
+(define gc-merge
+  {gcounter --> gcounter --> gcounter}
+  [gc As] [gc Bs] -> [gc (gc-collect Bs (gc-collect As []))])
+
+\\ insert one tally into an accumulator, keeping the max if its id is present
+(define gc-absorb
+  {gtally --> (list gtally) --> (list gtally)}
+  [Id N] [] -> [[Id N]]
+  [Id N] [[Id M] | Ts] -> [[Id (max-num N M)] | Ts]
+  T [T2 | Ts] -> [T2 | (gc-absorb T Ts)])
+
+(define gc-collect
+  {(list gtally) --> (list gtally) --> (list gtally)}
+  [] Acc -> Acc
+  [T | Ts] Acc -> (gc-collect Ts (gc-absorb T Acc)))
+
+(define gc-value
+  {gcounter --> number}
+  [gc Ts] -> (gc-sum Ts))
+
+(define gc-sum
+  {(list gtally) --> number}
+  [] -> 0
+  [[_ N] | Ts] -> (+ N (gc-sum Ts)))
+
+\\ the only update: a replica bumps its OWN tally. Monotonic (counts only go
+\\ up), which is what keeps every local update moving up the lattice.
+(define gc-inc
+  {string --> gcounter --> gcounter}
+  Id [gc Ts] -> [gc (gc-bump Id Ts)])
+
+(define gc-bump
+  {string --> (list gtally) --> (list gtally)}
+  Id [] -> [[Id 1]]
+  Id [[Id N] | Ts] -> [[Id (+ N 1)] | Ts]
+  Id [T | Ts] -> [T | (gc-bump Id Ts)])
+
+\\ The lattice partial order ⊑ : A ⊑ B iff every count in A is ≤ B's. Equality
+\\ is ⊑ both ways — order-independent, so it is the right notion for the laws.
+(define gc-leq?
+  {gcounter --> gcounter --> boolean}
+  [gc As] B -> (gc-all-leq As B))
+
+(define gc-all-leq
+  {(list gtally) --> gcounter --> boolean}
+  [] _ -> true
+  [[Id N] | Rest] B -> (and (<= N (gc-get Id (gc-tallies B)))
+                            (gc-all-leq Rest B)))
+
+(define gc-tallies
+  {gcounter --> (list gtally)}
+  [gc Ts] -> Ts)
+
+(define gc-eq?
+  {gcounter --> gcounter --> boolean}
+  A B -> (and (gc-leq? A B) (gc-leq? B A)))
+
+\\ -- the semilattice laws, as executable property checks (tier b) -----------
+(define gc-idempotent?
+  {gcounter --> boolean}
+  A -> (gc-eq? (gc-merge A A) A))
+
+(define gc-commutative?
+  {gcounter --> gcounter --> boolean}
+  A B -> (gc-eq? (gc-merge A B) (gc-merge B A)))
+
+(define gc-associative?
+  {gcounter --> gcounter --> gcounter --> boolean}
+  A B C -> (gc-eq? (gc-merge A (gc-merge B C))
+                   (gc-merge (gc-merge A B) C)))
+
+\\ ===========================================================================
+\\ LWW-Register — last-writer-wins. The value is INDIVISIBLE from its clock:
+\\ a register cannot be constructed without (timestamp, replica-id), so a merge
+\\ that "forgets" to compare clocks cannot be written — the type forbids it.
+\\ merge = pick the writer with the greater (timestamp, id); that pair is a
+\\ total order, so max over it is a genuine semilattice join.
+\\ ===========================================================================
+
+(datatype register
+  V : string; Ts : number; Id : string;
+  =====================================
+  [lww V Ts Id] : register;)
+
+\\ strict "A dominates B": later timestamp wins; ties broken by replica id, and
+\\ then by value. Breaking the final tie by value matters: two writes that
+\\ collide on the same (timestamp, id) but carry different values are malformed
+\\ (a replica never reuses a clock), yet they are still well-typed — so making
+\\ the order TOTAL over (ts, id, value) keeps merge commutative/associative for
+\\ every typed register, not just the well-formed ones.
+(define lww-after?
+  {string --> number --> string --> string --> number --> string --> boolean}
+  V1 T1 I1 V2 T2 I2 -> (if (> T1 T2)
+                           true
+                           (if (< T1 T2)
+                               false
+                               (if (str-gt? I1 I2)
+                                   true
+                                   (if (str-gt? I2 I1)
+                                       false
+                                       (str-gt? V1 V2))))))
+
+(define lww-merge
+  {register --> register --> register}
+  [lww V1 T1 I1] [lww V2 T2 I2] -> (if (lww-after? V1 T1 I1 V2 T2 I2)
+                                       [lww V1 T1 I1]
+                                       [lww V2 T2 I2]))
+
+(define lww-eq?
+  {register --> register --> boolean}
+  [lww V1 T1 I1] [lww V2 T2 I2] -> (and (= V1 V2) (and (= T1 T2) (= I1 I2))))
+
+(define lww-idempotent?
+  {register --> boolean}
+  A -> (lww-eq? (lww-merge A A) A))
+
+(define lww-commutative?
+  {register --> register --> boolean}
+  A B -> (lww-eq? (lww-merge A B) (lww-merge B A)))
+
+(define lww-associative?
+  {register --> register --> register --> boolean}
+  A B C -> (lww-eq? (lww-merge A (lww-merge B C))
+                    (lww-merge (lww-merge A B) C)))
+
+\\ ===========================================================================
+\\ LWW-Map (a document) — a map of field-name -> LWW-Register, merged
+\\ per-field. This is the demoable CRDT: two clients edit the same record
+\\ offline, each field keeps the last writer, and the documents converge.
+\\ ===========================================================================
+
+(datatype doc
+  K : string; R : register;
+  =========================
+  [K R] : field;
+
+  Fs : (list field);
+  ================
+  [doc Fs] : doc;)
+
+(define doc-get
+  {string --> (list field) --> (list register)}   \\ [] = absent, [R] = present
+  _ [] -> []
+  K [[K R] | _] -> [R]
+  K [_ | Fs] -> (doc-get K Fs))
+
+\\ per-field merge, canonicalized the same way as gc-merge: fold every field of
+\\ both documents into one accumulator, lww-merging when a key recurs. One entry
+\\ per field name in the result, whatever order (or duplicates) the inputs had.
+(define doc-merge
+  {doc --> doc --> doc}
+  [doc As] [doc Bs] -> [doc (doc-collect Bs (doc-collect As []))])
+
+(define doc-absorb
+  {field --> (list field) --> (list field)}
+  [K R] [] -> [[K R]]
+  [K R] [[K R2] | Fs] -> [[K (lww-merge R R2)] | Fs]
+  F [F2 | Fs] -> [F2 | (doc-absorb F Fs)])
+
+(define doc-collect
+  {(list field) --> (list field) --> (list field)}
+  [] Acc -> Acc
+  [F | Fs] Acc -> (doc-collect Fs (doc-absorb F Acc)))
diff --git a/examples/crdt/crdt_laws.shen b/examples/crdt/crdt_laws.shen
new file mode 100644
index 0000000..1235b07
--- /dev/null
+++ b/examples/crdt/crdt_laws.shen
@@ -0,0 +1,94 @@
+\\ crdt_laws.shen — TIER (c): machine-checked proofs in Shen's sequent calculus.
+\\
+\\ crdt.shen checks the merge laws by EXECUTION (tier b: gc-commutative? etc.
+\\ run over sample states). That tests instances. This file goes further: it
+\\ encodes equational logic as a `datatype` and has Shen's TYPE CHECKER verify
+\\ UNIVERSALLY-QUANTIFIED proofs — no inputs, all cases at once. Load it under
+\\ (tc +): if it loads, every proof below has been checked; a wrong proof is a
+\\ type error that aborts the load (see thm-bogus, commented out).
+\\
+\\ HONEST SCOPE. The three semilattice laws (comm/assoc/idem) are taken here as
+\\ AXIOMS — they are what any CRDT merge must satisfy, and what tier (b)
+\\ property-checks for the *executable* gc-merge. What the checker proves below
+\\ are universal CONSEQUENCES of those axioms (e.g. absorption: re-merging
+\\ already-merged state is a no-op — directly a convergence/stability fact).
+\\ It does NOT re-derive the axioms from gc-merge's Lua definition; closing that
+\\ model↔code gap (induction over the tally-list representation) is real proof
+\\ engineering and is deliberately out of scope. So: tier (b) certifies the
+\\ running code satisfies the laws on instances; tier (c) proves, for all
+\\ inputs, the algebra those laws generate — and proves it by a checked
+\\ derivation a theorem prover would recognize, not by testing.
+\\
+\\ This is also the answer to "is the sequent calculus enough?": yes — free
+\\ variables in a rule are universally quantified (Prolog variables), `>>`
+\\ gives hypothetical reasoning, and a proof is a term whose TYPE is the
+\\ proposition (Curry–Howard). The trade vs Coq/Agda is trust + automation +
+\\ totality, not raw expressiveness (see README).
+
+\\ -- equational logic over a binary `join`, entirely at the type level --------
+\\ A term of type (eq S T) is a PROOF that S = T. S and T are type expressions;
+\\ the variables X Y Z W are universally quantified over each rule.
+(datatype semilattice-proofs
+  \\ equality is reflexive, symmetric, transitive ...
+  ___________
+  [refl] : (eq X X);
+
+  P : (eq X Y);
+  =============
+  [sym P] : (eq Y X);
+
+  P : (eq X Y); Q : (eq Y Z);
+  ===========================
+  [trans P Q] : (eq X Z);
+
+  \\ ... and a congruence: equals rewrite under `join` on either side. The
+  \\ context (the unchanged side) lives only in the TYPE, so unification with
+  \\ the goal fixes it and the proof term stays free of value/type confusion.
+  P : (eq X Y);
+  =====================================
+  [cong-l P] : (eq (join X W) (join Y W));
+
+  P : (eq X Y);
+  =====================================
+  [cong-r P] : (eq (join W X) (join W Y));
+
+  \\ the three SEMILATTICE AXIOMS — the defining laws of any state-based CRDT
+  \\ merge (a join-semilattice). These are exactly the tier-(b) checks.
+  ___________________________________
+  [comm] : (eq (join X Y) (join Y X));
+
+  _____________________________________________________
+  [assoc] : (eq (join (join X Y) Z) (join X (join Y Z)));
+
+  ___________________________
+  [idem] : (eq (join X X) X);)
+
+\\ -- the theorems ------------------------------------------------------------
+\\ Each is a function whose RESULT TYPE is the proposition and whose body is the
+\\ proof term. `unit` is just a placeholder argument so the signature is a
+\\ well-formed arrow; the proof is the return value the checker validates.
+
+\\ idempotence (re-stated as a proof object, one step)
+(define proof-idempotent
+  { unit --> (eq (join A A) A) }
+  _ -> [idem])
+
+\\ commutativity is symmetric (derive the mirror from the axiom)
+(define proof-comm-sym
+  { unit --> (eq (join B C) (join C B)) }
+  _ -> [sym [comm]])
+
+\\ ABSORPTION — the convergence-relevant one: merging B into an already-merged
+\\ (join A B) changes nothing.  (join (join A B) B) = (join A B).
+\\   [assoc]          : (join (join A B) B) = (join A (join B B))
+\\   [cong-r [idem]]  : (join A (join B B)) = (join A B)        (rewrite (join B B)->B)
+\\   [trans ...]      : (join (join A B) B) = (join A B)
+(define proof-absorption
+  { unit --> (eq (join (join A B) B) (join A B)) }
+  _ -> [trans [assoc] [cong-r [idem]]])
+
+\\ -- a WRONG proof is a TYPE ERROR. Uncomment to watch the load abort:
+\\ [assoc] alone proves (join (join A B) B) = (join A (join B B)), NOT (join A B).
+\\ (define proof-bogus
+\\   { unit --> (eq (join (join A B) B) (join A B)) }
+\\   _ -> [assoc])
diff --git a/examples/crdt/json_shim.lua b/examples/crdt/json_shim.lua
new file mode 100644
index 0000000..0cd6bc6
--- /dev/null
+++ b/examples/crdt/json_shim.lua
@@ -0,0 +1,148 @@
+-- examples/openresty/json_shim.lua — a minimal JSON codec.
+--
+-- Used ONLY when the real lua-cjson is unavailable (i.e. running the example
+-- off-nginx under plain luajit, e.g. selftest.lua). OpenResty bundles cjson,
+-- so under the actual server this file is never loaded. It implements just
+-- the surface app.lua uses: decode, encode, and an empty_array sentinel.
+
+local json = {}
+
+-- A unique sentinel so an empty Lua table can be encoded as [] not {}.
+json.empty_array = setmetatable({}, { __tostring = function() return "[]" end })
+
+-- ---- encode ----------------------------------------------------------------
+local escapes = { ['"'] = '\\"', ['\\'] = '\\\\', ['\n'] = '\\n',
+                  ['\r'] = '\\r', ['\t'] = '\\t' }
+local function enc_str(s)
+  return '"' .. s:gsub('[%z\1-\31"\\]', function(c)
+    return escapes[c] or ('\\u%04x'):format(c:byte())
+  end) .. '"'
+end
+
+local encode
+local function enc_table(v, out)
+  if v == json.empty_array then out[#out + 1] = "[]"; return end
+  local n = #v
+  local is_array = n > 0
+  if is_array then
+    out[#out + 1] = "["
+    for i = 1, n do
+      if i > 1 then out[#out + 1] = "," end
+      encode(v[i], out)
+    end
+    out[#out + 1] = "]"
+  else
+    -- object (or empty table -> {})
+    out[#out + 1] = "{"
+    local first = true
+    for k, val in pairs(v) do
+      if not first then out[#out + 1] = "," end
+      first = false
+      out[#out + 1] = enc_str(tostring(k)); out[#out + 1] = ":"
+      encode(val, out)
+    end
+    out[#out + 1] = "}"
+  end
+end
+
+encode = function(v, out)
+  local t = type(v)
+  if t == "string" then out[#out + 1] = enc_str(v)
+  elseif t == "number" then out[#out + 1] = tostring(v)
+  elseif t == "boolean" then out[#out + 1] = v and "true" or "false"
+  elseif t == "nil" then out[#out + 1] = "null"
+  elseif t == "table" then enc_table(v, out)
+  else error("json: cannot encode " .. t) end
+end
+
+function json.encode(v)
+  local out = {}
+  encode(v, out)
+  return table.concat(out)
+end
+
+-- ---- decode (small recursive-descent parser) -------------------------------
+local function decode_error(s, i, msg)
+  error(("json: %s at byte %d"):format(msg, i), 0)
+end
+
+local parse_value
+local function skip_ws(s, i)
+  local _, j = s:find("^[ \t\r\n]*", i)
+  return (j or i - 1) + 1
+end
+
+local function parse_string(s, i)
+  i = i + 1                                   -- skip opening quote
+  local buf = {}
+  while i <= #s do
+    local c = s:sub(i, i)
+    if c == '"' then return table.concat(buf), i + 1
+    elseif c == '\\' then
+      local e = s:sub(i + 1, i + 1)
+      local map = { ['"'] = '"', ['\\'] = '\\', ['/'] = '/', n = '\n',
+                    t = '\t', r = '\r', b = '\b', f = '\f' }
+      if map[e] then buf[#buf + 1] = map[e]; i = i + 2
+      elseif e == 'u' then
+        local hex = s:sub(i + 2, i + 5)
+        buf[#buf + 1] = string.char(tonumber(hex, 16) % 256); i = i + 6
+      else decode_error(s, i, "bad escape") end
+    else buf[#buf + 1] = c; i = i + 1 end
+  end
+  decode_error(s, i, "unterminated string")
+end
+
+local function parse_number(s, i)
+  local j = s:find("[^%d%+%-eE%.]", i) or (#s + 1)
+  local num = tonumber(s:sub(i, j - 1))
+  if not num then decode_error(s, i, "bad number") end
+  return num, j
+end
+
+parse_value = function(s, i)
+  i = skip_ws(s, i)
+  local c = s:sub(i, i)
+  if c == '"' then return parse_string(s, i)
+  elseif c == '{' then
+    local obj = {}
+    i = skip_ws(s, i + 1)
+    if s:sub(i, i) == '}' then return obj, i + 1 end
+    while true do
+      local key; key, i = parse_string(s, skip_ws(s, i))
+      i = skip_ws(s, i)
+      if s:sub(i, i) ~= ':' then decode_error(s, i, "expected ':'") end
+      local val; val, i = parse_value(s, i + 1)
+      obj[key] = val
+      i = skip_ws(s, i)
+      local d = s:sub(i, i)
+      if d == '}' then return obj, i + 1
+      elseif d == ',' then i = skip_ws(s, i + 1)
+      else decode_error(s, i, "expected ',' or '}'") end
+    end
+  elseif c == '[' then
+    local arr = {}
+    i = skip_ws(s, i + 1)
+    if s:sub(i, i) == ']' then return arr, i + 1 end
+    while true do
+      local val; val, i = parse_value(s, i)
+      arr[#arr + 1] = val
+      i = skip_ws(s, i)
+      local d = s:sub(i, i)
+      if d == ']' then return arr, i + 1
+      elseif d == ',' then i = i + 1
+      else decode_error(s, i, "expected ',' or ']'") end
+    end
+  elseif s:sub(i, i + 3) == "true"  then return true, i + 4
+  elseif s:sub(i, i + 4) == "false" then return false, i + 5
+  elseif s:sub(i, i + 3) == "null"  then return nil, i + 4
+  else return parse_number(s, i) end
+end
+
+-- cjson.safe-style: returns nil, errmsg on failure rather than throwing.
+function json.decode(s)
+  local ok, v = pcall(parse_value, s, 1)
+  if not ok then return nil, v end
+  return v
+end
+
+return json
diff --git a/examples/crdt/nginx.conf b/examples/crdt/nginx.conf
new file mode 100644
index 0000000..26ce622
--- /dev/null
+++ b/examples/crdt/nginx.conf
@@ -0,0 +1,68 @@
+# examples/crdt/nginx.conf — the CRDT sync hub under OpenResty.
+#
+#     mkdir -p examples/crdt/logs
+#     openresty -p "$PWD/examples/crdt" -c nginx.conf
+#
+# then open http://127.0.0.1:8090/ in TWO browser tabs, edit each offline, and
+# Sync — they converge. The server merges every POST into one canonical
+# document with the typed `doc-merge` from crdt.shen (loaded under (tc +)).
+
+daemon off;
+worker_processes 1;
+pid logs/nginx.pid;
+error_log logs/error.log info;
+
+events { worker_connections 256; }
+
+http {
+    access_log logs/access.log;
+
+    types {
+        text/html        html htm;
+        text/css         css;
+        text/javascript  js mjs;
+        application/json json;
+    }
+    default_type application/octet-stream;
+
+    # The canonical document lives in a shared dict so it survives across
+    # requests (and across workers, were there more than one).
+    lua_shared_dict crdt 1m;
+
+    init_by_lua_block {
+        local prefix = ngx.config.prefix()
+        package.path = prefix .. "../../?.lua;" .. prefix .. "?.lua;" .. package.path
+    }
+
+    # Boot Shen ONCE per worker (kernel + typed load of crdt.shen), then wire
+    # the canonical-document store to the shared dict.
+    init_worker_by_lua_block {
+        local app  = require("app")
+        local dict = ngx.shared.crdt
+        app.use_store({
+            get = function() return dict:get("doc") end,
+            set = function(json) dict:set("doc", json) end,
+        })
+    }
+
+    server {
+        listen 8090;
+
+        # The sync API: GET the canonical doc, POST a replica's doc to merge.
+        location /api/ {
+            content_by_lua_block { require("app").handle() }
+        }
+
+        # Serve the shared kernel itself, so the page can show the exact merge
+        # source the server typechecked at boot (one source of truth).
+        location = /crdt.shen {
+            default_type text/plain;
+            alias crdt.shen;
+        }
+
+        location / {
+            root  public;
+            index index.html;
+        }
+    }
+}
diff --git a/examples/crdt/public/index.html b/examples/crdt/public/index.html
new file mode 100644
index 0000000..cf184f7
--- /dev/null
+++ b/examples/crdt/public/index.html
@@ -0,0 +1,192 @@
+<!DOCTYPE html>
+<!--
+  examples/crdt/public/index.html — a two-replica CRDT convergence demo.
+
+  Two panels are two replicas of one shared document. Edit them in EITHER
+  order, with the network "offline", then Sync: the server merges each POST
+  into one canonical document with the typed `doc-merge` from crdt.shen — the
+  same join-semilattice merge proved commutative/associative/idempotent in
+  crdt_laws.shen — so the replicas always converge, whatever the sync order.
+
+  The merge that decides the outcome runs in Shen (shen-lua, under OpenResty).
+  Running that SAME crdt.shen in the browser via ShenScript — as
+  examples/openresty/ does for its rules — is the documented next step; here
+  the browser is a thin replica and the server is the authoritative one.
+-->
+<html lang="en">
+<head>
+  <meta charset="utf-8">
+  <meta name="viewport" content="width=device-width, initial-scale=1">
+  <title>shen-lua · CRDT sync hub</title>
+  <style>
+    body { font: 16px/1.5 system-ui, sans-serif; max-width: 52rem; margin: 2.5rem auto; padding: 0 1rem; color: #1f2937; }
+    h1 { font-size: 1.4rem; }
+    a { color: #2563eb; } code { background: #f0f0f0; padding: 0 .25em; border-radius: 3px; }
+    .replicas { display: grid; grid-template-columns: 1fr 1fr; gap: 1rem; margin: 1.5rem 0; }
+    .replica { border: 1px solid #e5e7eb; border-radius: 8px; padding: 1rem; }
+    .replica h2 { font-size: 1rem; margin: 0 0 .5rem; display: flex; justify-content: space-between; }
+    .clock { font: .8rem ui-monospace, monospace; color: #6b7280; }
+    label { display: block; font-size: .8rem; color: #6b7280; margin-top: .5rem; }
+    input { font: inherit; padding: .4rem; border: 1px solid #ccc; border-radius: 4px; width: 100%; box-sizing: border-box; }
+    .row { display: flex; gap: .5rem; margin-top: .75rem; align-items: center; }
+    button { font: inherit; padding: .4rem .8rem; border: 0; border-radius: 4px; background: #2563eb; color: #fff; cursor: pointer; }
+    button.ghost { background: #e5e7eb; color: #1f2937; }
+    .canonical { background: #0f172a; color: #e2e8f0; border-radius: 8px; padding: 1rem; margin: 1rem 0; }
+    .canonical h2 { font-size: 1rem; margin: 0 0 .5rem; color: #93c5fd; }
+    table { width: 100%; border-collapse: collapse; font-size: .85rem; }
+    td, th { text-align: left; padding: .25rem .5rem; border-bottom: 1px solid #1e293b; }
+    .arch { background: #f8fafc; border: 1px solid #e5e7eb; border-radius: 8px; padding: 1rem 1.25rem; margin: 1.5rem 0; }
+    .arch h2 { font-size: 1rem; } .arch li { padding: .15rem 0; }
+    .win { color: #34d399; }
+  </style>
+</head>
+<body>
+  <h1>CRDT sync hub <small>— two replicas, one converged document</small></h1>
+  <p>Each panel is a replica of a shared record. Edit them <b>independently</b>
+     (pretend the network is down), then <b>Sync</b> each one. However you
+     interleave the syncs, both replicas converge to the same document —
+     because the server merges with <a href="/crdt.shen" target="_blank"><code>doc-merge</code></a>,
+     a join-semilattice merge whose convergence laws are
+     <a href="#how">proved, not hoped for ↓</a>. Per field, the write with the
+     greater <code>(timestamp, replica-id)</code> wins.</p>
+
+  <div class="replicas">
+    <div class="replica" id="rep-A">
+      <h2>Replica A <span class="clock" id="clock-A">clock 0</span></h2>
+      <label>name</label>      <input data-f="name">
+      <label>role</label>      <input data-f="role">
+      <label>team</label>      <input data-f="team">
+      <div class="row"><button data-sync="A">Sync A → hub</button>
+                       <button class="ghost" data-pull="A">Pull</button></div>
+    </div>
+    <div class="replica" id="rep-B">
+      <h2>Replica B <span class="clock" id="clock-B">clock 0</span></h2>
+      <label>name</label>      <input data-f="name">
+      <label>role</label>      <input data-f="role">
+      <label>team</label>      <input data-f="team">
+      <div class="row"><button data-sync="B">Sync B → hub</button>
+                       <button class="ghost" data-pull="B">Pull</button></div>
+    </div>
+  </div>
+
+  <div class="canonical">
+    <h2>canonical document (on the server)</h2>
+    <table id="canon"><tbody><tr><td>(empty)</td></tr></tbody></table>
+  </div>
+
+  <section class="arch" id="how">
+    <h2>What this demonstrates</h2>
+    <ul>
+      <li><b>One typed merge, shared.</b> The server merges every replica's
+          document with <code>doc-merge</code> from
+          <a href="/crdt.shen" target="_blank"><code>crdt.shen</code></a>,
+          loaded under <code>(tc +)</code> — proved well-typed before the first
+          request. The browser runs the identical source nowhere yet; pointing
+          ShenScript at the same file (as the OpenResty guestbook example does)
+          makes the client merge too, with zero drift.</li>
+      <li><b>Convergence is proved, not tested.</b> A state-based CRDT converges
+          iff its merge is a join-semilattice — commutative, associative,
+          idempotent. <code>crdt_laws.shen</code> has Shen's sequent-calculus
+          type checker verify those laws (and a consequence, absorption)
+          <i>universally</i>; <code>crdt.shen</code> also checks them by
+          execution. Order of syncs cannot change the result.</li>
+      <li><b>No coordination.</b> No locks, no "who wins" round-trip — each
+          field keeps the write with the greater <code>(timestamp, id)</code>,
+          and that tiebreak is a total order in pure portable Shen, identical
+          on every port.</li>
+    </ul>
+  </section>
+
+  <script type="module">
+    const $$ = (s, r = document) => r.querySelector(s);
+    const $$$ = (s, r = document) => [...r.querySelectorAll(s)];
+
+    // Each replica keeps a local document {field: {v, ts, id}} and a Lamport
+    // clock. Editing a field stamps it with ++clock and the replica id.
+    const replicas = {
+      A: { id: "A", clock: 0, doc: {} },
+      B: { id: "B", clock: 0, doc: {} },
+    };
+
+    function renderReplica(which) {
+      const r = replicas[which];
+      $$(`#clock-${which}`).textContent = `clock ${r.clock}`;
+      $$$(`#rep-${which} input`).forEach((inp) => {
+        const reg = r.doc[inp.dataset.f];
+        // only overwrite the box when not focused, so typing isn't clobbered
+        if (document.activeElement !== inp) inp.value = reg ? reg.v : "";
+      });
+    }
+
+    function renderCanon(doc) {
+      const keys = Object.keys(doc).sort();
+      $$("#canon").innerHTML =
+        "<tbody>" + (keys.length
+          ? keys.map((k) => {
+              const r = doc[k];
+              // escape EVERY interpolated field: keys and ids arrive from POSTs
+              // with arbitrary content, so unescaped they are stored XSS.
+              return `<tr><th>${escapeHtml(k)}</th><td class="win">${escapeHtml(r.v)}</td>`
+                   + `<td>ts ${Number(r.ts)}</td><td>by ${escapeHtml(r.id)}</td></tr>`;
+            }).join("")
+          : "<tr><td>(empty)</td></tr>") + "</tbody>";
+    }
+
+    function escapeHtml(s) {
+      return String(s).replace(/[&<>"]/g, (c) =>
+        ({ "&": "&amp;", "<": "&lt;", ">": "&gt;", '"': "&quot;" }[c]));
+    }
+
+    // local edit: stamp the field with the next logical time
+    $$$(".replica input").forEach((inp) => {
+      inp.addEventListener("change", () => {
+        const which = inp.closest(".replica").id.slice(-1);
+        const r = replicas[which];
+        r.clock += 1;
+        r.doc[inp.dataset.f] = { v: inp.value, ts: r.clock, id: r.id };
+        renderReplica(which);
+      });
+    });
+
+    async function getCanon() {
+      const res = await fetch("/api/doc");
+      return res.ok ? res.json() : {};
+    }
+
+    // sync = POST our whole doc; the server merges and returns the converged
+    // doc. Adopt it locally and advance our clock past everything we've seen
+    // (standard Lamport merge), so future edits beat what we just pulled.
+    async function sync(which) {
+      const r = replicas[which];
+      const res = await fetch("/api/doc", {
+        method: "POST",
+        headers: { "Content-Type": "application/json" },
+        body: JSON.stringify(r.doc),
+      });
+      const merged = await res.json();
+      adopt(which, merged);
+      renderCanon(merged);
+    }
+
+    async function pull(which) {
+      const merged = await getCanon();
+      adopt(which, merged);
+      renderCanon(merged);
+    }
+
+    function adopt(which, merged) {
+      const r = replicas[which];
+      r.doc = merged;
+      for (const k of Object.keys(merged)) r.clock = Math.max(r.clock, merged[k].ts);
+      renderReplica(which);
+    }
+
+    $$$("[data-sync]").forEach((b) => b.addEventListener("click", () => sync(b.dataset.sync)));
+    $$$("[data-pull]").forEach((b) => b.addEventListener("click", () => pull(b.dataset.pull)));
+
+    // initial paint
+    renderReplica("A"); renderReplica("B");
+    getCanon().then(renderCanon);
+  </script>
+</body>
+</html>
diff --git a/examples/crdt/selftest.lua b/examples/crdt/selftest.lua
new file mode 100644
index 0000000..0aee496
--- /dev/null
+++ b/examples/crdt/selftest.lua
@@ -0,0 +1,122 @@
+-- examples/crdt/selftest.lua — verify the CRDT demo off-nginx.
+--
+--   luajit examples/crdt/selftest.lua      (from the repo root)
+--
+-- Three checks, no nginx, no network:
+--   1. CONVERGENCE — three replicas edit the shared document offline, then
+--      sync through the hub in DIFFERENT orders; all land on the identical doc.
+--   2. LAWS (tier b) — the executable semilattice law checks from crdt.shen
+--      (gc-commutative? / gc-associative? / gc-idempotent?) over sample state.
+--   3. PROOFS (tier c) — load crdt_laws.shen under (tc +); if the universally
+--      quantified merge proofs did not check, the load would abort here.
+
+local root = arg[0]:match("^(.*)/examples/crdt/[^/]+$") or "."
+package.path = root .. "/?.lua;" .. root .. "/examples/crdt/?.lua;" .. package.path
+
+local app   = require("app")
+local cjson = app.json
+local shen  = require("shen")
+
+local fail = 0
+local function ok(cond, label)
+  io.write(("  %-44s %s\n"):format(label, cond and "ok" or "FAIL"))
+  if not cond then fail = fail + 1 end
+end
+
+-- A fresh in-memory hub (one canonical JSON document) per scenario.
+local function new_hub()
+  local cell = { json = nil }
+  app.use_store({ get = function() return cell.json end,
+                  set = function(s) cell.json = s end })
+  return cell
+end
+
+-- A replica's local edit of one field: value wins by (timestamp, replica-id).
+local function reg(v, ts, id) return { v = v, ts = ts, id = id } end
+
+-- ===========================================================================
+print("== 1. convergence: concurrent offline edits, synced in any order ==")
+
+-- Replica A, B, C each edited the doc while offline (note the clocks):
+local A = { name = reg("ada",   3, "A"), role = reg("admin", 1, "A") }
+local B = { name = reg("grace", 5, "B"), team = reg("core",  2, "B") }
+local C = { role = reg("owner", 4, "C"), team = reg("infra", 6, "C") }
+
+-- Sync them through the hub in two DIFFERENT orders; compare final docs.
+local function sync_all(order)
+  new_hub()
+  local last
+  for _, rep in ipairs(order) do
+    local _, body = app.dispatch("POST", "/api/doc", rep)
+    last = body
+  end
+  return last
+end
+
+-- canonical JSON (sorted keys) so two docs compare by value, not table order
+local function canon(doc)
+  local keys = {}
+  for k in pairs(doc) do keys[#keys + 1] = k end
+  table.sort(keys)
+  local parts = {}
+  for _, k in ipairs(keys) do
+    local r = doc[k]
+    parts[#parts + 1] = ("%s=%s@%d/%s"):format(k, r.v, r.ts, r.id)
+  end
+  return table.concat(parts, "  ")
+end
+
+local abc = sync_all({ A, B, C })
+local cba = sync_all({ C, B, A })
+local bca = sync_all({ B, C, A })
+
+print("  A⊔B⊔C : " .. canon(abc))
+print("  C⊔B⊔A : " .. canon(cba))
+print("  B⊔C⊔A : " .. canon(bca))
+ok(canon(abc) == canon(cba), "order A,B,C  ==  order C,B,A")
+ok(canon(abc) == canon(bca), "order A,B,C  ==  order B,C,A")
+-- expected winners: name=grace@5/B, role=owner@4/C, team=infra@6/C
+ok(abc.name.v == "grace" and abc.role.v == "owner" and abc.team.v == "infra",
+   "last-writer-wins picked the right value per field")
+
+-- idempotent: re-syncing an already-merged doc changes nothing
+local once = sync_all({ A, B, C })
+local _, twice = app.dispatch("POST", "/api/doc", once)
+ok(canon(once) == canon(twice), "re-syncing a merged doc is a no-op (idempotent)")
+
+-- ===========================================================================
+print("\n== 2. semilattice laws, checked by execution (tier b) ==")
+-- Build G-Counters in Shen and run the law predicates from crdt.shen.
+shen.eval([==[ (define gA -> (gc-inc "a" (gc-inc "a" [gc []])))
+               (define gB -> (gc-inc "b" [gc []]))
+               (define gC -> (gc-inc "c" (gc-inc "a" [gc []]))) ]==])
+ok(shen.call("gc-idempotent?", shen.call("gA")) == true,  "gc-idempotent?  (merge x x = x)")
+ok(shen.call("gc-commutative?", shen.call("gA"), shen.call("gB")) == true,
+   "gc-commutative? (merge a b = merge b a)")
+ok(shen.call("gc-associative?", shen.call("gA"), shen.call("gB"), shen.call("gC")) == true,
+   "gc-associative? (merge a (merge b c) = merge (merge a b) c)")
+
+-- adversarial: the laws must hold for EVERY typed value, not just well-formed
+-- ones. These are the exact counterexamples a review found before the merge
+-- was made dedup-canonicalizing / the LWW order made total over the value.
+shen.eval([==[ (define gDup -> [gc [["a" 1] ["a" 3]]])   \\ malformed: duplicate key
+               (define gOne -> [gc [["a" 2]]])
+               (define rX -> [lww "x" 1 "A"])            \\ same (ts,id), differ in value
+               (define rY -> [lww "y" 1 "A"]) ]==])
+ok(shen.call("gc-commutative?", shen.call("gDup"), shen.call("gOne")) == true,
+   "gc-commutative? on a duplicate-key counter")
+ok(shen.call("gc-idempotent?", shen.call("gDup")) == true,
+   "gc-idempotent? on a duplicate-key counter")
+ok(shen.call("lww-commutative?", shen.call("rX"), shen.call("rY")) == true,
+   "lww-commutative? on same (ts,id), different value")
+
+-- ===========================================================================
+print("\n== 3. universally-quantified proofs, checked by the type system (tier c) ==")
+shen.eval("(tc +)")
+local loaded = pcall(shen.prims.F["load"], root .. "/examples/crdt/crdt_laws.shen")
+shen.eval("(tc -)")
+ok(loaded, "crdt_laws.shen loads => idem/comm-sym/absorption proofs all check")
+
+-- ---------------------------------------------------------------------------
+if fail == 0 then print("\nOK — all checks passed")
+else print(("\n%d check(s) FAILED"):format(fail)); os.exit(1) end
diff --git a/examples/policy/README.md b/examples/policy/README.md
new file mode 100644
index 0000000..31d0717
--- /dev/null
+++ b/examples/policy/README.md
@@ -0,0 +1,70 @@
+# Authorization gateway — one typed rule set, enforced and proved
+
+Authorization is the textbook drift bug: the edge, the service, and the admin
+UI each re-implement "who may do what", and they disagree. Here it is **one
+typed Shen file**, loaded under `(tc +)`, that runs as the edge enforcement
+gate *and* drives a live preview UI — and whose model has a second life as a
+logic where **a permission is a proof term**.
+
+```
+luajit examples/policy/selftest.lua        # decisions + permission proofs, no deps
+```
+
+Serve the gateway + explorer under OpenResty:
+
+```
+mkdir -p examples/policy/logs
+openresty -p "$PWD/examples/policy" -c nginx.conf
+# open http://127.0.0.1:8091/  — set subject/action/resource, watch the verdict
+```
+
+The same `decide()` guards `/protected/` as an `access_by_lua` gate:
+
+```
+# allowed (admin in tenant t1):
+curl -i -H 'X-Subject: boss' -H 'X-Role: admin' -H 'X-Tenant: t1' \
+     -H 'X-Res-Owner: ada' -H 'X-Res-Tenant: t1' localhost:8091/protected/
+# denied (cross-tenant) — 403 with the reason:
+curl -i -H 'X-Subject: boss' -H 'X-Role: admin' -H 'X-Tenant: t2' \
+     -H 'X-Res-Owner: ada' -H 'X-Res-Tenant: t1' localhost:8091/protected/
+```
+
+## The two halves
+
+**`policy.shen` — the decision engine (what the edge runs).** Typed datatypes
+for `principal`, `resource`, and `decision`; a total `decide` function that
+returns allow/deny **with the reason**. Tenant isolation is checked first and
+is absolute — no role, not even admin, crosses a tenant boundary. Because the
+type checker proves `decide` covers every case, "what about this combination?"
+has an answer at compile time, not in an incident.
+
+**`policy_proof.shen` — authorization as type inhabitation (the idea with
+teeth).** The same model as a logic: a term of type `(may S A R)` is a *proof*
+that subject `S` may take action `A` on resource `R`. Grant rules are inference
+rules; ownership/role/tenancy facts are axioms. Then:
+
+- a request is **authorized exactly when `(may S A R)` is inhabited**, and the
+  inhabiting term is the justification — a checkable audit trail of *why*;
+- a **denied** request is an **uninhabited type** — no rule builds the term, so
+  it cannot typecheck. "Deny by default" is not a line you can forget to write;
+  it is the absence of a proof. (`perm-bob-delete`, commented out, is a type
+  error if you uncomment it.)
+
+This is the same sequent-calculus mechanism the CRDT example uses for its merge
+laws (see `examples/crdt/`), pointed at access control. The honest scope is the
+same too: the proof certifies the request against the *encoded* rules and facts;
+trusting it means trusting that encoding (you author the rules, there are no
+tactics, totality isn't enforced). It is stronger than a runtime `if`, short of
+a Coq-extracted gate.
+
+## Files
+
+| file | what it is |
+|---|---|
+| `policy.shen` | the typed decision engine: `principal`/`resource`/`decision`, `decide`, `allowed?`, `why`. Portable — the edge and a ShenScript preview run the same source. |
+| `policy_proof.shen` | authorization as type inhabitation: grant rules, facts, and permissions as checked proof terms. |
+| `app.lua` | OpenResty glue: the `/api/check` preview endpoint and the `/protected/` `access_by_lua` enforcement gate, both calling `decide`. |
+| `nginx.conf` | wires the API, the gate, and the explorer page; boots Shen once per worker. |
+| `selftest.lua` | drives `decide` over a request table and loads the permission proofs — no nginx, no network. |
+| `public/index.html` | the live explorer: pick a triple, see the verdict and reason. |
+| `json_shim.lua` | a tiny JSON codec for running off-nginx. |
diff --git a/examples/policy/app.lua b/examples/policy/app.lua
new file mode 100644
index 0000000..54ebab6
--- /dev/null
+++ b/examples/policy/app.lua
@@ -0,0 +1,96 @@
+-- examples/policy/app.lua — a typed authorization gateway on OpenResty.
+--
+-- One decision function (policy.shen, loaded under (tc +)) serves two roles:
+--   * an ENFORCEMENT gate (access_by_lua) on /protected/ — every request is
+--     marshaled into Shen, `decide`d, and allowed (200) or refused (403 with
+--     the reason) before it reaches anything behind the gate;
+--   * a PREVIEW endpoint (/api/check) the browser page calls to show, live,
+--     why any (subject, action, resource) triple is allowed or denied.
+-- Same rules, same reasons, edge and UI — no drift.
+--
+-- Kernel boot + the typed load happen ONCE per worker (see nginx.conf).
+
+local APP_DIR = debug.getinfo(1, "S").source:match("^@(.*)[/\\][^/\\]+$") or "."
+
+local shen = require("shen")
+local IO   = require("lua_interop")
+local P    = shen.prims
+
+local cjson
+do
+  local ok, m = pcall(require, "cjson.safe")
+  if not ok then ok, m = pcall(require, "cjson") end
+  cjson = ok and m or assert(loadfile(APP_DIR .. "/json_shim.lua"))()
+end
+
+shen.boot{quiet = true}
+shen.eval("(tc +)")
+P.F["load"](APP_DIR .. "/policy.shen")
+shen.eval("(tc -)")
+
+local decide = IO.fn("decide")
+local sym    = IO.sym
+
+-- ---- decide a request -------------------------------------------------------
+-- principal = {name, role, tenant}; resource = {owner, tenant}; action string.
+-- Returns allowed(bool), reason(string). The Shen `decision` comes back as
+-- {"allow"|"deny", reason}; we read the tag directly.
+local function check(principal, action, resource)
+  principal = principal or {}; resource = resource or {}
+  local prin = { sym("prin"), principal.name or "", principal.role or "", principal.tenant or "" }
+  local res  = { sym("res"),  resource.owner  or "", resource.tenant or "" }
+  local d = decide(prin, tostring(action or ""), res)
+  return d[1] == "allow", d[2]
+end
+
+-- ---- request handling (pure; shared with selftest) --------------------------
+local function dispatch(method, path, body)
+  if path == "/api/check" and method == "POST" then
+    local allowed, reason = check(body and body.subject, body and body.action, body and body.resource)
+    return 200, { allowed = allowed, reason = reason, decision = allowed and "allow" or "deny" }
+  end
+  return 404, { error = "not found" }
+end
+
+local M = { dispatch = dispatch, check = check, json = cjson }
+
+function M.handle()
+  local method = ngx.req.get_method()
+  local decoded
+  if method == "POST" then
+    ngx.req.read_body()
+    local raw = ngx.req.get_body_data()
+    if raw and raw ~= "" then
+      local d = cjson.decode(raw)
+      if d == nil then
+        ngx.status = 400; ngx.header.content_type = "application/json"
+        ngx.say(cjson.encode({ error = "invalid JSON" })); return
+      end
+      decoded = d
+    end
+  end
+  local status, body = dispatch(method, ngx.var.uri, decoded)
+  ngx.status = status
+  ngx.header.content_type = "application/json"
+  ngx.say(cjson.encode(body))
+end
+
+-- ---- the edge enforcement gate (access_by_lua on /protected/) --------------
+-- The principal/resource come from request headers for the demo; in production
+-- they'd come from a verified JWT / session and the resource being addressed.
+function M.gate()
+  local h = ngx.req.get_headers()
+  local allowed, reason = check(
+    { name = h["x-subject"], role = h["x-role"], tenant = h["x-tenant"] },
+    ngx.req.get_method() == "GET" and "read" or "write",
+    { owner = h["x-res-owner"], tenant = h["x-res-tenant"] })
+  if not allowed then
+    ngx.status = 403
+    ngx.header.content_type = "application/json"
+    ngx.say(cjson.encode({ error = "forbidden", reason = reason }))
+    return ngx.exit(403)
+  end
+  -- allowed: fall through to the protected content
+end
+
+return M
diff --git a/examples/policy/json_shim.lua b/examples/policy/json_shim.lua
new file mode 100644
index 0000000..0cd6bc6
--- /dev/null
+++ b/examples/policy/json_shim.lua
@@ -0,0 +1,148 @@
+-- examples/openresty/json_shim.lua — a minimal JSON codec.
+--
+-- Used ONLY when the real lua-cjson is unavailable (i.e. running the example
+-- off-nginx under plain luajit, e.g. selftest.lua). OpenResty bundles cjson,
+-- so under the actual server this file is never loaded. It implements just
+-- the surface app.lua uses: decode, encode, and an empty_array sentinel.
+
+local json = {}
+
+-- A unique sentinel so an empty Lua table can be encoded as [] not {}.
+json.empty_array = setmetatable({}, { __tostring = function() return "[]" end })
+
+-- ---- encode ----------------------------------------------------------------
+local escapes = { ['"'] = '\\"', ['\\'] = '\\\\', ['\n'] = '\\n',
+                  ['\r'] = '\\r', ['\t'] = '\\t' }
+local function enc_str(s)
+  return '"' .. s:gsub('[%z\1-\31"\\]', function(c)
+    return escapes[c] or ('\\u%04x'):format(c:byte())
+  end) .. '"'
+end
+
+local encode
+local function enc_table(v, out)
+  if v == json.empty_array then out[#out + 1] = "[]"; return end
+  local n = #v
+  local is_array = n > 0
+  if is_array then
+    out[#out + 1] = "["
+    for i = 1, n do
+      if i > 1 then out[#out + 1] = "," end
+      encode(v[i], out)
+    end
+    out[#out + 1] = "]"
+  else
+    -- object (or empty table -> {})
+    out[#out + 1] = "{"
+    local first = true
+    for k, val in pairs(v) do
+      if not first then out[#out + 1] = "," end
+      first = false
+      out[#out + 1] = enc_str(tostring(k)); out[#out + 1] = ":"
+      encode(val, out)
+    end
+    out[#out + 1] = "}"
+  end
+end
+
+encode = function(v, out)
+  local t = type(v)
+  if t == "string" then out[#out + 1] = enc_str(v)
+  elseif t == "number" then out[#out + 1] = tostring(v)
+  elseif t == "boolean" then out[#out + 1] = v and "true" or "false"
+  elseif t == "nil" then out[#out + 1] = "null"
+  elseif t == "table" then enc_table(v, out)
+  else error("json: cannot encode " .. t) end
+end
+
+function json.encode(v)
+  local out = {}
+  encode(v, out)
+  return table.concat(out)
+end
+
+-- ---- decode (small recursive-descent parser) -------------------------------
+local function decode_error(s, i, msg)
+  error(("json: %s at byte %d"):format(msg, i), 0)
+end
+
+local parse_value
+local function skip_ws(s, i)
+  local _, j = s:find("^[ \t\r\n]*", i)
+  return (j or i - 1) + 1
+end
+
+local function parse_string(s, i)
+  i = i + 1                                   -- skip opening quote
+  local buf = {}
+  while i <= #s do
+    local c = s:sub(i, i)
+    if c == '"' then return table.concat(buf), i + 1
+    elseif c == '\\' then
+      local e = s:sub(i + 1, i + 1)
+      local map = { ['"'] = '"', ['\\'] = '\\', ['/'] = '/', n = '\n',
+                    t = '\t', r = '\r', b = '\b', f = '\f' }
+      if map[e] then buf[#buf + 1] = map[e]; i = i + 2
+      elseif e == 'u' then
+        local hex = s:sub(i + 2, i + 5)
+        buf[#buf + 1] = string.char(tonumber(hex, 16) % 256); i = i + 6
+      else decode_error(s, i, "bad escape") end
+    else buf[#buf + 1] = c; i = i + 1 end
+  end
+  decode_error(s, i, "unterminated string")
+end
+
+local function parse_number(s, i)
+  local j = s:find("[^%d%+%-eE%.]", i) or (#s + 1)
+  local num = tonumber(s:sub(i, j - 1))
+  if not num then decode_error(s, i, "bad number") end
+  return num, j
+end
+
+parse_value = function(s, i)
+  i = skip_ws(s, i)
+  local c = s:sub(i, i)
+  if c == '"' then return parse_string(s, i)
+  elseif c == '{' then
+    local obj = {}
+    i = skip_ws(s, i + 1)
+    if s:sub(i, i) == '}' then return obj, i + 1 end
+    while true do
+      local key; key, i = parse_string(s, skip_ws(s, i))
+      i = skip_ws(s, i)
+      if s:sub(i, i) ~= ':' then decode_error(s, i, "expected ':'") end
+      local val; val, i = parse_value(s, i + 1)
+      obj[key] = val
+      i = skip_ws(s, i)
+      local d = s:sub(i, i)
+      if d == '}' then return obj, i + 1
+      elseif d == ',' then i = skip_ws(s, i + 1)
+      else decode_error(s, i, "expected ',' or '}'") end
+    end
+  elseif c == '[' then
+    local arr = {}
+    i = skip_ws(s, i + 1)
+    if s:sub(i, i) == ']' then return arr, i + 1 end
+    while true do
+      local val; val, i = parse_value(s, i)
+      arr[#arr + 1] = val
+      i = skip_ws(s, i)
+      local d = s:sub(i, i)
+      if d == ']' then return arr, i + 1
+      elseif d == ',' then i = i + 1
+      else decode_error(s, i, "expected ',' or ']'") end
+    end
+  elseif s:sub(i, i + 3) == "true"  then return true, i + 4
+  elseif s:sub(i, i + 4) == "false" then return false, i + 5
+  elseif s:sub(i, i + 3) == "null"  then return nil, i + 4
+  else return parse_number(s, i) end
+end
+
+-- cjson.safe-style: returns nil, errmsg on failure rather than throwing.
+function json.decode(s)
+  local ok, v = pcall(parse_value, s, 1)
+  if not ok then return nil, v end
+  return v
+end
+
+return json
diff --git a/examples/policy/nginx.conf b/examples/policy/nginx.conf
new file mode 100644
index 0000000..75d8c69
--- /dev/null
+++ b/examples/policy/nginx.conf
@@ -0,0 +1,61 @@
+# examples/policy/nginx.conf — a typed authorization gateway on OpenResty.
+#
+#     mkdir -p examples/policy/logs
+#     openresty -p "$PWD/examples/policy" -c nginx.conf
+#
+# then open http://127.0.0.1:8091/ for the live policy explorer. The same
+# decide() also guards /protected/ as an access_by_lua gate (try it with curl,
+# below) — one rule set, enforced at the edge and previewed in the browser.
+#
+#   # allowed (admin in tenant t1):
+#   curl -i -H 'X-Subject: boss' -H 'X-Role: admin' -H 'X-Tenant: t1' \
+#        -H 'X-Res-Owner: ada' -H 'X-Res-Tenant: t1' localhost:8091/protected/
+#   # denied (cross-tenant):
+#   curl -i -H 'X-Subject: boss' -H 'X-Role: admin' -H 'X-Tenant: t2' \
+#        -H 'X-Res-Owner: ada' -H 'X-Res-Tenant: t1' localhost:8091/protected/
+
+daemon off;
+worker_processes 1;
+pid logs/nginx.pid;
+error_log logs/error.log info;
+
+events { worker_connections 256; }
+
+http {
+    access_log logs/access.log;
+
+    types {
+        text/html        html htm;
+        text/javascript  js mjs;
+        application/json json;
+    }
+    default_type application/octet-stream;
+
+    init_by_lua_block {
+        local prefix = ngx.config.prefix()
+        package.path = prefix .. "../../?.lua;" .. prefix .. "?.lua;" .. package.path
+    }
+
+    init_worker_by_lua_block { require("app") }   -- boot Shen + typed load once
+
+    server {
+        listen 8091;
+
+        # the preview endpoint the explorer page calls
+        location /api/ {
+            content_by_lua_block { require("app").handle() }
+        }
+
+        # the enforcement gate: decide() runs BEFORE the protected content
+        location /protected/ {
+            access_by_lua_block { require("app").gate() }
+            content_by_lua_block { ngx.header.content_type = "application/json"
+                                   ngx.say('{"ok":true,"secret":"the protected resource"}') }
+        }
+
+        # serve the rules themselves (one source of truth)
+        location = /policy.shen { default_type text/plain; alias policy.shen; }
+
+        location / { root public; index index.html; }
+    }
+}
diff --git a/examples/policy/policy.shen b/examples/policy/policy.shen
new file mode 100644
index 0000000..7c660e5
--- /dev/null
+++ b/examples/policy/policy.shen
@@ -0,0 +1,66 @@
+\\ policy.shen — a typed authorization engine, shared by the edge (shen-lua
+\\ under OpenResty), the browser preview (ShenScript), and any other port.
+\\ One source of truth for "who may do what", loaded under (tc +) so every rule
+\\ is proved well-typed before the gateway serves a request.
+\\
+\\ The decision function returns not just allow/deny but the REASON — the same
+\\ value the edge enforces and the preview UI renders, so an operator sees
+\\ exactly why a request passed or failed. policy_proof.shen takes the same
+\\ rules to their logical conclusion: an authorization IS a proof term (a
+\\ permission you can typecheck), authz as type inhabitation.
+
+\\ -- the domain --------------------------------------------------------------
+\\ A principal carries its role and tenant; a resource carries its owner and
+\\ tenant. Both are tagged so the typechecker proves every rule covers them.
+(datatype principal
+  Name : string; Role : string; Tenant : string;
+  ==============================================
+  [prin Name Role Tenant] : principal;)
+
+(datatype resource
+  Owner : string; Tenant : string;
+  ================================
+  [res Owner Tenant] : resource;)
+
+\\ A decision is an allow or a deny, each carrying a human-readable reason.
+(datatype decision
+  R : string;
+  =================
+  [allow R] : decision;
+
+  R : string;
+  ================
+  [deny R] : decision;)
+
+\\ -- the rules ---------------------------------------------------------------
+\\ Tenant isolation is checked FIRST and is absolute: no role, not even admin,
+\\ crosses a tenant boundary. Within a tenant: owners may do anything; then
+\\ role decides. Every branch returns a decision, so `decide` is total.
+
+(define decide
+  {principal --> string --> resource --> decision}
+  [prin Name Role STenant] Action [res Owner RTenant]
+    -> (if (not (= STenant RTenant))
+           [deny (cn "cross-tenant: " (cn STenant (cn " cannot reach " RTenant)))]
+           (if (= Name Owner)
+               [allow (cn Name " owns this resource")]
+               (decide-role Role Action))))
+
+(define decide-role
+  {string --> string --> decision}
+  "admin"  _       -> [allow "admin role within tenant"]
+  "member" "read"  -> [allow "member may read"]
+  "member" "write" -> [allow "member may write"]
+  "viewer" "read"  -> [allow "viewer may read"]
+  Role     Action  -> [deny (cn "role " (cn Role (cn " may not " Action)))])
+
+\\ -- accessors the host (edge / preview) calls ------------------------------
+(define allowed?
+  {decision --> boolean}
+  [allow _] -> true
+  [deny _]  -> false)
+
+(define why
+  {decision --> string}
+  [allow R] -> R
+  [deny R]  -> R)
diff --git a/examples/policy/policy_proof.shen b/examples/policy/policy_proof.shen
new file mode 100644
index 0000000..be5220e
--- /dev/null
+++ b/examples/policy/policy_proof.shen
@@ -0,0 +1,63 @@
+\\ policy_proof.shen — authorization as TYPE INHABITATION.
+\\
+\\ policy.shen decides allow/deny by evaluating rules (and is what the edge
+\\ runs). This file shows the same authorization model as a logic: a term of
+\\ type (may S A R) is a PROOF that subject S may perform action A on resource
+\\ R. Grant rules are inference rules; environment facts (ownership, roles,
+\\ tenancy — what a directory or DB would supply) are axioms. A request is
+\\ AUTHORIZED exactly when (may S A R) is inhabited, and the inhabiting term is
+\\ the justification — the audit trail of *why*, checked by the type system.
+\\
+\\ A DENIED request is an UNINHABITED type: no rule builds the term, so it
+\\ cannot typecheck (see perm-bob-delete, commented out). "Deny by default" is
+\\ not a policy line you can forget to write — it is the absence of a proof.
+
+(datatype authz
+  \\ -- environment facts (axioms; would be fetched per request) --------------
+  ______________________________
+  [owns-fact] : (owns alice doc1);
+
+  ______________________________________
+  [alice-tenant] : (same-tenant alice doc1);
+
+  _________________________________
+  [member-fact] : (has-role bob member);
+
+  ____________________________________
+  [tenant-fact] : (same-tenant bob doc1);
+
+  \\ -- grant rules (universal in S, A, R) ------------------------------------
+  \\ an owner may take ANY action on what they own — but tenant isolation is
+  \\ absolute, so ownership ALONE is not enough: the owner must also be in the
+  \\ resource's tenant. This premise mirrors decide() in policy.shen, which
+  \\ checks the tenant boundary before it ever considers ownership.
+  P : (owns S R); Q : (same-tenant S R);
+  ======================================
+  [by-owner P Q] : (may S A R);
+
+  \\ a member, in the resource's tenant, may READ it
+  P : (has-role S member); Q : (same-tenant S R);
+  ===============================================
+  [by-member-read P Q] : (may S read R);)
+
+\\ -- authorizations, as checked proof terms ----------------------------------
+\\ Each function's RESULT TYPE is the permission; the body is the proof. If the
+\\ file loads under (tc +), the type checker has verified every authorization.
+
+\\ alice OWNS doc1 AND is in its tenant, so she may perform ANY action A on it:
+(define perm-alice-any
+  { unit --> (may alice A doc1) }
+  _ -> [by-owner [owns-fact] [alice-tenant]])
+
+\\ bob is a member in doc1's tenant, so he may READ it:
+(define perm-bob-read
+  { unit --> (may bob read doc1) }
+  _ -> [by-member-read [member-fact] [tenant-fact]])
+
+\\ -- denial is the absence of a proof ----------------------------------------
+\\ bob may NOT delete doc1: no grant rule produces (may bob delete _) for a
+\\ member, and bob does not own doc1 — the type is uninhabited. Uncomment and
+\\ the load fails with a type error: you cannot fabricate the proof.
+\\ (define perm-bob-delete
+\\   { unit --> (may bob delete doc1) }
+\\   _ -> [by-member-read [member-fact] [tenant-fact]])   \\ proves `read`, not `delete`
diff --git a/examples/policy/public/index.html b/examples/policy/public/index.html
new file mode 100644
index 0000000..5b484f5
--- /dev/null
+++ b/examples/policy/public/index.html
@@ -0,0 +1,98 @@
+<!DOCTYPE html>
+<!--
+  examples/policy/public/index.html — a live authorization explorer.
+
+  Set a subject, an action, and a resource; the page POSTs the triple to
+  /api/check and shows the verdict and the REASON, computed by decide() in
+  policy.shen (shen-lua, under OpenResty, loaded under (tc +)). The very same
+  decide() guards /protected/ as an edge gate — this UI previews exactly what
+  the gateway will enforce.
+-->
+<html lang="en">
+<head>
+  <meta charset="utf-8">
+  <meta name="viewport" content="width=device-width, initial-scale=1">
+  <title>shen-lua · authorization explorer</title>
+  <style>
+    body { font: 16px/1.5 system-ui, sans-serif; max-width: 46rem; margin: 2.5rem auto; padding: 0 1rem; color: #1f2937; }
+    h1 { font-size: 1.4rem; } a { color: #2563eb; } code { background: #f0f0f0; padding: 0 .25em; border-radius: 3px; }
+    .grid { display: grid; grid-template-columns: 1fr 1fr; gap: 1rem 1.5rem; margin: 1.5rem 0; }
+    fieldset { border: 1px solid #e5e7eb; border-radius: 8px; }
+    legend { font-size: .8rem; color: #6b7280; padding: 0 .4rem; }
+    label { display: block; font-size: .8rem; color: #6b7280; margin-top: .4rem; }
+    input, select { font: inherit; padding: .4rem; border: 1px solid #ccc; border-radius: 4px; width: 100%; box-sizing: border-box; }
+    .verdict { border-radius: 8px; padding: 1.25rem; margin: 1rem 0; font-size: 1.1rem; }
+    .allow { background: #dcfce7; border: 1px solid #86efac; color: #166534; }
+    .deny  { background: #fee2e2; border: 1px solid #fca5a5; color: #991b1b; }
+    .verdict b { font-size: 1.3rem; display: block; }
+    .reason { font-size: .95rem; opacity: .85; margin-top: .25rem; }
+    .arch { background: #f8fafc; border: 1px solid #e5e7eb; border-radius: 8px; padding: 1rem 1.25rem; margin: 1.5rem 0; font-size: .95rem; }
+  </style>
+</head>
+<body>
+  <h1>Authorization explorer <small>— decided by Shen</small></h1>
+  <p>Pick a subject, action, and resource. The verdict and reason are computed
+     by <code>decide</code> in <a href="/policy.shen" target="_blank"><code>policy.shen</code></a>,
+     the same typed rules that guard <code>/protected/</code> at the edge.
+     Try a cross-tenant request, or a viewer trying to write.</p>
+
+  <div class="grid">
+    <fieldset>
+      <legend>subject</legend>
+      <label>name</label>   <input id="s-name" value="ada">
+      <label>role</label>
+      <select id="s-role"><option>member</option><option>admin</option><option>viewer</option></select>
+      <label>tenant</label> <input id="s-tenant" value="t1">
+    </fieldset>
+    <fieldset>
+      <legend>resource</legend>
+      <label>action</label>
+      <select id="action"><option>read</option><option>write</option><option>delete</option></select>
+      <label>owner</label>  <input id="r-owner" value="ada">
+      <label>tenant</label> <input id="r-tenant" value="t1">
+    </fieldset>
+  </div>
+
+  <div class="verdict" id="verdict">…</div>
+
+  <section class="arch">
+    <b>What this demonstrates.</b> Authorization is a single typed rule set
+    (<code>policy.shen</code>), proven well-typed at boot under <code>(tc +)</code>,
+    shared by the edge gate and this preview — so what you see is what the
+    gateway enforces, with no drift. Tenant isolation is checked first and is
+    absolute. The companion <code>policy_proof.shen</code> takes it further:
+    a permission is a <i>proof term</i>, and a denied request is an uninhabited
+    type — "deny by default" you cannot forget to write.
+  </section>
+
+  <script type="module">
+    const $ = (id) => document.getElementById(id);
+    const esc = (s) => String(s).replace(/[&<>"]/g, (c) =>
+      ({ "&": "&amp;", "<": "&lt;", ">": "&gt;", '"': "&quot;" }[c]));
+    const fields = ["s-name", "s-role", "s-tenant", "action", "r-owner", "r-tenant"];
+
+    async function recheck() {
+      const body = {
+        subject:  { name: $("s-name").value, role: $("s-role").value, tenant: $("s-tenant").value },
+        action:   $("action").value,
+        resource: { owner: $("r-owner").value, tenant: $("r-tenant").value },
+      };
+      let res;
+      try {
+        res = await (await fetch("/api/check", {
+          method: "POST", headers: { "Content-Type": "application/json" },
+          body: JSON.stringify(body),
+        })).json();
+      } catch (e) { $("verdict").className = "verdict deny"; $("verdict").textContent = "server unreachable"; return; }
+      const v = $("verdict");
+      v.className = "verdict " + (res.allowed ? "allow" : "deny");
+      // the reason embeds user-controlled role/tenant/name strings — escape it
+      v.innerHTML = `<b>${res.allowed ? "ALLOW" : "DENY"}</b>`
+                  + `<div class="reason">${esc(res.reason || "")}</div>`;
+    }
+
+    fields.forEach((f) => { $(f).addEventListener("input", recheck); $(f).addEventListener("change", recheck); });
+    recheck();
+  </script>
+</body>
+</html>
diff --git a/examples/policy/selftest.lua b/examples/policy/selftest.lua
new file mode 100644
index 0000000..2b10185
--- /dev/null
+++ b/examples/policy/selftest.lua
@@ -0,0 +1,44 @@
+-- examples/policy/selftest.lua — verify the authorization demo off-nginx.
+--
+--   luajit examples/policy/selftest.lua      (from the repo root)
+--
+-- Drives the SAME decide() the edge gate uses over a table of requests, then
+-- loads policy_proof.shen under (tc +) to confirm the "permission is a proof"
+-- terms typecheck. No nginx, no network.
+
+local root = arg[0]:match("^(.*)/examples/policy/[^/]+$") or "."
+package.path = root .. "/?.lua;" .. root .. "/examples/policy/?.lua;" .. package.path
+
+local app  = require("app")
+local shen = require("shen")
+
+local fail = 0
+local function expect(label, want, principal, action, resource)
+  local allowed, reason = app.check(principal, action, resource)
+  io.write(("  %-22s %-5s  %s\n"):format(label, allowed and "ALLOW" or "DENY", reason))
+  if allowed ~= want then fail = fail + 1; print("      FAIL: expected " .. tostring(want)) end
+end
+
+local alice  = { name = "ada",  role = "member", tenant = "t1" }
+local boss   = { name = "boss", role = "admin",  tenant = "t1" }
+local viewer = { name = "viv",  role = "viewer", tenant = "t1" }
+local other  = { name = "boss", role = "admin",  tenant = "t2" }
+local doc    = { owner = "ada", tenant = "t1" }
+
+print("== decisions (the rules the edge gate enforces) ==")
+expect("owner writes own",  true,  alice,  "write",  doc)
+expect("admin deletes",     true,  boss,   "delete", doc)
+expect("viewer reads",      true,  viewer, "read",   doc)
+expect("viewer writes",     false, viewer, "write",  doc)
+expect("member deletes",    false, { name="bob", role="member", tenant="t1" }, "delete", doc)
+expect("cross-tenant admin",false, other,  "read",   doc)
+
+print("\n== permission-as-proof (tier c, type inhabitation) ==")
+shen.eval("(tc +)")
+local ok = pcall(shen.prims.F["load"], root .. "/examples/policy/policy_proof.shen")
+shen.eval("(tc -)")
+io.write(("  %-44s %s\n"):format("policy_proof.shen loads => proofs check", ok and "ok" or "FAIL"))
+if not ok then fail = fail + 1 end
+
+if fail == 0 then print("\nOK — all checks passed")
+else print(("\n%d check(s) FAILED"):format(fail)); os.exit(1) end