# REPRODUCE.ps1 — Re-run the cubie-tf TEP LAZY-8 sweep + (optionally) triple-kernel.
# Windows PowerShell 5+/7. Run from anywhere.

$ErrorActionPreference = "Stop"

$RepoDir  = $env:REPO_DIR  | ForEach-Object { if ($_) {$_} else {"C:\Users\NickV\cubie-tf-completion"} } | Select-Object -First 1
$VerusBin = $env:VERUS_BIN | ForEach-Object { if ($_) {$_} else {"C:\Users\NickV\Downloads\verus-win\verus-x86-win\verus.exe"} } | Select-Object -First 1
$OutDir   = $env:OUT_DIR   | ForEach-Object { if ($_) {$_} else {"$RepoDir\data\tep\layouts"} } | Select-Object -First 1
$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")

function Hr  { Write-Host ""; Write-Host "──────────────────────────────────────────────" }
function Ok  ($m) { Write-Host "[OK]  $m" -ForegroundColor Green }
function Err ($m) { Write-Host "[FAIL] $m" -ForegroundColor Red; exit 1 }

Hr; Write-Host "STEP 0  Environment"
Write-Host "  REPO_DIR  = $RepoDir"
Write-Host "  VERUS_BIN = $VerusBin"
Write-Host "  OUT_DIR   = $OutDir"
if (-not (Test-Path $RepoDir)) { Err "REPO_DIR does not exist" }
Set-Location $RepoDir

Hr; Write-Host "STEP 1  Build TEP detector"
cargo build --release --package cubie-tep --bin tep_layout_search 2>&1 | Select-Object -Last 5
$Tep = "$RepoDir\target\release\tep_layout_search.exe"
if (-not (Test-Path $Tep)) { Err "tep_layout_search.exe not at $Tep" }
Ok "Binary: $Tep"

Hr; Write-Host "STEP 2  LAZY-8 60-run sweep"
New-Item -ItemType Directory -Force $OutDir | Out-Null
$start = Get-Date
foreach ($seed in $Seeds) {
    foreach ($algo in $Algos) {
        & $Tep --seed $seed --algorithm $algo --max-iters 1000 --far-ceiling 0.0 `
              --out "$OutDir\run_${algo}_seed${seed}.json" 2>&1 | Out-Null
    }
}
$elapsed = (Get-Date) - $start
Ok ("Sweep complete in {0:N0}s" -f $elapsed.TotalSeconds)

Hr; Write-Host "STEP 3  Verify all 60 runs reach saturation"
$perfect = (Get-ChildItem "$OutDir\run_*.json" | Select-String '"far":   0\.000000').Count
Write-Host "  perfect-3 runs: $perfect / 60"
if ($perfect -eq 60) { Ok "60/60 saturate" } else { Err "Only $perfect/60 saturate" }

Hr; Write-Host "STEP 4  (optional) Triple-kernel verification"
if ($env:SKIP_KERNELS -eq "1") {
    Write-Host "  SKIPPED (SKIP_KERNELS=1)"
} else {
    if (Test-Path $VerusBin) {
        Write-Host ""; Write-Host "  --- Verus ---"
        $vp = 0; $vf = 0
        Get-ChildItem "proofs\verus\tep\CUB_19[4-6][0-9]_*_spec.rs" | ForEach-Object {
            $out = & $VerusBin --crate-type lib $_.FullName 2>&1
            if ($out -match "0 errors$|0 errors,") { $vp++ }
            else { $vf++; Write-Host "  VFAIL: $($_.Name)" }
        }
        Write-Host "  Verus: $vp / $($vp+$vf)"
    } else { Write-Host "  Verus binary not at $VerusBin — skipping" }

    if (Get-Command lean -ErrorAction SilentlyContinue) {
        Write-Host ""; Write-Host "  --- Lean ---"
        $lp = 0; $lf = 0
        Get-ChildItem "proofs\lean\tep\CUB_19[4-6][0-9]_*.lean" | ForEach-Object {
            $out = lean $_.FullName 2>&1 | Out-String
            if ($out -match "error:") { $lf++; Write-Host "  LFAIL: $($_.Name)" }
            else { $lp++ }
        }
        Write-Host "  Lean: $lp / $($lp+$lf)"
    } else { Write-Host "  Lean not on PATH" }

    if (Get-Command docker -ErrorAction SilentlyContinue) {
        Write-Host ""; Write-Host "  --- Coq 8.18 (Docker) ---"
        docker pull coqorg/coq:8.18 2>&1 | Out-Null
        $cp = 0; $cf = 0
        Get-ChildItem "proofs\coq\tep\CUB_19[4-6][0-9]_*.v" | ForEach-Object {
            $fname = $_.Name
            $cmd = "cp /src/$fname /tmp/$fname && cd /tmp && eval `$(opam env) && coqc $fname"
            $exit = (docker run --rm -v "$RepoDir\proofs\coq\tep:/src:ro" coqorg/coq:8.18 bash -c $cmd 2>&1 | Out-Null; $LASTEXITCODE)
            if ($exit -eq 0) { $cp++ } else { $cf++; Write-Host "  CFAIL: $fname" }
        }
        Write-Host "  Coq: $cp / $($cp+$cf)"
    } else { Write-Host "  Docker not available — skipping Coq" }
}

Hr; Write-Host "STEP 5  Rust runtime tests (CUB-1940)"
cargo test -p cubie-core --features std --lib input_validation 2>&1 | Select-Object -Last 15

Hr; Ok "Reproduction complete."
Write-Host "Outputs in: $OutDir\run_*.json (60 JSONs)"
