examples: typed-kernel trio (configc, policy, crdt)#30
Merged
Conversation
Three OpenResty-style examples, each extracting a correctness-critical kernel into one typed, portable Shen file that runs across tiers and climbs the same assurance ladder: types make illegal states unrepresentable (tc+), laws/rules are checked by execution, and the sharpest properties are proved by Shen's sequent-calculus type checker. - configc/: a typed config compiler. compile-config returns EITHER validation errors OR generated artifacts (k8s Deployment + nginx block), never both. Generators are typed over the config's `val` shape; configc_broken.shen shows a generator type-bug rejected at load. CLI (configc.lua) + web preview. - policy/: a typed authorization gateway. decide() returns allow/deny with a reason, enforced as an access_by_lua edge gate and shown in a live explorer. policy_proof.shen frames authz as type inhabitation: a permission is a proof term of type (may S A R); a denied request is an uninhabited type. - crdt/: a CRDT sync hub. crdt.shen is a portable typed kernel (G-Counter, LWW-Register, LWW-Map) whose join-semilattice merge laws are checked by execution; crdt_laws.shen has the type checker verify UNIVERSAL proofs of the laws (incl. absorption) and reject bogus ones. Replicas converge regardless of sync order (selftest) with an OpenResty two-replica web demo. Each runs off-nginx with no deps (luajit examples/<dir>/selftest.lua or configc.lua) and under OpenResty on ports 8090/8091/8092. examples/README.md updated with the trio. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Fixes seven findings from an adversarial review (all verified): - crdt: gc-merge now dedup-canonicalizes (fold via gc-absorb; gc-get takes the max over duplicate keys) and the LWW tiebreak is total over (ts, id, value). The semilattice laws now hold for EVERY typed value, not only well-formed states — previously [gc [["a" 1]["a" 3]]] and two registers colliding on (ts,id) with different values broke commutativity. selftest adds those exact adversarial cases. - policy: by-owner now requires (same-tenant S R), so policy_proof.shen matches decide() in policy.shen — tenant isolation is absolute for owners too. - crdt/policy web pages: escape all interpolated field names, replica ids, and the decision reason (were injected via innerHTML -> stored/reflected XSS). - configc: emitted k8s Deployment now includes template.metadata.labels matching spec.selector.matchLabels (was an invalid manifest); an empty JSON object POSTs as [obj []] so it yields field errors, not "must be an object". All four example selftests pass; the broken-generator rejection still holds. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Three OpenResty-style examples that build on the pattern in
examples/openresty/: extract a correctness-critical kernel into one typed, portable Shen file that runs across tiers, and climb the same assurance ladder — types make illegal states unrepresentable (tc +), laws/rules are checked by execution, and the sharpest properties are proved by Shen's sequent-calculus type checker.What's here
configc/— typed config compiler.compile-configreturns either validation errors or generated artifacts (a k8sDeployment+ an nginx server block), never half of each. Generators are typed over the config'svalshape;configc_broken.shenplants one generator type-bug (cn "listen " PortwithPortnumeric) that is rejected at load. CLI (configc.lua) + live web preview.policy/— typed authorization gateway.decide()returns allow/deny with the reason, enforced as anaccess_by_luaedge gate and shown in a live explorer.policy_proof.shenframes authz as type inhabitation: a permission is a proof term of type(may S A R), and a denied request is an uninhabited type — "deny by default" you can't forget to write.crdt/— CRDT sync hub.crdt.shenis a portable typed kernel (G-Counter, LWW-Register, LWW-Map) whose join-semilattice merge laws are checked by execution.crdt_laws.shenhas the type checker verify universal proofs of the laws (incl. absorption) and reject bogus ones. Replicas converge regardless of sync order.The through-line
crdt_laws.shen/policy_proof.shendemonstrate that Shen's sequent calculus is a working proof checker for universally-quantified properties: valid proofs typecheck, bogus proofs are type errors. The READMEs state the honest scope — the axioms are assumed of the executable code (property checks certify that), and the trade vs Coq/Agda is trust + automation + totality, not expressiveness.Running
Each runs off-nginx with no deps, and under OpenResty (ports 8090/8091/8092):
All four example selftests (incl. the existing
openresty/) pass.examples/README.mdupdated with the trio.🤖 Generated with Claude Code