diff --git a/.gitignore b/.gitignore
index c41455a..22aae81 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,3 +6,4 @@ build/shen-bundle.lua
 luacov.stats.out
 luacov.report.out
 examples/openresty/logs/
+examples/openresty-authz/logs/
diff --git a/examples/README.md b/examples/README.md
index 2fec0ca..bcf6143 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -13,6 +13,7 @@ has a `selftest.lua` that runs off-nginx):
 | [`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. |
+| [`openresty-authz/`](openresty-authz/) | durable multi-tenant **authorization**: the policy as a Prolog proof chain (`token → user → tenant → resource`), a typed `decision` witness that gates every response, and an event-sourced store (file + `lua-resty-lmdb`) whose append-only log makes decisions durable and auditable. Runs standalone via `luajit examples/openresty-authz/selftest.lua`; see [its README](openresty-authz/README.md). |
 
 The last three (`configc/`, `policy/`, `crdt/`) are a themed trio: each extracts
 a correctness-critical kernel into one typed, portable Shen file that runs
diff --git a/examples/openresty-authz/README.md b/examples/openresty-authz/README.md
new file mode 100644
index 0000000..33fb9df
--- /dev/null
+++ b/examples/openresty-authz/README.md
@@ -0,0 +1,246 @@
+# Durable multi-tenant authorization in Shen, on OpenResty
+
+A companion to [`examples/openresty`](../openresty) (the guestbook). That one
+shows the *shape* of a Shen web app and shares one typed `rules.shen` between
+server and browser. This one goes after a harder problem — **authorization** —
+and answers a specific design question:
+
+> Can we get [Shen-Backpressure][sb]'s "move the invariant into a structure the
+> agent cannot bypass" idea for a real, running authz endpoint — with the policy
+> as a proof chain, decisions that are durable and auditable — **without**
+> bolting on a new engine?
+
+Short answer: yes, by reusing three things shen-lua already has — the
+sequent-calculus typechecker, the native Prolog engine, and the Lua bridge —
+and adding one small durable, event-sourced store.
+
+[sb]: https://reubenbrooks.dev/blog/structural-backpressure-beats-smarter-agents/
+
+```
+examples/openresty-authz/
+  authz.shen     the TYPED core (tc +): the `decision` verdict and the guarded
+                 projection `render-doc` — content can only be serialized out of
+                 a [granted ...] witness. Proved total at load time.
+  app.shen       the policy (tc -): the authz PROOF CHAIN as Prolog rules, plus
+                 the router. Leaf facts are read from the durable store.
+  store.lua      durable, event-sourced fact store + append-only proof log.
+                 File backend (tested) and an lua-resty-lmdb backend (production).
+  auth.lua       identity at the head of the chain: local verification by default
+                 (JWT-style, no I/O); an opt-in cosocket resolver for opaque tokens.
+  app.lua        the glue: boots Shen, wires host bridges, marshals JSON <-> val.
+  selftest.lua   drives the whole thing under plain luajit — no nginx needed.
+  nginx.conf     OpenResty config: boot once per worker, replay the log, serve.
+```
+
+## Try it without nginx
+
+```sh
+luajit examples/openresty-authz/selftest.lua
+```
+
+It provisions two tenants over the JSON API, runs the proof chain (grants,
+cross-tenant denials, editor-only writes, a revocation), then **reopens the
+store from its durable log** to prove the facts and the audit trail survive a
+restart. It does this for **both** the file and lua-resty-lmdb backends and
+asserts they agree decision-for-decision, then prints the durable decision log.
+
+## The policy is a proof chain (Shen-Backpressure, at runtime)
+
+Shen-Backpressure encodes multi-tenant access as a chain where each step must
+hold before the next can be built: `token → authenticated user → tenant
+membership → resource access`. Here that chain is a Prolog rule in `app.shen`:
+
+```
+(defprolog can-read
+  Tok R <-- (is U (host-token-user (receive Tok)))   \\ token -> user
+            (when (not (= U "")))                     \\ ...authenticated
+            (is T (host-owner-tenant (receive R)))    \\ resource -> tenant
+            (when (not (= T "")))
+            (when (host-member? U T))                 \\ user in that tenant
+            (when (not (host-revoked? U (receive R)))); )
+```
+
+`can-write` is the same chain plus `(when (host-role? U T "editor"))`. The rule
+**is** the policy — one place, read top to bottom.
+
+The structural-backpressure half lives in the typed core (`authz.shen`). A
+`decision` is either `[granted U T R]` or `[denied Why]`, and `render-doc` is a
+*total* function over `decision` that places document content in the response
+for `[granted ...]` **and no other shape**:
+
+```
+(define render-doc
+  {decision --> string --> val}
+  [granted U T R] Content -> [obj [... ["content" [s Content]] ...]]
+  [denied Why] _          -> [obj [["ok" [b false]] ["error" [s Why]]]])
+```
+
+Shen's typechecker verifies that totality at load time, so "a document reached
+the client" implies "a `granted` witness was constructed." That is
+Shen-Backpressure's `shengen` guard-type idea — the constructor is the only path
+to a populated value — moved to a **runtime witness** because the facts
+(memberships, ownership) are dynamic. It is the honest version of the guarantee:
+the *shape* is enforced by types; the *decision* is enforced by the one gate
+(`authorize-*`) that every path must go through to obtain a `decision`.
+
+## Why Prolog, and not a Datalog engine
+
+Datalog is a subset of Prolog: ground facts, no compound terms in recursion,
+"safe" rules. Authorization rules are exactly that shape, so the temptation is
+to add a Datalog engine. We didn't, on purpose:
+
+- **shen-lua already ships a Prolog engine** (`defprolog` / `(prolog? ...)`, the
+  FFI/int32 soa32 machine — see [`examples/family.shen`](../family.shen)). The
+  authz rules stay inside the Datalog fragment *by discipline*, so they
+  terminate and stay decidable without a second engine.
+- **A ground authz query wants top-down evaluation.** You ask one specific goal
+  — `can-read? this-token this-resource` — which is SLD resolution's sweet spot.
+  A Datalog engine optimizes the opposite job: materializing *all* derivable
+  facts bottom-up. For "is this one request allowed?", Prolog is the better fit,
+  not a compromise.
+- **The one thing worth borrowing from Datalog** — stratified negation for
+  deny/revoke rules — we take carefully: negation only on *ground* goals
+  (`(not (host-revoked? U R))` with `U`, `R` bound), which is well-defined.
+
+The facts are **not** asserted into the engine. Prolog composes; the durable
+store supplies each leaf fact through `lua.call` (`host-member?`,
+`host-owner-tenant`, …). So the store stays the single source of truth and no
+per-worker fact cache can drift.
+
+## Durable execution: the log is the state
+
+`store.lua` is **event-sourced**. Every mutation (grant, revoke, create) and
+every authorization decision is appended to a log; the in-memory view everyone
+reads is a *cache* rebuilt by replaying that log on open. That is the
+durable-execution property, stated plainly:
+
+> Kill the process, reopen the same log, replay — you are in the exact same
+> state, facts **and** audit trail. Nothing lives only in RAM.
+
+`selftest.lua` demonstrates it literally: it builds up state, throws the store
+object away, constructs a fresh one over the same file, and shows a prior
+revocation still denies access.
+
+Two backends sit behind one `append` + `each` interface:
+
+- **file** — append-only JSONL on disk. `flush()`ed on each append, so it is
+  durable across a *process* crash; it does not `fsync`, so it is not power-loss
+  durable (use the lmdb backend, or add an fsync policy, if you need that). The
+  default under plain LuaJIT.
+- **lmdb** — the same log in [`lua-resty-lmdb`][lmdb] (memory-mapped, MVCC,
+  ACID, zero-copy FFI reads — the store Kong ships). Production path under
+  OpenResty; `nginx.conf` shows the two-line swap.
+
+`selftest.lua` runs the **whole scenario against both backends** — the lmdb one
+in-process against a faithful fake of `resty.lmdb` — and asserts they produce an
+identical, decision-for-decision audit trail. So the lmdb adapter's logic
+(transactional append, replay) is tested here; only the real memory-mapped
+environment needs OpenResty.
+
+[lmdb]: https://github.com/openresty/lua-resty-lmdb
+
+The decision events double as the **discharge report** from Shen-Backpressure:
+`POST /api/admin/audit` (admin-gated — it lists users and denial reasons)
+returns, for every decision, which premise carried it or which one failed (`not
+a member of tenant acme`, `requires the editor role`, `access … was revoked`).
+"Why was this allowed?" is answerable from durable state.
+
+## Identity: local by default, a cosocket only when the store is remote
+
+The head of the proof chain is `token → authenticated user`. Whether resolving
+it touches the network is a **token-format** decision, not a given — and the
+default here is **no network at all**:
+
+- **Signed tokens (JWT/PASETO)** — the usual choice for a stateless gate. You
+  verify **locally**: signature + `exp`/`aud`/`iss`. That is CPU (crypto), not
+  I/O; the only network is a JWKS key fetch, cached for hours. No cosocket on the
+  hot path. This is `M.local_resolver` and the default the app ships with.
+- **Opaque tokens (session ids / OAuth2 introspection)** — the token means
+  nothing on its own, so it *must* be looked up in a remote store. **Only then**
+  is identity network I/O, and a blocking socket would stall the whole
+  single-threaded worker for the round-trip.
+
+For that opaque case — and only that case — OpenResty's answer is the **cosocket
+API**, `ngx.socket.tcp()`, whose `connect`/`send`/`receive`/`setkeepalive` yield
+to the event loop instead of blocking and pool connections across requests.
+`M.cosocket_resolver` uses it directly (a minimal Redis `GET auth:<token>`;
+`lua-resty-redis` / `lua-resty-http` wrap these same calls), with a short-TTL
+`lua_shared_dict` cache in front so even then the common request never touches
+the socket, and a fallback to the local resolver so a store outage degrades
+rather than fails:
+
+```lua
+local sock = ngx.socket.tcp()
+sock:settimeout(cfg.timeout_ms)
+sock:connect(cfg.host, cfg.port)     -- pooled, non-blocking
+sock:send(resp_get)                  -- yields to the event loop, doesn't block
+local line = sock:receive("*l")      -- ...
+sock:setkeepalive(60000, 20)         -- return the conn to the per-worker pool
+```
+
+`token_user` is pluggable (`app.use_auth`), so this is the only place identity
+resolution changes — the Prolog policy is untouched. `selftest.lua` still
+exercises the cosocket path in-process against a fake `ngx.socket.tcp` (first
+lookup does one round-trip, second is cache-served, a missing key takes the
+Redis `$-1` path), so the opaque-token path is covered even though it isn't the
+default. Note that the durable *policy* store stays local (LMDB, zero-copy FFI
+reads) by design — so a well-tuned gate leans on cosockets **sparingly**: JWKS
+refresh, opaque-token introspection, or replicating the event log off the
+request path. It is not a per-request hop you want if you can avoid it.
+
+Two operational notes for the opaque path: the resolver **fails closed** by
+default — a store error resolves to no identity, so the chain denies (passing
+`opts.fallback` is an explicit opt-in to degrade to local data instead). And the
+shared-dict cache means a revocation recorded in the session store lags by up to
+its TTL (5s here) before every worker sees it — tune the TTL to your tolerance.
+
+## Leaning on LuaJIT
+
+- The Prolog engine is the FFI/int32 soa32 machine — no boxing on the reasoning
+  hot path; it JITs.
+- `authorize` is, per request, a handful of plain-hash-table lookups (the
+  materialized view) plus one ground Prolog query. The log append — the only
+  allocation-heavy step — is off the read/decide path.
+- Kernel boot + the typed load of `authz.shen` happen **once per worker** in
+  `init_worker_by_lua`, never per request; log replay happens once at that boot.
+- Under the lmdb backend, fact reads are zero-copy through the resty.lmdb FFI.
+
+## Running under OpenResty
+
+```sh
+mkdir -p examples/openresty-authz/logs
+openresty -p "$PWD/examples/openresty-authz" -c nginx.conf
+```
+
+The worker seeds a demo world on first boot (tokens `tok-admin`, `tok-alice`,
+`tok-bob`, `tok-carol`; tenants `acme`/`globex`; docs `doc-1`/`doc-2`).
+
+```sh
+# alice (editor@acme) reads an acme doc — granted
+curl -s localhost:8080/api/read  -d '{"token":"tok-alice","resource":"doc-1"}'
+# carol (no membership) — denied, with the discharge report
+curl -s localhost:8080/api/read  -d '{"token":"tok-carol","resource":"doc-1"}'
+# bob (viewer) cannot write — needs the editor role
+curl -s localhost:8080/api/write -d '{"token":"tok-bob","resource":"doc-1","content":"x"}'
+# the durable decision log (admin-gated)
+curl -s localhost:8080/api/admin/audit -d '{"token":"tok-admin"}'
+```
+
+## Things to know before building on this
+
+- **Single worker as written.** The materialized view is per-worker state, so
+  with `worker_processes > 1` a mutation on one worker is not visible to another
+  until it re-replays. LMDB is the shared, durable substrate to fix that — but
+  note it is not automatic: the demo's `append` allocates the sequence number
+  with a read-modify-write *outside* the transaction, which races across
+  workers. Making it multi-worker safe means allocating the seq atomically (read
+  it inside the txn and retry on conflict, or a compare-and-set) and having
+  readers re-replay when the txn id advances. The file backend can't be shared
+  at all.
+- **Tokens stand in for JWTs.** Off-nginx, `token_user` is a local lookup; under
+  nginx, `auth.lua` resolves it over a cosocket to a session store (or you'd
+  verify a JWT signature and return the subject). Either way the proof chain is
+  unchanged — only the leaf fact gets more honest.
+- **Never use Shen's blocking file I/O under nginx.** The file backend is for
+  the off-nginx demo; under OpenResty use the lmdb backend (or reach a DB via
+  the non-blocking cosocket libraries), exactly as the guestbook README warns.
diff --git a/examples/openresty-authz/app.lua b/examples/openresty-authz/app.lua
new file mode 100644
index 0000000..96e3859
--- /dev/null
+++ b/examples/openresty-authz/app.lua
@@ -0,0 +1,142 @@
+-- examples/openresty-authz/app.lua — glue between OpenResty and shen-lua for
+-- the multi-tenant authz demo. Same shape as the guestbook example's app.lua:
+-- boot the kernel ONCE per worker, register the typed Lua bridges, load the
+-- typed core (authz.shen, tc +) and the policy/router (app.shen, tc -), and
+-- expose M.handle() as the content handler. Per request it marshals nginx data
+-- into Shen, calls (route Method Path Body), and JSON-encodes the result.
+
+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 OpenResty; the repo's json_shim off-nginx (selftest under 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 .. "/../openresty/json_shim.lua"))()
+end
+
+-- A pluggable durable store (store.lua). selftest.lua injects a file-backed
+-- one; nginx wires an lmdb-backed one. Default no-op keeps this module loadable
+-- on its own.
+local store = {
+  token_user = function() return "" end, is_admin = function() return false end,
+  owner_tenant = function() return "" end, member = function() return false end,
+  role = function() return false end, revoked = function() return false end,
+  content = function() return "" end, grant = function() end, revoke = function() end,
+  create = function() end, log_decision = function() end, audit = function() return {} end,
+}
+local function set_store(s) store = s end
+
+-- Identity resolution (token -> user) is pluggable so it can go over a cosocket
+-- to a networked session store under nginx (see auth.lua / use_auth) while
+-- defaulting to the local store off-nginx. Everything else stays local.
+local auth = { token_user = function(tok) return store.token_user(tok) end }
+local function set_auth(a) auth = a end
+
+-- ---- host services the Shen policy calls (Shen -> Lua) ----------------------
+-- `host` is an INTENTIONAL global: the Shen policy reaches these via
+-- (lua.call "host.xxx" ...), which resolves dotted names against _G. Do not
+-- make it local — that would break the bridge.
+host = {
+  token_user   = function(tok)      return auth.token_user(tok) end,
+  is_admin     = function(tok)      return store.is_admin(tok) end,
+  owner_tenant = function(res)      return store.owner_tenant(res) end,
+  member       = function(u, t)     return store.member(u, t) end,
+  role         = function(u, t, r)  return store.role(u, t, r) end,
+  revoked      = function(u, r)     return store.revoked(u, r) end,
+  content      = function(res)      return store.content(res) end,
+  grant        = function(u, t, r)  return store.grant(u, t, r) end,
+  revoke       = function(u, r)     return store.revoke(u, r) end,
+  create       = function(t, r, c)  return store.create(t, r, c) end,
+  log          = function(u, a, r, d, why) return store.log_decision(u, a, r, d, why) end,
+  audit        = function()         return store.audit() end,
+}
+
+shen.boot{ quiet = true }
+
+shen.eval("(tc +)")
+P.F["load"](APP_DIR .. "/authz.shen")   -- typed core: a type error aborts boot
+shen.eval("(tc -)")
+P.F["load"](APP_DIR .. "/app.shen")     -- policy (Prolog) + router
+
+local route = IO.fn("route")
+
+-- ---- marshaling: cjson value <-> Shen `val` (identical to the guestbook) ----
+local sym = IO.sym
+
+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 or next(v) == nil then
+      local a = {}
+      for i, e in ipairs(v) do a[i] = to_val(e) end
+      return { sym("arr"), a }
+    end
+    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
+
+local function from_val(v)
+  local tag, payload = v[1], v[2]
+  if tag == "s" or tag == "n" or tag == "b" then return payload end
+  if tag == "arr" then
+    if #payload == 0 then return cjson.empty_array end
+    local out = {}
+    for i, e in ipairs(payload) do out[i] = from_val(e) end
+    return out
+  end
+  if tag == "obj" then
+    local o = {}
+    for _, pair in ipairs(payload) do o[pair[1]] = from_val(pair[2]) end
+    return o
+  end
+  return nil
+end
+
+-- ---- request handler (pure given method/path/decoded-body) ------------------
+local function dispatch(method, path, decoded_body)
+  local body = decoded_body and to_val(decoded_body) or nil
+  local resp = route(method, path, body)
+  return resp[1], from_val(resp[2])
+end
+
+local M = { dispatch = dispatch, to_val = to_val, from_val = from_val,
+            use_store = set_store, use_auth = set_auth, 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({ ok = false, 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/openresty-authz/app.shen b/examples/openresty-authz/app.shen
new file mode 100644
index 0000000..cc70b32
--- /dev/null
+++ b/examples/openresty-authz/app.shen
@@ -0,0 +1,201 @@
+\\ app.shen — the multi-tenant authz policy + router (loaded with tc OFF).
+\\
+\\ The POLICY lives here as a Prolog proof chain — deliberately kept inside the
+\\ Datalog fragment (ground facts, no compound terms, safe rules, negation only
+\\ on ground goals), so it terminates and stays decidable without a second
+\\ engine: shen-lua's native soa32 Prolog engine (FFI/int32, JIT-friendly) does
+\\ the reasoning. The leaf facts are read from the durable, event-sourced store
+\\ through `lua.call`, so LMDB / the log file stays the single source of truth.
+\\
+\\ The proof chain mirrors Shen-Backpressure's authorization example:
+\\   token -> authenticated user -> tenant membership -> resource access
+\\
+\\ CONSISTENCY: the identity (User) and tenant (Tenant) are resolved ONCE, in
+\\ Shen, BEFORE the proof, and the same values are passed into the query, the
+\\ [granted ...] witness, and the discharge report. That matters because under
+\\ OpenResty `host-token-user` can go over a cosocket and YIELD — if the witness
+\\ re-derived the user after the proof, another request could change state in
+\\ the yield window and the witness could name a different user than the chain
+\\ proved. Resolving once closes that window. The remaining leaf facts read
+\\ inside the query (membership, role, revocation) are local, non-yielding reads.
+
+\\ -- leaf facts: read the durable store (Shen -> Lua) --------------------------
+(define host-token-user   Tok    -> (lua.call "host.token_user" [Tok]))
+(define host-is-admin?    Tok    -> (lua.call "host.is_admin" [Tok]))
+(define host-owner-tenant R      -> (lua.call "host.owner_tenant" [R]))
+(define host-member?      U T    -> (lua.call "host.member" [U T]))
+(define host-role?        U T Ro -> (lua.call "host.role" [U T Ro]))
+(define host-revoked?     U R    -> (lua.call "host.revoked" [U R]))
+(define host-content      R      -> (lua.call "host.content" [R]))
+(define host-grant        U T Ro -> (lua.call "host.grant" [U T Ro]))
+(define host-revoke       U R    -> (lua.call "host.revoke" [U R]))
+(define host-create       T R C  -> (lua.call "host.create" [T R C]))
+(define host-log      U A R D Wy -> (lua.call "host.log" [U A R D Wy]))
+(define host-audit               -> (lua.call "host.audit" []))
+
+\\ -- the policy, as a Prolog proof chain (Datalog fragment) -------------------
+\\ User/Tenant arrive already resolved (see the CONSISTENCY note above); the rule
+\\ proves the remaining premises. `receive` derefs a logic var to its value so a
+\\ leaf fact can be read from the store inside a guard.
+(defprolog can-read
+  User Tenant R <-- (when (not (= (receive User) "")))
+                    (when (not (= (receive Tenant) "")))
+                    (when (host-member? (receive User) (receive Tenant)))
+                    (when (not (host-revoked? (receive User) (receive R))));)
+
+\\ can-write: all of the above, and the "editor" role in that tenant.
+(defprolog can-write
+  User Tenant R <-- (when (not (= (receive User) "")))
+                    (when (not (= (receive Tenant) "")))
+                    (when (host-member? (receive User) (receive Tenant)))
+                    (when (host-role? (receive User) (receive Tenant) "editor"))
+                    (when (not (host-revoked? (receive User) (receive R))));)
+
+\\ -- discharge reports: WHICH premise failed (for the audit log) --------------
+\\ Only run on a denial, over the SAME resolved User/Tenant the proof used. They
+\\ re-walk the premises to name the first failure; the membership/revocation
+\\ re-reads are local and non-yielding, so they cannot observe a different state
+\\ than the query did within one request.
+(define reason-read
+  User Tenant R -> (if (= User "") "unauthenticated: token does not identify a user"
+                     (if (= Tenant "") "unknown resource"
+                       (if (not (host-member? User Tenant)) (cn "not a member of tenant " Tenant)
+                         (if (host-revoked? User R) "access to this resource was revoked"
+                           "forbidden")))))
+
+(define reason-write
+  User Tenant R -> (if (= User "") "unauthenticated: token does not identify a user"
+                     (if (= Tenant "") "unknown resource"
+                       (if (not (host-member? User Tenant)) (cn "not a member of tenant " Tenant)
+                         (if (not (host-role? User Tenant "editor")) "requires the editor role"
+                           (if (host-revoked? User R) "access to this resource was revoked"
+                             "forbidden"))))))
+
+\\ -- authorize: resolve identity ONCE, run the gate, log, return a witness ----
+\\ Every call appends a decision event to the durable proof log (host-log), so
+\\ the audit trail is itself replayable state, not a side channel.
+(define authorize-read
+  Tok R -> (decide-read (host-token-user Tok) (host-owner-tenant R) R))
+
+(define decide-read
+  User Tenant R -> (if (prolog? (can-read (receive User) (receive Tenant) (receive R)))
+                       (grant User Tenant R "read")
+                       (deny User Tenant R "read" (reason-read User Tenant R))))
+
+(define authorize-write
+  Tok R -> (decide-write (host-token-user Tok) (host-owner-tenant R) R))
+
+(define decide-write
+  User Tenant R -> (if (prolog? (can-write (receive User) (receive Tenant) (receive R)))
+                       (grant User Tenant R "write")
+                       (deny User Tenant R "write" (reason-write User Tenant R))))
+
+(define grant
+  User Tenant R Action -> (do (host-log User Action R "grant" "ok")
+                              [granted User Tenant R]))
+
+(define deny
+  User Tenant R Action Why -> (do (host-log User Action R "deny" Why)
+                                  [denied Why]))
+
+\\ -- request field access -----------------------------------------------------
+(define find-val
+  _ [] -> []
+  K [[K V] | _] -> [V]
+  K [_ | Es] -> (find-val K Es))
+
+(define sfield
+  K Es -> (sfirst (find-val K Es)))
+
+(define sfirst
+  [[s S]] -> S
+  _ -> "")
+
+\\ present? distinguishes an ABSENT key ([]) from one present but empty (""), so
+\\ a write can require its content field rather than silently storing "".
+(define present?
+  K Es -> (not (empty? (find-val K Es))))
+
+\\ -- responses ----------------------------------------------------------------
+(define bad-request
+  Msg -> [400 [obj [["ok" [b false]] ["error" [s Msg]]]]])
+
+(define bad-body
+  -> (bad-request "body: must be a JSON object"))
+
+\\ respond/write-through take a typed `decision`; both status and body come from
+\\ the typed core (decision-status / render-doc), each total over `decision`.
+(define respond
+  [granted User Tenant R] -> [(decision-status [granted User Tenant R])
+                              (render-doc [granted User Tenant R] (host-content R))]
+  [denied Why]            -> [(decision-status [denied Why]) (render-doc [denied Why] "")])
+
+(define do-read
+  [obj Es] -> (respond (authorize-read (sfield "token" Es) (sfield "resource" Es)))
+  _ -> (bad-body))
+
+\\ a granted write requires a content field (missing -> 400, never a silent wipe),
+\\ then mutates the store durably; a denied write touches nothing.
+(define do-write
+  [obj Es] -> (if (present? "content" Es)
+                  (write-through (authorize-write (sfield "token" Es) (sfield "resource" Es))
+                                 (sfield "content" Es))
+                  (bad-request "content: is required"))
+  _ -> (bad-body))
+
+(define write-through
+  [granted User Tenant R] Content -> (do (host-create Tenant R Content)
+                                         [(decision-status [granted User Tenant R])
+                                          (render-doc [granted User Tenant R] Content)])
+  [denied Why] _ -> [(decision-status [denied Why]) (render-doc [denied Why] "")])
+
+\\ -- admin mutations (require an admin token) ---------------------------------
+(define require-admin
+  Tok Body -> (if (host-is-admin? Tok) (Body) (admin-denied)))
+
+(define admin-denied
+  -> [403 [obj [["ok" [b false]] ["error" [s "admin token required"]]]]])
+
+(define ok-obj
+  -> [200 [obj [["ok" [b true]]]]])
+
+(define do-grant
+  [obj Es] -> (require-admin (sfield "token" Es)
+                (freeze (do (host-grant (sfield "user" Es) (sfield "tenant" Es) (sfield "role" Es))
+                            (ok-obj))))
+  _ -> (bad-body))
+
+(define do-revoke
+  [obj Es] -> (require-admin (sfield "token" Es)
+                (freeze (do (host-revoke (sfield "user" Es) (sfield "resource" Es))
+                            (ok-obj))))
+  _ -> (bad-body))
+
+(define do-create
+  [obj Es] -> (require-admin (sfield "token" Es)
+                (freeze (do (host-create (sfield "tenant" Es) (sfield "resource" Es) (sfield "content" Es))
+                            (ok-obj))))
+  _ -> (bad-body))
+
+\\ -- audit: the durable proof log (admin only — it lists users + reasons) -----
+(define logrow->val
+  [Seq U A R D Why] -> [obj [["seq" [n Seq]] ["user" [s U]] ["action" [s A]]
+                             ["resource" [s R]] ["decision" [s D]] ["reason" [s Why]]]]
+  _ -> [obj []])
+
+(define do-audit
+  [obj Es] -> (require-admin (sfield "token" Es)
+                (freeze [200 [obj [["log" [arr (map (function logrow->val) (host-audit))]]]]]))
+  _ -> (bad-body))
+
+\\ -- the router ---------------------------------------------------------------
+\\ Each handler validates its own body shape (an [obj ...] or a 400), so a
+\\ bodyless POST to a real route is a 400, not a 404.
+(define route
+  "POST" "/api/read"          B -> (do-read B)
+  "POST" "/api/write"         B -> (do-write B)
+  "POST" "/api/admin/grant"   B -> (do-grant B)
+  "POST" "/api/admin/revoke"  B -> (do-revoke B)
+  "POST" "/api/admin/create"  B -> (do-create B)
+  "POST" "/api/admin/audit"   B -> (do-audit B)
+  _ _ _ -> [404 [obj [["error" [s "not found"]]]]])
diff --git a/examples/openresty-authz/auth.lua b/examples/openresty-authz/auth.lua
new file mode 100644
index 0000000..aa1ad5f
--- /dev/null
+++ b/examples/openresty-authz/auth.lua
@@ -0,0 +1,98 @@
+-- examples/openresty-authz/auth.lua — resolve a bearer token to a user at the
+-- HEAD of the proof chain.
+--
+-- Whether this touches the network is a TOKEN-FORMAT decision, not a given:
+--
+--   * Signed tokens (JWT/PASETO) — verify LOCALLY: check the signature + exp/
+--     aud/iss. That is CPU (crypto), no per-request I/O; the only network is a
+--     JWKS key fetch, cached for hours. This is the default and the common case
+--     for a stateless authz gate.
+--   * Opaque tokens (session ids / OAuth2 introspection) — must be looked up in
+--     a REMOTE store, so THEN it is network I/O. On a single-threaded nginx
+--     worker a blocking socket would stall the whole worker for the round-trip,
+--     so use a COSOCKET (ngx.socket.tcp, whose connect/send/receive/setkeepalive
+--     yield to the event loop and pool connections) and cache the result.
+--
+-- So the DEFAULT resolver is local (`local_resolver`); `cosocket_resolver` is an
+-- opt-in for the opaque-token case only. Either way, token_user(token) is the
+-- ONE leaf fact the Prolog policy reads for identity — everything downstream
+-- (membership, ownership) stays in the local durable store.
+
+local M = {}
+
+-- ---- minimal Redis RESP GET over a raw cosocket -----------------------------
+-- `GET auth:<token>` -> the username, or "" if the key is absent. This is what
+-- lua-resty-redis does under the hood; spelled out so the cosocket calls that
+-- keep the worker non-blocking are visible: connect, send, receive, and
+-- setkeepalive (which returns the socket to nginx's per-worker pool).
+local function redis_get(cfg, key)
+  local sock = ngx.socket.tcp()
+  sock:settimeout(cfg.timeout_ms or 200)          -- bound the round-trip
+  local ok, err = sock:connect(cfg.host, cfg.port)  -- reuses a pooled conn if any
+  if not ok then return nil, "connect: " .. tostring(err) end
+
+  local req = ("*2\r\n$3\r\nGET\r\n$%d\r\n%s\r\n"):format(#key, key)
+  local _, serr = sock:send(req)
+  if serr then sock:close(); return nil, "send: " .. serr end
+
+  local line, rerr = sock:receive("*l")           -- bulk header: "$<len>" or "$-1"
+  if not line then sock:close(); return nil, "receive: " .. tostring(rerr) end
+
+  local val = ""
+  if line ~= "$-1" then                            -- "$-1" == key missing
+    local n = tonumber(line:sub(2)) or 0
+    val = sock:receive(n) or ""                    -- exactly n bytes of payload
+    sock:receive(2)                                -- swallow the trailing CRLF
+  end
+
+  sock:setkeepalive(cfg.keepalive_ms or 60000, cfg.pool_size or 20)  -- pool, don't close
+  return val
+end
+
+-- ---- resolvers --------------------------------------------------------------
+-- A resolver is just { token_user = function(token) -> user }.
+
+-- DEFAULT resolver: identity verified/looked up locally, no per-request I/O.
+-- In production this is where a JWT signature check lives (lua-resty-jwt);
+-- `token_user_fn` returns the subject. It is also the fallback for the cosocket
+-- resolver when the remote store errors.
+function M.local_resolver(token_user_fn)
+  return { token_user = token_user_fn }
+end
+
+-- OPT-IN resolver, for OPAQUE tokens only (session ids / introspection) whose
+-- store is remote. A short-TTL shared-dict cache sits in front of a Redis lookup
+-- over ngx.socket.tcp, so the common case never touches the socket at all; a
+-- miss does one non-blocking round-trip; any error degrades to the local
+-- fallback rather than failing the request open. Do NOT use this for signed
+-- tokens — verify those locally with M.local_resolver instead.
+--
+-- opts = { redis = {host,port,timeout_ms,keepalive_ms,pool_size},
+--          cache = <ngx.shared dict or nil>, ttl = <seconds>,
+--          fallback = function(token) -> user }
+function M.cosocket_resolver(opts)
+  local cfg, cache = opts.redis, opts.cache
+  local ttl, fallback = opts.ttl or 5, opts.fallback
+  local R = {}
+  function R.token_user(token)
+    if cache then
+      local hit = cache:get(token)
+      if hit ~= nil then return hit end
+    end
+    local user, err = redis_get(cfg, "auth:" .. token)
+    if err then
+      if ngx and ngx.log then ngx.log(ngx.ERR, "auth cosocket: ", err) end
+      -- FAIL CLOSED by default: on a store error, resolve to no identity so the
+      -- proof chain denies. `opts.fallback` is an EXPLICIT opt-in to degrade to
+      -- a local resolver instead — only safe if you accept that a session-store
+      -- outage lets tokens resolve from local (possibly stale) data, which can
+      -- bypass revocations recorded only in the remote store.
+      return fallback and fallback(token) or ""
+    end
+    if cache then cache:set(token, user, ttl) end
+    return user
+  end
+  return R
+end
+
+return M
diff --git a/examples/openresty-authz/authz.shen b/examples/openresty-authz/authz.shen
new file mode 100644
index 0000000..683fd3f
--- /dev/null
+++ b/examples/openresty-authz/authz.shen
@@ -0,0 +1,78 @@
+\\ authz.shen — the TYPED core of the multi-tenant authorization demo.
+\\
+\\ This is the "structure the agent cannot bypass," in the type system. The
+\\ policy itself (who may access what) is the Prolog proof chain in app.shen;
+\\ this file owns the two things that must be provably total:
+\\
+\\   1. `decision` — an authorization verdict. The ONLY way app.shen turns a
+\\      stored document into a response is `render-doc`, and `render-doc` is a
+\\      total function over `decision` that reveals content for NO shape other
+\\      than [granted ...]. So "a document reached the client" implies "a
+\\      granted witness was constructed," checked at load time by Shen's
+\\      sequent-calculus typechecker — the runtime analogue of Shen-Backpressure's
+\\      shengen guard types, honest about the fact that the facts are dynamic.
+\\
+\\   2. `val` — the tagged JSON value space (identical to the guestbook example's
+\\      rules.shen), so app.lua marshals one shape both ways.
+\\
+\\ Loaded under (tc +): a type error here aborts worker startup, before the
+\\ server takes a request.
+
+\\ -- the value space of a decoded JSON body (same tags as the guestbook) ------
+(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;)
+
+\\ -- the authorization verdict ------------------------------------------------
+\\ [granted User Tenant Resource] : the proof chain closed — the request is
+\\   authenticated as User, Resource belongs to Tenant, and User has access.
+\\ [denied Why] : a premise failed; Why is the discharge report (which one).
+(datatype decision
+  U : string; T : string; R : string;
+  ====================================
+  [granted U T R] : decision;
+
+  Why : string;
+  =============
+  [denied Why] : decision;)
+
+\\ -- render-doc: the guarded projection ---------------------------------------
+\\ Total over `decision`. Content is placed in the body for [granted ...] and
+\\ for nothing else, so a document literally cannot be serialized on a denied
+\\ path. This is where the type system does the enforcing.
+(define render-doc
+  {decision --> string --> val}
+  [granted U T R] Content -> [obj [["ok" [b true]]
+                                   ["user" [s U]]
+                                   ["tenant" [s T]]
+                                   ["resource" [s R]]
+                                   ["content" [s Content]]]]
+  [denied Why] _ -> [obj [["ok" [b false]] ["error" [s Why]]]])
+
+\\ HTTP status for a decision — also total, also load-time checked.
+(define decision-status
+  {decision --> number}
+  [granted _ _ _] -> 200
+  [denied _] -> 403)
diff --git a/examples/openresty-authz/nginx.conf b/examples/openresty-authz/nginx.conf
new file mode 100644
index 0000000..e0ca8b8
--- /dev/null
+++ b/examples/openresty-authz/nginx.conf
@@ -0,0 +1,91 @@
+# examples/openresty-authz/nginx.conf — run the Shen authz app under OpenResty.
+#
+#     mkdir -p examples/openresty-authz/logs
+#     openresty -p "$PWD/examples/openresty-authz" -c nginx.conf
+#
+# then drive the JSON API (see README.md). The prefix is this directory, so
+# logs/ resolves here and init_by_lua derives the repo root for package.path.
+
+daemon off;
+worker_processes 1;                 # one worker: one kernel boot, one replay
+pid logs/nginx.pid;
+error_log logs/error.log info;
+
+events { worker_connections 256; }
+
+# --- Production durability: lua-resty-lmdb -----------------------------------
+# If your OpenResty ships the resty.lmdb module (Kong's build does), uncomment
+# these and set backend="lmdb" in init_worker below. The event log then lives
+# in a memory-mapped, MVCC, ACID store instead of a flat file — same interface,
+# same replay-on-boot, zero-copy FFI reads on the hot path.
+#
+# lmdb_environment_path logs/lmdb;
+# lmdb_map_size         64m;
+
+http {
+    access_log logs/access.log;
+
+    types { application/json json; text/plain txt; }
+    default_type application/json;
+
+    # Short-TTL cache in front of the networked identity lookup (see below), so
+    # the common request never touches the socket at all. Shared across workers.
+    lua_shared_dict auth_cache 1m;
+
+    # Put shen-lua (repo root) and this example dir on package.path. The prefix
+    # is .../examples/openresty-authz/, so ../../ is the repo root.
+    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 authz.shen), open the
+    # durable store, replay its log, and seed a demo tenant on first boot only.
+    init_worker_by_lua_block {
+        local app   = require("app")
+        local Store = require("store")
+        local store = Store.new{
+            codec   = app.json,
+            backend = "file",                 -- swap to "lmdb" with the directives above
+            path    = ngx.config.prefix() .. "logs/authz-log.jsonl",
+        }
+        if store.seq() == 0 then              -- fresh log: seed the demo world
+            store.seed_token("tok-admin", "admin", true)
+            store.seed_token("tok-alice", "alice", false)
+            store.seed_token("tok-bob",   "bob",   false)
+            store.seed_token("tok-carol", "carol", false)
+            store.create("acme",   "doc-1", "acme launch plan")
+            store.create("globex", "doc-2", "globex roadmap")
+            store.grant("alice", "acme", "editor")
+            store.grant("bob",   "acme", "viewer")
+        end
+        app.use_store(store)
+
+        -- Identity resolution (token -> user), the head of the proof chain.
+        -- Default: local — the app resolves against the store with no per-request
+        -- I/O. In production this is where a JWT signature check goes (verify the
+        -- token locally, no network on the hot path).
+        --
+        -- ONLY if your tokens are OPAQUE (session ids looked up in a REMOTE
+        -- store) do you need a network hop — and then it must be a cosocket, so
+        -- it never stalls the worker, cached in the shared dict above. Uncomment
+        -- to point at a Redis holding `SET auth:<token> <user>`:
+        --
+        -- local Auth = require("auth")
+        -- app.use_auth(Auth.cosocket_resolver{
+        --     redis    = { host = "127.0.0.1", port = 6379, timeout_ms = 200 },
+        --     cache    = ngx.shared.auth_cache,
+        --     ttl      = 5,
+        --     fallback = store.token_user,   -- degrade to local if Redis is down
+        -- })
+    }
+
+    server {
+        listen 8080;
+
+        # The whole JSON API goes through (route Method Path Body) in Shen.
+        location /api/ {
+            content_by_lua_block { require("app").handle() }
+        }
+    }
+}
diff --git a/examples/openresty-authz/selftest.lua b/examples/openresty-authz/selftest.lua
new file mode 100644
index 0000000..ee9b858
--- /dev/null
+++ b/examples/openresty-authz/selftest.lua
@@ -0,0 +1,213 @@
+-- examples/openresty-authz/selftest.lua — drive the authz app off-nginx.
+--
+--   luajit examples/openresty-authz/selftest.lua      (from the repo root)
+--
+-- Boots the same app.lua the server uses and runs the full multi-tenant policy
+-- through app.dispatch() against BOTH store backends (file + the lua-resty-lmdb
+-- adapter, faked in-process), then a THIRD time with identity resolved over a
+-- cosocket (ngx.socket.tcp, also faked in-process) to a Redis-style session
+-- store. All three must produce an identical, decision-for-decision audit trail
+-- — same policy, different I/O substrates.
+
+local root = arg[0]:match("^(.*)/examples/openresty%-authz/[^/]+$") or "."
+package.path = root .. "/?.lua;" .. root .. "/examples/openresty-authz/?.lua;" .. package.path
+
+local app   = require("app")
+local Store = require("store")
+local Auth  = require("auth")
+local cjson = app.json
+
+-- ---- a faithful in-process fake of lua-resty-lmdb --------------------------
+local function install_fake_lmdb()
+  local kv = {}
+  package.loaded["resty.lmdb"] = { get = function(k) return kv[k] end }
+  package.loaded["resty.lmdb.transaction"] = {
+    begin = function()
+      local buf = {}
+      return {
+        set    = function(_, k, v) buf[#buf + 1] = { k, v }; return true end,
+        commit = function(_) for _, p in ipairs(buf) do kv[p[1]] = p[2] end; return true end,
+      }
+    end,
+  }
+end
+
+-- ---- a faithful in-process fake of ngx.socket.tcp + a Redis-RESP server ------
+-- Speaks exactly the surface auth.lua's redis_get uses: settimeout, connect,
+-- send, receive("*l")/receive(n), setkeepalive. Records how many times a socket
+-- actually connects, so the test can prove the shared-dict cache elides
+-- round-trips.
+local sock_stats
+local function install_fake_cosocket(tokens)
+  local records = {}
+  for tok, user in pairs(tokens) do records["auth:" .. tok] = user end
+  sock_stats = { connects = 0 }
+  _G.ngx = _G.ngx or {}
+  ngx.ERR = ngx.ERR or "err"
+  ngx.log = ngx.log or function() end
+  ngx.socket = { tcp = function()
+    local s = { buf = "" }
+    function s:settimeout() end
+    function s:connect() sock_stats.connects = sock_stats.connects + 1; return 1 end
+    function s:send(req)
+      local key = req:match("(auth:[^\r]+)\r\n$")   -- last bulk string = the key
+      local v = key and records[key]
+      s.buf = v and (("$%d\r\n%s\r\n"):format(#v, v)) or "$-1\r\n"
+      return #req
+    end
+    function s:receive(pat)
+      if pat == "*l" then
+        local l, rest = s.buf:match("^([^\r]*)\r\n(.*)$")
+        s.buf = rest or ""; return l
+      end
+      local d = s.buf:sub(1, pat); s.buf = s.buf:sub(pat + 1); return d
+    end
+    function s:setkeepalive() return 1 end
+    function s:close() return 1 end
+    return s
+  end }
+end
+local function fake_cache()
+  local kv = {}
+  return { get = function(_, k) return kv[k] end, set = function(_, k, v) kv[k] = v end }
+end
+
+-- ---- test harness -----------------------------------------------------------
+local function req(method, path, body) return app.dispatch(method, path, body) end
+
+-- run the whole scenario against one store backend + identity resolver.
+-- make_auth(store) -> resolver, applied on the initial store and again after the
+-- simulated restart. Returns (fail_count, audit_rows).
+local function run_scenario(title, open_store, make_auth)
+  print("\n########## " .. title .. " ##########")
+  local fail = 0
+  local function expect(label, want, method, path, body)
+    local status, resp = req(method, path, body)
+    local note = resp and (resp.error or (resp.ok and resp.content) or "") or ""
+    print(("  %-38s -> %d  %s"):format(label, status, note ~= "" and ("(" .. note .. ")") or ""))
+    if status ~= want then fail = fail + 1; print(("      FAIL: expected %d"):format(want)) end
+    return resp
+  end
+
+  local s = open_store()
+  s.seed_token("tok-admin", "admin", true)
+  s.seed_token("tok-alice", "alice", false)
+  s.seed_token("tok-bob",   "bob",   false)
+  s.seed_token("tok-carol", "carol", false)
+  app.use_store(s); app.use_auth(make_auth(s))
+
+  print("== provision tenants, docs, memberships (admin) ==")
+  expect("create acme/doc-1",   200, "POST", "/api/admin/create",
+         { token = "tok-admin", tenant = "acme",   resource = "doc-1", content = "acme launch plan" })
+  expect("create globex/doc-2", 200, "POST", "/api/admin/create",
+         { token = "tok-admin", tenant = "globex", resource = "doc-2", content = "globex roadmap" })
+  expect("grant alice editor@acme", 200, "POST", "/api/admin/grant",
+         { token = "tok-admin", user = "alice", tenant = "acme", role = "editor" })
+  expect("grant bob viewer@acme",   200, "POST", "/api/admin/grant",
+         { token = "tok-admin", user = "bob",   tenant = "acme", role = "viewer" })
+  expect("non-admin cannot grant",  403, "POST", "/api/admin/grant",
+         { token = "tok-alice", user = "carol", tenant = "acme", role = "editor" })
+
+  print("\n== the proof chain: token -> user -> tenant -> resource ==")
+  expect("alice reads acme doc",     200, "POST", "/api/read", { token = "tok-alice", resource = "doc-1" })
+  expect("bob (viewer) reads acme",  200, "POST", "/api/read", { token = "tok-bob",   resource = "doc-1" })
+  expect("carol (no member) denied", 403, "POST", "/api/read", { token = "tok-carol", resource = "doc-1" })
+  expect("alice denied cross-tenant",403, "POST", "/api/read", { token = "tok-alice", resource = "doc-2" })
+  expect("bad token unauthenticated",403, "POST", "/api/read", { token = "nope",      resource = "doc-1" })
+  expect("unknown resource",         403, "POST", "/api/read", { token = "tok-alice", resource = "doc-404" })
+
+  print("\n== write needs the editor role ==")
+  expect("alice (editor) writes",    200, "POST", "/api/write", { token = "tok-alice", resource = "doc-1", content = "edited by alice" })
+  expect("bob (viewer) cannot write",403, "POST", "/api/write", { token = "tok-bob",   resource = "doc-1", content = "bob was here" })
+
+  print("\n== revocation (a deny that overrides membership) ==")
+  expect("revoke bob's access",      200, "POST", "/api/admin/revoke", { token = "tok-admin", user = "bob", resource = "doc-1" })
+  expect("bob now denied (revoked)", 403, "POST", "/api/read", { token = "tok-bob",   resource = "doc-1" })
+  expect("alice still reads",        200, "POST", "/api/read", { token = "tok-alice", resource = "doc-1" })
+
+  print("\n== request-shape guards ==")
+  expect("write w/o content -> 400", 400, "POST", "/api/write", { token = "tok-alice", resource = "doc-1" })
+  expect("...doc NOT wiped",         200, "POST", "/api/read",  { token = "tok-alice", resource = "doc-1" })
+  expect("bodyless POST -> 400",     400, "POST", "/api/read")
+  expect("audit needs admin -> 403", 403, "POST", "/api/admin/audit", { token = "tok-alice" })
+
+  print("\n== durable execution: simulate a restart (reopen + replay the log) ==")
+  local seq_before = s.seq()
+  local s2 = open_store()             -- brand-new store object, same durable log
+  app.use_store(s2); app.use_auth(make_auth(s2))
+  print(("  replayed %d events into a fresh process"):format(s2.seq()))
+  if s2.seq() ~= seq_before then fail = fail + 1; print("      FAIL: replayed seq mismatch") end
+  expect("alice reads after restart",  200, "POST", "/api/read", { token = "tok-alice", resource = "doc-1" })
+  expect("revocation survived restart",403, "POST", "/api/read", { token = "tok-bob",   resource = "doc-1" })
+
+  local _, audit = req("POST", "/api/admin/audit", { token = "tok-admin" })
+  return fail, (audit and audit.log) or {}
+end
+
+-- ---- backends + resolvers ---------------------------------------------------
+local function file_open()
+  local path = os.tmpname(); os.remove(path)
+  return function() return Store.new{ codec = cjson, backend = "file", path = path } end
+end
+local function lmdb_open()
+  install_fake_lmdb()
+  return function() return Store.new{ codec = cjson, backend = "lmdb" } end
+end
+local function local_auth(s)
+  return Auth.local_resolver(function(t) return s.token_user(t) end)
+end
+local REDIS = { host = "127.0.0.1", port = 6379 }
+local function cosocket_auth(_)
+  -- no fallback: fail closed on a store error (the default recommendation)
+  return Auth.cosocket_resolver{ redis = REDIS, cache = fake_cache(), ttl = 5 }
+end
+
+local fail = 0
+local f_fail, f_audit = run_scenario("file backend, local identity", file_open(), local_auth)
+local l_fail, l_audit = run_scenario("lua-resty-lmdb backend, local identity", lmdb_open(), local_auth)
+fail = f_fail + l_fail
+
+-- ---- cosocket unit check: one round-trip, then cached -----------------------
+print("\n########## cosocket identity resolver (ngx.socket.tcp fake) ##########")
+install_fake_cosocket{ ["tok-admin"]="admin", ["tok-alice"]="alice",
+                       ["tok-bob"]="bob", ["tok-carol"]="carol" }
+do
+  local r = Auth.cosocket_resolver{ redis = REDIS, cache = fake_cache(), ttl = 5 }
+  local function check(label, cond) print("  " .. (cond and "ok  " or "FAIL") .. " " .. label)
+                                     if not cond then fail = fail + 1 end end
+  local u1 = r.token_user("tok-alice"); check("resolves tok-alice -> alice over cosocket", u1 == "alice")
+  check("one connect for the first lookup", sock_stats.connects == 1)
+  local u2 = r.token_user("tok-alice"); check("second lookup served from cache (no reconnect)",
+                                              u2 == "alice" and sock_stats.connects == 1)
+  local u3 = r.token_user("nope");      check("missing key -> '' (Redis $-1 path)",
+                                              u3 == "" and sock_stats.connects == 2)
+end
+
+-- ---- cosocket end-to-end: whole policy with identity over the cosocket ------
+local c_fail, c_audit = run_scenario("file backend, opaque-token identity over a cosocket (opt-in)", file_open(), cosocket_auth)
+fail = fail + c_fail
+
+-- ---- all three substrates must agree, decision for decision -----------------
+print("\n########## backend parity ##########")
+local function audit_key(rows)
+  local t = {}
+  for i, r in ipairs(rows) do
+    t[i] = table.concat({ r.seq, r.user, r.action, r.resource, r.decision, r.reason }, "|")
+  end
+  return table.concat(t, "\n")
+end
+local kf, kl, kc = audit_key(f_audit), audit_key(l_audit), audit_key(c_audit)
+if kf == kl and kl == kc then
+  print(("  OK — identical %d-decision audit trail from file, lmdb, and cosocket runs"):format(#f_audit))
+else
+  fail = fail + 1; print("  FAIL: substrates produced different audit trails")
+end
+
+print("\n== the durable proof log (from the cosocket run) ==")
+for _, row in ipairs(c_audit) do
+  print(("  #%-2d %-6s %-6s %-7s %-6s %s"):format(
+    row.seq, row.user, row.action, row.resource, row.decision, row.reason))
+end
+
+if fail == 0 then print("\nOK — all cases passed (file + lmdb + cosocket)")
+else print(("\n%d case(s) FAILED"):format(fail)); os.exit(1) end
diff --git a/examples/openresty-authz/store.lua b/examples/openresty-authz/store.lua
new file mode 100644
index 0000000..da45e1b
--- /dev/null
+++ b/examples/openresty-authz/store.lua
@@ -0,0 +1,176 @@
+-- examples/openresty-authz/store.lua
+-- Durable, event-sourced fact store + append-only proof log for the authz demo.
+--
+-- The log is the source of truth; the in-memory view is a cache rebuilt by
+-- replaying the log on open. That IS the "durable execution" property: kill the
+-- process, reopen the same log, replay, and you are in the exact same state —
+-- facts AND the audit trail. Nothing lives only in RAM.
+--
+-- Two backends behind one tiny interface (append + iterate):
+--   file : append-only JSONL on disk. Durable across process restarts and the
+--          path exercised by selftest.lua and CI under plain LuaJIT.
+--   lmdb : the same event log in lua-resty-lmdb (the memory-mapped, MVCC,
+--          zero-copy KV that Kong ships). Production path under OpenResty.
+--
+-- LuaJIT perf: reads hit plain hash tables (O(1), trace-friendly); the log
+-- append is off the read/authorize path. Under OpenResty the module loads once
+-- per worker and every authorize is pure table lookups + one Prolog query.
+
+local M = {}
+
+-- ---- the materialized view (derived state) ---------------------------------
+local function new_view()
+  return {
+    tokens    = {},   -- token -> { user=, admin=bool }
+    member    = {},   -- user  -> { tenant -> role }
+    owner     = {},   -- res   -> tenant
+    content   = {},   -- res   -> string
+    revoked   = {},   -- user  -> { res -> true }
+    decisions = {},   -- ordered audit trail: { seq,user,action,resource,decision,reason }
+  }
+end
+
+-- fold one event into the view. Pure; used identically on replay and on append.
+local function apply(view, e)
+  local t = e.t
+  if t == "token" then
+    view.tokens[e.token] = { user = e.user, admin = e.admin == true }
+  elseif t == "grant" then
+    local m = view.member[e.user]; if not m then m = {}; view.member[e.user] = m end
+    m[e.tenant] = e.role or "viewer"
+  elseif t == "create" then
+    view.owner[e.resource]   = e.tenant
+    view.content[e.resource] = e.content or ""
+  elseif t == "revoke" then
+    local r = view.revoked[e.user]; if not r then r = {}; view.revoked[e.user] = r end
+    r[e.resource] = true
+  elseif t == "decision" then
+    view.decisions[#view.decisions + 1] =
+      { e.seq, e.user, e.action, e.resource, e.decision, e.reason }
+  end
+end
+
+-- ---- backends: each(fn) replays stored lines in order; append(line) adds one
+local function file_backend(path)
+  local be = { path = path }
+  function be:each(fn)
+    local f = io.open(self.path, "r")
+    if not f then return end
+    for line in f:lines() do if line ~= "" then fn(line) end end
+    f:close()
+  end
+  function be:append(line)
+    local f = self.fh
+    if not f then f = assert(io.open(self.path, "a")); self.fh = f end
+    -- flush() pushes to the OS, so this is durable across a PROCESS crash, but
+    -- not across power loss (no fsync). Good enough for the demo; a real deploy
+    -- uses the lmdb backend (or an fsync policy) for power-loss durability.
+    f:write(line, "\n"); f:flush()
+  end
+  return be
+end
+
+-- Faithful adapter for lua-resty-lmdb (production, under OpenResty). Kept
+-- deliberately small: the event log is `evt:<n>` with an `evtseq` counter,
+-- written in one ACID transaction. selftest.lua exercises THIS code path
+-- in-process against a faithful fake of resty.lmdb (get + transaction commit);
+-- only the real memory-mapped, MVCC environment needs OpenResty.
+local function lmdb_backend()
+  local lmdb = require("resty.lmdb")
+  local txn  = require("resty.lmdb.transaction")
+  local be = {}
+  function be:each(fn)
+    local n = tonumber(lmdb.get("evtseq")) or 0
+    for i = 1, n do
+      local v = lmdb.get("evt:" .. i)
+      if v then fn(v) end
+    end
+  end
+  function be:append(line)
+    -- NOTE: this reads evtseq OUTSIDE the transaction, so it is NOT safe under
+    -- worker_processes > 1 — two workers can read the same n and one overwrites
+    -- the other's event. Single-worker only as written. To make it multi-worker
+    -- safe, allocate the seq atomically: do the read inside the transaction and
+    -- fail/retry on a version conflict, or use a compare-and-set on evtseq.
+    local n = (tonumber(lmdb.get("evtseq")) or 0) + 1
+    local t = txn.begin()
+    t:set("evt:" .. n, line)
+    t:set("evtseq", tostring(n))
+    local ok, err = t:commit()
+    if not ok then error("lmdb commit failed: " .. tostring(err)) end
+  end
+  return be
+end
+
+-- ---- the store --------------------------------------------------------------
+-- opts = { codec = <cjson-like {encode,decode}>, backend = "file"|"lmdb",
+--          path = <file backend log path> }
+function M.new(opts)
+  opts = opts or {}
+  local codec = assert(opts.codec, "store.new: a JSON codec is required")
+  local backend = (opts.backend == "lmdb") and lmdb_backend()
+                  or file_backend(opts.path or "authz-log.jsonl")
+
+  local view = new_view()
+  local seq  = 0
+
+  -- replay the durable log into the view (this is the crash-recovery path)
+  backend:each(function(line)
+    local e = codec.decode(line)
+    if type(e) == "table" then seq = math.max(seq, e.seq or 0); apply(view, e) end
+  end)
+
+  local S = {}
+
+  -- append: stamp a monotonic seq, persist, THEN apply. If the process dies
+  -- mid-call, either the line is on disk (replayed next open) or it is not
+  -- (never happened) — no torn state, because the view is only ever rebuilt
+  -- from what the backend actually stored.
+  local function append(e)
+    seq = seq + 1
+    e.seq = seq
+    backend:append(codec.encode(e))
+    apply(view, e)
+    return seq
+  end
+
+  -- facts (Shen reads these through host.* via lua.call; all return plain
+  -- strings/booleans so the marshaler stays on the fast path)
+  function S.token_user(token)  local x = view.tokens[token]; return x and x.user or "" end
+  function S.is_admin(token)    local x = view.tokens[token]; return x ~= nil and x.admin == true end
+  function S.owner_tenant(res)  return view.owner[res] or "" end
+  function S.member(user, tenant)
+    local m = view.member[user]; return m ~= nil and m[tenant] ~= nil
+  end
+  function S.role(user, tenant, role)
+    local m = view.member[user]; return m ~= nil and m[tenant] == role
+  end
+  function S.revoked(user, res)
+    local r = view.revoked[user]; return r ~= nil and r[res] == true
+  end
+  function S.content(res) return view.content[res] or "" end
+
+  -- mutations (durable)
+  function S.seed_token(token, user, admin) return append{ t="token", token=token, user=user, admin=admin } end
+  function S.grant(user, tenant, role)      return append{ t="grant", user=user, tenant=tenant, role=role } end
+  function S.revoke(user, res)              return append{ t="revoke", user=user, resource=res } end
+  function S.create(tenant, res, content)   return append{ t="create", tenant=tenant, resource=res, content=content } end
+
+  -- the proof log: every authorize decision is a durable event
+  function S.log_decision(user, action, res, decision, reason)
+    return append{ t="decision", user=user, action=action, resource=res,
+                   decision=decision, reason=reason }
+  end
+
+  -- audit trail as a Lua array of rows, for POST /api/admin/audit
+  function S.audit()
+    local out = {}
+    for i, d in ipairs(view.decisions) do out[i] = d end
+    return out
+  end
+
+  S.seq = function() return seq end
+  return S
+end
+
+return M