feat(prover): add standalone policy maximum checker

[johnnygreco]

Summary

This PR adds the maximum-policy checking function and the standalone openshell-prover check CLI. It proves whether Allowed(candidate) ⊆ Allowed(maximum) 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; it does not contact a gateway, store a maximum policy, or enforce approval modes.

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

Loading

Related Issue

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

Changes

• Add reusable maximum-boundary checks for filesystem, L4 network, and enforced REST authority, including explicit REST denies and executable/ancestor identities.
• Match runtime policy semantics for path globs, underscore-containing hosts, ASCII wildcard selectors over Unicode runtime values, filesystem resolution, and binary identity. Cases that require unavailable runtime context fail closed as unsupported or inconclusive instead of being guessed.
• Validate and replay decoded solver witnesses against candidate && !maximum before returning counterexamples. Reject invalid inputs such as embedded NULs without panicking.
• Add the standalone openshell-prover check candidate.yaml --maximum maximum.yaml command with text and JSON output, stable exit codes and reason codes, bounded inputs, solver timeouts, resource limits, and Unix cancellation. No other prover subcommands are added.
• 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 filesystem and network containment, symlinks, path globs, Unicode and underscore hosts, witness decoding, invalid input, timeouts, limits, and SIGINT behavior.
• Distribute openshell-prover through the existing OpenShell installation paths: the Debian package, 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 containment checks.
• Document standard installation, effective-policy export, copyable contained and exceeding examples, output fields, exit codes, supported model boundaries, release assets, and macOS support.

Testing

• mise run pre-commit
• mise run test
• mise run ci
• cargo test --locked -p openshell-prover -p openshell-prover-cli with system Z3 4.8.12 and Z3 4.16
• cargo test -p openshell-prover-cli (unit and CLI integration tests)
• bash tasks/scripts/test-install-sh.sh
• bash tasks/scripts/test-packaging-assets.sh
• uv run pytest -q python/openshell/release_formula_test.py
• Generated Homebrew formula passes ruby -c
• Final hosted checks pass on commit ad953f64ec51948ce324f825cd8699cc73a2db4a, including Branch Checks on Linux x86_64, Linux aarch64, and macOS Apple Silicon; Branch E2E; Windows MSVC; Helm; docs preview; dependency review; Trivy; workflow security; and DCO

The local mise run e2e attempt could not execute the MCP conformance assertions because the runner could not read two mounted /tmp fixtures (EACCES). The final hosted Branch E2E workflow passed its required gate and skipped deployment-specific jobs because its change detector found no deployment inputs in scope.

Release workflows build and smoke-test the native release artifacts. They were not dispatched locally across every release target; the branch validates their definitions with Actionlint and the focused packaging tests above.

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