fix(docker): add openshell-prover to Dockerfile skeleton stages and provide z3

.github/workflows/release-dev.yml

@@ -149,6 +149,9 @@ jobs:
 
   # ---------------------------------------------------------------------------
   # Build CLI binaries (Linux musl — static, native on each arch)
+  #
+  # Builds run directly on the CI host (glibc Ubuntu).  Zig provides musl
+  # C/C++ toolchains for bundled-z3 and ring, and is also used as the linker.
   # ---------------------------------------------------------------------------
   build-cli-linux:
     name: Build CLI (Linux ${{ matrix.arch }})
@@ -159,9 +162,11 @@ jobs:
           - arch: amd64
             runner: build-amd64
             target: x86_64-unknown-linux-musl
+            zig_target: x86_64-linux-musl
           - arch: arm64
             runner: build-arm64
             target: aarch64-unknown-linux-musl
+            zig_target: aarch64-linux-musl
     runs-on: ${{ matrix.runner }}
     timeout-minutes: 60
     container:
@@ -195,23 +200,44 @@ jobs:
           cache-directories: .cache/sccache
           cache-targets: "true"
 
-      - name: Install musl toolchain
+      - name: Add Rust musl target
+        run: mise x -- rustup target add ${{ matrix.target }}
+
+      - name: Set up zig musl wrappers
         run: |
           set -euo pipefail
