#!/usr/bin/env bash
# repro/proof-estate-lean-z3/repro.sh -- reproduce the Z3 proof floor of `proof-estate-lean-z3` by running the lab's own
# witness (scripts/audit/verify_z3_proofs_gate.py) and parsing the counts it prints.
#   exit 0   the witness passed and every parsed count equals EXPECTED.md
#   exit 1   the witness failed, or printed counts that differ from EXPECTED.md
#   exit 69  ENV: a named tool is missing, so nothing was reproduced
# Run from anywhere; it works from the repository root. Writes nothing but __pycache__ and a temporary output file.
set -u -o pipefail
HERE="$(cd "$(dirname "$0")" && pwd)"
ROOT="$(cd "$HERE/../.." && pwd)"
cd "$ROOT" || exit 3

# The guard names the module literally (kit2 lint). The message names it through $SOLVER only so that the digit in "z3"
# is not read as a count EXPECTED.md states; it is never used to decide the guard.
SOLVER=z3
if ! python3 -c "import z3" >/dev/null 2>&1; then
  echo "ENV: the interpreter cannot import the $SOLVER module (pip package $SOLVER-solver); the witness would SKIP, nothing reproduced"
  exit 69
fi

OUT="$(mktemp "${TMPDIR:-/tmp}/repro_lean_z3.XXXXXX")"
trap 'rm -f "$OUT"' EXIT
PYTHONPATH=. python3 scripts/audit/verify_z3_proofs_gate.py >"$OUT" 2>&1
rc=$?
cat "$OUT"
if [ "$rc" -ne 0 ]; then
  echo "NOT REPRODUCED: the witness exited $rc"
  exit 1
fi
python3 repro/expect.py "$HERE/EXPECTED.md" "$OUT"