chore(build): remove bundled Z3 support

[SDAChess]

Summary

Replace the deprecated bundled-z3 alias with vendored-z3 for local gateway artifacts. Ordinary Cargo builds use the installed Z3 library, which may be static or shared. Gateway binaries built for local container and VM paths explicitly compile and statically link Z3 from z3-src; release binaries use the static Z3 supplied by Nix. Windows build tasks retain their existing prebuilt Z3 path.

Related Issue

No issue required: build maintenance and a correction to local gateway artifact packaging.

Changes

• Replace bundled-z3 feature forwarding with vendored-z3 (z3/vendored) in the prover, prover CLI, server, and gateway. Keep z3-src in Cargo.lock for that opt-in source build.
• Select vendored-z3 when staging local gateway images and building gateway binaries for Kubernetes external-driver E2E and VM E2E. Leave ordinary Cargo builds on the system Z3 path.
• Update contributor, telemetry, and Windows build guidance. Leave the Windows prebuilt-z3 feature and build tasks unchanged.
• Remove old Z3 CMake cache cleanup and unused macOS osxcross Dockerfiles, including their Trivy exclusion.

Testing

• nix develop -c cargo check --locked --offline -p openshell-gateway
• nix develop -c cargo test --locked --offline -p openshell-prover --lib (95 passed)
• cargo tree confirms openshell-gateway --features vendored-z3 selects z3-src
• ShellCheck and bash -n for the changed build scripts; git diff --check
• Full vendored Z3 build: the current Nix development shell lacks CMake and a C++ compiler. Those tools are required when local image or E2E scripts select vendored-z3 from that shell.
• mise run pre-commit: mise is unavailable in this environment; the checks above were run directly.
• E2E tests not run locally.

Checklist

• Conventional Commits and DCO sign-off
• Relevant contributor and published documentation updated

[github-actions]

🌿 Preview your docs: https://nvidia-preview-pr-3275.docs.buildwithfern.com/openshell

[github-actions]

Label test:e2e applied for ba19bea. Open the existing run and click Re-run all jobs to execute with the label set. The run will execute the standard E2E suite after building the required gateway and supervisor images once. The matching required CI gate status on this PR will flip green automatically once the run finishes.

[github-actions]

Label test:e2e-kubernetes applied for ba19bea. Open the existing run and click Re-run all jobs to execute with the label set. The run will execute Kubernetes HA and credential-driver E2E after building the required gateway and supervisor images once. This is an optional proof-of-life suite; failures are visible in the workflow run but do not publish a required CI gate status.

[github-actions]

Label test:e2e-gpu applied for ba19bea. Open the existing run and click Re-run all jobs to execute with the label set. The run will execute GPU E2E after building the required supervisor image once. The matching required CI gate status on this PR will flip green automatically once the run finishes.

[elezar]

Thanks @SDAChess. Looks OK from my side, but it may be good to get @pimlock or @drew to weigh in here too.

[elezar]

A note from tracing the Z3 history and terminology:

• bundled-z3 was introduced with the prover in #741 as an opt-in fallback for developers without a system Z3. It mapped to z3/bundled and compiled Z3 from source; Linux and macOS otherwise used the system library.
• The early Windows work made windows-msvc.ps1 explicitly enable that source-build path in 81cb5ac.
• #2738 then replaced the Windows source-fetch/build/cache machinery with the upstream precompiled-release path. The relevant branch commit was c2554cb, included on main through the squashed merge ddc8bba. That change added OpenShell prebuilt-z3 aliases mapping to z3/gh-release, pinned Z3_SYS_Z3_VERSION=4.16.0, and removed the bundled-specific PowerShell logic. This is why those .ps1 changes should not be reintroduced by this PR: they are already on main via ci(windows): add Windows MSVC CI jobs #2738.
• In the current z3-sys dependency, bundled is itself a deprecated alias for vendored. Both mean compiling the source shipped by z3-src; gh-release instead downloads a precompiled platform artifact. Therefore renaming the Windows prebuilt-z3 alias to vendored-z3 would either be semantically misleading if it continued to map to gh-release, or would change behavior back to the slower source build if mapped faithfully.

So the clean split is: system Z3 by default on non-Windows platforms, prebuilt-z3 / z3/gh-release in the Windows build tasks, and removal of the now-unused bundled-z3 source-build aliases as proposed here.

[SDAChess]

@pimlock i'm handing this over to you if you have some time to rebase-it/check it out while im on PTO.

[elezar]

Could we preserve a portable Z3 runtime for gateway binaries staged into minimal images?

I found that the default z3-sys configuration links against the system-installed Z3; only vendored and gh-release explicitly provide static linkage. Debian's documented libz3-dev contents include libz3.so and no static archive. This matters because CONTRIBUTING.md recommends apt install libz3-dev for non-Nix development.

CI passes because it runs inside nix develop, where nix/pkgs/z3.nix builds Z3 with Z3_BUILD_LIBZ3_SHARED=false. Outside Nix, however, the updated stage-prebuilt-binaries.sh and Kubernetes external-driver build can produce a gateway with a libz3.so dependency. Dockerfile.gateway and Dockerfile.external-kubernetes-gateway copy only the executable into their distroless runtime images, so those containers could fail at startup with a missing libz3.so.

This affects contributor-facing workflows such as mise run build:docker:gateway and local mise run e2e:kubernetes; the latter builds local images by default when it creates an ephemeral k3d cluster.

Could we do one of the following?

1. Enable prebuilt-z3 for binaries that are packaged, copied into a VM, or staged into a container.
2. Copy an ABI-compatible libz3 into the runtime image.
3. Require or automatically enter nix develop for these artifact-producing workflows, since that environment intentionally provides static Z3. If we choose this option, the scripts should enforce it and the contributor documentation should identify Nix as a prerequisite for these workflows.

Whichever approach we choose, I suggest adding a post-build readelf/ldd check that rejects an unexpected dynamic libz3 dependency. That verifies the artifact itself and covers the non-Nix path that current CI does not exercise.

References: z3-sys build configuration, Debian libz3-dev file list.

[SDAChess]

Thanks @elezar — you’re right about the non-Nix image builds: the default system Z3 path can link libz3.so, while the distroless images copy only the gateway executable.

I’ve updated this in 4da75d9. The default Cargo build still uses the installed Z3 (static or shared), and release gateway binaries still use the static Z3 supplied by nix develop. The local paths that stage or copy a gateway binary now explicitly enable vendored-z3: stage-prebuilt-binaries.sh, Kubernetes external-driver E2E, and e2e/run.sh. That feature maps to z3/vendored, which builds and statically links z3-src; Windows keeps its existing prebuilt-z3 path.

One limitation of the local source-build path: it needs CMake and a C++ compiler. The current Nix development shell does not provide those tools, so running these particular local scripts from that shell requires supplying them separately.

[elezar]

Approved. The Nix cross-build/artifact path uses Nix-provided Z3, so the development shell lacking CMake is not a blocker for that path. The separate local gateway image path now selects vendored-z3 and has not yet had a full source build verified. Please still test a fresh mise run build:docker:gateway and smoke-test the resulting openshell/gateway:dev image (for example, docker run --rm openshell/gateway:dev --help); follow up if the local build or image startup fails.