#!/usr/bin/env bash
# REPRODUCE.sh — Re-run the cubie-tf TEP LAZY-8 sweep + (optionally) the
# triple-kernel verification suite.  Bash / git-bash / WSL / Linux.

set -euo pipefail

REPO_DIR="${REPO_DIR:-C:/Users/NickV/cubie-tf-completion}"
VERUS_BIN="${VERUS_BIN:-C:/Users/NickV/Downloads/verus-win/verus-x86-win/verus.exe}"
OUT_DIR="${OUT_DIR:-$REPO_DIR/data/tep/layouts}"
SEEDS=(1 2 3 5 7 11 13 17 19 23 29 31 37 41 43 47 53 67 73 2024)
ALGOS=(greedy pareto anneal)

hr() { printf '\n%s\n' "──────────────────────────────────────────────"; }
ok() { printf '\033[32m✔\033[0m %s\n' "$*"; }
err() { printf '\033[31m✘\033[0m %s\n' "$*"; exit 1; }

hr; echo "STEP 0  Environment"
echo "  REPO_DIR  = $REPO_DIR"
echo "  VERUS_BIN = $VERUS_BIN"
echo "  OUT_DIR   = $OUT_DIR"
[ -d "$REPO_DIR" ] || err "REPO_DIR does not exist: $REPO_DIR"
cd "$REPO_DIR"

hr; echo "STEP 1  Build TEP detector (cargo build --release)"
cargo build --release --package cubie-tep --bin tep_layout_search 2>&1 | tail -5
TEP="$REPO_DIR/target/release/tep_layout_search.exe"
[ -f "$TEP" ] || TEP="$REPO_DIR/target/release/tep_layout_search"
[ -f "$TEP" ] || err "tep_layout_search binary not found at $TEP"
ok "Binary: $TEP"

hr; echo "STEP 2  LAZY-8 60-run sweep (20 seeds × 3 algorithms × 1000 iters)"
mkdir -p "$OUT_DIR"
start=$(date +%s)
for seed in "${SEEDS[@]}"; do
  for algo in "${ALGOS[@]}"; do
    "$TEP" --seed "$seed" --algorithm "$algo" --max-iters 1000 --far-ceiling 0.0 \
           --out "$OUT_DIR/run_${algo}_seed${seed}.json" >/dev/null 2>&1
  done
done
elapsed=$(( $(date +%s) - start ))
ok "Sweep complete in ${elapsed}s"

hr; echo "STEP 3  Verify all 60 runs reach saturation (FAR=0, FDR=100%³)"
perfect=$(grep -l '"far":   0.000000' "$OUT_DIR"/run_*.json | wc -l)
echo "  perfect-3 runs: $perfect / 60"
[ "$perfect" -eq 60 ] && ok "60/60 reach the saturation peak" || err "Only $perfect/60 saturate"

hr; echo "STEP 4  (optional) Triple-kernel verification on 27 CUBs"
if [ "${SKIP_KERNELS:-0}" = "1" ]; then
  echo "  SKIPPED (SKIP_KERNELS=1)"
else
  if [ -f "$VERUS_BIN" ]; then
    echo ""; echo "  --- Verus ---"
    vp=0; vf=0
    for f in proofs/verus/tep/CUB_19[4-6][0-9]_*_spec.rs; do
      [ -f "$f" ] || continue
      if "$VERUS_BIN" --crate-type lib "$f" 2>&1 | grep -qE "0 errors\$|0 errors,"; then
        vp=$((vp+1))
      else
        vf=$((vf+1)); echo "  VFAIL: $(basename $f)"
      fi
    done
    echo "  Verus: $vp / $((vp+vf))"
  else
    echo "  Verus binary not at $VERUS_BIN — skipping"
  fi
  if command -v lean >/dev/null 2>&1; then
    echo ""; echo "  --- Lean ($(lean --version | head -1)) ---"
    lp=0; lf=0
    for f in proofs/lean/tep/CUB_19[4-6][0-9]_*.lean; do
      [ -f "$f" ] || continue
      if lean "$f" 2>&1 | grep -q "error:"; then
        lf=$((lf+1)); echo "  LFAIL: $(basename $f)"
      else
        lp=$((lp+1))
      fi
    done
    echo "  Lean: $lp / $((lp+lf))"
  else
    echo "  Lean not on PATH — install via 'elan default leanprover/lean4:v4.10.0'"
  fi
  if command -v docker >/dev/null 2>&1; then
    echo ""; echo "  --- Coq 8.18 (Docker) ---"
    docker pull coqorg/coq:8.18 >/dev/null 2>&1 || true
    cp=0; cf=0
    for f in proofs/coq/tep/CUB_19[4-6][0-9]_*.v; do
      [ -f "$f" ] || continue
      fname=$(basename "$f")
      cmd='cp /src/'"$fname"' /tmp/'"$fname"' && cd /tmp && eval $(opam env) && coqc '"$fname"
      if docker run --rm -v "$REPO_DIR/proofs/coq/tep:/src:ro" coqorg/coq:8.18 bash -c "$cmd" >/dev/null 2>&1; then
        cp=$((cp+1))
      else
        cf=$((cf+1)); echo "  CFAIL: $fname"
      fi
    done
    echo "  Coq: $cp / $((cp+cf))"
  else
    echo "  Docker not available — skipping Coq"
  fi
fi

hr; echo "STEP 5  Rust runtime tests (CUB-1940 Layer-1)"
cargo test -p cubie-core --features std --lib input_validation 2>&1 | tail -15

hr; ok "Reproduction complete."
echo "Outputs in: $OUT_DIR/run_*.json (60 JSONs)"
