feat: keep Windows Z3 builds fast without Ring

[pimlock]

User Story

As an OpenShell maintainer, I want Windows x64 and ARM64 builds to obtain Z3 without adding ring to the Rust dependency graph, so that Windows CI stays reasonably fast and the workspace can enforce its AWS-LC-only dependency policy without exceptions.

Problem Statement

The Windows MSVC lane enables openshell-prover/prebuilt-z3, which forwards to z3/gh-release. The z3-sys build script then downloads an architecture-matched Z3 4.16.0 release through this build-time dependency path:

z3-sys -> reqwest -> rustls -> ring

ring is used only by the host-side archive downloader and is not linked into the OpenShell binaries. Cargo still records it in Cargo.lock, and the all-features dependency graph includes it. deny.toml therefore needs a wrapper exception for ring through rustls and rustls-webpki.

Removing the prebuilt feature without a replacement is not practical. Earlier Windows CI measurements showed that compiling bundled Z3 from source increased a cold workflow from about 37 minutes to about 75 minutes. Windows validation covers both x64 and native ARM64, and the main workflow separates cache seeding from release builds.

Impact / Why This Matters

The current arrangement weakens the dependency policy. The wrapper exception constrains the immediate parents of ring, but it does not prove that ring is build-time-only. Any future runtime path through those same wrappers would also pass.

Manually omitting the ring edge from Cargo.lock is not a valid workaround. It leaves the lockfile stale and causes locked commands such as cargo vendor --locked to fail. Returning to uncached source compilation would preserve the dependency policy but roughly double clean Windows CI time based on the earlier measurements.

We need a Z3 provisioning path that preserves practical Windows build times while removing ring from the lockfile and all-features graph.

Proposed Design

Windows x64 and ARM64 validation should use an architecture-matched, statically linked Z3 version compatible with the Rust z3 crate. Z3 provisioning must have a reusable cache or use a verified prebuilt artifact so that normal CI runs do not compile Z3 repeatedly.

The selected path should work for pull-request lint and test jobs, main cache-seed jobs, and the dependent release-build jobs. Local Windows contributors should have a documented equivalent workflow or a clear automatic setup path.

Cargo's workspace feature graph must no longer enable the z3-sys GitHub-release downloader or any other dependency path that introduces ring.

Acceptance Criteria

• Cargo.lock contains no ring package.
• cargo tree --workspace --all-features --target all -i ring reports no dependency path.
• deny.toml uses an unconditional ring ban without a wrappers exception, and cargo deny check bans passes.
• Windows x64 and ARM64 lint, test, and release-build jobs pass with statically linked Z3.
• Z3 provisioning is pinned and integrity-checked for both architectures.
• Cache-seed and release-build jobs reuse the same architecture-specific Z3 result instead of rebuilding or downloading it independently.
• A repeated warm-cache Windows run remains within 20% of the current measured per-job and end-to-end times.
• A clean-cache run completes successfully and publishes a reusable Z3 result.
• The Windows build documentation explains CI provisioning and the local developer workflow.

Alternatives Considered

Build Z3 with pinned vcpkg and cache the result

Use the z3/vcpkg feature with a pinned vcpkg baseline and Z3 version. Build x64-windows-static-md and arm64-windows-static-md, then cache the compiled packages by architecture and compiler version.

This removes ring and avoids relying on upstream precompiled Z3 archives. It adds vcpkg versioning and cache management, and a cache miss still pays the full native Z3 compilation cost. GitHub's Windows x64 and ARM64 runner images already include vcpkg, but the repository should pin the registry/tooling rather than inherit a changing runner-image revision.

Download and verify the official Z3 archive before Cargo runs

Download the pinned x64 or ARM64 archive in the workflow, verify its published SHA-256 digest, and set Z3_LIBRARY_PATH_OVERRIDE plus Z3_SYS_Z3_HEADER. The existing Windows wrapper already supports this system-library path.

This is the smallest and fastest change. It removes ring from Cargo because Rust no longer performs the download, but it still relies on the same upstream prebuilt Z3 artifact.

Compile vendored Z3 through Cargo

Use z3/vendored and rely on the Cargo target cache. This removes ring and keeps provisioning inside Cargo, but earlier measurements showed about 75 minutes for a cold run versus about 37 minutes with prebuilt Z3. Warm builds were much closer, about 19 minutes versus 16 minutes.

Add configurable AWS-LC support to the z3-sys downloader

Change z3-sys upstream so its Reqwest client can use AWS-LC instead of Ring, then retain the GitHub-release path. This would preserve current provisioning behavior and speed, but depends on an upstream change and release. It also continues to rely on upstream prebuilt Z3 archives.

Bake Z3 into a runner image

A custom Windows runner image could provide Z3 for both architectures without per-job setup. This shifts the cost into runner-image maintenance and is a poor fit for the current GitHub-hosted x64 and ARM64 jobs.

Chocolatey and the third-party setup-z3 action are not suitable replacements because their documented Windows support does not cover the required pinned x64 and ARM64 combination. Chocolatey's package also repackages upstream prebuilt release files.

Agent Investigation

• The current feature mapping is in crates/openshell-prover/Cargo.toml: prebuilt-z3 = ["z3/gh-release"].
• tasks/scripts/windows-msvc.ps1 enables that feature by default, pins Z3 4.16.0, and already supports Z3_LIBRARY_PATH_OVERRIDE plus Z3_SYS_Z3_HEADER.
• .github/workflows/windows-msvc.yml runs Windows x64 on windows-2025 and native ARM64 on windows-11-arm, with separate PR, cache-seed, and release-build jobs.
• The build-time and cache measurements are recorded in PR #2738.
• Issue #1060 proposes OpenShell-hosted prebuilt Z3 artifacts for other packaging paths. It may provide a reusable artifact model, but it does not currently cover removing ring from the Windows all-features graph.
• PR #3267 repairs the currently stale lockfile. This issue concerns replacing the dependency path afterward, not omitting required lockfile edges.
• Z3 documents both source builds and vcpkg installation: https://github.com/Z3Prover/z3#building-z3-using-vcpkg
• vcpkg documents deterministic baselines and exact overrides: https://learn.microsoft.com/vcpkg/users/versioning

Checklist

• I've reviewed existing issues and the architecture docs.
• This is a design proposal, not a "please build this" request.

[pimlock]

@SDAChess FYI, I just discovered this after merging the windows CI change. The downloader for the prebuilt z3 uses ring transitively, so it gets included in our build graph. It's only a build dependency, but I feel it would be cleaner to change to something that doesn't use that at all.

There are some options from an agent in the description, it seems to recommend the z3/vcpkg path, but I want to check with you first.

[SDAChess]

Yeah vcpkg sounds good from what I'm seeing. Do you want to tackle this or should i?

[pimlock]

Thanks for checking @SDAChess! I'll run with it and send the PR to review.