fix(windows): avoid rate-limited Z3 source lookup

Signed-off-by: Shailendra Singh <shailendras@nvidia.com>
Signed-off-by: Akber Raza <akberr@nvidia.com>

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

@@ -60,6 +60,7 @@ The skill reads these environment variables (PowerShell syntax):
 | `$env:OPENSHELL_WXC_EXEC_PATH` | unset | Optional path to `wxc-exec.exe`. Validated for existence and architecture match only. Not used in this build-only skill. |
 | `$env:OPENSHELL_MXC_SKIP_ARM64` | `0` | Set to `1` to skip aarch64 build (e.g., for fast x64-only iterations). |
 | `$env:OPENSHELL_MXC_FORK_BRANCH` | `windows-mxc-build` | Branch name created in the fork. |
+| `$env:Z3_SYS_BUNDLED_DIR_OVERRIDE` | pinned source cached under `CARGO_TARGET_DIR` | Reuse an existing Z3 source tree containing `src/api/z3.h`; otherwise the wrapper fetches and caches the pinned revision automatically. |
 
 ## Workflow
 
@@ -195,6 +196,11 @@ The PowerShell wrapper must:
 
 Use `mise run --skip-tools windows:*` in GitHub Actions and local Windows automation. `--skip-tools` is intentional: this repo should not ask mise to install Rust on Windows because the MSVC flow relies on rustup plus Visual Studio Build Tools.
 
+For bundled Z3, the wrapper fetches the revision pinned by `z3-sys` through
+Git, caches it under `CARGO_TARGET_DIR`, and sets
+`Z3_SYS_BUNDLED_DIR_OVERRIDE`. This bypasses the unauthenticated GitHub
+Contents API lookup that can fail with HTTP 403 on shared networks.
+
 ### Step 6: mise check on x86_64-pc-windows-msvc
 
 ```powershell

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

@@ -78,6 +78,12 @@ Same pattern — gate with `#[cfg(unix)]`.
 
 `libsecret` only works on Linux. If `openshell-providers` pulls it in, gate it. The build-only skill does not need credential storage on Windows; that is a follow-on skill.
 
+### Bundled Z3 fails with HTTP 403
+
+The wrapper should fetch the pinned Z3 revision through Git before Cargo starts.
+If that prefetch fails, inspect the reported partial checkout and verify that
+Git can reach `https://github.com/Z3Prover/z3.git`.
+
 ## Cfg gating patterns
 
 ### Module-level
@@ -181,6 +187,11 @@ native MSVC `cl.exe` with Ninja. Use a short `CARGO_TARGET_DIR` if Windows
 path-length limits are reached. Test tasks reject a target that does not match
 the Windows host architecture.
 
+Bundled Z3 source is pinned by revision, fetched through Git, and cached under
+`CARGO_TARGET_DIR`. The wrapper sets `Z3_SYS_BUNDLED_DIR_OVERRIDE` so `z3-sys`
+does not make an unauthenticated GitHub Contents API call. An explicit override
+must point to a source tree containing `src/api/z3.h`.
+
 ## What NOT to do in this skill
 
 - Do not implement named-pipe IPC. Stubs only. (Belongs to the follow-on MXC driver skill.)

architecture/windows-msvc-build.md

