bug(prover): containment check returns Inconclusive(InvalidWitness) for real expansions with system libz3 4.8.12 #4437

User Story

We run OpenShell gateways for an internal agent fleet and build the workspace from source outside
the Nix shell, linking the distro libz3-dev as CONTRIBUTING.md documents. Running the unit suite
on a fork rebased onto v0.1.4-pre.2, endpoint_selector_single_star_crosses_path_separators
fails every time on our machines.

Problem Statement

The network containment check decodes the solver's satisfying model into a concrete request and
rejects any model that is not a canonical request. The solver's action domain does not restrict the
path's characters, so which model comes back depends on the Z3 version. Z3 4.8.12 returns the path
/v1/\0/ for a /v1/* selector. The decoder correctly refuses it (the runtime canonicalizer never
presents control bytes to policy), and the check ends Inconclusive(InvalidWitness) instead of
Exceeds. Z3 4.13.3 returns a printable path and the same check reports Exceeds.

Impact / Why This Matters

• The documented install path (sudo apt install libz3-dev) yields Z3 4.8.12 on Ubuntu 22.04,
  Ubuntu 24.04 and Debian 12, so mise run test fails out of the box there. CI does not see it
  because Rust tests run in the Nix shell, which pins a newer Z3. (deploy/docker/Dockerfile.ci
  installs noble's 4.8.12, but the Rust test jobs do not use it.)
• openshell-prover-cli built against that Z3 reports a real boundary expansion as inconclusive
  and loses the counterexample. This fails closed, so it is not a soundness issue, but it hides
  exactly the evidence the check exists to produce.
• Workarounds are building with vendored-z3 (needs GCC 13+ for <format>, so not on Ubuntu
  22.04's default toolchain) or prebuilt-z3 (links against a newer glibc than 22.04 has).

Acceptance Criteria

• cargo test -p openshell-prover passes when linked against libz3 4.8.12 and 4.13.3.
• A real expansion is reported as Exceeds with a counterexample that replays against the runtime
  Rego, independent of the Z3 version.
• No result changes from Exceeds/Inconclusive to Within as a side effect.

Reproduction Steps

docker run --rm -v "$PWD":/src:ro rust:1.95.0-bookworm bash -c '
  apt-get update -qq && apt-get install -y -qq libz3-dev pkg-config clang libclang-dev protobuf-compiler >/dev/null
  cp -a /src /work && cd /work && rm -f rust-toolchain.toml
  cargo test -p openshell-prover --test runtime_parity'

The same command with rust:1.95.0-trixie (libz3 4.13.3) passes.

Suggested UX (if applicable)

Not applicable: no configuration or CLI change.

Environment

• OpenShell v0.1.4-pre.2 and main at the time of writing (prover unchanged between them)
• libz3 4.8.12 (Ubuntu 22.04 4.8.12-1, Ubuntu 24.04 4.8.12-3.1build1, Debian 12 4.8.12-3.1) fails
• libz3 4.13.3 (Debian 13 4.13.3-1) passes

Logs

test endpoint_selector_single_star_crosses_path_separators ... FAILED
runtime expansion must exceed the boundary: Inconclusive(ReasonEvidence { code: InvalidWitness, reason: "solver returned a model that could not be decoded" })

Instrumented, the model Z3 4.8.12 returns for the path is "/v1/\u{0}/". Restricting the path to
0x21..=0x7e makes it return "/v1/\"/", which the decoder also rejects (" is not a literal
pchar).