feat(prover): support REST query parameter containment

[kirit93]

Summary

Add generic REST query-parameter containment to the standalone policy prover. This allows policies to distinguish requests with identical methods and paths but different query values, such as Git discovery requests for service=git-upload-pack versus service=git-receive-pack.

Also improve the existing counterexample search so a straightforward permission expansion in a later rule can be found before falling through to a slow solver check.

Related Issue

No directly matching accepted issue has been identified yet. Opened as a draft at the author's request; an accepted issue link is still needed before this is ready to merge.

Changes

Query containment

• Support exact ASCII query values and the whole * wildcard on REST allow and deny rules.
• Preserve required-key presence, empty values, and runtime semantics for repeated parameters: all values must match an allow constraint; any matching value satisfies each configured deny constraint.
• Include decoded query parameters in network counterexamples and CLI JSON/text output.
• Bound query matchers and account for their keys and values in existing pattern-size limits.
• Keep partial globs, any matchers, non-ASCII literals, and embedded NULs unsupported. No application-specific read/write ordering is inferred.

Counterexample search

• Try requests from multiple candidate allow rules, including required query values.
• Replay each request against both complete policies before reporting a violation.
• Limit probing to eight endpoints, 64 rules, and 64 request replays per binary-identity mode, sharing the solver deadline and cancellation flag.
• Fall back to the solver when probing finds no violation; probes never establish containment.

This PR contains only implementation, tests, and fixtures. Documentation changes are intentionally excluded from this submission.

Testing

• Fresh cargo test --locked -p openshell-prover -p openshell-prover-cli: 146 unit/integration tests and one doc test passed, using local system Z3.
• Query matching, deny rules, missing/repeated values, unsupported inputs, and resource-limit coverage.
• Runtime Rego parity and CLI counterexample tests.
• GitHub regression tests covering all 24 rule orderings, probe exhaustion, cancellation, and solver fallback.
• Rust formatting and git diff --check passed.
• mise run pre-commit completed successfully (started; workspace-wide checks still pending at submission).
• Full repository CI and E2E validation.

Checklist

