docs(policy): rewrite policy prover guide for clarity

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

Author: johnnygreco

docs/reference/policy-prover.mdx

@@ -1,49 +1,51 @@
 ---
 # SPDX-FileCopyrightText: Copyright (c) 2025-2026 NVIDIA CORPORATION & AFFILIATES. All rights reserved.
 # SPDX-License-Identifier: Apache-2.0
-title: "Standalone Policy Prover"
+title: "Policy Prover"
 sidebar-title: "Prover"
-description: "Install and use the standalone OpenShell policy prover to check a local candidate policy against a managed boundary."
-keywords: "Generative AI, Cybersecurity, Policy, Prover, Boundary, Containment, CI"
+description: "Check that a policy grants no more access than a boundary policy you define, for example before you apply a change or in CI."
+keywords: "Generative AI, Cybersecurity, Policy, Prover, Boundary, CI"
 position: 8
 ---
 
-`openshell-prover` checks whether the authority in a local candidate policy is
-contained within a local boundary policy. The command reads files from the host
-and does not connect to an OpenShell gateway.
+The policy prover checks that a policy grants no more access than a limit you
+set. You write the limit as a second policy, called the boundary. The prover
+determines whether everything allowed by the policy you are testing, called the
+candidate, is also allowed by the boundary. If the candidate allows something
+the boundary does not, the prover shows an example.
 
