chore(build): remove bundled Z3 support

Signed-off-by: Simon Scatton <sscatton@nvidia.com>

Author: SDAChess

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

@@ -115,7 +115,7 @@ The lane targets a Windows host with Visual Studio Build Tools and rustup.
 | Visual C++ ARM64 tools | `vswhere -latest -products * -requires Microsoft.VisualStudio.Component.VC.Tools.ARM64 -property installationPath` | Required for native ARM64 check, build, and tests and for x64-to-ARM64 check/build. Tests always require a native runner. |
 | Visual C++ ARM64 Spectre-mitigated libraries | `vswhere -latest -products * -requires Microsoft.VisualStudio.Component.VC.Runtimes.ARM64.Spectre -property installationPath` | Required by `regorus` through `msvc_spectre_libs`; the build fails when the selected MSVC toolset lacks `lib\spectre\arm64`. |
 | Visual C++ Clang tools | `vswhere -latest -products * -requires Microsoft.VisualStudio.Component.VC.Llvm.Clang -property installationPath` | Provides host-native `libclang.dll` for `bindgen` and `clang-cl.exe` for ARM64 crypto dependencies such as `aws-lc-sys`. On ARM64, the wrapper uses `VC\Tools\Llvm\Arm64\bin`. |
-| Visual C++ CMake tools | `vswhere -latest -products * -requires Microsoft.VisualStudio.Component.VC.CMake.Project -property installationPath` | Provides CMake and Ninja for bundled Z3 and other native dependencies. The x64-to-ARM64 path adds Ninja to `PATH`; Z3 uses MSVC's Visual Studio generator. |
+| Visual C++ CMake tools | `vswhere -latest -products * -requires Microsoft.VisualStudio.Component.VC.CMake.Project -property installationPath` | Provides CMake and Ninja for native dependencies. The x64-to-ARM64 path adds Ninja to `PATH`; Z3 uses an architecture-specific prebuilt release. |
 | Windows SDK | `where.exe rc.exe` from a Developer PowerShell | Install an SDK containing target libraries and ARM64 tools. |
 | Rust via rustup | `rustc --version` | Add each target being validated: `x86_64-pc-windows-msvc` and/or `aarch64-pc-windows-msvc`. The wrapper also adds the selected target. |
 | mise | `mise --version` | Used as a task runner only. |
@@ -203,8 +203,7 @@ jobs in the current mirror push run, or push a new mirrored commit. The binaries
 The ARM64 check/build steps in this x64-host contract are cross-builds. The
 wrapper discovers and adds host-native LLVM and Ninja to `PATH`, requires the
 ARM64 compiler and Spectre-mitigated libraries, lets ARM64 crypto crates select
-`clang-cl`, and builds bundled Z3 with native MSVC `cl.exe` and the Visual
-Studio generator.
+`clang-cl`, and downloads the official prebuilt ARM64 Z3 static library.
 
 On ARM64 hosts, validate the native ARM64 check, build, and test path. The
 wrapper rejects test targets that do not match the host architecture, so x64
@@ -259,7 +258,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 |
 |---|---|---|
@@ -311,12 +310,13 @@ Useful log files:
 | `test-x86_64-pc-windows-msvc-unsupported-*.log` | Focused unsupported-driver contract output. |
 | `test-aarch64-pc-windows-msvc-unsupported-*.log` | Focused native ARM64 contract output. |
 
-The first check builds bundled Z3 from source through `z3-sys`. Cargo stores the
-native build output in its target tree, so the Windows target cache reuses it.
-The resulting release executables do not require `libz3.dll`. The artifact
-report computes SHA256 through .NET directly and does not rely on the
-`Get-FileHash` module being available inside the mise-launched Windows
-PowerShell process.
+The first check downloads the pinned official Z3 archive for the target
+architecture through `z3-sys`. GitHub Actions authenticates the lookup with its
+read-only workflow token; local users can set `READ_ONLY_GITHUB_TOKEN` if an
+unauthenticated lookup is rate-limited. Cargo stores the extracted library in
+its target tree, so the Windows target cache reuses it. The artifact report
+computes SHA256 through .NET directly and does not rely on the `Get-FileHash`
+module being available inside the mise-launched Windows PowerShell process.
 
 ## Common Fix Patterns
 

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

@@ -68,11 +68,11 @@ file.
 For ARM64, verify the Visual Studio instance contains the ARM64 MSVC tools,
 ARM64 Spectre-mitigated libraries, Clang tools, CMake tools, and a Windows SDK.
 Clang supplies host-native `libclang.dll` for `bindgen` and `clang-cl.exe` for
-ARM64 crypto dependencies such as `aws-lc-sys`. Native builds use the normal
-bundled-Z3 CMake path. An x64-to-ARM64 check/build discovers and adds
-host-native Ninja to `PATH`, builds bundled Z3 with native MSVC `cl.exe` and
-the Visual Studio generator, and lets the crypto crates select `clang-cl`. Use
-a short `CARGO_TARGET_DIR` if Windows path-length limits are reached.
+ARM64 crypto dependencies such as `aws-lc-sys`. Native and x64-to-ARM64 builds
+use the official prebuilt Z3 4.16.0 static library for the target architecture.
+An x64-to-ARM64 check/build discovers and adds host-native Ninja to `PATH`,
+while the crypto crates select `clang-cl`. Use a short `CARGO_TARGET_DIR` if
+Windows path-length limits are reached.
 
 ## Unsupported Driver Rules
 

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,18 +330,15 @@ 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:
 
