Dockerfile.buildkit

# syntax=docker.io/docker/dockerfile:1

ARG TARGETPLATFORM=linux/amd64
ARG RUNTIME_MODE=minimal

# =============================================================================
# PANTHER IVY Tester - Modern Multi-Platform BuildKit Dockerfile
# Cross-platform formal verification with automatic platform detection
#
# Multi-stage architecture for optimal layer caching:
#   deps        -> shared toolchain (apt, pyenv, pip, external deps)
#   z3-builder  -> Z3 compilation (only rebuilds when submodules/z3 changes)
#   base        -> remaining builds (picotls, aiger, abc) + setup.py install
#   final       -> runtime metadata and healthcheck
# =============================================================================

# BuildKit automatic platform arguments
ARG BUILDPLATFORM
ARG TARGETPLATFORM
ARG TARGETOS=linux
ARG TARGETARCH
ARG BUILDVARIANT

# Base image configuration
ARG BASE_IMAGE=panther_base_service:latest

# Build configuration
ARG VERSION=master  # Default version, can be overridden
ARG DEPENDENCIES="[]"  # JSON-formatted list of dependencies
ARG BUILD_MODE=""  # Build mode for Z3 compilation: '', 'debug-asan', 'rel-lto', or 'release-static-pgo'
ARG Z3_SOURCE="local"  # Z3 source: 'local' builds from submodule, 'pip' uses pip z3-solver only

# =============================================================================
# STAGE 1: DEPS - Shared toolchain for all build stages
# =============================================================================

FROM --platform=$TARGETPLATFORM ${BASE_IMAGE} AS deps

# Re-declare ARGs after FROM to make them available in this stage
ARG DEPENDENCIES
ARG TARGETARCH
ARG BUILDPLATFORM
ARG TARGETPLATFORM

ENV DEBIAN_FRONTEND=noninteractive
ENV DEPENDENCIES=${DEPENDENCIES}
ENV TARGETPLATFORM=${TARGETPLATFORM}

RUN bash -c '\
  cat /etc/os-release; \
  echo "---- sources.list ----"; cat /etc/apt/sources.list; \
  ls /etc/apt/sources.list.d || true'

# APT package installation with cache mounts for Ubuntu 20.04 + Deadsnakes PPA
RUN --mount=type=cache,target=/var/cache/apt-${TARGETPLATFORM},sharing=locked \
    --mount=type=cache,target=/var/lib/apt-${TARGETPLATFORM},sharing=locked \
    apt update && \
    apt install -y software-properties-common && \
    apt update && \
    apt --fix-missing -y install \
    build-essential python3-ply alien iptables iproute2 iputils-ping \
    tzdata curl tar gcc g++ cmake tix pkg-config libssl-dev lsof \
    graphviz graphviz-dev doxygen faketime libscope-guard-perl \
    libtest-tcp-perl libbrotli-dev libev-dev libhttp-parser-dev \
    libbsd-dev snapd rand binutils binutils-dev autoconf automake \
    autotools-dev libtool libjemalloc-dev libboost-all-dev libboost-dev \
    ca-certificates mime-support libevent-dev libdouble-conversion-dev \
    libgflags-dev libgoogle-glog-dev libiberty-dev liblz4-dev liblzma-dev \
    libsnappy-dev zlib1g-dev libsodium-dev libffi-dev cargo libunwind-dev \
    radare2 strace bridge-utils libreadline-dev tk libgv-tcl libgraphviz-dev \
    libdevil1c2 libgts-0.7-5 liblasi0 tcl-dev tcl libgmp-dev dsniff sudo jq ninja-build \
    libomp-dev git clang clang-tidy clang-format


# 0) System toolchain + CPython feature headers (bz2, sqlite, zlib, ssl, tk, etc.)
RUN apt-get update && apt-get install -y --no-install-recommends \
    build-essential make gcc g++ curl ca-certificates git \
    zlib1g-dev libbz2-dev liblzma-dev \
    libsqlite3-dev libssl-dev libffi-dev libreadline-dev \
    tk-dev tcl-dev libncursesw5-dev libgdbm-dev libnss3-dev libedit-dev \
    uuid-dev

