chore(build): remove bundled Z3 support

.agents/skills/build-openshell-mxc-windows/SKILL.md

@@ -260,7 +260,7 @@ MXC on Windows. Each other `compute-driver-*` feature installs its own Windows
 rejection stub without linking that driver crate. The default
 `in-tree-compute-drivers` alias enables all five features. An MXC-only build
 uses `--no-default-features --features compute-driver-mxc` (add `telemetry`
-and `bundled-z3` as needed).
+and `openshell-server/prebuilt-z3` as needed).
 
 | Driver | Windows build behavior | Runtime behavior |
 |---|---|---|

CONTRIBUTING.md

@@ -309,16 +309,15 @@ Project requirements:
 - Rust 1.94+
 - Python 3.11+
 - Docker (running)
-- CMake 3.16+ (only required when building with the `bundled-z3` feature)
 
 ### Z3 installation
 
 The `openshell-prover` crate links directly against Z3. The `openshell-server`
 crate depends on the prover, and the `openshell-gateway` binary crate depends
-on `openshell-server` in turn; both forward a `bundled-z3` feature down to
-`openshell-prover/bundled-z3`. The `openshell-cli` crate does not depend on
-Z3. On macOS and Linux, install the system Z3 development package; `z3-sys`
-discovers it through `pkg-config`.
+on `openshell-server` in turn. The `openshell-cli` crate does not depend on Z3.
+The Nix development shell supplies Z3. For builds outside that shell on macOS
+and Linux, install the system Z3 development package; `z3-sys` discovers it
+through `pkg-config`.
 
 ```bash
 # macOS
@@ -331,13 +330,6 @@ sudo apt install libz3-dev
 sudo dnf install z3-devel
 ```
 
-If you prefer not to install Z3 system-wide, use the bundled Z3 feature. This
-compiles Z3 from source during the Rust build and requires CMake 3.16+:
-
-```bash
-cargo build -p openshell-prover --features bundled-z3
-```
-
 For x86-64 and ARM64 Windows MSVC builds, use one of these Z3 paths:
 
 - Prebuilt Z3 (the default for `windows:*` tasks): `z3-sys` downloads the
@@ -351,14 +343,12 @@ For x86-64 and ARM64 Windows MSVC builds, use one of these Z3 paths:
   target-compatible MSVC Z3 library and `Z3_SYS_Z3_HEADER` at the full path to `z3.h`.
   The `windows:*` tasks use this path automatically when `Z3_LIBRARY_PATH_OVERRIDE`
   is set.
-- Bundled Z3: for direct Cargo builds, pass `--features bundled-z3` so `z3-sys`
-  builds Z3 from source.
 
 `openshell-prover` itself has no `bindgen`/`libclang` dependency, so building
 just this crate does not require `LIBCLANG_PATH`:
 
 ```powershell
-cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features bundled-z3
+cargo build -p openshell-prover --target x86_64-pc-windows-msvc --features prebuilt-z3
 ```
 
 ### Windows full build

Cargo.toml

@@ -139,7 +139,7 @@ k8s-openapi = { version = "0.24", features = ["v1_29"] }
 # IDs
 uuid = { version = "1.10", features = ["v4"] }
 
-# SMT solver (uses system libz3; enable z3/bundled via the prover's bundled-z3 feature for local dev without system z3)
+# SMT solver (uses system libz3; Windows build tasks enable the prebuilt release feature)
 z3 = "0.20"
 
 [workspace.lints.rust]

README.md

@@ -283,8 +283,8 @@ cargo build --release -p openshell-gateway --no-default-features --features tele
 # Docker and VM only, with telemetry compiled out.
 cargo build --release -p openshell-gateway --no-default-features --features compute-driver-docker,compute-driver-vm
 