-- Bundled Z3 (the default for `windows:*` tasks): `z3-sys` builds Z3 from
-  source and links it into the OpenShell binaries. This keeps the release
-  executables independent of `libz3.dll` when they are copied to another host.
+- Prebuilt Z3 (the default for `windows:*` tasks): `z3-sys` downloads the
+  pinned Z3 4.16.0 GitHub release for the target architecture on the first
+  build. Cargo reuses the extracted archive from its target directory. Windows
+  CI authenticates the GitHub API request with `READ_ONLY_GITHUB_TOKEN` and
+  preserves the archive in the architecture-specific Cargo target cache. For
+  cold local builds, you may set `READ_ONLY_GITHUB_TOKEN` to avoid anonymous
+  GitHub API rate limits.
 - System Z3: point `Z3_LIBRARY_PATH_OVERRIDE` at the directory containing the
   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
@@ -353,24 +349,24 @@ For x86-64 and ARM64 Windows MSVC builds, use one of these Z3 paths:
 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
 
 To build the full set of Windows binaries, including `openshell-gateway.exe`
 and `openshell.exe`, use the `windows:build:x64` mise task instead of a
-single-crate `cargo build`. It builds Z3 from source (bundled) by default. A full
-build also compiles crates that use `bindgen` (e.g. the MXC driver on Windows),
-so it requires `libclang.dll`; if LLVM is not on the default search path, set
-`LIBCLANG_PATH` to the directory containing `libclang.dll`:
+single-crate `cargo build`. It downloads the pinned prebuilt Z3 release by
+default. A full build also compiles crates that use `bindgen` (e.g. the MXC
+driver on Windows), so it requires `libclang.dll`; if LLVM is not on the default
+search path, set `LIBCLANG_PATH` to the directory containing `libclang.dll`:
 
 ```powershell
 $env:LIBCLANG_PATH='C:\Program Files\Microsoft Visual Studio\2022\<Edition>\VC\Tools\Llvm\x64\bin'
 mise run --skip-tools windows:build:x64
 ```
 
-To use a local x64 Z3 release instead of the bundled build, set
+To use a local x64 Z3 release instead of the prebuilt download, set
 `Z3_LIBRARY_PATH_OVERRIDE` and `Z3_SYS_Z3_HEADER` before running the task:
 
 ```powershell

Cargo.lock

@@ -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]

Cargo.toml

@@ -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.

README.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,8 +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.
+  `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.
   The base is pinned to a multi-architecture digest; distro security updates
   require refreshing that digest and rebuilding the gateway image.
 - **VM driver**: host GNU-linked binary installed at

architecture/build.md

@@ -110,13 +110,15 @@ packaging-asset tests; its
 cross-platform Python, Markdown, license, and documentation checks still run.
 Test tasks require the Rust target architecture to match the Windows host, so
 an ARM64 test result is native coverage rather than x64 emulation coverage.
-By default it enables bundled Z3 for reproducible Windows builds. `z3-sys`
-builds Z3 from source and links it into the release binaries, so copying
-`openshell-gateway.exe` and `openshell.exe` does not create an undeclared
-`libz3.dll` runtime dependency. When `Z3_LIBRARY_PATH_OVERRIDE` points at a
-directory containing `libz3.lib`, the wrapper uses that system Z3 instead and
-requires `Z3_SYS_Z3_HEADER` to point at the full path to `z3.h`. Binaries built
-against a dynamic system Z3 must be deployed with the matching `libz3.dll`.
+By default it enables the `z3-sys` prebuilt-release feature and pins Z3 4.16.0.
+On a clean target directory, `z3-sys` downloads the official static library for
+the selected Windows architecture instead of compiling Z3 through
+CMake/MSBuild. GitHub Actions supplies its read-only workflow token for the
+release lookup, and the Cargo target cache preserves the extracted library for
+subsequent runs. When `Z3_LIBRARY_PATH_OVERRIDE` points at a directory
+containing `libz3.lib`, the wrapper uses that system Z3 instead and requires
+`Z3_SYS_Z3_HEADER` to point at the full path to `z3.h`. Local clean builds use
+the unauthenticated GitHub API unless `READ_ONLY_GITHUB_TOKEN` is set.
 
 GitHub Actions layers the Cargo target cache with sccache's GitHub Actions
 backend. The target cache lets Cargo skip intact dependency builds; sccache
@@ -136,10 +138,10 @@ Spectre-mitigated libraries, host-native Clang tools, CMake tools, and an
 ARM64-capable Windows SDK. Clang provides `libclang.dll` for `bindgen` and
 `clang-cl.exe` for ARM64 crypto dependencies. During x64-to-ARM64 check/build,
 the wrapper discovers and adds the Visual Studio-bundled Ninja to `PATH` for
-native dependencies. Bundled Z3 uses native MSVC `cl.exe` with the Visual
-Studio generator, while the crypto crates select `clang-cl`. Artifact hashing
-uses .NET SHA256 directly because module autoloading in the mise-launched
-Windows PowerShell process is not guaranteed.
+native dependencies. Z3 uses the official prebuilt ARM64 static library, so it
+does not inherit compiler settings from those native dependencies. Artifact
+hashing uses .NET SHA256 directly because module autoloading in the
+mise-launched Windows PowerShell process is not guaranteed.
 
 The wrapper defaults Cargo compilation to four jobs. Set
 `OPENSHELL_WINDOWS_BUILD_JOBS` to a positive integer to override that limit.

architecture/windows-msvc-build.md

@@ -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-gateway/Cargo.toml

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