# Install pyenv (skip if already present from base image)
RUN if [ ! -d "$HOME/.pyenv" ]; then \
        curl https://pyenv.run | bash && \
        echo 'export PATH="$HOME/.pyenv/bin:$PATH"' >> ~/.bashrc && \
        echo 'export PATH="/root/.pyenv/bin:$PATH"' >> ~/.bashrc && \
        echo 'eval "$(pyenv init -)"' >> ~/.bashrc && \
        echo 'eval "$(pyenv virtualenv-init -)"' >> ~/.bashrc; \
    fi && \
    export PATH="$HOME/.pyenv/bin:$PATH" && \
    eval "$(pyenv init -)" && \
    eval "$(pyenv virtualenv-init -)" && \
    # Install Python 3.10 via pyenv (skip if already installed)
    if ! pyenv versions | grep -q "3.10.12"; then \
        pyenv install 3.10.12; \
    fi && \
    pyenv global 3.10.12 && \
    pyenv rehash && \
    ln -sf "$(pyenv which python3.10)" /usr/local/bin/python3.10 && \
    ln -sf "$(pyenv which python)"     /usr/local/bin/python  && \
    python3.10 -V && which python3.10 && python -V && which python

# Install pip with Python cache mount
RUN --mount=type=cache,target=/root/.cache-${TARGETPLATFORM}/pip \
    curl -sS https://bootstrap.pypa.io/get-pip.py | python3.10

# Python packages with pip cache
RUN --mount=type=cache,target=/root/.cache-${TARGETPLATFORM}/pip \
    python3.10 -m pip install \
    pexpect chardet pandas scandir ply pygraphviz pydot progressbar2

