feat(prover): add native Rust policy prover with Z3 solver

[zredlined]

Summary

Native Rust implementation of the OpenShell Policy Prover (OPP) using Z3 SMT solving. Answers two questions about any sandbox policy:

1. Can data leave this sandbox? — finds exfiltration paths through uninspected (L4-only) endpoints and wire protocol bypasses
2. Can the agent write despite read-only intent? — finds write operations that bypass read-only policy through binary capabilities and credential scopes

openshell policy prove is now a native CLI command — no Python, no subprocess, no PYTHONPATH.

Supersedes #703 (Python prototype). Closes #699.

Related Issue

Closes #699

Changes

New crate: crates/openshell-prover/

• model.rs — Z3 constraint model encoding policy rules, binary capabilities, and credential scopes as boolean satisfiability constraints
• queries.rs — two verification queries (exfiltration, write bypass)
• policy.rs — policy YAML parser with intent detection, L7 enforcement helpers, workdir modeling
• registry.rs — binary capability registry (git, curl, node, claude, etc.) loaded from YAML
• credentials.rs — credential and API capability loading
• accepted_risks.rs — risk acceptance matching by query + host
• report.rs — terminal and compact (CI) output
• finding.rs — finding types and risk levels (HIGH, CRITICAL only)
• lib.rs — public prove() API + 7 tests

Registry data (crates/openshell-prover/registry/):

• 9 binary capability descriptors, 1 API descriptor (GitHub)

CLI integration (crates/openshell-cli/src/main.rs):

• openshell policy prove calls openshell_prover::prove() directly

Dependencies (Cargo.toml):

• z3 = { version = "0.19", features = ["bundled"] } — self-contained Z3 build

Testing

• cargo build -p openshell-prover — compiles with Z3 bundled
• cargo test -p openshell-prover — 7/7 tests pass
• cargo build -p openshell-cli — CLI compiles
• End-to-end: openshell policy prove --compact detects exfil + write bypass on test fixture

Checklist

• Follows Conventional Commits
• Commits are signed off (DCO)
• SPDX license headers on all new files

[zredlined]

@NVIDIA/openshell-codeowners The Rust checks for PR #741 are failing because z3-sys needs libclang for bindgen, and our ghcr.io/nvidia/openshell/ci:latest image doesn’t include it. I can patch branch-checks.yml to install clang/libclang-dev in the Rust jobs for an immediate unblock, but I think we should also update deploy/docker/Dockerfile.ci and republish the CI image as the proper fix. Do folks prefer the workflow-level unblock first, or do we want to fix the CI image before rerunning checks?

[johntmyers]

@NVIDIA/openshell-codeowners The Rust checks for PR #741 are failing because z3-sys needs libclang for bindgen, and our ghcr.io/nvidia/openshell/ci:latest image doesn’t include it. I can patch branch-checks.yml to install clang/libclang-dev in the Rust jobs for an immediate unblock, but I think we should also update deploy/docker/Dockerfile.ci and republish the CI image as the proper fix. Do folks prefer the workflow-level unblock first, or do we want to fix the CI image before rerunning checks?

I'd make sure it's in the image.