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

[pyrex41]

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 8 (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

[pyrex41]

✅ Full ./scripts/gates.sh run on this branch — all gates green (verbatim):

[Gate 0: shengen-codegen] PASS
[Gate 1: fmt + clippy] PASS
[Gate 2: build] PASS
[Gate 3: test] PASS
[Gate 4: shen-check] PASS
[Gate 5: tcb-audit] PASS
[Gate 6: kernel-aot-audit] PASS
[Gate 7: kernel-tests] PASS   (passed: 134, failed: 0)
[Gate 8: cedar-equiv] PASS    (equiv 12/12 agree; reaches_equiv 49/49 agree)
ALL GATES GREEN

Resolves the caveat in the PR description — the full suite (not just the new gate) passes end-to-end.

[pyrex41]

Superseded by #5 — rebased onto current main (conflict in scripts/gates.sh resolved; cedar gate renumbered to Gate 10). Same changes, mergeable.