feat(abi): verdict record names its support; Sound only from a prover re-check (HYP-01, PR A)

.claude/CLAUDE.md

@@ -43,7 +43,7 @@ Hypatia                       # 133 Elixir modules total
 
 ## Key Commands
 
-`just` is the primary entry point (39 recipes; `CONTRIBUTING.md` treats it as canonical):
+`just` is the primary entry point (43 recipes, `just --summary | wc -w`; `CONTRIBUTING.md` treats it as canonical):
 
 ```bash
 just --list           # every recipe
@@ -172,6 +172,7 @@ Training pipeline reads outcomes/*.jsonl for ESN (confidence time series) and pa
 | `REST.idr` | REST endpoint definitions (18 endpoints, 6 groups) |
 | `FFI.idr` | GADT constructors for all C ABI functions + ffiReturnsApiResponse proof |
 | `RuleEngine.idr` | Rule-evaluation types |
+| `Verdict.idr` | Verdict records (HYP-01): support = Pattern / Observed n / Mechanical re-check; `Sound` only from a confirming re-check. Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) |
 
 **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager).
 The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles** — that is the

.github/workflows/verify-proofs.yml

@@ -22,6 +22,12 @@ on:
     - src/abi/**
     - src/Hypatia/ABI/**
     - verify/**
+    - tests/accept/**
+    - tests/reject/**
+    - scripts/check-verdicts.sh
+    - scripts/recheck-lean-hole.sh
+    - scripts/fetch-siblings.sh
+    - scripts/check-sibling-citations.sh
     branches:
     - main
   pull_request:
@@ -40,6 +46,12 @@ on:
     - src/abi/**
     - src/Hypatia/ABI/**
     - verify/**
+    - tests/accept/**
+    - tests/reject/**
+    - scripts/check-verdicts.sh
+    - scripts/recheck-lean-hole.sh
+    - scripts/fetch-siblings.sh
+    - scripts/check-sibling-citations.sh
     branches:
     - main
   schedule:
@@ -168,6 +180,13 @@ jobs:
       - name: Build the verify package (PipelineState, Verify.Fuel)
         run: idris2 --build verify/hypatia-verify.ipkg
 
+      # HYP-01: Verdict.idr claims a `Sound` verdict is constructible only
+      # from a confirming prover re-check. The typechecker is the falsifier:
+      # tests/accept/ must be accepted, and every tests/reject/ module must be
+      # refused at `invalid` with the diagnostic its `-- EXPECT:` line names.
+      - name: Verdict accept/reject fixtures (HYP-01)
+        run: bash scripts/check-verdicts.sh
+
       - name: Summary
         if: always()
         run: |
@@ -228,6 +247,13 @@ jobs:
           lake --version
           lake build
 
+      # HYP-01 positive control: the SoundVerdict in
+      # tests/accept/LeanHoleRecheckSound.idr records digests of a Lean run.
+      # Re-run Lean on the fixture from the repository root (where the
+      # control's paths are relative to) and require both digests to match.
+      - name: Re-check the Lean proof-hole fixture against the HYP-01 control
+        run: bash scripts/recheck-lean-hole.sh
+
       - name: Summary
         if: always()
         run: |
@@ -331,3 +357,23 @@ jobs:
 
       - name: No un-annotated trusted-base markers
         run: bash scripts/check-trusted-base.sh
+
+  # Sibling proof repos are consumed by pinned commit, never re-declared. The
+  # Idris2 records that follow them are transcriptions (correspondence
+  # ASSUMED); this job keeps the citation itself honest: the pin fetches,
+  # the cited definitions exist at it, and the citing header names it.
+  sibling-citations:
+    name: sibling citations at pin
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v7.0.1
+
+      - name: Fetch pinned siblings
+        run: bash scripts/fetch-siblings.sh
+
+      - name: Every citation resolves at its pin
+        run: bash scripts/check-sibling-citations.sh

Justfile

@@ -75,6 +75,19 @@ abi-gen:
 compile-verify:
     cd verify && idris2 --build hypatia-verify.ipkg
 
+# HYP-01 verdict gate: ABI builds, tests/accept accepted, tests/reject refused for the stated reason
+check-verdicts:
+    bash scripts/check-verdicts.sh
+
+# Re-run Lean on the proof-hole fixture; digests must match the HYP-01 positive control
+recheck-lean-hole:
+    bash scripts/recheck-lean-hole.sh
+
+# Fetch pinned sibling proof repos, then check every citation resolves at its pin
+check-siblings:
+    bash scripts/fetch-siblings.sh
+    bash scripts/check-sibling-citations.sh
+
 # Model-check TLA+ specifications (e.g. H8 Kin-gate atomicity)
 verify-tlaplus:
     #!/usr/bin/env bash

scripts/check-proof-status.sh

@@ -58,9 +58,12 @@ extract() {
   awk '
     function emit_row(b,   spans, n, i, span, file, first) {
       if (b ~ /line-through/ || b ~ /RETIRED/) return
+      # split() on the OPENING delimiter leaves exactly one span per piece, so
+      # every piece is visited. Until 2026-10-14 this loop stepped by 2 and
+      # silently checked every second identifier only (7 of 16 on main).
       n = split(b, spans, /`\+/)
       file = ""