-The candidate must be the fully composed effective policy after the proposed
-change, including any provider-contributed authority. The boundary is an
-operator-owned ceiling. It does not grant authority by itself.
+The prover checks only some parts of a policy: filesystem access, process
+identity, Landlock settings, network destinations, and REST methods and paths.
+If a policy uses anything else, such as GraphQL or MCP rules, the prover reports
+that it cannot check the policy instead of ignoring those rules.
+
+Use the prover to check a policy before you apply it, for example in CI, so
+that no change grants more than your organization allows. The prover is a
+separate command, `openshell-prover`, that reads policy files on your machine.
+It does not connect to a gateway, and it does not apply or approve policies.
 
 The [policy advisor](/sandboxes/policy-advisor#what-the-prover-checks) runs a
-separate prover check automatically on each proposal to find whether the
-proposal adds new access compared with the current policy. Use this command when
-you need to check a complete policy against a fixed boundary, for example in
-CI.
+different prover check on each proposal. That check compares the proposal with
+the sandbox's current policy instead of a boundary you write.
 
 ## Install the Prover
 
-The standard OpenShell installer includes `openshell-prover`:
+The OpenShell installer includes `openshell-prover`:
 
 ```shell
 curl -LsSf https://raw.githubusercontent.com/NVIDIA/OpenShell/main/install.sh | sh
 openshell-prover --version
 ```
 
-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.
+To install only the prover, download its archive from
+[OpenShell releases](https://github.com/NVIDIA/OpenShell/releases). The
+[Support Matrix](/reference/support-matrix#standalone-policy-prover) lists the
+available platforms. The prover runs on its own, without the `openshell` CLI, a
+gateway, or a separate Z3 installation.
 
-## Check a Policy Boundary
+## Check a Policy
 
-Create `boundary.yaml` with this boundary policy:
+Create `boundary.yaml`, a boundary that allows reading `/usr` and `/etc`:
 
 ```yaml
 version: 1
@@ -53,7 +55,7 @@ filesystem_policy:
     - /etc
 ```
 
-Create `candidate.yaml` with this contained candidate:
+Create `candidate.yaml`, a candidate that allows reading only `/usr`:
 
 ```yaml
 version: 1
@@ -62,16 +64,22 @@ filesystem_policy:
     - /usr
 ```
 
-Run the check:
+Check the candidate against the boundary:
 
 ```shell
 openshell-prover check candidate.yaml --boundary boundary.yaml
 ```
 
-A contained candidate prints `result: within_boundary` and exits with status `0`.
-To see an exceeding result and its counterexample, replace `candidate.yaml`
-with a policy that grants writes to `/tmp`. The boundary grants no write
-access:
+The candidate allows less than the boundary, so the check passes:
+
+```text
+result: within_boundary
+coverage: domains=filesystem,network_l4,network_rest,process,landlock
+```
+
+The `coverage` line lists the parts of the policy that the prover checked. Now
+change the candidate so that it also allows writing to `/tmp`, which the
+boundary does not allow:
 
 ```yaml
 version: 1
@@ -82,196 +90,92 @@ filesystem_policy:
     - /tmp
 ```
 
-```shell
-openshell-prover check candidate.yaml --boundary boundary.yaml
+Run the same command again. The check fails, and the `counterexample` line
+shows access that the candidate allows but the boundary does not:
+
+```text
+result: exceeds_boundary
+coverage: domains=filesystem,network_l4,network_rest,process,landlock
+counterexample: filesystem write /tmp
 ```
 
-To check the current effective policy of an existing sandbox, export it without
-display metadata:
+### Check a Sandbox's Policy
+
+To check the policy that a sandbox enforces, save its effective policy and use
+it as the candidate:
 
 ```shell
 openshell sandbox get my-sandbox --policy-only > candidate.yaml
 openshell-prover check candidate.yaml --boundary boundary.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:
+The effective policy includes rules from attached providers, so the check covers
+everything the sandbox can reach. The prover does not add provider rules itself.
+To check a change before you apply it, give the prover the complete effective
+policy as it would be after the change.
 
-```shell
-openshell-prover check candidate.yaml \
-  --boundary boundary.yaml \
-  --output json
-```
+## Read the Result
 
-The JSON object includes the result, exit code, input paths, schema version,
-prover version, and modeled domains. `schema_version` versions the JSON contract,
-`prover_version` identifies the implementation that produced the result, and
-`coverage.domains` is the machine-readable declaration of modeled policy
-domains. An exceeding result also includes a typed counterexample. Automation
-should use `result` and `reason_code` instead of parsing the human-readable
-explanation.
-
-| Field | When populated |
-|---|---|
-| `counterexample` | An object for `exceeds_boundary`; 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 `counterexample.domain` field selects one of these objects:
-
-| Domain | Fields |
-|---|---|
-| `filesystem` | `access` (`read` or `write`) and `path`. |
-| `process` | `field` (`run_as_user` or `run_as_group`), `boundary`, and `candidate`. |
-| `landlock` | `boundary` and `candidate` compatibility modes. |
-| `network` | `binary`, `ancestor_binary`, `binary_identity_required`, `host`, `destination_ip`, `trusted_gateway`, `port`, `protocol`, `method`, and `path`. |
-
-Network `binary` and `ancestor_binary` values are `null` when binary identity
-enforcement is disabled. `method` and `path` are `null` for L4 witnesses.
-`trusted_gateway: true` means the witness uses a recognized host-gateway alias
-with a runtime-provided trusted gateway binding; `false` uses ordinary
-destination validation.
-
-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`:
+The prover reports one of these results:
 
-```shell
-openshell-prover check candidate.yaml \
-  --boundary boundary.yaml \
-  --timeout 30s \
-  --output json
+| Result | Exit code | Meaning |
+|---|---|---|
+| `within_boundary` | `0` | The candidate allows nothing beyond the boundary in the parts of the policy that the prover checks. |
+| `exceeds_boundary` | `1` | The candidate allows access that the boundary does not. The counterexample shows one example. |
+| `error` | `2` | The prover could not run the check, for example because a file is missing or a policy is invalid. |
+| `unsupported` | `3` | A policy uses something the prover cannot check. The reason explains what. |
+| `inconclusive` | `3` | The prover could not finish, for example because it ran out of time or the policies are too large. |
+
+Only `within_boundary` means that the check passed. In CI, treat every other
+result as a failure. For example, a candidate with a GraphQL rule returns:
+
+```text
+result: unsupported
+coverage: domains=filesystem,network_l4,network_rest,process,landlock
+reason: candidate policy rule 'g' uses protocol 'graphql'; only L4 TCP and REST are modeled
 ```
 
-## Exit Codes
-
-| Exit | Result | Meaning |
-|---|---|---|
-| `0` | `within_boundary` | Containment was established for the reported modeled domains. |
-| `1` | `exceeds_boundary` | The candidate exceeds the boundary; inspect the counterexample. |
-| `2` | `error` | Arguments, input files, policy syntax, or command execution prevented a valid check. |
-| `3` | `unsupported` or `inconclusive` | The model cannot soundly cover the policy shape, or the solver did not reach a determination. |
-| `130` | `inconclusive` when graceful handling completes | The user interrupted the command with Ctrl-C on Unix; a second or very early interruption may prevent output. |
-
-Only exit `0` means the verification succeeded. Treat unsupported and
-inconclusive results as failures in CI.
-
-## Interpretation and Limits
-
-The containment check covers filesystem paths, process identity settings,
-Landlock compatibility requirements, L4 destination authority, and enforced
-REST method and path authority, including explicit REST denies. The result
-object reports the policy domains modeled by each check. Policies that use
-recognized authority outside that coverage return `unsupported` rather than
-silently ignoring it.
-
-Both inputs use the same bounded YAML/JSON parser and authored policy schema as
-OpenShell. Unknown fields, duplicate keys, malformed field types, and unsupported
-managed `metadata` or `review` annotations return `error` with
-`reason_code: invalid_input` and exit `2`. Schema-valid controls outside the
-containment model return `unsupported` and exit `3`.
-
-The prover applies aggregate limits across the candidate and boundary before
-semantic shape validation: 1,024 network rules, 4,096 endpoints, 4,096 binary
-selectors, 65,536 authored port entries, 4,096 `allowed_ips` entries, 16,384
-REST rules, 4 KiB per modeled pattern, and 1 MiB of modeled pattern text.
-Exceeding any limit returns `inconclusive` with `reason_code: resource_limit`.
-A cancellation already requested at preflight takes precedence over that
-result; otherwise a resource limit takes precedence over unsupported
-policy-shape diagnostics. This ordering keeps validation work bounded for
-checked-in CI inputs.
-
-### Process and Landlock settings
-
-Matching supported `run_as_user` and `run_as_group` values do not expand the
-configuration. Changing an explicit non-root identity to `root` or `0` returns
-`exceeds_boundary` with the field and both values. Other identity changes return
-`unsupported`; the command does not resolve accounts from a sandbox image.
-These comparisons assume consistent identity resolution and execution settings.
-They do not prove permission relationships between arbitrary Linux accounts.
-
-Landlock `hard_requirement` may not become `best_effort`. That change returns
-`exceeds_boundary`. Keeping the same mode or strengthening it to
-`hard_requirement` passes this part of the check. This compares the requested
-requirement, not whether a target kernel successfully installed Landlock
-restrictions.
-
-### Destination IP restrictions
-
-The network action includes an IPv4 or IPv6 destination address. CIDR entries
-in `allowed_ips` are modeled together with host, port, executable, and REST
-restrictions; network counterexamples include `destination_ip`. An empty IP
-list follows the runtime's destination rules and is not a universal allowlist.
-The check does not resolve DNS on the host running the CLI.
-
-Policies whose potentially overlapping endpoints select different destination
-restrictions remain unsupported because the runtime uses the selected
-endpoint's address filter. The prover conservatively treats wildcard host
-selectors on a shared port as potentially overlapping, including when their
-literal suffixes differ. CIDR unions within a supported endpoint are checked by
-the solver. Unsupported IP-literal wildcard selectors and ranges rejected by
-the runtime also cannot produce a successful proof.
-
-Consumers must inspect `coverage.domains` and require every domain relevant to
-their authorization decision. A successful result applies only to those
-reported domains and the documented assumptions.
-
-### Remaining limits
-
-Network binary selectors, endpoint host and path selectors, and REST allow and
-deny method and path selectors must use ASCII literals in both the candidate and
-boundary. A non-ASCII literal in one of these fields returns `unsupported` with
-`reason_code: unsupported_policy_shape`, including when it appears only in a
-deny. Embedded NUL bytes in these fields are also unsupported. This is a
-prover-model limitation, not a general policy validation rule: filesystem paths
-and unrelated policy text retain their existing Unicode behavior. ASCII
-wildcard selectors still cover non-ASCII runtime values matched by the policy
-engine.
-
-Containment means `Allowed(candidate)` is a subset of `Allowed(boundary)` under
-the reported model. It does not establish least privilege, automatic approval
-eligibility, semantic safety, or equivalence to a running sandbox's kernel
-state. In particular:
-
-- The command does not fetch the current sandbox policy or compose provider
-  rules. The caller must supply the effective candidate.
-- The command does not apply, approve, or persist a policy.
-- Environment-dependent authority, such as an unresolved image workdir,
-  returns `unsupported` when the result depends on that missing context.
-- Binary comparisons that can change when an image resolves an exact selector
-  through a symlink return `unsupported`. This covers exact candidate grants
-  under boundary globs and exact boundary denies replaced by candidate globs.
-  Use matching exact canonical paths when possible.
-- Policies with overlapping L4 and enforced REST endpoints return
-  `unsupported` because inspection selection depends on the complete set of
-  matching runtime endpoint configurations.
-- Network containment checks both supported runtime configurations: binary
-  identity enforcement enabled and disabled. When enabled, grants and denies
-  match the executable or an ancestor identity. Network counterexamples report
-  the configuration and identities that expose the additional authority.
-- REST containment witnesses use canonical request methods and paths.
-- If a solver string cannot be decoded and validated faithfully, the command
-  returns `inconclusive` with `reason_code: invalid_witness` instead of emitting
-  a counterexample.
-- Both files are interpreted in the same sandbox filesystem namespace and
-  mount model, with stable path resolution when enforcement rules are created.
-  The CLI does not resolve sandbox paths against the host.
-- Filesystem containment supports removing grants and reducing write grants to
-  read-only grants at matching paths. A boundary grant for `/` also covers other
-  paths for the same access. Comparisons between different paths otherwise
-  return `unsupported` with `reason_code: unresolved_filesystem_path`: a lexical
-  child can resolve outside its parent through a symlink, and unrelated paths
-  can resolve to the same object. This includes narrowing `/tmp` to `/tmp/cache`.
-  If the boundary grants no access of the requested kind, adding that access
-  returns `exceeds_boundary`.
-
-Use the [Policy Schema Reference](/reference/policy-schema) for the full policy
-language. A successful prover result covers only the policy domains reported in
-its evidence.
+For scripts, add `--output json`. Read the `result` and `reason_code` fields
+instead of parsing the text output. `reason_code` is a stable identifier, such
+as `unsupported_policy_shape` or `solver_timeout`. Also check that
+`coverage.domains` includes every part of the policy that you rely on. Run
+`openshell-prover check --help` for all options, including `--timeout`, which
+changes the default 10-second time limit.
+
+## What a Passing Result Means
+
+A passing result means that the candidate allows nothing beyond the boundary in
+the parts of the policy that the prover checks. It does not mean that the policy
+is as narrow as it could be, that it is safe for a particular task, or that a
+running sandbox enforces it.
+
+The prover reports `unsupported` instead of guessing when the answer depends on
+something it cannot see or does not check:
+
+- Network rules other than connection rules and REST rules, such as WebSocket,
+  GraphQL, MCP, and JSON-RPC rules.
+- Filesystem comparisons between different paths, such as narrowing `/tmp` to
+  `/tmp/cache`. A symlink in the sandbox image could make the paths refer to
+  different locations. Removing a path, or changing it from read-write to
+  read-only, is supported.
+- Binary rules that compare an exact path with a glob, because a symlink in the
+  sandbox image could change which executable the path refers to. Use matching
+  exact paths when you can.
+- Settings that depend on the sandbox image, such as the working directory.
+- Endpoints for the same host and port that set different `allowed_ips`, or
+  that mix connection-only and REST rules.
+- Process identity changes other than changing a non-root user or group to
+  root. The prover reports a change to root as exceeding the boundary.
+- Host, path, method, or binary values that contain non-ASCII characters.
+
+The prover also handles these cases in specific ways:
+
+- Changing Landlock from `hard_requirement` to `best_effort` exceeds the
+  boundary. The prover compares the settings, not what a kernel enforces.
+- The prover checks network rules both with and without binary identity
+  enforcement, because a sandbox runtime can turn it off.
+- The prover does not resolve hostnames on your machine. It checks
+  `allowed_ips` ranges together with hosts, ports, binaries, and REST rules.
+- Very large policies, for example with more than 1,024 network rules or 4,096
+  endpoints across both files, return `inconclusive` with the `reason_code`
+  `resource_limit`.

docs/sandboxes/policy-advisor.mdx

@@ -288,5 +288,5 @@ created from denials), and where the approval mode setting came from.
 - Use [Network Rules](/sandboxes/network-rules) and the
   [Policy Schema Reference](/reference/policy-schema) for rules that agents
   cannot propose.
-- Use the [Standalone Policy Prover](/reference/policy-prover) to check a
+- Use the [Policy Prover](/reference/policy-prover) to check a
   complete policy against a boundary you define.