#!/usr/bin/env bash
# Verify Lean 4 proof stub files exist and have 'sorry' placeholders.
# Exit 0 on success; non-zero on any missing file or missing sorry.
set -euo pipefail

cd "$(dirname "$0")/.."

echo "=== Lean 4 Proof Verification ==="

PROOF_FILES=(
    "proofs/PostSemClaw/BirkhoffClosure.lean"
    "proofs/PostSemClaw/SpectralBound.lean"
    "proofs/PostSemClaw/OjaConvergence.lean"
    "proofs/PostSemClaw/Discretization.lean"
    "proofs/PostSemClaw/SDRCollision.lean"
    "proofs/PostSemClaw/HestiaAnnealing.lean"
)

echo "Checking proof stub files exist..."
for f in "${PROOF_FILES[@]}"; do
    [ -f "$f" ] || { echo "FAIL: $f not found"; exit 1; }
    grep -q "sorry" "$f" || { echo "FAIL: $f has no 'sorry' (expected Phase 1 stub)"; exit 1; }
    echo "  OK: $f"
done
echo "All ${#PROOF_FILES[@]} proof stubs verified."

if command -v lake &>/dev/null; then
    echo ""
    echo "Running: lake build"
    lake build || echo "WARNING: lake build failed — 'sorry' stubs are expected to warn, not error"
else
    echo ""
    echo "SKIP: Lean 4 (lake) not installed. Install via elan to verify proofs."
fi