From 602b2be0ce5ebd3725df16e4e4628b6617f7b0e0 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 20 Sep 2026 19:00:12 +0200 Subject: [PATCH 1/5] PMAT-3459: the tag step cannot be reached without a clean milestone MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Closes the exit criterion #3459 is actually about. v0.68.1 was tagged 2026-09-17 15:06:29Z by an autopilot copy living OUTSIDE the repository, six minutes after #3455 merged the milestone gate; `grep -c check_milestone_cut autopilot.sh` was 0. The spec required the read and no code path that cuts a tag made it. THE GATE IS INSIDE THE FUNCTION THAT TAGS. cut_tag() calls scripts/check_milestone_cut.sh ahead of `git tag`, and there is no path through it that reaches `git tag` with the gate unsatisfied. Both non-zero codes are fail-closed and they are DIFFERENT failures, named separately: rc 0 -> MILESTONE-GATE clean at the cut; the tag is cut rc 1 -> the milestone holds open item(s): no tag, no publish rc 2+ -> the gate could not judge: no tag. Unknown is not a pass. THE GUARD IS BEHAVIOURAL, NOT A grep. "The file mentions the gate" is satisfied by a comment. scripts/check_tag_step_gated.sh EXTRACTS cut_tag() from the autopilot, runs it against a stubbed gate once per outcome, and asserts on whether a GIT-TAG appears in the transcript. Its --self-test then builds three mutants and requires each to be RED, and the real subject to be GREEN so a red subject cannot masquerade as a killed mutant: mutant 1 gate call deleted (the #3459 defect, restored) -> RED, 2 failing rows mutant 2 gate verdict discarded with `|| true` -> RED mutant 3 cut_tag() removed entirely -> ENV rc=2, never a pass That covers #3459's three required mutations: gate call removed => RED, gate exit 1 => no tag and no publish, gate exit 2 => no tag. contracts/tag-step-milestone-gate-v1.yaml (kind: pattern) lands in the same PR, per the ticket. `pv validate` and `pv lint` both PASS, and every one of its six falsification tests was RUN, not assumed -- which is how FALSIFY-TSMG-006 was caught asserting `test -x` on a file the repo deliberately keeps non-executable (guard_tree.sh invokes its whole universe as `bash scripts/...`, so the executable bit is not the property). The test was wrong, not the file; corrected to `test -f`. WIRING, with no .github/workflows edit and no operator check-in: guard_tree.sh's universe is exactly `git ls-files 'scripts/check_*.sh'`, a flat glob, so the guard runs in the guard-tree job -- and `ci / gate` reads needs.guard-tree.result, so it is gated by the required check transitively. #3459 notes that wiring a self-test literally inside the `ci` job would be a workflow edit; this route does not need one. SEC011 ("missing validation for 'd' before rm -rf") was real in the new guard and is fixed with ONE validated rmtree() used by every call site, not suppressed and not repeated per site. Gates, fresh worktree off origin/main 00e5d2dde -- all 12 rc=0: check_tag_step_gated.sh and --self-test · check_hardcoded_paths.sh --full-if-capable check_bashrs_gate.sh and --self-test · check_apr_bin_pinned.sh check_no_pipe_into_grep_q.sh · check_shell_lint_ratchet.sh · check_guards_are_wired.sh check_contract_enforcement.sh · check_contract_test_binding.sh check_sourced_libs_option_neutral.sh NOT in this PR, deliberately: V/T/MS/EPIC and AP are still 0.68.2's. Parameterising them is its own row -- mixing it here would make the gate change unreviewable, which is the lesson this ticket has been teaching all day. The hazard is stated in the PR body: the hardcoded-path ratchet does NOT match /mnt (#3592, proved with a committed two-path probe scoring +1 not +2), so AP=/mnt/... passes every gate we own and must be changed by hand with nothing to remind anyone. Refs #3080, #3445, #3455, #3592 Pmat-Ticket: PMAT-3459 Co-Authored-By: Claude Opus 5 (1M context) --- contracts/tag-step-milestone-gate-v1.yaml | 104 +++++++++++++++++++ scripts/check_tag_step_gated.sh | 121 ++++++++++++++++++++++ scripts/release/autopilot.sh | 24 ++++- 3 files changed, 247 insertions(+), 2 deletions(-) create mode 100644 contracts/tag-step-milestone-gate-v1.yaml create mode 100755 scripts/check_tag_step_gated.sh diff --git a/contracts/tag-step-milestone-gate-v1.yaml b/contracts/tag-step-milestone-gate-v1.yaml new file mode 100644 index 0000000000..8e18d272fc --- /dev/null +++ b/contracts/tag-step-milestone-gate-v1.yaml @@ -0,0 +1,104 @@ +metadata: + version: 1.0.0 + created: '2026-09-20' + author: PAIML Engineering + description: "The release train's tag step cannot be reached without a clean milestone. v0.68.1 was tagged 2026-09-17T15:06:29Z by an autopilot copy living outside the repository, six minutes after #3455 merged the milestone gate; `grep -c check_milestone_cut autopilot.sh` was 0. The spec required the read and no code path that cuts a tag made it. This contract is the property that the requirement and the mechanism are the same object: the gate call lives INSIDE cut_tag(), ahead of `git tag`, and a guard runs that function against each gate outcome and asserts on whether a tag was cut." + kind: pattern + references: + - "scripts/release/autopilot.sh — cut_tag(); the gate call precedes `git tag` inside it" + - "scripts/check_milestone_cut.sh — the gate (#3445, #3455); exit 0 clean, 1 open items, 2 cannot judge" + - "scripts/check_tag_step_gated.sh — the behavioural guard and its mutants" + - "docs/specifications/APR-RELEASE-001-train-and-build-kaizen.md — §4 T-0/T-3" + - "docs/specifications/06x-release-schedule.md — §4 steps 1 and 4" + - "contracts/release-schedule-06x-v1.yaml — milestone_settled_at_cut, the schedule-level statement of the same rule" + +five_whys: + symptom: "v0.68.1 was tagged while nothing had read its milestone, six minutes after the gate that would have read it merged." + why_1: "The script that cuts the tag was not in the repository — it was a per-train copy under /mnt/nvme-raid0/agent-wt/, so merging a gate into the repo could not reach it." + why_2: "The gate was wired into specifications and into CI, and the tag is cut by neither: the one caller that matters was the one surface nobody enumerated." + why_3: "A rule landed without its enforcer in the same change, so the enforcer's absence was invisible from the rule's side." + why_4: "The only evidence that the gate ran would have been a log line, and a missing log line reads as 'nothing to report' rather than as 'the gate did not run'." + why_5: "Nothing could refuse the tag: `git tag` was reachable from a code path that made no claim about the milestone at all." + root_cause: "The requirement lived in prose and the tag lived in an unversioned script, so there was no object in which both could be false together. The remedy is that the gate call is structurally inside the function that tags, and a guard proves by execution — not by grep — that no gate outcome other than 0 reaches `git tag`." + +equations: + tag_requires_clean_milestone: + formula: "cut_tag(v, t, mc) reaches `git tag` iff check_milestone_cut.sh(v) exited 0; rc 1 and rc 2 both die before it" + domain: "the gate's exit codes {0, 1, 2+}" + codomain: "a tag is cut, or the train stops with a STOP line naming which code refused it" + invariants: + - "rc 1 (the milestone holds open items) cuts no tag and publishes nothing" + - "rc 2 (the gate could not judge) cuts no tag — Unknown is not a pass" + - "the gate call precedes `git tag` inside one function, so removing it is a diff to that function and not to a distant caller" + + guard_is_behavioural_not_textual: + formula: "check_tag_step_gated.sh extracts cut_tag() from the autopilot, runs it against a stubbed gate once per outcome, and asserts on the presence of a GIT-TAG in the transcript" + domain: "scripts/release/autopilot.sh and three mutants of it" + codomain: "PASS only when rc 0 tags and rc 1 and rc 2 do not" + invariants: + - "a guard that greps for the gate's NAME is satisfied by a comment; this one is not" + - "a mutant with the gate call deleted is RED" + - "a mutant whose gate verdict is discarded with `|| true` is RED" + - "a subject with no cut_tag() is ENV (rc 2), never a pass" + +proof_obligations: + - id: TSMG-INV-001 + type: invariant + property: "No gate outcome other than 0 reaches `git tag`" + formal: "scripts/check_tag_step_gated.sh exit 0" + applies_to: tag_requires_clean_milestone + - id: TSMG-INV-002 + type: invariant + property: "The guard still fails on the defect it names" + formal: "scripts/check_tag_step_gated.sh --self-test exit 0 — three mutants killed and the real subject green" + applies_to: guard_is_behavioural_not_textual + - id: TSMG-INV-003 + type: invariant + property: "The autopilot that cuts the tag is in the repository and reviewed" + formal: "test -f scripts/release/autopilot.sh" + applies_to: tag_requires_clean_milestone + +falsification_tests: + - id: FALSIFY-TSMG-001 + rule: "The tag path is in the repository" + prediction: "scripts/release/autopilot.sh is a regular file" + test: "test -f scripts/release/autopilot.sh" + if_fails: "The tag is cut by a script no pull request has ever reviewed — the v0.68.1 condition, restored" + + - id: FALSIFY-TSMG-002 + rule: "The tag step names the milestone gate" + prediction: "cut_tag() in the autopilot calls scripts/check_milestone_cut.sh" + test: "awk '/^cut_tag\\(\\) \\{/,/^\\}/' scripts/release/autopilot.sh | grep -q 'check_milestone_cut\\.sh'" + if_fails: "`grep -c check_milestone_cut autopilot.sh` is 0 again, which is exactly what was true when v0.68.1 was tagged" + + - id: FALSIFY-TSMG-003 + rule: "The gate call precedes `git tag` inside cut_tag()" + prediction: "In cut_tag(), the check_milestone_cut.sh line is at a lower line number than the `git tag` line" + test: "b=$(awk '/^cut_tag\\(\\) \\{/,/^\\}/' scripts/release/autopilot.sh); g=$(printf '%s\\n' \"$b\" | grep -n 'check_milestone_cut\\.sh' | head -1 | cut -d: -f1); t=$(printf '%s\\n' \"$b\" | grep -n 'git tag -a' | head -1 | cut -d: -f1); [ -n \"$g\" ] && [ -n \"$t\" ] && [ \"$g\" -lt \"$t\" ]" + if_fails: "A gate that runs after the tag is a receipt, not a gate" + + - id: FALSIFY-TSMG-004 + rule: "No gate outcome other than 0 reaches `git tag`" + prediction: "The guard runs cut_tag() against a stubbed gate at rc 0, 1 and 2 and exits 0" + test: "bash scripts/check_tag_step_gated.sh" + if_fails: "A tag can be cut while the milestone holds open items, or while the gate could not judge at all" + + - id: FALSIFY-TSMG-005 + rule: "The guard can still fail on the defect it names" + prediction: "Three mutants — gate call deleted, gate verdict discarded, cut_tag() removed — are each RED, and the real subject is GREEN" + test: "bash scripts/check_tag_step_gated.sh --self-test" + if_fails: "The guard is theater: it would have passed the tree that tagged v0.68.1" + + - id: FALSIFY-TSMG-006 + rule: "The gate it calls is itself present and self-testing" + prediction: "scripts/check_milestone_cut.sh is a regular file — the repo invokes guards as `bash scripts/...`, so the executable bit is not the property (guard_tree.sh says so of its whole universe)" + test: "test -f scripts/check_milestone_cut.sh" + if_fails: "cut_tag() calls a script that is not there; every cut becomes rc 2 and the train stops — fail-closed, but the gate is gone" + +qa_gate: + id: F-TSMG-001 + name: "The release train's tag step cannot be reached without a clean milestone" + description: "The gate call lives inside cut_tag() ahead of `git tag`, and check_tag_step_gated.sh proves by execution that rc 1 and rc 2 both refuse the tag. guard_tree.sh's universe is `git ls-files 'scripts/check_*.sh'`, so the guard runs in the guard-tree job, which `ci / gate` reads through needs.guard-tree.result." + checks: + - "tag_requires_clean_milestone" + - "guard_is_behavioural_not_textual" diff --git a/scripts/check_tag_step_gated.sh b/scripts/check_tag_step_gated.sh new file mode 100755 index 0000000000..e72ce591cd --- /dev/null +++ b/scripts/check_tag_step_gated.sh @@ -0,0 +1,121 @@ +#!/usr/bin/env bash +# check_tag_step_gated.sh -- the release train's tag step must call +# scripts/check_milestone_cut.sh, and must not be reachable without it (PMAT-3459). +# +# THE DEFECT, measured 2026-09-17. v0.68.1 was tagged at 15:06:29Z by a per-train +# autopilot copy living OUTSIDE the repository, six minutes after #3455 merged the +# milestone gate. `grep -c check_milestone_cut autopilot.sh` was 0: the tag step read +# no milestone at all. The spec required the read; no code path that cuts a tag made it. +# +# WHY THIS IS BEHAVIOURAL AND NOT A grep. "The file mentions the gate" is satisfied by +# a comment. What must hold is that `git tag` is UNREACHABLE unless the gate returned +# 0, so this guard EXTRACTS cut_tag() from the autopilot and RUNS it against stubs, +# once per gate outcome, and asserts on whether a tag was cut: +# gate rc 0 -> tag is cut +# gate rc 1 -> no tag, no publish (the milestone holds open items) +# gate rc 2 -> no tag (Unknown; never a silent pass) +# --self-test then removes the gate call to build a MUTANT and requires this guard to +# go RED on it. A guard that cannot fail on the defect it names is theater. +# +# check_tag_step_gated.sh judge scripts/release/autopilot.sh +# check_tag_step_gated.sh --self-test case table + the gate-removed mutant +set -uo pipefail +ROOT="$(cd "$(dirname "$0")/.." && pwd)" || exit 2 + +# SEC011: never let an empty or '/' value reach `rm -rf`. One validated helper, used +# by every call site in this file, rather than the check repeated at each one. +rmtree() { case "${1:-}" in ''|/) return 0 ;; *) [ -d "$1" ] && rm -rf -- "$1" ;; esac; return 0; } +SUBJECT="$ROOT/scripts/release/autopilot.sh" + +# run_cut_tag -- extract cut_tag(), run it with stubs, print a +# transcript (SAY/DIE/GIT-TAG/GIT-PUSH lines). Returns 2 if the function is missing. +run_cut_tag() { + local ap=$1 grc=$2 d fn + d=$(mktemp -d) || return 2 + fn=$(awk '/^cut_tag\(\) \{/,/^\}/' "$ap") + [ -n "$fn" ] || { rmtree "$d"; return 2; } + mkdir -p "$d/scripts" + printf '#!/usr/bin/env bash\nexit %s\n' "$grc" > "$d/scripts/check_milestone_cut.sh" + { + printf 'set -uo pipefail\n' + printf 'REPO_ROOT=%q\nLOG=%q\n' "$d" "$d/log" + printf 'say() { printf "SAY %%s\\n" "$*"; }\n' + printf 'die() { printf "DIE %%s\\n" "$*"; exit 1; }\n' + printf 'git() { printf "GIT-%%s %%s\\n" "$(printf %%s "$1" | tr "a-z" "A-Z")" "$*"; }\n' + printf '%s\n' "$fn" + printf 'cut_tag 0.0.0 v0.0.0 deadbeef\n' + } > "$d/harness.sh" + bash "$d/harness.sh" 2>&1 + cat "$d/log" 2>/dev/null + rmtree "$d" +} + +# judge -- 0 when every gate outcome behaves; 1 otherwise. Prints rows. +judge() { + local ap=$1 out bad=0 + if ! grep -q '^cut_tag() {' "$ap"; then + printf 'FAIL %s has no cut_tag() -- the tag path moved and this guard is judging nothing\n' "$ap" >&2 + return 2 + fi + out=$(run_cut_tag "$ap" 0) || true + if grep -q 'GIT-TAG' <<< "$out"; then printf 'ok gate rc=0 -> the tag is cut\n' + else printf 'FAIL gate rc=0 -> NO tag was cut\n%s\n' "$out" >&2; bad=1; fi + + out=$(run_cut_tag "$ap" 1) || true + if grep -q 'GIT-TAG' <<< "$out"; then + printf 'FAIL gate rc=1 (milestone holds open items) -> A TAG WAS CUT ANYWAY\n%s\n' "$out" >&2; bad=1 + else printf 'ok gate rc=1 -> no tag, no publish\n'; fi + + out=$(run_cut_tag "$ap" 2) || true + if grep -q 'GIT-TAG' <<< "$out"; then + printf 'FAIL gate rc=2 (Unknown) -> A TAG WAS CUT ANYWAY\n%s\n' "$out" >&2; bad=1 + else printf 'ok gate rc=2 (Unknown) -> no tag\n'; fi + return "$bad" +} + +if [ "${1:-}" = "--self-test" ]; then + echo "=== the tag-gate guard must still turn RED (mutants) ===" + d=$(mktemp -d) || exit 2 + trap 'rmtree "${d:-}"' EXIT + bad=0 + ok() { printf 'ok %s\n' "$*"; } + nok() { printf 'FAIL %s\n' "$*" >&2; bad=1; } + + # M1: the gate call deleted -- the #3459 defect exactly, restored. + sed '/check_milestone_cut\.sh/d' "$SUBJECT" > "$d/m1.sh" + if judge "$d/m1.sh" > "$d/m1.out" 2>&1; then + nok "MUTANT 1 (gate call deleted) PASSED -- this guard cannot see its own defect" + else + ok "mutant 1: gate call deleted -> RED ($(grep -c '^FAIL' "$d/m1.out") failing row(s))" + fi + + # M2: the gate runs but its verdict is discarded (`|| true`) -- absence-as-consent. + sed 's#\(bash "$REPO_ROOT/scripts/check_milestone_cut.sh" "$v" >> "$LOG" 2>&1\) || rc=$?#\1 || true#' "$SUBJECT" > "$d/m2.sh" + if ! grep -q '|| true' "$d/m2.sh"; then + nok "MUTANT 2 could not be built -- the gate-call line did not match; this self-test is vacuous" + elif judge "$d/m2.sh" > "$d/m2.out" 2>&1; then + nok "MUTANT 2 (verdict discarded) PASSED -- a gate whose result is thrown away reads as gated" + else + ok "mutant 2: gate verdict discarded -> RED" + fi + + # M3: cut_tag() removed entirely -> ENV (2), never a pass. + awk '/^cut_tag\(\) \{/,/^\}/ {next} {print}' "$SUBJECT" > "$d/m3.sh" + judge "$d/m3.sh" > "$d/m3.out" 2>&1; rc=$? + [ "$rc" -eq 2 ] && ok "mutant 3: cut_tag() removed -> ENV rc=2, not a pass" \ + || nok "mutant 3: cut_tag() removed gave rc=$rc, wanted 2" + + # and the real subject must be GREEN, or a red subject masquerades as a killed mutant + if judge "$SUBJECT" > "$d/real.out" 2>&1; then + ok "the real subject is GREEN, so the REDs above are the mutants'" + else + nok "the real subject is itself RED -- the mutations prove nothing"; cat "$d/real.out" >&2 + fi + [ "$bad" -eq 0 ] && { echo "SELF-TEST PASSED"; exit 0; } + echo "SELF-TEST FAILED" >&2; exit 1 +fi + +echo "=== the tag step cannot be reached without the milestone gate (check_tag_step_gated.sh) ===" +judge "$SUBJECT"; rc=$? +[ "$rc" -eq 0 ] && echo "PASS" || echo "FAIL: the tag step is reachable without a clean milestone (rc=$rc)" >&2 +exit "$rc" diff --git a/scripts/release/autopilot.sh b/scripts/release/autopilot.sh index 9a89ba36c3..44ea8d7881 100755 --- a/scripts/release/autopilot.sh +++ b/scripts/release/autopilot.sh @@ -107,11 +107,31 @@ if run_step dogfood; then fi # 3. tag + release (binary-release.yml fires on release: published, from the TAG's workflow file) +# cut_tag -- PMAT-3459. The milestone gate lives INSIDE the +# function that tags, ahead of `git tag`, so the tag cannot be cut without it: there is +# no path through cut_tag() that reaches `git tag` with the gate unsatisfied. v0.68.1 +# was tagged 15:06:29Z by a copy of this script that read no milestone at all, six +# minutes after #3455 merged the gate (`grep -c check_milestone_cut autopilot.sh` = 0). +# Fail-closed on BOTH non-zero codes, and they are different failures: +# 1 = the milestone holds open item(s) -> no tag, no publish +# 2 = the gate could not judge (Unknown) -> no tag. Never a silent pass. +# scripts/check_tag_step_gated.sh runs this function against stubs and requires each +# of those three paths, plus a gate-call-removed MUTANT, to behave as stated. +cut_tag() { + local v=$1 t=$2 mc=$3 rc=0 + bash "$REPO_ROOT/scripts/check_milestone_cut.sh" "$v" >> "$LOG" 2>&1 || rc=$? + case "$rc" in + 0) say "MILESTONE-GATE $v clean at the cut (check_milestone_cut.sh rc=0)" ;; + 1) die "milestone $v still holds open item(s) -- no tag, no publish (check_milestone_cut.sh rc=1)" ;; + *) die "milestone $v could not be judged (check_milestone_cut.sh rc=$rc) -- no tag; Unknown is not a pass" ;; + esac + git tag -a "$t" -m "aprender $t" "$mc" >> "$LOG" 2>&1 || die "tag failed" + git push origin "$t" >> "$LOG" 2>&1 || die "tag push failed" +} if run_step tag; then git rev-parse -q --verify "refs/tags/$T" > /dev/null && die "tag $T already exists locally" [ -f "$AP/release_notes.md" ] || die "no $AP/release_notes.md (prepare_bump.sh writes it from CHANGELOG [$V])" - git tag -a "$T" -m "aprender $T" "$MC" >> "$LOG" 2>&1 || die "tag failed" - git push origin "$T" >> "$LOG" 2>&1 || die "tag push failed" + cut_tag "$V" "$T" "$MC" say "TAGGED $T at $MC" gh release create "$T" --repo $REPO --verify-tag --title "aprender $V" --notes-file "$AP/release_notes.md" >> "$LOG" 2>&1 || die "gh release create failed" say "RELEASED $(gh release view "$T" --repo $REPO --json url -q .url)" From d26b67093a1f723362103a256a029aea720ab83a Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 20 Sep 2026 19:45:29 +0200 Subject: [PATCH 2/5] =?UTF-8?q?PMAT-3459:=20give=20the=20tag-gate=20self-t?= =?UTF-8?q?est=20a=20caller=20=E2=80=94=20it=20was=20running=20nowhere?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Found while answering #3459's exit criterion 4. The self-test added in the previous commit was DISCOVERED BY NOTHING and therefore ran in no job at all: before: PASS scripts/check_tag_step_gated.sh [run] after: PASS scripts/check_tag_step_gated.sh [self-test] PASS scripts/check_tag_step_gated.sh [run] guard_tree.sh decides a guard "advertises --self-test" by looking for the literal substring `self-test` in that guard's OWN `--help` output (guard_tree.sh:47, advertises_self_test). check_tag_step_gated.sh had no --help handler, so it got one row instead of two and its three mutants were never executed by CI. The mutation proof existed and nothing ran it -- a facility with a self-test and no caller, in the commit that added the self-test. It is the same class this ticket keeps producing, and it was invisible to reading: the guard works, its self-test works, and the wiring between them did not exist. The fix is a --help handler printing the header comment, which is the idiom the rest of the tree uses (ci_run_explicit_test_commands.sh:147 and others). Verified by running guard_tree.sh --no-cargo, not by reading it: 66 checks, 0 failed, with both rows present. Refs #3080, #3459 Pmat-Ticket: PMAT-3459 Co-Authored-By: Claude Opus 5 (1M context) --- scripts/check_tag_step_gated.sh | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/scripts/check_tag_step_gated.sh b/scripts/check_tag_step_gated.sh index e72ce591cd..4545b2f011 100755 --- a/scripts/check_tag_step_gated.sh +++ b/scripts/check_tag_step_gated.sh @@ -73,6 +73,13 @@ judge() { return "$bad" } +# guard_tree.sh decides a guard "advertises --self-test" by looking for the literal +# substring `self-test` in its OWN `--help` output (guard_tree.sh:47, advertises_self_test). +# Without this handler the self-test below is discovered by nothing and runs nowhere -- +# a facility with a self-test and no caller. With it, guard_tree gives this guard TWO +# rows, `[self-test]` and `[run]`, inside the guard-tree job. +case "${1:-}" in -h|--help) sed -n '2,25p' "$0" | sed 's/^# \{0,1\}//'; exit 0 ;; esac + if [ "${1:-}" = "--self-test" ]; then echo "=== the tag-gate guard must still turn RED (mutants) ===" d=$(mktemp -d) || exit 2 From e5dbde86a0d9a6ade527e379d2c79766ecf5dcf3 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 20 Sep 2026 23:03:40 +0200 Subject: [PATCH 3/5] =?UTF-8?q?PMAT-3459:=20the=20contract's=20formals=20c?= =?UTF-8?q?arry=20=CE=A3=20symbols;=20census,=20graph=20and=20README=20reg?= =?UTF-8?q?enerated?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes the three REAL reds on this PR's first run (the rest were env: gx10 ENOSPC and an intel "dep info ... No such file" mid-build, #2822 class). 1. sigma gate (shard 3/3, lint_passes_on_real_contracts): two errors. - `proof_obligations[1].formal` carried an em-dash, which Σ does not declare. - formal_prose rose 1464 -> 1467: three `formal:` entries with no Σ symbol, against a shrink-only baseline. `prose: true` exempts the glyph check but NOT the ratchet (sigma_symbols.rs:107 counts before :110 checks the flag), so the fix is real formals, not a marker: ∀ rc ∈ {1, 2}: cut_tag(v, t, mc) with gate(v) = rc ⇒ ¬ tagged(t) ∧ gate(v) = 0 ⇒ tagged(t) ∀ m ∈ {gate_call_deleted, verdict_discarded, cut_tag_removed}: guard(m) ≠ 0 ∧ guard(subject) = 0 scripts/release/autopilot.sh ∈ tracked(main) ∧ cut_tag ∈ autopilot.sh The shell commands that were there belong in falsification_tests, where they already are. This is a better contract, not just a passing one. My local `pv lint` had reported "not armed: sigma" and I read that as clean. CI's test arms it. The CLAUDE.md pre-push checklist names `cargo test -p aprender-contracts --lib`, which reproduces CI exactly; I did not run it before the first push. Run now: 1666 passed, 0 failed. 2. the_tracked_repo_graph_is_fresh (shard 1/3): contracts/contracts.nt lacked the new contract's 5 triples. `pv extract contracts` with the pinned binary. 3. README claims must match measurement (guard-cargo): contracts/census.json said 1799, HEAD carries 1800. `pv census contracts --format json > contracts/census.json` (the Makefile's form -- bare `pv census` prints and writes nothing) and `scripts/readme_sync.sh --write`, CONTRACT_COUNT now 1800. All three derivatives produced with `. scripts/pv_bin.sh` (pv 0.68.2 from this tree's target dir), never a bare pv. Each of the three failing CI tests reproduced locally and re-run green. Refs #3080, #3459, #3569 Pmat-Ticket: PMAT-3459 Co-Authored-By: Claude Opus 5 (1M context) --- README.md | 4 ++-- contracts/census.json | 10 +++++----- contracts/contracts.nt | 5 +++++ contracts/tag-step-milestone-gate-v1.yaml | 6 +++--- 4 files changed, 15 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index b3f7f2d721..182bfb024b 100644 --- a/README.md +++ b/README.md @@ -41,7 +41,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift. | Metric | Count | Source of truth | |-------:|------:|---| | Workspace crates | **79** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) | -| Provable contracts | **1799** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | +| Provable contracts | **1800** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | | CLI commands | **110** CLI commands | `apr --help` | | Book CLI chapters | **112** chapters | `ls book/src/cli/*.md` | | Book lib chapters | **71** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) | @@ -262,7 +262,7 @@ falsification_tests: prediction: apr validate bad-model.apr exits non-zero ``` -The tree carries 1799 contracts across inference, training, quantization, attention, FFN, +The tree carries 1800 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates diff --git a/contracts/census.json b/contracts/census.json index 3009dd4060..0d342c742c 100644 --- a/contracts/census.json +++ b/contracts/census.json @@ -1,8 +1,8 @@ { "schema": "ont.paiml.dev/census/v1alpha1", "git_sha": null, - "n_files": 1799, - "n_parsed": 1799, + "n_files": 1800, + "n_parsed": 1800, "n_parse_errors": 0, "parse_errors": [], "quarantined_n": 0, @@ -12,7 +12,7 @@ "kernel": 362, "model-family": 28, "model-family-variant": 1, - "pattern": 86, + "pattern": 87, "pretraining-corpus": 2, "registry": 519, "schema": 766, @@ -25,11 +25,11 @@ "pv-contract": 1 }, "by_anchoring": { - "unanchored": 1796, + "unanchored": 1797, "class": 2, "instance": 1 }, - "id_set_sha256": "a547cd5527caeffade2d8260d25421f26506df1c1d8f00f5eb7b9cde12e8107e", + "id_set_sha256": "39eb736d97392dd28dae8cb4e36cc154b7728522b8f6ca4de4508f4abd20e5e3", "declared_external": [ { "name": "provable-contracts", diff --git a/contracts/contracts.nt b/contracts/contracts.nt index 16022a5f13..f308e93127 100644 --- a/contracts/contracts.nt +++ b/contracts/contracts.nt @@ -9003,6 +9003,11 @@ . "contracts/swiglu-kernel-v1.yaml"^^ . "swiglu-kernel-v1"^^ . + . + . + "contracts/tag-step-milestone-gate-v1.yaml"^^ . + "tag-step-milestone-gate-v1"^^ . + "pattern"^^ . . . "contracts/forjar/task-pipeline-v1.yaml"^^ . diff --git a/contracts/tag-step-milestone-gate-v1.yaml b/contracts/tag-step-milestone-gate-v1.yaml index 8e18d272fc..a887aeb030 100644 --- a/contracts/tag-step-milestone-gate-v1.yaml +++ b/contracts/tag-step-milestone-gate-v1.yaml @@ -45,17 +45,17 @@ proof_obligations: - id: TSMG-INV-001 type: invariant property: "No gate outcome other than 0 reaches `git tag`" - formal: "scripts/check_tag_step_gated.sh exit 0" + formal: "∀ rc ∈ {1, 2}: cut_tag(v, t, mc) with gate(v) = rc ⇒ ¬ tagged(t) ∧ gate(v) = 0 ⇒ tagged(t)" applies_to: tag_requires_clean_milestone - id: TSMG-INV-002 type: invariant property: "The guard still fails on the defect it names" - formal: "scripts/check_tag_step_gated.sh --self-test exit 0 — three mutants killed and the real subject green" + formal: "∀ m ∈ {gate_call_deleted, verdict_discarded, cut_tag_removed}: guard(m) ≠ 0 ∧ guard(subject) = 0" applies_to: guard_is_behavioural_not_textual - id: TSMG-INV-003 type: invariant property: "The autopilot that cuts the tag is in the repository and reviewed" - formal: "test -f scripts/release/autopilot.sh" + formal: "scripts/release/autopilot.sh ∈ tracked(main) ∧ cut_tag ∈ autopilot.sh" applies_to: tag_requires_clean_milestone falsification_tests: From b0e4be8e8072af119f936cdb903d37e1a78384c8 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 20 Sep 2026 23:22:09 +0200 Subject: [PATCH 4/5] PMAT-3459: regenerate census, graph and README from the merged tree #3617 went CONFLICTING after #3614 landed: #3581 and this branch each regenerated contracts/census.json, contracts/contracts.nt and README.md for their own contract additions, and git saw two edits to the same generated bytes. Resolved the only correct way for a derived file: merge origin/main (taking either side on the conflict, since it is overwritten next), then REGENERATE all three from the merged tree with the pinned pv (scripts/pv_bin.sh, pv 0.68.2) -- never by hand. A hand-merged contracts.nt is a derived file no derivation produced. Only census.json hard-conflicted. contracts.nt and README.md would have auto-merged line-wise, which is the worse case: combined derived output that happens to apply cleanly. Regenerated anyway and compared: contracts.nt is byte-identical to what git produced (15605 lines both ways) -- verified, not assumed. census 1800 -> 1801 (main's one plus this branch's one); README CONTRACT_COUNT 1801. cargo test -p aprender-contracts --lib 1666 passed, 0 failed the_tracked_repo_graph_is_fresh ok check_readme_claims.sh rc=0 check_tag_step_gated.sh --self-test rc=0 check_pr_ont_delta.sh on the merged file set PASS Refs #3080, #3459, #3569 Pmat-Ticket: PMAT-3459 Co-Authored-By: Claude Opus 5 (1M context) --- README.md | 4 ++-- contracts/census.json | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 182bfb024b..7980187815 100644 --- a/README.md +++ b/README.md @@ -41,7 +41,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift. | Metric | Count | Source of truth | |-------:|------:|---| | Workspace crates | **79** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) | -| Provable contracts | **1800** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | +| Provable contracts | **1801** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) | | CLI commands | **110** CLI commands | `apr --help` | | Book CLI chapters | **112** chapters | `ls book/src/cli/*.md` | | Book lib chapters | **71** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) | @@ -262,7 +262,7 @@ falsification_tests: prediction: apr validate bad-model.apr exits non-zero ``` -The tree carries 1800 contracts across inference, training, quantization, attention, FFN, +The tree carries 1801 contracts across inference, training, quantization, attention, FFN, tokenization, model formats, CLI safety — and this README itself. ## Migration from old crates diff --git a/contracts/census.json b/contracts/census.json index d6286d1147..016e5b245e 100644 --- a/contracts/census.json +++ b/contracts/census.json @@ -1,8 +1,8 @@ { "schema": "ont.paiml.dev/census/v1alpha1", "git_sha": null, - "n_files": 1800, - "n_parsed": 1800, + "n_files": 1801, + "n_parsed": 1801, "n_parse_errors": 0, "parse_errors": [], "quarantined_n": 0, @@ -12,7 +12,7 @@ "kernel": 363, "model-family": 28, "model-family-variant": 1, - "pattern": 86, + "pattern": 87, "pretraining-corpus": 2, "registry": 519, "schema": 766, @@ -25,11 +25,11 @@ "pv-contract": 1 }, "by_anchoring": { - "unanchored": 1797, + "unanchored": 1798, "class": 2, "instance": 1 }, - "id_set_sha256": "51cfc1e6cf27aa5cb6d9345e918a19863f13aa4728b4eba15bfa69bc6002bfb1", + "id_set_sha256": "e624814d2c82e8a53ab24faac0b5281c0dad15618d9f14e970c740c8391cb712", "declared_external": [ { "name": "provable-contracts", From 4a62af449128965f734ea9e0014b95d9693c0c37 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 21 Sep 2026 00:41:48 +0200 Subject: [PATCH 5/5] =?UTF-8?q?PMAT-3459:=20AD-04=20quorum=20receipt=20?= =?UTF-8?q?=E2=80=94=203/3=20PASS,=20three=20independent=20lanes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/audits/quorum-PMAT-3459.json from quorum-review.sh --base origin/main --pr 3617 --author-model claude-opus-5, executor agy, width 3, judged at head b0e4be8e8: lane 1 gemini-3.1-pro-high PASS 4 findings (all confirmations, 2 cited / 2 asserted) lane 2 gemini-3.8-flash-high PASS lane 3 gemini-3.7-flash-high PASS dissent: none Independence inspected, not assumed: every lane file (lane-{1,2,3}.{json,err}) has zero references to a sibling lane, to $WORK or to the .lanes/ dir -- the recorded failure where a 3/3 was one vote read through $WORK. Three models, none in the author's family. This receipt was owed before arming and was not there: the PR was armed through arm_pr_automerge.sh, which asserts guard-tree on the head and by its own header says nothing about review. Pulled from the merge queue, judged, re-armed on this receipt. The ticket text the lanes judged against came from #3461's registration (PMAT-3459's fragment lives only on that unmerged branch); it was placed in the working tree for `pmat work status` and never staged, so the diff the lanes judged is base...HEAD unchanged -- the six files this PR carries. Pmat-Ticket: PMAT-3459 Co-Authored-By: Claude Opus 5 (1M context) --- docs/audits/quorum-PMAT-3459.json | 150 ++++++++++++++++++++++++++++++ 1 file changed, 150 insertions(+) create mode 100644 docs/audits/quorum-PMAT-3459.json diff --git a/docs/audits/quorum-PMAT-3459.json b/docs/audits/quorum-PMAT-3459.json new file mode 100644 index 0000000000..5d61f5cae0 --- /dev/null +++ b/docs/audits/quorum-PMAT-3459.json @@ -0,0 +1,150 @@ +{ + "ticket": "PMAT-3459", + "base": "origin/main", + "base_resolved": "origin/main", + "base_note": "no origin/origin/main exists; judged against the local ref", + "head": "b0e4be8e8072af119f936cdb903d37e1a78384c8", + "diff_sha256": "0a4c6913df7af9280ca94772bbd16ca406dd96821115944954ee2457069dc634", + "width": 3, + "executor": "agy", + "prompt_mode": "inline", + "prompt_bytes": 22768, + "author": { + "model": "claude-opus-5", + "family": "claude", + "source": "flag" + }, + "agreed": true, + "lanes": [ + { + "lane": 1, + "status": "SUCCESS", + "verdict": "PASS", + "summary": "The diff cleanly implements PMAT-3459. It modifies the tag step in the release autopilot, enclosing it in `cut_tag()`, which checks `check_milestone_cut.sh` before running `git tag`. This fail-closed pattern correctly halts the release if open items remain (rc=1) or if the milestone cannot be judged (rc=2). The guard script (`check_tag_step_gated.sh`) properly verifies this by executing the function against stubbed gate scripts and ensuring no tag is cut unless the exit code is 0. Its `--self-test` checks mutations (deleting the gate call, discarding the gate verdict, and removing the function entirely), ensuring that the test fails on these regressions. The provable contracts and counts were correctly updated. No defects were found.", + "findings": [ + { + "claim": "The tag operation is extracted into `cut_tag` and successfully calls `check_milestone_cut.sh`.", + "file": "scripts/release/autopilot.sh", + "grounding": "cited", + "line": 122 + }, + { + "claim": "The `--self-test` correctly checks the mutant where the gate verdict is discarded (`|| true`), verifying that the behavioural guard will go RED if the defect is restored.", + "file": "scripts/check_tag_step_gated.sh", + "grounding": "asserted", + "line": 98 + }, + { + "claim": "The count in `census.json` and `README.md` correctly incremented to 1801 to account for the new pattern contract.", + "file": "contracts/census.json", + "grounding": "cited", + "line": 4 + }, + { + "claim": "The test correctly checks that `check_milestone_cut.sh` appears before `git tag -a` inside `cut_tag()`, ensuring it operates as a gate rather than a receipt.", + "file": "contracts/tag-step-milestone-gate-v1.yaml", + "grounding": "asserted", + "line": 63 + } + ], + "raw_bytes": 5540, + "err_bytes": 0, + "envelope_status": "SUCCESS", + "verdict_source": "structured_output", + "grounding_check": "parity", + "model": "gemini-3.1-pro-high", + "model_measured": "gemini-3.1-pro-high", + "model_source": "measured", + "family": "gemini" + }, + { + "lane": 2, + "status": "SUCCESS", + "verdict": "PASS", + "summary": "Review of diff for PMAT-3459 (origin/main...HEAD) in /mnt/nvme-raid0/agent-wt/pmat3459-milestone:\n\n1. **Ticket & Diff Conformance**:\n - `scripts/release/autopilot.sh`: Encapsulates the tag cut in `cut_tag()`, ensuring `scripts/check_milestone_cut.sh \"$v\"` is executed strictly prior to `git tag` and `git push`. Fails closed on rc 1 (milestone holds open items) and rc 2+ (judge failure/unknown), ensuring `git tag` is unreachable without a clean milestone (rc 0).\n - `scripts/check_tag_step_gated.sh`: Behavioural guard testing `cut_tag()` across gate return codes {0, 1, 2}. Validates `--self-test` across 3 distinct mutants (gate call removed, verdict discarded with `|| true`, `cut_tag()` missing). Exposes `--help` containing `self-test` so `scripts/guard_tree.sh` discovers and runs both `[self-test]` and `[run]` rows.\n - `contracts/tag-step-milestone-gate-v1.yaml`: Formal `kind: pattern` contract defining invariants TSMG-INV-001 through 003 and falsification tests FALSIFY-TSMG-001 through 006.\n - `README.md`, `contracts/census.json`, `contracts/contracts.nt`: Updated census count and RDF graph from 1800 to 1801 contracts.\n\n2. **Measured Verification**:\n - `bash scripts/check_tag_step_gated.sh`: PASS (rc=0)\n - `bash scripts/check_tag_step_gated.sh --self-test`: PASS (rc=0; 3 mutants killed)\n - FALSIFY-TSMG-001 through 006: all PASS\n - `bash scripts/check_readme_claims.sh`: PASS\n - `bash scripts/check_bashrs_gate.sh`: PASS (354 files linted, 0 errors)\n - `bash scripts/check_hardcoded_paths.sh`: PASS (1854 contract files scanned, 0 machine-specific paths)\n - `bash scripts/check_contract_enforcement.sh`: PASS\n - `bash scripts/check_contract_test_binding.sh`: PASS\n - `shellcheck -S error` and `bash -n` on modified/added shell scripts: PASS\n - `scripts/guard_tree.sh`: both `[self-test]` and `[run]` executed and PASS.\n\nNo weakened gates, unbacked receipt claims, or unauthorized changes found. Refutation attempts failed. Verdict: PASS.", + "findings": [], + "raw_bytes": 6365, + "err_bytes": 0, + "envelope_status": "SUCCESS", + "verdict_source": "structured_output", + "grounding_check": "parity", + "model": "gemini-3.8-flash-high", + "model_measured": "gemini-3.8-flash-high", + "model_source": "measured", + "family": "gemini" + }, + { + "lane": 3, + "status": "SUCCESS", + "verdict": "PASS", + "summary": "Review of diff for PMAT-3459 against ticket 'release train: move the release autopilot\\'s tag path into the repo; tag step calls check_milestone_cut.sh (#3459)':\n\n1. **Ticket & Diff Conformance**:\n - `scripts/release/autopilot.sh`: Introduced `cut_tag()`, ensuring `check_milestone_cut.sh` is invoked before `git tag` and failing closed on both rc 1 (open items) and rc 2+ (judge failure/unknown).\n - `scripts/check_tag_step_gated.sh`: Behavioural guard extracting `cut_tag()` from `autopilot.sh` and verifying gate behavior across all return codes (rc 0 tags; rc 1 and 2 die without tagging), with `--self-test` validating 3 distinct mutants (gate call deleted, verdict discarded with `|| true`, `cut_tag()` removed).\n - `contracts/tag-step-milestone-gate-v1.yaml`: Formal contract pattern specifying the tag-step milestone gate invariants and 6 falsification tests (FALSIFY-TSMG-001 through 006).\n - `README.md`, `contracts/census.json`, `contracts/contracts.nt`: Updated census and graph reflecting the addition of the new contract (1800 -> 1801).\n\n2. **Verification & Falsification**:\n - `bash scripts/check_tag_step_gated.sh`: PASS (rc=0)\n - `bash scripts/check_tag_step_gated.sh --self-test`: PASS (rc=0, 3 mutants killed)\n - All 6 falsification tests from `contracts/tag-step-milestone-gate-v1.yaml`: PASS\n - `bash scripts/check_milestone_cut.sh --self-test`: PASS (25 cases)\n - `bash scripts/check_readme_claims.sh`: PASS\n - `bash scripts/check_bashrs_gate.sh` & `check_shell_lint_ratchet.sh`: PASS\n - `bash scripts/check_guards_are_wired.sh`: PASS\n - `cargo test -p aprender-contracts --lib -- census`: PASS\n - `shellcheck -S error` and `bash -n` on modified/added shell scripts: PASS\n\nNo weakened gates, unbacked claims, or unauthorized changes found. Verdict: PASS.", + "findings": [], + "raw_bytes": 5880, + "err_bytes": 0, + "envelope_status": "SUCCESS", + "verdict_source": "structured_output", + "grounding_check": "parity", + "model": "gemini-3.7-flash-high", + "model_measured": "gemini-3.7-flash-high", + "model_source": "measured", + "family": "gemini" + } + ], + "dissent": [], + "dedup": [ + { + "file": "contracts/census.json", + "line": 4, + "lanes_agreeing": [ + 1 + ], + "claims": [ + "The count in `census.json` and `README.md` correctly incremented to 1801 to account for the new pattern contract." + ] + }, + { + "file": "contracts/tag-step-milestone-gate-v1.yaml", + "line": 63, + "lanes_agreeing": [ + 1 + ], + "claims": [ + "The test correctly checks that `check_milestone_cut.sh` appears before `git tag -a` inside `cut_tag()`, ensuring it operates as a gate rather than a receipt." + ] + }, + { + "file": "scripts/check_tag_step_gated.sh", + "line": 98, + "lanes_agreeing": [ + 1 + ], + "claims": [ + "The `--self-test` correctly checks the mutant where the gate verdict is discarded (`|| true`), verifying that the behavioural guard will go RED if the defect is restored." + ] + }, + { + "file": "scripts/release/autopilot.sh", + "line": 122, + "lanes_agreeing": [ + 1 + ], + "claims": [ + "The tag operation is extracted into `cut_tag` and successfully calls `check_milestone_cut.sh`." + ] + } + ], + "uncovered": [], + "coverage_source": "lanes", + "partial": false, + "partial_reasons": [], + "auto_merge": { + "checked": true, + "was_armed": false, + "disarmed": false, + "note": "auto-merge not armed" + }, + "lint": { + "ok": true, + "output": "receipt complete: kind=artifact lanes=3 author=claude-opus-5/claude" + } +}