@@ -64,7 +64,13 @@ an ARM64 test result is native coverage rather than x64 emulation coverage.
 By default it enables bundled Z3 for reproducible Windows builds. 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`.
+the full path to `z3.h`. For bundled builds, the wrapper fetches the Z3 source
+revision pinned by `z3-sys` through Git, caches it under `CARGO_TARGET_DIR`, and
+sets `Z3_SYS_BUNDLED_DIR_OVERRIDE`. This avoids the unauthenticated GitHub API
+lookup in the `z3-sys` build script, which can fail with HTTP 403 when a shared
+runner or developer network exhausts its API rate limit. An explicitly set
+`Z3_SYS_BUNDLED_DIR_OVERRIDE` remains supported and must contain
+`src/api/z3.h`.
 
 The lane uses `mise run --skip-tools windows:*` because Windows Rust comes from
 rustup and linking comes from Visual Studio Build Tools. Mise orchestrates the

tasks/scripts/windows-msvc.ps1

@@ -40,6 +40,10 @@ if ([string]::IsNullOrWhiteSpace($TargetDir)) {
 $UnsupportedDriverPackageExcludes = "--exclude openshell-driver-docker --exclude openshell-driver-kubernetes --exclude openshell-driver-podman --exclude openshell-driver-vm"
 $BundledZ3WorkspaceFeatures = "--features openshell-prover/bundled-z3"
 $BundledZ3ServerFeatures = "--features openshell-server/bundled-z3,openshell-prover/bundled-z3"
+$BundledZ3Repository = "https://github.com/Z3Prover/z3.git"
+$BundledZ3SysVersion = "0.10.9"
+# This is the matching z3-sys submodule revision. Update both pins together.
+$BundledZ3Revision = "ddb49568d3520e99799e364fb22f35fc67d887b1"
 $Z3WorkspaceFeatures = $BundledZ3WorkspaceFeatures
 $Z3ServerFeatures = $BundledZ3ServerFeatures
 
@@ -330,9 +334,87 @@ function Resolve-Z3HeaderPath([string] $HeaderPath) {
     return (Resolve-Path $HeaderPath).Path
 }
 
+function Assert-BundledZ3Source([string] $SourcePath, [string] $ExpectedRevision) {
+    if (-not (Test-Path $SourcePath -PathType Container)) {
+        throw "Bundled Z3 source directory does not exist: $SourcePath"
+    }
+
+    $header = Join-Path $SourcePath "src\api\z3.h"
+    if (-not (Test-Path $header -PathType Leaf)) {
+        throw "Bundled Z3 source directory does not contain src\api\z3.h: $SourcePath"
+    }
+
+    if (-not [string]::IsNullOrWhiteSpace($ExpectedRevision)) {
+        $actualRevision = (& git -C $SourcePath rev-parse HEAD 2>$null)
+        if ($LASTEXITCODE -ne 0 -or [string]::IsNullOrWhiteSpace($actualRevision)) {
+            throw "Could not verify the bundled Z3 source revision at: $SourcePath"
+        }
+        if ($actualRevision.Trim() -ne $ExpectedRevision) {
+            throw "Bundled Z3 source revision mismatch at ${SourcePath}: expected $ExpectedRevision, found $($actualRevision.Trim())"
+        }
+    }
+
+    return (Resolve-Path $SourcePath).Path
+}
+
+function Resolve-BundledZ3Source {
+    if (-not [string]::IsNullOrWhiteSpace($env:Z3_SYS_BUNDLED_DIR_OVERRIDE)) {
+        return Assert-BundledZ3Source $env:Z3_SYS_BUNDLED_DIR_OVERRIDE ""
+    }
+
+    $cargoLock = Get-Content (Join-Path $RepoRoot "Cargo.lock") -Raw
+    $packagePattern = '(?ms)^\[\[package\]\]\s+name = "z3-sys"\s+version = "([^"]+)"'
+    $packageMatches = [regex]::Matches($cargoLock, $packagePattern)
+    if ($packageMatches.Count -ne 1 -or $packageMatches[0].Groups[1].Value -ne $BundledZ3SysVersion) {
+        throw "Bundled Z3 source pin expects z3-sys $BundledZ3SysVersion. Update the version and revision pins for the z3-sys version in Cargo.lock."
+    }
+
+    $revisionPrefix = $BundledZ3Revision.Substring(0, 12)
+    $sourcePath = Join-Path $TargetDir "z3-source-$revisionPrefix"
+    if (Test-Path $sourcePath) {
+        return Assert-BundledZ3Source $sourcePath $BundledZ3Revision
+    }
+
+    if (-not (Get-Command git.exe -ErrorAction SilentlyContinue)) {
+        throw "Bundled Z3 source preparation requires git.exe on PATH."
+    }
+    if (-not (Test-Path $TargetDir -PathType Container)) {
+        New-Item -ItemType Directory -Force -Path $TargetDir | Out-Null
+    }
+
+    $stagingPath = "$sourcePath.partial-$([guid]::NewGuid().ToString('N'))"
+    Write-Host "==> Fetching bundled Z3 source"
+    Write-Host "    repository: $BundledZ3Repository"
+    Write-Host "    revision:   $BundledZ3Revision"
+    Write-Host "    cache:      $sourcePath"
+
+    & git init --quiet $stagingPath
+    if ($LASTEXITCODE -ne 0) {
+        throw "git init failed while preparing bundled Z3 source at: $stagingPath"
+    }
+    & git -C $stagingPath remote add origin $BundledZ3Repository
+    if ($LASTEXITCODE -ne 0) {
+        throw "git remote add failed while preparing bundled Z3 source at: $stagingPath"
+    }
+    & git -C $stagingPath fetch --quiet --depth 1 origin $BundledZ3Revision
+    if ($LASTEXITCODE -ne 0) {
+        throw "git fetch failed for bundled Z3 revision $BundledZ3Revision. Partial source remains at: $stagingPath"
+    }
+    & git -C $stagingPath checkout --quiet --detach FETCH_HEAD
+    if ($LASTEXITCODE -ne 0) {
+        throw "git checkout failed for bundled Z3 revision $BundledZ3Revision. Partial source remains at: $stagingPath"
+    }
+
+    Assert-BundledZ3Source $stagingPath $BundledZ3Revision | Out-Null
+    Move-Item -Path $stagingPath -Destination $sourcePath
+    return Assert-BundledZ3Source $sourcePath $BundledZ3Revision
+}
+
 function Configure-Z3 {
     if ([string]::IsNullOrWhiteSpace($env:Z3_LIBRARY_PATH_OVERRIDE)) {
         Write-Host "==> Z3: bundled"
+        $env:Z3_SYS_BUNDLED_DIR_OVERRIDE = Resolve-BundledZ3Source
+        Write-Host "    Z3_SYS_BUNDLED_DIR_OVERRIDE=$env:Z3_SYS_BUNDLED_DIR_OVERRIDE"
         return [pscustomobject]@{
             WorkspaceFeatures = $BundledZ3WorkspaceFeatures
             ServerFeatures = $BundledZ3ServerFeatures