Add Actor egress policy Alloy model

[Frederick F. Kautz IV (fkautz)]

Summary

• add a bounded Alloy model for the Actor Egress Policy proposal
• check policy selection, credential scope, protected destinations, overlapping rule effects, stale policy state, and required extensions
• document how to run, interpret, and extend the model

Why

The model provides a repeatable way to validate policy invariants, find counterexamples, and detect semantic regressions as the design evolves. It is a review artifact, not an implementation specification.

Validation

• Alloy Analyzer 6.2.0 model execution
• git diff --check origin/main...HEAD
• verified expected counterexamples and assertions as documented in the companion guide