shen.typecheck triple-read fix + proof-carrying requests example

[pyrex41]

Summary

This PR does two related things:

• Fixes the embedding helper shen.typecheck so host code can correctly check an expression against compound Shen type syntax like (may alice read doc1).
• Adds examples/pcr/, a proof-carrying-request gateway: clients present proof terms, OpenResty checks them against (may subject action resource), and live facts are consulted at proof-check time.

shen.typecheck Fix

The old helper read the expression and type independently. That breaks for 3+-ary user datatype types because read-from-string cooks expression position differently: standalone (may alice read doc1) is read as curried application syntax, so checks against that type silently returned false.

The helper now reads "EXPR : TYPE" as one triple, matching the shape Shen's loader consumes, validates that exactly one expression and one type were provided, and still resets shen.*infs* per call so shen.*maxinferences* is a per-check budget.

Proof-Carrying Requests

examples/pcr/ demonstrates runtime authorization as proof checking:

• A request carries X-Proof.
• The gate constructs (may subject action resource) from the request.
• Shen checks the presented proof term; it never searches for one.
• Fact leaves like [fact owns alice doc1] are discharged through a typed Lua bridge into a versioned live fact store.
• Grant/revoke changes affect the same proof bytes on the next check, across workers sharing the lua_shared_dict fact blob.
• Allowed requests log the proof, fact-store version, inference count, and consumed fact leaves as an audit trail.

The example covers owner/member/delegation proofs, TTL facts, replica-mode staleness denial, and a bounded hostile-input posture.

Review Fixes Included

Two review findings are fixed in the latest branch commit:

• External atoms are now lowercase-starting only, so admitted S/A/R-style atoms cannot be read as Shen type variables in the constructed judgment. Regression tests first admit uppercase atoms into the fact world and then assert subject/action/resource/proof-token paths still deny.
• Fact-store writes now propagate ngx.shared.DICT:set failures through grant/revoke and the admin endpoints. A failed write returns non-200 JSON and leaves the previous fact world in force; tests simulate failed revoke/grant and recovery.

The branch also merged origin/main and resolved the .gitignore overlap by keeping the generalized examples/*/logs/ and nginx temp-dir patterns.

Verification

• luajit examples/pcr/selftest.lua
• SHEN_TYPECHECK_NATIVE=off luajit examples/pcr/selftest.lua
• luajit test/typecheck_api_spec.lua
• make test -> 471 pass, 0 fail

PR branch is currently mergeable.

[pyrex41]

Pushed the second act: dynamic facts + revocation (PCR-Live).

Facts are no longer axioms — one side-condition rule discharges self-describing fact leaves ([fact owns alice doc1]) against a versioned live store at proof-check time. Revoke a fact and the identical proof bytes 403 on the next request on every worker (verified: 30 concurrent requests across 2 workers, zero grace); alice's unrelated proof keeps passing. TTL facts expire with no revoke call. Replica mode hard-caps staleness at 3W by failing closed. The audit line now names the fact-world version and the exact leaves consumed, making logged decisions offline-replayable.

Design chosen by an ultracode probe/design/critique workflow: live side-condition queries beat epoch datatype reloading (measured compiler wall + permanent per-reload leak) and HMAC fact tokens (every gate becomes a minting oracle). Key empirical facts: neither engine memoizes derivations (revocation is zero-staleness at the checker), side-condition rules translate natively with CPS-identical verdicts+infs, and the typed lua.function bridge is mandatory for that parity. Selftest covers the revocation window, staleness cap, predicate-allowlist, intern-DoS (10k hostile atoms, zero heap growth), and an engine-parity leg with byte-identical output.

[pyrex41]

Review findings from local review:

1. Blocking: admitted uppercase atoms still turn exact judgments into variables.

In examples/pcr/app.lua, atom_ok permits uppercase identifiers, and if those atoms are admitted through the fact world, Shen reads S, A, R, etc. as type variables in the constructed (may subject action resource) judgment. I reproduced this on the PR branch by granting uppercase atoms, after which Alice's proof authorized S write doc1, alice write R, and alice A doc1.

External atoms need to be encoded or restricted so they cannot parse as Shen variables, with regression tests for admitted uppercase subject/action/resource atoms.

2. Blocking: fact-store writes can silently fail while admin grant/revoke reports success.

In examples/pcr/facts.lua, ngx.shared.DICT:set returns failure information, but write() ignores the result and still returns the bumped version. If a revoke write fails under shared-dict pressure, the old blob remains and the proof can continue authorizing even though /admin/revoke returned {ok=true}.

Please propagate write failures from blob_set/write through grant, revoke, and start_sync_timer, and return a non-200 admin response when persistence fails.

Also noted: PR 33 is currently marked conflicting against main; git merge-tree HEAD origin/main shows the conflict in .gitignore.

Verification run locally:

• luajit examples/pcr/selftest.lua
• SHEN_TYPECHECK_NATIVE=off luajit examples/pcr/selftest.lua
• luajit test/typecheck_api_spec.lua
• make test (471 pass, 0 fail)

[pyrex41]

Both blocking findings fixed in 80f4e3c, each with regression tests, plus the merge conflict resolved:

1. Uppercase atoms → type variables (the wildcard-judgment exploit). Atoms are now lowercase-leading (^[a-z][a-z0-9-._]*$) at all three layers — the request gate, the proof-token admit, and the factq guard itself — so an uppercase atom cannot reach the judgment, the proof, or a store lookup even when smuggled directly into the fact world. Regression tests grant S/A/R into the store via facts.grant (bypassing the app layer, reproducing your repro) and assert uppercase subject, action, resource, and proof-atom paths all deny.

2. Silent fact-store write failures. blob_set now propagates the ngx.shared:set result through write → grant/revoke/seed and the sync timer; admin endpoints return 507 with the reason on persistence failure. Tests simulate write failure and assert the failed revoke keeps the grant effective and reports failure, the failed grant stays absent, the fact version never advances on a failed write, and both recover.

3. Merge conflict: merged origin/main (welcoming the new openresty-authz example); .gitignore resolved in favor of the generalized examples/*/logs/ + nginx temp-dir patterns, which subsume the per-example entries.

Verification: selftest green under both engines with byte-identical verdicts and inference counts (the parity leg), make test 471/471.

[pyrex41]

Addressed the two findings from my own detailed re-review (5eefbf8), each with a regression test:

A — mutate could silently reset the fact world on a corrupt blob. snapshot() denies reads on an undecodable blob, but mutate fell back to an empty {version=0} and rewrote version 1 — wiping every fact and rewinding the monotonic version the audit trail depends on. Now decode_blob distinguishes an absent blob (fine — first write) from a present-but-undecodable one (refused, surfaced as 507 at the admin API). Test corrupts the blob and asserts reads deny and a grant refuses rather than resetting.

B — the intern-DoS budget conflated hostile and legitimate atoms. The per-worker monotone seen-set capped at 4096 never bounded the attacker (fact-world membership already does — novel atoms are rejected before read-from-string) but false-denied legitimate atoms once a worker had handled >4096 distinct principals. admit is now stateless — atom_ok and (static or in the current fact world). A principal with no current facts denies at the gate; to keep the honest type-layer reason for the demo's money shot, carol is seeded a benign same-tenant membership, so revoking her delegation denies with "proof does not establish" (not "unknown subject"). Regression asserts that reason survives revocation.

Minor: the inference-count header is gated behind PCR_DEBUG_HEADERS (with an env directive so it works under OpenResty); X-Facts-Version stays as the legitimate consistency token. The write-failure test hook is consolidated under facts._test with the new corrupt-blob/clear injectors, clearly not-public-API.

Verification: selftest green under both engines, byte-identical verdicts and inference counts; make test 471/471; live demo unchanged (the honest revocation reason is preserved). Both findings also written up in the Garmr implementation note as productionization traps (the LRU-grace-set caveat for B, the read/write-must-agree invariant for A).