Codegen-equivalence gate: prove generated Cedar decides like the spec

[pyrex41]

Supersedes #1. Same changes, rebased onto current main. The only conflict was in scripts/gates.sh: main added kernel-test gates 8 and 9 after #1 was cut, so the cedar equivalence check is now wired in as Gate 10 (not Gate 8). All of main's existing gates are kept intact. The four other files apply verbatim. Verification below re-run and reproduced on the rebased branch.

---

What

Adds a native, shen-derive-style codegen-equivalence gate to examples/shen-cedar-authz, plus a Prolog/functional differential check, wired into the backpressure gate suite.

Why

generate.rs renders Cedar from spec/authz.shen and strict-validates the shape of the result against the schema. It never checks that the generated PolicySet decides the same way as the spec it came from. Schema validation catches an ill-typed policy; it does not catch a closure bug, a rendering bug, or a hand-edit that quietly drops a permit. The only prior safeguard was the convention "never hand-edit the generated Cedar." This turns that convention into a red/green gate.

Changes

• examples/shen-cedar-authz/examples/equiv.rs — loads spec/authz.shen into the served VM as the oracle (expand-all), renders the Cedar target, and asserts they agree on every request over a finite grid (one user per role × resources incl. an ungranted io). Exit 1 on any divergence; --inject-drift drops one permit to prove it catches drift. Generic over narrow Oracle/Target traits (ShenSpecOracle × CedarTarget); the seam is documented so a future SBCL oracle or shengen→Rust target can drop in.
• examples/shen-cedar-authz/examples/reaches_equiv.rs — the same VM runs role reachability two ways: functional reaches (defun, ported from verify.rs) and a real defprolog prolog-reaches, both built from one edge table and differentially checked over all role pairs.
• scripts/shen-cedar-equiv.sh + sb.toml + scripts/gates.sh — wired as Gate 10 (cedar-equiv).

Verification

All run locally, real exit codes:

cargo run -p shen-cedar-authz --example equiv                  → 12/12 agree, exit 0
cargo run -p shen-cedar-authz --example equiv -- --inject-drift → dana(Admin)·logs DIVERGENCE, exit 1
cargo run -p shen-cedar-authz --example reaches_equiv          → 49 pairs agree, exit 0
bash scripts/shen-cedar-equiv.sh                               → RESULT: PASS, exit 0
cargo fmt --all -- --check                                     → clean
cargo clippy -p shen-cedar-authz --all-targets -- -D warnings  → clean

Note: the new gate and fmt/clippy on the touched crate are verified; the full ./scripts/gates.sh (kernel tests etc.) was not re-run end-to-end in this change.

🤖 Generated with Claude Code