-          apt-get update
-          apt-get install -y --no-install-recommends musl-tools
-          rm -rf /var/lib/apt/lists/*
+          ZIG="$(mise which zig)"
+          ZIG_TARGET="${{ matrix.zig_target }}"
+          mkdir -p /tmp/zig-musl
+
+          # cc-rs injects --target=<rust-triple> (for example
+          # aarch64-unknown-linux-musl), which zig does not parse.  Strip any
+          # caller-provided --target and use the wrapper's zig-native target.
+          for tool in cc c++; do
+            printf '#!/bin/bash\nargs=()\nfor arg in "$@"; do\n  case "$arg" in\n    --target=*) ;;\n    *) args+=("$arg") ;;\n  esac\ndone\nexec "%s" %s --target=%s "${args[@]}"\n' \
+              "$ZIG" "$tool" "$ZIG_TARGET" > "/tmp/zig-musl/${tool}"
+            chmod +x "/tmp/zig-musl/${tool}"
+          done
 
-      - name: Add Rust musl target
-        run: mise x -- rustup target add ${{ matrix.target }}
+          TARGET_ENV=$(echo "${{ matrix.target }}" | tr '-' '_')
+          TARGET_ENV_UPPER=${TARGET_ENV^^}
+
+          # Use zig for C/C++ compilation and final linking.
+          echo "CC_${TARGET_ENV}=/tmp/zig-musl/cc" >> "$GITHUB_ENV"
+          echo "CXX_${TARGET_ENV}=/tmp/zig-musl/c++" >> "$GITHUB_ENV"
+          echo "CARGO_TARGET_${TARGET_ENV_UPPER}_LINKER=/tmp/zig-musl/cc" >> "$GITHUB_ENV"
+
+          # Let zig own CRT/startfiles to avoid duplicate _start symbols.
+          echo "CARGO_TARGET_${TARGET_ENV_UPPER}_RUSTFLAGS=-Clink-self-contained=no" >> "$GITHUB_ENV"
+
+          # z3 built with zig c++ uses libc++ symbols (std::__1::*).
+          # Override z3-sys default (stdc++) so Rust links the matching runtime.
+          echo "CXXSTDLIB=c++" >> "$GITHUB_ENV"
 
       - name: Scope workspace to CLI crates
         run: |
           set -euo pipefail
-          # Remove workspace members that are not needed for openshell-cli.
-          # This avoids Cargo feature-unification pulling in aws-lc-sys (via
-          # russh in openshell-sandbox / openshell-server).
-          sed -i 's|members = \["crates/\*"\]|members = ["crates/openshell-cli", "crates/openshell-core", "crates/openshell-bootstrap", "crates/openshell-policy", "crates/openshell-providers", "crates/openshell-tui"]|' Cargo.toml
+          sed -i 's|members = \["crates/\*"\]|members = ["crates/openshell-cli", "crates/openshell-core", "crates/openshell-bootstrap", "crates/openshell-policy", "crates/openshell-prover", "crates/openshell-providers", "crates/openshell-tui"]|' Cargo.toml
 
       - name: Patch workspace version
         if: needs.compute-versions.outputs.cargo_version != ''
@@ -220,7 +246,7 @@ jobs:
           sed -i -E '/^\[workspace\.package\]/,/^\[/{s/^version[[:space:]]*=[[:space:]]*".*"/version = "'"${{ needs.compute-versions.outputs.cargo_version }}"'"/}' Cargo.toml
 
       - name: Build ${{ matrix.target }}
-        run: mise x -- cargo build --release --target ${{ matrix.target }} -p openshell-cli
+        run: mise x -- cargo build --release --target ${{ matrix.target }} -p openshell-cli --features bundled-z3
 
       - name: sccache stats
         if: always()

.github/workflows/release-tag.yml

@@ -170,6 +170,9 @@ jobs:
 
   # ---------------------------------------------------------------------------
   # Build CLI binaries (Linux musl — static, native on each arch)
+  #
+  # Builds run directly on the CI host (glibc Ubuntu).  Zig provides musl
+  # C/C++ toolchains for bundled-z3 and ring, and is also used as the linker.
   # ---------------------------------------------------------------------------
   build-cli-linux:
     name: Build CLI (Linux ${{ matrix.arch }})
@@ -180,9 +183,11 @@ jobs:
           - arch: amd64
             runner: build-amd64
             target: x86_64-unknown-linux-musl
+            zig_target: x86_64-linux-musl
           - arch: arm64
             runner: build-arm64
             target: aarch64-unknown-linux-musl
+            zig_target: aarch64-linux-musl
     runs-on: ${{ matrix.runner }}
     timeout-minutes: 60
     container:
@@ -217,23 +222,44 @@ jobs:
           cache-directories: .cache/sccache
           cache-targets: "true"
 
-      - name: Install musl toolchain
+      - name: Add Rust musl target
+        run: mise x -- rustup target add ${{ matrix.target }}
+
+      - name: Set up zig musl wrappers
         run: |
           set -euo pipefail
-          apt-get update
-          apt-get install -y --no-install-recommends musl-tools
-          rm -rf /var/lib/apt/lists/*
+          ZIG="$(mise which zig)"
+          ZIG_TARGET="${{ matrix.zig_target }}"
+          mkdir -p /tmp/zig-musl
+
+          # cc-rs injects --target=<rust-triple> (for example
+          # aarch64-unknown-linux-musl), which zig does not parse.  Strip any
+          # caller-provided --target and use the wrapper's zig-native target.
+          for tool in cc c++; do
+            printf '#!/bin/bash\nargs=()\nfor arg in "$@"; do\n  case "$arg" in\n    --target=*) ;;\n    *) args+=("$arg") ;;\n  esac\ndone\nexec "%s" %s --target=%s "${args[@]}"\n' \
+              "$ZIG" "$tool" "$ZIG_TARGET" > "/tmp/zig-musl/${tool}"
+            chmod +x "/tmp/zig-musl/${tool}"
+          done
 
-      - name: Add Rust musl target
-        run: mise x -- rustup target add ${{ matrix.target }}
+          TARGET_ENV=$(echo "${{ matrix.target }}" | tr '-' '_')
+          TARGET_ENV_UPPER=${TARGET_ENV^^}
+
+          # Use zig for C/C++ compilation and final linking.
+          echo "CC_${TARGET_ENV}=/tmp/zig-musl/cc" >> "$GITHUB_ENV"
+          echo "CXX_${TARGET_ENV}=/tmp/zig-musl/c++" >> "$GITHUB_ENV"
+          echo "CARGO_TARGET_${TARGET_ENV_UPPER}_LINKER=/tmp/zig-musl/cc" >> "$GITHUB_ENV"
+
+          # Let zig own CRT/startfiles to avoid duplicate _start symbols.
+          echo "CARGO_TARGET_${TARGET_ENV_UPPER}_RUSTFLAGS=-Clink-self-contained=no" >> "$GITHUB_ENV"
+
+          # z3 built with zig c++ uses libc++ symbols (std::__1::*).
+          # Override z3-sys default (stdc++) so Rust links the matching runtime.
+          echo "CXXSTDLIB=c++" >> "$GITHUB_ENV"
 
       - name: Scope workspace to CLI crates
         run: |
           set -euo pipefail
-          # Remove workspace members that are not needed for openshell-cli.
-          # This avoids Cargo feature-unification pulling in aws-lc-sys (via
-          # russh in openshell-sandbox / openshell-server).
-          sed -i 's|members = \["crates/\*"\]|members = ["crates/openshell-cli", "crates/openshell-core", "crates/openshell-bootstrap", "crates/openshell-policy", "crates/openshell-providers", "crates/openshell-tui"]|' Cargo.toml
+          sed -i 's|members = \["crates/\*"\]|members = ["crates/openshell-cli", "crates/openshell-core", "crates/openshell-bootstrap", "crates/openshell-policy", "crates/openshell-prover", "crates/openshell-providers", "crates/openshell-tui"]|' Cargo.toml
 
       - name: Patch workspace version
         if: needs.compute-versions.outputs.cargo_version != ''
@@ -242,7 +268,7 @@ jobs:
           sed -i -E '/^\[workspace\.package\]/,/^\[/{s/^version[[:space:]]*=[[:space:]]*".*"/version = "'"${{ needs.compute-versions.outputs.cargo_version }}"'"/}' Cargo.toml
 
       - name: Build ${{ matrix.target }}
-        run: mise x -- cargo build --release --target ${{ matrix.target }} -p openshell-cli
+        run: mise x -- cargo build --release --target ${{ matrix.target }} -p openshell-cli --features bundled-z3
 
       - name: sccache stats
         if: always()

crates/openshell-cli/Cargo.toml

@@ -76,6 +76,7 @@ tracing-subscriber = { workspace = true }
 workspace = true
 
 [features]
+bundled-z3 = ["openshell-prover/bundled-z3"]
 dev-settings = ["openshell-core/dev-settings"]
 
 [dev-dependencies]

deploy/docker/Dockerfile.cli-macos

@@ -25,12 +25,15 @@ ENV LD_LIBRARY_PATH="/osxcross/lib"
 
 COPY --from=osxcross /osxcross /osxcross
 
+RUN SDKROOT="$(echo /osxcross/SDK/MacOSX*.sdk)" && ln -sfn "${SDKROOT}" /osxcross/SDK/MacOSX.sdk
+
 RUN apt-get update && apt-get install -y --no-install-recommends \
     build-essential \
     ca-certificates \
     clang \
     cmake \
     curl \
+    libclang-dev \
     pkg-config \
     && rm -rf /var/lib/apt/lists/*
 
@@ -49,6 +52,11 @@ ENV CXX_aarch64_apple_darwin=oa64-clang++
 ENV AR_aarch64_apple_darwin=aarch64-apple-darwin25.1-ar
 ENV CARGO_TARGET_AARCH64_APPLE_DARWIN_LINKER=oa64-clang
 ENV CARGO_TARGET_AARCH64_APPLE_DARWIN_AR=aarch64-apple-darwin25.1-ar
+ENV SDKROOT=/osxcross/SDK/MacOSX.sdk
+ENV MACOSX_DEPLOYMENT_TARGET=13.3
+ENV CFLAGS_aarch64_apple_darwin=--target=arm64-apple-macosx\ -mmacosx-version-min=13.3
+ENV CXXFLAGS_aarch64_apple_darwin=--target=arm64-apple-macosx\ -mmacosx-version-min=13.3
+ENV BINDGEN_EXTRA_CLANG_ARGS_aarch64_apple_darwin=--target=arm64-apple-macosx\ -isysroot\ ${SDKROOT}
 
 # ---------------------------------------------------------------------------
 # Stage 1: dependency caching — copy only manifests, create dummy sources,
@@ -61,31 +69,34 @@ COPY crates/openshell-core/Cargo.toml     crates/openshell-core/Cargo.toml
 COPY crates/openshell-policy/Cargo.toml   crates/openshell-policy/Cargo.toml
 COPY crates/openshell-providers/Cargo.toml crates/openshell-providers/Cargo.toml
 COPY crates/openshell-tui/Cargo.toml      crates/openshell-tui/Cargo.toml
+COPY crates/openshell-prover/Cargo.toml   crates/openshell-prover/Cargo.toml
 COPY crates/openshell-core/build.rs       crates/openshell-core/build.rs
 COPY proto/ proto/
 
 # Scope workspace to CLI crates only — avoids compiling aws-lc-sys (pulled
 # by russh in openshell-sandbox/openshell-server) which is difficult to
 # cross-compile and unnecessary for the CLI binary.
-RUN sed -i 's|members = \["crates/\*"\]|members = ["crates/openshell-cli", "crates/openshell-core", "crates/openshell-bootstrap", "crates/openshell-policy", "crates/openshell-providers", "crates/openshell-tui"]|' Cargo.toml
+RUN sed -i 's|members = \["crates/\*"\]|members = ["crates/openshell-cli", "crates/openshell-core", "crates/openshell-bootstrap", "crates/openshell-policy", "crates/openshell-prover", "crates/openshell-providers", "crates/openshell-tui"]|' Cargo.toml
 
 RUN mkdir -p crates/openshell-cli/src \
              crates/openshell-core/src \
              crates/openshell-bootstrap/src \
              crates/openshell-policy/src \
              crates/openshell-providers/src \
+             crates/openshell-prover/src \
              crates/openshell-tui/src && \
     echo "fn main() {}" > crates/openshell-cli/src/main.rs && \
     touch crates/openshell-core/src/lib.rs && \
     touch crates/openshell-bootstrap/src/lib.rs && \
     touch crates/openshell-policy/src/lib.rs && \
     touch crates/openshell-providers/src/lib.rs && \
+    touch crates/openshell-prover/src/lib.rs && \
     touch crates/openshell-tui/src/lib.rs
 
 RUN --mount=type=cache,id=cargo-registry-cli-macos,sharing=locked,target=/root/.cargo/registry \
     --mount=type=cache,id=cargo-git-cli-macos,sharing=locked,target=/root/.cargo/git \
     --mount=type=cache,id=cargo-target-cli-macos-${CARGO_TARGET_CACHE_SCOPE},sharing=locked,target=/build/target \
-    cargo build --release --target aarch64-apple-darwin -p openshell-cli 2>/dev/null || true
+    cargo build --release --target aarch64-apple-darwin -p openshell-cli --features bundled-z3 2>/dev/null || true
 
 # ---------------------------------------------------------------------------
 # Stage 2: real build
@@ -113,7 +124,7 @@ RUN --mount=type=cache,id=cargo-registry-cli-macos,sharing=locked,target=/root/.
     if [ -n "${OPENSHELL_CARGO_VERSION:-}" ]; then \
       sed -i -E '/^\[workspace\.package\]/,/^\[/{s/^version[[:space:]]*=[[:space:]]*".*"/version = "'"${OPENSHELL_CARGO_VERSION}"'"/}' Cargo.toml; \
     fi && \
-    cargo build --release --target aarch64-apple-darwin -p openshell-cli && \
+    cargo build --release --target aarch64-apple-darwin -p openshell-cli --features bundled-z3 && \
     cp target/aarch64-apple-darwin/release/openshell /openshell
 
 FROM scratch AS binary

deploy/docker/Dockerfile.python-wheels

@@ -12,9 +12,11 @@ ENV PATH="/root/.cargo/bin:${PATH}"
 
 RUN apt-get update && apt-get install -y --no-install-recommends \
     build-essential \
+    cmake \
     curl \
     gcc \
     libc6-dev \
+    libclang-dev \
     pkg-config \
     libssl-dev \
     && rm -rf /var/lib/apt/lists/*
@@ -46,19 +48,25 @@ COPY crates/openshell-router/Cargo.toml crates/openshell-router/Cargo.toml
 COPY crates/openshell-sandbox/Cargo.toml crates/openshell-sandbox/Cargo.toml
 COPY crates/openshell-server/Cargo.toml crates/openshell-server/Cargo.toml
 COPY crates/openshell-bootstrap/Cargo.toml crates/openshell-bootstrap/Cargo.toml
+COPY crates/openshell-policy/Cargo.toml crates/openshell-policy/Cargo.toml
+COPY crates/openshell-prover/Cargo.toml crates/openshell-prover/Cargo.toml
+COPY crates/openshell-tui/Cargo.toml crates/openshell-tui/Cargo.toml
 COPY crates/openshell-core/build.rs crates/openshell-core/build.rs
 COPY proto/ proto/
 
 # Create dummy source files to build dependencies.
-RUN mkdir -p crates/openshell-cli/src crates/openshell-core/src crates/openshell-ocsf/src crates/openshell-providers/src crates/openshell-router/src crates/openshell-sandbox/src crates/openshell-server/src crates/openshell-bootstrap/src && \
+RUN mkdir -p crates/openshell-cli/src crates/openshell-core/src crates/openshell-ocsf/src crates/openshell-policy/src crates/openshell-providers/src crates/openshell-prover/src crates/openshell-router/src crates/openshell-sandbox/src crates/openshell-server/src crates/openshell-bootstrap/src crates/openshell-tui/src && \
     echo "fn main() {}" > crates/openshell-cli/src/main.rs && \
     echo "fn main() {}" > crates/openshell-sandbox/src/main.rs && \
     echo "fn main() {}" > crates/openshell-server/src/main.rs && \
     touch crates/openshell-core/src/lib.rs && \
     touch crates/openshell-ocsf/src/lib.rs && \
     touch crates/openshell-providers/src/lib.rs && \
     touch crates/openshell-router/src/lib.rs && \
-    touch crates/openshell-bootstrap/src/lib.rs
+    touch crates/openshell-bootstrap/src/lib.rs && \
+    touch crates/openshell-policy/src/lib.rs && \
+    touch crates/openshell-prover/src/lib.rs && \
+    touch crates/openshell-tui/src/lib.rs
 
 # Build dependencies only (cached unless Cargo.toml/lock changes).
 # sccache uses memcached in CI or the local disk cache mount for local dev.
@@ -67,7 +75,7 @@ RUN --mount=type=cache,id=cargo-registry-python-wheels-${TARGETARCH},sharing=loc
     --mount=type=cache,id=cargo-git-python-wheels-${TARGETARCH},sharing=locked,target=/root/.cargo/git \
     --mount=type=cache,id=cargo-target-python-wheels-${TARGETARCH}-${CARGO_TARGET_CACHE_SCOPE},sharing=locked,target=/build/target \
     --mount=type=cache,id=sccache-python-wheels-${TARGETARCH},sharing=locked,target=/tmp/sccache \
-    . cross-build.sh && cargo_cross_build --release -p openshell-cli 2>/dev/null || true
+    . cross-build.sh && cargo_cross_build --release -p openshell-cli --features bundled-z3 2>/dev/null || true
 
 # Copy actual source code and Python packaging files.
 COPY crates/ crates/
@@ -101,7 +109,7 @@ RUN --mount=type=cache,id=cargo-registry-python-wheels-${TARGETARCH},sharing=loc
     if [ -n "${OPENSHELL_CARGO_VERSION:-}" ]; then \
       sed -i -E '/^\[workspace\.package\]/,/^\[/{s/^version[[:space:]]*=[[:space:]]*".*"/version = "'"${OPENSHELL_CARGO_VERSION}"'"/}' Cargo.toml; \
     fi && \
-    maturin build --release --target "${CARGO_BUILD_TARGET}" --out /wheels
+    maturin build --release --target "${CARGO_BUILD_TARGET}" --features bundled-z3 --out /wheels
 
 FROM scratch AS wheels
 COPY --from=builder /wheels/*.whl /