docs(prover): clarify installation and check results

Signed-off-by: Johnny Greco <jogreco@nvidia.com>

Author: johnnygreco

architecture/security-policy.md

@@ -343,38 +343,15 @@ candidate policy with an operator-supplied local maximum. It establishes
 result. It does not fetch gateway state, compose provider rules, apply policy,
 or decide whether an in-boundary change is eligible for automatic approval.
 
-The initial maximum-boundary model covers filesystem paths, L4 network
-authority, and enforced REST method and path authority, including explicit REST
-denies. Network containment covers runtime configurations both with and without
-binary identity enforcement. Strict checks match grants and denies against the
-executable and an ancestor identity, and the evidence identifies the identities
-for an exceeding witness. Network binary selectors, endpoint host and path
-selectors, and REST allow and deny method and path selectors must use ASCII
-literals. This restriction applies to both inputs, including deny-only rules;
-embedded NUL bytes in those fields are also unsupported. Other Unicode policy
-text and filesystem paths are unaffected. ASCII wildcard selectors still cover
-non-ASCII runtime values matched by the policy engine.
-Recognized authority outside the reviewed model produces an unsupported result
-rather than being silently ignored.
-Environment-dependent authority also remains unsupported when the result
-depends on context that is unavailable to the local command. This includes an
-unresolved workdir, filesystem or binary containment that depends on image-specific
-path resolution, and overlapping L4 and REST endpoints whose inspection selection
-depends on the complete runtime endpoint set. Candidate and maximum paths use
-the same sandbox namespace and mount interpretation; the checker does not
-resolve them against the CLI host or verify kernel enforcement in a running
-sandbox. Filesystem checks assume stable path resolution when enforcement rules
-are created. They support matching paths, grant removal, write-to-read reduction,
-and a maximum root grant. Other comparisons between paths remain unsupported;
-lexical ancestry or distinctness alone cannot establish resolved ancestry or
-distinctness. Adding access when the maximum grants none produces a counterexample.
-If the solver produces a string that cannot be decoded and checked faithfully,
-the command returns an inconclusive `invalid_witness` result instead of publishing
-the value as counterexample evidence.
+The initial model covers filesystem paths, L4 network authority, and enforced
+REST method and path authority. It returns explicit unsupported or inconclusive
+results when a sound decision depends on authority or runtime context outside
+the model. The result records the model version and covered domains so callers
+can bind a successful check to those semantics.
 
 This containment operation is separate from the proposal-risk queries below.
 See the [standalone policy prover documentation](../docs/reference/policy-prover.mdx)
-for installation, command behavior, evidence, and exit codes.
+for installation, command behavior, model limitations, evidence, and exit codes.
 
 ## What the proposal prover decides
 

crates/openshell-prover/README.md

@@ -63,8 +63,8 @@ pub struct ExfilPath {
 }
 ```
 
-The gateway's `finding_delta` keys paths by `(category, binary,
-host:port, category, method)` so that adding a new method on an
+The gateway's `finding_delta` keys paths by `(finding query, binary,
+host:port, path category, method)` so that adding a new method on an
 already-reached host surfaces as exactly one new path (not the whole
 re-emission of the existing method set).
 

docs/reference/policy-prover.mdx

@@ -18,43 +18,26 @@ operator-owned ceiling. It does not grant authority by itself.
 
 ## Install the Prover
 
-Download the archive for your platform from the
-[OpenShell releases](https://github.com/NVIDIA/OpenShell/releases) page:
-
-| Platform | Archive |
-|---|---|
-| Linux x86_64 | `openshell-prover-x86_64-unknown-linux-musl.tar.gz` |
-| Linux aarch64 | `openshell-prover-aarch64-unknown-linux-musl.tar.gz` |
-| macOS Apple Silicon | `openshell-prover-aarch64-apple-darwin.tar.gz` |
-
-Download `openshell-prover-checksums-sha256.txt` from the same release. On
-Linux, verify the selected archive before extracting it:
+The standard OpenShell installer includes `openshell-prover`:
 
 ```shell
