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>

Author: zredlined

.gitignore

@@ -197,3 +197,4 @@ architecture/plans
 .claude/settings.local.json.claude/worktrees/
 .claude/worktrees/
 rfc.md
+.z3-trace