feat(prover): add standalone policy boundary checker

[johnnygreco]

Summary

This PR adds a standalone policy boundary checker. It does not install, store, or enforce a managed gateway boundary. openshell-prover check proves whether Allowed(candidate) ⊆ Allowed(boundary) for the supported policy model and returns containment evidence, a counterexample, or an explicit unsupported/inconclusive result. The check runs locally against two fully composed policy files and does not contact a gateway.

flowchart LR
    boundary[Operator boundary policy] --> check[openshell-prover check]
    candidate[Fully composed candidate policy] --> check
    check --> within[within_boundary<br/>exit 0]
    check --> exceeds[exceeds_boundary + counterexample<br/>exit 1]
    check --> incomplete[unsupported or inconclusive + reason code<br/>exit 3 or 130]

Loading

Rust callers can use the containment engine without invoking the CLI:

use openshell_prover::containment::{
    check_within_boundary, parse_policy_str, CheckOptions,
};
use std::time::Duration;

let boundary = parse_policy_str(&boundary_yaml)?;
let candidate = parse_policy_str(&candidate_yaml)?;

let result = check_within_boundary(
    &boundary,
    &candidate,
    CheckOptions {
        timeout: Duration::from_secs(10),
    },
);

Related Issue

Part of #2109. This PR provides the reusable containment engine and standalone CLI. Gateway boundary storage, enforcement, and permission modes remain separate work, so the issue should stay open.

Changes

• Add reusable boundary checks for filesystem, L4 network, and enforced REST authority, including explicit REST denies and executable/ancestor identities.
• Add openshell-prover check candidate.yaml --boundary boundary.yaml with text and JSON output, stable exit and reason codes, bounded inputs, solver timeouts, resource limits, and Unix cancellation. No other prover subcommands are added.
• Return the definitive results within_boundary and exceeds_boundary; unsupported policy shapes and checks requiring unavailable runtime context continue to fail closed.
• Localize fail-closed validation by policy surface: common policy, filesystem, shared network selectors, L4, REST, GraphQL extensions, JSON-RPC extensions, MCP extensions, credentials, and cross-protocol overlap. The top-level gate now owns only deterministic ordering and diagnostic framing.
• Match runtime policy semantics for path globs, underscore-containing hosts, ASCII wildcard selectors over Unicode runtime values, filesystem resolution, and binary identity.
• Validate and replay decoded solver witnesses against candidate && !boundary before returning counterexamples. Reject invalid inputs such as embedded NULs without panicking.
• Keep exact filesystem comparison conservative: equal paths and root coverage are supported, while non-identical paths such as boundary /tmp and candidate /tmp/johnny return unsupported. Symlinks, bind mounts, and aliases mean lexical ancestry alone is not sound without target-filesystem evidence; that evidence contract is separate future work.
• Keep the result schema focused on scope (model_version, policy_version, and modeled domains), result, optional counterexample, and optional reason_code/reason fields. The removed assumptions field is not part of the contract.
• Add unit, runtime-parity, differential, fixture, and process tests covering containment, per-surface fail-closed validation, filesystem limitations, Unicode and underscore hosts, witness decoding, invalid input, timeouts, limits, and SIGINT behavior.
• Distribute openshell-prover through the existing OpenShell installation paths: Debian, an RPM subpackage installed alongside the CLI and gateway, and the Homebrew formula resource. Continue publishing standalone Linux x86_64/aarch64 and macOS Apple Silicon archives with a dedicated SHA-256 manifest.
• Add release and packaging smoke coverage for the installed binary, RPM selection, Debian staging, Homebrew formula generation, target linkage, and real boundary checks.
• Document installation, effective-policy export, copyable contained and exceeding examples, output fields, exit codes, the supported model, release assets, macOS support, and the filesystem limitation.

Testing

• mise run pre-commit
• mise run test
• mise run ci
• cargo test --locked -p openshell-prover -p openshell-prover-cli
• Manual CLI checks for --boundary, within_boundary, exceeds_boundary, JSON evidence, exit codes, and rejection of removed --maximum
• Hosted checks on final commit f778053, including Branch Checks on Linux x86_64, Linux aarch64, and macOS Apple Silicon; Windows MSVC; Helm; docs preview; DCO; dependency review; Trivy; and workflow security

Release workflows build and smoke-test native artifacts. They were not dispatched locally across every release target; Actionlint, the full local CI suite, and focused packaging tests validate their definitions and integration.

Checklist

• Follows Conventional Commits
• Commits are signed off (DCO)
• Architecture and published documentation updated

[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.

[github-actions]

🌿 Preview your docs: https://nvidia-preview-pr-3289.docs.buildwithfern.com/openshell

[pimlock]

/ok to test a86633f

[johnnygreco]

/ok to test fd2880f

[johnnygreco]

/ok to test 5764a6b

[johnnygreco]

/ok to test ae699e1

[johnnygreco]

/ok

[johnnygreco]

/ok to test 1fe1f95

[johnnygreco]

/ok to test 5797c58

[johnnygreco]

/ok to test f778053

[johnnygreco]

/ok to test d25d027