-      for (i = 2; i <= n; i += 2) {
+      for (i = 2; i <= n; i++) {
         span = spans[i]
         sub(/\+`.*/, "", span)   # cut at the closing +`
         first = span
@@ -90,7 +93,7 @@ extract() {
       body = s
       sub(/^[^\n]*\n/, "", body)
       n = split(body, spans, /`\+/)
-      for (i = 2; i <= n; i += 2) {
+      for (i = 2; i <= n; i++) {
         span = spans[i]
         sub(/\+`.*/, "", span)   # cut at the closing +`
         first = span

scripts/check-sibling-citations.sh

@@ -0,0 +1,75 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-sibling-citations.sh — keep hypatia's citations of sibling proofs
+# honest.  Run scripts/fetch-siblings.sh first.
+#
+# A module that transcribes a sibling's definitions names the sibling, the
+# commit, the file and the definitions in its header.  This script checks,
+# for every row of the table below:
+#
+#   1. the citing module names the commit that scripts/fetch-siblings.sh
+#      fetched (prose and pin agree);
+#   2. the cited file exists in the sibling at that commit;
+#   3. the cited definition is declared in that file (a declaration, not
+#      merely a mention: `record N`, `data N`, or `N :` at the start of a
+#      line, after indentation);
+#   4. the citing module's header mentions the definition by name.
+#
+# What this does NOT check: that the transcription corresponds to the Agda
+# definition.  That correspondence stays ASSUMED until a checked one exists.
+#
+# Usage: scripts/check-sibling-citations.sh
+# Exit:  0 = every citation resolves at its pin; 1 = a citation is stale;
+#        2 = a sibling has not been fetched.
+
+set -uo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." || exit 2
+deps=_build/dependencies
+
+# citing module | sibling | file in sibling | definition
+citations=(
+  "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|Warrant"
+  "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|Epi"
+  "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|SoundWarrant"
+  "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Warrant.agda|sound-epi"
+  "src/Hypatia/ABI/Verdict.idr|epistemic-types|src/EpistemicTypes/Applications/RapidNJSkip.agda|no-receipt-reflection"
+)
+
+failures=0
+checked=0
+for row in "${citations[@]}"; do
+  IFS='|' read -r citer sibling file def <<<"$row"
+  dir="$deps/$sibling"
+  if [[ ! -d "$dir/.git" ]]; then
+    echo "::error::$sibling not fetched; run scripts/fetch-siblings.sh"
+    exit 2
+  fi
+  pin="$(git -C "$dir" rev-parse HEAD)"
+  checked=$((checked + 1))
+  before=$failures
+
+  if ! grep -qF "hyperpolymath/$sibling @ $pin" "$citer"; then
+    echo "::error::$citer does not name hyperpolymath/$sibling @ $pin (the fetched pin)"
+    failures=$((failures + 1))
+  fi
+  if [[ ! -f "$dir/$file" ]]; then
+    echo "::error::$sibling @ ${pin:0:7} has no $file (cited by $citer)"
+    failures=$((failures + 1))
+    continue
+  fi
+  re="^[[:space:]]*((record|data)[[:space:]]+)?${def}([[:space:]]|$)"
+  if ! grep -Eq "$re" "$dir/$file"; then
+    echo "::error::$sibling @ ${pin:0:7}: $file declares no '$def' (cited by $citer)"
+    failures=$((failures + 1))
+  fi
+  if ! grep -qw -- "$def" "$citer"; then
+    echo "::error::$citer cites $sibling but never names '$def'"
+    failures=$((failures + 1))
+  fi
+  [[ "$failures" -eq "$before" ]] && echo "ok  $citer -> $sibling @ ${pin:0:7} $file :: $def"
+done
+
+echo "sibling citations: checked ${checked}, stale ${failures}"
+[[ "$failures" -eq 0 ]] || exit 1

scripts/check-verdicts.sh

@@ -0,0 +1,107 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-verdicts.sh — the mechanical falsifier for HYP-01's verdict record.
+#
+# src/Hypatia/ABI/Verdict.idr claims that a `Sound` verdict can be built only
+# from a `Mechanical` support whose prover re-check `Confirms`.  A claim about
+# what does NOT typecheck is tested by asking the typechecker:
+#
+#   1. the ABI package builds (the positive set, first: a broken toolchain or
+#      a missing import must never turn into a "successful" rejection);
+#   2. src/Hypatia/ABI/Verdict.idr contains no escape-hatch marker at all;
+#   3. every module under tests/accept/ is ACCEPTED (positive controls);
+#   4. every module under tests/reject/ is REFUSED, and refused only at its
+#      declaration `invalid`, with the diagnostic its `-- EXPECT:` line
+#      names — an error anywhere else, a different diagnostic (an arity
+#      slip is also "refused at invalid"), or a refusal for a missing name,
+#      import or parse, is a broken fixture, not a pass.
+#
+# An empty tests/accept/ or tests/reject/ is a broken checkout, not a pass.
+# The Lean half of the positive control (re-running the prover and comparing
+# digests) is scripts/recheck-lean-hole.sh.
+#
+# Usage: scripts/check-verdicts.sh
+# Env:   IDRIS2 (default: idris2)
+# Exit:  0 = all controls behave; 1 = a control misbehaved.
+
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+
+idris2="${IDRIS2:-idris2}"
+logs=_build/check-verdicts
+mkdir -p "$logs"
+
+"$idris2" --version
+
+# 1. Positive set: the ABI package, Verdict included.
+"$idris2" --build src/abi/hypatia-abi.ipkg
+export IDRIS2_PATH="$PWD/build/abi/ttc${IDRIS2_PATH:+:$IDRIS2_PATH}"
+
+# 2. No escape hatch in the module the rejections are about.
+if grep -nE 'believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry|admit|native_decide|Admitted|unsafeCoerce|Obj\.magic' \
+     src/Hypatia/ABI/Verdict.idr; then
+  echo "ERROR: escape-hatch marker in src/Hypatia/ABI/Verdict.idr" >&2
+  exit 1
+fi
+echo "PASS: no escape-hatch marker in src/Hypatia/ABI/Verdict.idr"
+
+shopt -s nullglob
+accepts=(tests/accept/*.idr)
+rejects=(tests/reject/*.idr)
+shopt -u nullglob
+if (( ${#accepts[@]} == 0 )); then
+  echo 'ERROR: no positive controls found under tests/accept' >&2
+  exit 1
+fi
+if (( ${#rejects[@]} == 0 )); then
+  echo 'ERROR: no expected-rejection modules found under tests/reject' >&2
+  exit 1
+fi
+
+# 3. Positive controls must typecheck.
+for file in "${accepts[@]}"; do
+  name="$(basename -- "$file" .idr)"
+  log="$logs/accept-$name.log"
+  if ! "$idris2" --source-dir tests/accept --build-dir "$logs/build" --check "$file" >"$log" 2>&1; then
+    cat "$log"
+    echo "ERROR: positive control refused: $name" >&2
+    exit 1
+  fi
+  if grep -q '^Error' "$log"; then
+    cat "$log"
+    echo "ERROR: positive control reported an error: $name" >&2
+    exit 1
+  fi
+  echo "PASS: accepted positive control $name"
+done
+
+# 4. Expected rejections must be refused, at `invalid`, for a typing reason.
+for file in "${rejects[@]}"; do
+  name="$(basename -- "$file" .idr)"
+  log="$logs/reject-$name.log"
+  if "$idris2" --source-dir tests/reject --build-dir "$logs/build" --check "$file" >"$log" 2>&1; then
+    cat "$log"
+    echo "ERROR: invalid verdict accepted: $name" >&2
+    exit 1
+  fi
+  expect="$(sed -n 's/^-- EXPECT: //p' "$file" | head -1)"
+  if [[ -z "$expect" ]]; then
+    echo "ERROR: $file declares no '-- EXPECT: <diagnostic>' line" >&2
+    exit 1
+  fi
+  errors="$(grep -c '^Error' "$log" || true)"
+  if [[ "$errors" -ne 1 ]] ||
+     ! grep -qF -- "$expect" "$log" ||
+     ! grep -q '^Error: While processing right hand side of invalid\.' "$log" ||
+     ! grep -Eq "^${name}:[0-9]+:[0-9]+--[0-9]+:[0-9]+" "$log" ||
+     grep -Eq 'Undefined name|Possible cause|Can.t find import|not in the source directory|Couldn.t parse|Parse error|is not a valid' "$log"; then
+    cat "$log"
+    echo "ERROR: unexpected failure while checking $name (want exactly one typing error, at invalid: $expect)" >&2
+    exit 1
+  fi
+  echo "PASS: rejected $name at invalid: $expect"
+done
+
+echo "PASS: ABI package, ${#accepts[@]} positive control(s), ${#rejects[@]} expected rejection(s)"

scripts/fetch-siblings.sh

@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Fetch the sibling proof repositories hypatia cites into _build/dependencies,
+# each at a recorded commit, with plain git (the residual-evidence-types
+# pattern).  A checkout that does not resolve to the pinned commit is a
+# failure, never a fallback to whatever the remote currently serves.
+#
+# Hypatia does not import these sources: Idris2 cannot consume Agda, so the
+# ABI records that follow them are transcriptions (ASSUMED correspondence).
+# The pins make the citation checkable — scripts/check-sibling-citations.sh
+# fails if a cited name is absent at the pin, or if a module header names a
+# different commit from the one fetched here.  Re-pin deliberately, one
+# commit per pin.
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+deps=_build/dependencies
+
+fetch() {
+  local name=$1 repo=$2 sha=$3 dir
+  dir=$deps/$name
+  if [[ ! -d "$dir/.git" ]]; then
+    git init -q "$dir"
+    git -C "$dir" remote add origin "https://github.com/$repo.git"
+  fi
+  git -C "$dir" fetch -q --depth 1 origin "$sha"
+  git -C "$dir" checkout -q --detach FETCH_HEAD
+  test "$(git -C "$dir" rev-parse HEAD)" = "$sha"
+  echo "$name @ $sha"
+}
+
+mkdir -p "$deps"
+# HYP-01 verdict record (src/Hypatia/ABI/Verdict.idr): Warrant / Epi / SoundWarrant.
+fetch epistemic-types hyperpolymath/epistemic-types 6a68de3141a981d766fd006b312f0919ade334bf