feat(policy): spike policy envelope and narrowness prover

[zredlined]

Summary

Spike Z3-backed policy-envelope checks in openshell-prover for two related use cases:

• maximum-policy containment: prove whether a candidate policy allows any modeled action outside a security-approved maximum policy;
• narrowness budgets: prove whether a candidate grant adds reach over the current policy, then score the modeled delta so exact grants can fit a small budget while broad globs, L7-to-L4 broadening, or credential-sensitive reach can trigger review.

This PR is draft / not merge-ready. It exists to make the spike branch, walkthrough, test evidence, and review feedback easy to share while we continue evaluating the production shape. The latest local review revisions have not been pushed yet; they are pending human review.

Related Issue

Related #1840

Recommendation

The spike supports the core thesis: the OpenShell policy prover can be used successfully for both maximum-policy envelope checks and narrowness-budget checks on the modeled OpenShell policy surface. The formal queries line up cleanly with the security/policy intent, and no major gap was identified between that intent and what we can express with Z3 for the modeled L4, REST, and WebSocket layers.

Remaining production gaps are explicit and fail closed rather than silently approved. They are engineering follow-ons to widen the modeled policy surface, not blockers to the underlying prover approach.

Changes

• Added envelope::check_within_maximum for maximum-policy containment.
• Added envelope::check_narrowness for candidate-policy deltas against the current policy.
• Modeled symbolic binary, host, port, layer, method, and path action variables in Z3.
• Modeled L4, REST, and WebSocket action layers:
  • L4 covers raw host/port reach plus REST/WebSocket actions on that host/port.
  • REST and WebSocket cover their own inspected layers only.
  • REST/WebSocket maximums do not silently cover raw L4 candidates.
• Compiled modeled host/path/binary globs into Z3 regex constraints.
• Added a coarse spike budget model for exact grants, wildcard grants, recursive-glob grants, and L7-to-L4 broadening.
• Added a separate credentialed-L4 check that asks whether raw L4 reach overlaps credential target hosts.
• Kept credential rewrite flags, deny rules, query constraints, GraphQL, MCP, CIDR/allowed_ips, and other unmodeled surfaces fail-closed.
• Added a tracked spike walkthrough at crates/openshell-prover/MAXIMUM_POLICY_ENVELOPE_SPIKE.md.

Production Gaps

These surfaces currently return Unsupported or remain explicit follow-ons before production auto-approval relies on them:

• deny-rule precedence and allow-minus-deny semantics;
• query-parameter constraints;
• GraphQL operations, fields, persisted queries, and body-size controls;
• MCP server/tool/resource controls;
• CIDR and allowed_ips endpoint scoping;
• credential rewrite authority checks;
• endpoint path scoping, TLS-mode semantics, and additional endpoint behavior flags;
• production configuration for budget scores, thresholds, and credentialed-L4 handling.

Review Notes

Principal review found several important tightening points, all incorporated in the local review state:

• WebSocket read-only should not imply WEBSOCKET_TEXT send authority.
• Credential rewrite flags should fail closed until modeled as a separate authority check.
• Exact L4 grants are common and should score like other exact grants unless they broaden an existing inspected L7 surface.
• L7-to-L4 broadening should be high-cost because it replaces method/path reasoning with raw host/port authority.
• Credentialed raw L4 should remain a separate high-signal check that production policy can combine with the narrowness budget.
• Complex external blueprint policies are useful as manual smoke tests but should not be committed as brittle test fixtures.

Testing

Latest local review state:

• mise exec -- cargo test -p openshell-prover (64 tests)
• mise run pre-commit
• Principal reviewer run before push
• Unit tests added/updated
• E2E tests added/updated (not applicable for this prover spike)

Earlier pushed draft state may differ until the final reviewed local changes are pushed.

Checklist

• Follows Conventional Commits
• Commits are signed off (DCO)

[copy-pr-bot]

This pull request requires additional validation before any workflows can run on NVIDIA's runners.

Pull request vetters can view their responsibilities here.

Contributors can view more details about this message here.