|
| 1 | +#!/usr/bin/env bash |
| 2 | +# SPDX-License-Identifier: MPL-2.0 |
| 3 | +# Absolute Zero — self-test for the prover gate. |
| 4 | +# |
| 5 | +# Proves that proofs/verify-all-provers.sh and proofs/z3/verify.sh turn RED when |
| 6 | +# they should, using a stub toolchain on a private PATH (no real prover needed), |
| 7 | +# plus two mutants under a REAL z3 (required on PATH). Every negative case must |
| 8 | +# fail with the expected reason string, not merely a non-zero exit — a parse |
| 9 | +# error would otherwise pass as a kill. |
| 10 | +# HOME is overridden because the gate prepends $HOME/.local/bin:$HOME/.elan/bin. |
| 11 | +set -uo pipefail |
| 12 | +HERE="$(cd "$(dirname "$0")" && pwd)" |
| 13 | +PROOFS="$(cd "$HERE/.." && pwd)" |
| 14 | +GATE="$PROOFS/verify-all-provers.sh" |
| 15 | +Z3CHECK="$PROOFS/z3/verify.sh" |
| 16 | +REAL_SMT2="$PROOFS/z3/ond/OND_checks.smt2" |
| 17 | +SCRATCH="$(mktemp -d "${TMPDIR:-/tmp}/az-gate-selftest.XXXXXX")" |
| 18 | +trap 'rm -rf "$SCRATCH"' EXIT |
| 19 | +STUB="$SCRATCH/bin"; mkdir -p "$STUB" "$SCRATCH/home" |
| 20 | +cases=0; fails=0 |
| 21 | +pass() { cases=$((cases+1)); echo "PASS: $1"; } |
| 22 | +flunk() { cases=$((cases+1)); fails=$((fails+1)); echo "FAIL: $1"; } |
| 23 | + |
| 24 | +for s in "$GATE" "$Z3CHECK"; do bash -n "$s" || { echo "FAIL: $s does not parse"; exit 1; }; done |
| 25 | + |
| 26 | +mkstub() { printf '#!/bin/sh\n%s\n' "${2:-exit 0}" > "$STUB/$1"; chmod +x "$STUB/$1"; } |
| 27 | +for t in coqc coq_makefile make agda lake isabelle accom verifier idris2; do mkstub "$t"; done |
| 28 | +z3_stub() { mkstub z3 "case \"\${1:-}\" in --version) echo \"Z3 version stub\";; *) printf '$1';; esac"; } |
| 29 | +z3_stub 'sat\nunsat\nsat\n' |
| 30 | +for s in "$STUB"/*; do sh -n "$s" || { echo "FAIL: stub $s does not parse"; exit 1; }; done |
| 31 | + |
| 32 | +OUT=""; RC=0 |
| 33 | +run_gate() { OUT="$(HOME="$SCRATCH/home" PATH="$STUB:/usr/bin:/bin" MIZFILES="${MIZ-$SCRATCH/miz}" bash "$GATE" 2>&1)"; RC=$?; } |
| 34 | +# expect <label> <exit-wanted> <must-contain> <must-not-contain> |
| 35 | +expect() { |
| 36 | + local label=$1 want=$2 must=$3 mustnot=$4 |
| 37 | + if [ "$RC" -ne "$want" ]; then flunk "$label — exit $RC, wanted $want"; printf '%s\n' "$OUT" | tail -6 | sed 's/^/ /'; return; fi |
| 38 | + if [ -n "$must" ] && ! printf '%s\n' "$OUT" | grep -qF -- "$must"; then flunk "$label — output lacks '$must'"; printf '%s\n' "$OUT" | tail -6 | sed 's/^/ /'; return; fi |
| 39 | + if [ -n "$mustnot" ] && printf '%s\n' "$OUT" | grep -qF -- "$mustnot"; then flunk "$label — output contains '$mustnot'"; return; fi |
| 40 | + pass "$label" |
| 41 | +} |
| 42 | + |
| 43 | +# A. positive control: every stub present and green |
| 44 | +run_gate; expect "A all provers present -> ALL-PROVERS-GREEN" 0 "ALL-PROVERS-GREEN" "SOME PROVERS FAILED" |
| 45 | +# B. isabelle absent must FAIL (pre-2026-09-23: printed 'skipped', stayed green) |
| 46 | +mv "$STUB/isabelle" "$SCRATCH/isabelle.off"; run_gate |
| 47 | +expect "B isabelle absent -> fail" 1 "isabelle missing" "ALL-PROVERS-GREEN" |
| 48 | +mv "$SCRATCH/isabelle.off" "$STUB/isabelle" |
| 49 | +# C. mizar verifier absent must FAIL |
| 50 | +mv "$STUB/verifier" "$SCRATCH/verifier.off"; run_gate |
| 51 | +expect "C mizar verifier absent -> fail" 1 "mizar verifier / MIZFILES missing" "ALL-PROVERS-GREEN" |
| 52 | +mv "$SCRATCH/verifier.off" "$STUB/verifier" |
| 53 | +# D. MIZFILES unset must FAIL |
| 54 | +MIZ="" run_gate; expect "D MIZFILES unset -> fail" 1 "mizar verifier / MIZFILES missing" "ALL-PROVERS-GREEN" |
| 55 | +# E. z3 verdict drift (second verdict sat instead of unsat) must FAIL |
| 56 | +z3_stub 'sat\nsat\nsat\n'; run_gate |
| 57 | +expect "E z3 verdict mismatch -> fail" 1 "verdicts differ from annotations" "ALL-PROVERS-GREEN" |
| 58 | +# F. z3 (error ...) line must FAIL even when the verdicts match |
| 59 | +z3_stub 'sat\n(error "boom")\nunsat\nsat\n'; run_gate |
| 60 | +expect "F z3 (error line -> fail" 1 "z3 reported an error" "ALL-PROVERS-GREEN" |
| 61 | +# G. z3 'unknown' must FAIL |
| 62 | +z3_stub 'sat\nunknown\nsat\n'; run_gate |
| 63 | +expect "G z3 unknown verdict -> fail" 1 "verdicts differ from annotations" "ALL-PROVERS-GREEN" |
| 64 | +z3_stub 'sat\nunsat\nsat\n' |
| 65 | +# H. a prover that runs but fails must FAIL |
| 66 | +mkstub idris2 'exit 3'; run_gate; expect "H idris2 exit 3 -> fail" 1 "IDRIS FAILED" "ALL-PROVERS-GREEN"; mkstub idris2 |
| 67 | +# I. after the mutants, the positive control is green again (no state leaked) |
| 68 | +run_gate; expect "I positive control repeats green" 0 "ALL-PROVERS-GREEN" "SOME PROVERS FAILED" |
| 69 | + |
| 70 | +# ---- the expect-checker under a REAL z3 ------------------------------------ |
| 71 | +if ! command -v z3 >/dev/null; then flunk "J-M need a real z3 on PATH"; else |
| 72 | + # J. positive control: the committed file matches its annotations |
| 73 | + OUT="$(bash "$Z3CHECK" 2>&1)"; RC=$?; expect "J real z3, committed OND_checks.smt2 -> OK" 0 "Z3-CHECK OK" "Z3-CHECK FAILED" |
| 74 | + # K. expect-flipped mutant: 'expect unsat' -> 'expect sat' must FAIL |
| 75 | + mkdir -p "$SCRATCH/k"; sed 's/; expect unsat/; expect sat/' "$REAL_SMT2" > "$SCRATCH/k/mutant.smt2" |
| 76 | + grep -q '; expect unsat' "$SCRATCH/k/mutant.smt2" && flunk "K mutant not applied" |
| 77 | + OUT="$(bash "$Z3CHECK" "$SCRATCH/k" 2>&1)"; RC=$?; expect "K real z3, expect-flipped mutant -> fail" 1 "verdicts differ from annotations" "Z3-CHECK OK" |
| 78 | + # L. an unannotated (check-sat) must FAIL |
| 79 | + mkdir -p "$SCRATCH/l"; sed 's/; expect .*$//' "$REAL_SMT2" > "$SCRATCH/l/bare.smt2" |
| 80 | + OUT="$(bash "$Z3CHECK" "$SCRATCH/l" 2>&1)"; RC=$?; expect "L real z3, (check-sat) without expect -> fail" 1 "without an '; expect sat|unsat' annotation" "Z3-CHECK OK" |
| 81 | + # M. a root with no .smt2 must FAIL (vacuous) |
| 82 | + mkdir -p "$SCRATCH/m"; OUT="$(bash "$Z3CHECK" "$SCRATCH/m" 2>&1)"; RC=$?; expect "M no .smt2 files -> fail" 1 "no .smt2 files" "Z3-CHECK OK" |
| 83 | + # N. a file whose assertions are unsatisfiable where 'sat' is expected: z3 says unsat -> FAIL |
| 84 | + mkdir -p "$SCRATCH/n"; printf '(declare-const x Int)\n(assert (< x 0))\n(assert (> x 0))\n(check-sat) ; expect sat\n' > "$SCRATCH/n/contra.smt2" |
| 85 | + OUT="$(bash "$Z3CHECK" "$SCRATCH/n" 2>&1)"; RC=$?; expect "N real z3, contradictory assertions vs expect sat -> fail" 1 "verdicts differ from annotations" "Z3-CHECK OK" |
| 86 | +fi |
| 87 | + |
| 88 | +echo |
| 89 | +if [ "$fails" -eq 0 ]; then echo "GATE-SELFTEST OK: $cases/$cases cases"; exit 0; fi |
| 90 | +echo "GATE-SELFTEST FAILED: $fails of $cases cases"; exit 1 |
0 commit comments