Potentially Fix Pipeline (Kani issues)

.devcontainer/Dockerfile

@@ -1,24 +1,28 @@
 # Fortress Rollback Development Container
 #
-# This container includes all verification tools:
+# Optimized for fast builds using cargo-binstall (pre-built binaries).
+# Full build: ~3-5 min (vs ~25 min compiling from source).
+# With pre-built image from GHCR: ~30 seconds (pull only).
+#
+# Tools included:
 # - TLA+ model checker
 # - Kani bounded model checker
 # - Miri (undefined behavior detection)
 # - Z3 theorem prover
-# - Loom (concurrency testing via Cargo)
 # - Various cargo tools for testing, coverage, and profiling
 
 FROM mcr.microsoft.com/devcontainers/rust:2-1-trixie
 
 # Use bash for all RUN commands to ensure consistent shell behavior
-# This prevents issues with bash-specific syntax (like process substitution)
 SHELL ["/bin/bash", "-c"]
 
 # Avoid prompts from apt
 ENV DEBIAN_FRONTEND=noninteractive
 
-# Install system dependencies
-RUN apt-get update && apt-get install -y \
+# ============================================================================
+# Layer 1: System dependencies (apt)
+# ============================================================================
+RUN apt-get update && apt-get install -y --no-install-recommends \
     # Build essentials
     build-essential \
     cmake \
@@ -32,7 +36,6 @@ RUN apt-get update && apt-get install -y \
     # Java (for TLA+)
     default-jdk \
     # macroquad example dependencies (graphics, audio, input)
-    # See: https://github.com/not-fl3/macroquad and examples/README.md
     libasound2-dev \
     libx11-dev \
     libxi-dev \
@@ -67,38 +70,61 @@ RUN apt-get update && apt-get install -y \
     htop \
     ncdu \
     silversearcher-ag \
