diff --git a/README.md b/README.md index e08d986..7e7f0aa 100644 --- a/README.md +++ b/README.md @@ -270,7 +270,12 @@ browser. One `rules.shen`, two runtimes, no client/server drift. See its | [`examples/hello_embed.lua`](examples/hello_embed.lua) | the smallest useful embedding: boot, define a typed function, call it both ways (~25 lines) | | [`examples/family.shen`](examples/family.shen) | Shen Prolog in twenty lines: facts, rules, queries via `bin/shen` | | [`examples/config_check.lua`](examples/config_check.lua) | the showcase: Shen datatypes + rules as a **typed validation layer** for nested Lua config tables — the typechecker rejects buggy rules at load time ([walkthrough](examples/README.md)) | +| [`examples/configc/`](examples/configc/) | a typed **config compiler**: one config validates *and* generates a Kubernetes Deployment + nginx server block; a generator type-bug is caught at load ([README](examples/configc/README.md)) | +| [`examples/policy/`](examples/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 ([README](examples/policy/README.md)) | +| [`examples/crdt/`](examples/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 ([README](examples/crdt/README.md)) | +| [`examples/pcr/`](examples/pcr/) | **proof-carrying requests over live facts**: the client carries a proof term, the OpenResty gate *checks* it — never searches — against a versioned fact store consulted at proof time, so revoking one fact makes the same proof bytes fail on the next request while delegation chains stay composable and every allow logs its justification ([README](examples/pcr/README.md)) | | [`examples/openresty/`](examples/openresty/) | a **complete web app in Shen on OpenResty** (nginx + LuaJIT): typed request validators + a Shen router behind a JSON API, with a front end that runs the **same** typed rules in the browser — Ratatoskr-shaken and ShenScript-compiled to a ~140 KB module. One `rules.shen`, validated client- and server-side. Runs standalone (`luajit examples/openresty/selftest.lua`) or under `openresty` ([README](examples/openresty/README.md)) | +| [`examples/openresty-authz/`](examples/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 ([README](examples/openresty-authz/README.md)) | ## Certification / Testing diff --git a/examples/pcr/README.md b/examples/pcr/README.md index 3379c34..6b3da7b 100644 --- a/examples/pcr/README.md +++ b/examples/pcr/README.md @@ -94,8 +94,11 @@ All fact state lives in **one atomically-written blob** — `{version, synced_at, facts}` in a single `lua_shared_dict` value — decoded into a per-worker snapshot revalidated on every request (one shm get; decode only on change). One blob means one epoch: a check can never mix two fact -worlds, an evicted or undecodable blob is a **deny**, and `synced_at` -travels inside the blob so freshness can never be stamped by a failed sync. +worlds, an evicted or undecodable blob is a **deny** on the read side and a +**refused write** on the mutate side (a grant/revoke over an undecodable blob +returns an error rather than silently resetting the fact world and rewinding +the version), and `synced_at` travels inside the blob so freshness can never +be stamped by a failed sync. * **Demo (authoritative mode):** `/admin` writes the blob synchronously — staleness is structurally zero; the next check anywhere sees the new @@ -160,5 +163,5 @@ belongs, presented by the client). | `rules.shen` | the logic: ONE live-fact rule + grant rules (owner, member-read, delegation) | | `facts.lua` | the versioned fact store: atomic epoch blob, snapshot, TTL facts, the guard, replica-pull stub | | `app.lua` | the gateway: pre-intern gates, judgment construction, the check, admin endpoints, the audit line | -| `selftest.lua` | allow/deny/revocation-window/TTL/staleness/hostile-input/intern cases + timing, off-nginx | +| `selftest.lua` | allow/deny/revocation-window/TTL/staleness/hostile-input/write-failure/corrupt-blob/intern cases + engine-parity + timing, off-nginx | | `nginx.conf` | two workers sharing one fact blob; the curl walkthrough |