-# Windows MXC only, with telemetry support and bundled Z3.
-cargo build --release -p openshell-gateway --no-default-features --features telemetry,compute-driver-mxc,bundled-z3
+# Windows MXC only, with telemetry support and prebuilt Z3.
+cargo build --release -p openshell-gateway --no-default-features --features telemetry,compute-driver-mxc,openshell-server/prebuilt-z3
 ```
 
 Regular builds retain their platform driver set through the default `in-tree-compute-drivers` compatibility feature. On Windows, `compute-driver-mxc` selects MXC; the other four features install unsupported-driver stubs. On other platforms, MXC is excluded.

architecture/build.md

@@ -82,8 +82,8 @@ already satisfies Linux distribution trust-store policy.
 
 The workspace uses `z3` versions whose `z3-sys` dependency keeps downloader
 HTTP/TLS support behind explicit build features, so default system-Z3 builds do
-not reintroduce bundled Mozilla roots. Release builds that need bundled Z3
-continue to opt in with `bundled-z3`.
+not reintroduce bundled Mozilla roots. Windows builds can explicitly select the
+prebuilt Z3 release path.
 
 ## Linux Runtime Environments
 
@@ -92,9 +92,9 @@ The standalone `openshell` CLI is built as a static musl binary so it can run on
 a wide range of Linux distributions without depending on the host's glibc. Host
 runtime binaries that use the GNU/Linux runtime environment are GNU-linked.
 `openshell-gateway` and `openshell-driver-vm` are built with a glibc 2.28 floor.
-The gateway bundles z3 into the release binary so Linux packages, standalone
-tarballs, and gateway images do not depend on distro-specific z3 shared-library
-SONAMEs.
+The gateway statically links the target-specific Z3 library supplied by the Nix
+toolchain so Linux packages, standalone tarballs, and gateway images do not
+depend on distro-specific Z3 shared-library SONAMEs.
 
 The supervisor is the one binary whose libc is selectable, because it is the one
 binary executed inside a userland OpenShell does not control. `SUPERVISOR_LIBC`
@@ -138,12 +138,12 @@ otherwise fail with `ProcessFdQuotaExceeded` under macOS's default soft limit of
 256. The guard is a no-op on Linux and when `cargo-zigbuild` is absent. Gateway
 binaries use `cargo zigbuild` with GNU targets pinned to glibc 2.28, including
 native-architecture builds, so the gateway image, standalone tarballs, and Linux
-packages share the same host portability floor. The gateway build enables
-`bundled-z3`. Linux VM driver release artifacts use the same glibc floor so
-package-managed VM support does not raise the package runtime requirement.
-Gateway staging and release workflows set up the Zig C/C++ wrapper before
-bundled Z3 builds and verify the maximum referenced `GLIBC_*` symbol version
-before publishing or copying artifacts.
+packages share the same host portability floor. The gateway build links the
+target-specific static Z3 library from the Nix toolchain. Linux VM driver
+release artifacts use the same glibc floor so package-managed VM support does
+not raise the package runtime requirement. Gateway staging and release
+workflows use the target-specific C/C++ toolchain and verify the maximum
+referenced `GLIBC_*` symbol version before publishing or copying artifacts.
 Supervisor binaries are static in every configuration. The default `musl`
 variant uses `cargo zigbuild` when available, including native CPU
 architectures, so C dependencies are compiled for the musl target instead of the
@@ -217,10 +217,8 @@ Runtime layout:
 - **Gateway**: `gcr.io/distroless/cc-debian13:nonroot` base, GNU-linked binary at
   `/usr/local/bin/openshell-gateway`, runs as UID/GID `1000:1000`. Linux GNU
   gateway binaries must not reference `GLIBC_*` symbols newer than
-  `GLIBC_2.28`; release workflows verify this before publishing artifacts. The
-  gateway bundles z3, so the image does not need a distro-provided z3 runtime.
-  The base is pinned to a multi-architecture digest; distro security updates
-  require refreshing that digest and rebuilding the gateway image.
+  `GLIBC_2.28`; release workflows verify this before publishing artifacts. Z3
+  is statically linked, so the image does not need a distro-provided Z3 runtime.
 - **VM driver**: host GNU-linked binary installed at
   `/usr/libexec/openshell/openshell-driver-vm` in Linux packages and published
   as a release artifact. Linux GNU VM driver binaries must not reference

crates/openshell-gateway/Cargo.toml

@@ -72,7 +72,6 @@ telemetry = ["openshell-core/telemetry", "openshell-server/telemetry"]
 ## telemetry-on build. Kept in sync with `default` by
 ## `rust:verify:defaults-without-telemetry`.
 defaults-without-telemetry = ["in-tree-compute-drivers"]
-bundled-z3 = ["openshell-server/bundled-z3"]
 
 [lints]
 workspace = true

crates/openshell-prover/Cargo.toml

@@ -11,7 +11,6 @@ license.workspace = true
 repository.workspace = true
 
 [features]
-bundled-z3 = ["z3/bundled"]
 prebuilt-z3 = ["z3/gh-release"]
 
 [dependencies]

crates/openshell-server/Cargo.toml

@@ -119,7 +119,6 @@ default = ["telemetry"]
 ## On by default; build with `--no-default-features` for a telemetry-free gateway
 ## that contains no telemetry endpoint, HTTP client, or emission code.
 telemetry = ["openshell-core/telemetry"]
-bundled-z3 = ["openshell-prover/bundled-z3"]
 prebuilt-z3 = ["openshell-prover/prebuilt-z3"]
 test-support = []