#!/bin/bash
# bench-proof.sh — verify the EML proof across every tier we have.
#
# Same five theorems, same symbolic-rewrite strategy, different hosts:
# Lean 4 (cached & cold) vs Lumbda (Python, C tree-walker, C --fast, asm).
# Prints best-of-3 in milliseconds.

set -u
cd "$(dirname "$0")/.."
ulimit -v 1048576 -s unlimited

CACHE=/tmp/lumbda-eml.cache

bestof_cold() {
    # Delete cache before each run so every measurement re-verifies.
    local cmd="$1" best=999999
    for _ in 1 2 3; do
        rm -f "$CACHE"
        local t0 t1 ms
        t0=$(date +%s%N)
        eval "$cmd" >/dev/null 2>&1 || true
        t1=$(date +%s%N)
        ms=$(( (t1 - t0) / 1000000 ))
        [ "$ms" -lt "$best" ] && best="$ms"
    done
    echo "$best"
}

bestof_cached() {
    # Ensure cache exists once, then measure cache-hit paths.
    local cmd="$1" best=999999
    rm -f "$CACHE"
    eval "$cmd" >/dev/null 2>&1 || true   # prime
    for _ in 1 2 3; do
        local t0 t1 ms
        t0=$(date +%s%N)
        eval "$cmd" >/dev/null 2>&1 || true
        t1=$(date +%s%N)
        ms=$(( (t1 - t0) / 1000000 ))
        [ "$ms" -lt "$best" ] && best="$ms"
    done
    echo "$best"
}

echo "══════════════════════════════════════════════════════"
echo "EML proof verification — best of 3 runs (ms)"
echo "  i5-8350U, same five theorems, same symbolic strategy"
echo "  cold = cache cleared first ('full re-verification')"
echo "  cached = prior run's cache artifact is trusted"
echo "══════════════════════════════════════════════════════"

printf "  %-38s %s\n" "Lumbda tier" "cold   cached"
printf "  %-38s %s\n" "─────────────────────────────────────" "───────────────"
printf "  %-38s %4s ms  %4s ms\n" "Python --fast" \
    "$(bestof_cold   'python3 lumbda.py --fast proof/eml_proof_in_lumbda.lsp')" \
    "$(bestof_cached 'python3 lumbda.py --fast proof/eml_proof_in_lumbda.lsp')"
printf "  %-38s %4s ms  %4s ms\n" "C (tree-walker)" \
    "$(bestof_cold   'c/lumbda proof/eml_proof_in_lumbda.lsp')" \
    "$(bestof_cached 'c/lumbda proof/eml_proof_in_lumbda.lsp')"
printf "  %-38s %4s ms  %4s ms\n" "C --fast (bytecode VM)" \
    "$(bestof_cold   'timeout 15 c/lumbda --fast proof/eml_proof_in_lumbda.lsp')" \
    "$(bestof_cached 'timeout 15 c/lumbda --fast proof/eml_proof_in_lumbda.lsp')"
printf "  %-38s %4s ms  %4s ms\n" "asm" \
    "$(bestof_cold   'asm/lumbda < proof/eml_proof_in_lumbda.lsp')" \
    "$(bestof_cached 'asm/lumbda < proof/eml_proof_in_lumbda.lsp')"

echo ""
echo "  Lean 4 comparison:"
if command -v lake >/dev/null 2>&1; then
    printf "  %-38s %4s ms\n" "Lean 4 (cached replay)" "$(bestof_cached 'cd proof/lean && lake build')"

    best=999999
    for _ in 1 2 3; do
        (cd proof/lean && lake clean >/dev/null 2>&1)
        t0=$(date +%s%N)
        (cd proof/lean && lake build >/dev/null 2>&1)
        t1=$(date +%s%N)
        ms=$(( (t1 - t0) / 1000000 ))
        [ "$ms" -lt "$best" ] && best="$ms"
    done
    printf "  %-38s %4s ms\n" "Lean 4 (cold rebuild)" "$best"
else
    echo "  (Lean 4 not installed — skipping Lean rows)"
fi

rm -f "$CACHE"
echo "══════════════════════════════════════════════════════"
echo "  Notes:"
echo "    - Cached replay re-reads an already-checked artifact;"
echo "      cold rebuild/run is the fair end-to-end compare."
echo "    - Clearing the cache: rm -f $CACHE"
echo "    - C --fast has a known cumulative-state compiler bug."