# Dependency building with git and build cache
RUN --mount=type=cache,target=/tmp/git-cache-${TARGETPLATFORM} \
    --mount=type=cache,target=/tmp/build-cache-${TARGETPLATFORM} \
    cd /opt && \
    echo $DEPENDENCIES | jq -c '.[]' | while read -r dep; do \
        DEP_NAME=$(echo $dep | jq -r '.name'); \
        DEP_URL=$(echo $dep | jq -r '.url'); \
        DEP_COMMIT=$(echo $dep | jq -r '.commit'); \
        if [ -n "$DEP_NAME" ] && [ -n "$DEP_URL" ] && [ -n "$DEP_COMMIT" ]; then \
            echo "Processing dependency '$DEP_NAME' from '$DEP_URL' at commit '$DEP_COMMIT'"; \
            # Use cached git repo if available
            if [ -d "/tmp/git-cache-${TARGETPLATFORM}/$DEP_NAME" ]; then \
                echo "Using cached repository for $DEP_NAME"; \
                cp -r "/tmp/git-cache-${TARGETPLATFORM}/$DEP_NAME" "$DEP_NAME"; \
                cd "$DEP_NAME" && git fetch && git checkout "$DEP_COMMIT"; \
            else \
                echo "Cloning fresh repository for $DEP_NAME"; \
                git clone "$DEP_URL" "$DEP_NAME"; \
                cd "$DEP_NAME" && git checkout "$DEP_COMMIT"; \
                # Cache the repository
                cp -r "/opt/$DEP_NAME" "/tmp/git-cache-${TARGETPLATFORM}/$DEP_NAME"; \
            fi; \
            git submodule update --init --recursive; \
            # Use build cache for compilation
            if [ -d "/tmp/build-cache-${TARGETPLATFORM}/$DEP_NAME" ]; then \
                echo "Restoring build cache for $DEP_NAME"; \
                cp -r "/tmp/build-cache-${TARGETPLATFORM}/$DEP_NAME"/* . 2>/dev/null || true; \
            fi; \
            OPENSSL_INCLUDE_DIR="/usr/include/openssl" cmake .; \
            make; \
            (make check || echo "[warn] make check failed (non-fatal)") && \
            # Save build artifacts to cache
            mkdir -p "/tmp/build-cache-${TARGETPLATFORM}/$DEP_NAME"; \
            cp -r . "/tmp/build-cache-${TARGETPLATFORM}/$DEP_NAME/" 2>/dev/null || true; \
            echo "Successfully built dependency '$DEP_NAME'"; \
            cd /opt; \
        else \
            echo "Invalid dependency configuration: $dep"; \
            exit 1; \
        fi; \
    done

# =============================================================================
# STAGE 2: Z3-BUILDER - Isolated Z3 compilation
# Only rebuilds when submodules/z3/, patches/, or build_submodules.py change.
# Changes to ivy/ or lib/ do NOT trigger Z3 rebuild (~30 min savings).
# =============================================================================

FROM deps AS z3-builder

ARG BUILD_MODE
ARG Z3_SOURCE
ARG VERSION
ARG TARGETPLATFORM

WORKDIR /opt/panther_ivy

# Copy ONLY what Z3 needs (ordered by change frequency)
COPY build_submodules.py setup.py pyproject.toml /opt/panther_ivy/
COPY patches /opt/panther_ivy/patches/
COPY submodules/z3 /opt/panther_ivy/submodules/z3/

# Apply patch only when building Z3 from submodule
RUN if [ "$Z3_SOURCE" = "local" ]; then \
        patch -p1 < patches/z3-cmake-git-optional.patch; \
    fi

# Ensure output directories exist for COPY --from in later stages
RUN mkdir -p lib include ivy/lib ivy/z3 ivy/include

# Build Z3 only when Z3_SOURCE=local. This entire stage is cached at the
# Docker layer level when inputs don't change.
RUN if [ "$Z3_SOURCE" = "local" ]; then \
        BUILD_MODE=${BUILD_MODE} python3.10 build_submodules.py --z3-only; \
    else \
        echo "Z3_SOURCE=pip: skipping local Z3 build (will use pip z3-solver)"; \
    fi


# =============================================================================
# STAGE 3: BASE - Main build (picotls, aiger, abc) + install
# =============================================================================

FROM deps AS base

ARG BUILD_MODE
ARG Z3_SOURCE
ARG VERSION
ARG TARGETPLATFORM

ENV VERSION=${VERSION}
ENV PYTHONPATH="/opt/panther_ivy${PYTHONPATH:+:${PYTHONPATH}}"
WORKDIR /opt/panther_ivy/

# Copy application files (order: stable first, volatile last)
COPY setup.py build_submodules.py pyproject.toml /opt/panther_ivy/
COPY patches /opt/panther_ivy/patches/
COPY submodules /opt/panther_ivy/submodules/
COPY ivy /opt/panther_ivy/ivy/
COPY lib /opt/panther_ivy/lib/

# Verify z3_shim fix is deployed (catches stale build context)
RUN grep -q "z3_shim" ivy/ivy_z3_utils.py || \
    (echo "ERROR: ivy_z3_utils.py does not import z3_shim — build context has stale files" && exit 1)

# Overlay Z3 build artifacts from z3-builder stage.
# These COPY --from layers are only re-executed if the z3-builder stage changed,
# even though previous COPY layers may have invalidated.
# The z3-builder stage is cached independently of ivy/ and lib/ changes.
COPY --from=z3-builder /opt/panther_ivy/lib/ /opt/panther_ivy/lib/
COPY --from=z3-builder /opt/panther_ivy/include/ /opt/panther_ivy/include/
# Z3 Python bindings + ivy-internal copies (from mk_make.py --pypkgdir + install_z3)
COPY --from=z3-builder /opt/panther_ivy/ivy/z3/ /opt/panther_ivy/ivy/z3/
COPY --from=z3-builder /opt/panther_ivy/ivy/lib/ /opt/panther_ivy/ivy/lib/
COPY --from=z3-builder /opt/panther_ivy/ivy/include/ /opt/panther_ivy/ivy/include/

# ---- tool-chain & wrappers --------------------------------------------------
RUN --mount=type=cache,target=/var/cache/apt,id=toolchain-$TARGETPLATFORM,sharing=locked \
    --mount=type=cache,target=/var/lib/apt,id=toolchainlib-$TARGETPLATFORM,sharing=locked \
    apt-get update && \
    apt-get install --no-install-recommends -y \
    build-essential git ninja-build binutils gcc g++ gdb && \
    rm -rf /var/lib/apt/lists/*

# Build remaining submodules (picotls, aiger, abc) and install.
# Z3 is already built - use --skip-z3 to skip it.
# BUILD_MODE passed as env var (not as layer ENV) to avoid invalidating COPY layers.
# NOTE: When Z3_SOURCE=local, both Python bindings and C++ test binaries
#   use Z3 4.7.1 from the submodule. When Z3_SOURCE=pip, Python uses 4.13.4.0.
RUN --mount=type=cache,target=/root/.cache/pip-$TARGETPLATFORM,sharing=locked \
    --mount=type=cache,target=/tmp/python-build-$TARGETPLATFORM,sharing=locked \
    BUILD_MODE=${BUILD_MODE} python3.10 build_submodules.py --skip-z3 && \
    if [ "$Z3_SOURCE" = "local" ]; then \
        # Install locally-built Z3 Python bindings as the system 'z3' package. \
        # This ensures 'import z3' uses v4.7.1, matching the C++ libz3.so. \
        mkdir -p /tmp/z3-pkg/z3 && \
        cp ivy/z3/*.py /tmp/z3-pkg/z3/ && \
        cp lib/libz3.so /tmp/z3-pkg/z3/ && \
        printf 'from setuptools import setup, find_packages\nsetup(name="z3-local", version="4.7.1", packages=find_packages(), package_data={"z3": ["*.so", "*.dylib"]})\n' > /tmp/z3-pkg/setup.py && \
        sudo python3.10 -m pip install /tmp/z3-pkg/ && \
        rm -rf /tmp/z3-pkg ; \
    else \
        sudo python3.10 -m pip install z3-solver==4.13.4.0 && \
        # Copy pip z3-solver's C++ headers and shared library to where \
        # ivy_to_cpp.py's get_lib_dirs() expects them (ivy/include/, ivy/lib/). \
        Z3_PKG_DIR=$(python3.10 -c "import z3; import os; print(os.path.dirname(os.path.abspath(z3.__file__)))") && \
        echo "Z3 pip package at: $Z3_PKG_DIR" && \
        mkdir -p ivy/include ivy/lib && \
        if [ -d "$Z3_PKG_DIR/include" ]; then \
            cp -r "$Z3_PKG_DIR/include/"* ivy/include/ && \
            echo "Copied Z3 C++ headers from pip package to ivy/include/"; \
        else \
            echo "WARN: pip z3-solver has no include/ dir — C++ compilation may fail"; \
        fi && \
        if [ -d "$Z3_PKG_DIR/lib" ]; then \
            cp "$Z3_PKG_DIR/lib/"libz3* ivy/lib/ && \
            echo "Copied libz3 from pip package to ivy/lib/"; \
        else \
            Z3_LIB=$(python3.10 -c "import z3; import os; d=os.path.dirname(os.path.abspath(z3.__file__)); [print(os.path.join(d,f)) for f in os.listdir(d) if f.startswith('libz3') and (f.endswith('.so') or f.endswith('.dylib'))]" 2>/dev/null | head -1) && \
            if [ -n "$Z3_LIB" ]; then \
                cp "$Z3_LIB" ivy/lib/ && \
                echo "Copied libz3 from pip package root to ivy/lib/"; \
            else \
                echo "WARN: pip z3-solver has no lib/ dir or libz3 — C++ linking may fail"; \
            fi; \
        fi ; \
    fi && \
    sudo env PURE_PYTHON_BUILD=1 python3.10 -m pip install . && \
    python3.10 -c "import z3; print('Python Z3 version:', z3.get_version_string())" && \
    if [ "$Z3_SOURCE" = "local" ]; then \
        # C++ linking: make libz3.so discoverable by the dynamic linker \
        if [ ! -f lib/libz3.so ]; then \
            echo "ERROR: lib/libz3.so not found - Z3 build may have failed"; \
            exit 1; \
        fi && \
        echo "/opt/panther_ivy/lib" | sudo tee /etc/ld.so.conf.d/panther-z3.conf && \
        sudo ldconfig && \
        echo "Z3_SOURCE=local: Python=4.7.1 (local pkg), C++=4.7.1 (ldconfig)"; \
    else \
        # For pip mode, make ivy/lib/libz3.so discoverable for C++ test binaries \
        if [ -f ivy/lib/libz3.so ] || ls ivy/lib/libz3* >/dev/null 2>&1; then \
            echo "/opt/panther_ivy/ivy/lib" | sudo tee /etc/ld.so.conf.d/panther-z3.conf && \
            sudo ldconfig && \
            echo "Z3_SOURCE=pip: Python=4.13.4.0, C++ headers+lib copied to ivy/{include,lib}"; \
        else \
            echo "Z3_SOURCE=pip: Python=4.13.4.0 (pip z3-solver, no C++ artifacts copied)"; \
        fi; \
    fi

# Verify egg has the z3_shim fix (catches pyenv egg caching stale code)
RUN python3.10 -c "\
import importlib.util, pathlib; \
spec = importlib.util.find_spec('ivy.ivy_z3_utils'); \
assert spec and spec.origin, 'Could not locate ivy.ivy_z3_utils module'; \
first_line = pathlib.Path(spec.origin).read_text().split('\n')[0]; \
assert 'z3_shim' in first_line, f'Egg has stale ivy_z3_utils.py: {first_line}'; \
print(f'OK: egg ivy_z3_utils.py imports z3_shim (from {spec.origin})')"

# Verify Ast types are consistent (catches the specific ctypes mismatch)
RUN python3.10 -c "\
from ivy import z3_shim, ivy_z3_utils; \
shim_ast = getattr(z3_shim, 'Ast', None); \
utils_ast = getattr(ivy_z3_utils, 'Ast', None); \
assert not (shim_ast and utils_ast) or shim_ast is utils_ast, \
    f'Ast mismatch: z3_shim.Ast={shim_ast} vs ivy_z3_utils.Ast={utils_ast}'; \
print(f'OK: Ast type consistent ({shim_ast})' if (shim_ast and utils_ast) else f'WARN: could not verify Ast types (shim={shim_ast}, utils={utils_ast})')"

# Verify ivy_to_cpp.py uses Python-based Z3 version detection (not __has_include).
RUN python3.10 -c "\
import pathlib; \
src = pathlib.Path('/opt/panther_ivy/ivy/ivy_to_cpp.py').read_text(); \
assert 'import z3 as _z3_ver_mod' in src, \
    'STALE: ivy_to_cpp.py still uses __has_include for Z3 version detection'; \
assert '#if defined(Z3_MAJOR_VERSION) && (Z3_MAJOR_VERSION > 4' in src, \
    'STALE: ivy_to_cpp.py has wrong #if guard for parse_smtlib2_compat'; \
assert 'Z3_MINOR_VERSION >= 12' in src, \
    'STALE: ivy_to_cpp.py missing Z3 4.12 version guard for mk_enum/mk_decl'; \
print('OK: ivy_to_cpp.py uses Python-based Z3 version macros with 4.12 guards')"

# Add protocol testing files (last to optimize layer caching)
COPY protocol-testing /opt/panther_ivy/protocol-testing/

# =============================================================================
# FINAL STAGE: Runtime configuration with platform metadata
# =============================================================================

# Target platform runtime stage (inherits platform from base)
FROM base AS final

# Platform and build metadata for debugging and compliance
ARG BUILDPLATFORM
ARG TARGETPLATFORM
ARG TARGETOS
ARG TARGETARCH
ARG VERSION
ARG BUILD_MODE
ARG Z3_SOURCE

LABEL platform.build="${BUILDPLATFORM}"
LABEL platform.target="${TARGETPLATFORM}"
LABEL platform.os="${TARGETOS}"
LABEL platform.arch="${TARGETARCH}"
LABEL service.type="tester"
LABEL service.name="panther_ivy"
LABEL version="${VERSION}"
LABEL build.mode="${BUILD_MODE}"
LABEL z3.source="${Z3_SOURCE}"
LABEL runtime.description="PANTHER IVY formal verification tester environment"
LABEL build.syntax="docker/dockerfile:1"

# Health check for runtime validation
HEALTHCHECK --interval=30s --timeout=10s --start-period=5s --retries=3 \
    CMD python3.10 --version && echo "IVY tester runtime healthy" || exit 1

# Set working directory
WORKDIR /opt/panther_ivy

# Default command
CMD ["/bin/bash"]