-    # Note: tldr is not available in Debian Trixie, installed via cargo below
-    # Note: eza, git-delta, dust, duf, procs, sd, etc. are installed via cargo below
     && rm -rf /var/lib/apt/lists/*
 
 # Install linux-perf if available (architecture dependent)
-RUN apt-get update && apt-get install -y linux-perf 2>/dev/null || true && rm -rf /var/lib/apt/lists/*
+RUN apt-get update && \
+    if apt-get install -y --no-install-recommends linux-perf; then \
+        echo "linux-perf: installed"; \
+    else \
+        echo "linux-perf: skipped (not available for this architecture)"; \
+    fi && \
+    rm -rf /var/lib/apt/lists/*
 
-# Set up TLA+ tools
+# ============================================================================
+# Layer 2: Direct downloads (TLA+, actionlint, Vale)
+# ============================================================================
 RUN mkdir -p /opt/tla && \
-    curl -L https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar -o /opt/tla/tla2tools.jar
+    curl --proto '=https' --tlsv1.2 -fsSL --retry 5 --retry-delay 2 --retry-all-errors --max-time 120 https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar \
+      -o /opt/tla/tla2tools.jar
 
+# Note: devcontainer.json containerEnv overrides this to the workspace copy
 ENV TLA_TOOLS_JAR=/opt/tla/tla2tools.jar
 
 # Install Z3 and yamllint via pip
-RUN pip3 install --break-system-packages z3-solver yamllint
+RUN pip3 install --no-cache-dir --break-system-packages z3-solver yamllint
 
 # Install actionlint (GitHub Actions linter)
-# Download the script first, then run with bash (avoids process substitution issues with /bin/sh)
-RUN curl -sL https://raw.githubusercontent.com/rhysd/actionlint/main/scripts/download-actionlint.bash -o /tmp/download-actionlint.bash && \
+RUN curl --proto '=https' --tlsv1.2 -fsSL --retry 5 --retry-delay 2 --retry-all-errors --max-time 120 https://raw.githubusercontent.com/rhysd/actionlint/main/scripts/download-actionlint.bash \
+      -o /tmp/download-actionlint.bash && \
     bash /tmp/download-actionlint.bash latest /usr/local/bin && \
     rm /tmp/download-actionlint.bash && \
     chmod +x /usr/local/bin/actionlint
 
-# Install Vale (prose linter)
-# Vale is used to check documentation for prose quality
+# Install Vale (prose linter) - architecture aware
 RUN VALE_VERSION="3.9.3" && \
-    curl -sL "https://github.com/errata-ai/vale/releases/download/v${VALE_VERSION}/vale_${VALE_VERSION}_Linux_64-bit.tar.gz" -o /tmp/vale.tar.gz && \
+    ARCH="$(uname -m)" && \
+    if [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then VALE_ARCH="arm64"; else VALE_ARCH="64-bit"; fi && \
+        curl --proto '=https' --tlsv1.2 -fsSL --retry 5 --retry-delay 2 --retry-all-errors --max-time 120 "https://github.com/errata-ai/vale/releases/download/v${VALE_VERSION}/vale_${VALE_VERSION}_Linux_${VALE_ARCH}.tar.gz" \
+      -o /tmp/vale.tar.gz && \
     tar -xzf /tmp/vale.tar.gz -C /usr/local/bin vale && \
     rm /tmp/vale.tar.gz && \
     chmod +x /usr/local/bin/vale
 
-# Switch to vscode user for remaining installations
+# ============================================================================
+# Layer 3: Node.js and linting tools
+# ============================================================================
+RUN curl --proto '=https' --tlsv1.2 -fsSL --retry 5 --retry-delay 2 --retry-all-errors --max-time 120 https://deb.nodesource.com/setup_22.x -o /tmp/nodesource_setup.sh && \
+    bash /tmp/nodesource_setup.sh && \
+    rm /tmp/nodesource_setup.sh && \
+    apt-get install -y --no-install-recommends nodejs && \
+    npm install -g markdownlint-cli markdown-link-check && \
+    pip3 install --no-cache-dir --break-system-packages pre-commit && \
+    rm -rf /var/lib/apt/lists/*
+
+# ============================================================================
+# Layer 4: Rust toolchains and components (as vscode user)
+# ============================================================================
 USER vscode
 
 # Install Rust nightly toolchain (required for Miri and some Kani features)
@@ -109,57 +135,76 @@ RUN rustup install nightly && \
 # Install Miri (undefined behavior detector)
 RUN rustup +nightly component add miri
 
-# Install Kani verifier
-# Note: Kani requires its own setup step which downloads CBMC
+# ============================================================================
+# Layer 5: cargo-binstall (enables fast pre-built binary downloads)
+# ~10 seconds instead of ~18 minutes compiling from source
+# ============================================================================
+ENV BINSTALL_DISABLE_TELEMETRY=true
+RUN set -e && \
+    ARCH="$(uname -m)" && \
+    CARGO_BIN_DIR="${CARGO_HOME:-$HOME/.cargo}/bin" && \
+    if [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then \
+        BINSTALL_ARCH="aarch64-unknown-linux-musl"; \
+    else \
+        BINSTALL_ARCH="x86_64-unknown-linux-musl"; \
+    fi && \
+    mkdir -p "$CARGO_BIN_DIR" && \
+    echo "Installing cargo-binstall for ${BINSTALL_ARCH}" && \
+    curl --proto '=https' --tlsv1.2 -fsSL --retry 5 --retry-delay 2 --retry-all-errors --max-time 120 "https://github.com/cargo-bins/cargo-binstall/releases/latest/download/cargo-binstall-${BINSTALL_ARCH}.tgz" \
+      -o /tmp/cargo-binstall.tgz && \
+    tar -xzf /tmp/cargo-binstall.tgz -C "$CARGO_BIN_DIR" && \
+    rm /tmp/cargo-binstall.tgz && \
+        cargo-binstall -V
+
+# ============================================================================
+# Layer 6: Verification & testing tools (via binstall - pre-built binaries)
+# These are the most critical tools, installed first for cache stability
+# ============================================================================
+RUN for tool in cargo-nextest cargo-audit cargo-deny cargo-tarpaulin cargo-llvm-cov cargo-mutants cargo-careful flamegraph; do \
+        cargo binstall --no-confirm "$tool" \
+            || echo "$tool: failed to install"; \
+    done
+
+# ============================================================================
+# Layer 7: Development workflow tools (via binstall)
+# ============================================================================
+RUN for tool in cargo-watch sccache cargo-shear; do \
+        cargo binstall --no-confirm "$tool" \
+            || echo "$tool: failed to install"; \
+    done
+
+# ============================================================================
+# Layer 8: High-performance CLI tools (via binstall)
+# These are optional -- each tool installs independently so one failure
+# does not block the others.
+# ============================================================================
+RUN for tool in eza git-delta du-dust duf procs sd hyperfine tokei zoxide tealdeer bottom; do \
+        cargo binstall --no-confirm "$tool" \
+            || echo "$tool: skipped (no prebuilt binary)"; \
+    done
+
+# ============================================================================
+# Layer 9: Kani verifier (compiled from source - no pre-built binary available)
+# This is the heaviest layer (~3-4 min). Cached unless kani version changes.
+# ============================================================================
 RUN cargo install --locked kani-verifier && \
-    cargo kani setup || echo "Kani setup may need to complete on first use"
-
-# Install cargo tools for testing and verification
-RUN cargo install cargo-audit && \
-    cargo install cargo-deny && \
-    cargo install cargo-tarpaulin && \
-    cargo install cargo-llvm-cov && \
-    cargo install cargo-mutants && \
-    cargo install cargo-fuzz || echo "cargo-fuzz requires nightly" && \
-    cargo install flamegraph && \
-    cargo install cargo-nextest && \
-    cargo install cargo-watch && \
-    cargo install sccache && \
-    # CI/CD linting and quality tools
-    cargo install cargo-shear && \
-    cargo install cargo-spellcheck && \
-    cargo install cargo-geiger && \
-    cargo install cargo-careful && \
-    # High-performance CLI tools (Rust-based, not available in Debian apt)
-    cargo install eza && \
-    cargo install git-delta && \
-    cargo install du-dust && \
-    cargo install duf && \
-    cargo install procs && \
-    cargo install sd && \
-    cargo install hyperfine && \
-    cargo install tokei && \
-    cargo install zoxide && \
-    cargo install tealdeer && \
-    cargo install bottom || echo "bottom (btm) optional"
-
-# Install Node.js and markdown/linting tools (for CI/CD and pre-commit hooks)
-# Note: Download and run as separate steps to avoid shell compatibility issues
-USER root
-RUN curl -fsSL https://deb.nodesource.com/setup_20.x -o /tmp/nodesource_setup.sh && \
-    bash /tmp/nodesource_setup.sh && \
-    rm /tmp/nodesource_setup.sh && \
-    apt-get install -y nodejs && \
-    npm install -g markdownlint-cli markdown-link-check && \
-    pip3 install --break-system-packages pre-commit && \
-    rm -rf /var/lib/apt/lists/*
-USER vscode
+    (cargo kani setup || echo "Kani setup may need to complete on first use")
+
+# ============================================================================
+# Layer 10: Remaining source-compiled tools (each isolated for cache stability)
+# ============================================================================
+RUN cargo install cargo-fuzz || echo "cargo-fuzz requires nightly"
+
+RUN cargo install cargo-geiger || echo "cargo-geiger optional"
+
+RUN cargo install cargo-spellcheck || echo "cargo-spellcheck optional"
 
-# Set environment variables
+# ============================================================================
+# Layer 11: Environment and helper scripts
+# ============================================================================
 ENV RUST_BACKTRACE=1
 ENV CARGO_INCREMENTAL=0
 
-# Reset to root for any final setup
 USER root
 
 # Create helper script for running TLA+
@@ -173,13 +218,13 @@ RUN echo '#!/bin/bash\njava -cp /opt/tla/tla2tools.jar tla2sany.SANY "$@"' > /us
 # Switch back to vscode user
 USER vscode
 
-WORKDIR /workspaces/ggrs
+WORKDIR /workspaces/fortress-rollback
 
 # Set up aliases for high-performance tools
 # Note: fd-find installs as 'fdfind' on Debian, bat as 'batcat'
-# eza, delta, dust, duf, procs are installed via cargo and have standard names
+# eza, delta, dust, duf, procs are installed via binstall and have standard names
 # tealdeer installs as 'tldr'
-RUN echo '\n# High-performance tool aliases\nalias fd="fdfind"\nalias bat="batcat"\nalias ls="eza"\nalias ll="eza -la"\nalias la="eza -la"\nalias tree="eza --tree"\nalias cat="batcat --paging=never"\nalias diff="delta"\nalias du="dust"\nalias df="duf"\nalias ps="procs"\nalias top="htop"\nalias sed="sd"\n\n# Initialize zoxide (smart cd)\neval "$(zoxide init bash)"\n\n# Conditionally enable sccache if available\nif command -v sccache &> /dev/null; then\n  export RUSTC_WRAPPER=sccache\nfi\n' >> ~/.bashrc
+RUN echo '\n# High-performance tool aliases\nalias fd="fdfind"\nalias bat="batcat"\nalias cat="batcat --paging=never"\nalias top="htop"\n\n# Optional tool aliases (installed via binstall; may not be present)\ncommand -v eza >/dev/null 2>&1 && alias ls="eza"\ncommand -v eza >/dev/null 2>&1 && alias ll="eza -la"\ncommand -v eza >/dev/null 2>&1 && alias la="eza -la"\ncommand -v eza >/dev/null 2>&1 && alias tree="eza --tree"\ncommand -v delta >/dev/null 2>&1 && alias diff="delta"\ncommand -v dust >/dev/null 2>&1 && alias du="dust"\ncommand -v duf >/dev/null 2>&1 && alias df="duf"\ncommand -v procs >/dev/null 2>&1 && alias ps="procs"\n\n# Initialize zoxide (smart cd) if available\ncommand -v zoxide >/dev/null 2>&1 && eval "$(zoxide init bash)"\n\n# Conditionally enable sccache if available\nif command -v sccache >/dev/null 2>&1; then\n  export RUSTC_WRAPPER=sccache\nfi\n' >> ~/.bashrc
 
 # Print tool versions on first login (via .bashrc)
-RUN echo '\n# Fortress Rollback Development Environment\nif [ -f /workspaces/ggrs/.devcontainer/welcome.sh ]; then\n  source /workspaces/ggrs/.devcontainer/welcome.sh\nfi' >> ~/.bashrc
+RUN echo '\n# Fortress Rollback Development Environment\nif [ -f /workspaces/fortress-rollback/.devcontainer/welcome.sh ]; then\n  source /workspaces/fortress-rollback/.devcontainer/welcome.sh\nfi' >> ~/.bashrc

.devcontainer/README.md

@@ -59,6 +59,38 @@ After the container starts, verify all tools:
 ./scripts/check-tools.sh
 ```
 
+## Build Performance
+
+The Dockerfile uses **cargo-binstall** to download pre-built binaries instead of
+compiling tools from source, reducing build time from ~25 minutes to ~3-5 minutes.
+
+| Method | Build Time | When to Use |
+|--------|-----------|-------------|
+| **Pre-built image (GHCR)** | ~30 seconds | Optional fast path when the image is available |
+| **Local Dockerfile build** | ~3-5 min | When modifying the Dockerfile |
+| **Without binstall (old)** | ~25-30 min | N/A (deprecated) |
+
+### Using the pre-built image (fastest)
+
+The local Dockerfile build remains the default path until the published image has been validated across the environments this project supports.
+
+In `devcontainer.json`, comment out the `"build"` block and uncomment the `"image"` line:
+
+```jsonc
+// "build": { ... },
+"image": "ghcr.io/wallstop/fortress-rollback/devcontainer:latest",
+```
+
+The image is automatically rebuilt weekly and on changes to `.devcontainer/` files.
+
+> **Note:** The pre-built GHCR image is x86_64 (amd64) only. Apple Silicon (arm64)
+> users should use the local Dockerfile build, which includes architecture detection.
+
+### Building locally
+
+The default `devcontainer.json` builds from the Dockerfile. Docker layer caching
+means subsequent rebuilds only reprocess changed layers.
+
 ## Running Verification
 
 ### All Verifiers
@@ -129,7 +161,7 @@ npm install -g markdownlint-cli markdown-link-check
 
 # actionlint (GitHub Actions linter)
 # Download the script first, then run with bash (avoids shell issues)
-curl -sL https://raw.githubusercontent.com/rhysd/actionlint/main/scripts/download-actionlint.bash -o /tmp/download-actionlint.bash
+curl --proto '=https' --tlsv1.2 -sSfL https://raw.githubusercontent.com/rhysd/actionlint/main/scripts/download-actionlint.bash -o /tmp/download-actionlint.bash
 bash /tmp/download-actionlint.bash latest /tmp
 sudo mv /tmp/actionlint /usr/local/bin/
 rm /tmp/download-actionlint.bash
@@ -151,10 +183,10 @@ If you see this error in other scripts, ensure they are run with bash explicitly
 
 ```bash
 # Instead of piping to sh
-curl -sL https://example.com/script.sh | bash
+curl --proto '=https' --tlsv1.2 -sSfL https://example.com/script.sh | bash
 
 # Download first, then run with bash
-curl -sL https://example.com/script.sh -o /tmp/script.sh
+curl --proto '=https' --tlsv1.2 -sSfL https://example.com/script.sh -o /tmp/script.sh
 bash /tmp/script.sh
 rm /tmp/script.sh
 ```
@@ -173,7 +205,7 @@ Try removing old containers and images:
 
 ```bash
 # List and remove devcontainer images
-docker images | grep vsc-ggrs | awk '{print $3}' | xargs -r docker rmi -f
+docker images | grep fortress-rollback | awk '{print $3}' | xargs -r docker rmi -f
 
 # Or prune all unused images
 docker system prune -a
@@ -202,7 +234,7 @@ Download manually:
 
 ```bash
 mkdir -p .tla-tools
-curl -L https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar -o .tla-tools/tla2tools.jar
+curl --proto '=https' --tlsv1.2 -sSfL https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar -o .tla-tools/tla2tools.jar
 ```
 
 ## Files