From 3d0c6b83c8a97535a54ce57030c4d4d89ddaadb7 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 10:44:40 +0000 Subject: [PATCH 01/51] ci(proofs): gate verification/proofs/ with the real all-proofs target MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Issue #57: `just proof-check-all` existed but no workflow ran it, and every prover recipe ended in `SKIP: not installed; exit 0`. The proofs were asserted, not enforced. Two further ways the target could go green without checking anything: a prover directory with no sources still printed PASS, and the banned-pattern scan flagged the *prose* "zero postulates" in EchoTyping.agda (exit 1 on a clean tree) while ignoring real escape hatches inside block comments. Enforcement added (no proof or safety flag weakened): * scripts/check-proof-enrolment.sh — registry gate. Parses [verification].allowed-proofs (placement.a2ml) and ALLOWED_PROOFS (check-coordination-boundary.sh), requires them to agree, requires every file under verification/proofs/ to be registered, requires every registration to exist on disk, refuses to pass on zero proof sources, and requires --safe/--without-K to stay in force. A required prover missing from PATH exits 2 (BLOCKED), never a skip. * scripts/proof-scan-dangerous.sh — comment-aware banned-pattern scan (block + line comments), word-boundary keywords, zero-work fails. * Justfile — proof-check-all now depends on the gate; every prover recipe fails BLOCKED when it has work and no prover, fails on any typecheck error, and prints NONE instead of PASS when it has no enrolled sources. * .github/workflows/proof-ci.yml — hosted lane for `just proof-check-all` on proof, manifest, Justfile and workflow changes. Agda 2.8.0 (sha256-verified official binary), agda-stdlib v2.3 (tag+commit asserted), just 1.59.0, echo-types and absolute-zero commit-pinned. No continue-on-error, no skip-on-missing-tool. Receipts uploaded as an artifact. * actions.lock — entry for the new workflow (existing pinned actions only). Local receipts: enrolment gate PASS (2 sources, 3 registered entries), banned-pattern scan PASS (2 files). Agda typecheck: BLOCKED locally (no Agda in this environment) — the hosted lane supplies it; not claimed as passing. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/actions.lock | 3 + .github/workflows/proof-ci.yml | 228 ++++++++++++ .../bot_directives/placement.a2ml | 5 + Justfile | 154 +++++--- scripts/check-proof-enrolment.sh | 349 ++++++++++++++++++ scripts/proof-scan-dangerous.sh | 130 +++++++ 6 files changed, 816 insertions(+), 53 deletions(-) create mode 100644 .github/workflows/proof-ci.yml create mode 100755 scripts/check-proof-enrolment.sh create mode 100755 scripts/proof-scan-dangerous.sh diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index c612c82..34f89b9 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -32,6 +32,9 @@ workflows: - 'actions/checkout@v7.0.1' - 'actions/deploy-pages@v5.0.1' - 'actions/upload-pages-artifact@v5.0.0' + '.github/workflows/proof-ci.yml': + - 'actions/checkout@v7.0.1' + - 'actions/upload-artifact@v7.0.2' '.github/workflows/push-email-notify.yml': - 'hyperpolymath/smtp-notify-action@v0.5.0' '.github/workflows/quality.yml': diff --git a/.github/workflows/proof-ci.yml b/.github/workflows/proof-ci.yml new file mode 100644 index 0000000..e653d44 --- /dev/null +++ b/.github/workflows/proof-ci.yml @@ -0,0 +1,228 @@ +# This workflow is managed by gh actions-lock. +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Proof CI — runs this repository's real all-proofs target, `just proof-check-all`, +# against the cross-project proofs hosted in verification/proofs/ (issue #57). +# +# Before this lane existed, `just proof-check-all` was never invoked by CI, and +# each recipe ended with `SKIP: not installed; exit 0`. The proofs were +# asserted, not enforced. This lane is deliberately intolerant: +# +# * a proof source that is not registered in the manifest -> FAIL +# * a manifest entry with no file behind it -> FAIL +# * the two registries disagreeing -> FAIL +# * nothing checked at all ("green on zero work") -> FAIL +# * a required prover not installed -> BLOCKED (fails) +# * a proof that does not typecheck -> FAIL +# +# There is no `continue-on-error` in this workflow, and no step is skipped when +# a tool is missing: a missing toolchain makes the run red, which is the point. +# +# Toolchain is pinned three ways so the lane cannot float: +# * Agda 2.8.0 — official release binary, sha256-verified before extraction +# * just 1.59.0 — exact version, installed from crates.io with --locked +# * libraries — agda-stdlib v2.3 (tag + commit asserted), echo-types and +# absolute-zero pinned by commit, each re-verified after checkout +# +# Receipts (versions, pins, registry hashes, per-prover results) are written to +# target/proof-receipts/ and uploaded as the `proof-receipts` artifact. +name: Proof CI + +on: + push: + branches: [main, master, develop] + paths: + - 'verification/proofs/**' + - '.machine_readable/bot_directives/placement.a2ml' + - 'scripts/check-coordination-boundary.sh' + - 'scripts/check-proof-enrolment.sh' + - 'scripts/proof-scan-dangerous.sh' + - 'Justfile' + - 'PROOF-NEEDS.adoc' + - 'PROOF-STATUS.adoc' + - '.github/workflows/proof-ci.yml' + pull_request: + branches: [main, master, develop] + paths: + - 'verification/proofs/**' + - '.machine_readable/bot_directives/placement.a2ml' + - 'scripts/check-coordination-boundary.sh' + - 'scripts/check-proof-enrolment.sh' + - 'scripts/proof-scan-dangerous.sh' + - 'Justfile' + - 'PROOF-NEEDS.adoc' + - 'PROOF-STATUS.adoc' + - '.github/workflows/proof-ci.yml' + workflow_dispatch: + +permissions: + contents: read + +concurrency: + group: proof-ci-${{ github.ref }} + cancel-in-progress: true + +env: + AGDA_VERSION: '2.8.0' + # sha256 of Agda-v2.8.0-linux.tar.xz (official GitHub release asset, agda/agda) + AGDA_LINUX_SHA256: '824081b8dcbe431289a50ac6bd83e451f390c51c3884ac7a8c4a5c0df2632faf' + JUST_VERSION: '1.59.0' + STDLIB_TAG: 'v2.3' + STDLIB_COMMIT: '8326c7475af1fa456ca04a0203c168d5d7ff842b' + # echo-types: the library the XP-1 proof is *about* (PROOF-STATUS.adoc). + # absolute-zero: declared dependency of echo-types' own .agda-lib. + ECHO_TYPES_COMMIT: 'b0982c44f36133acd2d0e1d4e03cf031fff7a470' + ABSOLUTE_ZERO_COMMIT: 'f486c29903434589117fa0662c6f29b0f17d1d5f' + PROOF_RECEIPT_DIR: 'target/proof-receipts' + +jobs: + proofs: + name: just proof-check-all (strict) + runs-on: ubuntu-24.04 + timeout-minutes: 45 + permissions: + contents: read + + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + + - name: Install pinned Agda (official binary, sha256-verified) + run: | + set -euo pipefail + mkdir -p "$RUNNER_TEMP/agda" "$HOME/.local/bin" + URL="https://github.com/agda/agda/releases/download/v${AGDA_VERSION}/Agda-v${AGDA_VERSION}-linux.tar.xz" + curl -fsSL -o "$RUNNER_TEMP/agda.tar.xz" "$URL" + echo "${AGDA_LINUX_SHA256} $RUNNER_TEMP/agda.tar.xz" | sha256sum --check --strict + tar -xJf "$RUNNER_TEMP/agda.tar.xz" -C "$RUNNER_TEMP/agda" + install -m 0755 "$RUNNER_TEMP/agda/agda" "$HOME/.local/bin/agda" + echo "$HOME/.local/bin" >> "$GITHUB_PATH" + "$HOME/.local/bin/agda" --version + "$HOME/.local/bin/agda" --setup + + - name: Install pinned just + run: | + set -euo pipefail + command -v cargo >/dev/null 2>&1 \ + || { echo "::error::cargo is required to build the pinned just; refusing to continue"; exit 1; } + cargo install just --version "${JUST_VERSION}" --locked + command -v just + just --version + + - name: Fetch pinned proof libraries + id: libs + run: | + set -euo pipefail + fetch_pinned() { # $1=url $2=dest $3=expected commit + git init -q "$2" + git -C "$2" remote add origin "$1" + git -C "$2" fetch -q --depth 1 origin "$3" + git -C "$2" checkout -q FETCH_HEAD + actual="$(git -C "$2" rev-parse HEAD)" + if [ "$actual" != "$3" ]; then + echo "::error::pin mismatch for $1: want $3 got $actual" + exit 1 + fi + echo "pinned $1 at $actual" + } + + # standard-library: tag and commit both asserted (a moved tag fails). + git clone -q --depth 1 --branch "$STDLIB_TAG" \ + https://github.com/agda/agda-stdlib.git "$RUNNER_TEMP/agda-stdlib" + actual="$(git -C "$RUNNER_TEMP/agda-stdlib" rev-parse HEAD)" + if [ "$actual" != "$STDLIB_COMMIT" ]; then + echo "::error::agda-stdlib $STDLIB_TAG moved: want $STDLIB_COMMIT got $actual" + exit 1 + fi + echo "pinned agda-stdlib $STDLIB_TAG at $actual" + + fetch_pinned https://github.com/hyperpolymath/echo-types.git \ + "$RUNNER_TEMP/echo-types" "$ECHO_TYPES_COMMIT" + fetch_pinned https://github.com/hyperpolymath/absolute-zero.git \ + "$RUNNER_TEMP/absolute-zero" "$ABSOLUTE_ZERO_COMMIT" + + - name: Register Agda libraries + run: | + set -euo pipefail + AGDA_DIR="$(agda --print-agda-app-dir)" + mkdir -p "$AGDA_DIR" + + # The upstream stdlib manifest is named `standard-library-2.3`, but + # nextgen-typing.agda-lib and echo-types.agda-lib both depend on + # `standard-library`, so register a manifest under that exact name + # (same include, same flags as upstream v2.3). + STDLIB_LIB="$RUNNER_TEMP/standard-library.agda-lib" + { + echo "name: standard-library" + echo "include: $RUNNER_TEMP/agda-stdlib/src" + echo "flags:" + echo " --warning=noUnsupportedIndexedMatch" + } > "$STDLIB_LIB" + + # Register the upstream manifests of the two pinned dependencies so + # their declared dependency graph (echo-types -> standard-library, + # absolute-zero) is honoured rather than shadowed. + ls "$RUNNER_TEMP/echo-types/echo-types.agda-lib" + ls "$RUNNER_TEMP/absolute-zero/absolute-zero.agda-lib" + + printf '%s\n%s\n%s\n' \ + "$STDLIB_LIB" \ + "$RUNNER_TEMP/echo-types/echo-types.agda-lib" \ + "$RUNNER_TEMP/absolute-zero/absolute-zero.agda-lib" \ + > "$AGDA_DIR/libraries" + printf 'standard-library\n' > "$AGDA_DIR/defaults" + echo "AGDA_DIR=$AGDA_DIR" + cat "$AGDA_DIR/libraries" + + - name: Toolchain receipt + run: | + set -euo pipefail + mkdir -p "$PROOF_RECEIPT_DIR" + { + echo "proof-ci toolchain receipt" + echo "generated: $(date -u +%Y-%m-%dT%H:%M:%SZ)" + echo "commit: $GITHUB_SHA" + echo "workflow-run: $GITHUB_SERVER_URL/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID" + echo "runner-image: ${ImageOS:-unknown} ${ImageVersion:-unknown}" + echo "agda: $(agda --version | head -n1)" + echo "just: $(just --version)" + echo "agda-stdlib: $STDLIB_TAG @ $STDLIB_COMMIT" + echo "echo-types: $ECHO_TYPES_COMMIT" + echo "absolute-zero: $ABSOLUTE_ZERO_COMMIT" + echo "placement.a2ml sha256: $(sha256sum .machine_readable/bot_directives/placement.a2ml | cut -d' ' -f1)" + echo "check-coordination-boundary.sh sha256: $(sha256sum scripts/check-coordination-boundary.sh | cut -d' ' -f1)" + } | tee "$PROOF_RECEIPT_DIR/toolchain.txt" + + # Version assertions: the lane must not silently run a different prover. + agda --version | grep -F "${AGDA_VERSION}" \ + || { echo "::error::Agda version is not the pinned ${AGDA_VERSION}"; agda --version; exit 1; } + just --version | grep -F "${JUST_VERSION}" \ + || { echo "::error::just version is not the pinned ${JUST_VERSION}"; just --version; exit 1; } + + - name: Enrolment gate (unlisted proofs, registry drift, missing provers) + run: just proof-enrolment + + - name: Run the real all-proofs target + run: just proof-check-all + + - name: Note receipts + run: | + echo "## Proof CI receipts" >> "$GITHUB_STEP_SUMMARY" + echo "" >> "$GITHUB_STEP_SUMMARY" + for f in "$PROOF_RECEIPT_DIR"/*.txt; do + [ -f "$f" ] || continue + echo "### $(basename "$f")" >> "$GITHUB_STEP_SUMMARY" + echo '```' >> "$GITHUB_STEP_SUMMARY" + cat "$f" >> "$GITHUB_STEP_SUMMARY" + echo '```' >> "$GITHUB_STEP_SUMMARY" + done + + - name: Upload receipts + if: always() + uses: actions/upload-artifact@v7.0.2 + with: + name: proof-receipts + path: target/proof-receipts/ + retention-days: 90 + if-no-files-found: warn diff --git a/.machine_readable/bot_directives/placement.a2ml b/.machine_readable/bot_directives/placement.a2ml index f3232cf..68e7470 100644 --- a/.machine_readable/bot_directives/placement.a2ml +++ b/.machine_readable/bot_directives/placement.a2ml @@ -76,6 +76,11 @@ allowed-proofs = [ "verification/proofs/agda/Verification.agda", # aggregator that typechecks the cross-project set "verification/proofs/agda/nextgen-typing.agda-lib", ] +enforced-by = [ + "just proof-enrolment (scripts/check-proof-enrolment.sh) -- FAILs when a proof is unlisted, when a registered entry has no file behind it, when this list and ALLOWED_PROOFS in scripts/check-coordination-boundary.sh disagree, or when zero proofs are enrolled; BLOCKED (exit 2) when a required prover is missing", + "just proof-scan-dangerous (scripts/proof-scan-dangerous.sh) -- FAILs on believe_me/assert_total/postulate/sorry/Admitted/unsafeCoerce/Obj.magic outside comments", + ".github/workflows/proof-ci.yml -- runs the real all-proofs target (`just proof-check-all`) on proof, manifest, Justfile and workflow changes", +] route-elsewhere = [ "ABI/FFI/memory-layout proofs -> typed-wasm", "TypeLL kernel proofs -> typell", diff --git a/Justfile b/Justfile index d8ebaee..e32a49f 100644 --- a/Justfile +++ b/Justfile @@ -1335,23 +1335,50 @@ help-me: # FORMAL VERIFICATION (PROOFS) # ═══════════════════════════════════════════════════════════════════════════════ -# Check all formal proofs (Idris2 + Lean4 + Agda + Coq) -proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous +# Strictness contract for every proof recipe below (they are what CI runs via +# .github/workflows/proof-ci.yml): +# +# exit 0 PASS the run actually checked something and it is clean +# exit 1 FAIL a proof failed, a proof is unlisted, or nothing was checked +# exit 2 BLOCKED a prover required by an enrolled proof is not installed +# +# No silent skips, no `continue-on-error`, no green run on zero work. A prover +# with no enrolled sources prints "NONE" instead of claiming a pass, and +# `proof-enrolment` guarantees at least one proof source is checked overall. +# +# Check all formal proofs — the real all-proofs target used by CI (strict) +proof-check-all: proof-enrolment proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous @echo "=== All proof checks complete ===" +# Enrolment gate: manifest <-> boundary allowlist <-> disk parity, required +# provers present, zero-work guard, --safe/--without-K still in force. +# Check proof enrolment (unlisted proofs, stale entries, missing provers) +proof-enrolment: + @bash scripts/check-proof-enrolment.sh --receipt "${PROOF_RECEIPT_DIR:-target/proof-receipts}/enrolment.txt" + # Check Idris2 proofs (ABI, types, dependent type proofs) proof-check-idris2: #!/usr/bin/env bash set -euo pipefail echo "=== Checking Idris2 proofs ===" - if ! command -v idris2 &>/dev/null; then - echo "SKIP: idris2 not installed" + mapfile -t FILES < <(find verification/proofs/idris2 -name '*.idr' -type f 2>/dev/null | sort) + RECEIPT_DIR="${PROOF_RECEIPT_DIR:-target/proof-receipts}" + mkdir -p "$RECEIPT_DIR" + if [ "${#FILES[@]}" -eq 0 ]; then + echo "NONE: no Idris2 proof sources enrolled under verification/proofs/idris2" + printf 'idris2: none-enrolled (0 files)\n' >>"$RECEIPT_DIR/provers.txt" exit 0 fi + if ! command -v idris2 &>/dev/null; then + echo "BLOCKED: ${#FILES[@]} Idris2 proof source(s) present but 'idris2' is not on PATH." + echo " A missing prover is BLOCKED, never a skip and never a pass." + printf 'idris2: BLOCKED (prover missing, %d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" + exit 2 + fi ERRORS=0 - for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do + for f in "${FILES[@]}"; do echo -n " Checking $f ... " - if idris2 --check "$f" 2>/dev/null; then + if idris2 --check "$f"; then echo "OK" else echo "FAIL" @@ -1360,23 +1387,35 @@ proof-check-idris2: done if [ "$ERRORS" -gt 0 ]; then echo "FAIL: $ERRORS Idris2 proof(s) failed" + printf 'idris2: FAIL (%d failed of %d)\n' "$ERRORS" "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" exit 1 fi - echo "PASS: All Idris2 proofs verified" + echo "PASS: ${#FILES[@]} Idris2 proof(s) verified" + printf 'idris2: PASS (%d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" # Check Lean4 proofs proof-check-lean4: #!/usr/bin/env bash set -euo pipefail echo "=== Checking Lean4 proofs ===" - if ! command -v lean &>/dev/null; then - echo "SKIP: lean not installed" + mapfile -t FILES < <(find verification/proofs/lean4 -name '*.lean' -type f 2>/dev/null | sort) + RECEIPT_DIR="${PROOF_RECEIPT_DIR:-target/proof-receipts}" + mkdir -p "$RECEIPT_DIR" + if [ "${#FILES[@]}" -eq 0 ]; then + echo "NONE: no Lean4 proof sources enrolled under verification/proofs/lean4" + printf 'lean4: none-enrolled (0 files)\n' >>"$RECEIPT_DIR/provers.txt" exit 0 fi + if ! command -v lean &>/dev/null; then + echo "BLOCKED: ${#FILES[@]} Lean4 proof source(s) present but 'lean' is not on PATH." + echo " A missing prover is BLOCKED, never a skip and never a pass." + printf 'lean4: BLOCKED (prover missing, %d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" + exit 2 + fi ERRORS=0 - for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do + for f in "${FILES[@]}"; do echo -n " Checking $f ... " - if lean "$f" 2>/dev/null; then + if lean "$f"; then echo "OK" else echo "FAIL" @@ -1385,23 +1424,37 @@ proof-check-lean4: done if [ "$ERRORS" -gt 0 ]; then echo "FAIL: $ERRORS Lean4 proof(s) failed" + printf 'lean4: FAIL (%d failed of %d)\n' "$ERRORS" "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" exit 1 fi - echo "PASS: All Lean4 proofs verified" + echo "PASS: ${#FILES[@]} Lean4 proof(s) verified" + printf 'lean4: PASS (%d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" -# Check Agda proofs +# Check Agda proofs (--safe; the proof sources also carry --without-K) proof-check-agda: #!/usr/bin/env bash set -euo pipefail echo "=== Checking Agda proofs ===" - if ! command -v agda &>/dev/null; then - echo "SKIP: agda not installed" + mapfile -t FILES < <(find verification/proofs/agda -name '*.agda' -type f 2>/dev/null | sort) + RECEIPT_DIR="${PROOF_RECEIPT_DIR:-target/proof-receipts}" + mkdir -p "$RECEIPT_DIR" + if [ "${#FILES[@]}" -eq 0 ]; then + echo "NONE: no Agda proof sources enrolled under verification/proofs/agda" + printf 'agda: none-enrolled (0 files)\n' >>"$RECEIPT_DIR/provers.txt" exit 0 fi + if ! command -v agda &>/dev/null; then + echo "BLOCKED: ${#FILES[@]} Agda proof source(s) present but 'agda' is not on PATH." + echo " Install Agda (see .github/workflows/proof-ci.yml for the pinned" + echo " toolchain and library registration). BLOCKED is not a pass." + printf 'agda: BLOCKED (prover missing, %d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" + exit 2 + fi + echo " toolchain: $(agda --version | head -n1)" ERRORS=0 - for f in $(find verification/proofs/agda -name '*.agda' 2>/dev/null); do + for f in "${FILES[@]}"; do echo -n " Checking $f ... " - if agda --safe "$f" 2>/dev/null; then + if agda --safe "$f"; then echo "OK" else echo "FAIL" @@ -1410,23 +1463,35 @@ proof-check-agda: done if [ "$ERRORS" -gt 0 ]; then echo "FAIL: $ERRORS Agda proof(s) failed" + printf 'agda: FAIL (%d failed of %d)\n' "$ERRORS" "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" exit 1 fi - echo "PASS: All Agda proofs verified" + echo "PASS: ${#FILES[@]} Agda proof(s) verified" + printf 'agda: PASS (%d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" # Check Coq proofs proof-check-coq: #!/usr/bin/env bash set -euo pipefail echo "=== Checking Coq proofs ===" - if ! command -v coqc &>/dev/null; then - echo "SKIP: coqc not installed" + mapfile -t FILES < <(find verification/proofs/coq -name '*.v' -type f 2>/dev/null | sort) + RECEIPT_DIR="${PROOF_RECEIPT_DIR:-target/proof-receipts}" + mkdir -p "$RECEIPT_DIR" + if [ "${#FILES[@]}" -eq 0 ]; then + echo "NONE: no Coq proof sources enrolled under verification/proofs/coq" + printf 'coq: none-enrolled (0 files)\n' >>"$RECEIPT_DIR/provers.txt" exit 0 fi + if ! command -v coqc &>/dev/null; then + echo "BLOCKED: ${#FILES[@]} Coq proof source(s) present but 'coqc' is not on PATH." + echo " A missing prover is BLOCKED, never a skip and never a pass." + printf 'coq: BLOCKED (prover missing, %d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" + exit 2 + fi ERRORS=0 - for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do + for f in "${FILES[@]}"; do echo -n " Checking $f ... " - if coqc "$f" 2>/dev/null; then + if coqc "$f"; then echo "OK" else echo "FAIL" @@ -1435,47 +1500,30 @@ proof-check-coq: done if [ "$ERRORS" -gt 0 ]; then echo "FAIL: $ERRORS Coq proof(s) failed" + printf 'coq: FAIL (%d failed of %d)\n' "$ERRORS" "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" exit 1 fi - echo "PASS: All Coq proofs verified" + echo "PASS: ${#FILES[@]} Coq proof(s) verified" + printf 'coq: PASS (%d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" -# Scan for dangerous patterns in proof files (believe_me, sorry, Admitted, etc.) +# Scan for banned escape hatches in proof files (comment-aware; zero-work fails) proof-scan-dangerous: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Scanning for dangerous patterns in proofs ===" - DANGEROUS=0 - PATTERNS="believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic" - for f in $(find verification/proofs -name '*.idr' -o -name '*.lean' -o -name '*.agda' -o -name '*.v' 2>/dev/null); do - MATCHES=$(grep -nE "$PATTERNS" "$f" 2>/dev/null || true) - if [ -n "$MATCHES" ]; then - echo " DANGEROUS: $f" - echo "$MATCHES" | sed 's/^/ /' - DANGEROUS=$((DANGEROUS + 1)) - fi - done - if [ "$DANGEROUS" -gt 0 ]; then - echo "FAIL: $DANGEROUS file(s) contain dangerous patterns" - exit 1 - fi - echo "PASS: No dangerous patterns found in proofs" + @bash scripts/proof-scan-dangerous.sh --receipt "${PROOF_RECEIPT_DIR:-target/proof-receipts}/dangerous-patterns.txt" -# Show proof status summary +# Show proof status summary (counts on disk vs. registered in the manifest) proof-status: #!/usr/bin/env bash echo "=== Proof Status ===" echo "" - echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null | wc -l) files" - echo "Lean4: $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null | wc -l) files" - echo "Agda: $(find verification/proofs/agda -name '*.agda' 2>/dev/null | wc -l) files" - echo "Coq: $(find verification/proofs/coq -name '*.v' 2>/dev/null | wc -l) files" - echo "TLA+: $(find verification/proofs/tlaplus -name '*.tla' 2>/dev/null | wc -l) files" + echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' -type f 2>/dev/null | wc -l) files" + echo "Lean4: $(find verification/proofs/lean4 -name '*.lean' -type f 2>/dev/null | wc -l) files" + echo "Agda: $(find verification/proofs/agda -name '*.agda' -type f 2>/dev/null | wc -l) files" + echo "Coq: $(find verification/proofs/coq -name '*.v' -type f 2>/dev/null | wc -l) files" + echo "TLA+: $(find verification/proofs/tlaplus -name '*.tla' -type f 2>/dev/null | wc -l) files" + echo "" + echo "Registered in .machine_readable/bot_directives/placement.a2ml:" + bash scripts/check-proof-enrolment.sh --static-only | sed -n '/proof sources on disk/,/^$/p' echo "" - if [ -f PROOF-STATUS.md ]; then - grep -E "^\| \*\*Total\*\*" PROOF-STATUS.md 2>/dev/null || echo "(No summary row in PROOF-STATUS.md)" - else - echo "(No PROOF-STATUS.md found)" - fi # ═══════════════════════════════════════════════════════════════════════════════ # SESSION MANAGEMENT (THIN BINDINGS TO CENTRAL STANDARDS) diff --git a/scripts/check-proof-enrolment.sh b/scripts/check-proof-enrolment.sh new file mode 100755 index 0000000..f6cb45a --- /dev/null +++ b/scripts/check-proof-enrolment.sh @@ -0,0 +1,349 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Proof enrolment gate. +# +# nextgen-typing hosts CROSS-project proofs (verification/proofs/) and claims +# they are machine-checked. This gate makes that claim enforceable *before* +# any prover runs, and closes the three ways a proof lane can lie: +# +# 1. UNLISTED — a proof source on disk that nobody registered in the +# manifest. (Fails: silent additions cannot ride along.) +# 2. STALE — a manifest entry with no file behind it. (Fails: the +# registry cannot drift away from reality.) +# 3. ZERO WORK — nothing checked at all, reported as "PASS". (Fails.) +# +# It also refuses to pretend a prover is present: a prover required by the +# manifest but missing from PATH is reported BLOCKED (exit 2), never PASS. +# +# Sources of truth (verified to agree with each other, not assumed): +# * .machine_readable/bot_directives/placement.a2ml [verification].allowed-proofs +# * scripts/check-coordination-boundary.sh ALLOWED_PROOFS +# * the files actually present under verification/proofs/ +# +# Exit codes: 0 = PASS 1 = FAIL 2 = BLOCKED (required prover missing) +# +# Usage: +# bash scripts/check-proof-enrolment.sh [--receipt PATH] +# bash scripts/check-proof-enrolment.sh --static-only # skip prover probe + +set -uo pipefail + +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "$ROOT" || exit 1 + +MANIFEST=".machine_readable/bot_directives/placement.a2ml" +BOUNDARY="scripts/check-coordination-boundary.sh" +PROOFS_DIR="verification/proofs" +RECEIPT="" +STATIC_ONLY=0 + +while [ "$#" -gt 0 ]; do + case "$1" in + --receipt) RECEIPT="${2:-}"; shift 2 ;; + --receipt=*) RECEIPT="${1#--receipt=}"; shift ;; + --static-only) STATIC_ONLY=1; shift ;; + -h|--help) sed -n '2,30p' "$0"; exit 0 ;; + *) echo "unknown argument: $1" >&2; exit 1 ;; + esac +done + +FAILS=() +BLOCKED=() +NOTES=() + +fail() { FAILS+=("$1"); } + +# --- prover table ------------------------------------------------------------ +# extension -> label|binary|extra safety requirement +prover_label() { + case "$1" in + agda) echo "Agda" ;; + idris2) echo "Idris2" ;; + lean4) echo "Lean4" ;; + coq) echo "Coq" ;; + tlaplus) echo "TLA+" ;; + *) echo "unknown" ;; + esac +} +prover_binary() { + case "$1" in + agda) echo "agda" ;; + idris2) echo "idris2" ;; + lean4) echo "lean" ;; + coq) echo "coqc" ;; + tlaplus) echo "" ;; # no prover wired for TLA+ in this repo + *) echo "" ;; + esac +} + +# Path -> prover key, by extension. Prints nothing for non-proof-source files. +prover_of_path() { + case "$1" in + *.agda) echo "agda" ;; + *.lagda) echo "agda" ;; + *.idr) echo "idris2" ;; + *.lean) echo "lean4" ;; + *.v) echo "coq" ;; + *.tla) echo "tlaplus" ;; + *.thy) echo "isabelle" ;; # known proof source, deliberately unwired + *) echo "" ;; + esac +} + +echo "=== Proof enrolment gate ===" +echo "repo: $ROOT" +echo "manifest: $MANIFEST" +echo "boundary: $BOUNDARY" +echo "" + +# --- 0. required inputs exist ----------------------------------------------- +[ -f "$MANIFEST" ] || { echo "FAIL: manifest not found: $MANIFEST"; exit 1; } +[ -f "$BOUNDARY" ] || { echo "FAIL: boundary guard not found: $BOUNDARY"; exit 1; } +[ -d "$PROOFS_DIR" ] || { echo "FAIL: proofs directory not found: $PROOFS_DIR"; exit 1; } + +# --- 1. parse the two registries and require them to agree ------------------- +# [verification].allowed-proofs = [ "path", ... ] (comments allowed) +normalize_list_entries() { + # strip comments, quotes, commas and all whitespace; drop blanks; sort + sed 's/#.*//' \ + | tr -d "\"' \t\r" \ + | sed 's/,*$//' \ + | grep -v '^$' \ + | sort +} + +manifest_list="$(awk ' + /^\[/ { in_section = ($0 ~ /^\[verification\]/); next } + in_section && /^[[:space:]]*allowed-proofs[[:space:]]*=[[:space:]]*\[/ { in_list = 1; next } + in_list && /^[[:space:]]*\][[:space:]]*$/ { in_list = 0; next } + in_list { print } +' "$MANIFEST" | normalize_list_entries)" + +boundary_list="$(awk ' + /^ALLOWED_PROOFS=\(/ { in_list = 1; next } + in_list && /^\)/ { in_list = 0; next } + in_list { print } +' "$BOUNDARY" | normalize_list_entries)" + +if [ -z "$manifest_list" ]; then + fail "manifest registry is empty: no allowed-proofs entries in $MANIFEST" +fi +if [ -z "$boundary_list" ]; then + fail "boundary allowlist is empty: no ALLOWED_PROOFS entries in $BOUNDARY" +fi + +while IFS= read -r entry; do + [ -z "$entry" ] && continue + if ! grep -Fxq -- "$entry" <<<"$boundary_list"; then + fail "registry drift: '$entry' is in $MANIFEST but not in ALLOWED_PROOFS of $BOUNDARY" + fi +done <<<"$manifest_list" + +while IFS= read -r entry; do + [ -z "$entry" ] && continue + if ! grep -Fxq -- "$entry" <<<"$manifest_list"; then + fail "registry drift: '$entry' is in ALLOWED_PROOFS of $BOUNDARY but not in $MANIFEST" + fi +done <<<"$boundary_list" + +# --- 2. enumerate what is actually on disk ---------------------------------- +disk_files="$(find "$PROOFS_DIR" -type f \ + ! -name '*.a2ml' ! -name '*.adoc' ! -name '*.md' ! -name '.gitkeep' \ + | sed 's|^\./||' | sort)" + +disk_proofs="$(while IFS= read -r f; do + [ -z "$f" ] && continue + [ -n "$(prover_of_path "$f")" ] && echo "$f" + done <<<"$disk_files")" + +# --- 3. every file on disk must be registered (UNLISTED proofs fail) -------- +list_size=0 +while IFS= read -r f; do + [ -z "$f" ] && continue + list_size=$((list_size + 1)) + if ! grep -Fxq -- "$f" <<<"$manifest_list"; then + if [ -n "$(prover_of_path "$f")" ]; then + fail "unlisted proof source: $f + Register it in [verification].allowed-proofs of $MANIFEST AND in + ALLOWED_PROOFS of $BOUNDARY (see verification/proofs/README.adoc)." + else + fail "unregistered file under $PROOFS_DIR: $f + Every tracked file here (including .agda-lib manifests) must be listed in + both registries, otherwise the proof set can drift silently." + fi + fi +done <<<"$disk_files" + +# --- 4. every registered entry must exist (STALE entries fail) -------------- +while IFS= read -r entry; do + [ -z "$entry" ] && continue + if [ ! -e "$entry" ]; then + fail "stale registry entry: '$entry' is registered but not present on disk" + fi +done <<<"$manifest_list" + +# --- 5. zero work is never a pass ------------------------------------------ +proof_count=0 +while IFS= read -r f; do + [ -z "$f" ] && continue + proof_count=$((proof_count + 1)) +done <<<"$disk_proofs" + +if [ "$proof_count" -eq 0 ]; then + fail "zero proof sources found under $PROOFS_DIR — refusing to report PASS on zero work" +fi + +# --- 6. safety flags must remain in force ---------------------------------- +while IFS= read -r f; do + [ -z "$f" ] && continue + case "$f" in + *.agda|*.lagda) + if ! grep -qE '\{-#[[:space:]]*OPTIONS[^#]*--safe' "$f"; then + fail "missing safety flag: $f does not declare --safe in its OPTIONS pragma" + fi + if ! grep -qE '\{-#[[:space:]]*OPTIONS[^#]*--without-K' "$f"; then + fail "missing safety flag: $f does not declare --without-K in its OPTIONS pragma + (If a genuinely cubical proof is being added, that is a deliberate policy + change: update PROOF-NEEDS.adoc and this gate in the same commit.)" + fi + ;; + esac +done <<<"$disk_proofs" + +# --- 7. per-prover census + prover presence -------------------------------- +declare -A per_prover=() +prover_order=() +while IFS= read -r f; do + [ -z "$f" ] && continue + key="$(prover_of_path "$f")" + if [ -z "${per_prover[$key]:-}" ]; then prover_order+=("$key"); fi + per_prover["$key"]=$(( ${per_prover["$key"]:-0} + 1 )) +done <<<"$disk_proofs" + +# Stable, human-readable prover list for receipts/summaries. +prover_list="" +if [ "${#prover_order[@]}" -gt 0 ]; then + prover_list="$(printf '%s,' "${prover_order[@]}" | sed 's/,$//')" +else + prover_list="none" +fi + +echo "--- proof sources on disk (registered: $list_size, proof sources: $proof_count) ---" +if [ "$proof_count" -gt 0 ]; then + while IFS= read -r f; do + [ -z "$f" ] && continue + printf ' %-12s %s\n' "$(prover_of_path "$f")" "$f" + done <<<"$disk_proofs" +else + echo " (none)" +fi +echo "" + +echo "--- required provers ---" +toolchain_report="" +if [ "${#per_prover[@]}" -eq 0 ]; then + echo " (none — no prover is required because no proof source is enrolled)" +else + for key in "${prover_order[@]}"; do + count="${per_prover[$key]}" + bin="$(prover_binary "$key")" + label="$(prover_label "$key")" + if [ -z "$bin" ]; then + fail "prover not wired: $count proof source(s) for '$key' ($label) but this repo has no prover recipe for it" + continue + fi + if [ "$STATIC_ONLY" -eq 1 ]; then + echo " $label ($key): $count source(s); binary '$bin' not probed (--static-only)" + toolchain_report+=" $key: not-probed"$'\n' + continue + fi + if command -v "$bin" >/dev/null 2>&1; then + ver="$("$bin" --version 2>&1 | head -n1 || true)" + [ -z "$ver" ] && ver="(version probe produced no output)" + echo " $label ($key): $count source(s), $bin present — $ver" + toolchain_report+=" $key: present ($ver)"$'\n' + NOTES+=("$label: $ver") + else + echo " $label ($key): $count source(s), $bin MISSING" + BLOCKED+=("required prover missing: '$bin' is needed by $count $label proof source(s) but is not on PATH + Install it, or the proof lane must stay red. A missing prover is BLOCKED, + never a skip and never a pass.") + toolchain_report+=" $key: MISSING"$'\n' + fi + done +fi +echo "" + +# --- 8. receipt + verdict -------------------------------------------------- +status="PASS" +[ "${#FAILS[@]}" -gt 0 ] && status="FAIL" +[ "$status" = "PASS" ] && [ "${#BLOCKED[@]}" -gt 0 ] && status="BLOCKED" + +if [ -n "$RECEIPT" ]; then + mkdir -p "$(dirname "$RECEIPT")" 2>/dev/null || true + { + echo "proof-enrolment receipt" + echo "generated: $(date -u +%Y-%m-%dT%H:%M:%SZ)" + echo "commit: ${GITHUB_SHA:-$(git rev-parse HEAD 2>/dev/null || echo unknown)}" + echo "runner: ${RUNNER_NAME:-local}/${RUNNER_OS:-$(uname -s)}" + echo "status: $status" + echo "registered-entries: $list_size" + echo "proof-sources: $proof_count" + echo "provers: $prover_list" + echo "manifest-sha256: $(sha256sum "$MANIFEST" | cut -d' ' -f1)" + echo "boundary-script-sha256: $(sha256sum "$BOUNDARY" | cut -d' ' -f1)" + echo "toolchain:" + printf '%s' "$toolchain_report" + if [ "${#FAILS[@]}" -gt 0 ]; then + echo "failures:" + printf ' - %s\n' "${FAILS[@]}" + fi + if [ "${#BLOCKED[@]}" -gt 0 ]; then + echo "blocked:" + printf ' - %s\n' "${BLOCKED[@]}" + fi + } >"$RECEIPT" + echo "receipt written: $RECEIPT" + if [ -n "${GITHUB_STEP_SUMMARY:-}" ]; then + { + echo "## Proof enrolment gate — **$status**" + echo "" + echo "| item | value |" + echo "|------|-------|" + echo "| registered entries | $list_size |" + echo "| proof sources on disk | $proof_count |" + echo "| provers | $prover_list |" + echo "| receipt | \`$RECEIPT\` |" + echo "" + } >>"$GITHUB_STEP_SUMMARY" + fi +fi + +if [ "${#FAILS[@]}" -gt 0 ]; then + echo "=== FAIL: ${#FAILS[@]} enrolment error(s) ===" + printf ' ✗ %s\n' "${FAILS[@]}" + echo "" +fi +if [ "${#BLOCKED[@]}" -gt 0 ]; then + echo "=== BLOCKED: ${#BLOCKED[@]} required prover(s) unavailable ===" + printf ' ⚠ %s\n' "${BLOCKED[@]}" + echo "" +fi + +case "$status" in + PASS) + echo "✅ PASS: $proof_count proof source(s) enrolled, registries agree, all required provers present." + exit 0 + ;; + FAIL) + echo "❌ FAIL: the proof registry and/or the proof set is not in an honest state." + exit 1 + ;; + BLOCKED) + echo "⚠️ BLOCKED: enrolment is consistent but a required prover is missing." + echo " This is NOT a pass. The proof lane stays red until the prover is installed." + exit 2 + ;; +esac diff --git a/scripts/proof-scan-dangerous.sh b/scripts/proof-scan-dangerous.sh new file mode 100755 index 0000000..26f4e48 --- /dev/null +++ b/scripts/proof-scan-dangerous.sh @@ -0,0 +1,130 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Banned-pattern scan for hosted proofs. +# +# PROOF-NEEDS.adoc bans every escape hatch a prover offers: +# believe_me, assert_total (Idris2) +# postulate (Idris2 / Agda) +# sorry (Lean4) +# Admitted (Coq) +# unsafeCoerce (Haskell) +# Obj.magic (OCaml / ReScript) +# +# This scan is comment-aware: a *prose* mention (for example "zero postulates" +# in a header comment) is not an escape hatch, and flagging it trains people to +# ignore the gate. A real `postulate` declaration, `sorry`, or `Admitted` is +# still caught, because the keyword survives comment stripping. +# +# Exit codes: 0 = clean 1 = banned pattern found 2 = nothing scanned +# +# Usage: bash scripts/proof-scan-dangerous.sh [--receipt PATH] + +set -uo pipefail + +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "$ROOT" || exit 1 + +PROOFS_DIR="verification/proofs" +RECEIPT="" + +while [ "$#" -gt 0 ]; do + case "$1" in + --receipt) RECEIPT="${2:-}"; shift 2 ;; + --receipt=*) RECEIPT="${1#--receipt=}"; shift ;; + -h|--help) sed -n '2,22p' "$0"; exit 0 ;; + *) echo "unknown argument: $1" >&2; exit 1 ;; + esac +done + +# Keyword-boundary patterns. \b keeps "postulates" (prose) out while still +# matching a bare `postulate` declaration. +PATTERNS='\b(believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce)\b|\bObj[.]magic\b' + +echo "=== Scanning for dangerous patterns in proofs ===" +echo "patterns: $PATTERNS" +echo "scope: $PROOFS_DIR" + +# Strip comments (line comments: -- and //; block comments: {- -} and (* *)) +# while preserving line numbers, so hits are reported against the real file. +strip_comments() { + awk ' + BEGIN { block = 0 } + { + line = $0 + out = "" + i = 1 + n = length(line) + while (i <= n) { + two = substr(line, i, 2) + if (block == 1) { + if (two == "-}" || two == "*)") { block = 0; i += 2 } else { i += 1 } + continue + } + if (two == "--" || two == "//") { break } + if (two == "{-" || two == "(*") { block = 1; i += 2; continue } + out = out substr(line, i, 1) + i += 1 + } + print out + } + ' "$1" +} + +FILES_SCANNED=0 +HITS=0 +REPORT="" + +while IFS= read -r f; do + [ -z "$f" ] && continue + FILES_SCANNED=$((FILES_SCANNED + 1)) + matches="$(strip_comments "$f" | grep -nE -- "$PATTERNS" || true)" + if [ -n "$matches" ]; then + echo " BANNED PATTERN: $f" + echo "$matches" | sed 's/^/ line /' + REPORT+="$f"$'\n'"$matches"$'\n' + HITS=$((HITS + 1)) + else + echo " clean: $f" + fi +done < <(find "$PROOFS_DIR" -type f \ + \( -name '*.agda' -o -name '*.lagda' -o -name '*.idr' \ + -o -name '*.lean' -o -name '*.v' -o -name '*.tla' \) \ + | sed 's|^\./||' | sort) + +echo "" +if [ "$FILES_SCANNED" -eq 0 ]; then + echo "FAIL: no proof sources scanned — refusing to report a clean scan on zero work" + [ -n "$RECEIPT" ] && printf 'status: FAIL\nreason: zero files scanned\n' >"$RECEIPT" + exit 2 +fi + +if [ "$HITS" -gt 0 ]; then + echo "FAIL: $HITS file(s) contain banned proof escape hatches" + if [ -n "$RECEIPT" ]; then + { + echo "proof-scan receipt" + echo "generated: $(date -u +%Y-%m-%dT%H:%M:%SZ)" + echo "commit: ${GITHUB_SHA:-$(git rev-parse HEAD 2>/dev/null || echo unknown)}" + echo "status: FAIL" + echo "files-scanned: $FILES_SCANNED" + echo "files-with-hits: $HITS" + printf '%s' "$REPORT" + } >"$RECEIPT" + fi + exit 1 +fi + +echo "PASS: $FILES_SCANNED proof source(s) scanned, no banned patterns outside comments" +if [ -n "$RECEIPT" ]; then + { + echo "proof-scan receipt" + echo "generated: $(date -u +%Y-%m-%dT%H:%M:%SZ)" + echo "commit: ${GITHUB_SHA:-$(git rev-parse HEAD 2>/dev/null || echo unknown)}" + echo "status: PASS" + echo "files-scanned: $FILES_SCANNED" + echo "files-with-hits: 0" + } >"$RECEIPT" +fi +exit 0 From 7325e7358c254a3e1e395821d9d4e866f09a5341 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 10:47:02 +0000 Subject: [PATCH 02/51] ci(proofs): annotate proof failures so the failing module is visible MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The hosted lane's first run went red inside `just proof-check-all`; raw runner logs were not retrievable, so the failing error was invisible to anyone reading the PR. Pipe the target's output through tee and, only on failure, re-emit the tail as ::error:: annotations (and into the job summary). Diagnostics only — the run is already red when this executes. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/proof-ci.yml | 27 ++++++++++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) diff --git a/.github/workflows/proof-ci.yml b/.github/workflows/proof-ci.yml index e653d44..0cc0009 100644 --- a/.github/workflows/proof-ci.yml +++ b/.github/workflows/proof-ci.yml @@ -204,7 +204,32 @@ jobs: run: just proof-enrolment - name: Run the real all-proofs target - run: just proof-check-all + run: | + set -o pipefail + just proof-check-all 2>&1 | tee "$RUNNER_TEMP/proof-check-all.log" + + # Diagnostics only: the run is already red by the time this executes. + # Proof failures are annotated so the failing module/error is visible in + # the PR and via the check-run API without unzipping raw runner logs. + - name: Surface prover diagnostics + if: failure() + run: | + set -uo pipefail + LOG="$RUNNER_TEMP/proof-check-all.log" + if [ ! -f "$LOG" ]; then + echo "::error::proof-check-all produced no log (a step before it failed)" + exit 0 + fi + tail -n 40 "$LOG" | while IFS= read -r line; do + [ -z "${line//[[:space:]]/}" ] && continue + echo "::error::${line:0:900}" + done + { + echo "### proof-check-all log tail (failure diagnostics)" + echo '```' + tail -n 60 "$LOG" + echo '```' + } >> "$GITHUB_STEP_SUMMARY" - name: Note receipts run: | From 8d3744bde472edcc84889e933a4d83cdfcd93a28 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 10:48:29 +0000 Subject: [PATCH 03/51] ci(proofs): annotate only the log tail (GitHub caps 10 annotations per step) Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/proof-ci.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/proof-ci.yml b/.github/workflows/proof-ci.yml index 0cc0009..e82251c 100644 --- a/.github/workflows/proof-ci.yml +++ b/.github/workflows/proof-ci.yml @@ -220,8 +220,9 @@ jobs: echo "::error::proof-check-all produced no log (a step before it failed)" exit 0 fi - tail -n 40 "$LOG" | while IFS= read -r line; do - [ -z "${line//[[:space:]]/}" ] && continue + # GitHub caps annotations at 10 per step, so emit the *last* lines: + # that is where the failing prover's diagnostic lands. + grep -vE '^[[:space:]]*$' "$LOG" | tail -n 10 | while IFS= read -r line; do echo "::error::${line:0:900}" done { From 5a05924a38d943a95b90186cb2975d3434fbe06a Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 10:50:47 +0000 Subject: [PATCH 04/51] ci(proofs): attach the whole failure tail as one newline-encoded annotation Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/proof-ci.yml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/.github/workflows/proof-ci.yml b/.github/workflows/proof-ci.yml index e82251c..f5ba927 100644 --- a/.github/workflows/proof-ci.yml +++ b/.github/workflows/proof-ci.yml @@ -220,11 +220,12 @@ jobs: echo "::error::proof-check-all produced no log (a step before it failed)" exit 0 fi - # GitHub caps annotations at 10 per step, so emit the *last* lines: - # that is where the failing prover's diagnostic lands. - grep -vE '^[[:space:]]*$' "$LOG" | tail -n 10 | while IFS= read -r line; do - echo "::error::${line:0:900}" - done + # GitHub caps annotations at 10 per step and each annotation is + # single-line, so emit ONE annotation carrying the last 100 lines + # newline-encoded (%0A). That keeps the failing prover's own + # diagnostic attached to the check run, not buried in runner logs. + PAYLOAD="$(grep -vE '^[[:space:]]*$' "$LOG" | tail -n 100 | head -c 60000 | sed ':a;N;$!ba;s/\n/%0A/g')" + echo "::error::proof-check-all failed. Log tail:%0A${PAYLOAD}" { echo "### proof-check-all log tail (failure diagnostics)" echo '```' From f2efcdd33449ad865c32a3adff0a8cf93fb29a10 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 10:52:50 +0000 Subject: [PATCH 05/51] fix(proofs): resolve the repo's Agda library manifest in proof-check-agda First hosted run of proof-ci.yml reached the prover and failed both modules with [ModuleNameDoesntMatchFileName]: Agda searched only CWD, the registered defaults and its primitive library, so the proof directory was never an include root and nextgen-typing.agda-lib was inert. Pass --library=verification/proofs/agda/nextgen-typing.agda-lib (and fail if the manifest is missing) so the manifest's include path and its standard-library/echo-types dependencies are what Agda uses. No proof source and no safety flag is touched: --safe stays, --without-K stays in the file pragmas. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- Justfile | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/Justfile b/Justfile index e32a49f..4913dac 100644 --- a/Justfile +++ b/Justfile @@ -1451,10 +1451,21 @@ proof-check-agda: exit 2 fi echo " toolchain: $(agda --version | head -n1)" + # Activate the repo's own Agda library manifest explicitly. Without it Agda + # searches only the CWD, the registered defaults and its primitive library, + # and reports [ModuleNameDoesntMatchFileName] for every proof module + # (observed on the first hosted run of proof-ci.yml). The manifest is the + # authority for include paths and dependencies (standard-library, + # echo-types); it is NOT shadowed or replaced here. + AGDA_LIB="verification/proofs/agda/nextgen-typing.agda-lib" + if [ ! -f "$AGDA_LIB" ]; then + echo "FAIL: Agda library manifest missing: $AGDA_LIB" + exit 1 + fi ERRORS=0 for f in "${FILES[@]}"; do echo -n " Checking $f ... " - if agda --safe "$f"; then + if agda --safe --library="$AGDA_LIB" "$f"; then echo "OK" else echo "FAIL" From 4c6b918998b9756fdeb1e64c74de27a968677ac1 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 10:54:52 +0000 Subject: [PATCH 06/51] fix(proofs): activate the repo's Agda library by name, and register it in CI Run 2 showed --library expects an installed library *name*, not a path (LibraryError). Derive the name from nextgen-typing.agda-lib itself and pass --library=, so drift between recipe and manifest fails loudly; register the repo manifest alongside standard-library/echo-types/absolute-zero in the lane's AGDA_DIR/libraries. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/proof-ci.yml | 15 +++++++++++---- Justfile | 22 +++++++++++++++------- 2 files changed, 26 insertions(+), 11 deletions(-) diff --git a/.github/workflows/proof-ci.yml b/.github/workflows/proof-ci.yml index f5ba927..0783871 100644 --- a/.github/workflows/proof-ci.yml +++ b/.github/workflows/proof-ci.yml @@ -162,14 +162,21 @@ jobs: # Register the upstream manifests of the two pinned dependencies so # their declared dependency graph (echo-types -> standard-library, - # absolute-zero) is honoured rather than shadowed. - ls "$RUNNER_TEMP/echo-types/echo-types.agda-lib" - ls "$RUNNER_TEMP/absolute-zero/absolute-zero.agda-lib" + # absolute-zero) is honoured rather than shadowed, plus this repo's + # own manifest (the authority for the proof include path and for the + # standard-library / echo-types dependency). + for lib in "$RUNNER_TEMP/echo-types/echo-types.agda-lib" \ + "$RUNNER_TEMP/absolute-zero/absolute-zero.agda-lib" \ + "$GITHUB_WORKSPACE/verification/proofs/agda/nextgen-typing.agda-lib"; do + [ -f "$lib" ] || { echo "::error::missing Agda library manifest: $lib"; exit 1; } + echo "registering $lib" + done - printf '%s\n%s\n%s\n' \ + printf '%s\n%s\n%s\n%s\n' \ "$STDLIB_LIB" \ "$RUNNER_TEMP/echo-types/echo-types.agda-lib" \ "$RUNNER_TEMP/absolute-zero/absolute-zero.agda-lib" \ + "$GITHUB_WORKSPACE/verification/proofs/agda/nextgen-typing.agda-lib" \ > "$AGDA_DIR/libraries" printf 'standard-library\n' > "$AGDA_DIR/defaults" echo "AGDA_DIR=$AGDA_DIR" diff --git a/Justfile b/Justfile index 4913dac..1e3fdcd 100644 --- a/Justfile +++ b/Justfile @@ -1451,21 +1451,29 @@ proof-check-agda: exit 2 fi echo " toolchain: $(agda --version | head -n1)" - # Activate the repo's own Agda library manifest explicitly. Without it Agda - # searches only the CWD, the registered defaults and its primitive library, - # and reports [ModuleNameDoesntMatchFileName] for every proof module - # (observed on the first hosted run of proof-ci.yml). The manifest is the - # authority for include paths and dependencies (standard-library, - # echo-types); it is NOT shadowed or replaced here. + # Activate the repo's own Agda library manifest explicitly, by the name it + # declares. Without it Agda searches only the CWD, the registered defaults + # and its primitive library, so the proof directory is not an include root + # and every module fails with [ModuleNameDoesntMatchFileName] (observed on + # the first hosted run of proof-ci.yml). The manifest stays the authority + # for include paths and dependencies (standard-library, echo-types); it is + # not shadowed or replaced here. Register it once with: + # agda --print-agda-app-dir # then add the .agda-lib path to libraries AGDA_LIB="verification/proofs/agda/nextgen-typing.agda-lib" if [ ! -f "$AGDA_LIB" ]; then echo "FAIL: Agda library manifest missing: $AGDA_LIB" exit 1 fi + AGDA_LIB_NAME="$(sed -n 's/^name:[[:space:]]*//p' "$AGDA_LIB" | head -n1 | tr -d '[:space:]')" + if [ -z "$AGDA_LIB_NAME" ]; then + echo "FAIL: $AGDA_LIB declares no library name" + exit 1 + fi + echo " library: $AGDA_LIB_NAME ($AGDA_LIB)" ERRORS=0 for f in "${FILES[@]}"; do echo -n " Checking $f ... " - if agda --safe --library="$AGDA_LIB" "$f"; then + if agda --safe --library="$AGDA_LIB_NAME" "$f"; then echo "OK" else echo "FAIL" From a267d58d524682d853965d24f3a443e7860c0176 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 10:57:29 +0000 Subject: [PATCH 07/51] docs(proofs): record the enforcement that now exists, from actual receipts PROOF-STATUS.adoc: add the guard table (enrolment gate, per-prover strictness, banned-pattern scan, proof-ci lane), the real verification commands, and a receipt table citing proof-ci run 41299544043 (green, sha 4c6b918) and the failing first runs that exposed the [ModuleNameDoesntMatchFileName] defect. Local run recorded as BLOCKED (no Agda), not as a pass. verification/proofs/README.adoc: replace the false claim that CI enforces the banned patterns via 'panic-attack assail --proofs-only' with the scripts that actually run; document that an unlisted proof fails the enrolment gate. PROOF-NEEDS.adoc: same correction, plus the proof-CI guard in References. No proof source and no safety flag is touched. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- PROOF-NEEDS.adoc | 13 ++++- PROOF-STATUS.adoc | 93 +++++++++++++++++++++++++++++++-- verification/proofs/README.adoc | 39 +++++++++++++- 3 files changed, 138 insertions(+), 7 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index c3cd384..884b334 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -66,11 +66,20 @@ When adding one, register it in `+[verification].allowed-proofs+` of |`+Obj.magic+` |OCaml/ReScript |Unsafe type cast |=== -CI rejects any PR introducing these (`+panic-attack assail+`). +CI rejects any PR introducing these. The enforcement is +`+just proof-scan-dangerous+` (`+scripts/proof-scan-dangerous.sh+`, run inside +`+just proof-check-all+`), plus the enrolment gate +(`+scripts/check-proof-enrolment.sh+`) which fails any proof that is not +registered in both `+[verification].allowed-proofs+` of +`+placement.a2ml+` and `+ALLOWED_PROOFS+` of +`+scripts/check-coordination-boundary.sh+`. Hosted lane: +`+.github/workflows/proof-ci.yml+`. === References * Routing table: `+.machine_readable/bot_directives/placement.a2ml+` -* CI guard: `+scripts/check-coordination-boundary.sh+` / +* CI guard (coordination boundary): `+scripts/check-coordination-boundary.sh+` / `+.github/workflows/coordination-boundary.yml+` +* CI guard (proofs): `+scripts/check-proof-enrolment.sh+`, +`+scripts/proof-scan-dangerous.sh+` / `+.github/workflows/proof-ci.yml+` * Proof status tracking: `+PROOF-STATUS.md+` (this repo) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 4b5741a..7d8b1a3 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -28,26 +28,111 @@ removed (the ABI proof obligations are owned by `+typed-wasm+`). |XP-1 |Pipeline information-loss = echo-types fibers |echo-types ↔ affinescript ↔ typed-wasm |Agda (`+--safe --without-K+`) |`+verification/proofs/agda/EchoTyping.agda+` -|`+agda Verification.agda+` +|`+just proof-check-all+` in `.github/workflows/proof-ci.yml` +|=== + +=== Enforcement (CI) + +Until 2026-11-01 these proofs were *asserted*: `+just proof-check-all+` +existed but no workflow invoked it, and every prover recipe ended in +`+SKIP: not installed+` followed by `+exit 0+`. Worse, a prover +directory with no sources still printed `+PASS+`, and the banned-pattern scan +matched the prose "zero postulates" in `+EchoTyping.agda+` while ignoring real +escape hatches inside block comments. The lane below closes all three. + +[cols="30%,70%",options="header",] +|=== +|Guard |Behaviour +|`+just proof-enrolment+` +(`+scripts/check-proof-enrolment.sh+`) +|Parses `+[verification].allowed-proofs+` (placement.a2ml) and +`+ALLOWED_PROOFS+` (`+scripts/check-coordination-boundary.sh+`) and requires +them to agree. Fails when a proof source is unlisted, when a registered entry +has no file behind it, when zero proofs are enrolled, or when an `.agda` proof +loses `+--safe+`/`+--without-K+`. A required prover missing from `PATH` is +**BLOCKED** (exit 2) — never a skip, never a pass. + +|`+just proof-check-agda+` (and the Idris2/Lean4/Coq equivalents) +|Exits 2 (BLOCKED) when proofs for that prover are enrolled but the prover is +absent; exits 1 on any typecheck failure; prints `+NONE+` instead of `+PASS+` +when that prover has no enrolled sources. + +|`+just proof-scan-dangerous+` +(`+scripts/proof-scan-dangerous.sh+`) +|Comment-aware keyword scan for `+believe_me+`, `+assert_total+`, +`+postulate+`, `+sorry+`, `+Admitted+`, `+unsafeCoerce+`, `+Obj.magic+`. Fails +on any hit outside a comment, and fails when it scans zero files. + +|`.github/workflows/proof-ci.yml` +|Hosted lane running `+just proof-check-all+` on pushes/PRs that touch +`+verification/proofs/**+`, the two registries, the gate scripts, `+Justfile+` +or the workflow itself. Pins Agda 2.8.0 (official binary, sha256-verified), +agda-stdlib v2.3 (tag + commit asserted), `+just+` 1.59.0, and +echo-types / absolute-zero by commit. No `+continue-on-error+`, no +skip-on-missing-tool. Receipts are uploaded as the `+proof-receipts+` artifact. |=== === Verification [source,bash] ---- -# Typecheck the cross-project Agda set (requires the echo-types library on the -# Agda include path; see verification/proofs/agda/nextgen-typing.agda-lib) -agda verification/proofs/agda/Verification.agda +# Everything, exactly as CI runs it (this is the real all-proofs target): +just proof-check-all + +# Just the registry/manifest gate (no prover needed): +bash scripts/check-proof-enrolment.sh --static-only + +# One prover, directly. The repo's own library manifest must be activated or +# Agda reports [ModuleNameDoesntMatchFileName] for every module (receipt: +# proof-ci run 41299261152, 2026-11-01). Register once with +# `agda --print-agda-app-dir`, then add +# verification/proofs/agda/nextgen-typing.agda-lib +# plus the `standard-library`, `echo-types` and `absolute-zero` manifests +# (echo-types' own manifest depends on absolute-zero) to +# /libraries: +agda --safe --library=nextgen-typing verification/proofs/agda/Verification.agda # Enforce the coordination boundary (no project code / non-allowlisted proofs) bash scripts/check-coordination-boundary.sh ---- +=== Enforcement receipts + +[cols="16%,20%,64%",options="header",] +|=== +|Date |Receipt |Result +|2026-11-01 |proof-ci run +https://github.com/hyperpolymath/nextgen-typing/actions/runs/41299544043 +(sha `+4c6b918+`) |**PASS** — `+just proof-check-all+` green on the hosted +lane: enrolment gate PASS (2 proof sources, 3 registered entries, registries +agree), Agda 2.8.0 typecheck of `+EchoTyping.agda+` and `+Verification.agda+` +under `+--safe --library=nextgen-typing+` against agda-stdlib v2.3, +echo-types `+b0982c4+` and absolute-zero `+f486c29+`, banned-pattern scan +clean. This is the first CI receipt that these proofs typecheck. + +|2026-11-01 |proof-ci runs 41298824595, 41299096293 (first attempts) |**FAIL**, +and correctly so: the proofs had never actually been run, and the old +documented invocation did not activate `+nextgen-typing.agda-lib+`, so every +module failed with `+[ModuleNameDoesntMatchFileName]+`. Fixed by activating the +library in the recipe; no proof source or safety flag was changed. + +|2026-11-01 |local receipts (this repository, no Agda installed) |Enrolment +gate `+--static-only+`: **PASS** (2 sources, 3 registered entries). +Banned-pattern scan: **PASS** (2 files). `+just proof-check-all+`: +**BLOCKED** (exit 2, Agda absent) — recorded as blocked, not as a pass. +|=== + === Changelog [width="100%",cols="32%,42%,26%",options="header",] |=== |Date |Change |By +|2026-11-01 |Proofs are now *enforced*, not asserted: `+just proof-check-all+` +runs in `.github/workflows/proof-ci.yml`; enrolment gate fails unlisted/stale/ +zero-work runs and blocks on a missing prover. Lane green at `+4c6b918+` +(run 41299544043); the Agda invocation had to activate +`+nextgen-typing.agda-lib+` to typecheck at all |Arena agent + |2026-06-19 |Reconciled to coordination reality: removed RSR ABI/TP scaffold proofs (owned by typed-wasm/typell); tracking cross-project proofs only |maintainer diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index 3025f7e..021de5a 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -50,6 +50,38 @@ Before adding anything, check the gate: * `[verification].allowed-proofs` in `.machine_readable/bot_directives/placement.a2ml`, and * `ALLOWED_PROOFS` in `scripts/check-coordination-boundary.sh`. . Ensure `--safe` / `%default total` / no escape hatches (see Banned Patterns). +. Run the gate. `just proof-enrolment` fails when a proof source under + `verification/proofs/` is not registered in *both* places above, when a + registered entry has no file behind it, when the two registries disagree, + and when zero proofs are enrolled. It is the first dependency of + `just proof-check-all`, so an unlisted proof cannot reach `main` green. + +== How a proof is checked + +Every proof source here is typechecked by the real all-proofs target, which CI +runs on any change to proofs, registries, `Justfile` or the lane: + +[source,bash] +---- +just proof-check-all # .github/workflows/proof-ci.yml +---- + +A prover that is required (because proofs for it are enrolled) but absent from +`PATH` makes the run **BLOCKED** (exit 2) — the lane never skips it and never +turns that into a pass. A prover with no enrolled sources prints `NONE`, not +`PASS`. + +The Agda layer needs its library manifest activated, otherwise Agda reports +`[ModuleNameDoesntMatchFileName]` for every module (observed on 2026-11-01): + +[source,bash] +---- +agda --safe --library=nextgen-typing verification/proofs/agda/Verification.agda +---- + +`nextgen-typing.agda-lib`, `standard-library`, `echo-types` and its own +dependency `absolute-zero` must be registered in `/libraries` +(`agda --print-agda-app-dir`). `.github/workflows/proof-ci.yml` pins all four. == Banned patterns @@ -60,5 +92,10 @@ The following MUST NOT appear in any proof file: * `sorry` (Lean4) * `Admitted` (Coq) * `unsafeCoerce` (Haskell) +* `Obj.magic` (OCaml/ReScript) -CI enforces this via `panic-attack assail --proofs-only`. +CI enforces this with `just proof-scan-dangerous` +(`scripts/proof-scan-dangerous.sh`), which runs inside `just proof-check-all`. +It is comment-aware — a prose mention such as "zero postulates" is not flagged, +while a real escape hatch is, including inside `{- ... -}` blocks. A scan that +finds no proof files to scan fails rather than reporting clean. From ebc14c680df4d0729ff323d3eecaf9de8484367f Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 11:37:39 +0000 Subject: [PATCH 08/51] Update scripts/check-proof-enrolment.sh Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- scripts/check-proof-enrolment.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/check-proof-enrolment.sh b/scripts/check-proof-enrolment.sh index f6cb45a..1376986 100755 --- a/scripts/check-proof-enrolment.sh +++ b/scripts/check-proof-enrolment.sh @@ -149,9 +149,9 @@ while IFS= read -r entry; do done <<<"$boundary_list" # --- 2. enumerate what is actually on disk ---------------------------------- -disk_files="$(find "$PROOFS_DIR" -type f \ - ! -name '*.a2ml' ! -name '*.adoc' ! -name '*.md' ! -name '.gitkeep' \ - | sed 's|^\./||' | sort)" +disk_files="$(git ls-files -- "$PROOFS_DIR" \ + | grep -Ev '\.(a2ml|adoc|md)$|(^|/)\.gitkeep$' \ + | sort)" disk_proofs="$(while IFS= read -r f; do [ -z "$f" ] && continue From 5e97ae474229e1743bc5200a545d55d5a13d1ccc Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 11:38:13 +0000 Subject: [PATCH 09/51] Update scripts/check-proof-enrolment.sh Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- scripts/check-proof-enrolment.sh | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/scripts/check-proof-enrolment.sh b/scripts/check-proof-enrolment.sh index 1376986..6a47cfd 100755 --- a/scripts/check-proof-enrolment.sh +++ b/scripts/check-proof-enrolment.sh @@ -218,6 +218,13 @@ prover_order=() while IFS= read -r f; do [ -z "$f" ] && continue key="$(prover_of_path "$f")" + case "$key:$f" in + agda:"$PROOFS_DIR"/agda/*.agda|idris2:"$PROOFS_DIR"/idris2/*.idr|\ + lean4:"$PROOFS_DIR"/lean4/*.lean|coq:"$PROOFS_DIR"/coq/*.v) ;; + agda:*|idris2:*|lean4:*|coq:*) + fail "proof source not reachable by its prover recipe: $f + proof-check-$key only checks $PROOFS_DIR/$key/ with its canonical extension." ;; + esac if [ -z "${per_prover[$key]:-}" ]; then prover_order+=("$key"); fi per_prover["$key"]=$(( ${per_prover["$key"]:-0} + 1 )) done <<<"$disk_proofs" From 8356cb6ee1598de2fe2c908a8745937744198983 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 11:38:40 +0000 Subject: [PATCH 10/51] Update scripts/proof-scan-dangerous.sh Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- scripts/proof-scan-dangerous.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/proof-scan-dangerous.sh b/scripts/proof-scan-dangerous.sh index 26f4e48..bc08bee 100755 --- a/scripts/proof-scan-dangerous.sh +++ b/scripts/proof-scan-dangerous.sh @@ -97,7 +97,7 @@ echo "" if [ "$FILES_SCANNED" -eq 0 ]; then echo "FAIL: no proof sources scanned — refusing to report a clean scan on zero work" [ -n "$RECEIPT" ] && printf 'status: FAIL\nreason: zero files scanned\n' >"$RECEIPT" - exit 2 + exit 1 fi if [ "$HITS" -gt 0 ]; then From ebe0fe4932572975f16184409ce14958271fa268 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Sun, 1 Nov 2026 11:57:06 +0000 Subject: [PATCH 11/51] docs(proofs): Document helper behavior and error handling in proof scripts and CI --- .github/workflows/proof-ci.yml | 2 ++ scripts/check-proof-enrolment.sh | 7 ++++++- scripts/proof-scan-dangerous.sh | 6 ++++-- 3 files changed, 12 insertions(+), 3 deletions(-) diff --git a/.github/workflows/proof-ci.yml b/.github/workflows/proof-ci.yml index 0783871..ee4f280 100644 --- a/.github/workflows/proof-ci.yml +++ b/.github/workflows/proof-ci.yml @@ -114,6 +114,8 @@ jobs: id: libs run: | set -euo pipefail + # Initialise $2, fetch and check out $3 from $1, and exit 1 if HEAD + # differs from $3. Git errors terminate this step under set -e. fetch_pinned() { # $1=url $2=dest $3=expected commit git init -q "$2" git -C "$2" remote add origin "$1" diff --git a/scripts/check-proof-enrolment.sh b/scripts/check-proof-enrolment.sh index 6a47cfd..547a3cb 100755 --- a/scripts/check-proof-enrolment.sh +++ b/scripts/check-proof-enrolment.sh @@ -53,10 +53,12 @@ FAILS=() BLOCKED=() NOTES=() +# Add an enrolment error to the global list used for the final verdict. fail() { FAILS+=("$1"); } # --- prover table ------------------------------------------------------------ # extension -> label|binary|extra safety requirement +# Print the display label for a prover key, or "unknown" for an unrecognised key. prover_label() { case "$1" in agda) echo "Agda" ;; @@ -67,6 +69,7 @@ prover_label() { *) echo "unknown" ;; esac } +# Print the executable for a prover key, or an empty line if none is wired. prover_binary() { case "$1" in agda) echo "agda" ;; @@ -105,8 +108,10 @@ echo "" # --- 1. parse the two registries and require them to agree ------------------- # [verification].allowed-proofs = [ "path", ... ] (comments allowed) +# Read registry lines from stdin, remove comments, quotes, spaces, tabs, carriage +# returns and trailing commas, then print non-empty lines sorted. Return non-zero +# if no lines remain or a pipeline command fails. normalize_list_entries() { - # strip comments, quotes, commas and all whitespace; drop blanks; sort sed 's/#.*//' \ | tr -d "\"' \t\r" \ | sed 's/,*$//' \ diff --git a/scripts/proof-scan-dangerous.sh b/scripts/proof-scan-dangerous.sh index bc08bee..a1eb1aa 100755 --- a/scripts/proof-scan-dangerous.sh +++ b/scripts/proof-scan-dangerous.sh @@ -46,8 +46,10 @@ echo "=== Scanning for dangerous patterns in proofs ===" echo "patterns: $PATTERNS" echo "scope: $PROOFS_DIR" -# Strip comments (line comments: -- and //; block comments: {- -} and (* *)) -# while preserving line numbers, so hits are reported against the real file. +# Print $1 with line comments (-- and //) and block comments ({- -} and (* *)) +# removed, preserving line numbers. Delimiters in strings are treated as comments +# and nested blocks are not supported. An awk read error returns non-zero; the +# scan's calling pipeline suppresses that error. strip_comments() { awk ' BEGIN { block = 0 } From 6c609c4a88a8a9241c3a1d8abd041229ac2f06bc Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 13:53:00 +0000 Subject: [PATCH 12/51] proof: audit the ledger and compile declared Rocq/Lean recheck legs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Follows standards/3-practice/PROOF-POLICY.adoc and mathesis `estate-mathematical-architecture` to the letter, examining only the Coq/Lean witness state. The previous lane re-ran the estate's own "all four provers" sweep; under §1/§2 that was the wrong shape. Agda is a theory proof's SOURCE leg and Rocq + Lean are its RECHECK legs, so: * the Agda leg is RECORDED in verification/proofs/LEDGER.json (commit, run, pinned library assumptions) and audited for form — not re-derived; * the ledger audit and the declared recheck legs are what CI enforces. Witness verdict, in the policy's own vocabulary: XP-1 kind=theory grade=3 (Agda only, not translated) agda: proven @ 4c6b918 (run 41299544043) rocq: open — no witness; §2 wants transport (Dedukti/Lambdapi) or a hand re-proof, with the statement comparison recorded lean4: open — no witness; no Mathlib, so a core-Lean re-proof Grade 2i needs one proven leg, 2ii needs two plus a non-DTT leg (Agda/Rocq/ Lean are all DTT/CIC, so 2ii is unreachable from this family), Grade 1 needs AXLE/coq-lsp/isabelle-server. None is established, and nothing here claims otherwise. New: scripts/check-proof-ledger.sh the policy gate: schema + closed §5 vocabulary, grade supported by proven legs, artifact/MANIFEST/route/statement- comparison/axiom bookkeeping for any claimed leg, no Mathlib, comment- aware escape-hatch scan, undeclared-axiom cross-check, manifest <-> ALLOWED_PROOFS <-> disk parity, witnesses on disk claimed by the ledger, docs anchored to the ledger. Open legs print POLICY GAP and are never counted as verification. scripts/check-proofs.sh the estate instrument, verbatim from mathesis (missing toolchain = FAIL, unmanifested file = ERROR, a quarantined module that starts compiling = ERROR). verification/proofs/LEDGER.json + per-prover MANIFESTs tests/proofs/run-controls.sh §7 both ways: closed Rocq/Lean proofs must be accepted (Print Assumptions "closed", #print axioms "no axioms"); `Admitted`/`sorry` controls, a grade with no leg behind it, and a witness planted on disk must all be rejected. No prover here => BLOCKED, exit 2. CI (.github/workflows/proof-ci.yml): pins Rocq 8.18 and Lean 4.15.0, runs the controls, then `just proof-witness-check` (enrolment + banned-pattern + ledger audit + declared Rocq/Lean legs), then the Agda source leg, and announces every policy gap as a warning. A zero-work guard fails if a leg is recorded proven with no gated module. No continue-on-error, no skip-on-missing-tool. Gates widened, not weakened: MANIFEST/LEDGER.json are excluded from the proof registries (they are the gates' inputs, not proofs) in both check-proof-enrolment.sh and check-coordination-boundary.sh; the latter allows tests/proofs/control/* only if each fixture declares itself and stays <= 20 lines. The ledger gate's unclaimed-witness check no longer degrades silently in a tree without .git. Docs: PROOF-STATUS.adoc re-anchored to the ledger (the "1 of 1 done" figure is withdrawn — it inflated a single-prover proof into a finished one), PROOF-NEEDS and verification/proofs/README updated to the §5 vocabulary and the MANIFEST format. Local receipts: enrolment --static-only PASS, ledger gate PASS (1 theorem, 2 sources, 0 proven legs, 2 policy gaps), boundary PASS, banned-pattern PASS, justfile parses; coqc/lean absent here, so the compile legs and the controls are BLOCKED locally and must be proven in CI. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/proof-ci.yml | 196 +++++- .../bot_directives/placement.a2ml | 2 +- Justfile | 259 +++----- PROOF-NEEDS.adoc | 13 +- PROOF-STATUS.adoc | 216 +++++-- scripts/check-coordination-boundary.sh | 30 +- scripts/check-proof-enrolment.sh | 8 + scripts/check-proof-ledger.sh | 599 ++++++++++++++++++ scripts/check-proofs.sh | 183 ++++++ tests/proofs/control/Control.lean | 6 + tests/proofs/control/Control.v | 8 + tests/proofs/control/PlantedAdmitted.v | 7 + tests/proofs/control/PlantedSorry.lean | 7 + tests/proofs/run-controls.sh | 171 +++++ verification/proofs/LEDGER.json | 97 +++ verification/proofs/README.adoc | 114 ++-- verification/proofs/agda/MANIFEST | 12 + verification/proofs/coq/MANIFEST | 15 + verification/proofs/lean4/MANIFEST | 10 + 19 files changed, 1648 insertions(+), 305 deletions(-) create mode 100755 scripts/check-proof-ledger.sh create mode 100755 scripts/check-proofs.sh create mode 100644 tests/proofs/control/Control.lean create mode 100644 tests/proofs/control/Control.v create mode 100644 tests/proofs/control/PlantedAdmitted.v create mode 100644 tests/proofs/control/PlantedSorry.lean create mode 100755 tests/proofs/run-controls.sh create mode 100644 verification/proofs/LEDGER.json create mode 100644 verification/proofs/agda/MANIFEST create mode 100644 verification/proofs/coq/MANIFEST create mode 100644 verification/proofs/lean4/MANIFEST diff --git a/.github/workflows/proof-ci.yml b/.github/workflows/proof-ci.yml index ee4f280..37e8b66 100644 --- a/.github/workflows/proof-ci.yml +++ b/.github/workflows/proof-ci.yml @@ -2,16 +2,40 @@ # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # -# Proof CI — runs this repository's real all-proofs target, `just proof-check-all`, -# against the cross-project proofs hosted in verification/proofs/ (issue #57). +# Proof CI — audits the proof ledger and compiles the recheck legs it declares, +# via `just proof-witness-check` (issue #57). # -# Before this lane existed, `just proof-check-all` was never invoked by CI, and -# each recipe ended with `SKIP: not installed; exit 0`. The proofs were -# asserted, not enforced. This lane is deliberately intolerant: +# Scope, per standards/3-practice/PROOF-POLICY.adoc and mathesis +# `estate-mathematical-architecture`: # -# * a proof source that is not registered in the manifest -> FAIL -# * a manifest entry with no file behind it -> FAIL -# * the two registries disagreeing -> FAIL +# * §1: a theory proof's source of truth is Agda. XP-1's Agda leg is RECORDED +# in verification/proofs/LEDGER.json (commit + run + assumptions pinned) and +# audited for form here. The lane does not re-derive it. +# * §2: that statement must be rechecked in Rocq AND Lean — transported +# through Dedukti/Lambdapi or re-proved by hand, with the statement +# comparison recorded and no Mathlib. Those are the legs this lane +# examines. BOTH ARE CURRENTLY OPEN: no witness exists, so the lane +# compiles zero recheck modules and the gate prints the gap as a +# `POLICY GAP` line on every run. +# * §5/§6: status is the closed vocabulary (open | argued | tested-only | +# proven-with-postulates | proven); a grade must be supported by the legs +# behind it; axioms are tracked (`Print Assumptions`, `#print axioms`), not +# assumed; receipts are pinned to a commit. +# * §7: a gate must be verified BOTH WAYS. tests/proofs/run-controls.sh feeds +# the instrument a closed Rocq proof and a closed Lean proof (must pass), a +# proof closed with `Admitted` and one closed with `sorry` (must fail), a +# ledger claiming a grade with no leg behind it (must fail), and a witness +# planted on disk that no ledger row claims (must fail). +# +# What this lane refuses, and why it exists: before it, `just proof-check-all` +# was never invoked by CI and each recipe ended in +# `SKIP: not installed; exit 0`. The proofs were asserted, not +# enforced. This lane is deliberately intolerant: +# +# * a proof source that is not in the ledger / a MANIFEST -> FAIL +# * a ledger or manifest entry with no file behind it -> FAIL +# * the registries disagreeing -> FAIL +# * a grade the proven legs do not support -> FAIL # * nothing checked at all ("green on zero work") -> FAIL # * a required prover not installed -> BLOCKED (fails) # * a proof that does not typecheck -> FAIL @@ -19,14 +43,21 @@ # There is no `continue-on-error` in this workflow, and no step is skipped when # a tool is missing: a missing toolchain makes the run red, which is the point. # -# Toolchain is pinned three ways so the lane cannot float: +# A green run does NOT mean XP-1 is verified in an independent kernel. It means +# the ledger is honest about what has and has not been proven. Today it records +# Grade 3 (Agda only) with both recheck legs open. +# +# Toolchains are pinned so the lane cannot float: # * Agda 2.8.0 — official release binary, sha256-verified before extraction # * just 1.59.0 — exact version, installed from crates.io with --locked +# * Rocq/Coq 8.18 — Ubuntu 24.04's package, version asserted after install +# * Lean 4 — official release archive, exact version asserted # * libraries — agda-stdlib v2.3 (tag + commit asserted), echo-types and # absolute-zero pinned by commit, each re-verified after checkout # -# Receipts (versions, pins, registry hashes, per-prover results) are written to -# target/proof-receipts/ and uploaded as the `proof-receipts` artifact. +# Receipts (versions, pins, ledger hash, census, policy gaps, per-prover +# results) are written to target/proof-receipts/ and uploaded as the +# `proof-receipts` artifact. name: Proof CI on: @@ -37,7 +68,10 @@ on: - '.machine_readable/bot_directives/placement.a2ml' - 'scripts/check-coordination-boundary.sh' - 'scripts/check-proof-enrolment.sh' + - 'scripts/check-proof-ledger.sh' + - 'scripts/check-proofs.sh' - 'scripts/proof-scan-dangerous.sh' + - 'tests/proofs/**' - 'Justfile' - 'PROOF-NEEDS.adoc' - 'PROOF-STATUS.adoc' @@ -49,7 +83,10 @@ on: - '.machine_readable/bot_directives/placement.a2ml' - 'scripts/check-coordination-boundary.sh' - 'scripts/check-proof-enrolment.sh' + - 'scripts/check-proof-ledger.sh' + - 'scripts/check-proofs.sh' - 'scripts/proof-scan-dangerous.sh' + - 'tests/proofs/**' - 'Justfile' - 'PROOF-NEEDS.adoc' - 'PROOF-STATUS.adoc' @@ -68,6 +105,10 @@ env: # sha256 of Agda-v2.8.0-linux.tar.xz (official GitHub release asset, agda/agda) AGDA_LINUX_SHA256: '824081b8dcbe431289a50ac6bd83e451f390c51c3884ac7a8c4a5c0df2632faf' JUST_VERSION: '1.59.0' + # Ubuntu 24.04 (noble) ships this exact Rocq/Coq build; asserted below. + ROCQ_VERSION: '8.18' + # No Mathlib (PROOF-POLICY §2): the lean leg must be core Lean. Asserted below. + LEAN_VERSION: '4.15.0' STDLIB_TAG: 'v2.3' STDLIB_COMMIT: '8326c7475af1fa456ca04a0203c168d5d7ff842b' # echo-types: the library the XP-1 proof is *about* (PROOF-STATUS.adoc). @@ -78,7 +119,7 @@ env: jobs: proofs: - name: just proof-check-all (strict) + name: just proof-witness-check (strict) runs-on: ubuntu-24.04 timeout-minutes: 45 permissions: @@ -110,6 +151,44 @@ jobs: command -v just just --version + - name: Install pinned Rocq (Ubuntu package, version asserted) + run: | + set -euo pipefail + sudo apt-get update + # zstd is for the Lean archive; coq is the Rocq recheck leg's compiler. + sudo apt-get install -y --no-install-recommends coq zstd + for tool in coqc coqtop coqchk; do command -v "$tool"; done + coqc --version + coqc --version | grep -F "${ROCQ_VERSION}" \ + || { echo "::error::Rocq is not the pinned ${ROCQ_VERSION}"; coqc --version; exit 1; } + + - name: Install pinned Lean 4 (official release archive, version asserted) + run: | + set -euo pipefail + # Core Lean only. Mathlib is forbidden by PROOF-POLICY §2, so nothing + # here fetches a package cache or a library: the leg must stand on the + # Lean kernel alone. + NAME="lean-${LEAN_VERSION}-linux.tar.zst" + URL="https://github.com/leanprover/lean4/releases/download/v${LEAN_VERSION}/${NAME}" + mkdir -p "$RUNNER_TEMP/lean-dl" "$RUNNER_TEMP/lean" + curl -fsSL -o "$RUNNER_TEMP/lean-dl/$NAME" "$URL" + # The release asset ships no published digest, so the archive identity + # is recorded rather than asserted against an upstream constant. The + # version assertion below is what actually pins the toolchain: a + # substituted archive that is not this Lean fails the step. + echo "$(stat -c%s "$RUNNER_TEMP/lean-dl/$NAME") bytes sha256 $(sha256sum "$RUNNER_TEMP/lean-dl/$NAME" | cut -d' ' -f1)" \ + | tee "$RUNNER_TEMP/lean-dl/archive.txt" + tar --zstd -xf "$RUNNER_TEMP/lean-dl/$NAME" -C "$RUNNER_TEMP/lean" + # Do NOT copy the binaries elsewhere: Lean resolves its core library + # relative to the executable, so a copied binary loses its sysroot. + echo "$RUNNER_TEMP/lean/lean-${LEAN_VERSION}-linux/bin" >> "$GITHUB_PATH" + export PATH="$RUNNER_TEMP/lean/lean-${LEAN_VERSION}-linux/bin:$PATH" + command -v lean lake + lean --version + lean --version | grep -F "${LEAN_VERSION}" \ + || { echo "::error::Lean is not the pinned ${LEAN_VERSION}"; lean --version; exit 1; } + lake --version + - name: Fetch pinned proof libraries id: libs run: | @@ -196,6 +275,10 @@ jobs: echo "runner-image: ${ImageOS:-unknown} ${ImageVersion:-unknown}" echo "agda: $(agda --version | head -n1)" echo "just: $(just --version)" + echo "rocq: $(coqc --version | head -n1)" + echo "rocq deb: $(dpkg-query -W -f='\${Version}' coq 2>/dev/null || echo unknown)" + echo "lean: $(lean --version | head -n1)" + echo "lean archive: $(cat "$RUNNER_TEMP/lean-dl/archive.txt" 2>/dev/null || echo unknown)" echo "agda-stdlib: $STDLIB_TAG @ $STDLIB_COMMIT" echo "echo-types: $ECHO_TYPES_COMMIT" echo "absolute-zero: $ABSOLUTE_ZERO_COMMIT" @@ -208,14 +291,91 @@ jobs: || { echo "::error::Agda version is not the pinned ${AGDA_VERSION}"; agda --version; exit 1; } just --version | grep -F "${JUST_VERSION}" \ || { echo "::error::just version is not the pinned ${JUST_VERSION}"; just --version; exit 1; } + coqc --version | grep -F "${ROCQ_VERSION}" \ + || { echo "::error::Rocq version is not the pinned ${ROCQ_VERSION}"; coqc --version; exit 1; } + lean --version | grep -F "${LEAN_VERSION}" \ + || { echo "::error::Lean version is not the pinned ${LEAN_VERSION}"; lean --version; exit 1; } - name: Enrolment gate (unlisted proofs, registry drift, missing provers) run: just proof-enrolment - - name: Run the real all-proofs target + # PROOF-POLICY §7: a gate that has only ever been seen to pass is + # indistinguishable from one that cannot fail. These controls feed the + # instrument closed proofs (must pass) and planted violations (must fail) + # before the lane is trusted with the real ledger. exit 2 = BLOCKED, which + # fails this step: an instrument that could not be exercised proved nothing. + - name: Instrument controls, both ways (§7) + run: | + set -o pipefail + bash tests/proofs/run-controls.sh 2>&1 | tee "$RUNNER_TEMP/proof-controls.log" + cp "$RUNNER_TEMP/proof-controls.log" "$PROOF_RECEIPT_DIR/controls.txt" + + # The CI target: audit the ledger, then compile every recheck leg the + # ledger declares. XP-1 declares Rocq and Lean 4, both `open`, so these + # compile zero modules — and the ledger gate refuses any claim that they + # compiled. The gate's receipt (census + POLICY GAP lines) is written to + # $PROOF_RECEIPT_DIR/ledger.txt by `just proof-ledger-check`. + - name: Ledger audit + declared recheck legs (Rocq, Lean 4) + run: | + set -o pipefail + just proof-witness-check 2>&1 | tee "$RUNNER_TEMP/proof-witness-check.log" + + # "PASS" from a per-prover step must never be reachable with nothing + # compiled. scripts/check-proofs.sh is the estate instrument and is used + # verbatim, so its zero-module case is closed around it here: if the ledger + # records a proven Rocq/Lean leg, that leg's MANIFEST must list at least one + # gated module. With no proven legs (today) zero compiled modules is the + # honest count and is stated as such, not glossed as a pass. + - name: Zero-work guard (a proven leg cannot compile nothing) + run: | + set -euo pipefail + LEDGER=verification/proofs/LEDGER.json + bad=0 + while IFS= read -r leg; do + [ -z "$leg" ] && continue + case "$leg" in + rocq|coq) dir=coq; prover="Rocq" ;; + lean4|lean) dir=lean4; prover="Lean 4" ;; + *) continue ;; + esac + gated="$(awk -F'|' '/^[[:space:]]*#/ || NF < 3 { next } $3 == "gated" { c++ } END { print c+0 }' "verification/proofs/$dir/MANIFEST")" + echo "$prover: ledger records a proven leg; $dir/MANIFEST lists $gated gated module(s)" + if [ "$gated" -lt 1 ]; then + echo "::error::zero-work: the ledger records a proven $prover leg but verification/proofs/$dir/MANIFEST lists no gated module" + bad=1 + fi + done < <(jq -r '.theorems[].legs[]? | select(.status == "proven" or .status == "proven-with-postulates") | .prover' "$LEDGER" | sort -u) + if [ "$bad" -ne 0 ]; then exit 1; fi + echo "no recheck leg is recorded proven, so zero compiled recheck modules is the honest count — not a pass" + + # The Agda SOURCE leg. PROOF-POLICY §1 makes Agda the source of truth; the + # ledger records it at a pinned commit and the audit checks that record. + # Typechecking it here keeps the recorded status true rather than assumed. + - name: Agda source leg (recorded in the ledger, re-typechecked here) run: | set -o pipefail - just proof-check-all 2>&1 | tee "$RUNNER_TEMP/proof-check-all.log" + just proof-check-agda 2>&1 | tee "$RUNNER_TEMP/proof-agda.log" + + # A green run means "the ledger is honest", NOT "the theorem is verified in + # an independent kernel". Say so on the check run itself, where it cannot + # be missed by someone who only reads the badge. + - name: Announce policy gaps (recorded, not verified) + run: | + set -uo pipefail + RECEIPT="$PROOF_RECEIPT_DIR/ledger.txt" + if [ ! -f "$RECEIPT" ]; then + echo "::error::no ledger receipt was written — the ledger gate did not run" + exit 0 + fi + GAPS="$(awk '/^gaps:/{f=1;next} /^[a-z-]+:/{f=0} f' "$RECEIPT" | sed 's/^ - //')" + if [ -z "${GAPS//[[:space:]]/}" ] || [ "$GAPS" = "(none)" ]; then + echo "no policy gaps recorded" + exit 0 + fi + while IFS= read -r gap; do + [ -z "${gap// }" ] && continue + echo "::warning::PROOF-POLICY §2 obligation UNMET (recorded as open, not verified):%0A${gap}" + done <<< "$GAPS" # Diagnostics only: the run is already red by the time this executes. # Proof failures are annotated so the failing module/error is visible in @@ -224,9 +384,9 @@ jobs: if: failure() run: | set -uo pipefail - LOG="$RUNNER_TEMP/proof-check-all.log" + LOG="$RUNNER_TEMP/proof-witness-check.log" if [ ! -f "$LOG" ]; then - echo "::error::proof-check-all produced no log (a step before it failed)" + echo "::error::proof-witness-check produced no log (an earlier step failed); see the step logs above" exit 0 fi # GitHub caps annotations at 10 per step and each annotation is @@ -234,9 +394,9 @@ jobs: # newline-encoded (%0A). That keeps the failing prover's own # diagnostic attached to the check run, not buried in runner logs. PAYLOAD="$(grep -vE '^[[:space:]]*$' "$LOG" | tail -n 100 | head -c 60000 | sed ':a;N;$!ba;s/\n/%0A/g')" - echo "::error::proof-check-all failed. Log tail:%0A${PAYLOAD}" + echo "::error::proof-witness-check failed. Log tail:%0A${PAYLOAD}" { - echo "### proof-check-all log tail (failure diagnostics)" + echo "### proof-witness-check log tail (failure diagnostics)" echo '```' tail -n 60 "$LOG" echo '```' diff --git a/.machine_readable/bot_directives/placement.a2ml b/.machine_readable/bot_directives/placement.a2ml index 68e7470..893ff4c 100644 --- a/.machine_readable/bot_directives/placement.a2ml +++ b/.machine_readable/bot_directives/placement.a2ml @@ -79,7 +79,7 @@ allowed-proofs = [ enforced-by = [ "just proof-enrolment (scripts/check-proof-enrolment.sh) -- FAILs when a proof is unlisted, when a registered entry has no file behind it, when this list and ALLOWED_PROOFS in scripts/check-coordination-boundary.sh disagree, or when zero proofs are enrolled; BLOCKED (exit 2) when a required prover is missing", "just proof-scan-dangerous (scripts/proof-scan-dangerous.sh) -- FAILs on believe_me/assert_total/postulate/sorry/Admitted/unsafeCoerce/Obj.magic outside comments", - ".github/workflows/proof-ci.yml -- runs the real all-proofs target (`just proof-check-all`) on proof, manifest, Justfile and workflow changes", + ".github/workflows/proof-ci.yml -- runs `just proof-witness-check` (audit verification/proofs/LEDGER.json, then compile every declared Rocq/Lean recheck leg) plus the both-ways instrument controls, on proof, ledger, manifest, tests/proofs, Justfile and workflow changes; a green run means the ledger is honest, NOT that XP-1 is verified in an independent kernel", ] route-elsewhere = [ "ABI/FFI/memory-layout proofs -> typed-wasm", diff --git a/Justfile b/Justfile index 1e3fdcd..cd60d77 100644 --- a/Justfile +++ b/Justfile @@ -1335,214 +1335,101 @@ help-me: # FORMAL VERIFICATION (PROOFS) # ═══════════════════════════════════════════════════════════════════════════════ -# Strictness contract for every proof recipe below (they are what CI runs via -# .github/workflows/proof-ci.yml): +# Proof work follows standards/3-practice/PROOF-POLICY.adoc: +# * theory is Agda (source of truth) and is RECHECKED in Rocq and Lean (§1, §2) +# * engineering is Idris2 (§1) +# * status is the closed vocabulary of §5: open | argued | tested-only | +# proven-with-postulates | proven +# * grades are mathesis/estate-mathematical-architecture §5 (Grade 3 → Grade 1) # -# exit 0 PASS the run actually checked something and it is clean -# exit 1 FAIL a proof failed, a proof is unlisted, or nothing was checked -# exit 2 BLOCKED a prover required by an enrolled proof is not installed +# This repository's proof CI examines the §2 recheck legs only — Rocq and Lean — +# and audits verification/proofs/LEDGER.json, which records every leg, its route, +# its axioms and the exact commit of the receipt. The Agda source leg is recorded +# and audited for form; it is not re-run in CI. # -# No silent skips, no `continue-on-error`, no green run on zero work. A prover -# with no enrolled sources prints "NONE" instead of claiming a pass, and -# `proof-enrolment` guarantees at least one proof source is checked overall. +# No silent skips anywhere: scripts/check-proofs.sh (the estate instrument) makes +# a missing prover FATAL, and scripts/check-proof-ledger.sh fails on a claim the +# evidence does not support. # -# Check all formal proofs — the real all-proofs target used by CI (strict) -proof-check-all: proof-enrolment proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous - @echo "=== All proof checks complete ===" +# The CI target: registry gates + ledger audit + every recheck leg declared +proof-witness-check: proof-enrolment proof-ledger-check proof-scan-dangerous proof-check-coq proof-check-lean4 # Enrolment gate: manifest <-> boundary allowlist <-> disk parity, required # provers present, zero-work guard, --safe/--without-K still in force. +# # Check proof enrolment (unlisted proofs, stale entries, missing provers) proof-enrolment: @bash scripts/check-proof-enrolment.sh --receipt "${PROOF_RECEIPT_DIR:-target/proof-receipts}/enrolment.txt" -# Check Idris2 proofs (ABI, types, dependent type proofs) -proof-check-idris2: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Idris2 proofs ===" - mapfile -t FILES < <(find verification/proofs/idris2 -name '*.idr' -type f 2>/dev/null | sort) - RECEIPT_DIR="${PROOF_RECEIPT_DIR:-target/proof-receipts}" - mkdir -p "$RECEIPT_DIR" - if [ "${#FILES[@]}" -eq 0 ]; then - echo "NONE: no Idris2 proof sources enrolled under verification/proofs/idris2" - printf 'idris2: none-enrolled (0 files)\n' >>"$RECEIPT_DIR/provers.txt" - exit 0 - fi - if ! command -v idris2 &>/dev/null; then - echo "BLOCKED: ${#FILES[@]} Idris2 proof source(s) present but 'idris2' is not on PATH." - echo " A missing prover is BLOCKED, never a skip and never a pass." - printf 'idris2: BLOCKED (prover missing, %d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" - exit 2 - fi - ERRORS=0 - for f in "${FILES[@]}"; do - echo -n " Checking $f ... " - if idris2 --check "$f"; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Idris2 proof(s) failed" - printf 'idris2: FAIL (%d failed of %d)\n' "$ERRORS" "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" - exit 1 - fi - echo "PASS: ${#FILES[@]} Idris2 proof(s) verified" - printf 'idris2: PASS (%d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" +# Comment-aware escape-hatch scan (believe_me, assert_total, postulate, sorry, +# Admitted, unsafeCoerce, Obj.magic). Fails on a hit outside a comment, and on a +# scan that finds no proof files at all. +# +# Scan proof sources for banned escape hatches +proof-scan-dangerous: + @bash scripts/proof-scan-dangerous.sh --receipt "${PROOF_RECEIPT_DIR:-target/proof-receipts}/dangerous-patterns.txt" -# Check Lean4 proofs +# Audit the proof ledger against PROOF-POLICY §5 and mathesis §5-§6 +proof-ledger-check: + @bash scripts/check-proof-ledger.sh --receipt "${PROOF_RECEIPT_DIR:-target/proof-receipts}/ledger.txt" + +# Compile Rocq recheck witnesses per verification/proofs/coq/MANIFEST. +# Fatal if coqc is absent: a missing prover is never a skip. +# +# Compile the declared Rocq recheck witnesses (missing coqc = fatal) +proof-check-coq: + @bash scripts/check-proofs.sh coq + +# Compile Lean 4 recheck witnesses per verification/proofs/lean4/MANIFEST. +# Fatal if lean is absent: a missing prover is never a skip. +# +# Compile the declared Lean 4 recheck witnesses (missing lean = fatal) proof-check-lean4: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Lean4 proofs ===" - mapfile -t FILES < <(find verification/proofs/lean4 -name '*.lean' -type f 2>/dev/null | sort) - RECEIPT_DIR="${PROOF_RECEIPT_DIR:-target/proof-receipts}" - mkdir -p "$RECEIPT_DIR" - if [ "${#FILES[@]}" -eq 0 ]; then - echo "NONE: no Lean4 proof sources enrolled under verification/proofs/lean4" - printf 'lean4: none-enrolled (0 files)\n' >>"$RECEIPT_DIR/provers.txt" - exit 0 - fi - if ! command -v lean &>/dev/null; then - echo "BLOCKED: ${#FILES[@]} Lean4 proof source(s) present but 'lean' is not on PATH." - echo " A missing prover is BLOCKED, never a skip and never a pass." - printf 'lean4: BLOCKED (prover missing, %d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" - exit 2 - fi - ERRORS=0 - for f in "${FILES[@]}"; do - echo -n " Checking $f ... " - if lean "$f"; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Lean4 proof(s) failed" - printf 'lean4: FAIL (%d failed of %d)\n' "$ERRORS" "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" - exit 1 - fi - echo "PASS: ${#FILES[@]} Lean4 proof(s) verified" - printf 'lean4: PASS (%d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" + @bash scripts/check-proofs.sh lean4 -# Check Agda proofs (--safe; the proof sources also carry --without-K) +# Re-typecheck the Agda SOURCE leg locally. Not part of the CI target: under +# PROOF-POLICY §1 the ledger records this leg, CI audits the record. Needs the +# nextgen-typing, standard-library, echo-types and absolute-zero libraries +# registered in /libraries + defaults. +# +# Re-typecheck the Agda source leg locally (needs registered libraries) proof-check-agda: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Agda proofs ===" - mapfile -t FILES < <(find verification/proofs/agda -name '*.agda' -type f 2>/dev/null | sort) - RECEIPT_DIR="${PROOF_RECEIPT_DIR:-target/proof-receipts}" - mkdir -p "$RECEIPT_DIR" - if [ "${#FILES[@]}" -eq 0 ]; then - echo "NONE: no Agda proof sources enrolled under verification/proofs/agda" - printf 'agda: none-enrolled (0 files)\n' >>"$RECEIPT_DIR/provers.txt" - exit 0 - fi - if ! command -v agda &>/dev/null; then - echo "BLOCKED: ${#FILES[@]} Agda proof source(s) present but 'agda' is not on PATH." - echo " Install Agda (see .github/workflows/proof-ci.yml for the pinned" - echo " toolchain and library registration). BLOCKED is not a pass." - printf 'agda: BLOCKED (prover missing, %d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" - exit 2 - fi - echo " toolchain: $(agda --version | head -n1)" - # Activate the repo's own Agda library manifest explicitly, by the name it - # declares. Without it Agda searches only the CWD, the registered defaults - # and its primitive library, so the proof directory is not an include root - # and every module fails with [ModuleNameDoesntMatchFileName] (observed on - # the first hosted run of proof-ci.yml). The manifest stays the authority - # for include paths and dependencies (standard-library, echo-types); it is - # not shadowed or replaced here. Register it once with: - # agda --print-agda-app-dir # then add the .agda-lib path to libraries - AGDA_LIB="verification/proofs/agda/nextgen-typing.agda-lib" - if [ ! -f "$AGDA_LIB" ]; then - echo "FAIL: Agda library manifest missing: $AGDA_LIB" - exit 1 - fi - AGDA_LIB_NAME="$(sed -n 's/^name:[[:space:]]*//p' "$AGDA_LIB" | head -n1 | tr -d '[:space:]')" - if [ -z "$AGDA_LIB_NAME" ]; then - echo "FAIL: $AGDA_LIB declares no library name" - exit 1 - fi - echo " library: $AGDA_LIB_NAME ($AGDA_LIB)" - ERRORS=0 - for f in "${FILES[@]}"; do - echo -n " Checking $f ... " - if agda --safe --library="$AGDA_LIB_NAME" "$f"; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Agda proof(s) failed" - printf 'agda: FAIL (%d failed of %d)\n' "$ERRORS" "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" - exit 1 - fi - echo "PASS: ${#FILES[@]} Agda proof(s) verified" - printf 'agda: PASS (%d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" + @bash scripts/check-proofs.sh agda -# Check Coq proofs -proof-check-coq: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Coq proofs ===" - mapfile -t FILES < <(find verification/proofs/coq -name '*.v' -type f 2>/dev/null | sort) - RECEIPT_DIR="${PROOF_RECEIPT_DIR:-target/proof-receipts}" - mkdir -p "$RECEIPT_DIR" - if [ "${#FILES[@]}" -eq 0 ]; then - echo "NONE: no Coq proof sources enrolled under verification/proofs/coq" - printf 'coq: none-enrolled (0 files)\n' >>"$RECEIPT_DIR/provers.txt" - exit 0 - fi - if ! command -v coqc &>/dev/null; then - echo "BLOCKED: ${#FILES[@]} Coq proof source(s) present but 'coqc' is not on PATH." - echo " A missing prover is BLOCKED, never a skip and never a pass." - printf 'coq: BLOCKED (prover missing, %d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" - exit 2 - fi - ERRORS=0 - for f in "${FILES[@]}"; do - echo -n " Checking $f ... " - if coqc "$f"; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Coq proof(s) failed" - printf 'coq: FAIL (%d failed of %d)\n' "$ERRORS" "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" - exit 1 - fi - echo "PASS: ${#FILES[@]} Coq proof(s) verified" - printf 'coq: PASS (%d files)\n' "${#FILES[@]}" >>"$RECEIPT_DIR/provers.txt" +# Compile Idris2 engineering proofs per verification/proofs/idris2/MANIFEST. +# This repository hosts none: engineering proofs belong in the owning repo. +# +# Compile Idris2 engineering proofs (this repository hosts none) +proof-check-idris2: + @bash scripts/check-proofs.sh idris2 -# Scan for banned escape hatches in proof files (comment-aware; zero-work fails) -proof-scan-dangerous: - @bash scripts/proof-scan-dangerous.sh --receipt "${PROOF_RECEIPT_DIR:-target/proof-receipts}/dangerous-patterns.txt" +# Full local sweep: ledger audit + every leg, including the Agda source leg. +# +# Full local sweep (registry gates + ledger + all four provers) +proof-check-all: proof-enrolment proof-ledger-check proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous -# Show proof status summary (counts on disk vs. registered in the manifest) +# Show the ledger: per theorem, its grade and each leg's status proof-status: #!/usr/bin/env bash - echo "=== Proof Status ===" + set -euo pipefail + LEDGER="verification/proofs/LEDGER.json" + echo "=== Proof status (source of truth: $LEDGER) ===" echo "" - echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' -type f 2>/dev/null | wc -l) files" - echo "Lean4: $(find verification/proofs/lean4 -name '*.lean' -type f 2>/dev/null | wc -l) files" - echo "Agda: $(find verification/proofs/agda -name '*.agda' -type f 2>/dev/null | wc -l) files" - echo "Coq: $(find verification/proofs/coq -name '*.v' -type f 2>/dev/null | wc -l) files" - echo "TLA+: $(find verification/proofs/tlaplus -name '*.tla' -type f 2>/dev/null | wc -l) files" + echo "Proof files on disk:" + echo " Agda: $(git ls-files -- 'verification/proofs/agda/*.agda' 2>/dev/null | wc -l)" + echo " Rocq: $(git ls-files -- 'verification/proofs/coq/*.v' 2>/dev/null | wc -l)" + echo " Lean4: $(git ls-files -- 'verification/proofs/lean4/*.lean' 2>/dev/null | wc -l)" + echo " Idris2: $(git ls-files -- 'verification/proofs/idris2/*.idr' 2>/dev/null | wc -l)" echo "" - echo "Registered in .machine_readable/bot_directives/placement.a2ml:" - bash scripts/check-proof-enrolment.sh --static-only | sed -n '/proof sources on disk/,/^$/p' + if [ ! -f "$LEDGER" ]; then + echo "FAIL: no ledger at $LEDGER" + exit 1 + fi + echo "Ledger:" + jq -r '.theorems[] | " \(.id) [\(.kind)] grade \(.grade) source=\(.source.prover):\(.source.status)", (.legs[]? | " leg \(.prover): \(.status)\(if .status == "open" then " (" + (.blocker // "no blocker recorded") + ")" else "" end)")' "$LEDGER" echo "" + echo "Policy gaps are printed by: just proof-ledger-check" + # ═══════════════════════════════════════════════════════════════════════════════ # SESSION MANAGEMENT (THIN BINDINGS TO CENTRAL STANDARDS) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 884b334..664b0de 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -68,12 +68,21 @@ When adding one, register it in `+[verification].allowed-proofs+` of CI rejects any PR introducing these. The enforcement is `+just proof-scan-dangerous+` (`+scripts/proof-scan-dangerous.sh+`, run inside -`+just proof-check-all+`), plus the enrolment gate +`+just proof-check-all+`) and the ledger gate +`+just proof-ledger-check+` (`+scripts/check-proof-ledger.sh+`, run in CI and +inside every sweep), plus the enrolment gate (`+scripts/check-proof-enrolment.sh+`) which fails any proof that is not registered in both `+[verification].allowed-proofs+` of `+placement.a2ml+` and `+ALLOWED_PROOFS+` of `+scripts/check-coordination-boundary.sh+`. Hosted lane: -`+.github/workflows/proof-ci.yml+`. +`+.github/workflows/proof-ci.yml+`, which runs `+just proof-witness-check+` — +the ledger audit plus every recheck leg the ledger declares — after the +both-ways instrument controls in `+tests/proofs/run-controls.sh+`. + +Status vocabulary (PROOF-POLICY §5) and grades (mathesis +`+estate-mathematical-architecture+` §5) live in `+PROOF-STATUS.adoc+` and are +recorded machine-readably in `+verification/proofs/LEDGER.json+`. Today XP-1 is +*Grade 3* (Agda only) with its Rocq and Lean 4 recheck legs `+open+`. === References diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 7d8b1a3..868a305 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -3,59 +3,149 @@ ____ Coordination repo. The only proofs tracked here are *cross-project* proofs (spanning ≥2 constituent repos). Single-project proof status is -tracked in the owning repos. Requirements: `+PROOF-NEEDS.md+`. +tracked in the owning repos. Requirements: `+PROOF-NEEDS.adoc+`. ____ -=== Summary +The machine-readable record of every proof is +`+verification/proofs/LEDGER.json+`. This page is a *summary of that ledger*; +where the two disagree the ledger is authoritative and +`+just proof-ledger-check+` fails. Nothing here is a percentage, a confidence +estimate, or a count of "done" work: mathesis §6 requires the exact form — +Open / Claimed, the grade, the axiom list, and the commit the receipt was taken +at. -[cols=",,,,",options="header",] +=== The one theorem + +[cols="10%,12%,9%,26%,21%,22%",options="header",] +|=== +|ID |Kind |Grade |Source leg |Rocq recheck leg |Lean 4 recheck leg +|XP-1 |theory |*3* |Agda — `+proven+` +(`+EchoTyping.agda+`, `+Verification.agda+`) +|*open* — no witness |*open* — no witness +|=== + +`+XP-1+` states that the pipeline's information-losing typing operations +(AffineScript affine weakening; refinement erasure into the +typed-wasm/kernel layer) are instances of echo-types' fiber construction. + +=== What the grade means + +mathesis `+estate-mathematical-architecture+` §5 defines the rungs. *Grade 3* +is the lowest: a proof carried by Agda alone, under `+--safe --without-K+`, and +*not translated* to another prover. That is exactly and only what is +established here. + +The rungs above it (`+2i+` = one independent prover, `+2ii+` = two +fundamentally distinct architectures, `+1+` = machine-checked through a +verified checker API) are *not established*. They are named here only so the +gap is unmistakable: *no leg other than Agda has been proven for XP-1.* + +* `+2i+` needs exactly one independent system (Lean 4 or Rocq) to carry the + statement. Neither does. +* `+2ii+` needs two, *and* the family caveat applies: Agda, Rocq and Lean are + all dependently-typed (DTT/CIC). Translating between them does not produce a + second architecture, so `+2ii+` is unreachable from the Agda/Rocq/Lean + family alone — it would need a non-DTT leg such as Isabelle/HOL. +* `+1+` needs the statement checked through a verified checker API (AXLE for + Lean, coq-lsp's REST surface for Rocq, isabelle-server). No such surface is + wired up. + +=== The recheck obligation, stated plainly + +`+standards/3-practice/PROOF-POLICY.adoc+` §1 makes Agda the source of truth +for theory proofs and §2 makes Rocq *and* Lean the recheck legs: each theorem +must be *transported* (Dedukti/Lambdapi) or *re-proved by hand*, the route and +the statement comparison recorded, and no Mathlib allowed. **That obligation is +currently unmet for XP-1.** Both legs are recorded `+open+` in the ledger, with +the blocker that stops each one, and the gate prints them as `+POLICY GAP+` +lines on every run. An `+open+` leg is a legal state in the §5 vocabulary; it +is not verification, and no part of this page or of CI claims that it is. + +[cols="14%,30%,56%",options="header",] |=== -|Category |Total |Done |In Progress |Remaining -|Cross-project (XP) |1 |1 |0 |0 -|*Total* |*1* |*1* |*0* |*0* +|Leg |Status |What would have to happen (the recorded blocker) +|Rocq |*open* |Transport the Agda term through Dedukti/Lambdapi (recording the +statement comparison and the `+Print Assumptions+` output), or re-prove the +statement by hand in Rocq. No `+TypeSafety.v+`-style witness exists here yet — +the Rocq MANIFEST is a header explaining this, and +`+just proof-check-coq+` therefore compiles zero modules while the ledger +refuses any claim that they were compiled. + +|Lean 4 |*open* |Same choice, re-proved by hand in core Lean: Mathlib is +forbidden by §2, and until a released Lambdapi Lean exporter exists there is no +transport route to use. `+#print axioms+` must then show no axiom, and +`+sorryAx+` must not appear. |=== -The earlier "`0 of 7`" RSR ABI/TP figure was template residue: it -counted mandatory ABI/FFI + typing proofs that belong in `+typed-wasm+` -/ `+typell+`, not in this coordination layer. Those scaffold files were -removed (the ABI proof obligations are owned by `+typed-wasm+`). +=== Assumptions and axiom tracking + +mathesis §6 requires the axioms behind a proof to be tracked, not assumed away: +`+#print axioms+` in Lean, `+Print Assumptions+` in Rocq. Those are kernel +queries, and they are the only accepted evidence that a compiled witness is +closed — compiling is not: Rocq accepts `+Admitted+` and Lean accepts `+sorry+` +with exit status 0. Since no witness exists on either leg there is no axiom +list for them yet; recording one would be fabrication. -=== Proofs Present +The Agda source leg rests on these pinned, recorded assumptions (all in the +ledger): -[width="100%",cols="12%,15%,15%,17%,13%,28%",options="header",] +[cols="30%,70%",options="header",] |=== -|ID |Proof |Spans |Prover |File |Verified By -|XP-1 |Pipeline information-loss = echo-types fibers |echo-types ↔ -affinescript ↔ typed-wasm |Agda (`+--safe --without-K+`) -|`+verification/proofs/agda/EchoTyping.agda+` -|`+just proof-check-all+` in `.github/workflows/proof-ci.yml` +|Component |Pin +|Agda |2.8.0 +|agda-stdlib |v2.3 (`+8326c7475af1fa456ca04a0203c168d5d7ff842b+`) +|echo-types |`+b0982c44f36133acd2d0e1d4e03cf031fff7a470+` +|absolute-zero |`+f486c29903434589117fa0662c6f29b0f17d1d5f+` +|Receipt commit |`+4c6b918998b9756fdeb1e64c74de27a968677ac1+` (run 41299544043) |=== === Enforcement (CI) -Until 2026-11-01 these proofs were *asserted*: `+just proof-check-all+` -existed but no workflow invoked it, and every prover recipe ended in -`+SKIP: not installed+` followed by `+exit 0+`. Worse, a prover -directory with no sources still printed `+PASS+`, and the banned-pattern scan -matched the prose "zero postulates" in `+EchoTyping.agda+` while ignoring real -escape hatches inside block comments. The lane below closes all three. +Nothing on this page is trusted because it is written here. Each claim is +gated, and every gate refuses rather than skips: [cols="30%,70%",options="header",] |=== |Guard |Behaviour +|`+just proof-ledger-check+` +(`+scripts/check-proof-ledger.sh+`) +|Audits `+LEDGER.json+` against PROOF-POLICY §5 and mathesis §5-§6: schema and +closed status vocabulary; a grade the proven legs do not support (a moved leg +with no artifact, no MANIFEST entry, no route, no statement comparison or no +axiom list); `+proven+` carrying axioms; `+proven-with-postulates+` without +them; a Mathlib import; escape hatches; undeclared axioms; registry drift +between the MANIFESTs, `+ALLOWED_PROOFS+` and the files on disk; a witness on +disk that neither the ledger nor a MANIFEST claims; and this page claiming a +grade the ledger does not record. Open legs are printed as `+POLICY GAP+`, and +are never counted as verification. + +|`+just proof-witness-check+` +|The CI target: the enrolment and banned-pattern gates, the ledger audit, and +*every recheck leg the ledger declares* (`+proof-check-coq+`, `+proof-check-lean4+`). Today both legs are declared open, +so the manifests compile nothing and the gate says so — the lane is green on +"the ledger is honest", never on "the theorem is verified". + +|`+tests/proofs/run-controls.sh+` +|PROOF-POLICY §7 requires a gate to be verified *both ways*. These controls +feed the instrument a closed Rocq proof and a closed Lean proof (must be +accepted, `+Print Assumptions+` / `+#print axioms+` must report them closed and +axiom-free), a proof closed with `+Admitted+` and one closed with `+sorry+` +(must be rejected), a ledger claiming a grade with no leg behind it, and a +witness planted on disk that no ledger row claims. A control that stops +failing is a broken instrument, and the run goes red. Where `+coqc+` or +`+lean+` is absent the controls report **BLOCKED**, never a pass. + |`+just proof-enrolment+` (`+scripts/check-proof-enrolment.sh+`) |Parses `+[verification].allowed-proofs+` (placement.a2ml) and `+ALLOWED_PROOFS+` (`+scripts/check-coordination-boundary.sh+`) and requires them to agree. Fails when a proof source is unlisted, when a registered entry has no file behind it, when zero proofs are enrolled, or when an `.agda` proof -loses `+--safe+`/`+--without-K+`. A required prover missing from `PATH` is -**BLOCKED** (exit 2) — never a skip, never a pass. +loses `+--safe+`/`+--without-K+`. |`+just proof-check-agda+` (and the Idris2/Lean4/Coq equivalents) |Exits 2 (BLOCKED) when proofs for that prover are enrolled but the prover is -absent; exits 1 on any typecheck failure; prints `+NONE+` instead of `+PASS+` -when that prover has no enrolled sources. +absent; exits 1 on any typecheck failure. |`+just proof-scan-dangerous+` (`+scripts/proof-scan-dangerous.sh+`) @@ -64,62 +154,59 @@ when that prover has no enrolled sources. on any hit outside a comment, and fails when it scans zero files. |`.github/workflows/proof-ci.yml` -|Hosted lane running `+just proof-check-all+` on pushes/PRs that touch -`+verification/proofs/**+`, the two registries, the gate scripts, `+Justfile+` -or the workflow itself. Pins Agda 2.8.0 (official binary, sha256-verified), -agda-stdlib v2.3 (tag + commit asserted), `+just+` 1.59.0, and +|Hosted lane running `+just proof-witness-check+` (plus the Agda source leg and +the both-ways controls) on pushes/PRs that touch `+verification/proofs/**+`, +`+tests/proofs/**+`, the two registries, the gate scripts, `+Justfile+` or the +workflow itself. Pins Agda 2.8.0 (official binary, sha256-verified), +agda-stdlib v2.3 (tag + commit asserted), `+just+` 1.59.0, Rocq, Lean 4, and echo-types / absolute-zero by commit. No `+continue-on-error+`, no -skip-on-missing-tool. Receipts are uploaded as the `+proof-receipts+` artifact. +skip-on-missing-tool. |=== === Verification [source,bash] ---- -# Everything, exactly as CI runs it (this is the real all-proofs target): +# What CI runs — ledger audit + every declared recheck leg: +just proof-witness-check + +# The instrument verified both ways (needs coqc + lean; BLOCKED without them): +bash tests/proofs/run-controls.sh + +# The ledger at a glance (grade, and each leg's status and blocker): +just proof-status + +# Everything, local only — the ledger plus all four provers: just proof-check-all -# Just the registry/manifest gate (no prover needed): +# Registry gate, no prover needed: bash scripts/check-proof-enrolment.sh --static-only - -# One prover, directly. The repo's own library manifest must be activated or -# Agda reports [ModuleNameDoesntMatchFileName] for every module (receipt: -# proof-ci run 41299261152, 2026-11-01). Register once with -# `agda --print-agda-app-dir`, then add -# verification/proofs/agda/nextgen-typing.agda-lib -# plus the `standard-library`, `echo-types` and `absolute-zero` manifests -# (echo-types' own manifest depends on absolute-zero) to -# /libraries: -agda --safe --library=nextgen-typing verification/proofs/agda/Verification.agda - -# Enforce the coordination boundary (no project code / non-allowlisted proofs) -bash scripts/check-coordination-boundary.sh ---- -=== Enforcement receipts +=== Receipts [cols="16%,20%,64%",options="header",] |=== |Date |Receipt |Result -|2026-11-01 |proof-ci run -https://github.com/hyperpolymath/nextgen-typing/actions/runs/41299544043 -(sha `+4c6b918+`) |**PASS** — `+just proof-check-all+` green on the hosted -lane: enrolment gate PASS (2 proof sources, 3 registered entries, registries -agree), Agda 2.8.0 typecheck of `+EchoTyping.agda+` and `+Verification.agda+` -under `+--safe --library=nextgen-typing+` against agda-stdlib v2.3, -echo-types `+b0982c4+` and absolute-zero `+f486c29+`, banned-pattern scan -clean. This is the first CI receipt that these proofs typecheck. +|2026-11-01 |proof-ci run 41299544043 (sha `+4c6b918+`) |**PASS** for the Agda +source leg: enrolment gate PASS (2 proof sources, registered entries agree), +Agda 2.8.0 typecheck of `+EchoTyping.agda+` and `+Verification.agda+` under +`+--safe --library=nextgen-typing+` against agda-stdlib v2.3, echo-types +`+b0982c4+` and absolute-zero `+f486c29+`, banned-pattern scan clean. This is +the receipt pinned in the ledger for the Agda leg — it is *not* a receipt for +XP-1 as a whole. |2026-11-01 |proof-ci runs 41298824595, 41299096293 (first attempts) |**FAIL**, and correctly so: the proofs had never actually been run, and the old documented invocation did not activate `+nextgen-typing.agda-lib+`, so every module failed with `+[ModuleNameDoesntMatchFileName]+`. Fixed by activating the -library in the recipe; no proof source or safety flag was changed. +library; no proof source or safety flag was changed. -|2026-11-01 |local receipts (this repository, no Agda installed) |Enrolment -gate `+--static-only+`: **PASS** (2 sources, 3 registered entries). -Banned-pattern scan: **PASS** (2 files). `+just proof-check-all+`: -**BLOCKED** (exit 2, Agda absent) — recorded as blocked, not as a pass. +|2026-11-01 |local receipts (no prover toolchain installed) |Enrolment gate +`+--static-only+`: **PASS**. Banned-pattern scan: **PASS** (2 files). +`+just proof-witness-check+` and the both-ways controls: **BLOCKED** — no +`+agda+`, `+coqc+` or `+lean+` here. Recorded as blocked (PROOF-POLICY §6: say +so instead of reporting the leg as passing), not as a pass. |=== === Changelog @@ -127,6 +214,13 @@ Banned-pattern scan: **PASS** (2 files). `+just proof-check-all+`: [width="100%",cols="32%,42%,26%",options="header",] |=== |Date |Change |By +|2026-11-01 |Status re-anchored to `+verification/proofs/LEDGER.json+` in the +policy's vocabulary. XP-1 recorded as *Grade 3* (Agda only); Rocq and Lean 4 +recheck legs recorded `+open+` under PROOF-POLICY §2, with their blockers. The +"1 of 1 done" figure is withdrawn: it inflated a single-prover proof into a +finished one (mathesis §11). Gate `+scripts/check-proof-ledger.sh+` added, plus +both-ways controls `+tests/proofs/run-controls.sh+` |Arena agent + |2026-11-01 |Proofs are now *enforced*, not asserted: `+just proof-check-all+` runs in `.github/workflows/proof-ci.yml`; enrolment gate fails unlisted/stale/ zero-work runs and blocks on a missing prover. Lane green at `+4c6b918+` diff --git a/scripts/check-coordination-boundary.sh b/scripts/check-coordination-boundary.sh index 46e16f7..e6a1009 100755 --- a/scripts/check-coordination-boundary.sh +++ b/scripts/check-coordination-boundary.sh @@ -45,7 +45,12 @@ is_allowed_proof() { if [ -d verification/proofs ]; then while IFS= read -r f; do case "$f" in - *.a2ml | *.adoc | *.md | *.gitkeep) continue ;; # docs/metadata are fine + # Proof METADATA is not a proof: the per-prover MANIFEST (the compile + # gate's input, scripts/check-proofs.sh) and LEDGER.json (the policy + # ledger, audited by scripts/check-proof-ledger.sh) are tracked here + # deliberately, but they are not hosted proofs. + *.a2ml | *.adoc | *.md | *.gitkeep) continue ;; + */MANIFEST | *.json) continue ;; esac if ! is_allowed_proof "$f"; then err "Proof outside the cross-project allowlist: $f @@ -60,7 +65,30 @@ fi # --- 3. No implementation/proof source languages outside verification/proofs/ # The coordination repo holds docs, .a2ml, k9/ncl, shell, and CI — not Rust, # Zig, Idris, Agda, Lean, Coq, Isabelle, Haskell, or OCaml source. +# Narrow, self-policing exception: tests/proofs/control/ holds the both-ways +# controls for the proof gate (PROOF-POLICY §7). They exist to be pointed at the +# instrument, not to prove anything, so the allowance is deliberately tiny and +# each fixture must police itself: +# * it must declare what it is in a header comment ("INSTRUMENT CONTROL"), and +# * it must stay <= 20 lines. A fixture that grows into a real proof has +# escaped the boundary, which is precisely what this check exists to stop. +INSTRUMENT_MARKER='INSTRUMENT CONTROL' +INSTRUMENT_MAX_LINES=20 while IFS= read -r f; do + case "$f" in + tests/proofs/control/*) + if grep -qF "$INSTRUMENT_MARKER" "$f" \ + && [ "$(wc -l < "$f")" -le "$INSTRUMENT_MAX_LINES" ]; then + continue + fi + err "Instrument fixture outside its narrow allowance: $f + tests/proofs/control/ may hold only tiny self-declaring controls: a header + comment containing '$INSTRUMENT_MARKER' and at most $INSTRUMENT_MAX_LINES + lines. Anything larger, or undeclared, is proof code escaping the + coordination boundary — host it in the owning repo instead." + continue + ;; + esac err "Implementation source outside the coordination boundary: $f Compiler / kernel / proof code belongs in the owning project repo (see $ROUTE)." done < <( diff --git a/scripts/check-proof-enrolment.sh b/scripts/check-proof-enrolment.sh index 547a3cb..b4fbf4c 100755 --- a/scripts/check-proof-enrolment.sh +++ b/scripts/check-proof-enrolment.sh @@ -154,8 +154,16 @@ while IFS= read -r entry; do done <<<"$boundary_list" # --- 2. enumerate what is actually on disk ---------------------------------- +# Proof METADATA is not a proof. The per-prover MANIFEST (the compile list read +# by scripts/check-proofs.sh) and LEDGER.json (the policy ledger, audited by +# scripts/check-proof-ledger.sh) are deliberately tracked under $PROOFS_DIR, but +# registering them in allowed-proofs/ALLOWED_PROOFS would mean registering the +# gate's own inputs as proofs. They are excluded here exactly as they are in +# scripts/check-coordination-boundary.sh, and the ledger gate cross-checks them +# against each other and against this registry. disk_files="$(git ls-files -- "$PROOFS_DIR" \ | grep -Ev '\.(a2ml|adoc|md)$|(^|/)\.gitkeep$' \ + | grep -Ev '(^|/)MANIFEST$|(^|/)LEDGER\.json$' \ | sort)" disk_proofs="$(while IFS= read -r f; do diff --git a/scripts/check-proof-ledger.sh b/scripts/check-proof-ledger.sh new file mode 100755 index 0000000..5d63dc5 --- /dev/null +++ b/scripts/check-proof-ledger.sh @@ -0,0 +1,599 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-proof-ledger.sh — proof-LEDGER gate for nextgen-typing. +# +# What this refuses to do, and why: +# +# * It does NOT re-run the Agda theory proof. Under +# standards/3-practice/PROOF-POLICY.adoc §1 a theory proof's source of +# truth is Agda and its §2 recheck legs are Rocq and Lean. Those legs are +# what this repository's proof CI examines (Coq/Rocq and Lean 4 only). +# The Agda leg is *recorded* — with the commit and run that checked it — +# and audited for form here, not re-derived. +# * It does NOT accept a grade the evidence does not support. mathesis +# `estate-mathematical-architecture` §5/§6 defines Grade 3 (Agda only, +# not translated) through Grade 1 (machine-checked through a verified +# checker API), and §6 requires exact recording rather than a confidence +# percentage. A ledger that claims a travelled leg must have the artifact, +# the manifest entry, the route, the statement comparison and the axiom +# list behind it, or this gate fails. +# * It does NOT report a clean run when there was nothing to audit: zero +# theorems, a theorem with no source file, or a theory theorem with no +# recheck legs listed are failures, not passes. +# +# An `open` leg is a LEGAL status (PROOF-POLICY §5). When a leg is open this +# gate prints a POLICY GAP line naming the leg and the policy clause it owes, +# and nothing in the output claims that the theorem is verified. +# +# Usage: +# bash scripts/check-proof-ledger.sh [--ledger PATH] [--receipt PATH] +# bash scripts/check-proof-ledger.sh --scan-file PATH # both-ways control +# +# Exit: 0 = PASS (every claim is backed, every open leg recorded) +# 1 = FAIL (a claim is unsupported, or bookkeeping does not add up) +# 2 = BLOCKED (gate could not audit: jq/git/policy input unavailable) + +set -uo pipefail + +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "$ROOT" || exit 2 + +LEDGER="verification/proofs/LEDGER.json" +RECEIPT="" +SCAN_FILE="" +PROOFS_DIR="verification/proofs" +MANIFEST_SOURCE=".machine_readable/bot_directives/placement.a2ml" +BOUNDARY_SCRIPT="scripts/check-coordination-boundary.sh" +DOCS_STATUS="PROOF-STATUS.adoc" + +while [ "$#" -gt 0 ]; do + case "$1" in + --ledger) LEDGER="${2:-}"; shift 2 ;; + --ledger=*) LEDGER="${1#--ledger=}"; shift ;; + --receipt) RECEIPT="${2:-}"; shift 2 ;; + --receipt=*) RECEIPT="${1#--receipt=}"; shift ;; + --scan-file) SCAN_FILE="${2:-}"; shift 2 ;; + --scan-file=*) SCAN_FILE="${1#--scan-file=}"; shift ;; + -h|--help) sed -n '2,40p' "$0"; exit 0 ;; + *) echo "unknown argument: $1" >&2; exit 2 ;; + esac +done + +FAILS=() +NOTES=() +GAPS=() +fail() { FAILS+=("$1"); } +note() { NOTES+=("$1"); } + +# --------------------------------------------------------------------------- +# Escape-hatch scan (shared by the repo audit and the both-ways control). +# Comment-aware: PROOF-POLICY keeps escape-hatch *policy* in +# docs/TRUSTED-BASE-REDUCTION-POLICY.adoc, and a prose mention of a banned +# construct is not a hole. Block comments {- -} and (* *) and line comments +# -- and // are stripped before matching, with line numbers preserved. +# --------------------------------------------------------------------------- +scan_escape_hatches() { + # $1 = file. Prints "line:token:text" for each real hit. + local file="$1" stripped + stripped="$(awk ' + BEGIN { block = 0 } + { + line = $0; out = ""; i = 1; n = length(line) + while (i <= n) { + two = substr(line, i, 2) + if (block == 1) { + if (two == "-}" || two == "*)") { block = 0; i += 2 } else { i += 1 } + continue + } + if (two == "--" || two == "//") { break } + if (two == "{-" || two == "(*") { block = 1; i += 2; continue } + out = out substr(line, i, 1); i += 1 + } + print out + }' "$file")" + # Hard bans: no status in PROOF-POLICY §5 can be carried by these. + printf '%s\n' "$stripped" \ + | grep -nE '\b(believe_me|assert_total|postulate|sorry|admit|Admitted|unsafeCoerce)\b|\bObj[.]magic\b|\bsorryAx\b' \ + || true +} + +# Declared axioms are different from escape hatches: PROOF-POLICY §5 allows +# `proven-with-postulates` when the axioms are named and allowed by +# TRUSTED-BASE-REDUCTION-POLICY. Collect them so the ledger can be cross-checked. +scan_declared_axioms() { + local file="$1" + case "$file" in + *.v) grep -nE '^[[:space:]]*(Axiom|Parameter|Conjecture)[[:space:]]' "$file" || true ;; + *.lean) grep -nE '^[[:space:]]*axiom[[:space:]]' "$file" || true ;; + *) true ;; + esac +} + +# --------------------------------------------------------------------------- +# --scan-file mode: the instrument's own control surface (PROOF-POLICY §7 — +# a gate must be shown to pass conforming input AND fail a planted violation). +# --------------------------------------------------------------------------- +if [ -n "$SCAN_FILE" ]; then + if [ ! -f "$SCAN_FILE" ]; then + echo "BLOCKED: --scan-file target does not exist: $SCAN_FILE" >&2 + exit 2 + fi + hits="$(scan_escape_hatches "$SCAN_FILE")" + if [ -n "$hits" ]; then + echo "FAIL: escape hatches in $SCAN_FILE" + echo "$hits" | sed 's/^/ line /' + exit 1 + fi + echo "PASS: no escape hatches in $SCAN_FILE" + exit 0 +fi + +# --------------------------------------------------------------------------- +# Inputs. A gate that cannot read its inputs must say so; it must not pass. +# --------------------------------------------------------------------------- +command -v jq >/dev/null 2>&1 || { echo "BLOCKED: jq is required to audit the ledger" >&2; exit 2; } + +[ -f "$LEDGER" ] || { echo "BLOCKED: proof ledger not found: $LEDGER" >&2; exit 2; } +jq -e . "$LEDGER" >/dev/null 2>&1 || { echo "BLOCKED: proof ledger is not valid JSON: $LEDGER" >&2; exit 2; } + +echo "=== Proof ledger gate ===" +echo "ledger: $LEDGER" +echo "policy: standards/3-practice/PROOF-POLICY.adoc" +echo "grades: mathesis/estate-mathematical-architecture §5-§6" +echo "" + +# Closed vocabulary, verbatim from PROOF-POLICY §5 (canonical lowercase tokens). +VOCAB='["argued","open","proven","proven-with-postulates","tested-only"]' +# Prover families, from mathesis §5 (the Grade 2ii diversity rule). +FAMILIES='{"agda":"dtt","rocq":"dtt","lean4":"dtt","idris2":"dtt","isabelle":"hol","tla+":"state-machine","smt":"smt"}' + +# --- 1. schema + non-empty --------------------------------------------------- +schema="$(jq -r '.schema // ""' "$LEDGER")" +[ "$schema" = "hyperpolymath/proof-ledger/1" ] \ + || fail "schema: expected 'hyperpolymath/proof-ledger/1', got '${schema}'" + +theorem_count="$(jq -r '.theorems | if type=="array" then length else -1 end' "$LEDGER")" +if [ "$theorem_count" -le 0 ]; then + fail "zero-work: the ledger must declare at least one theorem (it declares ${theorem_count})" +fi + +# --- 2. closed vocabulary, kinds, ids, grades -------------------------------- +while IFS= read -r bad; do + [ -n "$bad" ] && fail "status token outside PROOF-POLICY §5 vocabulary: '${bad}'" +done < <(jq -r --argjson vocab "$VOCAB" ' + [ .theorems[] | (.source.status // ""), (.legs[]?.status // "") ][] + | select(. as $s | $vocab | index($s) | not)' "$LEDGER" | sort -u) + +while IFS= read -r bad; do + [ -n "$bad" ] && fail "theorem kind must be 'theory' or 'engineering' (PROOF-POLICY §1): '${bad}'" +done < <(jq -r '[.theorems[].kind // ""][] | select(. != "theory" and . != "engineering")' "$LEDGER" | sort -u) + +while IFS= read -r dup; do + [ -n "$dup" ] && fail "duplicate theorem id in ledger: '${dup}'" +done < <(jq -r '[.theorems[].id] | group_by(.)[] | select(length > 1) | .[0]' "$LEDGER") + +while IFS= read -r bad; do + [ -n "$bad" ] && fail "grade must be one of 3, 2i, 2ii, 1 (mathesis §5): '${bad}'" +done < <(jq -r '[.theorems[].grade // "" | tostring][] | select(. != "3" and . != "2i" and . != "2ii" and . != "1")' "$LEDGER" | sort -u) + +# --- 3. per-theorem: legs, grades, claims ------------------------------------ +# Emitted as TSV so bash can drive the filesystem checks. +jq -r ' + .theorems[] | + [ .id, + .kind, + (.grade | tostring), + ([.legs[]?.prover] | join(",")), + ([.legs[]? | select(.status != "open")] | length), + ([.legs[]? | select(.status == "proven" or .status == "proven-with-postulates")] | length) + ] | @tsv' "$LEDGER" > /tmp/proof-ledger-rows.$$.tsv +trap 'rm -f /tmp/proof-ledger-rows.$$.tsv' EXIT + +declare -A THEOREM_PROVEN=() +while IFS=$'\t' read -r tid kind grade provers claimed proven; do + [ -z "$tid" ] && continue + THEOREM_PROVEN["$tid"]="$proven" + + # PROOF-POLICY §1/§2: theory is Agda, rechecked in Rocq AND Lean. + if [ "$kind" = "theory" ]; then + for required in rocq lean4; do + case ",$provers," in + *",$required,"*) ;; + *) fail "$tid: theory theorem is missing the '$required' recheck leg required by PROOF-POLICY §2 (legs: ${provers:-none})" ;; + esac + done + fi + + case "$grade" in + 3) + if [ "$proven" -gt 0 ]; then + fail "$tid: grade 3 claims no translated leg, but $proven leg(s) are recorded proven (mathesis §5)" + fi + ;; + 2i) + if [ "$proven" -ne 1 ]; then + fail "$tid: grade 2i requires exactly one proven recheck leg, ledger records $proven (mathesis §5)" + fi + ;; + 2ii) + if [ "$proven" -lt 2 ]; then + fail "$tid: grade 2ii requires two proven legs, ledger records $proven (mathesis §5)" + fi + non_dtt="$(jq -r --argjson fam "$FAMILIES" --arg id "$tid" ' + [ .theorems[] | select(.id == $id) | .legs[]? + | select(.status == "proven" or .status == "proven-with-postulates") + | select($fam[.prover // ""] != null and $fam[.prover] != "dtt") ] | length' "$LEDGER")" + if [ "${non_dtt:-0}" -lt 1 ]; then + fail "$tid: grade 2ii needs one proven leg outside the DTT/CIC family (mathesis §5 — Agda, Rocq and Lean are the same family); none recorded" + fi + ;; + 1) + api="$(jq -r --arg id "$tid" ' + [ .theorems[] | select(.id == $id) | .legs[]? + | select(.status == "proven" or .status == "proven-with-postulates") + | .api_receipt.api // empty ] | length' "$LEDGER")" + if [ "${api:-0}" -lt 1 ]; then + fail "$tid: grade 1 requires a verified-checker API receipt (AXLE, coq-lsp, isabelle-server — mathesis §5); none recorded" + fi + ;; + esac + + if [ "$claimed" -gt 0 ]; then + GAPS+=("$tid: $claimed leg(s) carry a non-open status and MUST compile in this lane") + fi +done < /tmp/proof-ledger-rows.$$.tsv + +# --- 4. every non-open claim must be backed by artifact + MANIFEST + route --- +while IFS=$'\t' read -r tid prover status artifact route compared axioms reproof; do + [ -z "$tid" ] && continue + [ "$status" = "open" ] && continue + + if [ -z "$artifact" ] || [ "$artifact" = "null" ]; then + fail "$tid/$prover: status '$status' recorded with no artifact" + continue + fi + if [ ! -f "$artifact" ]; then + fail "$tid/$prover: artifact listed but missing on disk: $artifact" + continue + fi + + # The artifact must be gated in the prover's MANIFEST, or the compile step + # (scripts/check-proofs.sh) would never touch it. + case "$prover" in + rocq) mdir="$PROOFS_DIR/coq" ;; + lean4) mdir="$PROOFS_DIR/lean4" ;; + agda) mdir="$PROOFS_DIR/agda" ;; + idris2) mdir="$PROOFS_DIR/idris2" ;; + *) mdir="" ;; + esac + if [ -n "$mdir" ]; then + if [ ! -f "$mdir/MANIFEST" ]; then + fail "$tid/$prover: $mdir/MANIFEST is missing, so $artifact cannot be compiled by the lane" + elif ! grep -vE '^[[:space:]]*(#|$)' "$mdir/MANIFEST" | grep -qF "|$(basename "$artifact")|"; then + fail "$tid/$prover: $artifact is not listed in $mdir/MANIFEST (unlisted witness)" + fi + fi + + # PROOF-POLICY §2.3: record the route; §2.1: without a statement comparison + # the leg is ASSUMED (argued), not PROVEN. + case "$route" in + transported|re-proved) ;; + *) fail "$tid/$prover: status '$status' requires route 'transported' or 're-proved' (PROOF-POLICY §2.3), got '${route}'" ;; + esac + if [ "$route" = "re-proved" ] && { [ -z "$reproof" ] || [ "$reproof" = "null" ]; }; then + fail "$tid/$prover: route 're-proved' requires a reproof_reason (PROOF-POLICY §2.2)" + fi + if [ "$status" = "proven" ] || [ "$status" = "proven-with-postulates" ]; then + case "$compared" in + ""|null|none) + fail "$tid/$prover: '$status' requires a statement comparison (PROOF-POLICY §2.1); without it the leg is 'argued'" ;; + esac + fi + + # §5: axioms are named, and only proven-with-postulates may have any. + axiom_count="$(jq -r --arg id "$tid" --arg p "$prover" ' + [ .theorems[] | select(.id == $id) | .legs[]? | select(.prover == $p) + | (.axioms // []) | length ] | .[0] // -1' "$LEDGER")" + if [ "${axiom_count:--1}" -lt 0 ]; then + fail "$tid/$prover: 'axioms' must be recorded as a list (empty when none) — mathesis §6 axiom tracking" + elif [ "$status" = "proven" ] && [ "$axiom_count" -ne 0 ]; then + fail "$tid/$prover: status 'proven' but $axiom_count axiom(s) recorded; that is 'proven-with-postulates' (§5)" + elif [ "$status" = "proven-with-postulates" ] && [ "$axiom_count" -eq 0 ]; then + fail "$tid/$prover: status 'proven-with-postulates' with an empty axiom list (§5: list the axioms)" + fi + + # §2: no Mathlib. A proof that needs a large external library is a + # dependency, not a proof the estate owns. + if [ "$prover" = "lean4" ] && grep -qE '^[[:space:]]*import[[:space:]]+Mathlib' "$artifact"; then + fail "$tid/$prover: $artifact imports Mathlib, which PROOF-POLICY §2 forbids" + fi +done < <(jq -r ' + .theorems[] as $t | $t.legs[]? | + [ $t.id, .prover, (.status // ""), (.artifact // ""), (.route // ""), + (if (.statement_compared // null) == null then "" else (.statement_compared | tostring) end), + (if (.axioms // null) == null then "" else "recorded" end), + (.reproof_reason // "") ] | @tsv' "$LEDGER") + +# --- 5. source legs: files, receipts, safety flags --------------------------- +while IFS=$'\t' read -r tid status files; do + [ -z "$tid" ] && continue + if [ -z "$files" ] || [ "$files" = "null" ]; then + fail "$tid: source leg lists no files (zero-work)" + continue + fi + IFS=',' read -r -a file_list <<<"$files" + for f in "${file_list[@]}"; do + [ -z "$f" ] && continue + [ -f "$f" ] || fail "$tid: source file listed but missing: $f" + done + + if [ "$status" = "proven" ] || [ "$status" = "proven-with-postulates" ]; then + read -r ekind ecommit edate erun < <(jq -r --arg id "$tid" ' + .theorems[] | select(.id == $id) | .source.evidence? | + [ (.kind // ""), (.commit // ""), (.date // ""), (.run // "") ] | @tsv' "$LEDGER") + for pair in "kind:${ekind:-}" "commit:${ecommit:-}" "date:${edate:-}" "run:${erun:-}"; do + if [ -z "${pair#*:}" ]; then + fail "$tid: source leg recorded '$status' without evidence '$pair' (mathesis §6: the receipt names the commit)" + fi + done + # mathesis §6: the receipt names the exact commit it verified. The commit + # must be a full SHA-1. Reachability is advisory, not fatal: a squash or + # rebase merge rewrites the commit that a green run was recorded against, + # and a gate that cannot survive the repository's own merge style would be + # turned off rather than fixed. + if [ -n "${ecommit:-}" ] && ! printf '%s' "$ecommit" | grep -qE '^[0-9a-f]{40}$'; then + fail "$tid: evidence commit '$ecommit' is not a full 40-character SHA-1" + elif [ -n "${ecommit:-}" ]; then + if git cat-file -e "${ecommit}^{commit}" 2>/dev/null; then + note "$tid: receipt commit ${ecommit:0:8} is reachable from this clone" + else + note "$tid: receipt commit ${ecommit:0:8} is not reachable here (squash/rebase merge?) — refresh the receipt" + fi + fi + fi +done < <(jq -r '.theorems[] | [ .id, (.source.status // ""), ((.source.files // []) | join(",")) ] | @tsv' "$LEDGER") + +# Agda safety flags stay in force (this repository's PROOF-NEEDS.adoc). +while IFS= read -r f; do + [ -z "$f" ] && continue + grep -qE '\{-#[[:space:]]*OPTIONS[^#]*--safe' "$f" \ + || fail "missing safety flag: $f does not declare --safe in its OPTIONS pragma" + grep -qE '\{-#[[:space:]]*OPTIONS[^#]*--without-K' "$f" \ + || fail "missing safety flag: $f does not declare --without-K in its OPTIONS pragma" +done < <(jq -r '.theorems[].source.files[]? | select(endswith(".agda"))' "$LEDGER" | sort -u) + +# --- 6. escape hatches + declared axioms in every proof/witness source ------- +declare -A DECLARED_AXIOMS=() +while IFS=$'\t' read -r tid _p axioms; do + [ -z "$tid" ] && continue + case "$axioms" in + ""|null) continue ;; + esac + IFS=',' read -r -a ax_list <<<"$axioms" + for a in "${ax_list[@]}"; do + [ -n "$a" ] && DECLARED_AXIOMS["$a"]=1 + done +done < <(jq -r '.theorems[] as $t | $t.legs[]? | [ $t.id, .prover, ((.axioms // []) | join(",")) ] | @tsv' "$LEDGER") + +scan_one() { + local f="$1" hits + hits="$(scan_escape_hatches "$f")" + if [ -n "$hits" ]; then + fail "escape hatch in $f: +$(printf '%s\n' "$hits" | sed 's/^/ line /')" + fi + local ax + ax="$(scan_declared_axioms "$f")" + if [ -n "$ax" ]; then + while IFS= read -r line; do + [ -z "$line" ] && continue + name="$(printf '%s\n' "$line" | sed -E 's/^[0-9]+:[[:space:]]*(Axiom|Parameter|Conjecture|axiom)[[:space:]]+([A-Za-z0-9_′]+).*/\2/')" + if [ -z "${DECLARED_AXIOMS[$name]:-}" ]; then + fail "undeclared axiom in $f:$line — PROOF-POLICY §5 requires every axiom to be named in the ledger (proven-with-postulates)" + fi + done <<<"$ax" + fi +} + +if git rev-parse --is-inside-work-tree >/dev/null 2>&1; then + PROOF_FILES="$(git ls-files -- "$PROOFS_DIR" | grep -E '\.(agda|lagda|idr|v|lean|tla)$' | sort)" +else + PROOF_FILES="$(find "$PROOFS_DIR" -type f \( -name '*.agda' -o -name '*.idr' -o -name '*.v' -o -name '*.lean' -o -name '*.tla' \) 2>/dev/null | sort)" +fi +scanned=0 +while IFS= read -r f; do + [ -z "$f" ] && continue + scanned=$((scanned + 1)) + scan_one "$f" +done <<<"$PROOF_FILES" + +if [ "$scanned" -eq 0 ]; then + fail "zero-work: no proof source or witness was scanned under $PROOFS_DIR" +fi + +# --- 7. witnesses on disk must be claimed in the ledger ---------------------- +# Enumerated the same way as section 6: `git ls-files` inside a work tree, a +# plain `find` otherwise. Using git alone here would make the check silently +# vacuous in an exported tree (no .git) — a null check that reports OK, which is +# the exact failure mode the estate instrument exists to prevent. +list_witnesses() { # $1 = prover dir under $PROOFS_DIR, $2 = extension + if git rev-parse --is-inside-work-tree >/dev/null 2>&1; then + git ls-files -- "$PROOFS_DIR/$1" 2>/dev/null | grep -E "\.$2\$" | sort + else + find "$PROOFS_DIR/$1" -type f -name "*.$2" 2>/dev/null | sort + fi +} +LEDGER_ARTIFACTS="$(jq -r '.theorems[].legs[]?.artifact // empty' "$LEDGER" | sort -u)" +for dir in coq lean4; do + ext=v; [ "$dir" = "lean4" ] && ext=lean + while IFS= read -r f; do + [ -z "$f" ] && continue + if ! printf '%s\n' "$LEDGER_ARTIFACTS" | grep -Fxq -- "$f"; then + fail "witness on disk is not claimed in the ledger: $f + Add a leg row with artifact '$f' (route, axioms, statement comparison) — an + unclaimed witness is exactly the silent-drift case mathesis §11 rejects." + fi + done < <(list_witnesses "$dir" "$ext") +done + +# --- 8. cross-project registry: manifest <-> boundary allowlist <-> disk ----- +normalize_list_entries() { + sed 's/#.*//' | tr -d "\"' \t\r" | sed 's/,*$//' | grep -v '^$' | sort +} + +if [ -f "$MANIFEST_SOURCE" ] && [ -f "$BOUNDARY_SCRIPT" ]; then + manifest_list="$(awk ' + /^\[/ { in_section = ($0 ~ /^\[verification\]/); next } + in_section && /^[[:space:]]*allowed-proofs[[:space:]]*=[[:space:]]*\[/ { in_list = 1; next } + in_list && /^[[:space:]]*\][[:space:]]*$/ { in_list = 0; next } + in_list { print } + ' "$MANIFEST_SOURCE" | normalize_list_entries)" + + boundary_list="$(awk ' + /^ALLOWED_PROOFS=\(/ { in_list = 1; next } + in_list && /^\)/ { in_list = 0; next } + in_list { print } + ' "$BOUNDARY_SCRIPT" | normalize_list_entries)" + + [ -n "$manifest_list" ] || fail "cross-project registry is empty in $MANIFEST_SOURCE" + [ -n "$boundary_list" ] || fail "cross-project allowlist is empty in $BOUNDARY_SCRIPT" + + while IFS= read -r entry; do + [ -z "$entry" ] && continue + grep -Fxq -- "$entry" <<<"$boundary_list" \ + || fail "registry drift: '$entry' is in $MANIFEST_SOURCE but not in ALLOWED_PROOFS of $BOUNDARY_SCRIPT" + [ -e "$entry" ] || fail "stale registry entry: '$entry' is registered but absent from disk" + done <<<"$manifest_list" + + while IFS= read -r entry; do + [ -z "$entry" ] && continue + grep -Fxq -- "$entry" <<<"$manifest_list" \ + || fail "registry drift: '$entry' is in ALLOWED_PROOFS of $BOUNDARY_SCRIPT but not in $MANIFEST_SOURCE" + done <<<"$boundary_list" + + # Proof sources on disk must be registered (the anti-drift rule). + while IFS= read -r f; do + [ -z "$f" ] && continue + grep -Fxq -- "$f" <<<"$manifest_list" \ + || fail "unlisted proof source: $f + Register it in [verification].allowed-proofs of $MANIFEST_SOURCE AND in + ALLOWED_PROOFS of $BOUNDARY_SCRIPT." + done <<<"$PROOF_FILES" +else + fail "cross-project registry inputs missing ($MANIFEST_SOURCE / $BOUNDARY_SCRIPT)" +fi + +# --- 9. documentation must not claim a grade the ledger does not support ----- +if [ -f "$DOCS_STATUS" ]; then + grep -qF 'LEDGER.json' "$DOCS_STATUS" \ + || fail "$DOCS_STATUS does not point at the proof ledger (LEDGER.json): status prose is unanchored" + while IFS= read -r tid; do + [ -z "$tid" ] && continue + grep -qF -- "$tid" "$DOCS_STATUS" \ + || fail "$DOCS_STATUS does not mention theorem '$tid' from the ledger" + done < <(jq -r '.theorems[].id' "$LEDGER" | sort -u) + + proven_total=0 + for k in "${!THEOREM_PROVEN[@]}"; do proven_total=$((proven_total + ${THEOREM_PROVEN[$k]})); done + if [ "$proven_total" -eq 0 ]; then + if grep -qE 'Grade[[:space:]]+(2i|2ii|2|1)\b|grade[[:space:]]+(2i|2ii|2|1)\b' "$DOCS_STATUS"; then + fail "$DOCS_STATUS claims a Grade 2/1 result but the ledger records no proven recheck leg (mathesis §5/§11)" + fi + fi +else + fail "proof status document missing: $DOCS_STATUS" +fi + +# --- 10. open legs are reported, never hidden and never counted ---------- +while IFS=$'\t' read -r tid prover status blocker; do + [ -z "$tid" ] && continue + [ "$status" = "open" ] || continue + GAPS+=("$tid: $prover leg is OPEN${blocker:+ — $blocker}") +done < <(jq -r '.theorems[] as $t | $t.legs[]? | select(.status == "open") | [ $t.id, .prover, .status, (.blocker // "") ] | @tsv' "$LEDGER") + +# --- 11. verdict ---------------------------------------------------------- +proven_legs=0 +for k in "${!THEOREM_PROVEN[@]}"; do proven_legs=$((proven_legs + ${THEOREM_PROVEN[$k]})); done + +if [ "${#NOTES[@]}" -gt 0 ]; then + echo "--- notes ---" + printf ' - %s\n' "${NOTES[@]}" + echo "" +fi + +echo "--- ledger census ---" +echo " theorems: $theorem_count" +echo " proof sources: $scanned scanned" +echo " proven legs: $proven_legs" +echo "" + +if [ "${#GAPS[@]}" -gt 0 ]; then + echo "--- POLICY GAPS (legal to record; NOT counted as verification) ---" + printf ' ! %s\n' "${GAPS[@]}" + echo "" +fi + +status="PASS" +[ "${#FAILS[@]}" -gt 0 ] && status="FAIL" + +if [ -n "$RECEIPT" ]; then + mkdir -p "$(dirname "$RECEIPT")" 2>/dev/null || true + { + echo "proof-ledger receipt" + echo "generated: $(date -u +%Y-%m-%dT%H:%M:%SZ)" + echo "commit: ${GITHUB_SHA:-$(git rev-parse HEAD 2>/dev/null || echo unknown)}" + echo "runner: ${RUNNER_NAME:-local}/${RUNNER_OS:-$(uname -s)}" + echo "status: $status" + echo "policy: standards/3-practice/PROOF-POLICY.adoc" + echo "grade-model: mathesis/estate-mathematical-architecture §5-§6" + echo "theorems: $theorem_count" + echo "proof-sources-scanned: $scanned" + echo "proven-recheck-legs: $proven_legs" + echo "ledger-sha256: $(sha256sum "$LEDGER" | cut -d' ' -f1)" + echo "gaps:" + if [ "${#GAPS[@]}" -eq 0 ]; then echo " (none)"; else printf ' - %s\n' "${GAPS[@]}"; fi + if [ "${#FAILS[@]}" -gt 0 ]; then + echo "failures:" + printf ' - %s\n' "${FAILS[@]}" + fi + } >"$RECEIPT" + echo "receipt written: $RECEIPT" + if [ -n "${GITHUB_STEP_SUMMARY:-}" ]; then + { + echo "## Proof ledger gate — **$status**" + echo "" + echo "| item | value |" + echo "|------|-------|" + echo "| theorems | $theorem_count |" + echo "| proof sources scanned | $scanned |" + echo "| proven recheck legs (Rocq/Lean) | $proven_legs |" + echo "| policy gaps | ${#GAPS[@]} |" + echo "" + if [ "${#GAPS[@]}" -gt 0 ]; then + echo "Policy gaps (recorded, not verified):" + printf -- '- %s\n' "${GAPS[@]}" + echo "" + fi + } >>"$GITHUB_STEP_SUMMARY" + fi +fi + +if [ "${#FAILS[@]}" -gt 0 ]; then + echo "=== FAIL: ${#FAILS[@]} ledger violation(s) ===" + printf ' x %s\n' "${FAILS[@]}" + echo "" + echo "Nothing above was treated as verified. Fix the ledger, the artifacts, or the" + echo "registries; do not relax the vocabulary to make this gate pass." + exit 1 +fi + +echo "✅ PASS: every recorded claim is backed by an artifact, a manifest entry, a" +echo " route and a statement comparison; open legs are recorded, not hidden." +if [ "$proven_legs" -eq 0 ]; then + echo " NOTE: 0 recheck legs are proven (Rocq: 0, Lean: 0). No Grade 2i/2ii/1" + echo " claim is made by this repository and nothing here says the theorem was" + echo " verified in an independent kernel." +fi +exit 0 diff --git a/scripts/check-proofs.sh b/scripts/check-proofs.sh new file mode 100755 index 0000000..5eba30f --- /dev/null +++ b/scripts/check-proofs.sh @@ -0,0 +1,183 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-proofs.sh prover in: idris2 | lean4 | agda | coq +# +# The single source of truth for "do the proofs in this repo compile?". +# build/just/proofs.just calls this (`just proof-check-`), and CI should +# too, so a green local run and a green CI run mean the same thing. +# +# It replaces four separate "checks that could not fail" that let non-compiling +# proofs sit in estate repos for months while every status file said "proved": +# +# 1. `command -v || { echo SKIP; exit 0; }` — a MISSING TOOLCHAIN +# reported success. A gate that cannot run must never report OK: it +# manufactures false confidence, which is worse than having no gate. +# 2. ` --check ` — Idris2 (and friends) derive the +# expected module name from the path they are handed, so a module checked +# from the wrong directory fails on a name mismatch rather than its real +# errors, and verdicts invert. Every module here is checked from its own +# SOURCE ROOT (declared in the MANIFEST). +# 3. Path-filtered CI that only looked at one directory — nothing checked the +# rest. Here, a proof file present on disk but absent from the MANIFEST is +# an ERROR, so new proofs are gated by default, not by remembering. +# 4. `idris2 --check X && ok` — `idris2 --check` EXITS 0 ON A MISSING IMPORT +# (verified against 0.7.0) while printing `Error: ...`. Testing the exit +# code alone is unsound; for idris2 we require exit 0 AND no `Error:` line. +# +# They share one shape: a null check that emits reassuring text. If you extend +# this script, the test to apply is not "does it pass?" but "have I watched it +# fail?". +# +# CONVENTION: proofs live under verification/proofs// ; the MANIFEST for +# a prover is verification/proofs//MANIFEST, one entry per line: +# +# ||gated|quarantine| +# +# source-root : directory the prover is invoked from, chosen so the module's +# declared name matches its path (getting this wrong is hole #2). +# gated : MUST compile. A failure fails this script and CI. +# quarantine : known-broken, tracked in docs/status/ROADMAP.adoc. Must CONTINUE to fail; +# if one starts compiling the script fails and tells you to +# promote it, so the list cannot rot into a permanent excuse. +# +# Blank lines and lines starting with # are ignored. +# +# Exit: 0 = every gated module compiles AND every quarantined module still fails +# AND every proof file on disk is listed; 1 = otherwise; 2 = misuse. + +set -euo pipefail + +PROVER="${1:-}" +case "$PROVER" in + idris2|lean4|agda|coq) ;; + *) echo "usage: $(basename "$0") " >&2; exit 2 ;; +esac + +# This script lives in /scripts/ ; run everything from the repo root. +cd "$(dirname "${BASH_SOURCE[0]}")/.." +ROOT="$PWD" +PROOF_DIR="verification/proofs/$PROVER" +MANIFEST_FILE="$PROOF_DIR/MANIFEST" + +# --- per-prover configuration ------------------------------------------------- +# CMD : executable that must be on PATH (absent => FAIL, never skip). +# EXT : file extension, for the "unlisted proof" coverage scan. +# ERROR_RE : if non-empty, output must not match it even when the exit code is 0. +# Only idris2 needs this (its --check exits 0 on a missing import); +# for lean4 it is a harmless belt-and-braces guard. +case "$PROVER" in + idris2) CMD=idris2; EXT=idr; ERROR_RE='^Error:' ;; + lean4) CMD=lean; EXT=lean; ERROR_RE='error:' ;; + agda) CMD=agda; EXT=agda; ERROR_RE='' ;; + coq) CMD=coqc; EXT=v; ERROR_RE='' ;; +esac + +check_one() { + # $1 source-root (rel to ROOT), $2 module (rel to source-root). + # Sets LAST_OUT to the tool output on failure; returns 0 iff the module compiles. + local root="$1" rel="$2" out rc + set +e + case "$PROVER" in + idris2) out="$(cd "$ROOT/$root" && idris2 --check "$rel" 2>&1)"; rc=$? ;; + lean4) out="$(cd "$ROOT/$root" && lean "$rel" 2>&1)"; rc=$? ;; + agda) out="$(cd "$ROOT/$root" && agda --safe --without-K --cubical-compatible "$rel" 2>&1)"; rc=$? ;; + coq) out="$(cd "$ROOT/$root" && coqc "$rel" 2>&1)"; rc=$? ;; + esac + set -e + if [ "$rc" -eq 0 ] && { [ -z "$ERROR_RE" ] || ! grep -qE "$ERROR_RE" <<<"$out"; }; then + LAST_OUT=""; return 0 + fi + LAST_OUT="$out"; return 1 +} + +echo "=== $PROVER proof check ===" + +# --- toolchain: absent means FAIL, never skip --------------------------------- +if ! command -v "$CMD" >/dev/null 2>&1; then + { + echo "FAIL: '$CMD' not found on PATH." + echo + echo "This is deliberately fatal. The previous recipe did 'exit 0' here with" + echo "\"SKIP: $CMD not installed\", so every $PROVER proof reported green on any" + echo "machine that could not check it. Install the $PROVER toolchain, or run" + echo "this in CI where the workflow installs it." + } >&2 + exit 1 +fi +"$CMD" --version 2>/dev/null | head -1 || true +echo + +# --- a repo with proofs but no MANIFEST is itself a failure ------------------- +if [ ! -f "$MANIFEST_FILE" ]; then + if [ -d "$PROOF_DIR" ] && [ -n "$(find "$PROOF_DIR" -name "*.$EXT" 2>/dev/null)" ]; then + echo "FAIL: $PROOF_DIR contains .$EXT proofs but has no MANIFEST." >&2 + echo " Create $MANIFEST_FILE listing each as 'gated' or 'quarantine'." >&2 + exit 1 + fi + echo "no $PROOF_DIR/*.$EXT proofs and no MANIFEST — nothing to check." + exit 0 +fi + +fails=0 +unexpected_pass=0 +listed_tmp="$(mktemp)" +trap 'rm -f "$listed_tmp"' EXIT + +while IFS='|' read -r root rel status note; do + # skip blank lines and comments + [ -z "${root// }" ] && continue + case "${root#"${root%%[![:space:]]*}"}" in \#*) continue ;; esac + printf ' %-30s %-24s ' "$root" "$rel" + echo "$root/$rel" >>"$listed_tmp" + if check_one "$root" "$rel"; then + if [ "$status" = gated ]; then + echo "PASS" + else + echo "PASS -- UNEXPECTED (quarantined module now compiles)" + echo " Promote '$rel' to 'gated' in $MANIFEST_FILE and update docs/status/ROADMAP.adoc." + unexpected_pass=$((unexpected_pass + 1)) + fi + else + if [ "$status" = gated ]; then + echo "FAIL" + printf '%s\n' "${LAST_OUT//$'\n'/$'\n '}" | sed '1s/^/ /' + fails=$((fails + 1)) + else + echo "fail (quarantined, expected)" + [ -n "${note// }" ] && echo " reason:$note" + fi + fi +done < "$MANIFEST_FILE" + +# --- coverage: every proof on disk must be listed ----------------------------- +# The anti-recurrence rule: proofs went unchecked for months because nothing +# forced them onto anyone's list. A file absent from the MANIFEST is an error. +echo +echo "=== manifest coverage ($PROOF_DIR) ===" +listed="$(sort -u "$listed_tmp")" +found="$(cd "$ROOT" && find "$PROOF_DIR" -name "*.$EXT" -not -path '*/build/*' 2>/dev/null | sort)" +unlisted="$(comm -13 <(printf '%s\n' "$listed") <(printf '%s\n' "$found") || true)" +missing="$(comm -23 <(printf '%s\n' "$listed") <(printf '%s\n' "$found") || true)" + +if [ -n "${unlisted//[[:space:]]/}" ]; then + echo "FAIL: .$EXT proofs on disk but absent from $MANIFEST_FILE:" + printf ' %s\n' $unlisted + echo " List each as 'gated' or 'quarantine'; new proofs are gated by default." + fails=$((fails + 1)) +fi +if [ -n "${missing//[[:space:]]/}" ]; then + echo "FAIL: MANIFEST lists modules that do not exist (stale entries):" + printf ' %s\n' $missing + fails=$((fails + 1)) +fi +[ -z "${unlisted//[[:space:]]/}${missing//[[:space:]]/}" ] && \ + echo " all $(printf '%s\n' "$found" | grep -c .) .$EXT file(s) accounted for" + +echo +if [ "$fails" -gt 0 ] || [ "$unexpected_pass" -gt 0 ]; then + echo "RESULT: FAIL ($fails failure(s), $unexpected_pass unexpected pass(es))" + exit 1 +fi +echo "RESULT: PASS -- gated modules compile; quarantined modules still fail as recorded" diff --git a/tests/proofs/control/Control.lean b/tests/proofs/control/Control.lean new file mode 100644 index 0000000..ba0a71a --- /dev/null +++ b/tests/proofs/control/Control.lean @@ -0,0 +1,6 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- INSTRUMENT CONTROL — NOT an estate proof. +-- Shows the Lean half of the instrument: `#print axioms` reports that a closed +-- proof depends on nothing (mathesis §6 axiom tracking). Must be accepted. +theorem control_true : True := True.intro +#print axioms control_true diff --git a/tests/proofs/control/Control.v b/tests/proofs/control/Control.v new file mode 100644 index 0000000..af106f2 --- /dev/null +++ b/tests/proofs/control/Control.v @@ -0,0 +1,8 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* INSTRUMENT CONTROL — NOT an estate proof. + This file proves nothing about the type-theory pipeline. It exists so the + proof CI instrument can be shown to work BOTH ways, as PROOF-POLICY §7 + requires (a gate passes conforming input and fails a planted violation): + a closed Rocq proof must be accepted, and its Print Assumptions must say so. *) +Theorem control_true : True. +Proof. exact I. Qed. diff --git a/tests/proofs/control/PlantedAdmitted.v b/tests/proofs/control/PlantedAdmitted.v new file mode 100644 index 0000000..e59aea2 --- /dev/null +++ b/tests/proofs/control/PlantedAdmitted.v @@ -0,0 +1,7 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* INSTRUMENT CONTROL — PLANTED VIOLATION (must be rejected). + `Admitted` closes a proof with an escape hatch. The instrument must refuse + it: the ledger gate's escape-hatch scan fails on the token, and the kernel's + Print Assumptions must NOT report the result as closed. *) +Theorem planted_true : True. +Proof. Admitted. diff --git a/tests/proofs/control/PlantedSorry.lean b/tests/proofs/control/PlantedSorry.lean new file mode 100644 index 0000000..972e578 --- /dev/null +++ b/tests/proofs/control/PlantedSorry.lean @@ -0,0 +1,7 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- INSTRUMENT CONTROL — PLANTED VIOLATION (must be rejected). +-- Lean compiles `sorry` and exits 0, so an exit code is NOT evidence of a +-- closed proof. The instrument relies on `#print axioms` (which shows sorryAx) +-- and on the ledger gate's escape-hatch scan. Both must reject this file. +theorem planted_true : True := sorry +#print axioms planted_true diff --git a/tests/proofs/run-controls.sh b/tests/proofs/run-controls.sh new file mode 100755 index 0000000..3a3d7ee --- /dev/null +++ b/tests/proofs/run-controls.sh @@ -0,0 +1,171 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# run-controls.sh — prove the proof-witness instrument works BOTH ways. +# +# standards/3-practice/PROOF-POLICY.adoc §7 requires a policy gate to be +# verified "both ways": it passes conforming input AND fails a deliberately +# planted violation. A gate that has only ever been seen to pass is +# indistinguishable from one that cannot fail. +# +# The controls are tiny fixtures under tests/proofs/control/. They are NOT +# estate proofs and they live outside verification/proofs/, so no census, no +# ledger and no catalogue ever counts them as mathematics. +# +# Assertions: +# 1. Rocq closed control -> coqc accepts, Print Assumptions: closed +# 2. Rocq planted `Admitted` -> escape-hatch scan REJECTS it, and the +# kernel does not report it closed +# 3. Lean 4 closed control -> lean accepts, #print axioms: no axioms +# 4. Lean 4 planted `sorry` -> #print axioms shows sorryAx, scan REJECTS +# 5. Ledger gate -> rejects a planted "grade 2i, legs open" +# claim (no evidence behind the grade) +# 6. Ledger gate -> rejects a witness planted on disk but not +# claimed in the ledger or the MANIFEST +# +# Exit: 0 every control behaved as required; 1 an expectation was violated; +# 2 BLOCKED — a prover the controls need is not installed here. +# BLOCKED is never reported as a pass (PROOF-POLICY §6). + +set -uo pipefail + +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)" +cd "$ROOT" || exit 2 + +CONTROLS="tests/proofs/control" +GATE="scripts/check-proof-ledger.sh" +LEDGER="verification/proofs/LEDGER.json" +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT + +VIOLATIONS=0 +ok() { echo " ✅ $*"; } +viol() { echo " ❌ $*"; VIOLATIONS=$((VIOLATIONS + 1)); } + +echo "=== Proof-witness instrument controls (PROOF-POLICY §7, both ways) ===" +echo "fixtures: $CONTROLS" +echo "" + +# --- toolchain: absent means BLOCKED, never a pass --------------------------- +missing=() +for tool in coqc coqtop lean; do + command -v "$tool" >/dev/null 2>&1 || missing+=("$tool") +done +if [ "${#missing[@]}" -gt 0 ]; then + echo "BLOCKED: the controls need ${missing[*]} on PATH, and the instrument cannot" + echo " be shown to work without them. This is NOT a pass (PROOF-POLICY §6)." + exit 2 +fi +echo "coqc: $(coqc --version 2>/dev/null | head -1)" +echo "lean: $(lean --version 2>/dev/null | head -1)" +echo "" + +# --- 1/2. Rocq: closed proof accepted, planted Admitted rejected ------------ +cp "$CONTROLS/Control.v" "$WORK/Control.v" +if ( cd "$WORK" && coqc -q Control.v ) >"$WORK/coqc-control.log" 2>&1; then + ok "1. coqc accepts the closed control (Control.v)" +else + viol "1. coqc rejected the closed control; the instrument is broken, not strict" + sed 's/^/ /' "$WORK/coqc-control.log" | head -20 +fi +assumptions="$( cd "$WORK" && printf 'Require Import Control.\nPrint Assumptions control_true.\n' | coqtop -quiet 2>&1 )" +if printf '%s' "$assumptions" | grep -q "Closed under the global context"; then + ok "1. Print Assumptions reports the closed control as closed" +else + viol "1. Print Assumptions did not report 'Closed under the global context'" + printf '%s\n' "$assumptions" | sed 's/^/ /' | head -20 +fi + +cp "$CONTROLS/PlantedAdmitted.v" "$WORK/PlantedAdmitted.v" +if ( cd "$WORK" && coqc -q PlantedAdmitted.v ) >"$WORK/coqc-planted.log" 2>&1; then + # Coq accepts Admitted at compile time; that is exactly why an exit code is + # not evidence. The scan must catch it. + ok "2. coqc accepts the planted Admitted control (exit code alone is not evidence)" +else + ok "2. coqc rejected the planted Admitted control outright" +fi +if bash "$GATE" --scan-file "$CONTROLS/PlantedAdmitted.v" >/dev/null 2>&1; then + viol "2. the escape-hatch scan ACCEPTED a proof closed with Admitted" +else + ok "2. the escape-hatch scan rejects the planted Admitted control" +fi +if bash "$GATE" --scan-file "$CONTROLS/Control.v" >/dev/null 2>&1; then + ok "2. the escape-hatch scan accepts the closed control (no false positive)" +else + viol "2. the escape-hatch scan rejected the closed control (false positive)" +fi +planted_assumptions="$( cd "$WORK" && printf 'Require Import PlantedAdmitted.\nPrint Assumptions planted_true.\n' | coqtop -quiet 2>&1 )" +if printf '%s' "$planted_assumptions" | grep -q "Closed under the global context"; then + viol "2. the kernel reported the Admitted control as closed — axiom tracking is blind" +else + ok "2. the kernel does not report the Admitted control as closed" +fi + +# --- 3/4. Lean 4: closed proof accepted, planted sorry detected ------------- +lean_clean="$( cd "$CONTROLS" && lean Control.lean 2>&1 )" +if printf '%s' "$lean_clean" | grep -q "does not depend on any axioms"; then + ok "3. #print axioms reports the closed Lean control as axiom-free" +else + viol "3. #print axioms did not report the closed Lean control as axiom-free" + printf '%s\n' "$lean_clean" | sed 's/^/ /' | head -20 +fi +lean_planted="$( cd "$CONTROLS" && lean PlantedSorry.lean 2>&1 )" +if printf '%s' "$lean_planted" | grep -q "sorryAx"; then + ok "4. #print axioms exposes sorryAx in the planted Lean control" +else + viol "4. #print axioms did not expose sorryAx — Lean axiom tracking is blind" + printf '%s\n' "$lean_planted" | sed 's/^/ /' | head -20 +fi +if bash "$GATE" --scan-file "$CONTROLS/PlantedSorry.lean" >/dev/null 2>&1; then + viol "4. the escape-hatch scan ACCEPTED a proof closed with sorry" +else + ok "4. the escape-hatch scan rejects the planted Lean sorry control" +fi +if bash "$GATE" --scan-file "$CONTROLS/Control.lean" >/dev/null 2>&1; then + ok "4. the escape-hatch scan accepts the closed Lean control (no false positive)" +else + viol "4. the escape-hatch scan rejected the closed Lean control (false positive)" +fi + +# --- 5. a grade with no evidence behind it must be refused ------------------ +jq '(.theorems[0].grade) = "2i"' "$LEDGER" > "$WORK/planted-grade.json" +if bash "$GATE" --ledger "$WORK/planted-grade.json" >"$WORK/planted-grade.log" 2>&1; then + viol "5. the ledger gate ACCEPTED a grade 2i claim with no translated leg" +else + ok "5. the ledger gate refuses a grade 2i claim with no proven leg behind it" +fi +if grep -q "grade 2i requires exactly one proven recheck leg" "$WORK/planted-grade.log"; then + ok "5. and it says which clause was violated" +else + viol "5. the ledger gate failed for an unexpected reason" + sed 's/^/ /' "$WORK/planted-grade.log" | tail -10 +fi + +# --- 6. a witness on disk with no ledger row must be refused --------------- +sandbox="$WORK/repo" +mkdir -p "$sandbox" +tar --exclude=.git --exclude=target -cf - . 2>/dev/null | ( cd "$sandbox" && tar -xf - ) +printf 'Theorem unlisted_witness : True.\nProof. exact I. Qed.\n' \ + > "$sandbox/verification/proofs/coq/UnlistedWitness.v" +if ( cd "$sandbox" && bash scripts/check-proof-ledger.sh ) >"$WORK/unlisted.log" 2>&1; then + viol "6. the ledger gate ACCEPTED a witness that is in neither the ledger nor the MANIFEST" +else + ok "6. the ledger gate refuses an unlisted witness on disk" +fi +if grep -q "witness on disk is not claimed in the ledger" "$WORK/unlisted.log"; then + ok "6. and it names the unclaimed witness" +else + viol "6. the unlisted-witness control failed for an unexpected reason" + sed 's/^/ /' "$WORK/unlisted.log" | tail -10 +fi + +echo "" +if [ "$VIOLATIONS" -gt 0 ]; then + echo "FAIL: $VIOLATIONS control expectation(s) violated — the instrument does not behave as" + echo " claimed, so a green proof lane would mean nothing." + exit 1 +fi +echo "PASS: every control behaved as required — the instrument passes what should pass" +echo " and fails what must fail." +exit 0 diff --git a/verification/proofs/LEDGER.json b/verification/proofs/LEDGER.json new file mode 100644 index 0000000..f8ea444 --- /dev/null +++ b/verification/proofs/LEDGER.json @@ -0,0 +1,97 @@ +{ + "schema": "hyperpolymath/proof-ledger/1", + "policy": { + "proof_policy": "standards/3-practice/PROOF-POLICY.adoc", + "grade_model": "mathesis/estate-mathematical-architecture §5 (Verification Pipeline) and §6 (Epistemic Precision)", + "escape_hatches": "standards/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc", + "note": "Theory proofs are Agda (source of truth) rechecked in Rocq and Lean. This ledger records, per theorem, the source leg and each recheck leg, with the route, the axioms and the exact commit of the verification receipt." + }, + "status_vocabulary": [ + "open", + "argued", + "tested-only", + "proven-with-postulates", + "proven" + ], + "theorems": [ + { + "id": "XP-1", + "kind": "theory", + "spans": [ + "affinescript", + "echo-types", + "typed-wasm" + ], + "statement": "The pipeline's information-losing typing operations are instances of the echo-types fiber Echo f y := Sigma A (lambda x -> f x === y): affine weakening (AffineScript linear is below affine) collapses a distinction, has no section, and refinement erasure is non-injective.", + "grade": "3", + "grade_basis": "mathesis §5 Grade 3: type-checks in Agda, has not been translated to an independent foundational system. The Rocq and Lean recheck legs required by PROOF-POLICY §2 are recorded here as open.", + "source": { + "prover": "agda", + "family": "dtt", + "status": "proven", + "files": [ + "verification/proofs/agda/EchoTyping.agda", + "verification/proofs/agda/Verification.agda" + ], + "safety_flags": [ + "--safe", + "--without-K" + ], + "evidence": { + "kind": "ci-receipt", + "commit": "4c6b918998b9756fdeb1e64c74de27a968677ac1", + "date": "2026-11-01", + "run": "https://github.com/hyperpolymath/nextgen-typing/actions/runs/41299544043", + "checked_by": "proof-ci.yml (then the Agda typecheck lane): Agda 2.8.0, --safe --library=nextgen-typing, agda-stdlib v2.3, echo-types b0982c4, absolute-zero f486c29", + "note": "Recorded, not re-run. This lane examines the §2 recheck legs; the Agda source leg is audited for form and evidence only. Use `just proof-check-agda` to re-typecheck it locally." + }, + "assumptions": [ + { + "kind": "dependency-pin", + "name": "agda", + "version": "2.8.0" + }, + { + "kind": "dependency-pin", + "name": "agda-stdlib", + "version": "v2.3" + }, + { + "kind": "dependency-pin", + "name": "echo-types", + "version": "b0982c44f36133acd2d0e1d4e03cf031fff7a470" + }, + { + "kind": "dependency-pin", + "name": "absolute-zero", + "version": "f486c29903434589117fa0662c6f29b0f17d1d5f" + } + ] + }, + "legs": [ + { + "prover": "rocq", + "family": "dtt", + "status": "open", + "route": null, + "artifact": null, + "axioms": null, + "statement_compared": null, + "api_receipt": null, + "blocker": "no Rocq witness exists. PROOF-POLICY §2 requires one: transport the Agda term through Dedukti/Lambdapi (record the statement comparison) or re-prove the statement in Rocq by hand." + }, + { + "prover": "lean4", + "family": "dtt", + "status": "open", + "route": null, + "artifact": null, + "axioms": null, + "statement_compared": null, + "api_receipt": null, + "blocker": "no Lean 4 witness exists. PROOF-POLICY §2 requires one and forbids Mathlib; until a released Lambdapi Lean exporter exists the lean leg is re-proved by hand in core Lean." + } + ] + } + ] +} diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index 021de5a..5f8be50 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -21,15 +21,21 @@ boundary via `.github/workflows/coordination-boundary.yml` (`scripts/check-coordination-boundary.sh`). ==== -== Current contents +== Layout [source] ---- proofs/ -└── agda/ - ├── EchoTyping.agda # echo-types <-> AffineScript/typed-wasm pipeline - ├── Verification.agda # aggregator: `agda Verification.agda` checks the set - └── nextgen-typing.agda-lib # depends on: standard-library, echo-types +├── LEDGER.json # the machine-readable record of every theorem +├── agda/ # SOURCE leg (PROOF-POLICY §1: theory is Agda) +│ ├── EchoTyping.agda # echo-types <-> AffineScript/typed-wasm pipeline +│ ├── Verification.agda # aggregator: checks the set +│ ├── nextgen-typing.agda-lib # depends on: standard-library, echo-types +│ └── MANIFEST +├── coq/ # recheck leg (§2) — currently OPEN, no witness +│ └── MANIFEST +└── lean4/ # recheck leg (§2) — currently OPEN, no witness + └── MANIFEST ---- `EchoTyping.agda` is the worked example of a qualifying proof: it depends on the @@ -39,40 +45,53 @@ erasure into the typed-wasm/kernel layer) are instances of echo-types' fiber construction. It genuinely spans `echo-types`, `affinescript`, and `typed-wasm`, so it is coordination material rather than any one project's. -== Adding a proof here +== Two records, one truth -Before adding anything, check the gate: +*`LEDGER.json`* is the record of what has actually been proven and how far it +has travelled. Under `standards/3-practice/PROOF-POLICY.adoc` §1 a theory proof +has an Agda source leg, and §2 requires that statement to be *rechecked* in Rocq +and Lean — `transported` (Dedukti/Lambdapi) or `re-proved` by hand, with the +statement comparison recorded and no Mathlib. Each theorem in the ledger carries +its grade (mathesis `estate-mathematical-architecture` §5), the status of every +leg from the §5 vocabulary (`open`, `argued`, `tested-only`, +`proven-with-postulates`, `proven`), the route taken, the axioms and the exact +commit of the receipt. -. *Does it import or relate two or more constituent repos?* If not, it is a - single-project proof — put it in the owning repo (see `placement.a2ml`). -. If it qualifies, add the file under the appropriate prover subdirectory, then - register it in **both**: - * `[verification].allowed-proofs` in `.machine_readable/bot_directives/placement.a2ml`, and - * `ALLOWED_PROOFS` in `scripts/check-coordination-boundary.sh`. -. Ensure `--safe` / `%default total` / no escape hatches (see Banned Patterns). -. Run the gate. `just proof-enrolment` fails when a proof source under - `verification/proofs/` is not registered in *both* places above, when a - registered entry has no file behind it, when the two registries disagree, - and when zero proofs are enrolled. It is the first dependency of - `just proof-check-all`, so an unlisted proof cannot reach `main` green. +*A `MANIFEST` per prover* is the compile list. One entry per line: -== How a proof is checked +[source] +---- +||gated|quarantine| +---- + +`gated` must compile. `quarantine` must *continue* to fail — if a quarantined +module starts compiling, the gate fails and tells you to promote it, so the list +cannot rot into a permanent excuse. Blank lines and `#` comments are ignored, +which is why `coq/MANIFEST` and `lean4/MANIFEST` can explain their empty state. + +A witness on disk that neither the ledger nor a MANIFEST claims is an error, in +both directions: no ledger row without a file, no file without a ledger row. + +== Current state -Every proof source here is typechecked by the real all-proofs target, which CI -runs on any change to proofs, registries, `Justfile` or the lane: +`XP-1` is *Grade 3*: Agda only, not translated. The Rocq and Lean 4 recheck legs +are `open` — the estate policy's §2 obligation is *unmet*, and the ledger says so +with the blocker that stops each leg rather than leaving a blank. Both legs are +reported as `POLICY GAP` on every run; neither is counted as verification. + +== How a proof here is checked [source,bash] ---- -just proof-check-all # .github/workflows/proof-ci.yml +just proof-witness-check # what CI runs: ledger audit + declared recheck legs +just proof-status # grade, and each leg's status and blocker +just proof-check-all # local only: ledger + all four provers ---- -A prover that is required (because proofs for it are enrolled) but absent from -`PATH` makes the run **BLOCKED** (exit 2) — the lane never skips it and never -turns that into a pass. A prover with no enrolled sources prints `NONE`, not -`PASS`. - -The Agda layer needs its library manifest activated, otherwise Agda reports -`[ModuleNameDoesntMatchFileName]` for every module (observed on 2026-11-01): +The Agda source leg is *recorded and audited for form*; the lane does not +re-derive it. It can still be typechecked locally, which needs its library +manifest activated — otherwise Agda reports `[ModuleNameDoesntMatchFileName]` for +every module (observed on 2026-11-01): [source,bash] ---- @@ -83,9 +102,27 @@ agda --safe --library=nextgen-typing verification/proofs/agda/Verification.agda dependency `absolute-zero` must be registered in `/libraries` (`agda --print-agda-app-dir`). `.github/workflows/proof-ci.yml` pins all four. +A prover that is required but absent from `PATH` makes the run **BLOCKED** — the +lane never skips it and never turns that into a pass. + +== Adding or promoting a witness + +. Write the witness under `verification/proofs//` (no Mathlib). +. Register it in that prover's `MANIFEST` as `gated` (or `quarantine` if it is + known broken and tracked). +. Add it to `LEDGER.json`: the leg's status, the route (`transported` / + `re-proved`), how the statement was compared with the Agda one, the axioms + from `Print Assumptions` (Rocq) or `#print axioms` (Lean), and the receipt + commit. A grade above 3 is refused unless the legs behind it are `proven`. +. Register the proof in **both** registries: + `[verification].allowed-proofs` in `.machine_readable/bot_directives/placement.a2ml` + and `ALLOWED_PROOFS` in `scripts/check-coordination-boundary.sh`. +. Run `just proof-witness-check`. An unlisted proof, a stale manifest entry, a + registry disagreement, a grade without evidence, or a zero-work run each fail. + == Banned patterns -The following MUST NOT appear in any proof file: +The following MUST NOT appear in any proof file outside a comment: * `believe_me`, `assert_total` (Idris2) * `postulate` (Idris2/Agda) @@ -94,8 +131,13 @@ The following MUST NOT appear in any proof file: * `unsafeCoerce` (Haskell) * `Obj.magic` (OCaml/ReScript) -CI enforces this with `just proof-scan-dangerous` -(`scripts/proof-scan-dangerous.sh`), which runs inside `just proof-check-all`. -It is comment-aware — a prose mention such as "zero postulates" is not flagged, -while a real escape hatch is, including inside `{- ... -}` blocks. A scan that -finds no proof files to scan fails rather than reporting clean. +`just proof-scan-dangerous` (`scripts/proof-scan-dangerous.sh`) and the ledger +gate's escape-hatch scan are both comment-aware — a prose mention such as "zero +postulates" is not flagged, while a real escape hatch is, including inside +`{- ... -}` blocks. A scan that finds no proof files to scan fails rather than +reporting clean. + +This matters because a compiler exit code is not evidence: Rocq accepts +`Admitted` and Lean accepts `sorry` with status 0. The controls in +`tests/proofs/` prove the instrument catches both — a gate must be shown to +fail, not only to pass (PROOF-POLICY §7). diff --git a/verification/proofs/agda/MANIFEST b/verification/proofs/agda/MANIFEST new file mode 100644 index 0000000..6d7e02f --- /dev/null +++ b/verification/proofs/agda/MANIFEST @@ -0,0 +1,12 @@ +# Agda proof manifest — read by scripts/check-proofs.sh agda +# (estate instrument, copied from hyperpolymath/mathesis@50a012d). +# Format: ||gated|quarantine| +# +# This is the SOURCE leg of XP-1 (PROOF-POLICY §1: theory is Agda, source of +# truth). CI does not re-run it: .github/workflows/proof-ci.yml examines the §2 +# recheck legs (Rocq and Lean). Status, evidence commit and assumptions for this +# leg live in ../LEDGER.json. `just proof-check-agda` re-typechecks it locally, +# which needs nextgen-typing, standard-library, echo-types and absolute-zero +# registered in /libraries and defaults. +verification/proofs/agda|EchoTyping.agda|gated|XP-1 source leg; receipt and assumptions in ../LEDGER.json +verification/proofs/agda|Verification.agda|gated|XP-1 aggregator: imports EchoTyping, so a green here covers the set diff --git a/verification/proofs/coq/MANIFEST b/verification/proofs/coq/MANIFEST new file mode 100644 index 0000000..d67d4e9 --- /dev/null +++ b/verification/proofs/coq/MANIFEST @@ -0,0 +1,15 @@ +# Rocq (Coq) recheck-leg manifest — read by scripts/check-proofs.sh coq +# Format: ||gated|quarantine| +# +# PROOF-POLICY §2 requires every Agda theory proof to be rechecked in Rocq (and +# Lean). No Rocq witness exists yet: XP-1's rocq leg is recorded `open` in +# ../LEDGER.json, so no artifact is listed here for the compile gate to run. +# +# Adding the witness means all four steps, in one change: +# 1. write verification/proofs/coq/.v +# 2. list it below as `gated` +# 3. fill in the rocq leg row in ../LEDGER.json: status, route +# (transported|re-proved), statement_compared, axioms, evidence +# 4. re-derive the grade in ../LEDGER.json +# The ledger gate fails if the artifact exists but is unlisted (here or in the +# ledger), or if the ledger claims a leg with no artifact behind it. diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST new file mode 100644 index 0000000..a2978f2 --- /dev/null +++ b/verification/proofs/lean4/MANIFEST @@ -0,0 +1,10 @@ +# Lean 4 recheck-leg manifest — read by scripts/check-proofs.sh lean4 +# Format: ||gated|quarantine| +# +# PROOF-POLICY §2 requires every Agda theory proof to be rechecked in Lean 4 as +# well as Rocq, and forbids Mathlib. No Lean witness exists yet: XP-1's lean4 +# leg is recorded `open` in ../LEDGER.json, so no artifact is listed here. +# +# A Lean leg must be re-proved in core Lean until a released Lambdapi Lean +# exporter exists. Record the leg's route, statement comparison, axiom list +# (`#print axioms`) and evidence commit in ../LEDGER.json in the same change. From c4baf549247c080d3a529236c6894afe14026dd6 Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 13:55:54 +0000 Subject: [PATCH 13/51] proof: make the controls' and ledger's counts visible as annotations The runner log and the receipts artifact are not retrievable from every client (both redirect to blob storage), so the evidence that the instrument actually ran was only inferable from a green step. Emit the census and the control count as ::notice:: annotations, which the check-run API serves. Local: ledger gate PASS, notice reads '1 theorem(s), 2 proof source(s), 0 proven recheck leg(s), 2 policy gap(s)'. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- scripts/check-proof-ledger.sh | 7 +++++++ tests/proofs/run-controls.sh | 11 +++++++++-- 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/scripts/check-proof-ledger.sh b/scripts/check-proof-ledger.sh index 5d63dc5..3e9115d 100755 --- a/scripts/check-proof-ledger.sh +++ b/scripts/check-proof-ledger.sh @@ -529,6 +529,13 @@ echo " proof sources: $scanned scanned" echo " proven legs: $proven_legs" echo "" +# Annotation-visible census: the step summary is not retrievable through the +# check-run API, so the counts also go out as a notice. A reader can then see +# "1 theorem, 2 sources, 0 proven legs, 2 gaps" without the runner log. +if [ -n "${GITHUB_ACTIONS:-}" ]; then + echo "::notice::proof ledger: ${theorem_count} theorem(s), ${scanned} proof source(s), ${proven_legs} proven recheck leg(s), ${#GAPS[@]} policy gap(s)" +fi + if [ "${#GAPS[@]}" -gt 0 ]; then echo "--- POLICY GAPS (legal to record; NOT counted as verification) ---" printf ' ! %s\n' "${GAPS[@]}" diff --git a/tests/proofs/run-controls.sh b/tests/proofs/run-controls.sh index 3a3d7ee..5fedbc7 100755 --- a/tests/proofs/run-controls.sh +++ b/tests/proofs/run-controls.sh @@ -40,7 +40,8 @@ WORK="$(mktemp -d)" trap 'rm -rf "$WORK"' EXIT VIOLATIONS=0 -ok() { echo " ✅ $*"; } +CHECKS=0 +ok() { CHECKS=$((CHECKS + 1)); echo " ✅ $*"; } viol() { echo " ❌ $*"; VIOLATIONS=$((VIOLATIONS + 1)); } echo "=== Proof-witness instrument controls (PROOF-POLICY §7, both ways) ===" @@ -167,5 +168,11 @@ if [ "$VIOLATIONS" -gt 0 ]; then exit 1 fi echo "PASS: every control behaved as required — the instrument passes what should pass" -echo " and fails what must fail." +echo " and fails what must fail ($CHECKS expectation(s))." +# Machine-readable evidence: annotations are retrievable through the check-run +# API, so "how many expectations actually ran?" is answerable without the raw +# runner log (which GitHub does not serve to every client). +if [ -n "${GITHUB_ACTIONS:-}" ]; then + echo "::notice::proof-witness instrument verified both ways (§7): $CHECKS expectation(s), 0 violations, coqc $(coqc --version | head -1), lean $(lean --version | head -1)" +fi exit 0 From 112a7bf7209e676e8ad7efd6f88862b24f4f6acf Mon Sep 17 00:00:00 2001 From: Arena Agent Date: Sun, 1 Nov 2026 14:02:47 +0000 Subject: [PATCH 14/51] proof: substantiate the grade-3 rung and check the ladder's edges MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The previous commit recorded XP-1 as Grade 3 with both recheck legs open. This one makes the rung *below* the gap as explicit as the gap itself, and puts the rungs either side of it under the gate. What the grade now rests on (each item checked against the tree, not asserted): * named declarations — statement_anchor/statement_formal pin TP-ECHO-1..3 in EchoTyping.agda and record their types; the gate re-reads the file whitespace-normalised and fails if a recorded type is no longer there, so a moved statement cannot leave a stale record behind; * flags in force — the gate reads the {-# OPTIONS #-} pragmas out of the proof files AND the CLI flags out of scripts/check-proofs.sh, and requires the ledger's safety_flags to equal their union. Drop or add a flag and the run goes red; * the §5 deviation — mathesis §5 names '--safe --erasure' or 'Full --cubical' for grade 3; this proof runs '--safe --without-K --cubical-compatible', which is neither. The grade stays 3 (Agda alone, safe, untranslated) but the difference is recorded in grade_deviation, and the gate requires that field whenever the flags are not a named configuration; * 'no postulates' — now evidenced by a mechanism (--safe + the comment-aware scans) in escape_hatch_evidence, not asserted. The rungs either side: * 2i needs exactly one proven recheck leg. `just proof-grade` prints the delta straight from the ledger; PROOF-STATUS carries the runbook, including what will NOT be accepted (Mathlib, exit-code-only evidence, a grade raised while the legs stay open); * 2ii still needs a non-DTT leg, which Rocq + Lean cannot supply; * 1 still needs an AXLE/coq-lsp/isabelle-server receipt. Regressions and supersession (mathesis §6) are now checked: every history entry needs date/target/from/to/evidence, the LAST entry for a target must equal that target's current value (so a downgrade cannot be quietly applied and a record cannot be quietly dropped), and a transition to a weaker state needs a reason. An honest, evidenced regression passes — control 7 pins that. Controls split into two halves: run-ledger-controls.sh (15 expectations, no prover needed, runs everywhere) and the kernel half in run-controls.sh (5). Planted: grade with no leg, contradictory history, unjustified regression, flag drift, statement drift, missing escape-hatch mechanism, unrecorded deviation, non-existent anchor, ghost source file, unclaimed witness — each refused for the stated reason. Local: enrolment --static-only PASS, ledger gate PASS (1 theorem, 2 sources, 0 proven legs, 2 policy gaps), boundary PASS, banned-pattern PASS, 15/15 ledger-form controls PASS, `just proof-grade` renders the ladder. The kernel half needs coqc/lean, which are absent here: BLOCKED, proven in CI. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- .github/workflows/proof-ci.yml | 22 ++- Justfile | 45 ++++++ PROOF-STATUS.adoc | 156 ++++++++++++++++++- scripts/check-proof-ledger.sh | 233 ++++++++++++++++++++++++++++ tests/proofs/run-controls.sh | 137 ++++++---------- tests/proofs/run-ledger-controls.sh | 155 ++++++++++++++++++ verification/proofs/LEDGER.json | 51 +++++- verification/proofs/README.adoc | 21 +++ 8 files changed, 713 insertions(+), 107 deletions(-) create mode 100755 tests/proofs/run-ledger-controls.sh diff --git a/.github/workflows/proof-ci.yml b/.github/workflows/proof-ci.yml index 37e8b66..42f3256 100644 --- a/.github/workflows/proof-ci.yml +++ b/.github/workflows/proof-ci.yml @@ -21,11 +21,23 @@ # proven-with-postulates | proven); a grade must be supported by the legs # behind it; axioms are tracked (`Print Assumptions`, `#print axioms`), not # assumed; receipts are pinned to a commit. -# * §7: a gate must be verified BOTH WAYS. tests/proofs/run-controls.sh feeds -# the instrument a closed Rocq proof and a closed Lean proof (must pass), a -# proof closed with `Admitted` and one closed with `sorry` (must fail), a -# ledger claiming a grade with no leg behind it (must fail), and a witness -# planted on disk that no ledger row claims (must fail). +# * §7: a gate must be verified BOTH WAYS. tests/proofs/run-controls.sh runs +# two halves: run-ledger-controls.sh (15 controls, no prover needed) plants +# a grade with no leg behind it, contradictory history, an unjustified +# regression, flag drift, statement drift, a missing escape-hatch mechanism, +# an unrecorded flag deviation, a non-existent anchor, a ghost source file +# and an unclaimed witness on disk — each must be refused for the stated +# reason, while an honest evidenced regression must still pass; and the +# kernel half requires a closed Rocq/Lean proof to be accepted with +# `Print Assumptions` / `#print axioms` reporting it closed, and the +# `Admitted` / `sorry` controls NOT to be reported closed. +# +# The Grade 3 claim itself is substantiated rather than labelled: the ledger +# names the Agda declarations that carry the statement (and the gate re-reads +# their types out of the file), records the flags in force (read out of the +# proof files and out of the instrument, not copied by hand), records the +# escape-hatch mechanism, and records the deviation from the configurations +# mathesis §5 names parenthetically. Any drift in those fails the run. # # What this lane refuses, and why it exists: before it, `just proof-check-all` # was never invoked by CI and each recipe ended in diff --git a/Justfile b/Justfile index cd60d77..7127df8 100644 --- a/Justfile +++ b/Justfile @@ -1431,6 +1431,51 @@ proof-status: echo "Policy gaps are printed by: just proof-ledger-check" +# Show the grade ladder: what the current grade rests on, and the exact delta +# up to the next rung (mathesis §5), computed from the ledger +proof-grade: + #!/usr/bin/env bash + set -euo pipefail + LEDGER="verification/proofs/LEDGER.json" + [ -f "$LEDGER" ] || { echo "FAIL: no ledger at $LEDGER" >&2; exit 1; } + jq -r ' + def proven: [ .legs[]? | select(.status == "proven" or .status == "proven-with-postulates") ] | length; + def non_dtt: [ .legs[]? | select(.status == "proven" or .status == "proven-with-postulates") | select(.prover == "isabelle" or .prover == "tla+" or .prover == "smt") ] | length; + "=== Grade ladder (mathesis §5) — recorded, not estimated ===", + "", + (.theorems[] | + "\(.id) kind=\(.kind) recorded grade: \(.grade)", + " source leg: \(.source.prover) \(.source.status) flags: \(.source.safety_flags | join(" "))", + (if (.grade_deviation // "") != "" then + " grade note: deviation from the §5 parenthetical is recorded in the ledger" + else empty end), + " recheck legs:", + (.legs[] | " \(.prover) [\(.family)]: \(.status)" + + (if .status == "open" then " blocker: " + (.blocker // "not recorded") + else " route: " + (.route // "not recorded") end)), + "", + " next rung:", + (if proven == 0 then + " grade 2i needs EXACTLY ONE proven recheck leg (Rocq or Lean), with its route\n" + + " (transported through Dedukti/Lambdapi, or re-proved by hand), the statement\n" + + " comparison against the Agda declarations, and the axiom query recorded.\n" + + " Proven today: 0. That is the whole of the work between here and 2i." + elif .grade == "3" then + " INCONSISTENT: a leg is proven while the grade still says 3 — the gate should\n" + + " have refused this ledger. Re-record the grade." + elif .grade == "2i" then + " grade 2ii needs TWO proven legs and one of them outside the DTT/CIC family.\n" + + " Agda, Rocq and Lean are all DTT, so a Rocq+Lean pair cannot reach 2ii: it needs\n" + + " a non-DTT leg such as Isabelle/HOL (proven non-DTT legs today: \(non_dtt))." + elif .grade == "2ii" then + " grade 1 needs the statement checked through a verified checker API — AXLE for\n" + + " Lean, coq-lsp for Rocq, isabelle-server for Isabelle — with the receipt recorded." + else + " grade 1 recorded: nothing higher is defined by the model." + end)), + "", + "Nothing here is a percentage: grades are recorded, never averaged (mathesis §6)."' "$LEDGER" + # ═══════════════════════════════════════════════════════════════════════════════ # SESSION MANAGEMENT (THIN BINDINGS TO CENTRAL STANDARDS) # ═══════════════════════════════════════════════════════════════════════════════ diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 868a305..d4fc181 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -50,6 +50,110 @@ gap is unmistakable: *no leg other than Agda has been proven for XP-1.* Lean, coq-lsp's REST surface for Rocq, isabelle-server). No such surface is wired up. +=== What the Grade 3 claim rests on + +Grade 3 is the lowest rung, so it is the one that most needs its evidence named +rather than implied. Four things carry the claim, and the gate checks each of +them against the tree on every run — if any of them drifts, the run goes red: + +[cols="22%,78%",options="header",] +|=== +|What |The evidence, and how it is checked +|Named declarations |`+TP-ECHO-1+`, `+TP-ECHO-2+`, `+TP-ECHO-3+` in +`+verification/proofs/agda/EchoTyping.agda+`. The ledger records each one's +*type*, and the gate re-reads the file (whitespace-normalised) to confirm the +recorded statement is still there. A grade anchored to a file rather than to a +named theorem is the proof inflation mathesis §11 rejects, so an anchor that is +not declared in the file is a failure. + +|Flags in force |`+--safe --without-K --cubical-compatible+`. The gate does not +take this on trust: it reads the `+{-# OPTIONS #-}+` pragmas out of the proof +files, reads the CLI flags out of `+scripts/check-proofs.sh+` (the instrument +`+just proof-check-agda+` calls), and requires the ledger's record to equal the +union. Drift in either direction fails. + +|The §5 parenthetical |mathesis §5 names the grade 3 configurations as +`+--safe --erasure+`, or Full `+--cubical+`. What runs here is neither: there is +no `+--erasure+` and no full `+--cubical+`. The grade is still recorded as 3 — +the result is carried by Agda alone under `+--safe+`, with no postulates and no +translation to an independent system — but the difference is recorded in the +ledger's `+grade_deviation+` field instead of being paraphrased away, and the +gate *requires* that field whenever the flags are not one of the named +configurations. + +|"No postulates" |`+--safe+` makes the compiler refuse postulates and the other +unsafe pragmas; `+scripts/proof-scan-dangerous.sh+` and the ledger gate's +comment-aware escape-hatch scan run over the same files in the same lane. The +mechanism is recorded in `+escape_hatch_evidence+`; asserting the absence of +escape hatches without naming a mechanism is a failure. +|=== + +The receipt behind all four is CI run 41299544043 at +`+4c6b918998b9756fdeb1e64c74de27a968677ac1+`. + +=== The ladder, and what each rung costs + +[cols="8%,47%,45%",options="header",] +|=== +|Rung |What it requires |State today +|`+3+` |Agda alone, `+--safe+`, not translated |*This is where XP-1 is.* The +Agda leg is proven and recorded; the flags, statements and escape-hatch +mechanism above are gated. + +|`+2i+` |Exactly *one* independent system (Rocq or Lean) carrying the same +statement: `+transported+` through Dedukti/Lambdapi, or `+re-proved+` by hand, +with the statement comparison and the axiom query recorded; no Mathlib +|*0 of 2 legs.* This is the whole of the remaining work, and it is a proving +job — not a bookkeeping one. `+just proof-grade+` prints the same delta. + +|`+2ii+` |Two proven legs *and* one outside the DTT/CIC family (e.g. +Isabelle/HOL). Rocq + Lean cannot reach this rung: they are the same family as +Agda, so a translation between them proves interoperability, not independence +|Unreachable with the current legs, by construction + +|`+1+` |The statement machine-checked through a verified checker API — AXLE for +Lean, coq-lsp for Rocq, isabelle-server for Isabelle — with its receipt recorded +|Not wired up; nothing here claims it +|=== + +=== Moving XP-1 up one rung (to `+2i+`): the runbook + +. Pick *one* leg. Two half-done legs are worth less than one done leg: `+2i+` + needs exactly one. +. Write the witness under `+verification/proofs/coq/+` or + `+verification/proofs/lean4/+`, with *no Mathlib* and no axiom of convenience. +. Register it in that prover's `+MANIFEST+` as `+gated+`. +. Record the leg in `+LEDGER.json+`: `+status+`, `+route+` (`+transported+` or + `+re-proved+`), `+artifact+`, `+axioms+` from `+Print Assumptions+` (Rocq) or + `+#print axioms+` (Lean), `+statement_compared+` against the declarations in + `+statement_formal+`, and the receipt commit. +. Record the promotion in `+history+`: `+{target: "grade", from: "3", to: "2i", + evidence: , ...}+`. The gate requires the last history entry for a target + to equal that target's current value, so history cannot be rewritten. +. Register the file in both registries (`+[verification].allowed-proofs+` and + `+ALLOWED_PROOFS+`) and run `+just proof-witness-check+`. + +What will *not* be accepted as reaching `+2i+`: a compiler exit code with no +axiom query (Rocq accepts `+Admitted+`, Lean accepts `+sorry+`); a leg marked +`+proven+` with no artifact, no MANIFEST entry, no route, no statement +comparison or no axiom list; a Mathlib import; or a grade raised while the legs +stay `+open+`. Each of those is a control in `+tests/proofs/+`. + +=== Regressions and supersession + +mathesis §6 requires a proof's history to say when it is superseded or +regresses. The ledger's `+history+` array is checked rather than decorative: + +* every entry needs a date, a target (`+grade+` or a prover), a `+from+`, a + `+to+` and the evidence that showed the transition; +* the *last* entry for a target must equal that target's current value — a + downgrade cannot be quietly applied, and a record cannot be quietly dropped; +* a transition to a weaker state (a grade moving down the ladder, or a leg + returning to `+open+`) must carry a `+reason+`. + +An honest, evidenced regression passes: the rule cuts both ways, and +`+tests/proofs/run-ledger-controls.sh+` control 7 pins that. + === The recheck obligation, stated plainly `+standards/3-practice/PROOF-POLICY.adoc+` §1 makes Agda the source of truth @@ -126,14 +230,25 @@ so the manifests compile nothing and the gate says so — the lane is green on "the ledger is honest", never on "the theorem is verified". |`+tests/proofs/run-controls.sh+` -|PROOF-POLICY §7 requires a gate to be verified *both ways*. These controls -feed the instrument a closed Rocq proof and a closed Lean proof (must be -accepted, `+Print Assumptions+` / `+#print axioms+` must report them closed and -axiom-free), a proof closed with `+Admitted+` and one closed with `+sorry+` -(must be rejected), a ledger claiming a grade with no leg behind it, and a -witness planted on disk that no ledger row claims. A control that stops -failing is a broken instrument, and the run goes red. Where `+coqc+` or -`+lean+` is absent the controls report **BLOCKED**, never a pass. +|PROOF-POLICY §7 requires a gate to be verified *both ways*, and this is where +that is done — in two halves. `+run-ledger-controls.sh+` (15 controls, no prover +needed) plants a grade with no leg behind it, a history whose last entry +contradicts the ledger, a regression with no reason, flag drift, statement +drift, a missing escape-hatch mechanism, an unrecorded deviation, an anchor that +does not exist, a source file that is not on disk, and a witness on disk that no +ledger row claims — each must be refused *for the stated reason* — and confirms +that an honest, evidenced regression is still accepted. The kernel half feeds +the compilers a closed Rocq proof and a closed Lean proof (must be accepted, +`+Print Assumptions+` / `+#print axioms+` must report them closed and +axiom-free), plus `+Admitted+` and `+sorry+` controls the kernels must *not* +report as closed. A control that stops failing is a broken instrument, and the +run goes red. Where `+coqc+` or `+lean+` is absent the kernel half reports +**BLOCKED**, never a pass. + +|`+just proof-grade+` +|Prints, per theorem, what the recorded grade rests on and the exact delta to +the next rung, computed from the ledger — so "how far off `+2i+` are we?" is +answered by the record rather than by prose. |`+just proof-enrolment+` (`+scripts/check-proof-enrolment.sh+`) @@ -176,6 +291,13 @@ bash tests/proofs/run-controls.sh # The ledger at a glance (grade, and each leg's status and blocker): just proof-status +# The same record as a ladder: what backs the grade, and the delta to the next +# rung (what "one proven recheck leg" would have to be): +just proof-grade + +# The ledger-form controls on their own (no prover needed): +bash tests/proofs/run-ledger-controls.sh + # Everything, local only — the ledger plus all four provers: just proof-check-all @@ -188,6 +310,14 @@ bash scripts/check-proof-enrolment.sh --static-only [cols="16%,20%,64%",options="header",] |=== |Date |Receipt |Result +|2026-11-01 |proof-ci run 41313633579 (sha `+c4baf54+`) |**PASS**, and the +run's annotations are the receipt: `+proof ledger: 1 theorem(s), 2 proof +source(s), 0 proven recheck leg(s), 2 policy gap(s)+`; +`+proof-witness instrument verified both ways (§7): 14 expectation(s), 0 +violations+` under coqc 8.18.0 and lean 4.15.0; plus one `+::warning::+` per +open leg, naming the §2 obligation it leaves unmet. A green run here means the +ledger is honest — not that XP-1 is verified in an independent kernel. + |2026-11-01 |proof-ci run 41299544043 (sha `+4c6b918+`) |**PASS** for the Agda source leg: enrolment gate PASS (2 proof sources, registered entries agree), Agda 2.8.0 typecheck of `+EchoTyping.agda+` and `+Verification.agda+` under @@ -214,6 +344,16 @@ so instead of reporting the leg as passing), not as a pass. [width="100%",cols="32%,42%,26%",options="header",] |=== |Date |Change |By +|2026-11-01 |The rung *below* `+2i+` is now substantiated rather than labelled: +the grade-3 claim is tied to named Agda declarations (`+TP-ECHO-1..3+`, whose +types the gate re-reads), to the flags actually in force (read out of the files +and the instrument, not copied by hand), and to a named escape-hatch mechanism. +The deviation from mathesis §5's parenthetical flags is recorded, not glossed. +`+history+` is now checked too — a regression must be evidenced and explained, +and the last entry must equal the current state. Added `+just proof-grade+` +(the ladder and the delta to the next rung) and split the §7 controls into +ledger-form (15, no prover) and kernel halves |Arena agent + |2026-11-01 |Status re-anchored to `+verification/proofs/LEDGER.json+` in the policy's vocabulary. XP-1 recorded as *Grade 3* (Agda only); Rocq and Lean 4 recheck legs recorded `+open+` under PROOF-POLICY §2, with their blockers. The diff --git a/scripts/check-proof-ledger.sh b/scripts/check-proof-ledger.sh index 3e9115d..5c3a0f2 100755 --- a/scripts/check-proof-ledger.sh +++ b/scripts/check-proof-ledger.sh @@ -245,6 +245,239 @@ while IFS=$'\t' read -r tid kind grade provers claimed proven; do fi done < /tmp/proof-ledger-rows.$$.tsv +# --- 3b. the SOURCE leg must be substantiated, and its flags must be the ones +# actually in force ----------------------------------------------------------- +# A Grade 3 claim is "Agda alone, and safe". That is only meaningful if (a) the +# source leg really is proven, (b) the flags recorded are the flags the lane +# really passes, and (c) the named declarations the statement rests on exist. +# None of this is taken on trust: the CLI flags are read out of the instrument +# (scripts/check-proofs.sh), the {-# OPTIONS #-} out of the proof files, and the +# identifiers out of the file named as the anchor. +AGDA_CLI_FLAGS="$( + grep -oE 'agda --safe[^"]*' scripts/check-proofs.sh 2>/dev/null | head -1 \ + | grep -oE -- '--[a-zA-Z][a-zA-Z0-9-]*' | sort -u | tr '\n' ' ' | sed 's/ *$//' +)" +if [ -z "$AGDA_CLI_FLAGS" ]; then + fail "could not read the Agda CLI flags out of scripts/check-proofs.sh (instrument changed shape) — the recorded flags cannot be cross-checked" +fi + +file_agda_options() { # $1.. = agda files; prints the sorted union of OPTIONS flags + local f + for f in "$@"; do + [ -f "$f" ] || continue + awk '/OPTIONS/ { rest = $0 + while (match(rest, /--[a-zA-Z][a-zA-Z0-9-]*/)) { + print substr(rest, RSTART, RLENGTH) + rest = substr(rest, RSTART + RLENGTH) + } }' "$f" + done | sort -u | tr '\n' ' ' | sed 's/ *$//' +} + +while IFS=$'\t' read -r tid sprover sstatus rec_file_opts rec_cli rec_effective files_csv anchor_ids escape_evidence; do + [ -z "$tid" ] && continue + kind_of="$( + jq -r --arg id "$tid" '.theorems[] | select(.id == $id) | .kind' "$LEDGER" + )" + + # (a) PROOF-POLICY §1: a theory theorem's source of truth is Agda, and it + # must actually be proven — a grade resting on an open source leg is a guess. + if [ "$kind_of" = "theory" ] && [ "$sprover" != "agda" ]; then + fail "$tid: a theory theorem's source leg must be Agda (PROOF-POLICY §1); ledger records '${sprover:-}'" + fi + case "$sstatus" in + proven|proven-with-postulates) ;; + *) fail "$tid: source leg status is '${sstatus:-}' — a recorded grade rests on the source of truth being proven, not asserted (PROOF-POLICY §5)" ;; + esac + + # (b) every source file must exist + IFS=',' read -r -a src_files <<< "$files_csv" + for f in "${src_files[@]}"; do + [ -z "$f" ] && continue + [ -f "$f" ] || fail "$tid: source file recorded but missing on disk: $f" + done + + # (c) flags: what the instrument passes, what the files declare, and the + # union the ledger claims must agree. Drift here silently changes what a + # Grade 3 claim means. + actual_file_opts="$(file_agda_options "${src_files[@]}")" + if [ "$rec_cli" != "$AGDA_CLI_FLAGS" ]; then + fail "$tid: flags drift — scripts/check-proofs.sh invokes 'agda ${AGDA_CLI_FLAGS}' but the ledger records CLI '${rec_cli:-}'" + fi + if [ "$rec_file_opts" != "$actual_file_opts" ]; then + fail "$tid: flags drift — the proof files declare '${actual_file_opts:-}' in {-# OPTIONS #-} but the ledger records '${rec_file_opts:-}'" + fi + effective_expected="$(printf '%s %s\n' "$actual_file_opts" "$AGDA_CLI_FLAGS" | tr ' ' '\n' | grep -v '^$' | sort -u | tr '\n' ' ' | sed 's/ *$//')" + if [ "$rec_effective" != "$effective_expected" ]; then + fail "$tid: effective safety flags recorded as '${rec_effective:-}' but the files+instrument actually apply '${effective_expected:-}'" + fi + case " $rec_effective " in + *" --safe "*) ;; + *) fail "$tid: '--safe' is not in the effective flags — postulates and other escape hatches are not ruled out, so the grade is unsupported (mathesis §5)" ;; + esac + + # (d) mathesis §5 names the Grade 3 configurations parenthetically + # (--safe --erasure, or Full --cubical). If the flags in force are neither, + # the deviation must be recorded rather than glossed over. + grade3_named=0 + case " $rec_effective " in *" --erasure "*) grade3_named=1 ;; esac + case " $rec_effective " in + *" --cubical "*) + case " $rec_effective " in + *" --cubical-compatible "*) ;; + *) grade3_named=1 ;; + esac + ;; + esac + if [ "$grade3_named" -eq 0 ]; then + deviation="$( + jq -r --arg id "$tid" '.theorems[] | select(.id == $id) | .grade_deviation // ""' "$LEDGER" + )" + if [ -z "${deviation// }" ]; then + fail "$tid: the flags in force ('$rec_effective') are neither of the configurations mathesis §5 names for grade 3 (--safe --erasure, or Full --cubical) — record the deviation in .grade_deviation instead of paraphrasing the policy" + fi + fi + + # (e) the statement must rest on named declarations that exist. A grade + # anchored to a file rather than a theorem is the "proof inflation" mathesis + # §11 rejects. + if [ -z "${anchor_ids// }" ]; then + fail "$tid: no .statement_anchor — a grade must point at the named declarations that carry the statement, not at a file" + else + IFS=',' read -r -a anchors <<< "$anchor_ids" + for a in "${anchors[@]}"; do + [ -z "${a// }" ] && continue + hit=0 + for f in "${src_files[@]}"; do + [ -f "$f" ] || continue + grep -qE "^[[:space:]]*${a//./\\.}[[:space:]]*:" "$f" && hit=1 + done + [ "$hit" -eq 1 ] || fail "$tid: statement anchor '$a' is not declared in any recorded source file (looked in: $files_csv)" + done + fi + + # (e2) PROOF-POLICY §2 needs a statement comparison between the Agda source + # and any recheck leg. That is impossible if the Agda statement is only prose, + # so each recorded declaration's TYPE must still be in the file, whitespace- + # normalised. When the Agda statement moves, this record has to move with it. + while IFS=$'\t' read -r decl_name decl_type; do + [ -z "${decl_name// }" ] && continue + if [ -z "${decl_type// }" ]; then + fail "$tid: statement_formal.$decl_name records no type — a recheck leg cannot be compared against it" + continue + fi + norm_type="$(printf '%s' "$decl_type" | tr -s '[:space:]' ' ' | sed 's/^ *//; s/ *$//')" + found=0 + for f in "${src_files[@]}"; do + [ -f "$f" ] || continue + norm_file="$(tr -s '[:space:]' ' ' < "$f")" + case "$norm_file" in + *"$norm_type"*) found=1 ;; + esac + done + if [ "$found" -eq 0 ]; then + fail "$tid: statement drifted — statement_formal.$decl_name records the type + '$norm_type' + which no recorded source file contains any more. If the Agda statement + changed, re-record it here (and re-check any leg that was compared against + it) — PROOF-POLICY §2's statement comparison is void otherwise." + fi + done < <(jq -r --arg id "$tid" ' + .theorems[] | select(.id == $id) | .statement_formal.declarations[]? | + [ (.name // ""), (.type // "") ] | @tsv' "$LEDGER") + + # (f) "no escape hatches" has to be evidenced by a mechanism, not a claim. + if [ -z "${escape_evidence// }" ]; then + fail "$tid: no .escape_hatch_evidence — the absence of postulates has to be evidenced by a mechanism (--safe plus the comment-aware scan), not asserted" + fi +done < <(jq -r ' + .theorems[] | + [ .id, + (.source.prover // ""), + (.source.status // ""), + ((.source.flags_provenance.file_options // []) | sort | join(" ")), + ((.source.flags_provenance.cli // []) | sort | join(" ")), + ((.source.safety_flags // []) | sort | join(" ")), + ((.source.files // []) | join(",")), + ((.statement_anchor // []) | join(",")), + (.source.escape_hatch_evidence // "") + ] | @tsv' "$LEDGER") + +# --- 3c. Superseded / Regressed (mathesis §6) -------------------------------- +# §6 requires a proof's history to record when it is superseded or regresses. +# Two rules make that real rather than decorative: +# * every history entry is well formed (date, target, from, to, evidence); +# * the LAST entry for a target must equal that target's current value — so a +# downgrade cannot be quietly applied, and a record cannot be quietly +# dropped. A transition to a weaker state must also carry a reason. +GRADE_STRENGTH='{"1":4,"2ii":3,"2i":2,"3":1}' +while IFS=$'\t' read -r tid target from to date evidence reason; do + [ -z "$tid" ] && continue + if [ -z "${target// }" ]; then + fail "$tid: history entry has no target (expected 'grade' or a prover name)" + continue + fi + printf '%s' "$date" | grep -qE '^[0-9]{4}-[0-9]{2}-[0-9]{2}$' \ + || fail "$tid/$target: history date '${date:-}' is not YYYY-MM-DD" + [ -n "${evidence// }" ] \ + || fail "$tid/$target: history entry ${from:-?}->${to:-?} has no evidence — a recorded transition needs the receipt that showed it" + [ -n "${from// }" ] && [ -n "${to// }" ] \ + || fail "$tid/$target: history entry has an empty from/to" + + if [ "$target" = "grade" ]; then + for g in "$from" "$to"; do + case "$g" in 3|2i|2ii|1) ;; *) fail "$tid: history records grade '$g', which is not one of 3, 2i, 2ii, 1 (mathesis §5)" ;; esac + done + else + case ",$target," in + *,agda,*|*,rocq,*|*,lean4,*|*,idris2,*|*,isabelle,*|*,"tla+",*|*,smt,*) ;; + *) fail "$tid: history target '$target' is not a prover in this estate's vocabulary" ;; + esac + case "$to" in + open|argued|tested-only|proven-with-postulates|proven) ;; + *) fail "$tid/$target: history records status '$to', which is outside the PROOF-POLICY §5 vocabulary" ;; + esac + case "$from" in + open|argued|tested-only|proven-with-postulates|proven) ;; + *) fail "$tid/$target: history records status '$from', which is outside the PROOF-POLICY §5 vocabulary" ;; + esac + fi + + # a transition to a weaker state must say why (mathesis §6: Regressed) + if [ "$target" = "grade" ]; then + old_rank="$(printf '%s' "$GRADE_STRENGTH" | jq -r --arg g "$from" '.[$g] // 0')" + new_rank="$(printf '%s' "$GRADE_STRENGTH" | jq -r --arg g "$to" '.[$g] // 0')" + if [ "$new_rank" -lt "$old_rank" ] && [ -z "${reason// }" ]; then + fail "$tid: grade regressed from '$from' to '$to' with no .reason recorded (mathesis §6 requires Regressed to be explained)" + fi + else + if [ "$to" = "open" ] && [ "$from" != "open" ] && [ -z "${reason// }" ]; then + fail "$tid/$target: leg regressed from '$from' to open with no .reason recorded (mathesis §6)" + fi + fi +done < <(jq -r ' + .theorems[] | .id as $id | (.history // [])[] | + [ $id, (.target // ""), (.from // ""), (.to // ""), (.date // ""), (.evidence // ""), (.reason // "") ] | @tsv' "$LEDGER") + +# the last entry for each target must be the current value +while IFS=$'\t' read -r tid target last_to; do + [ -z "$tid" ] && continue + if [ "$target" = "grade" ]; then + current="$(jq -r --arg id "$tid" '.theorems[] | select(.id == $id) | .grade | tostring' "$LEDGER")" + [ "$last_to" = "$current" ] \ + || fail "$tid: history's last recorded grade is '$last_to' but the ledger now records '$current' — record the regression (or the promotion) instead of rewriting history (mathesis §6)" + else + current="$(jq -r --arg id "$tid" --arg p "$target" '.theorems[] | select(.id == $id) | .legs[]? | select(.prover == $p) | .status' "$LEDGER")" + if [ -z "$current" ]; then + fail "$tid: history records a transition for '$target', but the ledger has no such leg" + elif [ "$last_to" != "$current" ]; then + fail "$tid/$target: history's last recorded status is '$last_to' but the leg now records '$current' — record the change instead of rewriting history (mathesis §6)" + fi + fi +done < <(jq -r ' + .theorems[] | .id as $id + | (.history // []) | group_by(.target)[] | .[-1] + | [ $id, (.target // ""), (.to // "") ] | @tsv' "$LEDGER") + # --- 4. every non-open claim must be backed by artifact + MANIFEST + route --- while IFS=$'\t' read -r tid prover status artifact route compared axioms reproof; do [ -z "$tid" ] && continue diff --git a/tests/proofs/run-controls.sh b/tests/proofs/run-controls.sh index 5fedbc7..aa6468a 100755 --- a/tests/proofs/run-controls.sh +++ b/tests/proofs/run-controls.sh @@ -9,20 +9,20 @@ # planted violation. A gate that has only ever been seen to pass is # indistinguishable from one that cannot fail. # -# The controls are tiny fixtures under tests/proofs/control/. They are NOT -# estate proofs and they live outside verification/proofs/, so no census, no -# ledger and no catalogue ever counts them as mathematics. +# This script runs the whole verification in two halves: # -# Assertions: -# 1. Rocq closed control -> coqc accepts, Print Assumptions: closed -# 2. Rocq planted `Admitted` -> escape-hatch scan REJECTS it, and the -# kernel does not report it closed -# 3. Lean 4 closed control -> lean accepts, #print axioms: no axioms -# 4. Lean 4 planted `sorry` -> #print axioms shows sorryAx, scan REJECTS -# 5. Ledger gate -> rejects a planted "grade 2i, legs open" -# claim (no evidence behind the grade) -# 6. Ledger gate -> rejects a witness planted on disk but not -# claimed in the ledger or the MANIFEST +# 1. run-ledger-controls.sh — 15 controls over the RECORDED claims (grades, +# statements, flags, history, unclaimed witnesses, escape hatches). No +# prover needed: that half runs everywhere. +# 2. the kernel controls below — a closed Rocq proof and a closed Lean proof +# must be accepted by their kernels, and Print Assumptions / #print axioms +# must report them closed and axiom-free. This half exists because a +# compiler's exit code is not evidence of a closed proof: Rocq accepts +# `Admitted` and Lean accepts `sorry` with status 0. +# +# The fixtures live in tests/proofs/control/. They are NOT estate proofs and +# they sit outside verification/proofs/, so no census, ledger or catalogue ever +# counts them as mathematics. # # Exit: 0 every control behaved as required; 1 an expectation was violated; # 2 BLOCKED — a prover the controls need is not installed here. @@ -34,132 +34,86 @@ ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)" cd "$ROOT" || exit 2 CONTROLS="tests/proofs/control" -GATE="scripts/check-proof-ledger.sh" -LEDGER="verification/proofs/LEDGER.json" -WORK="$(mktemp -d)" -trap 'rm -rf "$WORK"' EXIT - VIOLATIONS=0 CHECKS=0 ok() { CHECKS=$((CHECKS + 1)); echo " ✅ $*"; } viol() { echo " ❌ $*"; VIOLATIONS=$((VIOLATIONS + 1)); } echo "=== Proof-witness instrument controls (PROOF-POLICY §7, both ways) ===" -echo "fixtures: $CONTROLS" echo "" -# --- toolchain: absent means BLOCKED, never a pass --------------------------- +# --- 1. the recorded-claim half --------------------------------------------- +if bash tests/proofs/run-ledger-controls.sh; then + : +else + echo " ✗ the ledger-form controls failed; the instrument does not behave as claimed." + VIOLATIONS=$((VIOLATIONS + 1)) +fi +echo "" + +# --- 2/3. the kernel half: absent means BLOCKED, never a pass --------------- +echo "=== Kernel controls (need coqc, coqtop and lean) ===" missing=() for tool in coqc coqtop lean; do command -v "$tool" >/dev/null 2>&1 || missing+=("$tool") done if [ "${#missing[@]}" -gt 0 ]; then - echo "BLOCKED: the controls need ${missing[*]} on PATH, and the instrument cannot" - echo " be shown to work without them. This is NOT a pass (PROOF-POLICY §6)." + echo "BLOCKED: the kernel controls need ${missing[*]} on PATH, and the instrument" + echo " cannot be shown to work without them. This is NOT a pass (PROOF-POLICY §6)." exit 2 fi echo "coqc: $(coqc --version 2>/dev/null | head -1)" echo "lean: $(lean --version 2>/dev/null | head -1)" echo "" -# --- 1/2. Rocq: closed proof accepted, planted Admitted rejected ------------ +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT + cp "$CONTROLS/Control.v" "$WORK/Control.v" if ( cd "$WORK" && coqc -q Control.v ) >"$WORK/coqc-control.log" 2>&1; then - ok "1. coqc accepts the closed control (Control.v)" + ok "K1. coqc accepts the closed control (Control.v)" else - viol "1. coqc rejected the closed control; the instrument is broken, not strict" + viol "K1. coqc rejected the closed control; the instrument is broken, not strict" sed 's/^/ /' "$WORK/coqc-control.log" | head -20 fi assumptions="$( cd "$WORK" && printf 'Require Import Control.\nPrint Assumptions control_true.\n' | coqtop -quiet 2>&1 )" if printf '%s' "$assumptions" | grep -q "Closed under the global context"; then - ok "1. Print Assumptions reports the closed control as closed" + ok "K2. Print Assumptions reports the closed control as closed" else - viol "1. Print Assumptions did not report 'Closed under the global context'" + viol "K2. Print Assumptions did not report 'Closed under the global context'" printf '%s\n' "$assumptions" | sed 's/^/ /' | head -20 fi cp "$CONTROLS/PlantedAdmitted.v" "$WORK/PlantedAdmitted.v" if ( cd "$WORK" && coqc -q PlantedAdmitted.v ) >"$WORK/coqc-planted.log" 2>&1; then # Coq accepts Admitted at compile time; that is exactly why an exit code is - # not evidence. The scan must catch it. - ok "2. coqc accepts the planted Admitted control (exit code alone is not evidence)" -else - ok "2. coqc rejected the planted Admitted control outright" -fi -if bash "$GATE" --scan-file "$CONTROLS/PlantedAdmitted.v" >/dev/null 2>&1; then - viol "2. the escape-hatch scan ACCEPTED a proof closed with Admitted" -else - ok "2. the escape-hatch scan rejects the planted Admitted control" -fi -if bash "$GATE" --scan-file "$CONTROLS/Control.v" >/dev/null 2>&1; then - ok "2. the escape-hatch scan accepts the closed control (no false positive)" + # not evidence. The scan must catch it (control L2), and the kernel must not + # report it closed (K3). + ok "K3. coqc accepts the planted Admitted control — exit code alone is not evidence" else - viol "2. the escape-hatch scan rejected the closed control (false positive)" + ok "K3. coqc rejected the planted Admitted control outright" fi planted_assumptions="$( cd "$WORK" && printf 'Require Import PlantedAdmitted.\nPrint Assumptions planted_true.\n' | coqtop -quiet 2>&1 )" if printf '%s' "$planted_assumptions" | grep -q "Closed under the global context"; then - viol "2. the kernel reported the Admitted control as closed — axiom tracking is blind" + viol "K3. the kernel reported the Admitted control as closed — axiom tracking is blind" else - ok "2. the kernel does not report the Admitted control as closed" + ok "K3. the kernel does not report the Admitted control as closed" fi -# --- 3/4. Lean 4: closed proof accepted, planted sorry detected ------------- lean_clean="$( cd "$CONTROLS" && lean Control.lean 2>&1 )" if printf '%s' "$lean_clean" | grep -q "does not depend on any axioms"; then - ok "3. #print axioms reports the closed Lean control as axiom-free" + ok "K4. #print axioms reports the closed Lean control as axiom-free" else - viol "3. #print axioms did not report the closed Lean control as axiom-free" + viol "K4. #print axioms did not report the closed Lean control as axiom-free" printf '%s\n' "$lean_clean" | sed 's/^/ /' | head -20 fi lean_planted="$( cd "$CONTROLS" && lean PlantedSorry.lean 2>&1 )" if printf '%s' "$lean_planted" | grep -q "sorryAx"; then - ok "4. #print axioms exposes sorryAx in the planted Lean control" + ok "K5. #print axioms exposes sorryAx in the planted Lean control" else - viol "4. #print axioms did not expose sorryAx — Lean axiom tracking is blind" + viol "K5. #print axioms did not expose sorryAx — Lean axiom tracking is blind" printf '%s\n' "$lean_planted" | sed 's/^/ /' | head -20 fi -if bash "$GATE" --scan-file "$CONTROLS/PlantedSorry.lean" >/dev/null 2>&1; then - viol "4. the escape-hatch scan ACCEPTED a proof closed with sorry" -else - ok "4. the escape-hatch scan rejects the planted Lean sorry control" -fi -if bash "$GATE" --scan-file "$CONTROLS/Control.lean" >/dev/null 2>&1; then - ok "4. the escape-hatch scan accepts the closed Lean control (no false positive)" -else - viol "4. the escape-hatch scan rejected the closed Lean control (false positive)" -fi - -# --- 5. a grade with no evidence behind it must be refused ------------------ -jq '(.theorems[0].grade) = "2i"' "$LEDGER" > "$WORK/planted-grade.json" -if bash "$GATE" --ledger "$WORK/planted-grade.json" >"$WORK/planted-grade.log" 2>&1; then - viol "5. the ledger gate ACCEPTED a grade 2i claim with no translated leg" -else - ok "5. the ledger gate refuses a grade 2i claim with no proven leg behind it" -fi -if grep -q "grade 2i requires exactly one proven recheck leg" "$WORK/planted-grade.log"; then - ok "5. and it says which clause was violated" -else - viol "5. the ledger gate failed for an unexpected reason" - sed 's/^/ /' "$WORK/planted-grade.log" | tail -10 -fi - -# --- 6. a witness on disk with no ledger row must be refused --------------- -sandbox="$WORK/repo" -mkdir -p "$sandbox" -tar --exclude=.git --exclude=target -cf - . 2>/dev/null | ( cd "$sandbox" && tar -xf - ) -printf 'Theorem unlisted_witness : True.\nProof. exact I. Qed.\n' \ - > "$sandbox/verification/proofs/coq/UnlistedWitness.v" -if ( cd "$sandbox" && bash scripts/check-proof-ledger.sh ) >"$WORK/unlisted.log" 2>&1; then - viol "6. the ledger gate ACCEPTED a witness that is in neither the ledger nor the MANIFEST" -else - ok "6. the ledger gate refuses an unlisted witness on disk" -fi -if grep -q "witness on disk is not claimed in the ledger" "$WORK/unlisted.log"; then - ok "6. and it names the unclaimed witness" -else - viol "6. the unlisted-witness control failed for an unexpected reason" - sed 's/^/ /' "$WORK/unlisted.log" | tail -10 -fi echo "" if [ "$VIOLATIONS" -gt 0 ]; then @@ -168,11 +122,12 @@ if [ "$VIOLATIONS" -gt 0 ]; then exit 1 fi echo "PASS: every control behaved as required — the instrument passes what should pass" -echo " and fails what must fail ($CHECKS expectation(s))." +echo " and fails what must fail ($CHECKS kernel expectation(s); the ledger-form" +echo " controls reported their own count above)." # Machine-readable evidence: annotations are retrievable through the check-run # API, so "how many expectations actually ran?" is answerable without the raw # runner log (which GitHub does not serve to every client). if [ -n "${GITHUB_ACTIONS:-}" ]; then - echo "::notice::proof-witness instrument verified both ways (§7): $CHECKS expectation(s), 0 violations, coqc $(coqc --version | head -1), lean $(lean --version | head -1)" + echo "::notice::proof-witness kernel controls verified both ways (§7): $CHECKS expectation(s), 0 violations, coqc $(coqc --version | head -1), lean $(lean --version | head -1)" fi exit 0 diff --git a/tests/proofs/run-ledger-controls.sh b/tests/proofs/run-ledger-controls.sh new file mode 100755 index 0000000..38d7356 --- /dev/null +++ b/tests/proofs/run-ledger-controls.sh @@ -0,0 +1,155 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# run-ledger-controls.sh — the ledger/scan half of the both-ways verification of +# the proof instrument (standards/3-practice/PROOF-POLICY.adoc §7). +# +# These controls need no prover: they exercise the rules that decide whether a +# RECORDED claim is honest — the escape-hatch scan, the grade/evidence +# arithmetic, statement and flag drift, and the history rules of mathesis §6. +# The kernel-level half (a closed proof accepted, `Admitted`/`sorry` rejected by +# the kernel's own axiom query) needs coqc and lean and lives in +# run-controls.sh, which calls this script first. +# +# Every control that must FAIL is checked for the specific refusal, not just for +# a non-zero exit: a gate that fails for the wrong reason is not doing its job. +# +# Exit: 0 all controls behaved; 1 an expectation was violated; 2 BLOCKED (a +# tool the controls need — jq — is missing). + +set -uo pipefail + +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd)" +cd "$ROOT" || exit 2 + +CONTROLS="tests/proofs/control" +GATE="scripts/check-proof-ledger.sh" +LEDGER="verification/proofs/LEDGER.json" + +VIOLATIONS=0 +CHECKS=0 +ok() { CHECKS=$((CHECKS + 1)); echo " ✅ $*"; } +viol() { echo " ❌ $*"; VIOLATIONS=$((VIOLATIONS + 1)); } + +command -v jq >/dev/null 2>&1 || { + echo "BLOCKED: these controls need jq to plant violations; not found on PATH." >&2 + exit 2 +} +[ -f "$LEDGER" ] || { echo "BLOCKED: no ledger at $LEDGER" >&2; exit 2; } + +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT + +echo "=== Ledger-form controls (no prover needed) ===" + +# expect_refusal