examples: typed-kernel trio (configc, policy, crdt)

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

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

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

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