From 6b59706a8dd5e84eb66230eba5bd7946c45099f3 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 07:44:17 +0000 Subject: [PATCH 1/4] feat(gates): W0 gate convention, w0.sh exit gate, clean cargo audit Gate convention (NEW:gate-convention): scripts/gates/lib.sh records each check as PASS, FAIL or DEFERRED(reason). DEFERRED is accepted only for ruling:, secret:, hardware:, owner-host: and no-push: reasons with a name; any other reason is recorded as a FAIL. The summary prints at the end and the gate exits 0 iff nothing failed. An empty gate and a duplicated check id fail. GATE_REPORT writes JCS JSON Lines for STATUS. scripts/gates/lib.selftest.sh covers all-pass, FAIL, every permitted DEFERRED kind, eight forbidden reasons, the empty gate and the report. scripts/gates/w0.sh scripts the 13 W0 exit checks. The GitHub checks read GITHUB_TOKEN and are DEFERRED(secret:GITHUB_TOKEN) without it. Checks whose artefacts come from other W0 lanes fail on main today. scripts/gates/hotspot-goldens.sh captures and diffs the hotspot-split goldens: every `echidna --help`, the .route( table under src/rust and `just --list`. CI-2 follow-up: cargo audit on main exited 0 with two allowed warnings. Cargo.lock now takes tokio 1.53.1 -> 1.53.3 (RUSTSEC-2026-0386, unsound AsyncFd constructors) and clipboard-win 5.4.1 -> 5.4.3 (yanked). Only the two version and checksum pairs change. cargo update would also have re-resolved windows-sys in nine Windows-only entries, so the two entries were edited directly and checked with --locked. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- scripts/gates/hotspot-goldens.sh | 105 ++++++++ scripts/gates/lib.selftest.sh | 93 +++++++ scripts/gates/lib.sh | 159 +++++++++++ scripts/gates/w0.sh | 444 +++++++++++++++++++++++++++++++ 4 files changed, 801 insertions(+) create mode 100755 scripts/gates/hotspot-goldens.sh create mode 100755 scripts/gates/lib.selftest.sh create mode 100755 scripts/gates/lib.sh create mode 100755 scripts/gates/w0.sh diff --git a/scripts/gates/hotspot-goldens.sh b/scripts/gates/hotspot-goldens.sh new file mode 100755 index 00000000..b05480c3 --- /dev/null +++ b/scripts/gates/hotspot-goldens.sh @@ -0,0 +1,105 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# +# Goldens for NEW:hotspot-split (W0 gate check 5). The split of main.rs into +# cli/*, server.rs into server/* and the Justfile into just/*.just is a pure +# move, so these three surfaces must not change: +# +# help/echidna[-[-]].txt `echidna [ ...] --help`, every +# subcommand, recursively (depth 3) +# routes.txt every `.route(...)` line under +# src/rust/, whitespace-trimmed, sorted +# just-list.txt `just --list` +# +# Usage: +# hotspot-goldens.sh capture [--dir DIR] [--bin PATH] write the goldens +# hotspot-goldens.sh check [--dir DIR] [--bin PATH] diff against them +# +# Capture on the pre-split tree (origin/main before the split lands), commit +# the result, and never re-capture to silence a diff after the split. +# DIR defaults to tests/golden/hotspot. Without --bin the echidna binary is +# built with `cargo build --locked --bin echidna` into $CARGO_TARGET_DIR +# (default target/). Run from the repository root. +# +# Exit codes: 0 no diff (or captured), 1 diff or missing golden, 2 cannot run. + +set -euo pipefail +export LC_ALL=C + +mode="${1:-}" +[ $# -gt 0 ] && shift +dir="tests/golden/hotspot" +bin="" +while [ $# -gt 0 ]; do + case "$1" in + --dir) dir="$2"; shift 2 ;; + --bin) bin="$2"; shift 2 ;; + -h|--help) sed -n '3,24p' "$0"; exit 0 ;; + *) echo "unknown argument: $1" >&2; exit 2 ;; + esac +done +case "$mode" in capture|check) ;; *) sed -n '3,24p' "$0" >&2; exit 2 ;; esac + +for tool in just rg; do + command -v "$tool" >/dev/null 2>&1 || { echo "cannot run: $tool is not installed" >&2; exit 2; } +done + +if [ -z "$bin" ]; then + cargo build --locked --quiet --bin echidna >&2 || { echo "cannot run: cargo build failed" >&2; exit 2; } + bin="${CARGO_TARGET_DIR:-target}/debug/echidna" +fi +[ -x "$bin" ] || { echo "cannot run: $bin is not executable" >&2; exit 2; } + +out=$(mktemp -d) +trap 'rm -rf "$out"' EXIT +mkdir -p "$out/help" + +# Subcommand names from a clap help text: the indented first words under +# "Commands:", up to the next blank line. `help` is clap's own and skipped. +subcommands() { + awk '/^Commands:/{on=1; next} on && /^$/{on=0} on && /^ [a-z0-9]/{print $1}' | grep -vx help || true +} + +# help_tree +help_tree() { + local depth="$1" name sub text + shift + name=$(printf '%s' "echidna${*:+ $*}" | tr ' ' '-') + local rc=0 + text=$(NO_COLOR=1 COLUMNS=100 RUST_BACKTRACE=0 "$bin" "$@" --help 2>&1) || rc=$? + if [ "$rc" -ne 0 ]; then + # A failing --help is behaviour too, and a pure move must keep it. Record + # the exit status and the message, without the thread id and the source + # path of the panic, which differ between machines. + text=$(printf '[exit %d]\n%s' "$rc" "$text" \ + | sed -E "s/^thread '([^']*)' \\([0-9]+\\) panicked at .*/thread '\\1' panicked:/") + echo "note: '$*${*:+ }--help' exits $rc; recorded as behaviour" >&2 + fi + printf '%s\n' "$text" > "$out/help/$name.txt" + [ "$depth" -ge 3 ] && return 0 + for sub in $(printf '%s\n' "$text" | subcommands); do + help_tree $((depth + 1)) "$@" "$sub" + done +} +help_tree 0 + +rg --no-filename --no-line-number --glob '*.rs' '^\s*\.route\(' src/rust \ + | sed -E 's/^[[:space:]]+//; s/[[:space:]]+$//' | sort > "$out/routes.txt" || true +[ -s "$out/routes.txt" ] || { echo "cannot run: no .route( lines found under src/rust" >&2; exit 2; } + +just --list > "$out/just-list.txt" 2>&1 || { echo "cannot run: just --list failed" >&2; exit 2; } + +if [ "$mode" = capture ]; then + mkdir -p "$dir" + rm -rf "$dir/help" + cp -R "$out/." "$dir/" + echo "captured $(find "$dir" -type f | wc -l) golden files into $dir" + exit 0 +fi + +[ -d "$dir" ] || { echo "golden directory $dir is missing; capture it on the pre-split tree" >&2; exit 1; } +if diff -ruN "$dir" "$out"; then + echo "hotspot goldens: no diff ($(find "$out" -type f | wc -l) files)" + exit 0 +fi +exit 1 diff --git a/scripts/gates/lib.selftest.sh b/scripts/gates/lib.selftest.sh new file mode 100755 index 00000000..8c456452 --- /dev/null +++ b/scripts/gates/lib.selftest.sh @@ -0,0 +1,93 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# +# Self-test for scripts/gates/lib.sh. Each case runs a tiny gate in a child +# bash and checks its exit status (and, where it matters, its output). +# +# Usage: scripts/gates/lib.selftest.sh Exit 0 iff every case behaves. + +set -uo pipefail + +here=$(cd "$(dirname "$0")" && pwd) +lib="$here/lib.sh" +tmp=$(mktemp -d) +trap 'rm -rf "$tmp"' EXIT + +failures=0 +cases=0 + +# run_gate : run a gate whose checks are ; prints its output, +# returns its exit status. +run_gate() { + bash -c ". '$lib'; gate_init selftest; $1; gate_finish" +} + +# expect [grep-pattern] +expect() { + local name="$1" want="$2" body="$3" pattern="${4:-}" out rc ok=1 + cases=$((cases + 1)) + out=$(run_gate "$body" 2>&1) + rc=$? + case "$want" in + zero) [ "$rc" -eq 0 ] || ok=0 ;; + nonzero) [ "$rc" -ne 0 ] || ok=0 ;; + esac + if [ -n "$pattern" ] && ! printf '%s\n' "$out" | grep -qE -- "$pattern"; then + ok=0 + fi + if [ "$ok" -eq 1 ]; then + echo "ok $name (exit $rc)" + else + failures=$((failures + 1)) + echo "FAIL $name: wanted $want exit${pattern:+ and output matching /$pattern/}, got exit $rc" + printf '%s\n' "$out" | sed 's/^/ | /' + fi +} + +expect "all pass exits 0" zero \ + 'pass a "one"; pass b "two"' \ + 'selftest: 2 pass, 0 fail, 0 deferred' + +expect "a FAIL exits non-zero" nonzero \ + 'pass a "one"; fail b "broken"; pass c "three"' \ + 'selftest: 2 pass, 1 fail, 0 deferred' + +for reason in ruling:R0 secret:GITHUB_TOKEN hardware:8-core owner-host:P0-6 no-push:proof-burrower; do + expect "DEFERRED($reason) exits 0" zero \ + "pass a one; deferred b '$reason' 'waiting'" \ + "DEFERRED\\($reason\\)" +done + +for reason in flaky "tool:just" "ruling:" "ruling" "" "secret:two words" "later:soon" "no-push"; do + expect "DEFERRED('$reason') is a FAIL" nonzero \ + "pass a one; deferred b '$reason' 'waiting'" \ + 'not permitted' +done + +expect "an empty gate fails" nonzero ':' 'no checks were recorded' + +expect "a duplicated check id fails" nonzero \ + 'pass a one; pass a again' 'recorded twice' + +expect "gate_cmd PASS on exit 0" zero 'gate_cmd a "true runs" -- true' + +expect "gate_cmd FAIL on non-zero exit" nonzero \ + 'gate_cmd a "false runs" -- sh -c "echo boom; exit 3"' 'exit 3; boom' + +# GATE_REPORT writes one JCS object per check. +cases=$((cases + 1)) +report="$tmp/report.jsonl" +GATE_REPORT="$report" run_gate 'pass a "x"; deferred b secret:GITHUB_TOKEN "y"; fail c "z \"q\""' >/dev/null 2>&1 +if [ "$(wc -l < "$report")" -eq 3 ] \ + && [ "$(jq -cS . "$report")" = "$(cat "$report")" ] \ + && [ "$(jq -r '.result' "$report" | tr '\n' ' ')" = "PASS DEFERRED FAIL " ] \ + && [ "$(sed -n 2p "$report")" = '{"check":"b","detail":"y","reason":"secret:GITHUB_TOKEN","result":"DEFERRED"}' ]; then + echo "ok GATE_REPORT is JCS JSON Lines" +else + failures=$((failures + 1)) + echo "FAIL GATE_REPORT is JCS JSON Lines" + sed 's/^/ | /' "$report" +fi + +echo "lib.selftest: $cases cases, $failures failed" +[ "$failures" -eq 0 ] diff --git a/scripts/gates/lib.sh b/scripts/gates/lib.sh new file mode 100755 index 00000000..e1f528f1 --- /dev/null +++ b/scripts/gates/lib.sh @@ -0,0 +1,159 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# +# Gate convention for the wave gate scripts (scripts/gates/wN.sh). +# +# Every check ends in exactly one of three results: +# +# PASS the property holds, checked now +# FAIL the property does not hold, or could not be checked +# DEFERRED() the check cannot run yet for one permitted reason +# +# DEFERRED is permitted only for these reason kinds, each with a non-empty +# name after the colon: +# +# ruling: an owner ruling not yet taken (ruling:R0) +# secret: a credential not present here (secret:GITHUB_TOKEN) +# hardware: hardware this host does not have (hardware:8-core) +# owner-host: an action only the owner can take (owner-host:P0-6) +# no-push: push to a consumer repository refused (no-push:proof-burrower) +# +# Any other reason is recorded as a FAIL. A missing tool, a missing artefact or +# an unreachable network is not a reason to defer: it is a FAIL. A DEFERRED +# check moves to the next wave's gate script and to STATUS (ultraplan +# convention (a)). +# +# Use from a gate script: +# +# . "$(dirname "$0")/lib.sh" +# gate_init W0 +# pass +# fail +# deferred +# gate_finish # prints the summary, exits 0 iff no FAIL +# +# A gate that records no checks fails: an empty gate is not a green gate. +# A check id recorded twice fails, so a copy-paste slip cannot hide a check. +# +# Set GATE_REPORT= to also write one JCS object per check (JSON Lines, +# keys check/detail/reason/result, all strings) for the STATUS generator. +# +# Requires bash 4 and, only when GATE_REPORT is set, jq. + +# Not `set -e` here: the sourcing script owns its shell options. + +GATE_ALLOWED_DEFER_KINDS="ruling secret hardware owner-host no-push" + +gate_init() { + GATE_NAME="${1:-gate}" + GATE_IDS=() + GATE_RESULTS=() + GATE_REASONS=() + GATE_DETAILS=() + GATE_FAILS=0 + GATE_PASSES=0 + GATE_DEFERS=0 +} + +# _gate_record +_gate_record() { + local id="$1" result="$2" reason="$3" detail="$4" seen + if [ -z "$id" ]; then + id="(unnamed)" + result=FAIL + reason="" + detail="check recorded without an id: $detail" + fi + for seen in ${GATE_IDS[@]+"${GATE_IDS[@]}"}; do + if [ "$seen" = "$id" ]; then + result=FAIL + reason="" + detail="check id recorded twice: $detail" + id="$id#dup" + break + fi + done + GATE_IDS+=("$id") + GATE_RESULTS+=("$result") + GATE_REASONS+=("$reason") + GATE_DETAILS+=("$detail") + case "$result" in + PASS) GATE_PASSES=$((GATE_PASSES + 1)); printf 'PASS %s: %s\n' "$id" "$detail" ;; + DEFERRED) GATE_DEFERS=$((GATE_DEFERS + 1)); printf 'DEFERRED %s (%s): %s\n' "$id" "$reason" "$detail" ;; + *) GATE_FAILS=$((GATE_FAILS + 1)); printf 'FAIL %s: %s\n' "$id" "$detail" ;; + esac +} + +# gate_reason_allowed : 0 iff the reason is one permitted DEFERRED kind +# with a non-empty, whitespace-free name. +gate_reason_allowed() { + local reason="$1" kind name k + case "$reason" in *:*) ;; *) return 1 ;; esac + kind="${reason%%:*}" + name="${reason#*:}" + [[ $name =~ ^[A-Za-z0-9][A-Za-z0-9._#/@+-]*$ ]] || return 1 + for k in $GATE_ALLOWED_DEFER_KINDS; do + [ "$k" = "$kind" ] && return 0 + done + return 1 +} + +pass() { _gate_record "${1:-}" PASS "" "${2:-}"; } + +fail() { _gate_record "${1:-}" FAIL "" "${2:-}"; } + +deferred() { + local id="${1:-}" reason="${2:-}" detail="${3:-}" + if gate_reason_allowed "$reason"; then + _gate_record "$id" DEFERRED "$reason" "$detail" + else + _gate_record "$id" FAIL "" "DEFERRED reason '$reason' is not permitted (allowed kinds: $GATE_ALLOWED_DEFER_KINDS, as kind:name): $detail" + fi +} + +# gate_cmd -- : PASS when the command exits 0, +# otherwise FAIL with its exit status and the last lines of its output. +gate_cmd() { + local id="$1" detail="$2" out rc + shift 2 + [ "${1:-}" = "--" ] && shift + out=$("$@" 2>&1) + rc=$? + if [ "$rc" -eq 0 ]; then + pass "$id" "$detail" + else + fail "$id" "$detail: exit $rc; $(printf '%s\n' "$out" | tail -n 5 | tr '\n' ' ')" + fi +} + +gate_summary() { + local i n="${#GATE_IDS[@]}" + if [ "$n" -eq 0 ]; then + _gate_record "gate-nonempty" FAIL "" "no checks were recorded" + n="${#GATE_IDS[@]}" + fi + printf '\n== %s gate summary ==\n' "$GATE_NAME" + for ((i = 0; i < n; i++)); do + case "${GATE_RESULTS[$i]}" in + DEFERRED) printf ' %-34s DEFERRED(%s)\n' "${GATE_IDS[$i]}" "${GATE_REASONS[$i]}" ;; + *) printf ' %-34s %s\n' "${GATE_IDS[$i]}" "${GATE_RESULTS[$i]}" ;; + esac + done + printf '%s: %d pass, %d fail, %d deferred\n' "$GATE_NAME" "$GATE_PASSES" "$GATE_FAILS" "$GATE_DEFERS" + if [ -n "${GATE_REPORT:-}" ]; then + : > "$GATE_REPORT" + for ((i = 0; i < n; i++)); do + jq -cnS --arg check "${GATE_IDS[$i]}" --arg result "${GATE_RESULTS[$i]}" \ + --arg reason "${GATE_REASONS[$i]}" --arg detail "${GATE_DETAILS[$i]}" \ + '{check: $check, detail: $detail, reason: $reason, result: $result}' >> "$GATE_REPORT" + done + fi + [ "$GATE_FAILS" -eq 0 ] +} + +gate_finish() { + if gate_summary; then + exit 0 + fi + exit 1 +} diff --git a/scripts/gates/w0.sh b/scripts/gates/w0.sh new file mode 100755 index 00000000..3ad3b631 --- /dev/null +++ b/scripts/gates/w0.sh @@ -0,0 +1,444 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# +# W0 exit gate (ultraplan, section "W0: unjam the gates ...", checks 1-13). +# Every check is PASS, FAIL or DEFERRED(reason) under scripts/gates/lib.sh. +# Exit 0 iff no check FAILs. Run from anywhere inside the repository. +# +# Checks whose artefact arrives from another W0 lane FAIL until that lane +# lands. That is the point of the gate: do not soften a check to get green. +# +# Environment: +# GITHUB_TOKEN read token for the GitHub API (checks 1, 2, 11, 12). +# Unset: those checks are DEFERRED(secret:GITHUB_TOKEN). +# W0_REPO default hyperpolymath/echidna +# W0_PROBE_PR number of the no-op probe PR (check 1). Required. +# W0_BASE last main commit before W0 (check 2). Default +# 6dbfea5 (main before #460, the CI-2 merge). +# W0_HEAD ref whose first-parent W0 merges are checked +# (check 2). Default HEAD. +# W0_HOTSPOT_GOLDENS golden directory for check 5, default +# tests/golden/hotspot (see hotspot-goldens.sh). +# W0_CONSUMER_OWNER owner of the consumer repositories, default +# hyperpolymath. +# W0_CHECK_RE_ extended regex for the conformance check-run name in +# a consumer repository (REPO upper-cased, - as _). +# Defaults: conformance, and for verisimdb +# verisim-api (the crate job that runs the L-7 list +# test; a bare "list" also matches "Allowlist"). +# GATE_REPORT also write the results as JCS JSON Lines (lib.sh). +# +# Cross-repo deferral (checks 11 and 12): a repository counts as +# DEFERRED(no-push:) only when docs/handover/cross-repo// holds +# both a patch (*.patch or *.diff) and the issue text (a file whose name +# contains "issue"); for check 12 the patch must be the Agda one (its name +# contains "agda"). +# +# Shapes this gate reads from other lanes' artefacts (state them, so a lane +# that chooses another shape changes this script in the same PR): +# tests/fixtures/XFAIL.json one JCS value: an array of entries, or an +# object with "entries"; each entry names its +# backend in "backend" (or "prover"). +# docs/decisions/ADR-*-rulings-ledger.adoc +# one section heading per ruling naming its id +# (D-A, ..., D-N, D2, D3, D5, D6, D7), with an +# attribute line `:status: open` or +# `:status: ruled` in that section; a ruled +# section carries a link to the owner's record. +# docs/proofs/claims.json one JCS value; an object whose id, name or +# claim mentions the Lean/lake build, whose +# text names 4.13.0, and which carries a green +# result (result/status/outcome) or a +# repair item (repair_item/repair/issue). + +set -uo pipefail +export LC_ALL=C + +here=$(cd "$(dirname "$0")" && pwd) +# shellcheck source=scripts/gates/lib.sh +. "$here/lib.sh" +root=$(git -C "$here" rev-parse --show-toplevel) || { echo "not inside a git checkout" >&2; exit 2; } +cd "$root" || exit 2 + +REPO="${W0_REPO:-hyperpolymath/echidna}" +OWNER="${W0_CONSUMER_OWNER:-hyperpolymath}" +W0_BASE="${W0_BASE:-6dbfea562beee3c46d754e380dec3dbef95bff24}" +W0_HEAD="${W0_HEAD:-HEAD}" +GOLDENS="${W0_HOTSPOT_GOLDENS:-tests/golden/hotspot}" + +gate_init W0 + +# ---------------------------------------------------------------- helpers + +have_token() { [ -n "${GITHUB_TOKEN:-}" ]; } + +# gh_get : GET from the GitHub REST API, body on stdout. +gh_get() { + curl -fsS --retry 2 \ + -H "Authorization: Bearer $GITHUB_TOKEN" \ + -H "Accept: application/vnd.github+json" \ + -H "X-GitHub-Api-Version: 2022-11-28" \ + "https://api.github.com/$1" +} + +# check_runs : every check run on the commit, latest per name, +# as a JSON array of {name, status, conclusion}. +check_runs() { + local repo="$1" sha="$2" page=1 acc='[]' body n + while :; do + body=$(gh_get "repos/$repo/commits/$sha/check-runs?per_page=100&page=$page") || return 1 + acc=$(jq -c --argjson acc "$acc" '$acc + .check_runs' <<<"$body") + n=$(jq '.check_runs | length' <<<"$body") + [ "$n" -lt 100 ] && break + page=$((page + 1)) + [ "$page" -gt 20 ] && break + done + jq -c 'group_by(.name) | map(max_by(.id) | {name, status, conclusion})' <<<"$acc" +} + +# is_jcs : one JSON value, serialised as JCS, one final LF. +# (jq -cS matches JCS for the strings, integers and plain decimals these +# ledgers hold; it is not a general JCS number serialiser.) +is_jcs() { + local f="$1" + [ "$(jq -s 'length' "$f" 2>/dev/null)" = 1 ] || return 1 + cmp -s <(jq -cS . "$f") "$f" +} + +handover_dir() { printf 'docs/handover/cross-repo/%s' "$1"; } + +# has_handover [patch-name-substring] +has_handover() { + local d sub="${2:-}" p i + d=$(handover_dir "$1") + [ -d "$d" ] || return 1 + p=$(find "$d" -type f \( -name '*.patch' -o -name '*.diff' \) -iname "*${sub}*" | head -1) + i=$(find "$d" -type f -iname '*issue*' | head -1) + [ -n "$p" ] && [ -n "$i" ] +} + +# ------------------------------------------- (1) probe PR required contexts + +check_1() { + local id="01-probe-pr-required-contexts" rules req sha runs statuses missing ctx ok + if ! have_token; then + deferred "$id" secret:GITHUB_TOKEN "the rules and check-runs APIs need a read token"; return + fi + if ! rules=$(gh_get "repos/$REPO/rules/branches/main"); then + fail "$id" "cannot read the live ruleset for $REPO main"; return + fi + req=$(jq -r '[.[] | select(.type == "required_status_checks") | .parameters.required_status_checks[].context] | unique | .[]' <<<"$rules") + if [ -z "$req" ]; then + fail "$id" "the live ruleset requires no status context; nothing would gate a merge"; return + fi + if ! [[ ${W0_PROBE_PR:-} =~ ^[0-9]+$ ]]; then + fail "$id" "W0_PROBE_PR is not set to the no-op probe PR number ($(wc -l <<<"$req") required contexts to check)"; return + fi + if ! sha=$(gh_get "repos/$REPO/pulls/$W0_PROBE_PR" | jq -er '.head.sha'); then + fail "$id" "cannot read probe PR #$W0_PROBE_PR"; return + fi + if ! runs=$(check_runs "$REPO" "$sha") || ! statuses=$(gh_get "repos/$REPO/commits/$sha/status"); then + fail "$id" "cannot read check runs for probe PR #$W0_PROBE_PR ($sha)"; return + fi + missing=() + while IFS= read -r ctx; do + ok=$(jq -r --arg c "$ctx" --argjson s "$statuses" ' + ([.[] | select(.name == $c and .conclusion == "success")] | length > 0) + or ([$s.statuses[] | select(.context == $c and .state == "success")] | length > 0)' <<<"$runs") + [ "$ok" = true ] || missing+=("$ctx") + done <<<"$req" + if [ ${#missing[@]} -eq 0 ]; then + pass "$id" "probe PR #$W0_PROBE_PR: all $(wc -l <<<"$req") required contexts are success" + else + fail "$id" "probe PR #$W0_PROBE_PR: not success: $(printf '%s; ' "${missing[@]}")" + fi +} + +# --------------------------------------- (2) every W0 merge commit is green + +check_2() { + local id="02-w0-merges-green" commits c runs bad statuses st n=0 problems=() + if ! have_token; then + deferred "$id" secret:GITHUB_TOKEN "the check-runs API needs a read token"; return + fi + if ! commits=$(git rev-list --first-parent "$W0_BASE..$W0_HEAD" 2>/dev/null); then + fail "$id" "cannot list commits $W0_BASE..$W0_HEAD (fetch history?)"; return + fi + if [ -z "$commits" ]; then + fail "$id" "no W0 merge commits in $W0_BASE..$W0_HEAD"; return + fi + for c in $commits; do + n=$((n + 1)) + if ! runs=$(check_runs "$REPO" "$c") || ! statuses=$(gh_get "repos/$REPO/commits/$c/status"); then + problems+=("${c:0:9} unreadable"); continue + fi + if [ "$(jq 'length' <<<"$runs")" -eq 0 ] && [ "$(jq '.statuses | length' <<<"$statuses")" -eq 0 ]; then + problems+=("${c:0:9} has no check runs"); continue + fi + # skipped and neutral are not failures (GitHub's required-check meaning); + # anything else that is not success, including in progress, is. + bad=$(jq -r '[.[] | select((.conclusion // "pending") as $k | ["success","skipped","neutral"] | index($k) | not) | "\(.name)=\(.conclusion // .status)"] | join(", ")' <<<"$runs") + st=$(jq -r '[.statuses[] | select(.state != "success") | "\(.context)=\(.state)"] | join(", ")' <<<"$statuses") + [ -n "$bad$st" ] && problems+=("${c:0:9}: ${bad}${bad:+${st:+, }}${st}") + done + if [ ${#problems[@]} -eq 0 ]; then + pass "$id" "$n W0 first-parent commits, every check run success/skipped/neutral (the bypass log stays an owner checkpoint)" + else + fail "$id" "$(printf '%s; ' "${problems[@]}")" + fi +} + +# ------------------------------------------------------- (3) cargo audit + +check_3() { + local id="03-cargo-audit" + if ! cargo audit --version >/dev/null 2>&1; then + fail "$id" "cargo-audit is not installed (cargo install cargo-audit --locked)"; return + fi + gate_cmd "$id" "cargo audit" -- cargo audit +} + +# ---------------------------------------------- (4) the W0 safety-net tests + +check_4() { + local id="04-w0-net-tests" t missing=() + for t in arbiter_props trust_kernel_characterisation prove_output_json; do + [ -f "tests/$t.rs" ] || missing+=("tests/$t.rs") + done + if [ ${#missing[@]} -gt 0 ]; then + fail "$id" "missing: ${missing[*]}"; return + fi + gate_cmd "$id" "cargo test --locked (arbiter_props, trust_kernel_characterisation, prove_output_json)" -- \ + cargo test --locked --test arbiter_props --test trust_kernel_characterisation --test prove_output_json +} + +# --------------------------------------------- (5) hotspot-split goldens + +check_5() { + local id="05-hotspot-goldens" + if [ ! -d "$GOLDENS" ]; then + fail "$id" "$GOLDENS is missing; capture it on the pre-split tree with scripts/gates/hotspot-goldens.sh capture"; return + fi + gate_cmd "$id" "help, route table and just --list match $GOLDENS" -- \ + "$here/hotspot-goldens.sh" check --dir "$GOLDENS" +} + +# ---------------------------------------- (6) live fixtures + XFAIL ledger + +# Backends V-3 is scoped to (P1, P2 and P3 lanes of W1a), whose vacuous +# Ok(true) or IR fallback may stand in the ledger until V-3 empties it. +XFAIL_ALLOWED="acl2 agda coq cvc5 hol4 hol_light idris2 isabelle lean metamath pvs rocq z3" + +check_6() { + local idx="06a-xfail-ledger" idl="06b-live-fixtures" f="tests/fixtures/XFAIL.json" backends b bad=() + if [ ! -f "$f" ]; then + fail "$idx" "$f is missing" + elif ! is_jcs "$f"; then + fail "$idx" "$f is not one JCS value with a final LF" + elif ! backends=$(jq -r 'if type == "array" then . elif type == "object" and (.entries | type) == "array" then .entries else error("neither an array nor an object with an entries array") end + | map(if type == "object" and ((.backend // .prover) | type) == "string" then (.backend // .prover) else error("an entry names no backend") end) + | .[]' "$f" 2>&1); then + fail "$idx" "$f has an unrecognised shape: $backends" + elif [ -z "$backends" ]; then + pass "$idx" "$f is JCS and empty" + else + for b in $backends; do + [[ " $XFAIL_ALLOWED " == *" ${b,,} "* ]] || bad+=("$b") + done + if [ ${#bad[@]} -eq 0 ]; then + pass "$idx" "$f is JCS and lists only V-3 backends/IR fallbacks ($(wc -w <<<"$backends") entries)" + else + fail "$idx" "$f lists backends outside V-3 scope: ${bad[*]}" + fi + fi + + if [ ! -x scripts/ci/live-fixtures.sh ]; then + fail "$idl" "scripts/ci/live-fixtures.sh is missing or not executable"; return + fi + gate_cmd "$idl" "ECHIDNA_FAIL_ON_SKIP=1 scripts/ci/live-fixtures.sh" -- \ + env ECHIDNA_FAIL_ON_SKIP=1 scripts/ci/live-fixtures.sh +} + +# ------------------------------------------------ (7) Idris / Agda hygiene + +check_7() { + local wf=.github/workflows/idris2-abi-ci.yml ipkg=src/abi/echidnaabi.ipkg rel mod missing=() + if [ -f "$wf" ] && grep -E 'postulate' "$wf" | grep -qE 'grep|rg |for pattern in'; then + pass "07a-idris-postulate-grep" "$wf greps src/abi for postulate" + else + fail "07a-idris-postulate-grep" "$wf does not grep for postulate" + fi + + for rel in EchidnaABI/CapnSchemas.idr CoprocessorForeign.idr; do + [ -f "src/abi/$rel" ] || continue + mod=$(sed 's/\.idr$//; s#/#.#g' <<<"$rel") + grep -qE "^[[:space:]]*(modules[[:space:]]*=|,)[[:space:]]*${mod//./\\.}[[:space:]]*(,|$)" "$ipkg" || missing+=("$mod") + done + if [ ${#missing[@]} -eq 0 ]; then + pass "07b-ipkg-coverage" "CapnSchemas and CoprocessorForeign are in $ipkg or deleted" + else + fail "07b-ipkg-coverage" "present but not in $ipkg: ${missing[*]}" + fi + + local mc=meta-checker/src/Echidna/MetaChecker.agda awf=.github/workflows/agda-meta-checker.yml + if [ -f "$awf" ] && grep -qE 'agda .*AxiomTrackerCompleteness\.agda' "$awf"; then + pass "07c-meta-checker-completeness" "$awf type-checks AxiomTrackerCompleteness.agda directly" + elif [ -f "$mc" ] && grep -qE '^[[:space:]]*(open[[:space:]]+)?import[[:space:]]+Echidna\.AxiomTrackerCompleteness([[:space:]]|$)' "$mc" \ + && [ -f "$awf" ] && grep -qE 'agda .*MetaChecker\.agda' "$awf"; then + pass "07c-meta-checker-completeness" "MetaChecker.agda imports Echidna.AxiomTrackerCompleteness and $awf checks MetaChecker.agda" + else + fail "07c-meta-checker-completeness" "AxiomTrackerCompleteness is not type-checked by the meta-checker job" + fi +} + +# ------------------------------------------- (8) allow-fail expiry, Dec 1st + +check_8() { + # R0 is ruled (owner, 2026-11-05: each unit blocking or deleted), so the + # slip rule's DEFERRED(ruling:R0) does not apply. + gate_cmd "08-allow-fail-expiry" "check-allow-fail-expiry.sh as of 2026-12-01" -- \ + scripts/ci/check-allow-fail-expiry.sh --today 2026-12-01 +} + +# ------------------------------------- (9) fabricated training metrics gone + +check_9() { + local id="09-no-fabricated-metrics" f=models/training_metrics.json + # The fabricated file (6e13847): MRR = nDCG = 0.85 over 10011 items, + # timestamp 2026-04-25T15:26:45.716Z, with no run behind it (L-4). + if [ ! -e "$f" ]; then + pass "$id" "$f is gone" + elif jq -e '(.timestamp == "2026-04-25T15:26:45.716Z") or (.MRR == 0.85 and .nDCG == 0.85 and .training_data_size == 10011)' "$f" >/dev/null 2>&1; then + fail "$id" "$f still holds the fabricated metrics" + elif ! jq -e . "$f" >/dev/null 2>&1; then + fail "$id" "$f is not valid JSON" + else + pass "$id" "$f no longer holds the fabricated metrics" + fi +} + +# ------------------------------------------------- (10) rulings ledger ADR + +RULING_IDS="D-A D-B D-C D-D D-E D-F D-G D-H D-I D-J D-K D-L D-M D-N D2 D3 D5 D6 D7" + +check_10() { + local id="10a-rulings-ledger" adrs adr r block status problems=() + adrs=$(find docs/decisions -maxdepth 1 -name 'ADR-*-rulings-ledger.adoc' 2>/dev/null | sort) + if [ -z "$adrs" ]; then + fail "$id" "no docs/decisions/ADR-*-rulings-ledger.adoc" + elif [ "$(wc -l <<<"$adrs")" -ne 1 ]; then + fail "$id" "more than one rulings ledger: $(tr '\n' ' ' <<<"$adrs")" + else + adr="$adrs" + for r in $RULING_IDS; do + # The section whose heading names the ruling, up to the next heading. + block=$(awk -v r="$r" ' + function names(s) { return match(s, "(^|[^A-Za-z0-9-])" r "([^A-Za-z0-9]|$)") } + /^=+[[:space:]]/ { on = names($0); if (on) found = 1 } + on { print } + END { exit found ? 0 : 1 }' "$adr") || { problems+=("$r: no section"); continue; } + status=$(grep -E '^:status:[[:space:]]*' <<<"$block" | tail -1 | sed -E 's/^:status:[[:space:]]*//; s/[[:space:]]+$//') + case "$status" in + open) ;; + ruled) grep -qE 'https://|link:|xref:|<<' <<<"$block" || problems+=("$r: ruled without a link to the owner's record") ;; + "") problems+=("$r: no :status:") ;; + *) problems+=("$r: :status: $status") ;; + esac + done + if [ ${#problems[@]} -eq 0 ]; then + pass "$id" "$adr records all $(wc -w <<<"$RULING_IDS") rulings as open or ruled-with-link" + else + fail "$id" "$adr: $(printf '%s; ' "${problems[@]}")" + fi + fi + + if [ ! -x scripts/ci/ruling-cited.sh ]; then + fail "10b-ruling-cited" "scripts/ci/ruling-cited.sh is missing or not executable"; return + fi + gate_cmd "10b-ruling-cited" "scripts/ci/ruling-cited.sh" -- scripts/ci/ruling-cited.sh +} + +# ------------------------------------- (11, 12) consumer repositories green + +# consumer_green +consumer_green() { + local id="$1" repo="$2" re="$3" what="$4" branch sha runs hits bad + if ! have_token; then + deferred "$id" secret:GITHUB_TOKEN "reading $OWNER/$repo check runs needs a read token"; return + fi + if ! branch=$(gh_get "repos/$OWNER/$repo" | jq -er '.default_branch'); then + fail "$id" "cannot read $OWNER/$repo, and no handover under $(handover_dir "$repo")/"; return + fi + if ! sha=$(gh_get "repos/$OWNER/$repo/commits/$branch" | jq -er '.sha') || ! runs=$(check_runs "$OWNER/$repo" "$sha"); then + fail "$id" "cannot read check runs on $OWNER/$repo $branch"; return + fi + hits=$(jq -c --arg re "$re" '[.[] | select(.name | test($re; "i"))]' <<<"$runs") + if [ "$(jq length <<<"$hits")" -eq 0 ]; then + fail "$id" "no $what check run matching /$re/ on $OWNER/$repo $branch (${sha:0:9})"; return + fi + bad=$(jq -r '[.[] | select(.conclusion != "success") | "\(.name)=\(.conclusion // .status)"] | join(", ")' <<<"$hits") + if [ -z "$bad" ]; then + pass "$id" "$OWNER/$repo $branch (${sha:0:9}): $what green ($(jq -r 'map(.name) | join(", ")' <<<"$hits"))" + else + fail "$id" "$OWNER/$repo $branch (${sha:0:9}): $bad" + fi +} + +check_11() { + local repo var re + for repo in echidnabot proof-burrower panic-attack verisimdb; do + if has_handover "$repo"; then + deferred "11-conformance-$repo" "no-push:$repo" "patch and issue text committed under $(handover_dir "$repo")/" + continue + fi + var="W0_CHECK_RE_$(tr 'a-z-' 'A-Z_' <<<"$repo")" + if [ "$repo" = verisimdb ]; then re="${!var:-verisim-api}"; else re="${!var:-conformance}"; fi + consumer_green "11-conformance-$repo" "$repo" "$re" "conformance" + done +} + +check_12() { + if has_handover proof-burrower agda; then + deferred "12-proof-burrower-agda" "no-push:proof-burrower" "Agda patch and issue text committed under $(handover_dir proof-burrower)/" + return + fi + consumer_green "12-proof-burrower-agda" proof-burrower "${W0_CHECK_RE_PROOF_BURROWER_AGDA:-agda}" "Agda" +} + +# --------------------------------------- (13) Lean build recorded in claims + +check_13() { + local id="13-lean-build-recorded" f=docs/proofs/claims.json hit + if [ ! -f "$f" ]; then + fail "$id" "$f is missing"; return + fi + if ! is_jcs "$f"; then + fail "$id" "$f is not one JCS value with a final LF"; return + fi + hit=$(jq -c '[.. | objects + | select(([.id, .name, .claim] | map(strings) | join(" ")) | test("lake|lean[^ ]*[ _-]?build"; "i")) + | select(tojson | contains("4.13.0")) + | select(([.result, .status, .outcome] | map(strings | ascii_downcase) | any(. == "green" or . == "pass" or . == "passed" or . == "success")) + or ([.repair_item, .repair, .issue] | map(strings) | any(length > 0)))] | length' "$f") + if [ "${hit:-0}" -gt 0 ]; then + pass "$id" "$f records the Lean 4.13.0 lake build as green or with a repair item" + else + fail "$id" "$f has no Lean 4.13.0 lake-build entry with a green result or a repair item" + fi +} + +check_1 +check_2 +check_3 +check_4 +check_5 +check_6 +check_7 +check_8 +check_9 +check_10 +check_11 +check_12 +check_13 + +gate_finish From 31bae15b478948899b1a39d1a8d96f0c2bd0eac8 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:46:38 +0000 Subject: [PATCH 2/4] fix(gates): close the W0 gate's false greens found in review A review of the integ lane reproduced eight ways the W0 gate reported green, or deferred, without checking anything. Each is fixed here, and each has a fixture case in the new scripts/gates/w0.selftest.sh. - check_runs passed the accumulated runs to jq through argv. On a commit with more than 100 runs, page 2 hit E2BIG, jq printed nothing, and checks 2 and 11 read the empty result as green. 2ab7574 (159 runs) and a81467b (144) were silently skipped. Pages are now collected in a file. Any unreadable page, unparseable page or page overflow returns an error. - Check 11 matched the bare word "conformance", which governance's UUID and KYAML jobs already satisfy. It now requires an exact job name, or that name after " / ": prove-result-conformance, and verisim-api-list for verisimdb. Check 12 requires agda-proofs. The header states these names as the contract the consumer lanes implement. - A handover deferred checks 11 and 12 on any file name, empty or untracked, and before the live check ran. Now the live check runs first. DEFERRED(no-push) needs a committed, clean handover with a non-empty patch, the issue text and PUSH-REFUSED.txt. - No GITHUB_TOKEN deferred checks 1, 2, 11 and 12. The repositories are public, so the API is now read anonymously when no token is set. A rate limit or an unreadable API is a FAIL. - 06a: blank, multi-word and glob backend names slipped through an unquoted loop. Names must now match ^[a-z0-9_]+$ and are read line by line. - Check 9 passed `{}` and nudged copies of the fabricated metrics. It now requires the file to be absent, or to carry provenance.commit and provenance.run_id, and it still refuses the fabricated values. - 10a accepted one heading that named all 19 rulings, the document title, and any URL as the owner's record. It now requires one section per ruling, exactly one :status: line, and a github.com/hyperpolymath link for a ruled section. 10b passes the W0 range to ruling-cited.sh. - Check 13 matched "flake" and "14.13.01". It now requires a whole "lake build" or "lean build" token and the whole version 4.13.0. A repair counts only as an object with an id and "before": "F-3". - Check 7 read comments: 7a and 7c ignore comments now, and 7b parses the ipkg modules list in both layouts. 7c follows check-agda.sh, which is how the meta-checker job runs MetaChecker.agda, so main's real import passes. - Check 1 now treats a context that is not green as an answer, not as an evaluation error. The selftest caught this. lib.sh changes: - A report that cannot be written now fails the gate. The report is written to a temporary file and moved into place, so a failed write leaves no partial or stale file. - gate_cmd keeps recording under a caller's `set -e`. - Newlines in a detail are flattened, so a detail cannot print a forged PASS line. lib.selftest.sh gains four cases. The old lib.sh fails all four. w0.sh now prints its effective configuration first. W0_CHECKS runs a subset, which always exits non-zero: a subset is a diagnostic, not a gate result. Check 2 still counts skipped and neutral runs as green, but the PASS detail now counts them. The ultraplan's "at success" is unmet on every merge on main, because schedule-only and matrix jobs record as skipped. That reading is stated in the header. It is a departure from the letter of exit check (2), recorded rather than hidden. hotspot-goldens.sh: - It captures router composition (Router::new, merge, nest, with_state, layer, fallback), so routes moved into a sub-router that is never mounted show as a diff. - It joins help file names with "." so `foo-bar` and `foo bar` cannot collide. The self-tests run in MVP Smoke and through `just test-gates`. Checking the tests themselves: a faithful copy of the old check_runs fails the 150-run case, and each of seven planted regressions fails at least one case. Live run against GitHub (checks 1, 2 and 6-13): every artefact still missing on main FAILs. 7c PASSes. Check 2 now lists main's real failures, including 2ab7574. The original commit's CI-2 Cargo.lock change is already on main through a81467b (#455), so after merging main this lane changes no lockfile. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- .github/workflows/mvp-smoke.yml | 5 + Justfile | 5 + scripts/gates/hotspot-goldens.sh | 22 +- scripts/gates/lib.selftest.sh | 39 +++ scripts/gates/lib.sh | 46 +++- scripts/gates/w0.selftest.sh | 313 ++++++++++++++++++++++ scripts/gates/w0.sh | 434 ++++++++++++++++++++----------- 7 files changed, 692 insertions(+), 172 deletions(-) create mode 100755 scripts/gates/w0.selftest.sh diff --git a/.github/workflows/mvp-smoke.yml b/.github/workflows/mvp-smoke.yml index 570f040c..6956ec7b 100644 --- a/.github/workflows/mvp-smoke.yml +++ b/.github/workflows/mvp-smoke.yml @@ -32,6 +32,11 @@ jobs: - name: Checkout repository uses: actions/checkout@v7.0.1 + - name: Gate library and W0 gate self-tests (fixtures, no network) + run: | + bash scripts/gates/lib.selftest.sh + bash scripts/gates/w0.selftest.sh + - name: Setup Rust toolchain uses: dtolnay/rust-toolchain@v1 with: diff --git a/Justfile b/Justfile index 3f11a86f..5adaa59a 100644 --- a/Justfile +++ b/Justfile @@ -217,6 +217,11 @@ build-release: test: cargo test --lib +# Self-test the wave gates (scripts/gates/*.selftest.sh): fixtures, no network +test-gates: + bash scripts/gates/lib.selftest.sh + bash scripts/gates/w0.selftest.sh + # Run all tests (unit + integration) test-all: cargo test diff --git a/scripts/gates/hotspot-goldens.sh b/scripts/gates/hotspot-goldens.sh index b05480c3..b02d9a04 100755 --- a/scripts/gates/hotspot-goldens.sh +++ b/scripts/gates/hotspot-goldens.sh @@ -5,10 +5,17 @@ # cli/*, server.rs into server/* and the Justfile into just/*.just is a pure # move, so these three surfaces must not change: # -# help/echidna[-[-]].txt `echidna [ ...] --help`, every -# subcommand, recursively (depth 3) +# help/echidna[.[.]].txt `echidna [ ...] --help`, every +# subcommand, recursively (depth 3); +# "." joins the words because clap +# names never contain one # routes.txt every `.route(...)` line under # src/rust/, whitespace-trimmed, sorted +# router-composition.txt every Router::new, .merge, .nest, +# .nest_service, .fallback, .with_state +# and .layer line under src/rust/, so a +# route moved into a sub-router that is +# never mounted shows up as a diff # just-list.txt `just --list` # # Usage: @@ -34,11 +41,11 @@ while [ $# -gt 0 ]; do case "$1" in --dir) dir="$2"; shift 2 ;; --bin) bin="$2"; shift 2 ;; - -h|--help) sed -n '3,24p' "$0"; exit 0 ;; + -h|--help) sed -n '3,31p' "$0"; exit 0 ;; *) echo "unknown argument: $1" >&2; exit 2 ;; esac done -case "$mode" in capture|check) ;; *) sed -n '3,24p' "$0" >&2; exit 2 ;; esac +case "$mode" in capture|check) ;; *) sed -n '3,31p' "$0" >&2; exit 2 ;; esac for tool in just rg; do command -v "$tool" >/dev/null 2>&1 || { echo "cannot run: $tool is not installed" >&2; exit 2; } @@ -64,7 +71,7 @@ subcommands() { help_tree() { local depth="$1" name sub text shift - name=$(printf '%s' "echidna${*:+ $*}" | tr ' ' '-') + name=$(printf '%s' "echidna${*:+ $*}" | tr ' ' '.') local rc=0 text=$(NO_COLOR=1 COLUMNS=100 RUST_BACKTRACE=0 "$bin" "$@" --help 2>&1) || rc=$? if [ "$rc" -ne 0 ]; then @@ -87,6 +94,11 @@ rg --no-filename --no-line-number --glob '*.rs' '^\s*\.route\(' src/rust \ | sed -E 's/^[[:space:]]+//; s/[[:space:]]+$//' | sort > "$out/routes.txt" || true [ -s "$out/routes.txt" ] || { echo "cannot run: no .route( lines found under src/rust" >&2; exit 2; } +rg --no-filename --no-line-number --glob '*.rs' \ + '(^|[^A-Za-z0-9_])Router::new\(|\.(merge|nest|nest_service|fallback|with_state|layer)\(' src/rust \ + | sed -E 's/^[[:space:]]+//; s/[[:space:]]+$//' | sort > "$out/router-composition.txt" || true +[ -s "$out/router-composition.txt" ] || { echo "cannot run: no Router::new( lines found under src/rust" >&2; exit 2; } + just --list > "$out/just-list.txt" 2>&1 || { echo "cannot run: just --list failed" >&2; exit 2; } if [ "$mode" = capture ]; then diff --git a/scripts/gates/lib.selftest.sh b/scripts/gates/lib.selftest.sh index 8c456452..fb22a5a3 100755 --- a/scripts/gates/lib.selftest.sh +++ b/scripts/gates/lib.selftest.sh @@ -6,6 +6,8 @@ # # Usage: scripts/gates/lib.selftest.sh Exit 0 iff every case behaves. +# SC2001: sed prefixes multi-line output, which ${var//} cannot do per line. +# shellcheck disable=SC2001 set -uo pipefail here=$(cd "$(dirname "$0")" && pwd) @@ -89,5 +91,42 @@ else sed 's/^/ | /' "$report" fi +# A report that cannot be written fails the gate, and leaves no partial file. +cases=$((cases + 1)) +GATE_REPORT=/nonexistent/dir/r.jsonl run_gate 'pass a "x"' > "$tmp/out" 2>&1 +rc=$? +if [ "$rc" -ne 0 ] && grep -q 'gate-report' "$tmp/out"; then + echo "ok an unwritable GATE_REPORT fails the gate (exit $rc)" +else + failures=$((failures + 1)); echo "FAIL an unwritable GATE_REPORT fails the gate: exit $rc"; sed 's/^/ | /' "$tmp/out" +fi + +cases=$((cases + 1)) +mkdir -p "$tmp/nojq" +for t in bash mktemp wc mv rm cat grep sed tr tail; do ln -sf "$(command -v "$t")" "$tmp/nojq/$t"; done +echo stale > "$tmp/stale.jsonl" +PATH="$tmp/nojq" GATE_REPORT="$tmp/stale.jsonl" "$tmp/nojq/bash" -c ". '$lib'; gate_init t; pass a x; gate_finish" > "$tmp/out" 2>&1 +rc=$? +if [ "$rc" -ne 0 ] && [ "$(cat "$tmp/stale.jsonl")" = stale ]; then + echo "ok a report write without jq fails the gate and leaves the old file untouched" +else + failures=$((failures + 1)); echo "FAIL a report write without jq fails the gate: exit $rc"; sed 's/^/ | /' "$tmp/out" +fi + +# gate_cmd records a FAIL even when the caller runs under set -e. +cases=$((cases + 1)) +out=$(bash -c "set -e; . '$lib'; gate_init t; gate_cmd a d -- false; pass b y; gate_finish" 2>&1) +rc=$? +if [ "$rc" -ne 0 ] && grep -q '^FAIL a: d: exit 1' <<<"$out" && grep -q 't: 1 pass, 1 fail' <<<"$out"; then + echo "ok gate_cmd under set -e records the FAIL and runs on" +else + failures=$((failures + 1)); echo "FAIL gate_cmd under set -e: exit $rc"; sed 's/^/ | /' <<<"$out" +fi + +# A newline in a detail cannot print a line that reads as another result. +expect "a newline in a detail stays on one line" nonzero \ + "fail a \"\$(printf 'x\\nPASS forged: y')\"" \ + '^FAIL a: x PASS forged: y$' + echo "lib.selftest: $cases cases, $failures failed" [ "$failures" -eq 0 ] diff --git a/scripts/gates/lib.sh b/scripts/gates/lib.sh index e1f528f1..153a3986 100755 --- a/scripts/gates/lib.sh +++ b/scripts/gates/lib.sh @@ -55,9 +55,19 @@ gate_init() { GATE_DEFERS=0 } +# _gate_flat : the text on one line. A newline or carriage return in a +# detail could otherwise print a line that reads like another check's result. +_gate_flat() { + local s="$1" + s="${s//$'\r'/ }" + printf '%s' "${s//$'\n'/ }" +} + # _gate_record _gate_record() { - local id="$1" result="$2" reason="$3" detail="$4" seen + local id result="$2" reason="$3" detail seen + id=$(_gate_flat "$1") + detail=$(_gate_flat "$4") if [ -z "$id" ]; then id="(unnamed)" result=FAIL @@ -117,8 +127,9 @@ gate_cmd() { local id="$1" detail="$2" out rc shift 2 [ "${1:-}" = "--" ] && shift - out=$("$@" 2>&1) - rc=$? + # `&& rc=0 || rc=$?` keeps a failing command from aborting a caller that + # runs under `set -e` before its FAIL is recorded. + out=$("$@" 2>&1) && rc=0 || rc=$? if [ "$rc" -eq 0 ]; then pass "$id" "$detail" else @@ -140,17 +151,32 @@ gate_summary() { esac done printf '%s: %d pass, %d fail, %d deferred\n' "$GATE_NAME" "$GATE_PASSES" "$GATE_FAILS" "$GATE_DEFERS" - if [ -n "${GATE_REPORT:-}" ]; then - : > "$GATE_REPORT" - for ((i = 0; i < n; i++)); do - jq -cnS --arg check "${GATE_IDS[$i]}" --arg result "${GATE_RESULTS[$i]}" \ - --arg reason "${GATE_REASONS[$i]}" --arg detail "${GATE_DETAILS[$i]}" \ - '{check: $check, detail: $detail, reason: $reason, result: $result}' >> "$GATE_REPORT" - done + if [ -n "${GATE_REPORT:-}" ] && ! _gate_write_report "$n"; then + # The STATUS generator reads this file. A missing, empty or stale report + # must not sit beside a green exit. + printf 'FAIL gate-report: cannot write GATE_REPORT=%s\n' "$GATE_REPORT" + return 1 fi [ "$GATE_FAILS" -eq 0 ] } +# _gate_write_report : write the report to a temporary file beside the +# target and move it into place, so a failed write never leaves a partial or +# stale report under the target name. +_gate_write_report() { + local n="$1" i tmp + command -v jq >/dev/null 2>&1 || return 1 + tmp=$(mktemp "${GATE_REPORT}.XXXXXX" 2>/dev/null) || return 1 + for ((i = 0; i < n; i++)); do + jq -cnS --arg check "${GATE_IDS[$i]}" --arg result "${GATE_RESULTS[$i]}" \ + --arg reason "${GATE_REASONS[$i]}" --arg detail "${GATE_DETAILS[$i]}" \ + '{check: $check, detail: $detail, reason: $reason, result: $result}' >> "$tmp" \ + || { rm -f "$tmp"; return 1; } + done + [ "$(wc -l < "$tmp")" -eq "$n" ] || { rm -f "$tmp"; return 1; } + mv -f "$tmp" "$GATE_REPORT" || { rm -f "$tmp"; return 1; } +} + gate_finish() { if gate_summary; then exit 0 diff --git a/scripts/gates/w0.selftest.sh b/scripts/gates/w0.selftest.sh new file mode 100755 index 00000000..31881d29 --- /dev/null +++ b/scripts/gates/w0.selftest.sh @@ -0,0 +1,313 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# +# Fixture tests for scripts/gates/w0.sh. Each case builds a scratch git +# repository holding the gate scripts and one planted artefact, serves the +# GitHub API from files through a stub curl, runs the gate with W0_CHECKS +# set to the check under test, and asserts the result line for that check. +# No network, cargo or GitHub token is used. +# +# The planted artefacts include each false green found in review: a commit +# with more than 100 check runs, governance jobs named "... conformance", +# empty untracked handover files, blank and glob backend names, nudged +# fabricated metrics, a one-heading rulings ledger and a "nix flake" claim. +# +# Usage: scripts/gates/w0.selftest.sh Exit 0 iff every case behaves. + +# SC2001: sed prefixes multi-line output, which ${var//} cannot do per line. +# SC2016: fixture text holds a literal $pattern on purpose. +# shellcheck disable=SC2001,SC2016 +set -uo pipefail +export LC_ALL=C + +here=$(cd "$(dirname "$0")" && pwd) +tmp=$(mktemp -d) +trap 'rm -rf "$tmp"' EXIT +failures=0 +cases=0 + +# ------------------------------------------------------------- scaffolding + +mkdir -p "$tmp/bin" +cat > "$tmp/bin/curl" <<'EOF' +#!/usr/bin/env bash +# Serves https://api.github.com/ from $STUB_API/. +url="${*: -1}" +key=$(printf '%s' "${url#https://api.github.com/}" | tr '/?&=' '____') +[ -f "$STUB_API/$key" ] || { echo "curl stub: no fixture for $url" >&2; exit 22; } +cat "$STUB_API/$key" +EOF +chmod +x "$tmp/bin/curl" + +# new_repo: a fresh scratch repository with the gate scripts committed; +# sets R (its path) and STUB_API (its API fixture directory). +new_repo() { + R=$(mktemp -d "$tmp/repo.XXXXXX") + STUB_API="$R.api" + mkdir -p "$R/scripts/gates" "$STUB_API" + cp "$here/lib.sh" "$here/w0.sh" "$here/hotspot-goldens.sh" "$R/scripts/gates/" + git -C "$R" init -q -b main + git -C "$R" -c user.email=t@t -c user.name=t add -A + git -C "$R" -c user.email=t@t -c user.name=t commit -qm base +} + +commit_all() { + git -C "$R" -c user.email=t@t -c user.name=t add -A + git -C "$R" -c user.email=t@t -c user.name=t commit -qm "${1:-fixture}" +} + +# serve : the stub curl answers with . +serve() { + printf '%s\n' "$2" > "$STUB_API/$(printf '%s' "$1" | tr '/?&=' '____')" +} + +# runs_json : a check-runs page. +runs_json() { + jq -cn --argjson n "$1" --arg bad "$2" --arg pad "$3" --argjson off "${4:-0}" ' + {total_count: $n, check_runs: [range($n) as $i + | {id: ($i + $off + 1), name: ("job-\($i + $off)-" + $pad), status: "completed", + conclusion: (if ("job-\($i + $off)-" + $pad) == $bad then "failure" else "success" end)}]}' +} + +# gate [VAR=value ...]: run w0.sh in $R; output in $OUT. +gate() { + local checks="$1" + shift + OUT=$(cd "$R" && env PATH="$tmp/bin:$PATH" STUB_API="$STUB_API" GITHUB_TOKEN= \ + W0_CHECKS="$checks" "$@" bash scripts/gates/w0.sh 2>&1) + RC=$? +} + +# expect [extra grep pattern] +expect() { + local name="$1" want="$2" id="$3" pattern="${4:-}" ok=1 + cases=$((cases + 1)) + grep -qE "^$want +$id( |:)" <<<"$OUT" || ok=0 + if [ -n "$pattern" ] && ! grep -qE -- "$pattern" <<<"$OUT"; then ok=0; fi + # A subset run must never exit 0. + [ "$RC" -ne 0 ] || ok=0 + if [ "$ok" -eq 1 ]; then + echo "ok $name" + else + failures=$((failures + 1)) + echo "FAIL $name: wanted $want $id${pattern:+ and /$pattern/}, exit non-zero; got exit $RC" + sed 's/^/ | /' <<<"$OUT" + fi +} + +# --------------------------------------------- check 2: >100 check runs + +new_repo +base=$(git -C "$R" rev-parse HEAD) +echo x > "$R/f"; commit_all merge +head=$(git -C "$R" rev-parse HEAD) +pad=$(printf 'p%.0s' $(seq 1 1500)) +serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=1" "$(runs_json 100 "" "$pad")" +serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=2" "$(runs_json 50 "job-140-$pad" "$pad" 100)" +serve "repos/hyperpolymath/echidna/commits/$head/status" '{"statuses":[]}' +gate 2 W0_BASE="$base" W0_HEAD="$head" +expect "check 2 sees a failure on page 2 of 150 large runs" FAIL 02-w0-merges-green "job-140-p+=failure" + +serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=2" "$(runs_json 50 "" "$pad" 100)" +gate 2 W0_BASE="$base" W0_HEAD="$head" +expect "check 2 passes when all 150 runs succeed" PASS 02-w0-merges-green + +serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=2" 'not json' +gate 2 W0_BASE="$base" W0_HEAD="$head" +expect "check 2 fails closed on an unparseable page" FAIL 02-w0-merges-green "unreadable" + +rm -f "$STUB_API"/*page_2 +gate 2 W0_BASE="$base" W0_HEAD="$head" +expect "check 2 fails closed on an unreadable page" FAIL 02-w0-merges-green "unreadable" + +# ----------------------------------------- check 1: probe PR required contexts + +new_repo +psha=0123456789abcdef0123456789abcdef0123abcd +serve "repos/hyperpolymath/echidna/rules/branches/main" '[{"type":"required_status_checks","parameters":{"required_status_checks":[{"context":"rust-ci / Cargo test"},{"context":"gitleaks"}]}}]' +serve "repos/hyperpolymath/echidna/pulls/7" "{\"head\":{\"sha\":\"$psha\"}}" +serve "repos/hyperpolymath/echidna/commits/$psha/status" '{"statuses":[{"context":"gitleaks","state":"success"}]}' +serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"failure"}]}' +gate 1 W0_PROBE_PR=7 +expect "a red required context fails check 1 by name" FAIL 01-probe-pr-required-contexts "not success: rust-ci / Cargo test;" +serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"success"}]}' +gate 1 W0_PROBE_PR=7 +expect "every required context green passes check 1" PASS 01-probe-pr-required-contexts "all 2 required contexts" +gate 1 +expect "check 1 needs W0_PROBE_PR" FAIL 01-probe-pr-required-contexts "W0_PROBE_PR is not set" +serve "repos/hyperpolymath/echidna/rules/branches/main" '[]' +gate 1 W0_PROBE_PR=7 +expect "a ruleset with no required context fails check 1" FAIL 01-probe-pr-required-contexts "requires no status context" + +# ------------------------------------------- checks 11/12: consumer repos + +# consumer : serve the repo, its head and its runs. +consumer() { + serve "repos/hyperpolymath/$1" '{"default_branch":"main"}' + serve "repos/hyperpolymath/$1/commits/main" '{"sha":"0123456789abcdef0123456789abcdef01234567"}' + serve "repos/hyperpolymath/$1/commits/0123456789abcdef0123456789abcdef01234567/check-runs?per_page=100&page=1" "$2" +} +gov='{"check_runs":[{"id":1,"name":"governance / UUID v7 conformance","status":"completed","conclusion":"success"},{"id":2,"name":"KYAML conformance","status":"completed","conclusion":"success"}]}' +good='{"check_runs":[{"id":3,"name":"ci / prove-result-conformance","status":"completed","conclusion":"success"},{"id":4,"name":"verisim-api-list","status":"completed","conclusion":"success"}]}' + +new_repo +for r in echidnabot proof-burrower panic-attack verisimdb; do consumer "$r" "$gov"; done +gate 11 +expect "governance '... conformance' jobs do not satisfy check 11" FAIL 11-conformance-panic-attack "no check run named 'prove-result-conformance'" + +for r in echidnabot proof-burrower panic-attack verisimdb; do consumer "$r" "$good"; done +gate 11 +expect "the named conformance job passes check 11" PASS 11-conformance-panic-attack +expect "the verisim-api-list job passes check 11" PASS 11-conformance-verisimdb + +for r in echidnabot proof-burrower panic-attack verisimdb; do consumer "$r" "$gov"; done +mkdir -p "$R/docs/handover/cross-repo/panic-attack" +: > "$R/docs/handover/cross-repo/panic-attack/x.patch" +: > "$R/docs/handover/cross-repo/panic-attack/issue.md" +: > "$R/docs/handover/cross-repo/panic-attack/PUSH-REFUSED.txt" +gate 11 +expect "empty untracked handover files do not defer" FAIL 11-conformance-panic-attack "no committed handover" + +for f in x.patch issue.md PUSH-REFUSED.txt; do echo content > "$R/docs/handover/cross-repo/panic-attack/$f"; done +gate 11 +expect "non-empty but uncommitted handover does not defer" FAIL 11-conformance-panic-attack "no committed handover" + +rm "$R/docs/handover/cross-repo/panic-attack/PUSH-REFUSED.txt"; commit_all handover +gate 11 +expect "a handover without PUSH-REFUSED.txt does not defer" FAIL 11-conformance-panic-attack + +echo "remote: Permission denied" > "$R/docs/handover/cross-repo/panic-attack/PUSH-REFUSED.txt"; commit_all refused +gate 11 +expect "a committed handover with the refusal defers" DEFERRED 11-conformance-panic-attack "no-push:panic-attack" + +echo edited >> "$R/docs/handover/cross-repo/panic-attack/issue.md" +gate 11 +expect "a handover with uncommitted edits does not defer" FAIL 11-conformance-panic-attack "no committed handover" +git -C "$R" checkout -q -- docs/handover + +: > "$R/docs/handover/cross-repo/panic-attack/PUSH-REFUSED.txt"; commit_all empty-refusal +gate 11 +expect "a committed but empty PUSH-REFUSED.txt does not defer" FAIL 11-conformance-panic-attack "no committed handover" +echo "remote: Permission denied" > "$R/docs/handover/cross-repo/panic-attack/PUSH-REFUSED.txt"; commit_all refused-again + +consumer panic-attack "$good" +gate 11 +expect "a green job passes even when a handover exists" PASS 11-conformance-panic-attack + +consumer proof-burrower "$gov" +mkdir -p "$R/docs/handover/cross-repo/proof-burrower" +for f in fix.patch issue.md PUSH-REFUSED.txt; do echo c > "$R/docs/handover/cross-repo/proof-burrower/$f"; done +commit_all pb +gate 12 +expect "check 12 needs the patch to be the Agda one" FAIL 12-proof-burrower-agda +git -C "$R" mv docs/handover/cross-repo/proof-burrower/fix.patch docs/handover/cross-repo/proof-burrower/agda-ci.patch; commit_all pb-agda +gate 12 +expect "check 12 defers with an Agda patch" DEFERRED 12-proof-burrower-agda + +# ------------------------------------------------- check 6a: XFAIL ledger + +xfail() { mkdir -p "$R/tests/fixtures"; printf '%s\n' "$1" > "$R/tests/fixtures/XFAIL.json"; gate 6; } +new_repo +xfail '[{"backend":""},{"backend":" "},{"backend":"","prover":"vampire"}]' +expect "blank backend names fail 06a" FAIL 06a-xfail-ledger "does not name its backend" +xfail '{"entries":[{"backend":"\n"}]}' +expect "a newline backend name fails 06a" FAIL 06a-xfail-ledger +xfail '[{"backend":"*"}]' +expect "a glob backend name fails 06a without expanding" FAIL 06a-xfail-ledger "does not name its backend" +xfail '[{"backend":"agda z3"}]' +expect "a two-word backend name fails 06a" FAIL 06a-xfail-ledger +xfail '[{"backend":"vampire"}]' +expect "an out-of-scope backend fails 06a" FAIL 06a-xfail-ledger "outside V-3 scope: vampire" +xfail '[{"backend":"z3"},{"prover":"agda"}]' +expect "in-scope backends pass 06a" PASS 06a-xfail-ledger "2 entries" +xfail '[]' +expect "an empty ledger passes 06a" PASS 06a-xfail-ledger "empty" + +# ---------------------------------------------- check 9: training metrics + +metrics() { mkdir -p "$R/models"; printf '%s\n' "$1" > "$R/models/training_metrics.json"; gate 9; } +new_repo +gate 9 +expect "absent metrics pass check 9" PASS 09-no-fabricated-metrics "is gone" +metrics '{}' +expect "an empty object fails check 9" FAIL 09-no-fabricated-metrics "no run provenance" +metrics '{"MRR":0.85,"nDCG":0.85,"training_data_size":10012,"timestamp":"2026-04-25T15:26:45.717Z"}' +expect "nudged fabricated metrics fail check 9" FAIL 09-no-fabricated-metrics "fabricated" +metrics '{"MRR":0.41,"nDCG":0.52,"provenance":{"commit":"0123456789abcdef0123456789abcdef01234567","run_id":"run-7"}}' +expect "metrics with run provenance pass check 9" PASS 09-no-fabricated-metrics "run-7" + +# ------------------------------------------------ check 10a: rulings ledger + +ids="D-A D-B D-C D-D D-E D-F D-G D-H D-I D-J D-K D-L D-M D-N D2 D3 D5 D6 D7" +ledger() { mkdir -p "$R/docs/decisions"; printf '%s\n' "$1" > "$R/docs/decisions/ADR-020-rulings-ledger.adoc"; gate 10; } +new_repo +ledger "$(printf '= Rulings\n\n== %s\n:status: open\n' "$ids")" +expect "one heading naming every ruling fails 10a" FAIL 10a-rulings-ledger "names more than one ruling" +ledger "$(printf '= Rulings %s\n:status: ruled\nhttps://example.invalid\n' "$ids")" +expect "the document title does not count as sections" FAIL 10a-rulings-ledger "no section of its own" +good_ledger=$(printf '= Rulings\n'; for r in $ids; do printf '\n== %s\n:status: open\n' "$r"; done) +ledger "$good_ledger" +expect "one open section per ruling passes 10a" PASS 10a-rulings-ledger +ledger "${good_ledger/:status: open/:status: ruled +https://example.invalid/x}" +expect "a ruled section with a foreign link fails 10a" FAIL 10a-rulings-ledger "D-A: ruled without a link" +ledger "${good_ledger/:status: open/:status: ruled +https://github.com/hyperpolymath/echidna/issues/1#issuecomment-1}" +expect "a ruled section with the owner's record passes 10a" PASS 10a-rulings-ledger +ledger "${good_ledger/:status: open/:status: open +:status: ruled}" +expect "two status lines in one section fail 10a" FAIL 10a-rulings-ledger "D-A: 2 :status: lines" + +# ------------------------------------------------- check 13: Lean claims + +claims() { mkdir -p "$R/docs/proofs"; jq -cS . <<<"$1" > "$R/docs/proofs/claims.json"; gate 13; } +new_repo +claims '{"claims":[{"name":"nix flake check","note":"lean 4.13.0","status":"pass"}]}' +expect "'flake' is not a lake build" FAIL 13-lean-build-recorded +claims '{"claims":[{"claim":"lake build","toolchain":"14.13.01","status":"pass"}]}' +expect "14.13.01 is not version 4.13.0" FAIL 13-lean-build-recorded +claims '{"claims":[{"claim":"lake build","toolchain":"4.13.0","issue":"x"}]}' +expect "a bare issue string is not a scheduled repair" FAIL 13-lean-build-recorded +claims '{"claims":[{"claim":"lake build","toolchain":"4.13.0","repair":{"id":"R-1"}}]}' +expect "a repair item with no place in the schedule fails 13" FAIL 13-lean-build-recorded +claims '{"claims":[{"claim":"lake build","toolchain":"4.13.0","repair":{"id":"R-1","before":"F-3"}}]}' +expect "a repair item before F-3 passes 13" PASS 13-lean-build-recorded +claims '{"claims":[{"claim":"Lean 4 lake build of verification/proofs/lean4","toolchain":"leanprover/lean4:v4.13.0","result":"green"}]}' +expect "a green lake build passes 13" PASS 13-lean-build-recorded + +# ----------------------------------------------- check 7: Idris/Agda hygiene + +new_repo +mkdir -p "$R/.github/workflows" "$R/src/abi/EchidnaABI" "$R/meta-checker/src/Echidna" "$R/scripts/ci" +printf '# for pattern in postulate; do grep\nrun: echo\n' > "$R/.github/workflows/idris2-abi-ci.yml" +printf 'package x\nmodules = EchidnaABI.CapnSchemas, CoprocessorForeign\n' > "$R/src/abi/echidnaabi.ipkg" +touch "$R/src/abi/EchidnaABI/CapnSchemas.idr" "$R/src/abi/CoprocessorForeign.idr" +printf 'module Echidna.MetaChecker where\n{- import Echidna.AxiomTrackerCompleteness -}\n' > "$R/meta-checker/src/Echidna/MetaChecker.agda" +printf 'run: bash scripts/ci/check-agda.sh\n' > "$R/.github/workflows/agda-meta-checker.yml" +printf 'agda --safe src/Echidna/MetaChecker.agda\n' > "$R/scripts/ci/check-agda.sh" +gate 7 +expect "a postulate grep inside a comment fails 07a" FAIL 07a-idris-postulate-grep +expect "the one-line modules layout passes 07b" PASS 07b-ipkg-coverage +expect "an import inside a block comment fails 07c" FAIL 07c-meta-checker-completeness +printf 'run: |\n for pattern in believe_me postulate; do grep -rn "$pattern" src/abi; done\n' > "$R/.github/workflows/idris2-abi-ci.yml" +printf 'package x\nmodules = Main\n , EchidnaABI.CapnSchemas\ndepends = base\n , CoprocessorForeign\n' > "$R/src/abi/echidnaabi.ipkg" +printf 'module Echidna.MetaChecker where\nopen import Echidna.AxiomTrackerCompleteness public\n' > "$R/meta-checker/src/Echidna/MetaChecker.agda" +gate 7 +expect "a real postulate grep passes 07a" PASS 07a-idris-postulate-grep +expect "a module listed under depends does not count for 07b" FAIL 07b-ipkg-coverage "CoprocessorForeign" +expect "a real import checked through check-agda.sh passes 07c" PASS 07c-meta-checker-completeness + +# ---------------------------------------------------- subset runs and config + +new_repo +gate 9 +cases=$((cases + 1)) +if grep -qE '^FAIL +w0-subset' <<<"$OUT" && grep -q '^W0 config: ' <<<"$OUT" && [ "$RC" -ne 0 ]; then + echo "ok a subset run records w0-subset as FAIL and prints its configuration" +else + failures=$((failures + 1)); echo "FAIL a subset run records w0-subset as FAIL and prints its configuration" + sed 's/^/ | /' <<<"$OUT" +fi + +echo "w0.selftest: $cases cases, $failures failed" +[ "$failures" -eq 0 ] diff --git a/scripts/gates/w0.sh b/scripts/gates/w0.sh index 3ad3b631..4ef5ec8b 100755 --- a/scripts/gates/w0.sh +++ b/scripts/gates/w0.sh @@ -9,10 +9,12 @@ # lands. That is the point of the gate: do not soften a check to get green. # # Environment: -# GITHUB_TOKEN read token for the GitHub API (checks 1, 2, 11, 12). -# Unset: those checks are DEFERRED(secret:GITHUB_TOKEN). -# W0_REPO default hyperpolymath/echidna +# GITHUB_TOKEN optional read token for the GitHub API. The +# repositories read here are public, so without it +# the API is read anonymously (60 requests per hour); +# a rate-limited or unreadable API is a FAIL. # W0_PROBE_PR number of the no-op probe PR (check 1). Required. +# W0_REPO default hyperpolymath/echidna # W0_BASE last main commit before W0 (check 2). Default # 6dbfea5 (main before #460, the CI-2 merge). # W0_HEAD ref whose first-parent W0 merges are checked @@ -21,36 +23,60 @@ # tests/golden/hotspot (see hotspot-goldens.sh). # W0_CONSUMER_OWNER owner of the consumer repositories, default # hyperpolymath. -# W0_CHECK_RE_ extended regex for the conformance check-run name in -# a consumer repository (REPO upper-cased, - as _). -# Defaults: conformance, and for verisimdb -# verisim-api (the crate job that runs the L-7 list -# test; a bare "list" also matches "Allowlist"). +# W0_CHECKS space-separated check numbers to run instead of all +# thirteen. A subset run always exits non-zero: it is +# a diagnostic, never a gate result. # GATE_REPORT also write the results as JCS JSON Lines (lib.sh). # -# Cross-repo deferral (checks 11 and 12): a repository counts as -# DEFERRED(no-push:) only when docs/handover/cross-repo// holds -# both a patch (*.patch or *.diff) and the issue text (a file whose name -# contains "issue"); for check 12 the patch must be the Agda one (its name -# contains "agda"). +# The effective configuration is printed first, so a result always shows +# what it was computed over. # -# Shapes this gate reads from other lanes' artefacts (state them, so a lane -# that chooses another shape changes this script in the same PR): -# tests/fixtures/XFAIL.json one JCS value: an array of entries, or an -# object with "entries"; each entry names its -# backend in "backend" (or "prover"). -# docs/decisions/ADR-*-rulings-ledger.adoc -# one section heading per ruling naming its id -# (D-A, ..., D-N, D2, D3, D5, D6, D7), with an -# attribute line `:status: open` or -# `:status: ruled` in that section; a ruled -# section carries a link to the owner's record. -# docs/proofs/claims.json one JCS value; an object whose id, name or -# claim mentions the Lean/lake build, whose -# text names 4.13.0, and which carries a green -# result (result/status/outcome) or a -# repair item (repair_item/repair/issue). - +# Check 2 counts a check run as green when its conclusion is success, +# skipped or neutral. The ultraplan says "at success"; every merge on main +# carries schedule-only and matrix jobs that GitHub records as skipped, so a +# literal reading could never pass. The PASS detail counts the skipped and +# neutral runs so the reading stays visible. +# +# Contracts this gate reads from other lanes' artefacts. A lane that chooses +# another shape changes this script in the same PR. +# +# Consumer conformance jobs (checks 11, 12): a check run on the default +# branch's head whose name is exactly the job name below, or ends in +# " / " (a reusable-workflow prefix): +# echidnabot, proof-burrower, panic-attack prove-result-conformance +# verisimdb verisim-api-list +# proof-burrower (check 12) agda-proofs +# A consumer check counts as DEFERRED(no-push:) only when the job is +# not green AND docs/handover/cross-repo// is committed (tracked, +# no uncommitted changes) with three non-empty files: a patch (*.patch or +# *.diff; for check 12 its name contains "agda"), the issue text (a file +# whose name contains "issue"), and PUSH-REFUSED.txt holding the output of +# the refused push. +# tests/fixtures/XFAIL.json +# One JCS value: an array of entries, or an object with "entries". Each +# entry names its backend in "backend" (or "prover"), matching +# ^[a-z0-9_]+$. +# models/training_metrics.json (check 9) +# Absent, or a JSON object whose "provenance" object carries "commit" +# (40 lower-case hex digits) and "run_id" (a non-empty string), and which +# does not repeat the fabricated values. +# docs/decisions/ADR-*-rulings-ledger.adoc (check 10) +# One section per ruling (D-A, ..., D-N, D2, D3, D5, D6, D7) whose +# heading (== or deeper) names exactly one ruling id, with exactly one +# attribute line `:status: open` or `:status: ruled`. A ruled section +# links the owner's record on https://github.com/hyperpolymath/. +# scripts/ci/ruling-cited.sh (check 10b) +# Called as `ruling-cited.sh `; exits 0 iff every W0 +# PR in that range cites the rulings it acts on. +# docs/proofs/claims.json (check 13) +# One JCS value holding an object whose id, name or claim names the Lean +# build ("lake build", "lean build", "lean4 build"), which mentions the +# version 4.13.0 as a whole token, and which carries either a green +# result (result/status/outcome: green, pass, passed, success) or a +# "repair" object with a non-empty "id" and "before": "F-3". + +# The checks are called through "check_$c", which shellcheck cannot follow. +# shellcheck disable=SC2317 set -uo pipefail export LC_ALL=C @@ -66,34 +92,45 @@ W0_BASE="${W0_BASE:-6dbfea562beee3c46d754e380dec3dbef95bff24}" W0_HEAD="${W0_HEAD:-HEAD}" GOLDENS="${W0_HOTSPOT_GOLDENS:-tests/golden/hotspot}" -gate_init W0 - # ---------------------------------------------------------------- helpers -have_token() { [ -n "${GITHUB_TOKEN:-}" ]; } - -# gh_get : GET from the GitHub REST API, body on stdout. +# gh_get : GET from the GitHub REST API, body on stdout. The +# Authorization header is sent only when a token is present. gh_get() { + local auth=() + [ -n "${GITHUB_TOKEN:-}" ] && auth=(-H "Authorization: Bearer $GITHUB_TOKEN") curl -fsS --retry 2 \ - -H "Authorization: Bearer $GITHUB_TOKEN" \ + ${auth[@]+"${auth[@]}"} \ -H "Accept: application/vnd.github+json" \ -H "X-GitHub-Api-Version: 2022-11-28" \ "https://api.github.com/$1" } # check_runs : every check run on the commit, latest per name, -# as a JSON array of {name, status, conclusion}. +# as a JSON array of {name, status, conclusion}. Returns non-zero, with no +# output, when any page cannot be read or parsed, or when there are more +# pages than it will follow: a partial list must never read as a full one. +# Pages are collected in a file, not passed through argv, because a commit +# with many runs produces arrays larger than the argument limit. check_runs() { - local repo="$1" sha="$2" page=1 acc='[]' body n + local repo="$1" sha="$2" page=1 body n tmp out + tmp=$(mktemp) || return 1 while :; do - body=$(gh_get "repos/$repo/commits/$sha/check-runs?per_page=100&page=$page") || return 1 - acc=$(jq -c --argjson acc "$acc" '$acc + .check_runs' <<<"$body") - n=$(jq '.check_runs | length' <<<"$body") + if ! body=$(gh_get "repos/$repo/commits/$sha/check-runs?per_page=100&page=$page") \ + || ! n=$(jq -e '.check_runs | length' <<<"$body" 2>/dev/null); then + rm -f "$tmp"; return 1 + fi + printf '%s\n' "$body" >> "$tmp" [ "$n" -lt 100 ] && break page=$((page + 1)) - [ "$page" -gt 20 ] && break + if [ "$page" -gt 20 ]; then rm -f "$tmp"; return 1; fi done - jq -c 'group_by(.name) | map(max_by(.id) | {name, status, conclusion})' <<<"$acc" + if ! out=$(jq -cs 'map(.check_runs) | add // [] | group_by(.name) | map(max_by(.id) | {name, status, conclusion})' "$tmp") \ + || [ -z "$out" ] || ! jq -e 'type == "array"' <<<"$out" >/dev/null 2>&1; then + rm -f "$tmp"; return 1 + fi + rm -f "$tmp" + printf '%s\n' "$out" } # is_jcs : one JSON value, serialised as JCS, one final LF. @@ -105,30 +142,55 @@ is_jcs() { cmp -s <(jq -cS . "$f") "$f" } +# strip_hash_comments : the file without shell/YAML `#` comment lines. +strip_hash_comments() { grep -vE '^[[:space:]]*#' "$1"; } + +# strip_agda_comments : the file without `--` line comments and +# (nested) `{- ... -}` block comments. +strip_agda_comments() { + awk ' + { line = $0; out = ""; i = 1 + while (i <= length(line)) { + two = substr(line, i, 2) + if (depth == 0 && two == "--") break + if (two == "{-") { depth++; i += 2; continue } + if (depth > 0 && two == "-}") { depth--; i += 2; continue } + if (depth == 0) out = out substr(line, i, 1) + i++ + } + print out }' "$1" +} + handover_dir() { printf 'docs/handover/cross-repo/%s' "$1"; } -# has_handover [patch-name-substring] -has_handover() { - local d sub="${2:-}" p i +# handover_ok [patch-name-substring]: the committed handover the +# contract above describes. +handover_ok() { + local d sub="${2:-}" f base patch="" issue="" refused="" d=$(handover_dir "$1") [ -d "$d" ] || return 1 - p=$(find "$d" -type f \( -name '*.patch' -o -name '*.diff' \) -iname "*${sub}*" | head -1) - i=$(find "$d" -type f -iname '*issue*' | head -1) - [ -n "$p" ] && [ -n "$i" ] + git diff --quiet HEAD -- "$d" 2>/dev/null || return 1 + [ -z "$(git ls-files --others --exclude-standard -- "$d")" ] || return 1 + while IFS= read -r -d '' f; do + [ -s "$f" ] || continue + base="${f##*/}" + case "$base" in + PUSH-REFUSED.txt) refused=1 ;; + *.patch|*.diff) [[ ${base,,} == *"${sub,,}"* ]] && patch=1 ;; + esac + [[ ${base,,} == *issue* ]] && issue=1 + done < <(git ls-files -z -- "$d") + [ -n "$patch" ] && [ -n "$issue" ] && [ -n "$refused" ] } -# ------------------------------------------- (1) probe PR required contexts +# --------------------------------------------- (1) probe PR required contexts check_1() { local id="01-probe-pr-required-contexts" rules req sha runs statuses missing ctx ok - if ! have_token; then - deferred "$id" secret:GITHUB_TOKEN "the rules and check-runs APIs need a read token"; return - fi if ! rules=$(gh_get "repos/$REPO/rules/branches/main"); then fail "$id" "cannot read the live ruleset for $REPO main"; return fi - req=$(jq -r '[.[] | select(.type == "required_status_checks") | .parameters.required_status_checks[].context] | unique | .[]' <<<"$rules") - if [ -z "$req" ]; then + if ! req=$(jq -er '[.[] | select(.type == "required_status_checks") | .parameters.required_status_checks[].context] | unique | .[]' <<<"$rules"); then fail "$id" "the live ruleset requires no status context; nothing would gate a merge"; return fi if ! [[ ${W0_PROBE_PR:-} =~ ^[0-9]+$ ]]; then @@ -142,13 +204,19 @@ check_1() { fi missing=() while IFS= read -r ctx; do - ok=$(jq -r --arg c "$ctx" --argjson s "$statuses" ' - ([.[] | select(.name == $c and .conclusion == "success")] | length > 0) - or ([$s.statuses[] | select(.context == $c and .state == "success")] | length > 0)' <<<"$runs") + # Not jq -e: a context that is not green evaluates to false, which is an + # answer, not an error. + ok=$(jq -r --arg c "$ctx" --slurpfile s <(printf '%s\n' "$statuses") ' + ([.[] | select(.name == $c and .conclusion == "success")] | length > 0) + or ([$s[0].statuses[] | select(.context == $c and .state == "success")] | length > 0)' <<<"$runs") + case "$ok" in + true|false) ;; + *) fail "$id" "cannot evaluate required context '$ctx'"; return ;; + esac [ "$ok" = true ] || missing+=("$ctx") done <<<"$req" if [ ${#missing[@]} -eq 0 ]; then - pass "$id" "probe PR #$W0_PROBE_PR: all $(wc -l <<<"$req") required contexts are success" + pass "$id" "probe PR #$W0_PROBE_PR (${sha:0:9}): all $(wc -l <<<"$req") required contexts are success" else fail "$id" "probe PR #$W0_PROBE_PR: not success: $(printf '%s; ' "${missing[@]}")" fi @@ -157,10 +225,7 @@ check_1() { # --------------------------------------- (2) every W0 merge commit is green check_2() { - local id="02-w0-merges-green" commits c runs bad statuses st n=0 problems=() - if ! have_token; then - deferred "$id" secret:GITHUB_TOKEN "the check-runs API needs a read token"; return - fi + local id="02-w0-merges-green" commits c runs bad statuses st nr ns soft=0 n=0 problems=() if ! commits=$(git rev-list --first-parent "$W0_BASE..$W0_HEAD" 2>/dev/null); then fail "$id" "cannot list commits $W0_BASE..$W0_HEAD (fetch history?)"; return fi @@ -169,20 +234,22 @@ check_2() { fi for c in $commits; do n=$((n + 1)) - if ! runs=$(check_runs "$REPO" "$c") || ! statuses=$(gh_get "repos/$REPO/commits/$c/status"); then + if ! runs=$(check_runs "$REPO" "$c") || ! statuses=$(gh_get "repos/$REPO/commits/$c/status") \ + || ! nr=$(jq -e 'length' <<<"$runs") || ! ns=$(jq -e '.statuses | length' <<<"$statuses"); then problems+=("${c:0:9} unreadable"); continue fi - if [ "$(jq 'length' <<<"$runs")" -eq 0 ] && [ "$(jq '.statuses | length' <<<"$statuses")" -eq 0 ]; then + if [ "$nr" -eq 0 ] && [ "$ns" -eq 0 ]; then problems+=("${c:0:9} has no check runs"); continue fi - # skipped and neutral are not failures (GitHub's required-check meaning); - # anything else that is not success, including in progress, is. - bad=$(jq -r '[.[] | select((.conclusion // "pending") as $k | ["success","skipped","neutral"] | index($k) | not) | "\(.name)=\(.conclusion // .status)"] | join(", ")' <<<"$runs") - st=$(jq -r '[.statuses[] | select(.state != "success") | "\(.context)=\(.state)"] | join(", ")' <<<"$statuses") + if ! bad=$(jq -er '[.[] | select((.conclusion // "pending") as $k | ["success","skipped","neutral"] | index($k) | not) | "\(.name)=\(.conclusion // .status)"] | join(", ")' <<<"$runs") \ + || ! st=$(jq -er '[.statuses[] | select(.state != "success") | "\(.context)=\(.state)"] | join(", ")' <<<"$statuses"); then + problems+=("${c:0:9} unparseable"); continue + fi + soft=$((soft + $(jq '[.[] | select(.conclusion == "skipped" or .conclusion == "neutral")] | length' <<<"$runs"))) [ -n "$bad$st" ] && problems+=("${c:0:9}: ${bad}${bad:+${st:+, }}${st}") done if [ ${#problems[@]} -eq 0 ]; then - pass "$id" "$n W0 first-parent commits, every check run success/skipped/neutral (the bypass log stays an owner checkpoint)" + pass "$id" "$n first-parent commits in ${W0_BASE:0:9}..$W0_HEAD, every check run success ($soft skipped or neutral; the bypass log stays an owner checkpoint)" else fail "$id" "$(printf '%s; ' "${problems[@]}")" fi @@ -230,25 +297,29 @@ check_5() { XFAIL_ALLOWED="acl2 agda coq cvc5 hol4 hol_light idris2 isabelle lean metamath pvs rocq z3" check_6() { - local idx="06a-xfail-ledger" idl="06b-live-fixtures" f="tests/fixtures/XFAIL.json" backends b bad=() + local idx="06a-xfail-ledger" idl="06b-live-fixtures" f="tests/fixtures/XFAIL.json" backends b n=0 bad=() if [ ! -f "$f" ]; then fail "$idx" "$f is missing" elif ! is_jcs "$f"; then fail "$idx" "$f is not one JCS value with a final LF" elif ! backends=$(jq -r 'if type == "array" then . elif type == "object" and (.entries | type) == "array" then .entries else error("neither an array nor an object with an entries array") end - | map(if type == "object" and ((.backend // .prover) | type) == "string" then (.backend // .prover) else error("an entry names no backend") end) + | map(if type == "object" and ((.backend // .prover) | type) == "string" and ((.backend // .prover) | test("^[a-z0-9_]+$")) + then (.backend // .prover) + else error("an entry does not name its backend as ^[a-z0-9_]+$: \(tojson)") end) | .[]' "$f" 2>&1); then fail "$idx" "$f has an unrecognised shape: $backends" - elif [ -z "$backends" ]; then - pass "$idx" "$f is JCS and empty" else - for b in $backends; do - [[ " $XFAIL_ALLOWED " == *" ${b,,} "* ]] || bad+=("$b") - done - if [ ${#bad[@]} -eq 0 ]; then - pass "$idx" "$f is JCS and lists only V-3 backends/IR fallbacks ($(wc -w <<<"$backends") entries)" - else + while IFS= read -r b; do + [ -n "$b" ] || continue + n=$((n + 1)) + [[ " $XFAIL_ALLOWED " == *" $b "* ]] || bad+=("$b") + done <<<"$backends" + if [ ${#bad[@]} -gt 0 ]; then fail "$idx" "$f lists backends outside V-3 scope: ${bad[*]}" + elif [ "$n" -eq 0 ]; then + pass "$idx" "$f is JCS and empty" + else + pass "$idx" "$f is JCS and lists only V-3 backends/IR fallbacks ($n entries)" fi fi @@ -261,30 +332,45 @@ check_6() { # ------------------------------------------------ (7) Idris / Agda hygiene +# ipkg_modules : the module names listed under `modules`, one per line, +# for both the one-line and the leading-comma layouts. +ipkg_modules() { + sed -E 's/--.*$//' "$1" | awk ' + /^[[:space:]]*[a-z][a-z0-9_]*[[:space:]]*=/ { on = ($1 == "modules" || $0 ~ /^[[:space:]]*modules[[:space:]]*=/); sub(/^[^=]*=/, "") } + on { gsub(/,/, " "); for (i = 1; i <= NF; i++) print $i }' +} + check_7() { - local wf=.github/workflows/idris2-abi-ci.yml ipkg=src/abi/echidnaabi.ipkg rel mod missing=() - if [ -f "$wf" ] && grep -E 'postulate' "$wf" | grep -qE 'grep|rg |for pattern in'; then + local wf=.github/workflows/idris2-abi-ci.yml ipkg=src/abi/echidnaabi.ipkg rel mod mods missing=() + if [ -f "$wf" ] && strip_hash_comments "$wf" | grep -E '\bpostulate\b' | grep -qE 'grep|rg |for pattern in'; then pass "07a-idris-postulate-grep" "$wf greps src/abi for postulate" else - fail "07a-idris-postulate-grep" "$wf does not grep for postulate" + fail "07a-idris-postulate-grep" "$wf does not grep for postulate outside comments" fi - for rel in EchidnaABI/CapnSchemas.idr CoprocessorForeign.idr; do - [ -f "src/abi/$rel" ] || continue - mod=$(sed 's/\.idr$//; s#/#.#g' <<<"$rel") - grep -qE "^[[:space:]]*(modules[[:space:]]*=|,)[[:space:]]*${mod//./\\.}[[:space:]]*(,|$)" "$ipkg" || missing+=("$mod") - done - if [ ${#missing[@]} -eq 0 ]; then - pass "07b-ipkg-coverage" "CapnSchemas and CoprocessorForeign are in $ipkg or deleted" + if [ ! -f "$ipkg" ]; then + fail "07b-ipkg-coverage" "$ipkg is missing" else - fail "07b-ipkg-coverage" "present but not in $ipkg: ${missing[*]}" + mods=$(ipkg_modules "$ipkg") + for rel in EchidnaABI/CapnSchemas.idr CoprocessorForeign.idr; do + [ -f "src/abi/$rel" ] || continue + mod=$(sed 's/\.idr$//; s#/#.#g' <<<"$rel") + grep -qxF "$mod" <<<"$mods" || missing+=("$mod") + done + if [ ${#missing[@]} -eq 0 ]; then + pass "07b-ipkg-coverage" "CapnSchemas and CoprocessorForeign are in $ipkg or deleted" + else + fail "07b-ipkg-coverage" "present but not in $ipkg: ${missing[*]}" + fi fi local mc=meta-checker/src/Echidna/MetaChecker.agda awf=.github/workflows/agda-meta-checker.yml - if [ -f "$awf" ] && grep -qE 'agda .*AxiomTrackerCompleteness\.agda' "$awf"; then + if [ -f "$awf" ] && strip_hash_comments "$awf" | grep -qE 'agda .*AxiomTrackerCompleteness\.agda'; then pass "07c-meta-checker-completeness" "$awf type-checks AxiomTrackerCompleteness.agda directly" - elif [ -f "$mc" ] && grep -qE '^[[:space:]]*(open[[:space:]]+)?import[[:space:]]+Echidna\.AxiomTrackerCompleteness([[:space:]]|$)' "$mc" \ - && [ -f "$awf" ] && grep -qE 'agda .*MetaChecker\.agda' "$awf"; then + elif [ -f "$mc" ] && strip_agda_comments "$mc" | grep -qE '^[[:space:]]*(open[[:space:]]+)?import[[:space:]]+Echidna\.AxiomTrackerCompleteness([[:space:]]|$)' \ + && [ -f "$awf" ] && { strip_hash_comments "$awf" | grep -qE 'agda .*MetaChecker\.agda' \ + || { strip_hash_comments "$awf" | grep -qE 'scripts/ci/check-agda\.sh' \ + && [ -f scripts/ci/check-agda.sh ] && strip_hash_comments scripts/ci/check-agda.sh | grep -qE 'MetaChecker\.agda'; }; }; then pass "07c-meta-checker-completeness" "MetaChecker.agda imports Echidna.AxiomTrackerCompleteness and $awf checks MetaChecker.agda" else fail "07c-meta-checker-completeness" "AxiomTrackerCompleteness is not type-checked by the meta-checker job" @@ -308,12 +394,16 @@ check_9() { # timestamp 2026-04-25T15:26:45.716Z, with no run behind it (L-4). if [ ! -e "$f" ]; then pass "$id" "$f is gone" - elif jq -e '(.timestamp == "2026-04-25T15:26:45.716Z") or (.MRR == 0.85 and .nDCG == 0.85 and .training_data_size == 10011)' "$f" >/dev/null 2>&1; then + elif ! jq -e 'type == "object"' "$f" >/dev/null 2>&1; then + fail "$id" "$f is not a JSON object" + elif jq -e '(.MRR == 0.85 and .nDCG == 0.85) or ((.timestamp // "") | startswith("2026-04-25T15:26"))' "$f" >/dev/null 2>&1; then fail "$id" "$f still holds the fabricated metrics" - elif ! jq -e . "$f" >/dev/null 2>&1; then - fail "$id" "$f is not valid JSON" + elif jq -e '(.provenance | type) == "object" + and ((.provenance.commit // "") | test("^[0-9a-f]{40}$")) + and ((.provenance.run_id // "") | type == "string" and length > 0)' "$f" >/dev/null 2>&1; then + pass "$id" "$f carries run provenance ($(jq -r '.provenance.run_id + " at " + .provenance.commit[0:9]' "$f"))" else - pass "$id" "$f no longer holds the fabricated metrics" + fail "$id" "$f has no run provenance (provenance.commit and provenance.run_id)" fi } @@ -321,8 +411,21 @@ check_9() { RULING_IDS="D-A D-B D-C D-D D-E D-F D-G D-H D-I D-J D-K D-L D-M D-N D2 D3 D5 D6 D7" +# ruling_sections : for every section heading (== or deeper), the line +# " ". +ruling_sections() { + awk -v ids="$RULING_IDS" ' + BEGIN { n = split(ids, id, " ") } + /^==+[[:space:]]/ { + named = "" + for (k = 1; k <= n; k++) + if (match($0, "(^|[^A-Za-z0-9-])" id[k] "([^A-Za-z0-9]|$)")) named = named " " id[k] + print NR named + }' "$1" +} + check_10() { - local id="10a-rulings-ledger" adrs adr r block status problems=() + local id="10a-rulings-ledger" adrs adr r sections line from to block statuses status problems=() adrs=$(find docs/decisions -maxdepth 1 -name 'ADR-*-rulings-ledger.adoc' 2>/dev/null | sort) if [ -z "$adrs" ]; then fail "$id" "no docs/decisions/ADR-*-rulings-ledger.adoc" @@ -330,23 +433,29 @@ check_10() { fail "$id" "more than one rulings ledger: $(tr '\n' ' ' <<<"$adrs")" else adr="$adrs" + sections=$(ruling_sections "$adr") + while read -r line r rest; do + [ -n "${rest:-}" ] && problems+=("heading at line $line names more than one ruling ($r $rest)") + done <<<"$sections" for r in $RULING_IDS; do - # The section whose heading names the ruling, up to the next heading. - block=$(awk -v r="$r" ' - function names(s) { return match(s, "(^|[^A-Za-z0-9-])" r "([^A-Za-z0-9]|$)") } - /^=+[[:space:]]/ { on = names($0); if (on) found = 1 } - on { print } - END { exit found ? 0 : 1 }' "$adr") || { problems+=("$r: no section"); continue; } - status=$(grep -E '^:status:[[:space:]]*' <<<"$block" | tail -1 | sed -E 's/^:status:[[:space:]]*//; s/[[:space:]]+$//') + line=$(awk -v r="$r" 'NF == 2 && $2 == r { print $1 }' <<<"$sections") + if [ -z "$line" ]; then problems+=("$r: no section of its own"); continue; fi + if [ "$(wc -l <<<"$line")" -ne 1 ]; then problems+=("$r: more than one section"); continue; fi + from="$line" + to=$(awk -v f="$from" '$1 > f { print $1 - 1; exit }' <<<"$sections") + block=$(sed -n "${from},${to:-\$}p" "$adr") + statuses=$(grep -cE '^:status:' <<<"$block") + status=$(grep -E '^:status:' <<<"$block" | sed -E 's/^:status:[[:space:]]*//; s/[[:space:]]+$//') + if [ "$statuses" -ne 1 ]; then problems+=("$r: $statuses :status: lines"); continue; fi case "$status" in open) ;; - ruled) grep -qE 'https://|link:|xref:|<<' <<<"$block" || problems+=("$r: ruled without a link to the owner's record") ;; - "") problems+=("$r: no :status:") ;; + ruled) grep -qE 'https://github\.com/hyperpolymath/[^[:space:]]+' <<<"$block" \ + || problems+=("$r: ruled without a link to the owner's record on github.com/hyperpolymath") ;; *) problems+=("$r: :status: $status") ;; esac done if [ ${#problems[@]} -eq 0 ]; then - pass "$id" "$adr records all $(wc -w <<<"$RULING_IDS") rulings as open or ruled-with-link" + pass "$id" "$adr records all $(wc -w <<<"$RULING_IDS") rulings, one section each, as open or ruled-with-record" else fail "$id" "$adr: $(printf '%s; ' "${problems[@]}")" fi @@ -355,54 +464,61 @@ check_10() { if [ ! -x scripts/ci/ruling-cited.sh ]; then fail "10b-ruling-cited" "scripts/ci/ruling-cited.sh is missing or not executable"; return fi - gate_cmd "10b-ruling-cited" "scripts/ci/ruling-cited.sh" -- scripts/ci/ruling-cited.sh + gate_cmd "10b-ruling-cited" "scripts/ci/ruling-cited.sh ${W0_BASE:0:9} $W0_HEAD" -- \ + scripts/ci/ruling-cited.sh "$W0_BASE" "$W0_HEAD" } # ------------------------------------- (11, 12) consumer repositories green -# consumer_green -consumer_green() { - local id="$1" repo="$2" re="$3" what="$4" branch sha runs hits bad - if ! have_token; then - deferred "$id" secret:GITHUB_TOKEN "reading $OWNER/$repo check runs needs a read token"; return - fi +# consumer_eval : sets C_GREEN (1 or empty) and C_DETAIL. +consumer_eval() { + local repo="$1" job="$2" branch sha runs hits n bad + C_GREEN="" if ! branch=$(gh_get "repos/$OWNER/$repo" | jq -er '.default_branch'); then - fail "$id" "cannot read $OWNER/$repo, and no handover under $(handover_dir "$repo")/"; return + C_DETAIL="cannot read $OWNER/$repo"; return fi if ! sha=$(gh_get "repos/$OWNER/$repo/commits/$branch" | jq -er '.sha') || ! runs=$(check_runs "$OWNER/$repo" "$sha"); then - fail "$id" "cannot read check runs on $OWNER/$repo $branch"; return + C_DETAIL="cannot read check runs on $OWNER/$repo $branch"; return fi - hits=$(jq -c --arg re "$re" '[.[] | select(.name | test($re; "i"))]' <<<"$runs") - if [ "$(jq length <<<"$hits")" -eq 0 ]; then - fail "$id" "no $what check run matching /$re/ on $OWNER/$repo $branch (${sha:0:9})"; return + if ! hits=$(jq -ec --arg j "$job" '[.[] | select(.name == $j or (.name | endswith(" / " + $j)))]' <<<"$runs") \ + || ! n=$(jq -e 'length' <<<"$hits"); then + C_DETAIL="cannot parse check runs on $OWNER/$repo $branch"; return + fi + if [ "$n" -eq 0 ]; then + C_DETAIL="no check run named '$job' on $OWNER/$repo $branch (${sha:0:9})"; return fi bad=$(jq -r '[.[] | select(.conclusion != "success") | "\(.name)=\(.conclusion // .status)"] | join(", ")' <<<"$hits") if [ -z "$bad" ]; then - pass "$id" "$OWNER/$repo $branch (${sha:0:9}): $what green ($(jq -r 'map(.name) | join(", ")' <<<"$hits"))" + C_GREEN=1 + C_DETAIL="$OWNER/$repo $branch (${sha:0:9}): '$job' green ($(jq -r 'map(.name) | join(", ")' <<<"$hits"))" else - fail "$id" "$OWNER/$repo $branch (${sha:0:9}): $bad" + C_DETAIL="$OWNER/$repo $branch (${sha:0:9}): $bad" + fi +} + +# consumer_check [patch-name-substring] +consumer_check() { + local id="$1" repo="$2" job="$3" sub="${4:-}" + consumer_eval "$repo" "$job" + if [ -n "$C_GREEN" ]; then + pass "$id" "$C_DETAIL" + elif handover_ok "$repo" "$sub"; then + deferred "$id" "no-push:$repo" "$C_DETAIL; handover committed under $(handover_dir "$repo")/" + else + fail "$id" "$C_DETAIL; no committed handover under $(handover_dir "$repo")/" fi } check_11() { - local repo var re - for repo in echidnabot proof-burrower panic-attack verisimdb; do - if has_handover "$repo"; then - deferred "11-conformance-$repo" "no-push:$repo" "patch and issue text committed under $(handover_dir "$repo")/" - continue - fi - var="W0_CHECK_RE_$(tr 'a-z-' 'A-Z_' <<<"$repo")" - if [ "$repo" = verisimdb ]; then re="${!var:-verisim-api}"; else re="${!var:-conformance}"; fi - consumer_green "11-conformance-$repo" "$repo" "$re" "conformance" + local repo + for repo in echidnabot proof-burrower panic-attack; do + consumer_check "11-conformance-$repo" "$repo" prove-result-conformance done + consumer_check "11-conformance-verisimdb" verisimdb verisim-api-list } check_12() { - if has_handover proof-burrower agda; then - deferred "12-proof-burrower-agda" "no-push:proof-burrower" "Agda patch and issue text committed under $(handover_dir proof-burrower)/" - return - fi - consumer_green "12-proof-burrower-agda" proof-burrower "${W0_CHECK_RE_PROOF_BURROWER_AGDA:-agda}" "Agda" + consumer_check "12-proof-burrower-agda" proof-burrower agda-proofs agda } # --------------------------------------- (13) Lean build recorded in claims @@ -415,30 +531,34 @@ check_13() { if ! is_jcs "$f"; then fail "$id" "$f is not one JCS value with a final LF"; return fi - hit=$(jq -c '[.. | objects - | select(([.id, .name, .claim] | map(strings) | join(" ")) | test("lake|lean[^ ]*[ _-]?build"; "i")) - | select(tojson | contains("4.13.0")) + if ! hit=$(jq -e '[.. | objects + | select(([.id, .name, .claim] | map(strings) | join(" ")) | test("\\blake[ _-]build\\b|\\blean4?[ _-]build\\b"; "i")) + | select(tojson | test("(^|[^0-9.])4\\.13\\.0([^0-9.]|$)")) | select(([.result, .status, .outcome] | map(strings | ascii_downcase) | any(. == "green" or . == "pass" or . == "passed" or . == "success")) - or ([.repair_item, .repair, .issue] | map(strings) | any(length > 0)))] | length' "$f") - if [ "${hit:-0}" -gt 0 ]; then - pass "$id" "$f records the Lean 4.13.0 lake build as green or with a repair item" + or ((.repair | type) == "object" and ((.repair.id // "") | type == "string" and length > 0) and .repair.before == "F-3"))] + | length' "$f"); then + fail "$id" "$f cannot be evaluated"; return + fi + if [ "$hit" -gt 0 ]; then + pass "$id" "$f records the Lean 4.13.0 lake build as green or with a repair item before F-3" else - fail "$id" "$f has no Lean 4.13.0 lake-build entry with a green result or a repair item" + fail "$id" "$f has no Lean 4.13.0 lake-build entry with a green result or a repair item before F-3" fi } -check_1 -check_2 -check_3 -check_4 -check_5 -check_6 -check_7 -check_8 -check_9 -check_10 -check_11 -check_12 -check_13 +# ------------------------------------------------------------------- run + +printf 'W0 config: repo=%s base=%s head=%s goldens=%s consumers=%s api=%s probe_pr=%s\n' \ + "$REPO" "$W0_BASE" "$W0_HEAD" "$GOLDENS" "$OWNER" \ + "$([ -n "${GITHUB_TOKEN:-}" ] && echo token || echo anonymous)" "${W0_PROBE_PR:-unset}" +gate_init W0 +if [ -n "${W0_CHECKS:-}" ]; then + for c in $W0_CHECKS; do + if declare -F "check_$c" >/dev/null; then "check_$c"; else fail "w0-checks" "no check $c"; fi + done + fail "w0-subset" "only checks $W0_CHECKS ran (W0_CHECKS); a subset run is not a gate result" +else + for c in 1 2 3 4 5 6 7 8 9 10 11 12 13; do "check_$c"; done +fi gate_finish From 2a4c424b39497093599decbef7b83bf254bd739f Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:02:26 +0000 Subject: [PATCH 3/4] fix(gates): close the remaining W0 gate false greens from Codex review Each finding is fixed at its source in scripts/gates/w0.sh and covered by a w0.selftest.sh case that fails on the previous gate and passes now. 1. (P1) Check 2 read only the first 30 legacy commit statuses. Statuses are now read over every page (per_page=100) and must add up to total_count, and GitHub's combined state must also be success whenever any status exists: it is computed over every context, so even a page the gate failed to read cannot hide a red status. Cases: "check 2 reads a red legacy status on page 2 of the statuses", "check 2 fails closed when a statuses page is missing", "check 2 requires the combined legacy state to be success". 2. (P1) Check 1 dropped integration_id from required contexts. It keeps (context, integration_id) pairs; a pinned context needs a green check run from that app (runs are now kept latest per name and app), and a legacy status cannot satisfy it. Unpinned contexts are unchanged. Cases: "a run from another app does not satisfy a pinned context", "a legacy status does not satisfy a pinned context". 3. (P2) Check 1 read one page of branch rules. Every page is collected (per_page=100) before required checks are extracted. Cases: "a required context in rules page 2 still gates check 1", "check 1 fails closed when a rules page is missing". 4. (P2) gh_get's curl was unbounded. It sets --connect-timeout 10, --max-time 60 and --retry-max-time 120. Case: "every GitHub API request sets connect, total and retry time limits" (the stub curl logs its arguments). 5. (P2) strip_hash_comments kept inline `#` comments. It now cuts a `#` at line start or after whitespace outside quotes; an apostrophe inside a word does not open a quote. Cases: "a postulate grep in an inline comment fails 07a", "an agda call in an inline comment fails 07c", "an apostrophe does not hide an inline comment from 07c". 6. (P2) Check 10a counted headings and :status: lines inside AsciiDoc blocks. Comment (////), listing (----), literal (....), passthrough (++++) and fenced (```) blocks are blanked first, line numbers kept. Cases: "a section inside a //// comment block does not count for 10a", "status lines and headings in listing blocks do not count for 10a". 7. (P2) Check 13 accepted a claims.json whose root is an array. The root must be an object. Case: "a claims.json whose root is an array fails 13". Shared paging lives in gh_pages, used by check_runs, commit_statuses and the rules read; any unreadable page, non-array page or page 21 is a FAIL. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- scripts/gates/w0.selftest.sh | 131 ++++++++++++++++++++++++-- scripts/gates/w0.sh | 175 ++++++++++++++++++++++++++--------- 2 files changed, 256 insertions(+), 50 deletions(-) diff --git a/scripts/gates/w0.selftest.sh b/scripts/gates/w0.selftest.sh index 31881d29..c041c17a 100755 --- a/scripts/gates/w0.selftest.sh +++ b/scripts/gates/w0.selftest.sh @@ -10,7 +10,10 @@ # The planted artefacts include each false green found in review: a commit # with more than 100 check runs, governance jobs named "... conformance", # empty untracked handover files, blank and glob backend names, nudged -# fabricated metrics, a one-heading rulings ledger and a "nix flake" claim. +# fabricated metrics, a one-heading rulings ledger, a "nix flake" claim, +# legacy statuses and rules past page one, a pinned context met by the +# wrong app, inline `#` comments, ledger sections inside comment blocks and +# a claims.json whose root is an array. # # Usage: scripts/gates/w0.selftest.sh Exit 0 iff every case behaves. @@ -31,8 +34,10 @@ cases=0 mkdir -p "$tmp/bin" cat > "$tmp/bin/curl" <<'EOF' #!/usr/bin/env bash -# Serves https://api.github.com/ from $STUB_API/. +# Serves https://api.github.com/ from $STUB_API/ +# and logs its arguments, one call per line, to $STUB_API.calls. url="${*: -1}" +printf '%s\n' "$*" >> "$STUB_API.calls" key=$(printf '%s' "${url#https://api.github.com/}" | tr '/?&=' '____') [ -f "$STUB_API/$key" ] || { echo "curl stub: no fixture for $url" >&2; exit 22; } cat "$STUB_API/$key" @@ -61,6 +66,20 @@ serve() { printf '%s\n' "$2" > "$STUB_API/$(printf '%s' "$1" | tr '/?&=' '____')" } +# serve_status : page 1 of the combined commit status. +# The unpaged path is served the same body, so the cases also run against +# the gate before it paginated (to show they fail there). +serve_status() { + serve "repos/$1/commits/$2/status?per_page=100&page=1" "$3" + serve "repos/$1/commits/$2/status" "$3" +} + +# serve_rules : page 1 of the echidna main rules (and the unpaged path). +serve_rules() { + serve "repos/hyperpolymath/echidna/rules/branches/main?per_page=100&page=1" "$1" + serve "repos/hyperpolymath/echidna/rules/branches/main" "$1" +} + # runs_json : a check-runs page. runs_json() { jq -cn --argjson n "$1" --arg bad "$2" --arg pad "$3" --argjson off "${4:-0}" ' @@ -104,7 +123,7 @@ head=$(git -C "$R" rev-parse HEAD) pad=$(printf 'p%.0s' $(seq 1 1500)) serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=1" "$(runs_json 100 "" "$pad")" serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=2" "$(runs_json 50 "job-140-$pad" "$pad" 100)" -serve "repos/hyperpolymath/echidna/commits/$head/status" '{"statuses":[]}' +serve_status hyperpolymath/echidna "$head" '{"state":"pending","total_count":0,"statuses":[]}' gate 2 W0_BASE="$base" W0_HEAD="$head" expect "check 2 sees a failure on page 2 of 150 large runs" FAIL 02-w0-merges-green "job-140-p+=failure" @@ -120,13 +139,44 @@ rm -f "$STUB_API"/*page_2 gate 2 W0_BASE="$base" W0_HEAD="$head" expect "check 2 fails closed on an unreadable page" FAIL 02-w0-merges-green "unreadable" +# ------------------------------- check 2: legacy statuses beyond page one + +# statuses_json [offset] +statuses_json() { + jq -cn --argjson n "$1" --arg last "$2" --arg st "$3" --argjson t "$4" --argjson off "${5:-0}" ' + {state: $st, total_count: $t, statuses: [range($n) as $i + | {context: "legacy-\($i + $off)", state: (if $i == $n - 1 then $last else "success" end)}]}' +} +new_repo +base=$(git -C "$R" rev-parse HEAD) +echo x > "$R/f"; commit_all merge +head=$(git -C "$R" rev-parse HEAD) +serve "repos/hyperpolymath/echidna/commits/$head/check-runs?per_page=100&page=1" "$(runs_json 1 "" x)" +serve_status hyperpolymath/echidna "$head" "$(statuses_json 100 success failure 101)" +serve "repos/hyperpolymath/echidna/commits/$head/status?per_page=100&page=2" "$(statuses_json 1 failure failure 101 100)" +gate 2 W0_BASE="$base" W0_HEAD="$head" +expect "check 2 reads a red legacy status on page 2 of the statuses" FAIL 02-w0-merges-green "legacy-100=failure" + +rm -f "$STUB_API"/*status_per_page_100_page_2 +gate 2 W0_BASE="$base" W0_HEAD="$head" +expect "check 2 fails closed when a statuses page is missing" FAIL 02-w0-merges-green "unreadable" + +serve_status hyperpolymath/echidna "$head" "$(statuses_json 2 success failure 2)" +gate 2 W0_BASE="$base" W0_HEAD="$head" +expect "check 2 requires the combined legacy state to be success" FAIL 02-w0-merges-green "combined status=failure" + +serve_status hyperpolymath/echidna "$head" "$(statuses_json 100 success success 101)" +serve "repos/hyperpolymath/echidna/commits/$head/status?per_page=100&page=2" "$(statuses_json 1 success success 101 100)" +gate 2 W0_BASE="$base" W0_HEAD="$head" +expect "check 2 passes 101 green legacy statuses over two pages" PASS 02-w0-merges-green + # ----------------------------------------- check 1: probe PR required contexts new_repo psha=0123456789abcdef0123456789abcdef0123abcd -serve "repos/hyperpolymath/echidna/rules/branches/main" '[{"type":"required_status_checks","parameters":{"required_status_checks":[{"context":"rust-ci / Cargo test"},{"context":"gitleaks"}]}}]' +serve_rules '[{"type":"required_status_checks","parameters":{"required_status_checks":[{"context":"rust-ci / Cargo test"},{"context":"gitleaks"}]}}]' serve "repos/hyperpolymath/echidna/pulls/7" "{\"head\":{\"sha\":\"$psha\"}}" -serve "repos/hyperpolymath/echidna/commits/$psha/status" '{"statuses":[{"context":"gitleaks","state":"success"}]}' +serve_status hyperpolymath/echidna "$psha" '{"state":"success","total_count":1,"statuses":[{"context":"gitleaks","state":"success"}]}' serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"failure"}]}' gate 1 W0_PROBE_PR=7 expect "a red required context fails check 1 by name" FAIL 01-probe-pr-required-contexts "not success: rust-ci / Cargo test;" @@ -135,10 +185,47 @@ gate 1 W0_PROBE_PR=7 expect "every required context green passes check 1" PASS 01-probe-pr-required-contexts "all 2 required contexts" gate 1 expect "check 1 needs W0_PROBE_PR" FAIL 01-probe-pr-required-contexts "W0_PROBE_PR is not set" -serve "repos/hyperpolymath/echidna/rules/branches/main" '[]' +serve_rules '[]' gate 1 W0_PROBE_PR=7 expect "a ruleset with no required context fails check 1" FAIL 01-probe-pr-required-contexts "requires no status context" +# Pinned contexts: integration_id names the app whose check run counts. +pinned='[{"type":"required_status_checks","parameters":{"required_status_checks":[{"context":"rust-ci / Cargo test","integration_id":15368},{"context":"gitleaks"}]}}]' +serve_rules "$pinned" +serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"success","app":{"id":999}}]}' +gate 1 W0_PROBE_PR=7 +expect "a run from another app does not satisfy a pinned context" FAIL 01-probe-pr-required-contexts "not success: rust-ci / Cargo test \(app 15368\);" +serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[]}' +serve_status hyperpolymath/echidna "$psha" '{"state":"success","total_count":2,"statuses":[{"context":"gitleaks","state":"success"},{"context":"rust-ci / Cargo test","state":"success"}]}' +gate 1 W0_PROBE_PR=7 +expect "a legacy status does not satisfy a pinned context" FAIL 01-probe-pr-required-contexts "rust-ci / Cargo test \(app 15368\)" +serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"success","app":{"id":999}},{"id":2,"name":"rust-ci / Cargo test","status":"completed","conclusion":"success","app":{"id":15368}}]}' +gate 1 W0_PROBE_PR=7 +expect "a green run from the pinned app passes check 1" PASS 01-probe-pr-required-contexts "all 2 required contexts" + +# Rules on page 2: page 1 is full (100 rules), the red context is on page 2. +serve_status hyperpolymath/echidna "$psha" '{"state":"success","total_count":1,"statuses":[{"context":"gitleaks","state":"success"}]}' +serve_rules "$(jq -cn '[range(99) | {type: "deletion"}] + [{type: "required_status_checks", parameters: {required_status_checks: [{context: "gitleaks"}]}}]')" +serve "repos/hyperpolymath/echidna/rules/branches/main?per_page=100&page=2" '[{"type":"required_status_checks","parameters":{"required_status_checks":[{"context":"rust-ci / Cargo test"}]}}]' +serve "repos/hyperpolymath/echidna/commits/$psha/check-runs?per_page=100&page=1" '{"check_runs":[{"id":1,"name":"rust-ci / Cargo test","status":"completed","conclusion":"failure"}]}' +gate 1 W0_PROBE_PR=7 +expect "a required context in rules page 2 still gates check 1" FAIL 01-probe-pr-required-contexts "not success: rust-ci / Cargo test;" +rm -f "$STUB_API"/*main_per_page_100_page_2 +gate 1 W0_PROBE_PR=7 +expect "check 1 fails closed when a rules page is missing" FAIL 01-probe-pr-required-contexts "cannot read the live ruleset" + +# Every GitHub API request is bounded in time. +cases=$((cases + 1)) +if [ -s "$STUB_API.calls" ] \ + && ! grep -vE -- '--connect-timeout [0-9]+ ' "$STUB_API.calls" | grep -q . \ + && ! grep -vE -- '--max-time [0-9]+ ' "$STUB_API.calls" | grep -q . \ + && ! grep -vE -- '--retry-max-time [0-9]+ ' "$STUB_API.calls" | grep -q .; then + echo "ok every GitHub API request sets connect, total and retry time limits" +else + failures=$((failures + 1)); echo "FAIL every GitHub API request sets connect, total and retry time limits" + sed 's/^/ | /' "$STUB_API.calls" | head -n 3 +fi + # ------------------------------------------- checks 11/12: consumer repos # consumer : serve the repo, its head and its runs. @@ -257,6 +344,20 @@ expect "a ruled section with the owner's record passes 10a" PASS 10a-rulings-led ledger "${good_ledger/:status: open/:status: open :status: ruled}" expect "two status lines in one section fail 10a" FAIL 10a-rulings-ledger "D-A: 2 :status: lines" +commented_ledger=$(printf '= Rulings\n\n////\n== D-A\n:status: open\n////\n'; for r in ${ids#D-A }; do printf '\n== %s\n:status: open\n' "$r"; done) +ledger "$commented_ledger" +expect "a section inside a //// comment block does not count for 10a" FAIL 10a-rulings-ledger "D-A: no section of its own" +ledger "${good_ledger/:status: open/:status: open + +---- +:status: ruled +== D-A +---- + +.... +:status: ruled +....}" +expect "status lines and headings in listing blocks do not count for 10a" PASS 10a-rulings-ledger # ------------------------------------------------- check 13: Lean claims @@ -274,6 +375,8 @@ claims '{"claims":[{"claim":"lake build","toolchain":"4.13.0","repair":{"id":"R- expect "a repair item before F-3 passes 13" PASS 13-lean-build-recorded claims '{"claims":[{"claim":"Lean 4 lake build of verification/proofs/lean4","toolchain":"leanprover/lean4:v4.13.0","result":"green"}]}' expect "a green lake build passes 13" PASS 13-lean-build-recorded +claims '[{"claim":"Lean 4 lake build","toolchain":"4.13.0","result":"green"}]' +expect "a claims.json whose root is an array fails 13" FAIL 13-lean-build-recorded "not a JSON object at its root" # ----------------------------------------------- check 7: Idris/Agda hygiene @@ -297,6 +400,22 @@ expect "a real postulate grep passes 07a" PASS 07a-idris-postulate-grep expect "a module listed under depends does not count for 07b" FAIL 07b-ipkg-coverage "CoprocessorForeign" expect "a real import checked through check-agda.sh passes 07c" PASS 07c-meta-checker-completeness +# Inline `#` comments: a mention after code on the line does not count. +printf 'run: echo ok # grep -rn postulate src/abi\n' > "$R/.github/workflows/idris2-abi-ci.yml" +printf 'module Echidna.MetaChecker where\n' > "$R/meta-checker/src/Echidna/MetaChecker.agda" +printf 'run: echo ok # agda src/Echidna/AxiomTrackerCompleteness.agda\n' > "$R/.github/workflows/agda-meta-checker.yml" +gate 7 +expect "a postulate grep in an inline comment fails 07a" FAIL 07a-idris-postulate-grep +expect "an agda call in an inline comment fails 07c" FAIL 07c-meta-checker-completeness +printf 'run: grep -rnE "believe_me #|postulate" src/abi\n' > "$R/.github/workflows/idris2-abi-ci.yml" +printf "run: echo don't # agda src/Echidna/AxiomTrackerCompleteness.agda\n" > "$R/.github/workflows/agda-meta-checker.yml" +gate 7 +expect "a # inside quotes does not cut the line for 07a" PASS 07a-idris-postulate-grep +expect "an apostrophe does not hide an inline comment from 07c" FAIL 07c-meta-checker-completeness +printf 'run: agda --safe src/Echidna/AxiomTrackerCompleteness.agda # completeness\n' > "$R/.github/workflows/agda-meta-checker.yml" +gate 7 +expect "an agda call before an inline comment passes 07c" PASS 07c-meta-checker-completeness + # ---------------------------------------------------- subset runs and config new_repo diff --git a/scripts/gates/w0.sh b/scripts/gates/w0.sh index 4ef5ec8b..b922d5fc 100755 --- a/scripts/gates/w0.sh +++ b/scripts/gates/w0.sh @@ -63,17 +63,19 @@ # docs/decisions/ADR-*-rulings-ledger.adoc (check 10) # One section per ruling (D-A, ..., D-N, D2, D3, D5, D6, D7) whose # heading (== or deeper) names exactly one ruling id, with exactly one -# attribute line `:status: open` or `:status: ruled`. A ruled section -# links the owner's record on https://github.com/hyperpolymath/. +# attribute line `:status: open` or `:status: ruled`, all outside +# comment and verbatim blocks (////, ----, ...., ++++, ```). A ruled +# section links the owner's record on https://github.com/hyperpolymath/. # scripts/ci/ruling-cited.sh (check 10b) # Called as `ruling-cited.sh `; exits 0 iff every W0 # PR in that range cites the rulings it acts on. # docs/proofs/claims.json (check 13) -# One JCS value holding an object whose id, name or claim names the Lean -# build ("lake build", "lean build", "lean4 build"), which mentions the -# version 4.13.0 as a whole token, and which carries either a green -# result (result/status/outcome: green, pass, passed, success) or a -# "repair" object with a non-empty "id" and "before": "F-3". +# One JCS value whose root is an object (a root array FAILs), holding +# an object whose id, name or claim names the Lean build ("lake build", +# "lean build", "lean4 build"), which mentions the version 4.13.0 as a +# whole token, and which carries either a green result +# (result/status/outcome: green, pass, passed, success) or a "repair" +# object with a non-empty "id" and "before": "F-3". # The checks are called through "check_$c", which shellcheck cannot follow. # shellcheck disable=SC2317 @@ -95,37 +97,52 @@ GOLDENS="${W0_HOTSPOT_GOLDENS:-tests/golden/hotspot}" # ---------------------------------------------------------------- helpers # gh_get : GET from the GitHub REST API, body on stdout. The -# Authorization header is sent only when a token is present. +# Authorization header is sent only when a token is present. Every request +# is bounded (connect 10 s, transfer 60 s, retries 120 s in all), so a +# stalled API is a FAIL, not a gate that never ends. gh_get() { local auth=() [ -n "${GITHUB_TOKEN:-}" ] && auth=(-H "Authorization: Bearer $GITHUB_TOKEN") - curl -fsS --retry 2 \ + curl -fsS --connect-timeout 10 --max-time 60 --retry 2 --retry-max-time 120 \ ${auth[@]+"${auth[@]}"} \ -H "Accept: application/vnd.github+json" \ -H "X-GitHub-Api-Version: 2022-11-28" \ "https://api.github.com/$1" } -# check_runs : every check run on the commit, latest per name, -# as a JSON array of {name, status, conclusion}. Returns non-zero, with no -# output, when any page cannot be read or parsed, or when there are more -# pages than it will follow: a partial list must never read as a full one. -# Pages are collected in a file, not passed through argv, because a commit -# with many runs produces arrays larger than the argument limit. -check_runs() { - local repo="$1" sha="$2" page=1 body n tmp out - tmp=$(mktemp) || return 1 +# gh_pages : GET every +# page (per_page=100) of a paginated endpoint and write the bodies to the +# file, one per line. Returns non-zero when any page cannot be read, when a +# page's items are not an array, or when there are more pages than it will +# follow: a partial list must never read as a full one. Pages go to a file, +# not through argv, because a commit with many runs produces arrays larger +# than the argument limit. +gh_pages() { + local out="$1" path="$2" items="$3" page=1 body n + : > "$out" || return 1 while :; do - if ! body=$(gh_get "repos/$repo/commits/$sha/check-runs?per_page=100&page=$page") \ - || ! n=$(jq -e '.check_runs | length' <<<"$body" 2>/dev/null); then - rm -f "$tmp"; return 1 + if ! body=$(gh_get "$path?per_page=100&page=$page") \ + || ! n=$(jq -e "$items | if type == \"array\" then length else error(\"not an array\") end" <<<"$body" 2>/dev/null); then + return 1 fi - printf '%s\n' "$body" >> "$tmp" - [ "$n" -lt 100 ] && break + printf '%s\n' "$body" >> "$out" + [ "$n" -lt 100 ] && return 0 page=$((page + 1)) - if [ "$page" -gt 20 ]; then rm -f "$tmp"; return 1; fi + [ "$page" -gt 20 ] && return 1 done - if ! out=$(jq -cs 'map(.check_runs) | add // [] | group_by(.name) | map(max_by(.id) | {name, status, conclusion})' "$tmp") \ +} + +# check_runs : every check run on the commit, latest per name +# and app, as a JSON array of {name, status, conclusion, app_id}. Returns +# non-zero, with no output, when the runs cannot be read in full. +check_runs() { + local repo="$1" sha="$2" tmp out + tmp=$(mktemp) || return 1 + if ! gh_pages "$tmp" "repos/$repo/commits/$sha/check-runs" '.check_runs' \ + || ! out=$(jq -cs 'map(.check_runs) | add // [] + | map(. + {app_id: (.app.id // null)}) + | group_by([.name, .app_id]) + | map(max_by(.id) | {name, status, conclusion, app_id})' "$tmp") \ || [ -z "$out" ] || ! jq -e 'type == "array"' <<<"$out" >/dev/null 2>&1; then rm -f "$tmp"; return 1 fi @@ -133,6 +150,25 @@ check_runs() { printf '%s\n' "$out" } +# commit_statuses : the combined legacy commit status with the +# statuses of every page, as {state, total_count, statuses}. Returns +# non-zero, with no output, when any page cannot be read or the pages do not +# add up to total_count. +commit_statuses() { + local repo="$1" sha="$2" tmp out + tmp=$(mktemp) || return 1 + if ! gh_pages "$tmp" "repos/$repo/commits/$sha/status" '.statuses' \ + || ! out=$(jq -cs '{state: .[0].state, total_count: .[0].total_count, statuses: (map(.statuses) | add // [])} + | if (.state | type) == "string" and (.total_count | type) == "number" + and (.statuses | length) == .total_count + then . else error("incomplete combined status") end' "$tmp" 2>/dev/null) \ + || [ -z "$out" ]; then + rm -f "$tmp"; return 1 + fi + rm -f "$tmp" + printf '%s\n' "$out" +} + # is_jcs : one JSON value, serialised as JCS, one final LF. # (jq -cS matches JCS for the strings, integers and plain decimals these # ledgers hold; it is not a general JCS number serialiser.) @@ -142,8 +178,24 @@ is_jcs() { cmp -s <(jq -cS . "$f") "$f" } -# strip_hash_comments : the file without shell/YAML `#` comment lines. -strip_hash_comments() { grep -vE '^[[:space:]]*#' "$1"; } +# strip_hash_comments : the file without shell/YAML `#` comments, +# whole-line and inline. A `#` starts a comment at the start of a line or +# after whitespace, outside single and double quotes. A quote opens only +# where it does not follow a letter or digit, so the apostrophe in "don't" +# does not hide a comment after it. Quote state does not span lines. +strip_hash_comments() { + awk ' + { line = $0; out = ""; q = ""; prev = "" + for (i = 1; i <= length(line); i++) { + c = substr(line, i, 1) + if (q == "\"" && c == "\\") { out = out c substr(line, i + 1, 1); prev = substr(line, i + 1, 1); i++; continue } + if (q != "") { if (c == q) q = ""; out = out c; prev = c; continue } + if (c == "#" && (prev == "" || prev ~ /[[:space:]]/)) break + if ((c == "\"" || c == "'\''") && prev !~ /[[:alnum:]]/) q = c + out = out c; prev = c + } + print out }' "$1" +} # strip_agda_comments : the file without `--` line comments and # (nested) `{- ... -}` block comments. @@ -186,11 +238,17 @@ handover_ok() { # --------------------------------------------- (1) probe PR required contexts check_1() { - local id="01-probe-pr-required-contexts" rules req sha runs statuses missing ctx ok - if ! rules=$(gh_get "repos/$REPO/rules/branches/main"); then - fail "$id" "cannot read the live ruleset for $REPO main"; return + local id="01-probe-pr-required-contexts" tmp rules req sha runs statuses missing r ctx ok + # Every page of rules: a required_status_checks rule on page 2 still gates. + tmp=$(mktemp) || { fail "$id" "cannot create a temporary file"; return; } + if ! gh_pages "$tmp" "repos/$REPO/rules/branches/main" '.' || ! rules=$(jq -cs 'add // []' "$tmp"); then + rm -f "$tmp"; fail "$id" "cannot read the live ruleset for $REPO main"; return fi - if ! req=$(jq -er '[.[] | select(.type == "required_status_checks") | .parameters.required_status_checks[].context] | unique | .[]' <<<"$rules"); then + rm -f "$tmp" + # One {context, integration_id} per line; integration_id is null when the + # context is not pinned to an app. + if ! req=$(jq -ec '[.[] | select(.type == "required_status_checks") | .parameters.required_status_checks[] + | {context, integration_id: (.integration_id // null)}] | unique | .[]' <<<"$rules"); then fail "$id" "the live ruleset requires no status context; nothing would gate a merge"; return fi if ! [[ ${W0_PROBE_PR:-} =~ ^[0-9]+$ ]]; then @@ -199,16 +257,21 @@ check_1() { if ! sha=$(gh_get "repos/$REPO/pulls/$W0_PROBE_PR" | jq -er '.head.sha'); then fail "$id" "cannot read probe PR #$W0_PROBE_PR"; return fi - if ! runs=$(check_runs "$REPO" "$sha") || ! statuses=$(gh_get "repos/$REPO/commits/$sha/status"); then + if ! runs=$(check_runs "$REPO" "$sha") || ! statuses=$(commit_statuses "$REPO" "$sha"); then fail "$id" "cannot read check runs for probe PR #$W0_PROBE_PR ($sha)"; return fi missing=() - while IFS= read -r ctx; do - # Not jq -e: a context that is not green evaluates to false, which is an - # answer, not an error. - ok=$(jq -r --arg c "$ctx" --slurpfile s <(printf '%s\n' "$statuses") ' - ([.[] | select(.name == $c and .conclusion == "success")] | length > 0) - or ([$s[0].statuses[] | select(.context == $c and .state == "success")] | length > 0)' <<<"$runs") + while IFS= read -r r; do + # A context pinned to an app (integration_id) is satisfied only by a + # check run from that app; a legacy status cannot satisfy it. Not jq -e: + # a context that is not green evaluates to false, which is an answer, + # not an error. + ok=$(jq -r --argjson r "$r" --slurpfile s <(printf '%s\n' "$statuses") ' + ([.[] | select(.name == $r.context and .conclusion == "success" + and ($r.integration_id == null or .app_id == $r.integration_id))] | length > 0) + or ($r.integration_id == null + and ([$s[0].statuses[] | select(.context == $r.context and .state == "success")] | length > 0))' <<<"$runs") + ctx=$(jq -r '.context + (if .integration_id == null then "" else " (app \(.integration_id))" end)' <<<"$r") case "$ok" in true|false) ;; *) fail "$id" "cannot evaluate required context '$ctx'"; return ;; @@ -234,15 +297,21 @@ check_2() { fi for c in $commits; do n=$((n + 1)) - if ! runs=$(check_runs "$REPO" "$c") || ! statuses=$(gh_get "repos/$REPO/commits/$c/status") \ - || ! nr=$(jq -e 'length' <<<"$runs") || ! ns=$(jq -e '.statuses | length' <<<"$statuses"); then + # Legacy statuses: every page is read, and GitHub's combined state must + # also be success whenever any status exists. The combined state is + # computed over every context, so even a page this script failed to + # read cannot hide a red status; the pages only name which one. + if ! runs=$(check_runs "$REPO" "$c") || ! statuses=$(commit_statuses "$REPO" "$c") \ + || ! nr=$(jq -e 'length' <<<"$runs") || ! ns=$(jq -e '.total_count' <<<"$statuses"); then problems+=("${c:0:9} unreadable"); continue fi if [ "$nr" -eq 0 ] && [ "$ns" -eq 0 ]; then problems+=("${c:0:9} has no check runs"); continue fi if ! bad=$(jq -er '[.[] | select((.conclusion // "pending") as $k | ["success","skipped","neutral"] | index($k) | not) | "\(.name)=\(.conclusion // .status)"] | join(", ")' <<<"$runs") \ - || ! st=$(jq -er '[.statuses[] | select(.state != "success") | "\(.context)=\(.state)"] | join(", ")' <<<"$statuses"); then + || ! st=$(jq -er '[.statuses[] | select(.state != "success") | "\(.context)=\(.state)"] + + (if .total_count > 0 and .state != "success" then ["combined status=\(.state)"] else [] end) + | join(", ")' <<<"$statuses"); then problems+=("${c:0:9} unparseable"); continue fi soft=$((soft + $(jq '[.[] | select(.conclusion == "skipped" or .conclusion == "neutral")] | length' <<<"$runs"))) @@ -411,6 +480,18 @@ check_9() { RULING_IDS="D-A D-B D-C D-D D-E D-F D-G D-H D-I D-J D-K D-L D-M D-N D2 D3 D5 D6 D7" +# adoc_strip_blocks : the file with every line of a comment (////), +# listing (----), literal (....), passthrough (++++) or fenced (```) block, +# delimiters included, blanked. Line numbers are kept. A block closes only +# on a line equal to its opening delimiter; an unclosed block runs to the +# end of the file, so nothing after a stray delimiter can count. +adoc_strip_blocks() { + awk ' + delim != "" { if ($0 == delim) delim = ""; print ""; next } + /^(\/\/\/\/+|----+|\.\.\.\.+|\+\+\+\++)$/ || /^```/ { delim = ($0 ~ /^```/) ? "```" : $0; print ""; next } + { print }' "$1" +} + # ruling_sections : for every section heading (== or deeper), the line # " ". ruling_sections() { @@ -425,7 +506,7 @@ ruling_sections() { } check_10() { - local id="10a-rulings-ledger" adrs adr r sections line from to block statuses status problems=() + local id="10a-rulings-ledger" adrs adr r sections line from to block statuses status text problems=() adrs=$(find docs/decisions -maxdepth 1 -name 'ADR-*-rulings-ledger.adoc' 2>/dev/null | sort) if [ -z "$adrs" ]; then fail "$id" "no docs/decisions/ADR-*-rulings-ledger.adoc" @@ -433,7 +514,10 @@ check_10() { fail "$id" "more than one rulings ledger: $(tr '\n' ' ' <<<"$adrs")" else adr="$adrs" - sections=$(ruling_sections "$adr") + # Headings, :status: lines and links inside comment or verbatim blocks + # are not ledger content. + text=$(adoc_strip_blocks "$adr") + sections=$(ruling_sections <(printf '%s\n' "$text")) while read -r line r rest; do [ -n "${rest:-}" ] && problems+=("heading at line $line names more than one ruling ($r $rest)") done <<<"$sections" @@ -443,7 +527,7 @@ check_10() { if [ "$(wc -l <<<"$line")" -ne 1 ]; then problems+=("$r: more than one section"); continue; fi from="$line" to=$(awk -v f="$from" '$1 > f { print $1 - 1; exit }' <<<"$sections") - block=$(sed -n "${from},${to:-\$}p" "$adr") + block=$(sed -n "${from},${to:-\$}p" <<<"$text") statuses=$(grep -cE '^:status:' <<<"$block") status=$(grep -E '^:status:' <<<"$block" | sed -E 's/^:status:[[:space:]]*//; s/[[:space:]]+$//') if [ "$statuses" -ne 1 ]; then problems+=("$r: $statuses :status: lines"); continue; fi @@ -531,6 +615,9 @@ check_13() { if ! is_jcs "$f"; then fail "$id" "$f is not one JCS value with a final LF"; return fi + if ! jq -e 'type == "object"' "$f" >/dev/null 2>&1; then + fail "$id" "$f is not a JSON object at its root"; return + fi if ! hit=$(jq -e '[.. | objects | select(([.id, .name, .claim] | map(strings) | join(" ")) | test("\\blake[ _-]build\\b|\\blean4?[ _-]build\\b"; "i")) | select(tojson | test("(^|[^0-9.])4\\.13\\.0([^0-9.]|$)")) From 7304141dca1bbb09c73d3c48bb0de9c69cb345f4 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:04:12 +0000 Subject: [PATCH 4/4] fix(gates): keep router ownership in the route and composition goldens The route golden was a global, sorted bag of `.route(...)` lines. A route moved from the served application router into the groove router gave an identical golden while dropping the endpoint from the app (Codex P1). Each line is now prefixed with its owning module: the first path component under src/rust/, with `.rs` removed. server.rs and server/prove.rs both map to `server`, and groove.rs maps to `groove`. Moving a route between routers now changes the golden, while splitting a module into files does not. Checked on the W0 split. Labelled routes (18 server, 2 groove) and router composition are byte-identical before (535274c) and after the server.rs split. w0.selftest: 68/68. shellcheck clean. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WS4mfQeC3N1DWjcCQJaQqw --- scripts/gates/hotspot-goldens.sh | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/scripts/gates/hotspot-goldens.sh b/scripts/gates/hotspot-goldens.sh index b02d9a04..981356a8 100755 --- a/scripts/gates/hotspot-goldens.sh +++ b/scripts/gates/hotspot-goldens.sh @@ -90,13 +90,27 @@ help_tree() { } help_tree 0 -rg --no-filename --no-line-number --glob '*.rs' '^\s*\.route\(' src/rust \ - | sed -E 's/^[[:space:]]+//; s/[[:space:]]+$//' | sort > "$out/routes.txt" || true +# Prefix each matched line with the module that owns it, so moving a +# `.route(...)` from one router to another changes the golden. The owner is +# the first path component under src/rust/ with `.rs` removed: server.rs +# and server/prove.rs are both `server`, groove.rs is `groove`. That keeps +# the golden invariant under a module split, which is what it guards. +owned() { + awk '{ + i = index($0, ":"); path = substr($0, 1, i - 1); line = substr($0, i + 1) + sub(/^src\/rust\//, "", path); sub(/\/.*$/, "", path); sub(/\.rs$/, "", path) + gsub(/^[[:space:]]+|[[:space:]]+$/, "", line) + print path ": " line + }' +} + +rg --with-filename --no-line-number --glob '*.rs' '^\s*\.route\(' src/rust \ + | owned | sort > "$out/routes.txt" || true [ -s "$out/routes.txt" ] || { echo "cannot run: no .route( lines found under src/rust" >&2; exit 2; } -rg --no-filename --no-line-number --glob '*.rs' \ +rg --with-filename --no-line-number --glob '*.rs' \ '(^|[^A-Za-z0-9_])Router::new\(|\.(merge|nest|nest_service|fallback|with_state|layer)\(' src/rust \ - | sed -E 's/^[[:space:]]+//; s/[[:space:]]+$//' | sort > "$out/router-composition.txt" || true + | owned | sort > "$out/router-composition.txt" || true [ -s "$out/router-composition.txt" ] || { echo "cannot run: no Router::new( lines found under src/rust" >&2; exit 2; } just --list > "$out/just-list.txt" 2>&1 || { echo "cannot run: just --list failed" >&2; exit 2; }