• Conventional Commit with DCO sign-off.
• No documentation or POC changes included.
• Accepted issue linked.
• Architecture/reference documentation update, if required by maintainers (excluded at author's request).

[copy-pr-bot]

Auto-sync is disabled for draft pull requests in this repository. Workflows must be run manually.

Contributors can view more details about this message here.

[johnnygreco]

Panel review: OpenShell PR #3533

Result: changes required before merge. The panel found one high-severity policy-modeling defect that can produce a false containment proof, plus an incomplete documentation update. The PR also lacks the accepted issue required by repository conventions. No PR code, commits, branches, or GitHub discussion were changed.

Reviewed September 22, 2026: feat(prover): support REST query parameter containment.

Findings

High: query * does not have the runtime meaning assumed by the prover

Locations: query.rs:66, query.rs:170–177.

Before this PR, query-constrained policies were unsupported. With this PR, a boundary allowing q: "*" and an otherwise identical candidate allowing q: "a.b" produce within_boundary and exit code 0. At runtime, /?q=a.b is rejected by the boundary and allowed by the candidate. A caller relying on the prover can therefore approve a policy expansion incorrectly.

The runtime calls glob.match(matcher, [], value) in sandbox-policy.rego:742–745. The pinned Regorus 0.9.1 implementation interprets an empty delimiter list as the default . delimiter. Consequently, * does not match a.b.

Both new modeling paths make the same incorrect assumption:

• The structural shortcut accepts every supported candidate matcher under a boundary *, including dotted exact literals.
• The symbolic model treats * as key presence. Its single “other value” class combines values with different runtime matching behavior. Wildcard allow rules also need all repeated values to match, while wildcard deny rules need any value to match. For q=["a", "a.b"], runtime wildcard allow is false and wildcard deny is true; presence alone cannot express that distinction.

The lead independently reproduced the CLI result and ran the reviewer's reproduction against the actual runtime Rego allow_request rule. Results for q=["a.b"] were:

Case	Boundary	Candidate	Runtime boundary allows	Runtime candidate allows	Prover
Allow	Allow q: "*"	Allow q: "a.b"	false	true	within_boundary
Deny	Unrestricted allow; deny q: "a.b"	Unrestricted allow; deny q: "*"	false	true	within_boundary

The deny case also exercises the symbolic path because boundary denies disable the structural shortcut. The lead confirmed its CLI result without solver warnings using /** paths. An earlier exact / version emitted warnings from the installed system Z3; that earlier invocation is not needed for the finding. The primary allow case returns through the structural shortcut and does not depend on solver behavior.

Smallest appropriate correction: preserve runtime semantics and make the finite abstraction distinguish wildcard-matching and nonmatching values; use all/any matching for allow/deny rules and correct the structural implication check. A conservative alternative is to return unsupported for * until it is modeled correctly. Add focused dotted-value and mixed-repeat runtime parity regressions. Changing runtime glob semantics or introducing a general glob framework would exceed this PR's scope.

Low: update the existing prover contract documentation

The new supported query forms, decoded query_params output, and aggregate limit of 256 query matchers are missing from the authoritative documentation:

• docs/reference/policy-prover.mdx:124 omits query_params from network counterexamples; its coverage description at line 164 remains method/path-only and its limits at line 175 omit query matchers.
• architecture/security-policy.md:396–398 retains the previous coverage description.
• crates/openshell-prover/README.md:22 does not include the new query literal restrictions in its scope description.

For example, comparing identical policies with 129 query matchers now exceeds the combined-input limit, despite satisfying the published numeric limits. The PR explicitly excludes documentation, but AGENTS.md requires relevant published and architecture updates for user-facing behavior changes.

Minimal correction: update those existing contract descriptions with the final supported semantics, repeated-value behavior, decoded output and empty-map omission, and the combined-input matcher limit. No new documentation structure or unrelated skill changes are needed.

Repository readiness

The PR body acknowledges that no accepted issue is linked. Repository conventions require an accepted issue for a new feature or user-visible behavior. A maintainer must resolve that gate; the review did not create an issue, apply acceptance labels, or expand the feature scope.

Other checked conventions were followed: the commit is conventional and DCO-signed; the new module has appropriate ownership and license headers; the public counterexample addition uses the existing non-exhaustive API pattern; tests follow existing fixture and integration conventions. Relevant sync-agent-infra maintenance routing found no stale standalone-prover contract in agent skills and no inventory changes requiring broader synchronization.

The PR body describes draft submission, but GitHub reported draft: false at final verification. The available CI snapshot includes successful lint, DCO, and vouch checks, while the main PR test/build and E2E jobs were skipped. Green aggregate statuses therefore do not establish that those suites ran. Repository-wide local CI and E2E were not run during this review.

Panel and scope control

Three independent reviewers inspected the same frozen target concurrently:

Reviewer	Scope	Result
Policy-model soundness	Finite abstraction, runtime equivalence, structural implication, witness realizability, containment security	Wildcard soundness finding
Probe and integration	Complete-policy replay, budgets, cancellation/deadline, solver fallback, CLI output, regression coverage	No independent findings
Implementation clarity and conventions	Modeling clarity, ownership, complexity, repository patterns, docs and skill maintenance	Documentation finding

The lead monitored progress, requested concrete reproductions, independently verified findings, consolidated duplicated documentation observations, and kept proposed corrections at the existing model boundary. No broad refactor, runtime behavior change, unsupported matcher expansion, or new abstraction was requested.

The exact-only abstraction, missing versus empty values, repeated-value sets, conjunction across keys, validation before shortcuts, bounded probing, full-policy replay, and conservative solver fallback had no additional confirmed findings. The code is generally cohesive; the high-severity finding concerns semantic correctness rather than implementation style.

No relevant core review lens was omitted: correctness/security, tests, maintainability, CLI experience, documentation, and API/integration concerns were covered across the three reviewers. Separate deployment, database migration, dependency/supply-chain, GUI accessibility, and FFI reviews were inapplicable to this diff. Performance review was limited to the changed probe/model bounds; no benchmark project was warranted.

One review round was completed, with no code edits or reruns. Findings remain unresolved because this was a review-and-report task. All reviewer sessions were concluded after their results were captured.

Validation

Run from the isolated checkout at the reviewed head:

cargo test --locked -p openshell-prover -p openshell-prover-cli --target-dir /tmp/pr3533-target
git diff --check fa8f6d394983b541ac31363f8a2d5ea027b08acf 48e12bdbf15d7f202456b6bcc9667cc6cdebe85d

• Focused tests: 146 unit/integration tests and 1 doc test passed, using installed system Z3 4.8.12.
• Diff whitespace check: passed.
• Actual runtime Rego reproduction: boundary rejects and candidate allows the dotted query, for both allow and deny examples.
• Existing query parity tests pass but omit dotted wildcard behavior; passing tests do not resolve the soundness finding.
• Reviewed checkout remained clean. The only workspace deliverable is this report.

Reproduce the primary finding

At the reviewed commit, create these two authored policies and run the CLI. They differ only in the query constraint:

cat > /tmp/pr3533-boundary.json <<'EOF'
{"version":1,"network_policies":{"n":{"endpoints":[{"host":"example.com","port":443,"protocol":"rest","enforcement":"enforce","rules":[{"allow":{"method":"GET","path":"/","query":{"q":"*"}}}]}]}}}
EOF
cat > /tmp/pr3533-candidate.json <<'EOF'
{"version":1,"network_policies":{"n":{"endpoints":[{"host":"example.com","port":443,"protocol":"rest","enforcement":"enforce","rules":[{"allow":{"method":"GET","path":"/","query":{"q":"a.b"}}}]}]}}}
EOF
cargo run --locked -p openshell-prover-cli --bin openshell-prover -- check /tmp/pr3533-candidate.json --boundary /tmp/pr3533-boundary.json --output json

Observed: result: "within_boundary", exit_code: 0. Correct result with complete modeling: exceeds_boundary, because GET /?q=a.b distinguishes the policies. A conservative unsupported result is also preferable to an unsound proof.

For runtime verification, load the checked-in supervisor Rego with normalized endpoint ports: [443], set the policy's runtime binary-identity configuration, and evaluate data.openshell.sandbox.allow_request on the same request with decoded query_params: {"q":["a.b"]}. The standalone review reproduction is available locally at /tmp/pr3533-query-full-repro.rs; it evaluates both allow and deny pairs against that actual rule. The main finding is also directly traceable to the pinned Regorus src/builtins/glob.rs default-delimiter logic and the runtime call cited above.

Frozen target and reproduction of the diff

• Base ref: main at 96c08f111b7ccf3d048a876c23e724014babb585.
• Head ref: kirit93/prover-query-containment at 48e12bdbf15d7f202456b6bcc9667cc6cdebe85d.
• Actual PR diff baseline / merge-base: fa8f6d394983b541ac31363f8a2d5ea027b08acf.
• One commit: feat(prover): support REST query parameter containment.
• Scope: 12 files, 1,209 additions, 50 deletions.
• Isolated checkout: /tmp/openshell-pr3533-review; clean detached head, no uncommitted work included.
• GitHub head was rechecked and remained unchanged.

git diff fa8f6d394983b541ac31363f8a2d5ea027b08acf 48e12bdbf15d7f202456b6bcc9667cc6cdebe85d

Accepted findings are the wildcard modeling defect and documentation gap. No separate finding was raised for a missing mixed-value integration witness without a demonstrated defect; the necessary wildcard regression is included in the confirmed finding. Decoded NUL handling raised a runtime evaluation error and was not elevated into a speculative second bug. Generic hardening and stylistic refactors were excluded. No additional out-of-scope engineering follow-up was requested.