docs(policy): correct prover installation and coverage limits

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

Author: johnnygreco

docs/reference/policy-prover.mdx

@@ -50,8 +50,12 @@ or MCP rules, the prover reports that it cannot check the policy instead of
 ignoring those rules. [What the Boundary Check
 Covers](#what-the-boundary-check-covers) describes each part and its limits.
 
-The `openshell-prover` CLI is installed with OpenShell. It reads policy files on
-your machine, does not need a gateway, and does not apply or approve policies.
+The Homebrew, Debian, and RPM packages install the `openshell-prover` CLI. The
+snap package does not include it, so on a snap installation, download the
+`openshell-prover` archive for your platform from the [OpenShell
+releases](https://github.com/NVIDIA/OpenShell/releases). The CLI reads policy
+files on your machine, does not need a gateway, and does not apply or approve
+policies.
 
 Create `boundary.yaml`, a boundary that allows reading `/usr` and `/etc`:
 
@@ -85,7 +89,7 @@ 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
+The `coverage` line lists the parts of a policy that the prover can check. Now
 change the candidate so that it also allows writing to `/tmp`, which the
 boundary does not allow:
 
@@ -117,8 +121,9 @@ openshell sandbox get my-sandbox --policy-only > candidate.yaml
 openshell-prover check candidate.yaml --boundary boundary.yaml
 ```
 
-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.
+The effective policy includes rules from attached providers, so the check
+includes network access that providers add. 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.
 
@@ -206,8 +211,13 @@ The prover returns `unsupported` in these cases:
   glob, such as `/usr/bin/curl` under `/usr/bin/*`. A symlink in the sandbox
   image could make the exact path refer to an executable outside the glob. Use
   the same exact paths in both policies when you can.
-- Endpoints that could match the same host and port, including wildcard hosts,
-  set different `allowed_ips`.
+- Endpoints on the same port set different `allowed_ips`, and their hosts are
+  the same or one of them is a wildcard. The prover treats a wildcard host as
+  overlapping every host on its port.
+- An exact host and a wildcard host share a port and neither sets
+  `allowed_ips`, such as `github.com` and `*.githubusercontent.com` on port 443.
+- An endpoint omits `host`, sets both `port` and `ports`, or uses an IPv6
+  address as its host.
 - A host, path, method, or binary contains non-ASCII characters.
 
 ### REST Requests
@@ -216,5 +226,6 @@ The prover compares method and path allow and deny rules on endpoints with
 `protocol: rest`. These endpoints must use `enforcement: enforce`. An endpoint
 in audit mode returns `unsupported`, because it does not block requests. A host
 and port that has both a REST endpoint and an endpoint without request rules
-also returns `unsupported`. Other request protocols, such as WebSocket, GraphQL,
-MCP, and JSON-RPC, return `unsupported`.
+also returns `unsupported`, as do REST rules that match query parameters or use
+`?` or bracket expressions in paths. Other request protocols, such as WebSocket,
+GraphQL, MCP, and JSON-RPC, return `unsupported`.