# Tamarin ローカルデモ用イメージ（Tamarin と、ブラウザ画面を提供する FastAPI アプリをまとめたもの）
#
# x86_64 (amd64) / aarch64 (arm64) の両方でネイティブに動作する。
#   - Maude  : Debian の apt パッケージ
#   - Tamarin: GitHub 公式リリースの Homebrew bottle (Linux 用)
#              https://github.com/tamarin-prover/tamarin-prover/releases
FROM debian:trixie-slim

# 使用する Tamarin のバージョン (決め打ち)
ARG TAMARIN_VERSION=1.12.0

ENV DEBIAN_FRONTEND=noninteractive
# Tamarin/GHC はロケール依存でファイルを読むため UTF-8 を明示
ENV LANG=C.UTF-8 LC_ALL=C.UTF-8

# 実行時依存 (Maude, Graphviz, GMP, zlib) + ダウンロード用ツール + ブラウザ画面用アプリを動かす Python
RUN set -eux; \
    apt-get update; \
    apt-get install -y --no-install-recommends \
        maude graphviz libgmp10 zlib1g \
        curl ca-certificates patchelf \
        python3 python3-venv; \
    rm -rf /var/lib/apt/lists/*; \
    maude --version

# Tamarin を GitHub リリースの Homebrew bottle から取得して /usr/local/bin に配置
#   x86_64 / arm64 (aarch64) を自動判別する。
#   bottle 内のバイナリはローダのパスが Homebrew 用のプレースホルダになっているため、
#   patchelf で Debian のローダに差し替える。
RUN set -eux; \
    case "$(uname -m)" in \
        x86_64)  BOTTLE_ARCH=x86_64; LOADER=/lib64/ld-linux-x86-64.so.2 ;; \
        aarch64) BOTTLE_ARCH=arm64;  LOADER=/lib/ld-linux-aarch64.so.1 ;; \
        *) echo "Unsupported architecture: $(uname -m)" >&2; exit 1 ;; \
    esac; \
    DOWNLOAD_URL="https://github.com/tamarin-prover/tamarin-prover/releases/download/${TAMARIN_VERSION}/tamarin-prover-${TAMARIN_VERSION}.${BOTTLE_ARCH}_linux.bottle.tar.gz"; \
    mkdir -p /tmp/tamarin; \
    curl -fsSL "$DOWNLOAD_URL" | tar -xz -C /tmp/tamarin; \
    install -m 755 "/tmp/tamarin/tamarin-prover/${TAMARIN_VERSION}/bin/tamarin-prover" /usr/local/bin/tamarin-prover; \
    patchelf --set-interpreter "$LOADER" --remove-rpath /usr/local/bin/tamarin-prover; \
    rm -rf /tmp/tamarin; \
    tamarin-prover --version

# ブラウザ画面用アプリ (FastAPI)
WORKDIR /app
COPY requirements.txt .
RUN python3 -m venv /opt/venv && /opt/venv/bin/pip install --no-cache-dir -r requirements.txt
ENV PATH=/opt/venv/bin:$PATH

# エディタ部品 (CodeMirror) をイメージに同梱し、オフラインでも画面が使えるようにする
ENV CODEMIRROR_URL=https://cdnjs.cloudflare.com/ajax/libs/codemirror/5.65.16
RUN set -eux; \
    mkdir -p /app/frontend/vendor/codemirror; \
    cd /app/frontend/vendor/codemirror; \
    curl -fsSLO "$CODEMIRROR_URL/codemirror.min.css"; \
    curl -fsSLO "$CODEMIRROR_URL/codemirror.min.js"; \
    curl -fsSLO "$CODEMIRROR_URL/addon/mode/simple.min.js"

COPY app.py .
COPY frontend /app/frontend
COPY examples /app/examples

# root 以外のユーザーで実行
RUN useradd -m -u 10001 tamarin
USER tamarin

# コンテナ内では 0.0.0.0:8000 で待ち受ける（コンテナ外から届くようにするため）。
# PC 側では docker-compose.yml の ports、または wslc run / container run の
# -p 127.0.0.1:8000:8000 で localhost のみに限定する。
EXPOSE 8000
CMD ["uvicorn", "app:app", "--host", "0.0.0.0", "--port", "8000"]