-archive=openshell-prover-x86_64-unknown-linux-musl.tar.gz
-grep " ${archive}$" openshell-prover-checksums-sha256.txt | sha256sum --check
-tar -xzf "${archive}"
-mkdir -p ~/.local/bin
-install -m 0755 openshell-prover ~/.local/bin/openshell-prover
+curl -LsSf https://raw.githubusercontent.com/NVIDIA/OpenShell/main/install.sh | sh
+openshell-prover --version
 ```
 
-On macOS, use `shasum` for verification:
-
-```shell
-archive=openshell-prover-aarch64-apple-darwin.tar.gz
-grep " ${archive}$" openshell-prover-checksums-sha256.txt | shasum -a 256 --check
-tar -xzf "${archive}"
-mkdir -p ~/.local/bin
-install -m 0755 openshell-prover ~/.local/bin/openshell-prover
-```
+The prover remains independent of the gateway at runtime. If you only need the
+standalone binary, use the artifacts listed in the
+[Support Matrix](/reference/support-matrix#standalone-policy-prover). These
+artifacts and `openshell-prover-checksums-sha256.txt` are attached to
+[OpenShell releases](https://github.com/NVIDIA/OpenShell/releases).
 
 The release archive includes the solver linkage required by the executable.
 It does not require the main `openshell` command, a gateway configuration, or
 a separate Z3 installation.
 
 ## Check a Policy Boundary
 
-Create a maximum policy:
+Create `maximum.yaml` with this maximum policy:
 
 ```yaml
 version: 1
@@ -66,7 +49,7 @@ filesystem_policy:
     - /tmp
 ```
 
-Create the fully composed candidate policy:
+Create `candidate.yaml` with this contained candidate:
 
 ```yaml
 version: 1
@@ -84,6 +67,36 @@ openshell-prover check candidate.yaml --maximum maximum.yaml
 ```
 
 A contained candidate prints `result: within_max` and exits with status `0`.
+To see an exceeding result and its counterexample, replace `candidate.yaml`
+with a policy that makes `/etc` writable even though the maximum grants only
+read access:
+
+```yaml
+version: 1
+filesystem_policy:
+  read_only:
+    - /usr
+  read_write:
+    - /tmp
+    - /etc
+```
+
+```shell
+openshell-prover check candidate.yaml --maximum maximum.yaml
+```
+
+To check the current effective policy of an existing sandbox, export it without
+display metadata:
+
+```shell
+openshell sandbox get my-sandbox --policy-only > candidate.yaml
+openshell-prover check candidate.yaml --maximum maximum.yaml
+```
+
+This export includes provider-contributed rules. For a proposed change that is
+not active, supply the complete post-change effective policy. The standalone
+prover does not compose a base policy with provider rules.
+
 Use JSON when a script consumes the result:
 
 ```shell
@@ -99,6 +112,17 @@ version. An exceeding result also includes a filesystem or network
 counterexample. Automation should use `result` and `reason_code` instead of
 parsing the human-readable explanation.
 
+| Field | When populated |
+|---|---|
+| `counterexample` | An object for `exceeds_max`; otherwise `null`. |
+| `reason_code` | A stable identifier for an emitted `error`, `unsupported`, or `inconclusive` result; otherwise `null`. |
+| `reason` | A human-readable explanation paired with `reason_code`; otherwise `null`. |
+
+The stable reason codes are `invalid_input`, `unsupported_policy_shape`,
+`unresolved_workdir`, `unresolved_binary_path`,
+`unresolved_filesystem_path`, `solver_timeout`, `solver_unknown`,
+`resource_limit`, `invalid_witness`, and `cancelled`.
+
 The solver has a finite 10-second default budget. Set a different positive
 budget with an integer followed by `ms`, `s`, or `m`: