219 lines
9.0 KiB
Bash
Executable File
219 lines
9.0 KiB
Bash
Executable File
#!/usr/bin/env bash
|
||
# validate-973.sh — #973 validation driver. One run produces the complete
|
||
# evidence chain for the 261-site conversion:
|
||
#
|
||
# 0. instrument self-test (microtest) — no validate evidence is trusted
|
||
# before the instrument itself has been proven, including its abort arms.
|
||
# 1. expected set: 261 coordinates from the FROZEN artifact (+7 header
|
||
# shift: 3 converter lines + 4 #984 guard lines), count asserted against the number declared below BEFORE any
|
||
# suite runs.
|
||
# 2. static inventory: converted call sites re-derived from SOURCE TEXT,
|
||
# must equal the expected set exactly (amendment ONE, leg 1 — the
|
||
# inventory comes from the text, never from the ledger).
|
||
# 3. green instrumented run: all ten suites with WAKE_ASSERT_LEDGER; each
|
||
# must exit 0 AND emit its own sentinel (per-suite formats differ and are
|
||
# pinned here — a suite that died early must never pass on another
|
||
# suite's output).
|
||
# 4. trace arithmetic on coordinate SETS (loops re-execute sites and the
|
||
# multi-grep lines append twice per pass, so counts are meaningless;
|
||
# sets are not):
|
||
# trace − expected MUST be empty (a helper ran at a coordinate the
|
||
# denominator never measured);
|
||
# expected − trace = converted-but-never-executed: enumerated, and
|
||
# every entry must carry a disposition in the
|
||
# committed unexecuted-sites-dispositions.txt, with
|
||
# no stale dispositions the other way (amendment
|
||
# ONE, legs 2+3 — the ledger is an execution trace,
|
||
# not an inventory; the difference is enumerated and
|
||
# individually dispositioned, never silently absent).
|
||
# 5. forced-error arms: the 19 denominator canaries plus one E-form and one
|
||
# F-form site, each run with WAKE_ASSERT_FORCE_GREP_ERROR_AT: the suite
|
||
# must emit the ARMED line (the arm proved it fired), the ABORT line
|
||
# naming the site, exit non-zero, emit NO sentinel, and the aborting
|
||
# site's ledger row must already be present (the append lands before the
|
||
# grep).
|
||
# 6. residual sweep: the denominator's own classifier finds zero unconverted
|
||
# verdict greps in the suites — and eight plants (six per-form + two
|
||
# absorb-branch probes, #985) in the same run.
|
||
#
|
||
# Output discipline (A10): every line that reports on a suite names the file
|
||
# under test; exit codes are reported before failure counts.
|
||
set -uo pipefail
|
||
|
||
HERE="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
|
||
WAKE="$(cd "$HERE/.." && pwd)"
|
||
CHECK="$HERE/check-973.py"
|
||
DISPO="$HERE/unexecuted-sites-dispositions.txt"
|
||
TMP="$(mktemp -d)"
|
||
trap 'rm -rf "$TMP"' EXIT
|
||
|
||
# Declared BEFORE any suite runs (A2): the run must produce THESE numbers,
|
||
# not be described by whatever numbers it produced.
|
||
EXPECTED_SUITES=10
|
||
EXPECTED_SITES=261
|
||
EXPECTED_ARMS=21
|
||
|
||
fails=0
|
||
flag() {
|
||
printf 'FAIL %s\n' "$*"
|
||
fails=$((fails + 1))
|
||
}
|
||
|
||
SUITES=(
|
||
test-wake-beacon.sh
|
||
test-wake-detector.sh
|
||
test-wake-digest-hmac.sh
|
||
test-wake-digest-quarantine.sh
|
||
test-wake-fn-oracle.sh
|
||
test-wake-install.sh
|
||
test-wake-preimage.sh
|
||
test-wake-reconcile.sh
|
||
test-wake-store-ack.sh
|
||
test-wake-store-enqueue-race.sh
|
||
)
|
||
[ "${#SUITES[@]}" -eq "$EXPECTED_SUITES" ] ||
|
||
flag "suite list has ${#SUITES[@]} entries, declared $EXPECTED_SUITES"
|
||
|
||
# Per-suite sentinel patterns, pinned: nine suites share the harness template
|
||
# (enqueue-race appends a tail after it); preimage uses its own format.
|
||
sentinel_for() {
|
||
case "$1" in
|
||
test-wake-preimage.sh) printf '%s' '^== test-wake-preimage: 17/17 passed ==$' ;;
|
||
*) printf '%s' 'harness: all invariants passed' ;;
|
||
esac
|
||
}
|
||
|
||
# --- 0: instrument self-test ------------------------------------------------
|
||
if bash "$HERE/microtest-wake-assert.sh" >"$TMP/microtest.out" 2>&1; then
|
||
echo "MICROTEST microtest-wake-assert.sh exit=0 (instrument proven)"
|
||
else
|
||
rc=$?
|
||
echo "MICROTEST microtest-wake-assert.sh exit=$rc"
|
||
sed 's/^/ /' "$TMP/microtest.out" | tail -n 15
|
||
flag "instrument self-test failed — no validate evidence below is trustworthy"
|
||
fi
|
||
|
||
# --- 1+2: expected set (artifact) vs static inventory (source text) ---------
|
||
python3 "$CHECK" expected | sort >"$TMP/expected.txt" ||
|
||
flag "check-973.py expected failed"
|
||
n_expected="$(grep -c . "$TMP/expected.txt")"
|
||
echo "EXPECTED-SET $n_expected coordinates (declared: $EXPECTED_SITES)"
|
||
[ "$n_expected" -eq "$EXPECTED_SITES" ] ||
|
||
flag "expected set has $n_expected coordinates, declared $EXPECTED_SITES"
|
||
|
||
python3 "$CHECK" static | sort >"$TMP/static.txt" ||
|
||
flag "check-973.py static failed"
|
||
if cmp -s "$TMP/expected.txt" "$TMP/static.txt"; then
|
||
echo "STATIC-INVENTORY equals expected set ($(grep -c . "$TMP/static.txt") rows from source text)"
|
||
else
|
||
flag "static inventory (source text) differs from expected set (artifact):"
|
||
diff "$TMP/expected.txt" "$TMP/static.txt" | head -n 20 | sed 's/^/ /'
|
||
fi
|
||
|
||
# --- 3: green instrumented run ----------------------------------------------
|
||
LEDGER="$TMP/ledger"
|
||
: >"$LEDGER"
|
||
for s in "${SUITES[@]}"; do
|
||
out="$(WAKE_ASSERT_LEDGER="$LEDGER" bash "$WAKE/$s" 2>&1)"
|
||
rc=$?
|
||
if printf '%s\n' "$out" | grep -Eq "$(sentinel_for "$s")"; then
|
||
sent="present"
|
||
else
|
||
sent="ABSENT"
|
||
fi
|
||
echo "SUITE $s exit=$rc sentinel=$sent"
|
||
[ "$rc" -eq 0 ] || flag "$s exited $rc in the green instrumented run"
|
||
[ "$sent" = "present" ] || flag "$s did not emit its sentinel"
|
||
done
|
||
|
||
# --- 4: trace arithmetic on coordinate sets ---------------------------------
|
||
sort -u "$LEDGER" >"$TMP/trace.txt"
|
||
echo "TRACE $(grep -c . "$TMP/trace.txt") distinct coordinates from $(grep -c . "$LEDGER") ledger rows"
|
||
|
||
comm -13 "$TMP/expected.txt" "$TMP/trace.txt" >"$TMP/rogue.txt"
|
||
if [ -s "$TMP/rogue.txt" ]; then
|
||
flag "trace contains coordinates OUTSIDE the frozen denominator:"
|
||
sed 's/^/ ROGUE /' "$TMP/rogue.txt"
|
||
else
|
||
echo "TRACE-MINUS-EXPECTED empty (no helper ran at an unmeasured coordinate)"
|
||
fi
|
||
|
||
comm -23 "$TMP/expected.txt" "$TMP/trace.txt" >"$TMP/unexec.txt"
|
||
n_unexec="$(grep -c . "$TMP/unexec.txt" || true)"
|
||
echo "UNEXECUTED $n_unexec of $EXPECTED_SITES converted sites did not execute in the green run"
|
||
if [ ! -f "$DISPO" ]; then
|
||
flag "disposition file missing: $DISPO — every unexecuted site must be individually dispositioned"
|
||
sed 's/^/ UNDISPOSITIONED /' "$TMP/unexec.txt"
|
||
else
|
||
awk '!/^#/ && NF >= 2 {print $1, $2}' "$DISPO" | sort -u >"$TMP/dispo-keys.txt"
|
||
comm -23 "$TMP/unexec.txt" "$TMP/dispo-keys.txt" >"$TMP/undispo.txt"
|
||
comm -13 "$TMP/unexec.txt" "$TMP/dispo-keys.txt" >"$TMP/stale-dispo.txt"
|
||
if [ -s "$TMP/undispo.txt" ]; then
|
||
flag "unexecuted sites WITHOUT a disposition:"
|
||
sed 's/^/ UNDISPOSITIONED /' "$TMP/undispo.txt"
|
||
fi
|
||
if [ -s "$TMP/stale-dispo.txt" ]; then
|
||
flag "dispositions for sites that DID execute (stale — the file no longer matches the run):"
|
||
sed 's/^/ STALE-DISPO /' "$TMP/stale-dispo.txt"
|
||
fi
|
||
if [ ! -s "$TMP/undispo.txt" ] && [ ! -s "$TMP/stale-dispo.txt" ]; then
|
||
echo "DISPOSITIONS all $n_unexec unexecuted sites individually dispositioned, none stale"
|
||
fi
|
||
fi
|
||
|
||
# --- 5: forced-error arms ---------------------------------------------------
|
||
python3 "$CHECK" arms >"$TMP/arms.txt" || flag "check-973.py arms failed"
|
||
n_arms="$(grep -c . "$TMP/arms.txt")"
|
||
echo "ARMS $n_arms forced-error arms (declared: $EXPECTED_ARMS)"
|
||
[ "$n_arms" -eq "$EXPECTED_ARMS" ] ||
|
||
flag "arm list has $n_arms entries, declared $EXPECTED_ARMS"
|
||
|
||
while read -r helper site form; do
|
||
f="${site%%:*}"
|
||
aled="$TMP/ledger-arm"
|
||
: >"$aled"
|
||
out="$(WAKE_ASSERT_LEDGER="$aled" WAKE_ASSERT_FORCE_GREP_ERROR_AT="$site" \
|
||
bash "$WAKE/$f" 2>&1)"
|
||
rc=$?
|
||
bad=""
|
||
[ "$rc" -ne 0 ] || bad="$bad exit=0"
|
||
printf '%s\n' "$out" | grep -q "WAKE-ASSERT ARMED: forcing real grep error at $site" ||
|
||
bad="$bad no-ARMED-line"
|
||
printf '%s\n' "$out" | grep -q "WAKE-ASSERT ABORT: ${helper} at ${site}: grep exit" ||
|
||
bad="$bad no-ABORT-line"
|
||
# AND-polarity check (a match is the defect): a grep error (rc>=2) must be
|
||
# its own loud arm — it cannot fall through as "no sentinel = pass".
|
||
rc_sent=0
|
||
printf '%s\n' "$out" | grep -Eq "$(sentinel_for "$f")" || rc_sent=$?
|
||
case "$rc_sent" in
|
||
0) bad="$bad sentinel-emitted" ;;
|
||
1) : ;;
|
||
*) bad="$bad sentinel-grep-error-rc=$rc_sent" ;;
|
||
esac
|
||
grep -q "^${helper} ${site}\$" "$aled" ||
|
||
bad="$bad no-ledger-row"
|
||
if [ -z "$bad" ]; then
|
||
echo "ARM $site ($form) exit=$rc armed+abort+no-sentinel+ledger-row"
|
||
else
|
||
echo "ARM $site ($form) exit=$rc DEFECTS:$bad"
|
||
flag "arm $site ($form) failed:$bad"
|
||
fi
|
||
done <"$TMP/arms.txt"
|
||
|
||
# --- 6: residual sweep ------------------------------------------------------
|
||
if python3 "$CHECK" sweep >"$TMP/sweep.out" 2>&1; then
|
||
echo "SWEEP exit=0"
|
||
else
|
||
echo "SWEEP exit=$?"
|
||
flag "residual sweep failed"
|
||
fi
|
||
sed 's/^/ /' "$TMP/sweep.out"
|
||
|
||
# --- summary (exit codes above, failure count last — A10) --------------------
|
||
echo
|
||
if [ "$fails" -gt 0 ]; then
|
||
echo "validate-973: FAILED ($fails failure(s))" >&2
|
||
exit 1
|
||
fi
|
||
echo "validate-973: OK — $EXPECTED_SUITES suites, $EXPECTED_SITES sites, $EXPECTED_ARMS arms, sweep clean"
|