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

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

Add openshell-prover crate implementing formal policy verification
using Z3 SMT solving. Answers two questions about any sandbox policy:
"Can data leave?" and "Can the agent write despite read-only intent?"

Native Rust — no Python subprocess, no PYTHONPATH, no uv dependency.
Z3 bundled via z3-sys for self-contained builds.

Replaces the Python prototype from #703.

Closes #699

Signed-off-by: Alexander Watson <zredlined@gmail.com>

* fix(prover): skip L7-write in exfil, write bypass only on read-only intent

Port two fixes from the Python branch:
- Exfil query skips endpoints where L7 is enforced and working
- Write bypass only fires on explicit read-only intent, not L4-only

Signed-off-by: Alexander Watson <zredlined@gmail.com>

* chore(prover): add missing SPDX license headers to registry and testdata YAML files

* fix(prover): revert serde_yaml to serde_yml to match workspace dependency on main

* fix(prover): apply cargo fmt formatting to prover and cli source files

* ci: add clang and libclang-dev to CI image for z3-sys bindgen

z3-sys requires libclang at build time for bindgen to generate FFI
bindings. Without it, the Rust CI jobs fail on the prover crate.

* fix(prover): use system libz3 instead of compiling from source

Add libz3-dev to the CI image and drop the z3 `bundled` feature from
the workspace dependency. This eliminates the ~30 min z3 C++ build
that ran on every CI cache miss.

sccache only wraps rustc — it does not intercept the cmake C++ build
that z3-sys runs when `bundled` is enabled. The cargo target cache
helped on warm runs but evicts on toolchain bumps and fork PRs.
With the system library pre-installed in the CI image, z3 link time
is always zero.

A `bundled-z3` opt-in feature is added to the prover crate for local
development without system z3:

  cargo build -p openshell-prover --features bundled-z3

Regular local dev: brew install z3 (macOS) or apt install libz3-dev
(Linux), then cargo build just works.

Signed-off-by: Alexander Watson <zredlined@gmail.com>
Made-with: Cursor

* fix(prover): use u16 for ports, align include_workdir default with runtime

Port fields changed from u32 to u16 across all prover types (policy,
model, finding, queries). Prevents the prover from silently accepting
port values >65535 that the runtime rejects, which would produce
misleading PASS results on invalid policies.

Change include_workdir serde default from true to false to match the
runtime (openshell-policy uses #[serde(default)] which gives false).
The previous mismatch caused the prover to model a /sandbox path that
does not exist at runtime, producing false analysis.

Signed-off-by: Alexander Watson <zredlined@gmail.com>
Made-with: Cursor

* refactor(prover): embed registry at compile time, replace hand-rolled glob

Embed binary and API capability registry YAML files into the binary at
compile time using include_dir!. The previous approach used
env!("CARGO_MANIFEST_DIR") which bakes in the build machine's source
path — works in tests but breaks for installed binaries. The CWD
fallback was equally fragile.

The --registry CLI flag still works as a filesystem override for custom
registries. Credentials remain filesystem-loaded (user-supplied data).

Replace the hand-rolled glob matching (~60 lines) with the glob crate's
Pattern::matches(), which is already a transitive dependency.

Remove unused dependencies: openshell-policy, openshell-core, thiserror,
tracing. The prover parses policy YAML directly into its own types and
does not use the policy or core crate APIs.

Signed-off-by: Alexander Watson <zredlined@gmail.com>
Made-with: Cursor

* docs: add Z3 system library to prerequisites

The prover crate now links against system libz3 instead of compiling
from source. Document the install steps for macOS, Ubuntu, and Fedora,
and note the bundled-z3 feature flag as a fallback.

Signed-off-by: Alexander Watson <zredlined@gmail.com>
Made-with: Cursor

* fix(prover): apply cargo fmt formatting

Made-with: Cursor

---------

Signed-off-by: Alexander Watson <zredlined@gmail.com>

Author: zredlined

.gitignore

@@ -201,3 +201,4 @@ architecture/plans
 .claude/worktrees/
 rfc.md
 .worktrees
+.z3-trace

CONTRIBUTING.md

@@ -119,6 +119,28 @@ Project requirements:
 - Rust 1.88+
 - Python 3.12+
 - Docker (running)
+- Z3 solver library (for the policy prover crate)
+
+### Z3 installation
+
+The `openshell-prover` crate links against the system Z3 library via pkg-config.
+
+```bash
+# macOS
+brew install z3
+
+# Ubuntu / Debian
+sudo apt install libz3-dev
+
+# Fedora
+sudo dnf install z3-devel
+```
+
+If you prefer not to install Z3 system-wide, you can compile it from source as a one-time step:
+
+```bash
+cargo build -p openshell-prover --features bundled-z3
+```
 
 ## Getting Started