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..17ae3f7 --- /dev/null +++ b/.github/workflows/proof-ci.yml @@ -0,0 +1,463 @@ +# This workflow is managed by gh actions-lock. +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Proof CI — audits the proof ledger and compiles the recheck legs it declares, +# via `just proof-witness-check` (issue #57). +# +# Scope, per metadatastician/standards 3-practice/PROOF-POLICY.adoc (the pin +# this repository audits against is in LEDGER.json .policy.proof_policy) and mathesis +# `estate-mathematical-architecture`: +# +# * §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), +# audited for form here, and re-typechecked on every run (`just proof-check-agda`) +# under `agda --safe --without-K --cubical-compatible`. +# * §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 (`coqchk -silent -o` + `Print Assumptions` for Rocq; `#print axioms` +# for Lean). 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 runs +# two halves: run-ledger-controls.sh (55 ledger 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 (17 kernel & witness controls) verifies `check-proofs.sh` +# both ways on closed, declared-axiom, cross-module imported-axiom, +# cross-module `sorryAx`, and `Admitted`-in-`.axioms` witnesses. +# +# 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 +# `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 +# +# 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. +# +# 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.4 (tag + commit asserted), echo-types and +# absolute-zero pinned by commit, each re-verified after checkout +# +# 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: + 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/check-proof-ledger.sh' + - 'scripts/check-proofs.sh' + - 'scripts/proof-scan-dangerous.sh' + - 'tests/proofs/**' + - 'Justfile' + - 'PROOF-NEEDS.adoc' + - 'PROOF-STATUS.adoc' + # Scanner policy inputs. .trusted-base-ignore decides which files the + # escape-hatch scan exempts and docs/proof-debt.md is the register it + # requires: changing either changes what the gate means, so either must + # run the gate. + - '.trusted-base-ignore' + - 'docs/proof-debt.md' + - 'docs/proof-debt.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/check-proof-ledger.sh' + - 'scripts/check-proofs.sh' + - 'scripts/proof-scan-dangerous.sh' + - 'tests/proofs/**' + - 'Justfile' + - 'PROOF-NEEDS.adoc' + - 'PROOF-STATUS.adoc' + # Scanner policy inputs, as in the push filter above. + - '.trusted-base-ignore' + - 'docs/proof-debt.md' + - 'docs/proof-debt.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' + # 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.4' + STDLIB_COMMIT: '2a5a0dec0a3cb5c87468ce101388a513d39dbf10' + # 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-witness-check (strict) + runs-on: ubuntu-24.04 + timeout-minutes: 45 + permissions: + contents: read + + steps: + - name: Checkout + uses: actions/checkout@v7.0.1 + with: + # Nothing later in the lane pushes; the one clone it makes is of a + # public library. Leaving the job token in .git/config would be a + # credential in a runner that only reads. + persist-credentials: false + + - name: Install pinned Agda (official binary, sha256-verified) + run: | + set -euo pipefail + mkdir -p "$RUNNER_TEMP/agda" "$HOME/.local/bin" + # The scheme is written at the call site and pinned with --proto so a + # redirect cannot downgrade the transfer to clear text: the archive is + # the interpreter for every Agda receipt in the ledger. + curl -fsSL --proto '=https' --proto-redir '=https' --tlsv1.2 \ + -o "$RUNNER_TEMP/agda.tar.xz" \ + "https://github.com/agda/agda/releases/download/v${AGDA_VERSION}/Agda-v${AGDA_VERSION}-linux.tar.xz" + 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: 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" + mkdir -p "$RUNNER_TEMP/lean-dl" "$RUNNER_TEMP/lean" + curl -fsSL --proto '=https' --proto-redir '=https' --tlsv1.2 \ + -o "$RUNNER_TEMP/lean-dl/$NAME" \ + "https://github.com/leanprover/lean4/releases/download/v${LEAN_VERSION}/${NAME}" + # 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: | + 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" + 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.4). + 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, 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%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" + 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 "rocq: $(coqc --version | head -n1)" + echo "coqchk: $(coqchk --version 2>&1 | 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" + 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; } + coqc --version | grep -F "${ROCQ_VERSION}" \ + || { echo "::error::Rocq version is not the pinned ${ROCQ_VERSION}"; coqc --version; exit 1; } + command -v coqchk >/dev/null 2>&1 \ + || { echo "::error::coqchk is missing from the Rocq installation"; 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 + + # 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 + mkdir -p "$PROOF_RECEIPT_DIR" + bash tests/proofs/run-controls.sh 2>&1 | tee "$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-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 after the ledger gate succeeded" + exit 1 + 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 + # the PR and via the check-run API without unzipping raw runner logs. + - name: Surface prover diagnostics + if: failure() + run: | + set -uo pipefail + found_log=0 + for candidate in "$RUNNER_TEMP/proof-controls.log" "$RUNNER_TEMP/proof-witness-check.log" "$RUNNER_TEMP/proof-agda.log"; do + [ -f "$candidate" ] || continue + found_log=1 + label="$(basename "$candidate")" + PAYLOAD="$(grep -vE '^[[:space:]]*$' "$candidate" | tail -n 40 | tail -c 3500 | sed ':a;N;$!ba;s/\n/%0A/g')" + echo "::error::${label} tail:%0A${PAYLOAD}" + { + echo "### ${label} tail (failure diagnostics)" + echo '```' + tail -n 60 "$candidate" + echo '```' + } >> "$GITHUB_STEP_SUMMARY" + done + if [ "$found_log" -eq 0 ]; then + echo "::error::proof-ci failed before producing step logs; see the step logs above" + fi + + - 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/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml index 2c216f1..81684b6 100644 --- a/.github/workflows/workflow-linter.yml +++ b/.github/workflows/workflow-linter.yml @@ -70,9 +70,18 @@ jobs: XDG_DATA_HOME: ${{ runner.temp }}/workflow-linter-data run: | # Binary extensions accept release tags, not source commit pins. - # Verify the v0.1.6 linux-amd64 release bytes before executing them. - gh release download v0.1.6 --repo github/gh-actions-lock --pattern linux-amd64 --output "$RUNNER_TEMP/gh-actions-lock" - echo "4181ec1da5408b34b9a542a7ee5c6ce3a4d6ac815c7d0206a00ceca8a817f4e3 $RUNNER_TEMP/gh-actions-lock" | sha256sum --check --strict + # Verify the v0.4.0 linux-amd64 release bytes before executing them. + # + # v0.4.0 bundles actions-lockfile go v0.0.6, which reads lockfile + # v0.0.3 — the version the current tool writes. The v0.1.6 binary + # pinned here before bundled go v0.0.4 and caps out at lockfile + # v0.0.2, so it aborted with "lockfile version v0.0.3 is newer than + # this binary supports" as soon as anything wrote the lock with a + # current release. That is a tool-version gate, not a finding about + # our pins: the pin has to track the schema the estate writes, or + # this step reports red on a perfectly covered lockfile. + gh release download v0.4.0 --repo github/gh-actions-lock --pattern linux-amd64 --output "$RUNNER_TEMP/gh-actions-lock" + echo "f9da98f2a6e9e0ae77deadf9a2319a8a86bb002b541cc3203b247cc59fb04842 $RUNNER_TEMP/gh-actions-lock" | sha256sum --check --strict chmod +x "$RUNNER_TEMP/gh-actions-lock" "$RUNNER_TEMP/gh-actions-lock" --verify-local diff --git a/.machine_readable/bot_directives/placement.a2ml b/.machine_readable/bot_directives/placement.a2ml index f3232cf..893ff4c 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 `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", "TypeLL kernel proofs -> typell", diff --git a/.machine_readable/descriptiles/NEUROSYM.a2ml b/.machine_readable/descriptiles/NEUROSYM.a2ml index e9930ed..d4ce74c 100644 --- a/.machine_readable/descriptiles/NEUROSYM.a2ml +++ b/.machine_readable/descriptiles/NEUROSYM.a2ml @@ -3,15 +3,23 @@ # # NEUROSYM.a2ml — Neurosymbolic integration metadata # Configuration for Hypatia scanning and symbolic reasoning. +# +# Local divergence from the fleet template written by gitbot-fleet +# (robot-repo-automaton/templates/skeleton/): that template still says +# report-format = "logtalk", removed as a Hypatia format on 2026-04-14. +# Reported upstream: https://github.com/hyperpolymath/gitbot-fleet/issues/641 [metadata] -version = "0.1.0" -last-updated = "2026-06-12" +version = "0.2.0" +last-updated = "2026-11-01" [hypatia-config] scan-enabled = true scan-depth = "standard" # quick | standard | deep -report-format = "logtalk" +# JSON AssailReport from panic-attack. Logtalk was removed as a report format on +# 2026-04-14 (hypatia .machine_readable/descriptiles/NEUROSYM.a2ml); the "logtalk" +# value that shipped in the fleet template is dead and this repo emits no .lgt. +report-format = "json" [symbolic-rules] # Custom symbolic rules for this project diff --git a/.machine_readable/integrations/verisimdb.a2ml b/.machine_readable/integrations/verisimdb.a2ml index 78ca1f0..b646e36 100644 --- a/.machine_readable/integrations/verisimdb.a2ml +++ b/.machine_readable/integrations/verisimdb.a2ml @@ -2,16 +2,29 @@ # OPTIONAL: VeriSimDB Feed — Cross-Repo Analytics Data Store # Delete this file if your project does not feed data to VeriSimDB. # See https://github.com/hyperpolymath/nextgen-databases for details. +# +# Local divergence from the fleet template written by gitbot-fleet's +# scripts/fix-missing-verisim-feed.sh: that template says format = "hexad" and +# destination = "verisim-data/feeds/", neither of which exists in VeriSimDB. +# Reported upstream: https://github.com/hyperpolymath/gitbot-fleet/issues/640 [integration] name = "verisimdb" type = "data-feed" -repository = "https://github.com/hyperpolymath/nextgen-databases" +# The engine is verisimdb; nextgen-databases is only the research parent. +repository = "https://github.com/hyperpolymath/verisimdb" +parent = "https://github.com/hyperpolymath/nextgen-databases" data-store = "verisimdb-data" [feed-config] emit-scan-results = true emit-build-metrics = true emit-dependency-graph = true -format = "hexad" -destination = "verisimdb-data/feeds/" +# The record schema is the octad (8 modal witnesses). "HEXAD" is a LEGACY VCL +# keyword for the octad source, kept in verisimdb's surface grammar v3.0 for +# backward compatibility — it is a query keyword, not a wire format. Records +# carry "schema": "verisimdb.octad.v1" (see verisimdb-data scans/octads/). +format = "verisimdb.octad.v1" +# The store's layout (verisimdb-data README): scans/ holds per-repo results and +# scans/octads/ holds octad records. There is no feeds/ directory. +destination = "verisimdb-data/scans/octads/" diff --git a/.trusted-base-ignore b/.trusted-base-ignore new file mode 100644 index 0000000..02817ea --- /dev/null +++ b/.trusted-base-ignore @@ -0,0 +1,13 @@ +# SPDX-License-Identifier: MPL-2.0 +# Comments start with `#`. +# Each non-comment line is a path-fragment substring match against the +# repo-relative file path. Narrow the fragment to avoid hiding adjacent +# findings. +# +# Scanner test fixtures: exist solely to verify the detector fires. +# tests/proofs/control/PlantedAdmitted.v and PlantedSorry.lean contain a real +# `Admitted` and a real `sorry` on purpose. The instrument must reject them — +# tests/proofs/run-controls.sh asserts that it does — so documenting them as +# debt would be wrong twice: they are not soundness holes in this repository, +# and the whole point is that they stay detectable. +tests/proofs/control/ diff --git a/CLAUDE.md b/CLAUDE.md index af63d59..690d647 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -49,7 +49,7 @@ katagoria → typell → typed-wasm → PanLL (TypeFix Zero / μType₀ sit | TypeFix Zero / μType₀ calibration calculus | `typefix-zero` | | AffineScript / Ephapax language code | `affinescript` · `ephapax` | | Query-language type safety (SQL/GraphQL/Cypher/SPARQL/VQL) | `typedqliser` · `vcl-ut` | -| Tropical / semiring type theory (Isabelle/Lean) | `tropical-resource-typing` | +| Tropical / semiring type theory (Isabelle/Lean) | `tropical-types` (renamed from `tropical-resource-typing`, 2026-09-09) | | Transport-adapter / max-plus pathfinding | `protocol-squisher` | | Any compiler/app code, single-project ABI/FFI, benchmarks, or tests | the owning project repo | @@ -61,6 +61,30 @@ The machine-readable form of this table is the source of truth: `.machine_readable/bot_directives/placement.a2ml`. It is enforced in CI by `.github/workflows/coordination-boundary.yml`. +## Proofs and verification + +The normative policy is *outside* this repository: +`3-practice/PROOF-POLICY.adoc` in `metadatastician/standards`, owner ruling +2026-10-26, amended 2026-11-01, pinned at commit +`46ee18323305d5b36e2eef936e47dd54c39ea736`. It is referenced, not vendored — a +bare path is a dangling citation, so name the commit or the URL. + +It decides *where* a proof lives: theory → **Agda**, rechecked in **Rocq and +Lean** (§2, with the canonical invocation in §2.1); engineering/ABI → **Idris2**; +Rust → Creusot, Ada → SPARK. A gate that enforces it must be verified **both +ways** (§7): it passes conforming input *and* fails a planted violation. + +Status lives in `verification/proofs/LEDGER.json`, never in prose: + +```bash +just proof-witness-check # CI target: registry gates + ledger audit + declared recheck legs +just proof-grade # the grade ladder and the delta to the next rung +bash tests/proofs/run-controls.sh # the §7 controls (ledger-form + kernel) +``` + +A missing prover is **BLOCKED**, never a skip. `docs/decisions/` records the +local rulings where they differ from the policy, including what was superseded. + ## After the boundary, follow the estate conventions 1. Read `0-AI-MANIFEST.a2ml`, then `.machine_readable/descriptiles/STATE.a2ml`. diff --git a/Justfile b/Justfile index d8ebaee..537cc9f 100644 --- a/Justfile +++ b/Justfile @@ -1335,147 +1335,151 @@ 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 - @echo "=== All proof checks complete ===" +# Proof work follows metadatastician/standards 3-practice/PROOF-POLICY.adoc +# (owner ruling 2026-10-26, amended 2026-11-01). The commit this repository +# audits against is pinned in verification/proofs/LEDGER.json .policy.proof_policy, +# and scripts/check-proof-ledger.sh fails when that pin is missing: +# * 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) +# +# This repository's proof CI audits verification/proofs/LEDGER.json, compiles and +# kernel-queries any declared §2 recheck legs (Rocq and Lean) via +# `just proof-witness-check`, and separately re-typechecks the §1 Agda source leg +# via `just proof-check-agda` once the pinned Agda libraries are registered. +# +# 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. +# +# 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 -# 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" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do - echo -n " Checking $f ... " - if idris2 --check "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Idris2 proof(s) failed" - exit 1 - fi - echo "PASS: All Idris2 proofs verified" +# 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" + +# 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" + +# 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" -# Check Lean4 proofs +# Compile Rocq recheck witnesses per verification/proofs/coq/MANIFEST and query +# kernel assumptions (coqchk -silent -o + Print Assumptions) against LEDGER.json. +# Fatal if coqc/coqchk/coqtop is absent when work exists: never a skip. +# +# Compile and assumption-check the declared Rocq recheck witnesses +proof-check-coq: + @bash scripts/check-proofs.sh coq --receipt "${PROOF_RECEIPT_DIR:-target/proof-receipts}/witness-coq.txt" + +# Compile Lean 4 recheck witnesses per verification/proofs/lean4/MANIFEST and +# query kernel assumptions (#print axioms probe) against LEDGER.json. +# Fatal if lean is absent when work exists: never a skip. +# +# Compile and assumption-check the declared Lean 4 recheck witnesses 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" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do - echo -n " Checking $f ... " - if lean "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Lean4 proof(s) failed" - exit 1 - fi - echo "PASS: All Lean4 proofs verified" + @bash scripts/check-proofs.sh lean4 --receipt "${PROOF_RECEIPT_DIR:-target/proof-receipts}/witness-lean4.txt" -# Check Agda proofs +# Re-typecheck the Agda SOURCE leg under `agda --safe --without-K --cubical-compatible`. +# Invoked as a dedicated step in .github/workflows/proof-ci.yml (after library +# registration) and available locally once nextgen-typing, standard-library, +# echo-types and absolute-zero are registered in /libraries + defaults. +# +# Re-typecheck the Agda source leg (needs registered libraries) 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" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/agda -name '*.agda' 2>/dev/null); do - echo -n " Checking $f ... " - if agda --safe "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Agda proof(s) failed" - exit 1 - fi - echo "PASS: All Agda proofs verified" + @bash scripts/check-proofs.sh agda --receipt "${PROOF_RECEIPT_DIR:-target/proof-receipts}/witness-agda.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" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do - echo -n " Checking $f ... " - if coqc "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Coq proof(s) failed" - exit 1 - fi - echo "PASS: All Coq proofs verified" +# 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 --receipt "${PROOF_RECEIPT_DIR:-target/proof-receipts}/witness-idris2.txt" -# Scan for dangerous patterns in proof files (believe_me, sorry, Admitted, etc.) -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" +# 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 +# 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' 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 "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 "" - 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)" + 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" + + +# 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 AT LEAST ONE independent proven recheck leg (Rocq or Lean),\n" + + " with its route (transported through Dedukti/Lambdapi, or re-proved by hand),\n" + + " the statement comparison against the Agda declarations, and the kernel\n" + + " assumption query recorded. Proven today: 0." + 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-NEEDS.adoc b/PROOF-NEEDS.adoc index c3cd384..88f39fa 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -15,8 +15,26 @@ ____ === Proof Tier -*Tier*: T5 — Exempt (coordination layer; no owned code to prove). -Cross-project proofs are hosted, not mandated. +*Tier*: T5 — Exempt from the RSR template's *mandated* obligations +(coordination layer; no owned code to prove). Cross-project proofs are hosted, +not mandated. + +*Exempt is not outside the policy.* Reading T5 as "the proof policy does not +apply here" would license exactly the weak treatment the estate policies exist +to prevent, so this repository states the other reading, which is the true one: + +. **Hosting a proof makes this repo proof-bearing.** It owns no code to prove, + but it owns the proof it hosts. `docs/TRUSTED-BASE-REDUCTION-POLICY.adoc` + requires a `docs/proof-debt.md` from a proof-bearing repo, and PROOF-POLICY §7 + requires any gate enforcing the policy to be verified both ways — both apply + here, and both are wired. +. **"Not mandated" is about starting a proof, not about finishing one.** XP-1 is + recorded `proven` at Grade 3 (mathesis §5), which puts it under PROOF-POLICY §2 + like any other theory proof: a Rocq recheck leg and a Lean recheck leg are + owed. They are `open`, reported as policy gaps on every run, and the grade is + held at 3 rather than inflated. +. **A hosted proof is not a lower grade.** The rungs are about the proof, not + about which repository stores it. === Cross-Project Proofs (the only category that applies here) @@ -66,11 +84,29 @@ 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+`) 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+`, 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 * 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+` -* Proof status tracking: `+PROOF-STATUS.md+` (this repo) +* CI guard (proofs): `+scripts/check-proof-enrolment.sh+`, +`+scripts/proof-scan-dangerous.sh+` / `+.github/workflows/proof-ci.yml+` +* Proof status tracking: `+PROOF-STATUS.adoc+` (this repo) diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 4b5741a..8245178 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -1,53 +1,614 @@ +// SPDX-License-Identifier: MPL-2.0 + == Proof Status — nextgen-typing ____ 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*; +each theorem's presence and documented grade in the summary table are checked +against the ledger, and `+just proof-ledger-check+` fails if they differ. +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. + +=== 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. + +Four caveats belong to that sentence, and the ledger carries them in +`+caveats+` so the gate can refuse a record that drops one: + +. **echo-types' identity claim is open.** What is proven here is a statement + about *this pipeline's* operations. The claim that `+Echo+` *is* the identity + of structured loss is echo-types' own, and at the pinned revision it is open + by design: their README says "Positive identity is open ... Criterion 2 is + open". Citing XP-1 for that claim would be circular. If echo-types closes + criterion 2, XP-1 inherits it; until then XP-1 consumes a construction, it does + not witness the thesis. +. **absolute-zero is a proof-bearing consumer with 61 undischarged axioms** and + OND-6 open by design. None of its Coq is in this proof's import cone — it + reaches us only through echo-types' library manifest — but the record must not + be read as saying that repository is axiom-free. +. **epistemic-types is a sibling, not a dependency.** That repository formalises + the same object from a different premise: its `EchoBridge.Echo` is a *certified + residue* (`residue`, `certified : Cert residue y`) over a `Retention` record, + while the `Echo` used here is echo-types' fibre `Σ A (λ x → f x ≡ y)`. Neither + imports the other. XP-1 says nothing about epistemic-types' warrant transport + (`checkerSound`, `proofCannotSupportFalse`, `opaqueNotCertifying`, + `verifyReceiptIsGap`) or its `ForgedResidue` rejection; the ledger records it + under `related_developments` with `consumed_by_this_proof: false`, and the gate + refuses a record that claims otherwise. +. **No second kernel has checked this.** The Rocq and Lean legs are open, so the + theorem is Grade 3 and no waiver is claimed: §4 waives a leg when a statement + cannot be expressed in the mapped prover, not when the estate has archived one. + +=== 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. + +=== Corroboration: the same proof under a second Agda + +The receipt is one run of one toolchain. On 2026-11-01 the two modules were also +type-checked in an agent sandbox with a *different* Agda — 2.7.0.1 (PyPI +manylinux wheel, GHC 9.6.5) rather than the pinned 2.8.0 — against agda-stdlib +v2.3 (and again against v2.4), echo-types `+b0982c44+` and absolute-zero +`+f486c29+`, under the same canonical invocation: + +[source,bash] +---- +agda --safe --without-K --cubical-compatible EchoTyping.agda +agda --safe --without-K --cubical-compatible Verification.agda +---- + +Both passed, with only the `+-WnoUnsupportedIndexedMatch+` warnings that come +from echo-types' own indexed matches. The environment was shown to reject a +planted `+⊥+` (Agda exit 42) in the same session, so the pass is not vacuous. + +This is recorded in the ledger as `+local_evidence+` and it is deliberately +*not* the receipt: §2.1 pins the compiler version with the result, and a run at +a different version cannot carry the grade. It answers a different question — +"is this proof an artifact of one toolchain?" — and the gate refuses a local run +that sets `+corroboration_only+` to anything but true. + +=== Where each requirement comes from, and how it is met + +Two documents govern this, and they are not the same kind of document +(`+mathesis+` `+docs/standards/AUTHORITY.adoc+`). `+metadatastician/standards+` +`+3-practice/PROOF-POLICY.adoc+` (pinned at `+46ee1832+`, owner ruling +2026-10-26, amended 2026-11-01) is the sole normative estate proof policy: it +says **where a proof lives, which provers own which obligations, and how a +theorem is rechecked**. `+mathesis+` `+docs/proposals/estate-mathematical-architecture.adoc+` +is an unratified architectural framework that **defines the grade ladder** (§5) +and the **evidence/receipt discipline** (§6, §11), supplemented by `+mathesis+` +`+docs/status/CROSS-PROVER-RECONCILIATION.adoc+` (`+AGDA-VERIFIED+`, +`+NOT-INVENTORIED+` / `+COQ-CHECKED+` / `+LEAN-CHECKED+`, `+BRIDGE-PENDING+` / +`+RECONCILED+`) so source verification, target kernel checking, and +correspondence justification are never collapsed into one number. Where any +proposal example differs from `+PROOF-POLICY.adoc+`, the standards ruling +governs. + +[cols="14%,34%,36%,16%",options="header",] +|=== +|Source |Requirement |Where it is met |State +|mathesis §5 |Grade 3: the proof type-checks in Agda |Agda 2.8.0 + agda-stdlib v2.4, +`+EchoTyping.agda+` and `+Verification.agda+`, receipt run 41314454646 at +`+3cd1859+`; re-typechecked on every CI run by `+just proof-check-agda+`, not +taken from the file's existence |met +|mathesis §5 |Grade 3: *not translated* to an independent foundational system +|Both recheck legs are `+open+`. This is what makes the rung 3 rather than 2i — +and it is simultaneously the gap PROOF-POLICY §2 makes an obligation |met, and +reported every run +|mathesis §5 |Grade 3 relies on strict solver flags (parenthetically +`+--safe --erasure+`, or Full `+--cubical+`) |In force: `+--safe --without-K +--cubical-compatible+`. Neither named configuration exactly; the difference is +recorded in `+grade_deviation+`, and PROOF-POLICY §2.1 (later, normative) fixes +this combined invocation as canonical |deviation, recorded +|mathesis §5 (family note) |The dual-translation rung (`+2ii+`) needs a *non-DTT* +second architecture +|The gate's `+FAMILIES+` map records agda/rocq/lean4 as `+dtt+`, isabelle as +`+hol+`. Unreachable while both legs are DTT, so it is not claimed |recorded +|mathesis §6 |Do not flatten confidence into a percentage |Tokens only; nothing +in this file or the gate averages anything, and `+just proof-grade+` prints +"recorded, not estimated" |met +|mathesis §6 |Axiom tracking: postulates, `+#print axioms+`, `+Print Assumptions+`, +pinned library versions |Source leg: zero postulates under `+--safe+`, with +pinned Agda, stdlib, echo-types and absolute-zero. Recheck legs: no axiom list, +because no witness exists — recording one would be fabrication |met, and the gap +stated +|mathesis §6 |Track the exact Git commit of the verification receipt |`+3cd1859…+` +in the ledger; the gate refuses a receipt that is not a full 40-character SHA +|met +|mathesis §6 |`+Superseded+` and `+Regressed+` are first-class states |Every +historical receipt carries `+state+` (`+superseded+` for the pre-§2.1 one) and a +reason; the gate refuses an unmarked archived receipt or a state outside the pair +|met +|mathesis §11 |Reject silent index drift, proof inflation and false verification +claims; report unavailable evidence plainly |Statement anchors must exist in the +source files, flags are read out of the files and the instrument rather than +copied, unclaimed witnesses are refused in both directions, and the policy gaps +print on every run |met +|=== + +=== 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 **41314454646** at +`+3cd185939179773f177b59e6fee360719695dfc7+` — the first run that invoked the +policy's canonical form, `+agda --safe --without-K --cubical-compatible+` +(PROOF-POLICY §2.1, amended 2026-11-01), through `+just proof-check-agda+`. + +The earlier receipt (run 41299544043 at `+4c6b918+`) invoked `+--safe+` with the +library manifest only: `+--without-K+` came from the file's `+{-# OPTIONS #-}+` +and `+--cubical-compatible+` was never passed. §2.1 says such a success is +*historical evidence, not a receipt* for the combined profile, so the ledger +keeps it as history and pins the canonical run. + +=== 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+` |At least *one* independent system (Rocq or Lean) carrying the same +statement: `+transported+` through Dedukti/Lambdapi, or `+re-proved+` by hand, +with the statement comparison, target declaration mapping, and verbatim kernel +assumption query recorded; no Mathlib. Completing *both* DTT legs (`+rocq+` + +`+lean4+`) satisfies `+PROOF-POLICY+` §2 while staying at rung `+2i+` until a +non-DTT leg is added +|*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 -[cols=",,,,",options="header",] +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 + +`+metadatastician/standards+` `+3-practice/PROOF-POLICY.adoc+` (pinned at +`+46ee1832+`) §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+`). +[[waivers]] +=== Waivers + +**No waiver is claimed for XP-1, and none is recorded in the ledger.** §4 of +`+3-practice/PROOF-POLICY.adoc+` waives a leg when the mapped prover cannot +*express* the statement — not when the estate has simply not built the witness +yet. The Rocq and Lean legs are absent for the second reason, so they are open +obligations, not waivers, and a waiver would be the wrong instrument even if it +were convenient. + +The ledger half of the rule is mechanical, and it is deliberately hard to +satisfy with a citation that does not exist. A waiver must carry an +`+obligation+`, a `+tool+`, a `+reason+` and a `+record+`; the `+record+` must be +`+[#]+` inside this repository, the path must exist, the anchor +must occur in the file, and the file must name the `+tool+`. Anything else — a +bare string, a plausible-looking filename, an anchor this page does not have — +is refused, because a waiver whose record cannot be read is an obligation +removed without a reason. Controls 26, 37 and 38 in +`+tests/proofs/run-ledger-controls.sh+` pin the three cases: a conforming +waiver is accepted and printed in the verdict, an unresolvable record is +refused, and an anchor that does not occur in the cited file is refused. + +This section is itself the anchor that a waiver record would cite +(`+PROOF-STATUS.adoc#waivers+`), which is why it exists before the first waiver +does. + +=== 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. + +**Enforced per compiled witness (issue #131 closed):** `+scripts/check-proofs.sh+` +does not stop at compiler exit status 0. Every `+gated+` Rocq or Lean module in +`+MANIFEST+` is compiled in an isolated scratch workspace and immediately +subjected to kernel-level assumption queries compared against the claiming leg's +`+axioms+` array in `+verification/proofs/LEDGER.json+`: -=== Proofs Present +* **Rocq (`+coq+`):** runs `+coqchk -Q . "" -silent -o +` on the + compiled `+.vo+` (requiring predicative `+Set+`, `++` for + `+type-in-type+`, unsafe `+(co)fixpoints+`, and assumed positivity, and + matching `+* Axioms:+` against `+legs[].axioms+`) *and* compiles a generated + probe that `+Require+`s `++` and executes `+Print Assumptions + ..+` for every mapped declaration, failing on any undeclared or + stale axiom — including standard-library or cross-module imported axioms that + carry zero banned lexical tokens. +* **Lean 4 (`+lean4+`):** compiles `+.olean+` and runs a generated probe + that `+import+`s `++` and executes `+#print axioms +` for every + mapped declaration, unconditionally rejecting `+sorryAx+` (even across module + imports or if listed in `+axioms+`) and failing on any undeclared or stale + ledger axiom. +* **Verbatim receipts:** `+just proof-check-coq+` and `+just proof-check-lean4+` + write the verbatim `+coqchk+`, `+Print Assumptions+`, and `+#print axioms+` + outputs into `+target/proof-receipts/witness-coq.txt+` and + `+target/proof-receipts/witness-lean4.txt+` (uploaded by `+proof-ci.yml+`). -[width="100%",cols="12%,15%,15%,17%,13%,28%",options="header",] +The Agda source leg rests on these pinned, recorded assumptions (all in the +ledger): + +[cols="22%,16%,62%",options="header",] +|=== +|Component |Kind |Pin, and what it is to this proof +|Agda |dependency-pin |2.8.0 +|agda-stdlib |dependency-pin |v2.4 (`+2a5a0dec0a3cb5c87468ce101388a513d39dbf10+`) +|echo-types |external development |`+b0982c44f36133acd2d0e1d4e03cf031fff7a470+` — +the library whose fiber construction XP-1 compares the pipeline's loss +operations against. Its own identity claim is **open** (see caveat 1 below). +|absolute-zero |proof-bearing consumer |`+f486c29903434589117fa0662c6f29b0f17d1d5f+` — +115 Qed / 0 Admitted / **61 undischarged axioms**, OND-6 open by design. It +reaches this proof only through echo-types' library manifest; none of its Coq is +in the import cone. +|Receipt commit |receipt |`+3cd185939179773f177b59e6fee360719695dfc7+` (run 41314454646, canonical §2.1 invocation) |=== -|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+` -|`+agda Verification.agda+` + +These are not the same kind of entry, and the ledger says so: a *dependency-pin* +is a version, an *external development* is another repository whose own +obligations have to be recorded alongside it, and a *proof-bearing consumer* +consumes the estate's proof infrastructure rather than providing ground truth for +it. Three things follow, all enforced by the ledger gate: + +. A dependency that carries open obligations must be named in the theorem's + `caveats`. A theorem that lists 61 undischarged axioms against its own name + without saying so in prose would be read as axiom-free. +. The **import cone** is recorded, module by module, with its `{-# OPTIONS #-}` + flags and postulate counts (`+source.import_cone+`). `+--safe+` refuses an + import that is not itself safe, so that cone *is* the trust base for the "no + escape hatches" claim. At the pin it is `Echo`, `EchoCharacteristic` and + `EchoLinear`, all `+--safe --without-K --cubical-compatible+`, all with zero + postulates. The postulated modules in echo-types (`+EchoImageFactorizationPropPostulated+`, + `+Ordinal/Buchholz/Fidelity+`) are outside `+All.agda+` and outside this cone; + they are recorded as outside, not omitted. +. A claim about another repository needs evidence — the file and the date it was + read — and the gate refuses one that has none. + +The current caveats are listed under "The Grade 3 claim rests on". They are part +of the record, not decoration: the gate fails if an open obligation loses its +caveat. + +=== Enforcement (CI) + +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*, and this is where +that is done — in two halves. `+run-ledger-controls.sh+` (55 controls, no prover +needed) exercises grades, history, flags, formal declaration-to-type binding, +quarantined and out-of-order MANIFEST bypasses, `+sorryAx+` bans, reconciliation +status rules, external import-cone checks, waivers, debt-register presence, and +per-language comment-aware lexical scanning. +The kernel & witness half (`+K1+`–`+K17+`) checks `+coqc+`/`+coqchk+`/`+coqtop+` +and `+lean+` both directly and end-to-end through `+scripts/check-proofs.sh+`: +clean witnesses must pass and write verbatim `+CONTEXT SUMMARY+`, +`+Closed under the global context+`, and `+does not depend on any axioms+` +receipts; witnesses importing `+Coq.Logic.Classical_Prop.classic+` or +`+Classical.em+` (clean to lexical scan) must fail under `+axioms: []+` and pass +under `+proven-with-postulates+` naming the exact axioms; cross-module helper +axioms, cross-module `+sorryAx+`, `+Admitted+` theorems listed in `+.axioms+`, +out-of-order multi-file `+MANIFEST+` entries, missing declarations, and stale +`+axioms+` entries must all be refused. Where `+coqc+`, `+coqchk+`, `+coqtop+`, 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+`) +|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+`. + +|`+just proof-check-agda+` (and the Idris2/Lean4/Coq equivalents) +|Exits 1 (`+FAIL (missing-toolchain)+`) when proofs for that prover are enrolled +but the prover is absent, and exits 1 on any typecheck or kernel-assumption failure. + +|`+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-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.4 (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. |=== === 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 +# 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 -# Enforce the coordination boundary (no project code / non-allowlisted proofs) -bash scripts/check-coordination-boundary.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 + +# Registry gate, no prover needed: +bash scripts/check-proof-enrolment.sh --static-only ---- +=== Receipts + +[cols="16%,20%,64%",options="header",] +|=== +|Date |Receipt |Result +|2026-11-01 |proof-ci run 41314202374 (sha `+112a7bf+`) |**PASS** with the +grade-3 substantiation and the split controls in place. Annotations: +`+proof ledger controls: 15 expectation(s), 0 violations+` (grades, statements, +flags, history, unclaimed witnesses) and `+proof-witness kernel controls +verified both ways (§7): 6 expectation(s), 0 violations+` under coqc 8.18.0 and +lean 4.15.0, plus the census (1 theorem, 2 sources, 0 proven legs, 2 policy +gaps) and one `+::warning::+` per open leg. 21 expectations, none of them a +pass-by-absence. + +|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 +`+--safe --library=nextgen-typing+` against the then-current agda-stdlib v2.3, echo-types +`+b0982c4+` and absolute-zero `+f486c29+`, banned-pattern scan clean. This run is +*historical evidence only*: the receipt the ledger pins for the Agda leg is run +41314454646 (cited under "Assumptions and axiom tracking"), which superseded this +one when the stdlib moved to v2.4. Neither is 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; no proof source or safety flag was changed. + +|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 [width="100%",cols="32%,42%,26%",options="header",] |=== |Date |Change |By +|2026-11-01 |Closed issue #131 and aligned with `+mathesis+` authority & +cross-prover reconciliation guidance (`+docs/standards/AUTHORITY.adoc+`, +`+docs/proposals/estate-mathematical-architecture.adoc+`, +`+docs/status/CROSS-PROVER-RECONCILIATION.adoc+`). `+scripts/check-proofs.sh+` +now queries kernel-level assumptions for every gated Rocq (`+coqchk -silent -o+` ++ generated `+Print Assumptions+` probe) and Lean (`+import+` + `+#print axioms+` +probe) witness against `+LEDGER.json+` `+legs[].axioms+`, writing verbatim +assumption receipts (`+witness-coq.txt+`, `+witness-lean4.txt+`). Bidirectional +controls expanded to 55 ledger controls + 17 kernel/witness controls +(`+K1+`–`+K17+`) |Arena agent + +|2026-11-01 |Reconciled with the estate policy, which moved twice: owner ruling +2026-10-26, amended *today* (pinned `+46ee1832+`, recorded in the ledger, printed +by the gate, and a missing pin is now a failure). `+D-2026-10-12+` is amended +clause by clause — "Coq archived" and "Lean is provenance only" are superseded, +so the Rocq and Lean legs below are *obligations*, not waivers. The Agda receipt +was re-baselined: §2.1 makes a `+--safe+`-only run historical evidence, so the +pin moved to run 41314454646 (`+3cd1859+`, canonical invocation). Dependencies +are no longer two version strings: echo-types (identity claim open) and +absolute-zero (61 undischarged axioms) are recorded with what they are, with +evidence, and with caveats the gate refuses to see dropped; `+import_cone+` +records the 3-module trust base and what is deliberately outside it. XP-1's scope +is stated where a reader starts: it does not prove echo-types' identity claim. +Controls: 15 → 26 |Arena agent + +|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 +"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+` +(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/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc b/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc index 9c0c1d5..9b3e27e 100644 --- a/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc +++ b/docs/decisions/D-2026-10-12-proof-kernel-ruling.adoc @@ -7,6 +7,62 @@ Ruled by the owner, 2026-10-12, after a comparison recorded in the accompanying session. Supersedes per-repo prover choice for the family. +=== Amendment, 2026-11-01 — partly superseded + +The estate proof policy (`metadatastician/standards`, `3-practice/PROOF-POLICY.adoc`) +is an owner ruling of 2026-10-26, amended 2026-11-01, and states that *every* +hyperpolymorph repository follows it. It postdates this ruling, so where the two +disagree the policy governs. Nothing above is deleted: a superseded ruling is +still the record of what was decided, and of why. + +[cols="40%,20%,40%",options="header",] +|=== +|Clause of this ruling |Disposition, 2026-11-01 |Authority +|Agda `--safe --without-K` is the proof kernel of the type family |*stands* +|PROOF-POLICY §1 (theory → Agda, source of truth) and §2.1, which fixes the +canonical invocation as `agda --safe --without-K --cubical-compatible` — the +profile this repository's instrument (`scripts/check-proofs.sh`) already passes + +|Idris2 is the ABI/runtime layer, not a kernel candidate |*stands* +|PROOF-POLICY §1 (APIs, ABIs, engineering properties → Idris2) + +|Isabelle/HOL only for AFP submissions; existing Isabelle is supplementary +|*stands* +|PROOF-POLICY §3: an Isabelle proof of a theory statement satisfies neither the +Rocq leg nor the Lean leg + +|"Coq, Mizar: archived" |*superseded* +|PROOF-POLICY §2 requires a **Rocq** recheck leg for every Agda theory proof. +Coq/Rocq is therefore a required leg of a theory proof, not an archived tool. +The archive of absolute-zero's *own* Coq development (their notice of +2026-10-10) is their internal call, but it cannot discharge this repository's §2 +obligation. + +|"Lean 4 is provenance: tropical-types' Lean and Isabelle developments remain as +the Mathlib/AFP-facing record and are *ported*, not imported" |*partly +superseded* — the port-not-import distinction stands; "provenance only" does not +|PROOF-POLICY §2 requires a Lean recheck leg, and §2.2 requires per-theorem +correspondence evidence for it (exact proposition, assumptions, universe +discipline, revision, versions, invocation, observed result) + +|Effect on this repository's proof lane |`XP-1`'s Rocq and Lean legs are **open +obligations**, not waivers +|PROOF-POLICY §4 waives a leg when the statement *cannot be expressed* in the +mapped prover. A strategic archive decision is not that, so no waiver is +claimed and the lane must keep printing the gap. +|=== + +Two further consequences, both already reflected in the repository: + +. §2.1 says a prior `--safe` or `--safe --without-K` success is *historical + evidence, not a receipt* for the combined `--cubical-compatible` profile. The + Agda receipt pinned in `verification/proofs/LEDGER.json` was re-baselined onto + a canonical-invocation run; the earlier one is retained there as history. +. §6 requires proof toolchains to come from a Guix manifest or the container. The + proof lane installs Rocq and Lean 4 from the package index and the official + release archive instead. That is recorded as an open **deviation** in the + ledger's `policy.deviations`, not as a waiver. + == Decision . *Agda `--safe --without-K` is the proof kernel of the type family* diff --git a/docs/decisions/D-2026-11-01-policy-reconciliation.adoc b/docs/decisions/D-2026-11-01-policy-reconciliation.adoc new file mode 100644 index 0000000..0f3c3cb --- /dev/null +++ b/docs/decisions/D-2026-11-01-policy-reconciliation.adoc @@ -0,0 +1,200 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) += Policy reconciliation: where the estate's proof rules disagree, and which reading binds +:revdate: 2026-11-01 +:status: ADOPTED for this repository; upstream items are proposals pending owner ruling +:toc: + +A consistency audit of this repository's proof lane against the estate policies +found not one authority but five, and they do not say the same thing. Each +disagreement below has a weak reading and a strict reading. This record names the +reading this repository adopts, and what the upstream document would have to say +for the strict reading to be the only one available. + +Nothing here weakens a gate. Where the strict reading is ours to implement it is +implemented and controlled; where it is not, it is written as an owner-ruling +proposal rather than paraphrased into compliance. + +== The five documents, and what each actually owns + +[cols="32%,68%",options="header",] +|=== +|Document |What it owns +|`metadatastician/standards` `3-practice/PROOF-POLICY.adoc` (owner ruling +2026-10-26, amended 2026-11-01, pinned `46ee1832…`) +|*Where a proof lives*: prover mapping, the Rocq and Lean recheck obligation, the +canonical Agda invocation, the correspondence record, routes, waivers, the closed +status vocabulary, toolchains, and how to amend it. +|`metadatastician/standards` `docs/README-EXPLAINME-STANDARD.adoc` §5 +|A second, older definition of the proof ledger: a markdown table, the same +closed vocabulary, and a README scorecard row that *requires* a ratio. +|`metadatastician/standards` `docs/TRUSTED-BASE-REDUCTION-POLICY.adoc` (2026-05-27, +extended tier 2026-10-30) +|*Which escape hatches exist and what may be done with them*: the two tiers, the +four dispositions, `docs/proof-debt.md`, `.trusted-base-ignore`, +`.trusted-base-budget`, and `check-trusted-base.sh`. +|`hyperpolymath/mathesis` `docs/proposals/estate-mathematical-architecture.adoc`, +`docs/standards/AUTHORITY.adoc`, and `docs/status/CROSS-PROVER-RECONCILIATION.adoc` +|*The grade ladder, evidence contract, and non-collapsing reconciliation states*: +§5 Grade 3 / 2i / 2ii / 1 and the prover-family caveat; §6 record discipline, +axiom tracking, `Superseded`/`Regressed`; §11 no inflation; `AUTHORITY.adoc` +routes normative proof policy to `metadatastician/standards` while keeping home +repositories sovereign over theorem truth and receipts; +`CROSS-PROVER-RECONCILIATION.adoc` keeps `AGDA-VERIFIED`, `COQ-CHECKED` / +`LEAN-CHECKED`, and `BRIDGE-PENDING` / `RECONCILED` distinct. +|`metadatastician/standards` `3-practice/LANGUAGE-POLICY.adoc`, +`TOOLING-VERSION-INTEGRITY-POLICY.adoc` +|*How toolchains are installed and pinned*: Guix manifest or container; declared +floors, asserted versions, no silent transitive skew. +|=== + +PROOF-POLICY itself says which of these it defers to: escape hatches stay with +TRUSTED-BASE-REDUCTION-POLICY, and the canonical token list is the one in +README-EXPLAINME-STANDARD. It says nothing about mathesis, and mathesis says +nothing about the standards repository. That silence is where the weak readings +live. + +== The disagreements, and the strict reading + +[cols="4%,40%,28%,28%",options="header",] +|=== +|# |Disagreement, and the weak reading it licenses |Strict reading (adopted here) +|Fix belongs +|A1 |PROOF-POLICY §2.1 (2026-11-01) says first-party Agda entrypoints *shall* use +`--safe --without-K --cubical-compatible`. TRUSTED-BASE §"Why the prover +invocation is not standardised" says "How a repository invokes its prover is its +own business". *Weak:* cite the trusted-base document to keep a `--safe`-only +lane, which is exactly what §2.1 was amended to stop. +|§2.1 governs entrypoints; the trusted-base clause governs the *debt tooling* +(budgets, dispositions, detection) and is not a licence for entrypoint flags. +|Upstream: one sentence in each, cross-referencing the other's scope. +|A2 |mathesis §5 offers "Full `--cubical`" as a Grade-3 configuration. §2.1 +requires "an explicit, separately reviewed proof profile" for full Cubical. +*Weak:* a Full-Cubical development is Grade 3 with nothing recorded. +|Grade 3 rests on the configured, recorded profile. Full `--cubical` without a +recorded §2.1 profile is not a grade, it is an unreviewed configuration. +|Upstream (mathesis) + here (the profile would be recorded in the ledger). +|A3 |mathesis §5: 2i = translated to **one** alternative system. PROOF-POLICY §2: +rechecked in Rocq **and** Lean. *Weak:* claim 2i with one leg and let a reader +infer the policy is satisfied. +|A rung is not a discharge. 2i is a partial state; §2 still owes the second leg. +This repository's status text says so explicitly. +|Upstream (mathesis) + here (already stated) +|A4 |mathesis §6 requires `Superseded` and `Regressed` states. The closed +vocabulary of §5/README-EXPLAINME has neither. *Weak:* drop the lineage +requirement — observed here: a retained receipt carried no state until today. +|Lineage lives on the *receipt*, not on the status token: `historical_evidence[]. +state` + reason. The closed vocabulary stays closed. +|Implemented here (gate refuses an unmarked archived receipt). Upstream: both +documents should say this, or every repo will invent a token. +|A5 |README-EXPLAINME §5 requires the README scorecard "Proofs" row to show "the +count of `proven` rows over all rows". mathesis §6 forbids flattening confidence +into a percentage. *Weak:* quote whichever document flatters the moment. +|Ratios of *rows* are counts with a stated denominator, not confidence. No +document may be read as licensing a "percentage proved". This repo prints the +ladder and the delta to the next rung, and withdrew its "1 of 1 done" figure. +|Upstream: one sentence in each. +|A6 |Two ledger shapes: a markdown table (README-EXPLAINME §5) and a machine +ledger with a per-theorem correspondence record (PROOF-POLICY §2.2). *Weak:* keep +the easy one; gates then have nothing to read. +|One canonical machine ledger (this repo: `verification/proofs/LEDGER.json`); the +README table, where present, is derived from it and cites it. §5 already says the +machine ledger holds the canonical token — say it in README-EXPLAINME too. +|Here: the status file points at the ledger and the gate enforces it. Upstream: +state the precedence. +|A7 |PROOF-POLICY §1.1 makes reliance on a dependency's *behaviour* an `ASSUMED` +contract. It has no shape for a dependency whose definitions and theorems are +*kernel-checked* at import. *Weak:* treat the dependency as invisible +(over-claim) or as ASSUMED (under-claim). +|Third case, now recorded here: an import closure compiled under the prover's +safe mode with zero postulates is *checked, not assumed*, and the cone is +recorded module by module (`.source.import_cone`). +|Upstream (§1.1) + here (implemented) +|A8 |`proven-with-postulates` defers to TRUSTED-BASE(c), which cites MathLib4 as +an example of a canonical formalisation to point at — while §2 forbids Mathlib. +*Weak:* import the library, then cite it as justification. +|The two clauses govern different things: §2 forbids the *dependency*; TRB(c) +governs the *axiom*. An axiom may cite a canonical formalisation as justification +and must not enter through the library. +|Upstream: one sentence in both. +|A9 |§6 requires proof toolchains "through the repo's Guix manifest or its +container", with **no deviation mechanism** — unlike §4, which has one. *Weak:* +silently non-compliant, which is what this repository's recorded `§6` deviation +is: visible here, invisible to the policy. +|Either (i) §6 states an equivalence — an asserted version plus a recorded digest +from the upstream package/release index, recorded in the proof ledger, satisfies +the clause — or (ii) §6 gains a `deviation` field with §4's discipline. Until +then this repo either complies or records the gap and says the policy cannot see +it. +|Upstream (owner ruling). Here: the deviation is recorded, and the strict route +(a Guix manifest for the lane) is the default plan. +|A10 |mathesis defines Grade 1 (AXLE, coq-lsp REST, isabelle-server) but no +policy requires it. *Weak:* the strictest rung is unowned, so nobody is ever +obliged to reach it. +|State it: either Grade 1 is required for an estate-level "verified through a +checker API" claim, or it is explicitly aspirational and no status may be worded +to imply it. +|Upstream (mathesis + an owner ruling in the policy). +|A11 |§7 requires that "a gate that enforces this policy cites this file" — but +not that the citation be *pinned*. The policy moved twice in six days. +*Weak:* cite the path, audit against whatever the path says today. +|A citation names repository, path and the full 40-character commit it was read +at, and the gate fails without it. mathesis §11's "no silent index drift" says +the same from the other side. +|Implemented here (this repo's gate prints the pin and fails without it). +Upstream: §7 should require the pin. +|A12 |§4: "The theorem is complete when the Agda proof is PROVEN or +PROVEN-WITH-AXIOMS and every leg that is not waived is too." mathesis has no +notion of a waiver. *Weak:* report "complete", reader hears "Grade 2". +|A waiver never buys a rung: a theorem with a waived leg has no independent +witness, so it is at most Grade 3, and the word "complete" is about the policy's +own ledger, not about a grade. +|Implemented here (a waived leg carries no status at all, so nothing can count +it; the verdict lists waivers separately). Upstream: say it in §4. +|=== + +== The local document that was doing the same thing + +`PROOF-NEEDS.adoc` declared *Tier T5 — Exempt* and stopped. A reader — or an +agent — could take that as "the proof policy does not apply to this repo", which +would have excused the open Rocq and Lean legs. It now states the other reading: +exemption is from the RSR template's *mandated* obligations, and hosting a proof +makes this repository proof-bearing for the trusted-base policy and for §7. See +the file. + +== What was fixed here rather than argued + +* `docs/proof-debt.md` added, and `.trusted-base-ignore` for the instrument's + planted fixtures. The estate checker now reports + `core_undocumented=0` — before, `governance-reusable.yml`'s `trusted-base` job + failed this repository for having an escape hatch and no register. +* `scripts/proof-scan-dangerous.sh` widened to the estate's **core tier** + (Coq `Axiom`, Lean `axiom`, Idris2 `really_believe_me`/`partial`, F* `assume + val`/`admit_p`, `unsafePerformIO`), and the ledger gate no longer keeps a + second, narrower copy of the pattern list — it delegates. One list, one + meaning: a marker cannot be caught by one gate and missed by the other. + Controls 29 and 30 plant a Coq `Axiom` and remove the debt register. +* §2.1's canonical invocation, §5's closed vocabulary, §6's absence of a + deviation mechanism, and A11's pin are reflected in the gate and the ledger. +* `scripts/check-proofs.sh` (issue #131) now executes kernel-level assumption + queries for every gated Rocq (`coqchk -silent -o` + generated + `Print Assumptions` probe) and Lean (`import` + `#print axioms` probe) module, + comparing against `LEDGER.json` `legs[].axioms`, unconditionally rejecting + `sorryAx` and `Admitted` theorems listed in `.axioms`, writing verbatim + assumption receipts (`witness-coq.txt`, `witness-lean4.txt`), and exercising + both directions across `K6`–`K17` in `tests/proofs/run-controls.sh`. + +== What is still wrong, and is not this repository's to fix + +A1–A3, A5, A6, A8–A11 are owner-ruling items in the standards repository or in +mathesis. They are filed with the proposed strict text rather than described +here: standards#1389 carries A1, A6, A7, A8, A9, A11, A12; mathesis#11 carries +A2, A3, A4, A5, A10. Until they land, either reading can be defended by citation, and the +strict treatment depends on each repository choosing it. This repository chooses +it, records the choice, and gates it — which is the most a single repo can do. + +The one substantive gap left here is A9: the proof lane installs Rocq and Lean +from the package index and the release archive with asserted versions and a +recorded digest, and the policy has no lawful way to acknowledge that. Closing it +by compliance rather than by exemption means a Guix manifest (or the container) +carrying both provers, with the lane installing from it. diff --git a/docs/decisions/README.adoc b/docs/decisions/README.adoc index cb9c6d8..8080737 100644 --- a/docs/decisions/README.adoc +++ b/docs/decisions/README.adoc @@ -1,3 +1,27 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = decisions Unit + +== Decisions in this unit + +[cols="40%,20%,40%",options="header",] +|=== +|Decision |Status |Note +|`D-2026-10-12-proof-kernel-ruling.adoc` |partly superseded +|Prover mapping: the Agda-kernel, Idris2-ABI and Isabelle-supplementary clauses +stand; "Coq archived" and "Lean is provenance only" are superseded by the estate +`PROOF-POLICY` (owner ruling 2026-10-26, amended 2026-11-01). See the amendment +inside the document. + +|`D-2026-11-01-policy-reconciliation.adoc` |current +|Which document binds where: PROOF-POLICY vs mathesis vs the README-EXPLAINME +ledger vs TRUSTED-BASE-REDUCTION-POLICY. Twelve disagreements with the strict +reading named for each, and what is left for owner rulings. + +|`0001-adopt-rsr-standard.adoc` |current |Repository standard adoption. +|`0000-template.adoc` |template |Copy for a new decision; delete the guidance. +|=== + +A decision that has been superseded stays in this unit: it is the record of what +was decided and why. What changes is its status line, not its existence. + diff --git a/docs/proof-debt.md b/docs/proof-debt.md new file mode 100644 index 0000000..0628835 --- /dev/null +++ b/docs/proof-debt.md @@ -0,0 +1,76 @@ + + + +# Proof debt + +Dispositions per `docs/TRUSTED-BASE-REDUCTION-POLICY.adoc` (estate policy, +enforced by `scripts/check-trusted-base.sh` through `governance-reusable.yml`). +Scope: this repository is proof-bearing — `verification/proofs/agda/` carries +XP-1 (see `verification/proofs/LEDGER.json` and `PROOF-STATUS.adoc`). + +The file exists even though the answer is "nothing outstanding", because an +absent file is indistinguishable from an unexamined repository, and the policy +requires a proof-bearing repo to maintain one. + +## (a) Discharged in this repo + +- (none — no escape hatch has ever been present in this repository's proof + sources to discharge) + +`Verification.agda` and `EchoTyping.agda` declare `{-# OPTIONS --safe +--without-K #-}` and the instrument invokes them with +`agda --safe --without-K --cubical-compatible`. Under `--safe` the compiler +refuses `postulate` and the unsafe pragmas, so the absence above is enforced by +the toolchain rather than asserted here. `scripts/proof-scan-dangerous.sh` scans +the same files, comment-aware, on every run; the ledger's `import_cone` records +each imported module's postulate count (0 at the pin). + +## (b) Budgeted — tested with refutation budget + +- (none — nothing in this repository needs a refutation budget, because there is + nothing to refute: no `unsafe` extraction boundary, no FFI, no partially-total + definition in a proof source) + +## (c) Necessary axiom + +- (none) Nothing in this repository rests on an axiom. The one theorem is + `proven` with zero postulates, so there is no axiom to justify or cite. The + external developments it consumes are recorded in the ledger instead — see + `verification/proofs/LEDGER.json` `.source.assumptions` and `.caveats` + — because a dependency's own obligations are that dependency's to discharge, + not an axiom of this proof. + +## (d) DEBT — actively to be closed + +- (none) + +## Exemptions, and why they are not debt + +`.trusted-base-ignore` exempts the whole of `tests/proofs/control/`, which holds +the both-ways controls for the proof gate. The planted fixtures contain a real +`Admitted` (`PlantedAdmitted.v`), a real `sorry` (`PlantedSorry.lean`), a real +`Axiom` (`PlantedAxiom.v`), a real Coq `admit.` (`PlantedAdmit.v`), an `Axiom` +written inside `(* *)` in a Lean file where those characters are text +(`PlantedLeanBlockText.lean`) and a `sorry` behind Lean subtype notation +(`PlantedLeanSubtype.lean`) — **so that they are detected**: +`tests/proofs/run-ledger-controls.sh` fails if the instrument accepts any of +them, and controls 35, 41 and 43 exist because those three alternatives had +become unfirable. `ControlImportedAxiom.v` and `ControlImportedAxiom.lean` carry +no lexical escape hatches at all and exist so `tests/proofs/run-controls.sh` +(`K7`/`K8`, `K12`/`K13`) can prove `scripts/check-proofs.sh` catches standard-library +imported axioms (`Coq.Logic.Classical_Prop.classic`, `Classical.em`) via kernel +assumption queries (`coqchk -silent -o`, `Print Assumptions`, `#print axioms`). +The remaining fixtures (`Control.v`, `Control.lean`, +`ControlCommentAxiom.v`) are closed proofs or comment-only prose with no escape +hatch; they are exempted only because the exemption is by directory. Recording +any of these here as debt would both misreport the repository and invite someone +to "fix" the fixtures. + +## How this file is kept honest + +- The estate checker runs on every push via `governance-reusable.yml` + (`trusted-base` job) and fails on a naked core marker. +- `scripts/proof-scan-dangerous.sh` fails on any core-tier marker outside the + exempted path, and fails if this file is missing while one exists. +- Neither gate is "declared": both can fail on a planted violation, which is + what `tests/proofs/run-ledger-controls.sh` asserts. diff --git a/scripts/check-coordination-boundary.sh b/scripts/check-coordination-boundary.sh index 46e16f7..472c55c 100755 --- a/scripts/check-coordination-boundary.sh +++ b/scripts/check-coordination-boundary.sh @@ -45,7 +45,15 @@ 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 + # Literate Agda (.lagda.md, .lagda.tex, .lagda.rst, .lagda.org) is a + # proof source, never prose metadata — match it before *.md / *.adoc. + *.lagda | *.lagda.*) ;; + # 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 | */LEDGER.json) continue ;; esac if ! is_allowed_proof "$f"; then err "Proof outside the cross-project allowlist: $f @@ -60,7 +68,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 new file mode 100755 index 0000000..601bc35 --- /dev/null +++ b/scripts/check-proof-enrolment.sh @@ -0,0 +1,368 @@ +#!/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=() + +# 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" ;; + idris2) echo "Idris2" ;; + lean4) echo "Lean4" ;; + coq) echo "Coq" ;; + tlaplus) echo "TLA+" ;; + *) 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" ;; + 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 | *.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) +# 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() { + 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 ---------------------------------- +# 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" \ + | awk '!/\.(a2ml|adoc)$|(^|\/)\.gitkeep$|(^|\/)MANIFEST$|(^|\/)LEDGER\.json$/ && (!/\.md$/ || /\.lagda\.md$/)' \ + | 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")" + 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" + +# 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/check-proof-ledger.sh b/scripts/check-proof-ledger.sh new file mode 100755 index 0000000..1269cce --- /dev/null +++ b/scripts/check-proof-ledger.sh @@ -0,0 +1,1426 @@ +#!/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 +# metadatastician/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=() +WAIVERS=() +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. The delegated scanner strips comments according to +# the file's language and preserves line numbers. +# --------------------------------------------------------------------------- +scan_escape_hatches() { + # $1 = file. Prints numbered matching lines; scanner errors become a + # synthetic line 0 hit, so callers treat them as failures. + # + # ONE pattern list, not two. This function used to carry its own copy, which + # drifted: it knew `believe_me|assert_total|postulate|sorry|admit|Admitted| + # unsafeCoerce` and missed the rest of the estate policy's CORE tier (Coq + # `Axiom`, Lean `axiom`, Idris2 `really_believe_me`/`partial`, F* `assume val`, + # `unsafePerformIO`). The scanner owns the list; this delegates so a marker + # can never be caught by one gate and missed by the other. + local file="$1" + local out rc + out="$(bash "$ROOT/scripts/proof-scan-dangerous.sh" --scan-file "$file" 2>&1)"; rc=$? + if [ "$rc" -gt 1 ]; then + printf '0:scanner-error:proof-scan-dangerous.sh exited %s for %s\n' "$rc" "$file" + return 0 + fi + printf '%s\n' "$out" | sed -n 's/^\([0-9][0-9]*\):/\1:/p' +} + +# 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; } + +# The authority this audit is against. It is read out of the ledger rather than +# hard-coded: the policy lives in another repository, so a bare path here would +# be a citation to a file this tree does not contain. +POLICY_REPO="$(jq -r '.policy.proof_policy.repo // ""' "$LEDGER")" +POLICY_PATH="$(jq -r '.policy.proof_policy.path // ""' "$LEDGER")" +POLICY_COMMIT="$(jq -r '.policy.proof_policy.commit // ""' "$LEDGER")" +POLICY_RULING="$(jq -r '.policy.proof_policy.ruling // ""' "$LEDGER")" +POLICY_AMENDED="$(jq -r '.policy.proof_policy.amended // ""' "$LEDGER")" +POLICY_VENDORED="$(jq -r '.policy.proof_policy.vendored_here // false | tostring' "$LEDGER")" + +policy_label() { + if [ -n "$POLICY_REPO" ] && [ -n "$POLICY_PATH" ]; then + printf '%s %s' "$POLICY_REPO" "$POLICY_PATH" + else + printf '%s' "${POLICY_PATH:-}" + fi +} + +echo "=== Proof ledger gate ===" +echo "ledger: $LEDGER" +echo "policy: $(policy_label)${POLICY_COMMIT:+ @ ${POLICY_COMMIT:0:12}}${POLICY_RULING:+ (${POLICY_RULING})}${POLICY_AMENDED:+, amended ${POLICY_AMENDED}}" +if [ "$POLICY_VENDORED" = "true" ]; then + echo " vendored copy in this tree" +else + echo " referenced, not vendored: this repository carries no copy of the policy" +fi +echo "grades: mathesis/estate-mathematical-architecture §5-§6" +echo "" + +# --- 1b. the authority must be pinned, not merely named ---------------------- +if [ -z "$POLICY_REPO" ] || [ -z "$POLICY_PATH" ] || [ -z "$POLICY_RULING" ]; then + fail "policy: the ledger's .policy.proof_policy must name the repository, the path and the ruling it was decided by (got repo='${POLICY_REPO}', path='${POLICY_PATH}', ruling='${POLICY_RULING}')" +fi +if ! printf '%s' "$POLICY_COMMIT" | grep -qE '^[0-9a-f]{40}$'; then + fail "policy: .policy.proof_policy.commit must be the full 40-character commit the policy was read at (got '${POLICY_COMMIT}') — an unpinned policy is an unspecified obligation" +fi +if [ "$POLICY_VENDORED" = "true" ]; then + [ -f "$POLICY_PATH" ] \ + || fail "policy: vendored_here is true but there is no file at '$POLICY_PATH' in this tree" +else + if [ -f "$POLICY_PATH" ]; then + note "policy: '$POLICY_PATH' exists in this tree but is recorded as not vendored — reconcile the two" + fi +fi + +# 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"}' + +# Print the 1-based entry index if the manifest has a gated entry for the target +# path; return 1 if the manifest is missing or has no such entry. +manifest_gated_index() { + local mfile="$1" target="$2" + [[ -f "$mfile" ]] || return 1 + awk -F'|' -v want="$target" ' + /^[[:space:]]*(#|$)/ { next } + NF >= 3 { + idx++ + r = $1; sub(/^[[:space:]]+/, "", r); sub(/[[:space:]]+$/, "", r); sub(/\/+$/, "", r); sub(/^\.\//, "", r) + m = $2; sub(/^[[:space:]]+/, "", m); sub(/[[:space:]]+$/, "", m); sub(/^\.\//, "", m) + s = $3; sub(/^[[:space:]]+/, "", s); sub(/[[:space:]]+$/, "", s) + full = (r == "" || r == ".") ? m : (r "/" m) + if (full == want && s == "gated") { print idx; found = 1; exit } + } + END { exit (found ? 0 : 1) } + ' "$mfile" +} + +# Return success if the manifest has a gated entry for the target path; +# return 1 if the manifest is missing or a readable manifest has no such entry. +manifest_is_gated() { + manifest_gated_index "$1" "$2" >/dev/null +} + +is_valid_target_ident() { + local ident="$1" + [[ "$ident" =~ ^[A-Za-z_][A-Za-z0-9_\']*(\.[A-Za-z_][A-Za-z0-9_\']*)*$ ]] +} + +# --- 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[]? | select(.waiver == null) | (.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. Independent recheck +# counts exclude `.source.prover`, so duplicating the source prover as a leg +# cannot inflate Grade 3 to Grade 2i. +ROWS_TSV="$(mktemp)" || { echo "BLOCKED: cannot create a temporary file" >&2; exit 2; } +trap 'rm -f "$ROWS_TSV"' EXIT +jq -r ' + .theorems[] as $t | + ($t.source.prover // "") as $src | + [ $t.id, + $t.kind, + ($t.grade | tostring), + ([$t.legs[]?.prover] | join(",")), + ([$t.legs[]? | select(.waiver == null) | select(.status != "open")] | length), + ([$t.legs[]? | select(.waiver == null) + | select((.prover // "") != $src) + | select(.status == "proven" or .status == "proven-with-postulates")] | length) + ] | map(tostring) | join("\u001f")' "$LEDGER" > "$ROWS_TSV" + +declare -A THEOREM_PROVEN=() +while IFS=$'\x1f' 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) + # mathesis §5: Grade 2i applies when >=1 independent recheck leg is proven + # within the DTT family (including when both PROOF-POLICY §2 DTT legs — + # rocq + lean4 — are proven, before a non-DTT leg promotes the theorem to 2ii). + if [[ "$proven" -lt 1 ]]; then + fail "$tid: grade 2i requires at least one independent 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) as $t + | [ $t.legs[]? + | select(.waiver == null) + | select((.prover // "") != ($t.source.prover // "")) + | 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) + valid_api="$(jq -r --arg id "$tid" ' + [ .theorems[] | select(.id == $id) | .legs[]? + | select(.waiver == null) + | select(.status == "proven" or .status == "proven-with-postulates") + | .api_receipt? | select(type == "object") + | select((.api // "") == "axle" or (.api // "") == "coq-lsp" or (.api // "") == "isabelle-server") + | select((.commit // "") | test("^[0-9a-f]{40}$")) + | select(((.run // "") | gsub("\\s+"; "")) != "") + ] | length' "$LEDGER")" + if [[ "${valid_api:-0}" -lt 1 ]]; then + fail "$tid: grade 1 requires a verified-checker API receipt (axle, coq-lsp, or isabelle-server with 40-char commit and run — 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 < "$ROWS_TSV" + +# --- 3a. cross-prover reconciliation status (mathesis CROSS-PROVER-RECONCILIATION) +# Never collapse distinct dimensions of verification: source Agda status, target +# Rocq/Lean kernel status, and bridge correspondence justification remain distinct. +while IFS=$'\x1f' read -r tid ragda rrocq rlean rbridge sstatus rocq_st lean_st uncomp_cnt; do + [[ -z "$tid" ]] && continue + case "$ragda" in + ""|NOT-INVENTORIED|INVENTORIED|AGDA-PENDING|AGDA-VERIFIED|COUNTEREXAMPLE|QUARANTINED) ;; + *) fail "$tid: reconciliation.agda '${ragda}' is outside mathesis CROSS-PROVER-RECONCILIATION vocabulary" ;; + esac + case "$rrocq" in + ""|NOT-INVENTORIED|INVENTORIED|COQ-CHECKED|COUNTEREXAMPLE|QUARANTINED) ;; + *) fail "$tid: reconciliation.rocq '${rrocq}' is outside mathesis CROSS-PROVER-RECONCILIATION vocabulary" ;; + esac + case "$rlean" in + ""|NOT-INVENTORIED|INVENTORIED|LEAN-CHECKED|COUNTEREXAMPLE|QUARANTINED) ;; + *) fail "$tid: reconciliation.lean4 '${rlean}' is outside mathesis CROSS-PROVER-RECONCILIATION vocabulary" ;; + esac + case "$rbridge" in + ""|BRIDGE-PENDING|RECONCILED|COUNTEREXAMPLE|QUARANTINED) ;; + *) fail "$tid: reconciliation.bridge '${rbridge}' is outside mathesis CROSS-PROVER-RECONCILIATION vocabulary" ;; + esac + if [[ "$ragda" == "AGDA-VERIFIED" && "$sstatus" != "proven" && "$sstatus" != "proven-with-postulates" ]]; then + fail "$tid: reconciliation.agda claims 'AGDA-VERIFIED' while source.status is '$sstatus'" + fi + if [[ "$rrocq" == "COQ-CHECKED" && "$rocq_st" != "proven" && "$rocq_st" != "proven-with-postulates" ]]; then + fail "$tid: reconciliation.rocq claims 'COQ-CHECKED' while the rocq leg is '${rocq_st:-missing}'" + fi + if [[ "$rlean" == "LEAN-CHECKED" && "$lean_st" != "proven" && "$lean_st" != "proven-with-postulates" ]]; then + fail "$tid: reconciliation.lean4 claims 'LEAN-CHECKED' while the lean4 leg is '${lean_st:-missing}'" + fi + if [[ "$rbridge" == "RECONCILED" ]]; then + if [[ "$rocq_st" != "proven" && "$rocq_st" != "proven-with-postulates" ]] \ + || [[ "$lean_st" != "proven" && "$lean_st" != "proven-with-postulates" ]] \ + || [[ "${uncomp_cnt:-0}" -gt 0 ]]; then + fail "$tid: reconciliation.bridge claims 'RECONCILED', which requires independently verified Rocq and Lean targets plus justified statement comparisons (mathesis CROSS-PROVER-RECONCILIATION)" + fi + fi +done < <(jq -r ' + .theorems[] | select(.reconciliation != null) | + . as $t | + ([ $t.legs[]? | select(.prover == "rocq") | .status // "open" ][0] // "missing") as $rocq_st | + ([ $t.legs[]? | select(.prover == "lean4") | .status // "open" ][0] // "missing") as $lean_st | + ([ $t.legs[]? | select(.prover == "rocq" or .prover == "lean4") + | select((.statement_compared // "") == "" or (.statement_compared | tostring) == "false") ] | length) as $uncomp | + [ $t.id, + ($t.reconciliation.agda // ""), + ($t.reconciliation.rocq // ""), + ($t.reconciliation.lean4 // ""), + ($t.reconciliation.bridge // ""), + ($t.source.status // ""), + $rocq_st, + $lean_st, + ($uncomp | tostring) + ] | join("\u001f")' "$LEDGER") + +# --- 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=$'\x1f' 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) .source.files must be a non-empty array of strings, every file must exist, + # and for a proven source leg its files must be gated in the prover's MANIFEST. + src_files_valid="$(jq -r --arg id "$tid" ' + .theorems[] | select(.id == $id) | .source.files + | (type == "array" and length > 0 and all(.[]; type == "string" and length > 0)) | tostring' "$LEDGER")" + if [[ "$src_files_valid" != "true" ]]; then + fail "$tid: .source.files must be a non-empty JSON array of file paths" + continue + fi + src_mdir="" + case "$sprover" in + agda) src_mdir="$PROOFS_DIR/agda" ;; + rocq|coq) src_mdir="$PROOFS_DIR/coq" ;; + lean4|lean) src_mdir="$PROOFS_DIR/lean4" ;; + idris2) src_mdir="$PROOFS_DIR/idris2" ;; + esac + IFS=',' read -r -a src_files <<< "$files_csv" + for f in "${src_files[@]}"; do + [[ -z "$f" ]] && continue + if [[ ! -f "$f" ]]; then + fail "$tid: source file recorded but missing on disk: $f" + elif [[ ( "$sstatus" == "proven" || "$sstatus" == "proven-with-postulates" ) && -n "$src_mdir" ]]; then + if ! manifest_is_gated "$src_mdir/MANIFEST" "$f"; then + fail "$tid: proven source file '$f' is not listed as 'gated' in $src_mdir/MANIFEST" + fi + fi + 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, and check-proofs.sh queries Print Assumptions / #print + # axioms against .statement_formal.declarations. Require a non-empty array + # covering every .statement_anchor, and verify each recorded declaration's + # TYPE is still present in the source file, whitespace-normalised. + formal_decl_count="$(jq -r --arg id "$tid" ' + .theorems[] | select(.id == $id) + | if (.statement_formal.declarations | type) == "array" then (.statement_formal.declarations | length) else -1 end' "$LEDGER")" + if [[ "${formal_decl_count:-0}" -le 0 ]]; then + fail "$tid: .statement_formal.declarations must be a non-empty array — recheck statement comparison (PROOF-POLICY §2) and kernel assumption queries (#131) cannot run without recorded formal declarations" + elif [[ -n "${anchor_ids// }" ]]; then + missing_formal_anchors="$(jq -r --arg id "$tid" ' + .theorems[] | select(.id == $id) as $t + | ([$t.statement_anchor[]? // empty]) - ([$t.statement_formal.declarations[]?.name // empty]) + | join(", ")' "$LEDGER")" + if [[ -n "$missing_formal_anchors" ]]; then + fail "$tid: .statement_formal.declarations is missing formal signature(s) for statement_anchor entry/entries: $missing_formal_anchors" + fi + fi + while IFS=$'\x1f' 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 + *" ${decl_name} : ${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 declares under '$decl_name : ...' 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 // "") ] | map(tostring) | join("\u001f")' "$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 // "") + ] | map(tostring) | join("\u001f")' "$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=$'\x1f' 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 // "") ] | map(tostring) | join("\u001f")' "$LEDGER") + +# the last entry for each target must be the current value +while IFS=$'\x1f' 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" | head -1)" + # A transition may concern the SOURCE leg rather than a recheck leg (e.g. a + # re-baselining under a new canonical invocation). Fall back to .source. + if [ -z "$current" ]; then + current="$(jq -r --arg id "$tid" --arg p "$target" '.theorems[] | select(.id == $id) | select(.source.prover == $p) | .source.status' "$LEDGER" | head -1)" + fi + 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 // "") ] | map(tostring) | join("\u001f")' "$LEDGER") + +# --- 3d. the trust base beyond this repo ------------------------------------- +# PROOF-POLICY §1.1 (a caller is proved only *relative to* an ASSUMED contract), +# §3 (any axioms the Agda proof rests on belong in that leg's trust boundary) and +# §2.2 (per-theorem assumptions, recorded) all say the same thing: what a proof +# leans on has to be named, and named accurately. A dependency that is itself a +# proof-bearing system with open obligations is not a version string. +while IFS=$'\x1f' read -r tid aname akind arelation aev aaxioms aclaim aversion acommit; do + [ -z "${aname// }" ] && continue + [ -n "${akind// }" ] || fail "$tid: assumption '$aname' has no kind — an untagged assumption is an unnamed one" + case "$akind" in + dependency-pin|external-development) ;; + *) fail "$tid: assumption '$aname' has kind '${akind}', which is not one of dependency-pin | external-development" ;; + esac + if [ "$akind" = "dependency-pin" ]; then + # A dependency-pin that names no version and no commit pins nothing; it is a + # dependency *mention*. Without this, deleting `version` from the Agda row + # left a recorded assumption that constrained nothing and the audit passed. + if [ -z "${aversion// }" ] && [ -z "${acommit// }" ]; then + fail "$tid: dependency-pin '$aname' records neither a version nor a commit — a dependency that pins nothing is not a pin (§2.2)" + fi + fi + if [ "$akind" = "external-development" ]; then + [ -n "${arelation// }" ] || fail "$tid: external development '$aname' records no relation — say what it is to this proof (construction-under-comparison, proof-bearing-consumer, ...)" + [ -n "${aev// }" ] || fail "$tid: external development '$aname' records no evidence — a claim about another repository needs the file and date it was read from" + fi + # A known open obligation must be said out loud in the theorem's caveats, by + # name. This is the §1.1 rule applied to a whole dependency rather than to one + # contract: the caller is never unconditionally proven while the thing it rests + # on has open obligations. + trigger="" + [ -n "${aaxioms// }" ] && [ "$aaxioms" != "0" ] && trigger="undischarged axioms ($aaxioms)" + [ "$aclaim" = "open" ] && trigger="${trigger:+$trigger; }open identity claim" + if [ -n "$trigger" ]; then + if ! jq -r --arg id "$tid" '.theorems[] | select(.id == $id) | (.caveats // [])[]' "$LEDGER" \ + | grep -Fiq -- "$aname"; then + fail "$tid: '$aname' carries $trigger, but no entry in .caveats names it — the theorem would be read as if that obligation did not exist (§1.1, §3)" + fi + fi +done < <(jq -r ' + .theorems[] | .id as $id | (.source.assumptions // [])[] | + [ $id, (.name // ""), (.kind // ""), (.relation // ""), (.evidence // ""), + ((.undischarged_axioms // "") | tostring), (.identity_claim // ""), + (.version // ""), (.commit // "") ] | map(tostring) | join("\u001f")' "$LEDGER") + +# import cone: Agda's --safe refuses an import that is not itself safe, so the +# cone is the trust base. If the record admits a postulated module inside it, +# Validate .source.axioms independently of import_cone, and require an explicit +# .source.import_cone.modules audit whenever an Agda source imports external +# non-stdlib modules (for example Echo / EchoCharacteristic / EchoLinear). +while IFS=$'\x1f' read -r tid sprover sstatus sfiles_csv saxioms_state; do + [[ -z "$tid" ]] && continue + if [[ "$saxioms_state" == "bad" ]]; then + fail "$tid: .source.axioms must be null or a JSON array of non-empty strings (never 'sorryAx')" + elif [[ "$sstatus" == "proven" && "$saxioms_state" != "0" ]]; then + fail "$tid: source.status is 'proven' but .source.axioms lists $saxioms_state axiom(s) — record 'proven-with-postulates' (§5)" + elif [[ "$sstatus" == "proven-with-postulates" && "$saxioms_state" == "0" ]]; then + fail "$tid: source.status is 'proven-with-postulates' with an empty .source.axioms list (§5: list the axioms)" + fi + + if [[ "$sprover" == "agda" && -n "$sfiles_csv" ]]; then + IFS=',' read -r -a agda_src_files <<<"$sfiles_csv" + local_mods=" " + for af in "${agda_src_files[@]}"; do + [[ -f "$af" ]] || continue + base_mod="$(basename "$af")" + base_mod="${base_mod%.lagda.*}" + base_mod="${base_mod%.lagda}" + base_mod="${base_mod%.agda}" + local_mods="${local_mods}${base_mod} " + done + ext_imports="" + for af in "${agda_src_files[@]}"; do + [[ -f "$af" ]] || continue + while IFS= read -r imod; do + [[ -z "$imod" ]] && continue + case "$imod" in + Agda.*|Data.*|Relation.*|Function|Function.*|Level|Level.*| Algebra.*|Category.*|Codata.*|Effect.*|Foreign.*|IO|IO.*|Induction.*|Reflection|Reflection.*|Strict|Text.*) + continue ;; + esac + case "$local_mods" in + *" $imod "*) continue ;; + esac + ext_imports="${ext_imports}${imod}"$'\n' + done < <(sed -nE 's/^[[:space:]]*(open[[:space:]]+)?import[[:space:]]+([A-Za-z0-9_.]+).*/\2/p' "$af") + done + if [[ -n "${ext_imports//[[:space:]]/}" ]]; then + cone_mods="$(jq -r --arg id "$tid" '[.theorems[] | select(.id == $id) | (.source.import_cone.modules // [])[]?.module // empty] | join("\n")' "$LEDGER")" + if [[ -z "${cone_mods//[[:space:]]/}" ]]; then + fail "$tid: Agda source imports external module(s) ($(printf '%s' "$ext_imports" | sort -u | tr '\n' ' ' | sed 's/ *$//')) but .source.import_cone.modules is missing or empty — audit external imports for postulates (§3)" + else + while IFS= read -r imod; do + [[ -z "$imod" ]] && continue + if ! printf '%s\n' "$cone_mods" | grep -Fxq -- "$imod"; then + fail "$tid: Agda source imports external module '$imod', which is missing from .source.import_cone.modules (§3)" + fi + done < <(printf '%s' "$ext_imports" | sort -u) + fi + fi + fi +done < <(jq -r ' + .theorems[] | [ + .id, + (.source.prover // ""), + (.source.status // ""), + ((.source.files // []) | join(",")), + (if (.source.axioms // null) == null then "0" + elif (.source.axioms | type) != "array" or (all(.source.axioms[]; type == "string" and length > 0) | not) or ((.source.axioms | index("sorryAx")) != null) then "bad" + else (.source.axioms | length | tostring) end) + ] | join("\u001f")' "$LEDGER") + +# the source leg cannot be plain `proven` (§3: list the axioms). +while IFS=$'\x1f' read -r tid mod count; do + [ -z "${mod// }" ] && continue + printf '%s' "$count" | grep -qE '^[0-9]+$' \ + || { fail "$tid: import cone entry '$mod' has a non-numeric postulate count '${count}'"; continue; } + if [ "$count" -gt 0 ]; then + sstatus="$(jq -r --arg id "$tid" '.theorems[] | select(.id == $id) | .source.status' "$LEDGER")" + naxioms="$(jq -r --arg id "$tid" '[.theorems[] | select(.id == $id) | (.source.axioms // [])[]] | length' "$LEDGER")" + if [ "$sstatus" != "proven-with-postulates" ]; then + fail "$tid: import cone module '$mod' has $count postulate(s), so the source leg cannot be '$sstatus' — record it as 'proven-with-postulates' and list them (§3, §5)" + elif [ "$naxioms" -lt 1 ]; then + fail "$tid: import cone module '$mod' has $count postulate(s) but .source.axioms lists none (§5: list the axioms)" + fi + fi +done < <(jq -r ' + .theorems[] | .id as $id | (.source.import_cone.modules // [])[] | + [ $id, (.module // ""), ((.postulates // "") | tostring) ] | map(tostring) | join("\u001f")' "$LEDGER") + +# An open leg with no caveat is a claim by omission: a reader who skims the +# grade must still meet the fact that the theorem is not fully rechecked. +while IFS=$'\x1f' read -r tid open_count caveat_count; do + [ -z "$tid" ] && continue + if [ "${open_count:-0}" -gt 0 ] && [ "${caveat_count:-0}" -lt 1 ]; then + fail "$tid: $open_count leg(s) are open and .caveats is empty — say in the record that the theorem is not fully rechecked" + fi +done < <(jq -r ' + .theorems[] | [ .id, + ([.legs[]? | select(.status == "open")] | length), + ((.caveats // []) | length) ] | map(tostring) | join("\u001f")' "$LEDGER") + +# --- 3d2. related but not relied upon --------------------------------------- +# A sibling formalisation of the same object is the most likely thing a reader +# will mistake for evidence. It is not an assumption (nothing rests on it) and it +# is not evidence for this theorem (it proves something else), so it gets its own +# array and must say so explicitly. +while IFS=$'\x1f' read -r tid name relation consumed ev; do + [ -z "$tid" ] && continue + [ -n "${name// }" ] || fail "$tid: related development with no name" + [ -n "${relation// }" ] || fail "$tid: related development '$name' records no relation — say how it relates, since it is not being consumed" + [ -n "${ev// }" ] || fail "$tid: related development '$name' records no evidence (file and date read)" + if [ "$consumed" = "true" ]; then + fail "$tid: related development '$name' claims to be consumed — then it belongs in .source.assumptions, and here it would double-count" + fi +done < <(jq -r ' + .theorems[] | .id as $id | (.source.related_developments // [])[] | + [ $id, (.name // ""), (.relation // ""), + ((.consumed_by_this_proof // false) | tostring), (.evidence // "") ] + | map(tostring) | join("\u001f")' "$LEDGER") + +# --- 3e. waivers: PROOF-POLICY §4 ------------------------------------------- +# A waiver is for a statement the mapped prover cannot express. It is not a +# softer status token: a waived leg carries NO status at all (so nothing can +# count it), it names the obligation, the tool and the reason, and it points at +# the exception record. Nothing here lets a waiver create a grade. +while IFS=$'\x1f' read -r tid prover wstatus wobligation wtool wreason wrecord; do + [ -z "$tid" ] && continue + if [ -n "${wstatus// }" ] && [ "$wstatus" != "null" ]; then + fail "$tid/$prover: a waived leg also carries status '$wstatus' — a waiver is not a status token (§4)" + fi + for pair in "obligation:${wobligation}" "tool:${wtool}" "reason:${wreason}" "record:${wrecord}"; do + if [ -z "${pair#*:}" ] || [ "${pair#*:}" = "null" ]; then + fail "$tid/$prover: waiver without '${pair%%:*}' — §4 requires the obligation, the tool, the reason and the exception record" + fi + done + # The record must RESOLVE, not merely be non-empty. Accepting any string let a + # required leg carry `record: does-not-exist` and still pass: the presence + # check was satisfied, and the waiver then removed that leg from the status + # and artifact rules below. A record is `[#]` in this + # repository; when an anchor is given it must occur in the file, and the file + # must name the tool, so the citation actually binds to this waiver. An + # external ruling belongs in a file here that cites it. + wrec_path="${wrecord%%#*}" + wrec_anchor="" + case "$wrecord" in *'#'*) wrec_anchor="${wrecord#*#}" ;; esac + if [ ! -f "$wrec_path" ]; then + fail "$tid/$prover: waiver record '$wrecord' does not resolve — no file '$wrec_path' in the repository (§4)" + else + if [ -n "$wrec_anchor" ] && ! grep -qiF -- "$wrec_anchor" "$wrec_path"; then + fail "$tid/$prover: waiver record '$wrecord' names anchor '$wrec_anchor', which does not occur in $wrec_path (§4)" + fi + if ! grep -qiF -- "$wtool" "$wrec_path"; then + fail "$tid/$prover: waiver record '$wrecord' never mentions the tool '$wtool' — the record does not bind to this waiver (§4)" + fi + fi + WAIVERS+=("$tid: $prover leg WAIVED — ${wreason} (tool: ${wtool}; record: ${wrecord})") +done < <(jq -r ' + .theorems[] as $t | $t.legs[]? | select(.waiver != null) | + [ $t.id, .prover, (.status // ""), (.waiver.obligation // ""), (.waiver.tool // ""), + (.waiver.reason // ""), (.waiver.record // "") ] | map(tostring) | join("\u001f")' "$LEDGER") + +# --- 4. every non-open claim must be backed by artifact + MANIFEST + route --- +# Nine emitted fields, nine names — in order: id, prover, status, artifact, +# route, statement_compared, axioms, reproof_reason, blocker. A dropped name +# here silently shifts every later field left (blocker would receive the +# reproof_reason), which is how a rule ends up never firing. +while IFS=$'\x1f' read -r tid prover status artifact route compared axioms reproof_reason blocker; do + [ -z "$tid" ] && continue + # Waived legs are audited in 3e and carry no claim here. + [ -z "${status// }" ] && continue + + # PROOF-POLICY §2.2: a leg declares `transported`, `re-proved` or + # `unavailable`. The route is a property of the leg, not of the claim, so it + # is checked before the open/claimed split. + case "${route:-}" in + ""|null) + if [ "$status" != "open" ]; then + fail "$tid/$prover: status '$status' recorded with no route — say whether it was transported or re-proved (§2.2)" + fi + ;; + transported|re-proved) ;; + unavailable) + # 'unavailable' is a statement about the route, not a proof: it cannot + # carry a claim, and it must say what is missing. + if [ "$status" != "open" ]; then + fail "$tid/$prover: route 'unavailable' with status '$status' — a route that does not exist cannot support a claim (§2.2)" + fi + if [ -z "${blocker// }" ] || [ "$blocker" = "null" ]; then + fail "$tid/$prover: route 'unavailable' with no blocker recorded — say what the missing route is (§2.2)" + fi + ;; + *) fail "$tid/$prover: route '${route}' is not one of transported, re-proved, unavailable (PROOF-POLICY §2.2)" ;; + esac + + [ "$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 + # A prover the lane has no recipe for cannot support a claim. Without this the + # default branch left $mdir empty, skipped every manifest check, and a 'proven' + # Isabelle/SMT/TLA+ row pointing at any file on disk would count towards a + # grade with nothing having run. The wired set is the set check-proofs.sh + # implements; write it out here so the two cannot drift silently. + if [ -z "$mdir" ]; then + fail "$tid/$prover: status '$status' recorded for a prover the lane cannot compile — scripts/check-proofs.sh wires idris2, lean4, agda and coq only, so this leg would contribute to a grade without any proof system running. Record the leg as open, or add a compile recipe for '$prover' first (PROOF-POLICY §2.3)." + continue + fi + 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 ! manifest_is_gated "$mdir/MANIFEST" "$artifact"; then + fail "$tid/$prover: $artifact is not listed as 'gated' in $mdir/MANIFEST (unlisted or quarantined witness)" + fi + fi + + # Optional support_files (helper modules imported by .artifact): every entry + # must exist on disk, be gated in the same MANIFEST, and obey the Mathlib ban. + sup_type="$(jq -r --arg id "$tid" --arg p "$prover" ' + [ .theorems[] | select(.id == $id) | .legs[]? | select(.prover == $p) + | if (.support_files // null) == null then "none" + elif (.support_files | type) == "array" and all(.support_files[]; type == "string" and length > 0) then "ok" + else "bad" end ][0] // "none"' "$LEDGER")" + if [[ "$sup_type" == "bad" ]]; then + fail "$tid/$prover: .support_files must be an array of non-empty file path strings" + elif [[ "$sup_type" == "ok" ]]; then + art_idx="$(manifest_gated_index "$mdir/MANIFEST" "$artifact" || echo 0)" + while IFS= read -r sf; do + [[ -z "$sf" ]] && continue + if [[ ! -f "$sf" ]]; then + fail "$tid/$prover: support file listed but missing on disk: $sf" + elif ! sf_idx="$(manifest_gated_index "$mdir/MANIFEST" "$sf")"; then + fail "$tid/$prover: support file '$sf' is not listed as 'gated' in $mdir/MANIFEST" + elif [[ "$art_idx" -gt 0 && "$sf_idx" -ge "$art_idx" ]]; then + fail "$tid/$prover: support file '$sf' must appear BEFORE '$artifact' in $mdir/MANIFEST so its compiled artifact exists when the witness compiles" + elif [[ "$prover" == "lean4" ]] && grep -qE '^[[:space:]]*import[[:space:]]+Mathlib' "$sf"; then + fail "$tid/$prover: support file '$sf' imports Mathlib, which PROOF-POLICY §2 forbids" + fi + done < <(jq -r --arg id "$tid" --arg p "$prover" ' + .theorems[] | select(.id == $id) | .legs[]? | select(.prover == $p) | (.support_files // [])[]' "$LEDGER") + fi + + # PROOF-POLICY §2.3: record the route; §2.1/§2.2: without an affirmative + # statement comparison the leg is ASSUMED (argued), not PROVEN. + if [[ "$route" == "re-proved" ]] && { [[ -z "$reproof_reason" ]] || [[ "$reproof_reason" == "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|false|no) + fail "$tid/$prover: '$status' requires an affirmative statement comparison (PROOF-POLICY §2.1/§2.2); without it the leg is 'argued'" ;; + esac + fi + + # §5: axioms must be a JSON array of strings, never contain sorryAx, and only + # proven-with-postulates may carry a non-empty axiom list. + axiom_check="$(jq -r --arg id "$tid" --arg p "$prover" ' + [ .theorems[] | select(.id == $id) | .legs[]? | select(.prover == $p) + | if (.axioms | type) != "array" or (all(.axioms[]; type == "string" and length > 0) | not) then "not-string-array" + elif (.axioms | index("sorryAx")) != null then "has-sorryAx" + else (.axioms | length | tostring) end ][0] // "not-string-array"' "$LEDGER")" + if [[ "$axiom_check" == "not-string-array" ]]; then + fail "$tid/$prover: 'axioms' must be recorded as a JSON array of strings (empty [] when none) — mathesis §6 axiom tracking" + elif [[ "$axiom_check" == "has-sorryAx" ]]; then + fail "$tid/$prover: 'sorryAx' is an incomplete-proof marker, never a permissible axiom in .axioms" + elif [[ "$status" == "proven" && "$axiom_check" -ne 0 ]]; then + fail "$tid/$prover: status 'proven' but $axiom_check axiom(s) recorded; that is 'proven-with-postulates' (§5)" + elif [[ "$status" == "proven-with-postulates" && "$axiom_check" -eq 0 ]]; then + fail "$tid/$prover: status 'proven-with-postulates' with an empty axiom list (§5: list the axioms)" + fi + + # Target declarations + kernel-assumption receipt check for Rocq/Lean witnesses + # (nextgen-typing#131): check-proofs.sh queries Print Assumptions / #print axioms + # on every target declaration, so each formal anchor must resolve to a distinct, + # valid target-prover identifier, and promoted legs must record evidence. + if [[ ( "$status" == "proven" || "$status" == "proven-with-postulates" ) && ( "$prover" == "rocq" || "$prover" == "lean4" ) ]]; then + decl_audit="$(jq -r --arg id "$tid" --arg p "$prover" ' + .theorems[] | select(.id == $id) as $t + | ([ $t.statement_formal.declarations[]?.name // empty ]) as $anchors + | ($t.legs[] | select(.prover == $p)) as $leg + | if ($leg.declarations // null) != null then + if ($leg.declarations | type) != "array" or ($leg.declarations | length) == 0 then + "ERR:legs[].declarations must be a non-empty array" + else + ([ $leg.declarations[] | if type == "object" then (.name // "") else tostring end ]) as $names + | ([ $leg.declarations[] | select(type == "object") | (.anchor // "") ]) as $mapped_anchors + | if ($names | unique | length) != ($names | length) then + "ERR:legs[].declarations maps multiple anchors to the same target declaration" + elif ($anchors | length) > 0 and (($mapped_anchors | length) > 0) and (($anchors - $mapped_anchors) | length) > 0 then + "ERR:legs[].declarations is missing anchor mapping(s): " + (($anchors - $mapped_anchors) | join(", ")) + elif ($anchors | length) > 0 and ($names | length) < ($anchors | length) then + "ERR:legs[].declarations lists fewer declarations than statement_formal.declarations" + else + "OK:" + ($names | join(",")) + end + end + elif ($anchors | length) > 0 then + "OK:" + ($anchors | join(",")) + else + "ERR:no declarations recorded in statement_formal.declarations or legs[].declarations" + end' "$LEDGER")" + if [[ "$decl_audit" == ERR:* ]]; then + fail "$tid/$prover: ${decl_audit#ERR:}" + else + IFS=',' read -r -a leg_decls <<<"${decl_audit#OK:}" + for dname in "${leg_decls[@]}"; do + if ! is_valid_target_ident "$dname"; then + fail "$tid/$prover: declaration '$dname' is not a valid $prover identifier — map hyphenated Agda anchors to $prover identifiers in legs[].declarations" + fi + done + fi + + IFS=$'\x1f' read -r le_commit le_run le_assumptions < <(jq -r --arg id "$tid" --arg p "$prover" ' + .theorems[] | select(.id == $id) | .legs[] | select(.prover == $p) | (.evidence // {}) | + [ (.commit // ""), (.run // ""), (.assumptions_output // "") ] | map(tostring) | join("\u001f")' "$LEDGER") + if ! [[ "${le_commit:-}" =~ ^[0-9a-f]{40}$ ]] || [[ -z "${le_run//[[:space:]]/}" ]] || [[ -z "${le_assumptions//[[:space:]]/}" ]]; then + fail "$tid/$prover: '$status' recheck leg must record .evidence with a 40-character .commit, .run, and verbatim .assumptions_output from Print Assumptions / #print axioms (mathesis §6, issue #131)" + fi + 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[]? | select(.waiver == null) | + [ $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 // ""), (.blocker // "") ] | map(tostring) | join("\u001f")' "$LEDGER") + +# --- 5. source legs: files, receipts, safety flags --------------------------- +while IFS=$'\x1f' 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 + IFS=$'\x1f' read -r ekind ecommit edate erun < <(jq -r --arg id "$tid" ' + .theorems[] | select(.id == $id) | .source.evidence? | + [ (.kind // ""), (.commit // ""), (.date // ""), (.run // "") ] | map(tostring) | join("\u001f")' "$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(",")) ] | map(tostring) | join("\u001f")' "$LEDGER") + +# --- 5a. corroboration is not a receipt ------------------------------------- +# A local run under a different compiler version is useful — it says the proof is +# not an artifact of one toolchain — but §2.1 pins the version *with* the result, +# and a receipt is what the grade rests on. So a corroborating run must declare +# itself as such, and must say which toolchain produced it. +while IFS=$'\x1f' read -r tid toolchain invocation result corrob; do + [ -z "$tid" ] && continue + [ -n "${toolchain// }" ] || fail "$tid: local evidence with no toolchain — a check that does not name its compiler cannot be reproduced (§2.1)" + [ -n "${invocation// }" ] || fail "$tid: local evidence with no recorded invocation (§2.2)" + [ -n "${result// }" ] || fail "$tid: local evidence with no observed result (§2.2)" + [ "$corrob" = "true" ] || fail "$tid: local evidence must set corroboration_only: true — it cannot stand in for the pinned receipt" +done < <(jq -r ' + .theorems[] | .id as $id | (.local_evidence // [])[] | + [ $id, (.toolchain // ""), (.invocation // ""), (.observed_result // ""), + ((.corroboration_only // false) | tostring) ] | map(tostring) | join("\u001f")' "$LEDGER") + +# --- 5b. receipt lineage: an archived receipt says why (mathesis §6) -------- +# mathesis §6 introduces `Superseded` and `Regressed` as first-class states for a +# receipt. A receipt kept but not marked is indistinguishable from one that is +# still evidence, which is the drift the clause exists to stop. +while IFS=$'\x1f' read -r tid idx state why; do + [ -z "$tid" ] && continue + case "$state" in + superseded|regressed) ;; + "") + fail "$tid: historical evidence entry $idx has no state — mathesis §6 requires 'superseded' or 'regressed', not a silently archived receipt" ;; + *) + fail "$tid: historical evidence entry $idx has state '${state}', which is not one of superseded | regressed (mathesis §6)" ;; + esac + [ -n "${why// }" ] || fail "$tid: historical evidence entry $idx does not say why it is no longer the current receipt" +done < <(jq -r ' + .theorems[] | .id as $id | (.source.evidence.historical_evidence // []) | to_entries[] | + [ $id, (.key | tostring), (.value.state // ""), + (.value.why_not_current // .value.reason // "") ] | map(tostring) | join("\u001f")' "$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 ------- +# Axioms are scoped to the specific leg(s) claiming each file (never pooled +# globally across unrelated legs), so an axiom permitted on one leg cannot +# license an undeclared axiom in another witness. +# Return success if an unwaived proven-with-postulates leg claiming the file +# lists the axiom, either by its name or with a qualified prefix. A jq failure +# also returns a non-zero status. +file_allows_axiom() { + local file="$1" ax_name="$2" + jq -e --arg f "$file" --arg ax "$ax_name" ' + [ .theorems[].legs[]? + | select(.waiver == null and (.status // "open") == "proven-with-postulates") + | select((.artifact // "") == $f or (((.support_files // []) | type) == "array" and ((.support_files // []) | index($f)) != null)) + | (.axioms // [])[] + | select(. == $ax or endswith("." + $ax)) + ] | length > 0 + ' "$LEDGER" >/dev/null 2>&1 +} + +# Add escape-hatch and unrecorded axiom findings for the file to $FAILS. +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 ! file_allows_axiom "$f" "$name"; then + fail "undeclared axiom in $f:$line — PROOF-POLICY §5 requires every axiom to be named on the owning leg 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|lagda\.[A-Za-z0-9]+|idr|v|lean|tla)$' | sort)" +else + PROOF_FILES="$(find "$PROOFS_DIR" -type f \( -name '*.agda' -o -name '*.lagda' -o -name '*.lagda.*' -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. Covers Agda sources as well as Rocq and Lean witnesses. +list_witnesses() { # $1 = prover dir under $PROOFS_DIR, $2 = extension + if git rev-parse --is-inside-work-tree >/dev/null 2>&1; then + if [[ "$2" == "agda" ]]; then + git ls-files -- "$PROOFS_DIR/$1" 2>/dev/null | grep -E '\.(agda|lagda|lagda\.[A-Za-z0-9]+)$' | sort + else + git ls-files -- "$PROOFS_DIR/$1" 2>/dev/null | grep -E "\.$2\$" | sort + fi + else + if [[ "$2" == "agda" ]]; then + find "$PROOFS_DIR/$1" -type f \( -name '*.agda' -o -name '*.lagda' -o -name '*.lagda.*' \) 2>/dev/null | sort + else + find "$PROOFS_DIR/$1" -type f -name "*.$2" 2>/dev/null | sort + fi + fi +} +LEDGER_ARTIFACTS="$(jq -r ' + [ .theorems[] + | (if (.source.files | type) == "array" then .source.files[] else empty end), + (.legs[]? | (.artifact // empty), (if (.support_files | type) == "array" then .support_files[] else empty end)) + ][] | select(type == "string" and length > 0)' "$LEDGER" | sort -u)" +for dir in agda coq lean4; do + ext=v + [[ "$dir" == "lean4" ]] && ext=lean + [[ "$dir" == "agda" ]] && ext=agda + 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 source/leg entry claiming '$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 ----- +# Print non-empty registry entries from stdin in sorted order, after removing +# comments, quotes, spaces, tabs, carriage returns and trailing commas. An +# empty result or a pipeline failure returns a non-zero status. +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) + + # Per theorem, not repository-wide. The old rule only ran when NO theorem had + # a proven leg, so one proven recheck leg anywhere switched off the comparison + # for every theorem — a `2i` theorem could be described as Grade 1, and in a + # multi-theorem ledger a single proof masked every other claim. The summary + # table is the machine-readable place the page states a grade, so the gate + # reads the row for each theorem id and compares it with that theorem's own + # ledger grade, in both directions. + while IFS=$'\x1f' read -r tid g; do + [ -z "$tid" ] && continue + claimed="$(awk -F'|' -v id="$tid" ' + /^\|/ { + cell = $2; gsub(/^[ \t]+|[ \t]+$/, "", cell) + if (cell == id) { g = $4; print g; exit } + }' "$DOCS_STATUS" | tr -d '*+`' | tr -d ' \t')" + if [ -z "$claimed" ]; then + fail "$DOCS_STATUS has no grade row for theorem '$tid' — the summary table must carry the ledger's grade where the gate can read it (mathesis §11)" + elif [ "$claimed" != "$g" ]; then + fail "$DOCS_STATUS records '$tid' at Grade $claimed but the ledger says Grade $g (mathesis §5/§6: the page is a summary of the ledger, and the ledger wins)" + fi + done < <(jq -r '.theorems[] | [.id, (.grade | tostring)] | join("\u001f")' "$LEDGER") + + 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=$'\x1f' 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 // "") ] | map(tostring) | join("\u001f")' "$LEDGER") + +if [ "${#WAIVERS[@]}" -gt 0 ]; then + echo "--- waived legs (no status token; PROOF-POLICY §4) ---" + printf ' - %s\n' "${WAIVERS[@]}" + echo "" +fi + +# --- 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 "" + +# 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[@]}" + echo "" +fi + +status="PASS" +[ "${#FAILS[@]}" -gt 0 ] && status="FAIL" + +if [[ -n "$RECEIPT" ]]; then + if ! mkdir -p "$(dirname "$RECEIPT")" 2>/dev/null; then + echo "FAIL: cannot create receipt directory for $RECEIPT" >&2 + exit 1 + fi + { + 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: $(policy_label)${POLICY_COMMIT:+ @ $POLICY_COMMIT}${POLICY_RULING:+ ($POLICY_RULING)}${POLICY_AMENDED:+, amended $POLICY_AMENDED}" + echo "policy-vendored-here: $POLICY_VENDORED" + 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 + echo "waivered-legs:" + if [[ "${#WAIVERS[@]}" -eq 0 ]]; then echo " (none)"; else printf ' - %s\n' "${WAIVERS[@]}"; fi + if [[ "${#FAILS[@]}" -gt 0 ]]; then + echo "failures:" + printf ' - %s\n' "${FAILS[@]}" + fi + } >"$RECEIPT" || { + echo "FAIL: cannot write receipt $RECEIPT" >&2 + exit 1 + } + 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..da4a6d8 --- /dev/null +++ b/scripts/check-proofs.sh @@ -0,0 +1,991 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-proofs.sh [--root PATH] [--ledger PATH] [--receipt PATH] +# prover in: idris2 | lean4 | agda | coq +# +# Single source of truth for compiling proofs AND, for every gated +# Rocq/Lean recheck witness, querying kernel-level assumptions against the +# owning leg's recorded `axioms` list in verification/proofs/LEDGER.json +# (nextgen-typing#131, PROOF-POLICY §2 / §5 / §6 / §7, mathesis §5-§6). +# +# Why compilation alone is insufficient: +# - `coqc` exits 0 on `Admitted`, on local `Axiom`/`Parameter` declarations, +# and on clean proofs that `Require Import` axioms from another module +# (such as `Coq.Logic.Classical_Prop.classic`). +# - `lean` exits 0 on `sorry`, on local `axiom` declarations, and on proofs +# whose imported dependencies use `Classical.choice` or `sorryAx`. +# - Single-file lexical scanning (`proof-scan-dangerous.sh`) catches tokens +# written inside the witness file itself, NOT assumptions imported across a +# module boundary or drawn from a standard library. +# +# Therefore, after compiling every gated Rocq or Lean module in an isolated +# scratch tree (leaving no `.vo`/`.glob`/`.olean` build artifacts in the working +# tree): +# * Rocq (`coq`): +# 1. Runs `coqchk -Q . "" -silent -o ` on the compiled `.vo`, +# verifying a predicative `Set`, `` for `type-in-type`, unsafe +# `(co)fixpoints`, and assumed positivity, and comparing `* Axioms:` +# against the ledger's `axioms` list for the claiming leg(s). +# 2. Generates and compiles a probe that `Require`s `` and runs +# `Print Assumptions ..` for every recorded target +# declaration, failing closed unless output is `Closed under the +# global context` or `Axioms:` matching the ledger entry. +# * Lean 4 (`lean4`): +# 1. Compiles with `-R -o .olean` (preserving +# `lean --print-libdir` on `LEAN_PATH`). +# 2. Generates and runs a probe that `import`s `` and executes +# `#print axioms ` for every recorded target declaration, +# failing unconditionally on `sorryAx` and on any unrecorded or stale +# ledger axiom. +# * Verbatim kernel query output is appended to `--receipt` whenever supplied. +# +# Exit: 0 = every gated module compiles, passes kernel assumption checks, every +# quarantined module still fails, and every proof on disk is listed; +# 1 = compilation, coverage, or assumption failure; +# 2 = CLI misuse. + +set -euo pipefail + +usage() { + echo "usage: $(basename "$0") [--root PATH] [--ledger PATH] [--receipt PATH]" >&2 + exit 2 +} + +PROVER="${1:-}" +case "$PROVER" in + idris2|lean4|agda|coq) shift ;; + *) usage ;; +esac + +CALLER_PWD="$PWD" +SCRIPT_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +ROOT_ARG="" +LEDGER_ARG="" +RECEIPT_ARG="" + +while [[ "$#" -gt 0 ]]; do + case "$1" in + --root) + [[ "$#" -ge 2 ]] || usage + ROOT_ARG="$2" + shift 2 + ;; + --root=*) + ROOT_ARG="${1#--root=}" + shift + ;; + --ledger) + [[ "$#" -ge 2 ]] || usage + LEDGER_ARG="$2" + shift 2 + ;; + --ledger=*) + LEDGER_ARG="${1#--ledger=}" + shift + ;; + --receipt) + [[ "$#" -ge 2 ]] || usage + RECEIPT_ARG="$2" + shift 2 + ;; + --receipt=*) + RECEIPT_ARG="${1#--receipt=}" + shift + ;; + -h|--help) + sed -n '2,47p' "$0" + exit 0 + ;; + *) + echo "unknown argument: $1" >&2 + usage + ;; + esac +done + +# Resolve a relative path against the original caller's directory; leave an +# absolute path unchanged. This does not check whether the path exists. +resolve_caller_path() { + local p="$1" + if [[ "$p" == /* ]]; then + printf '%s\n' "$p" + else + printf '%s/%s\n' "$CALLER_PWD" "$p" + fi +} + +if [[ -n "$ROOT_ARG" ]]; then + ROOT="$(cd "$(resolve_caller_path "$ROOT_ARG")" && pwd)" +else + ROOT="$SCRIPT_ROOT" +fi +cd "$ROOT" + +PROOF_DIR="verification/proofs/$PROVER" +MANIFEST_FILE="$PROOF_DIR/MANIFEST" + +if [[ -n "$LEDGER_ARG" ]]; then + LEDGER="$(resolve_caller_path "$LEDGER_ARG")" +else + LEDGER="$ROOT/verification/proofs/LEDGER.json" +fi + +RECEIPT="" +if [[ -n "$RECEIPT_ARG" ]]; then + RECEIPT="$(resolve_caller_path "$RECEIPT_ARG")" + if ! mkdir -p "$(dirname "$RECEIPT")" 2>/dev/null; then + echo "FAIL: cannot create receipt directory for $RECEIPT" >&2 + exit 1 + fi +fi + +# --- per-prover configuration ------------------------------------------------- +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 + +RECEIPT_SECTIONS=() +append_receipt_section() { + RECEIPT_SECTIONS+=("$1") +} + +# Write the verdict, module counts and collected query output to $RECEIPT. +# With no receipt path this does nothing; a write failure exits the script. +write_receipt() { + local status="$1" gated_cnt="$2" quar_cnt="$3" note_line="${4:-}" + [[ -n "$RECEIPT" ]] || return 0 + local ledger_sha="unavailable" + if [[ -f "$LEDGER" ]]; then + ledger_sha="$(sha256sum "$LEDGER" | cut -d' ' -f1)" + fi + { + echo "proof-witness receipt ($PROVER)" + echo "generated: $(date -u +%Y-%m-%dT%H:%M:%SZ)" + echo "commit: ${GITHUB_SHA:-$(git rev-parse HEAD 2>/dev/null || echo unknown)}" + echo "prover: $PROVER" + echo "status: $status" + echo "manifest: $MANIFEST_FILE" + echo "ledger: ${LEDGER#"$ROOT"/}" + echo "ledger-sha256: $ledger_sha" + echo "gated-modules: $gated_cnt" + echo "quarantined-modules: $quar_cnt" + if [[ -n "$note_line" ]]; then + echo "note: $note_line" + fi + if [[ "${#RECEIPT_SECTIONS[@]}" -gt 0 ]]; then + echo "" + echo "=== verbatim kernel assumption queries ===" + local sec + for sec in "${RECEIPT_SECTIONS[@]}"; do + printf '%s\n' "$sec" + done + fi + } >"$RECEIPT" || { + echo "FAIL: cannot write receipt $RECEIPT" >&2 + exit 1 + } +} + +find_proof_files() { + local dir="$1" + if [[ "$PROVER" == "agda" ]]; then + find "$dir" \( -name '*.agda' -o -name '*.lagda' -o -name '*.lagda.*' \) -not -path '*/build/*' 2>/dev/null + else + find "$dir" -name "*.$EXT" -not -path '*/build/*' 2>/dev/null + fi +} + +echo "=== $PROVER proof check ===" + +# --- a repo with proofs but no MANIFEST is itself a failure ------------------- +if [[ ! -f "$MANIFEST_FILE" ]]; then + if [[ -d "$PROOF_DIR" ]] && [[ -n "$(find_proof_files "$PROOF_DIR" | head -1)" ]]; then + echo "FAIL: $PROOF_DIR contains .$EXT proofs but has no MANIFEST." >&2 + echo " Create $MANIFEST_FILE listing each as 'gated' or 'quarantine'." >&2 + write_receipt "FAIL" 0 0 "missing MANIFEST for non-empty $PROOF_DIR" + exit 1 + fi + echo "no $PROOF_DIR/*.$EXT proofs and no MANIFEST — nothing to check." + write_receipt "PASS (no-manifest)" 0 0 "no .$EXT proofs and no MANIFEST" + exit 0 +fi + +# --- nothing to check is not the same as a missing toolchain ----------------- +manifest_entries=0 +if [[ -f "$MANIFEST_FILE" ]]; then + while IFS='|' read -r mroot _mrel _mstatus _mnote; do + [[ -z "${mroot// }" ]] && continue + case "${mroot#"${mroot%%[![:space:]]*}"}" in \#*) continue ;; esac + manifest_entries=$((manifest_entries + 1)) + done < "$MANIFEST_FILE" +fi +disk_proofs="$(find_proof_files "$PROOF_DIR" | head -1)" +if [[ "$manifest_entries" -eq 0 ]] && [[ -z "$disk_proofs" ]]; then + echo "no $PROOF_DIR/*.$EXT proofs and no MANIFEST entries — nothing to check." + write_receipt "PASS (no-modules)" 0 0 "0 gated modules in MANIFEST; no witness compiled or assumption-queried" + exit 0 +fi + +# --- toolchain: absent means FAIL, never skip --------------------------------- +required_tools=("$CMD") +case "$PROVER" in + coq) required_tools+=(coqchk coqtop jq) ;; + lean4) required_tools+=(jq) ;; +esac +for req_tool in "${required_tools[@]}"; do + if ! command -v "$req_tool" >/dev/null 2>&1; then + { + echo "FAIL: '$req_tool' not found on PATH." + echo + echo "This is deliberately fatal. A missing $PROVER verification tool must" + echo "never report green on work it could not check. Install '$req_tool'," + echo "or run this in CI where the workflow installs the pinned toolchain." + } >&2 + write_receipt "FAIL (missing-toolchain)" 0 0 "missing required tool: $req_tool" + exit 1 + fi +done + +TOOLCHAIN_LINE="$("$CMD" --version 2>/dev/null | head -1 || true)" +printf '%s\n' "$TOOLCHAIN_LINE" +if [[ "$PROVER" == "coq" ]]; then + COQCHK_LINE="$(coqchk --version 2>&1 | head -1 || true)" + append_receipt_section "toolchain: coqc=${TOOLCHAIN_LINE}; coqchk=${COQCHK_LINE}" +elif [[ "$PROVER" == "lean4" ]]; then + LEAN_LIBDIR="$(lean --print-libdir 2>/dev/null || printf '%s/lib/lean' "$(lean --print-prefix)")" + append_receipt_section "toolchain: lean=${TOOLCHAIN_LINE}" +elif [[ -n "$TOOLCHAIN_LINE" ]]; then + append_receipt_section "toolchain: ${CMD}=${TOOLCHAIN_LINE}" +fi +echo + +listed_tmp="$(mktemp)" +compiled_gated_tmp="$(mktemp)" +WORK_BASE="$(mktemp -d)" +trap 'rm -f "$listed_tmp" "$compiled_gated_tmp"; rm -rf "$WORK_BASE"' EXIT + +normalize_rel_path() { + local root="${1%/}" rel="${2#./}" + root="${root#./}" + if [[ -z "$root" || "$root" == "." ]]; then + printf '%s\n' "$rel" + else + printf '%s/%s\n' "$root" "$rel" + fi +} + +# Copy a source root into the scratch tree once and print its staged path. +# Subsequent calls reuse it, including any compiled modules already there. +stage_source_root() { + local root="${1%/}" + root="${root#./}" + [[ -z "$root" ]] && root="." + local dest="$WORK_BASE/$root" + if [[ ! -d "$dest" ]]; then + mkdir -p "$dest" + cp -a "$ROOT/$root/." "$dest/" + fi + printf '%s\n' "$dest" +} + +LAST_OUT="" +# Compile the module relative to its source root. Return 1 and set $LAST_OUT +# to the tool output on failure; clear $LAST_OUT on success. Rocq and Lean +# compile in the staged tree, while Idris2 and Agda run from the source root. +check_one() { + local root="$1" rel="$2" out rc work_root olean_rel olean_out + set +e + case "$PROVER" in + idris2) + out="$(cd "$ROOT/$root" && idris2 --check "$rel" 2>&1)" + rc=$? + ;; + lean4) + work_root="$(stage_source_root "$root")" + olean_rel="${rel#./}" + olean_out="$work_root/${olean_rel%.lean}.olean" + mkdir -p "$(dirname "$olean_out")" + out="$(cd "$work_root" && LEAN_PATH="$work_root:$LEAN_LIBDIR${LEAN_PATH:+:$LEAN_PATH}" lean -R "$work_root" -o "$olean_out" "$work_root/$olean_rel" 2>&1)" + rc=$? + ;; + agda) + out="$(cd "$ROOT/$root" && agda --safe --without-K --cubical-compatible "$rel" 2>&1)" + rc=$? + ;; + coq) + work_root="$(stage_source_root "$root")" + out="$(cd "$work_root" && coqc -Q . "" "$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 +} + +is_valid_ident() { + local ident="$1" + [[ "$ident" =~ ^[A-Za-z_][A-Za-z0-9_\']*(\.[A-Za-z_][A-Za-z0-9_\']*)*$ ]] +} + +array_contains() { + local needle="$1" + shift + local item + for item in "$@"; do + [[ "$item" == "$needle" ]] && return 0 + done + return 1 +} + +# Match a kernel-reported Coq axiom `.` or external `.` +# against the owning leg's recorded `.axioms` array. Whenever `` maps +# to a staged `.v` file in `$work_root` (either the primary witness or a staged +# support module), `` MUST be declared via `Axiom`/`Parameter`/`Conjecture` +# in that file — so an incomplete `Theorem ... Admitted.` can never satisfy the +# kernel check even if its full name is listed in `.axioms`. +coq_axiom_allowed() { + local ax="$1" mod_path="$2" work_root="$3" + shift 3 + local allowed=("$@") + [[ "${#allowed[@]}" -gt 0 ]] || return 1 + + if [[ "$ax" == *.* ]]; then + local cand_mod="${ax%.*}" + local short="${ax##*.}" + local local_v="$work_root/${cand_mod//./\/}.v" + if [[ -f "$local_v" ]]; then + if ! grep -qE "^[[:space:]]*(Axiom|Parameter|Conjecture)[[:space:]]+${short//./\\.}([^A-Za-z0-9_']|$)" "$local_v" 2>/dev/null; then + return 1 + fi + if array_contains "$ax" "${allowed[@]}" || { [[ "$cand_mod" == "$mod_path" ]] && array_contains "$short" "${allowed[@]}"; }; then + return 0 + fi + return 1 + fi + fi + + array_contains "$ax" "${allowed[@]}" +} + +ASSUMPTION_ERR="" + +# Return 1 and set $ASSUMPTION_ERR if the ledger is missing or invalid JSON. +# The path argument identifies the witness in the error message. +verify_ledger_ready() { + local full_rel="$1" + if [[ ! -f "$LEDGER" ]]; then + ASSUMPTION_ERR="assumption check failed for $full_rel: ledger not found at $LEDGER" + return 1 + fi + if ! jq -e . "$LEDGER" >/dev/null 2>&1; then + ASSUMPTION_ERR="assumption check failed for $full_rel: ledger is not valid JSON ($LEDGER)" + return 1 + fi + return 0 +} + +# Emit matching non-open legs for ($1 = prover_kind: coq|lean4, $2 = full_rel). +# Output lines use US (\x1f): role (primary|support), theorem id, status, +# axioms JSON and declarations JSON. A jq failure returns non-zero, although +# callers using process substitution do not receive that status. +query_claiming_legs() { + local pkind="$1" full_rel="$2" + jq -r --arg kind "$pkind" --arg path "$full_rel" ' + def match_prover($p): + if $kind == "coq" then ($p == "rocq" or $p == "coq") + else ($p == "lean4" or $p == "lean") + end; + def target_decls($t; $leg): + if ($leg.declarations // null) != null then + if ($leg.declarations | type) == "array" then + [ $leg.declarations[] | if type == "object" then (.name // "") else tostring end ] + else + [""] + end + elif (($t.statement_formal.declarations // []) | length) > 0 then + [ $t.statement_formal.declarations[] | (.name // "") ] + else + [ ($t.statement_anchor // [])[] | tostring ] + end; + .theorems[] as $t + | ($t.legs // [])[] as $leg + | select($leg.waiver == null) + | select(match_prover($leg.prover // "")) + | select(($leg.status // "open") != "open") + | (if ($leg.artifact // "") == $path then "primary" + elif ((($leg.support_files // []) | type) == "array" and (($leg.support_files // []) | index($path)) != null) then "support" + else "" end) as $role + | select($role != "") + | [ + $role, + ($t.id // ""), + ($leg.status // ""), + (if (($leg.axioms // []) | type) == "array" then (($leg.axioms // []) | tojson) else "null" end), + (target_decls($t; $leg) | tojson) + ] + | join("\u001f") + ' "$LEDGER" +} + +# Check a compiled Rocq module against each claiming ledger leg. The arguments +# are its source root, path relative to that root and staged root. Append query +# output to the receipt sections; on rejection return 1 and set $ASSUMPTION_ERR. +verify_coq_assumptions() { + local root="$1" rel="$2" work_root="$3" + local clean_rel="${rel#./}" + local full_rel mod_path src_file + full_rel="$(normalize_rel_path "$root" "$clean_rel")" + mod_path="${clean_rel%.v}" + mod_path="${mod_path//\//.}" + + verify_ledger_ready "$full_rel" || return 1 + + local leg_rows=() + local row + while IFS= read -r row; do + [[ -n "$row" ]] && leg_rows+=("$row") + done < <(query_claiming_legs "coq" "$full_rel") + + if [[ "${#leg_rows[@]}" -eq 0 ]]; then + ASSUMPTION_ERR="assumption check failed for $full_rel: gated in $MANIFEST_FILE, but no non-open Rocq leg in $LEDGER claims '$full_rel' (in .artifact or .support_files)" + return 1 + fi + + # 1. Kernel checker over the compiled .vo (`coqchk -silent -o`). + local coqchk_out coqchk_rc + set +e + coqchk_out="$(cd "$work_root" && coqchk -Q . "" -silent -o "$mod_path" 2>&1)" + coqchk_rc=$? + set -e + + append_receipt_section "--- [coqchk] $full_rel (module: $mod_path) --- +\$ coqchk -Q . \"\" -silent -o $mod_path +${coqchk_out}" + + if [[ "$coqchk_rc" -ne 0 ]] || ! grep -qF 'CONTEXT SUMMARY' <<<"$coqchk_out"; then + ASSUMPTION_ERR="coqchk failed or emitted no CONTEXT SUMMARY for $full_rel (exit $coqchk_rc): +$coqchk_out" + return 1 + fi + if ! grep -qE '^\* Theory: Set is predicative[[:space:]]*$' <<<"$coqchk_out"; then + ASSUMPTION_ERR="$full_rel: coqchk did not confirm predicative Set: +$coqchk_out" + return 1 + fi + if ! grep -qE '^\* Constants/Inductives relying on type-in-type:[[:space:]]*[[:space:]]*$' <<<"$coqchk_out"; then + ASSUMPTION_ERR="$full_rel: coqchk reported type-in-type reliance: +$coqchk_out" + return 1 + fi + if ! grep -qE '^\* Constants/Inductives relying on unsafe \(co\)fixpoints:[[:space:]]*[[:space:]]*$' <<<"$coqchk_out"; then + ASSUMPTION_ERR="$full_rel: coqchk reported unsafe (co)fixpoints: +$coqchk_out" + return 1 + fi + if ! grep -qE '^\* Inductives whose positivity is assumed:[[:space:]]*[[:space:]]*$' <<<"$coqchk_out"; then + ASSUMPTION_ERR="$full_rel: coqchk reported assumed inductive positivity: +$coqchk_out" + return 1 + fi + + local coqchk_ax_raw coqchk_parse_rc + set +e + coqchk_ax_raw="$(awk ' + /^\* Axioms:[[:space:]]*[[:space:]]*$/ { seen = 1; none = 1; next } + /^\* Axioms:[[:space:]]*$/ { seen = 1; in_ax = 1; next } + in_ax && /^\*/ { in_ax = 0 } + in_ax && NF > 0 { + line = $0 + sub(/^[[:space:]]+/, "", line) + sub(/[[:space:]]+$/, "", line) + if (line != "") { print line; count++ } + } + END { + if (!seen) exit 2 + if (!none && count == 0) exit 3 + } + ' <<<"$coqchk_out")" + coqchk_parse_rc=$? + set -e + if [[ "$coqchk_parse_rc" -ne 0 ]]; then + ASSUMPTION_ERR="$full_rel: could not parse '* Axioms:' block from coqchk output (code $coqchk_parse_rc): +$coqchk_out" + return 1 + fi + + local coqchk_axioms=() + local ax_line + while IFS= read -r ax_line; do + [[ -n "$ax_line" ]] && coqchk_axioms+=("$ax_line") + done <<<"$coqchk_ax_raw" + + # 2. Validate against every claiming leg and run per-declaration Print Assumptions. + local role tid leg_status axioms_json decls_json + for row in "${leg_rows[@]}"; do + IFS=$'\x1f' read -r role tid leg_status axioms_json decls_json <<<"$row" + if [[ "$axioms_json" == "null" ]]; then + ASSUMPTION_ERR="$full_rel ($tid): leg .axioms must be a JSON array" + return 1 + fi + + local allowed_axioms=() + local a_entry + while IFS= read -r a_entry; do + [[ -n "$a_entry" ]] && allowed_axioms+=("$a_entry") + done < <(jq -r '.[]' <<<"$axioms_json") + + if [[ "${#allowed_axioms[@]}" -gt 0 ]] && array_contains "sorryAx" "${allowed_axioms[@]}"; then + ASSUMPTION_ERR="$full_rel ($tid): 'sorryAx' is never permitted in .axioms" + return 1 + fi + if [[ "$leg_status" == "proven" && "${#allowed_axioms[@]}" -gt 0 ]]; then + ASSUMPTION_ERR="$full_rel ($tid): status is 'proven' (zero axioms permitted) but .axioms lists: ${allowed_axioms[*]}" + return 1 + fi + if [[ "$leg_status" == "proven-with-postulates" && "${#allowed_axioms[@]}" -eq 0 ]]; then + ASSUMPTION_ERR="$full_rel ($tid): status is 'proven-with-postulates' but .axioms is empty" + return 1 + fi + + local cax + for cax in ${coqchk_axioms[@]+"${coqchk_axioms[@]}"}; do + if ! coq_axiom_allowed "$cax" "$mod_path" "$work_root" ${allowed_axioms[@]+"${allowed_axioms[@]}"}; then + ASSUMPTION_ERR="$full_rel ($tid): coqchk reported undeclared or non-axiom assumption '$cax' (Admitted theorems are never allowed; ledger allows: [${allowed_axioms[*]:-none}])" + return 1 + fi + done + + if [[ "$role" == "primary" ]]; then + local target_decls=() + local d_entry + while IFS= read -r d_entry; do + [[ -n "$d_entry" ]] && target_decls+=("$d_entry") + done < <(jq -r '.[]' <<<"$decls_json") + + if [[ "${#target_decls[@]}" -eq 0 ]]; then + ASSUMPTION_ERR="$full_rel ($tid): no target declarations recorded in statement_formal.declarations or leg.declarations" + return 1 + fi + + local seen_leg_axioms=() + local decl qdecl probe_v probe_out probe_rc + for decl in "${target_decls[@]}"; do + if ! is_valid_ident "$decl"; then + ASSUMPTION_ERR="$full_rel ($tid): declaration '$decl' is not a valid Rocq identifier — map Agda anchors to Rocq identifiers in legs[].declarations" + return 1 + fi + if [[ "$decl" == "${mod_path}."* ]]; then + qdecl="$decl" + else + qdecl="${mod_path}.${decl}" + fi + probe_v="$work_root/__probe_assumptions.v" + printf 'Set Printing Width 1000000.\nRequire %s.\nPrint Assumptions %s.\n' "$mod_path" "$qdecl" >"$probe_v" + set +e + probe_out="$(cd "$work_root" && coqc -Q . "" __probe_assumptions.v 2>&1)" + probe_rc=$? + set -e + rm -f "$work_root"/__probe_assumptions.* + + append_receipt_section "--- [Print Assumptions] $full_rel ($tid :: $qdecl) --- +recorded-axioms: ${axioms_json} +\$ Print Assumptions ${qdecl}. +${probe_out}" + + if [[ "$probe_rc" -ne 0 ]] || grep -qE '^Error:' <<<"$probe_out"; then + ASSUMPTION_ERR="$full_rel ($tid): Print Assumptions failed for '$qdecl' (exit $probe_rc): +$probe_out" + return 1 + fi + if grep -qE '^(Section Variables|Type Variables|Opaque constants|Transparent constants|Theory):' <<<"$probe_out" \ + || grep -qE '(is assumed to be (positive|guarded)|relies on (an unsafe hierarchy|definitional UIP))' <<<"$probe_out"; then + ASSUMPTION_ERR="$full_rel ($tid): '$qdecl' relies on unclosed variables or unsafe kernel flags: +$probe_out" + return 1 + fi + if grep -qE '^Closed under the global context[[:space:]]*$' <<<"$probe_out" \ + && ! grep -qE '^Axioms:' <<<"$probe_out"; then + continue + fi + if grep -qE '^Axioms:[[:space:]]*$' <<<"$probe_out"; then + local decl_ax_raw + decl_ax_raw="$(awk ' + /^Axioms:[[:space:]]*$/ { in_ax = 1; next } + in_ax && /^[A-Za-z_][A-Za-z0-9_\x27.]*[[:space:]]*:/ { + line = $0 + sub(/[[:space:]]*:.*$/, "", line) + print line + } + ' <<<"$probe_out")" + if [[ -z "${decl_ax_raw//[[:space:]]/}" ]]; then + ASSUMPTION_ERR="$full_rel ($tid): Print Assumptions printed 'Axioms:' for '$qdecl' but no axiom names could be parsed: +$probe_out" + return 1 + fi + local dax resolved_ax cax_cand + while IFS= read -r dax; do + [[ -z "$dax" ]] && continue + resolved_ax="" + if coq_axiom_allowed "$dax" "$mod_path" "$work_root" ${allowed_axioms[@]+"${allowed_axioms[@]}"}; then + resolved_ax="$dax" + else + # Coq's Nametab pretty-printer elides `-R` prefixes in scope (for + # example printing `Classical_Prop.classic` where `coqchk` printed + # the canonical kernel KerName `Coq.Logic.Classical_Prop.classic`). + # Because every element of `coqchk_axioms` was already verified + # against `allowed_axioms` above, resolve `dax` to a canonical + # kernel axiom ending in `.${dax}` when unambiguous. + for cax_cand in ${coqchk_axioms[@]+"${coqchk_axioms[@]}"}; do + if [[ "$cax_cand" == *".${dax}" ]] \ + && coq_axiom_allowed "$cax_cand" "$mod_path" "$work_root" ${allowed_axioms[@]+"${allowed_axioms[@]}"}; then + resolved_ax="$cax_cand" + break + fi + done + fi + if [[ -z "$resolved_ax" ]]; then + ASSUMPTION_ERR="$full_rel ($tid): '$qdecl' depends on undeclared axiom '$dax' (ledger allows: [${allowed_axioms[*]:-none}])" + return 1 + fi + seen_leg_axioms+=("$resolved_ax") + done <<<"$decl_ax_raw" + else + ASSUMPTION_ERR="$full_rel ($tid): unexpected Print Assumptions output for '$qdecl': +$probe_out" + return 1 + fi + done + + # Every axiom listed in .axioms on the primary leg must actually be used + # by at least one recorded declaration in Print Assumptions, preventing + # stale or padded axiom lists. + local lax matched_lax obs + for lax in ${allowed_axioms[@]+"${allowed_axioms[@]}"}; do + matched_lax=0 + for obs in ${seen_leg_axioms[@]+"${seen_leg_axioms[@]}"}; do + [[ -z "$obs" ]] && continue + if [[ "$obs" == "$lax" || "$obs" == "${mod_path}.${lax}" ]]; then + matched_lax=1 + break + fi + done + if [[ "$matched_lax" -eq 0 ]]; then + ASSUMPTION_ERR="$full_rel ($tid): ledger .axioms lists '$lax', but Print Assumptions did not report '$lax' on any recorded declaration — remove stale axioms (or promote status to 'proven' if axiom-free)" + return 1 + fi + done + fi + done + + return 0 +} + +# Check a compiled Lean module against each claiming ledger leg. The arguments +# are its source root, path relative to that root and staged root. Append query +# output to the receipt sections; on rejection return 1 and set $ASSUMPTION_ERR. +verify_lean_assumptions() { + local root="$1" rel="$2" work_root="$3" + local clean_rel="${rel#./}" + local full_rel mod_path + full_rel="$(normalize_rel_path "$root" "$clean_rel")" + mod_path="${clean_rel%.lean}" + mod_path="${mod_path//\//.}" + + verify_ledger_ready "$full_rel" || return 1 + + local leg_rows=() + local row + while IFS= read -r row; do + [[ -n "$row" ]] && leg_rows+=("$row") + done < <(query_claiming_legs "lean4" "$full_rel") + + if [[ "${#leg_rows[@]}" -eq 0 ]]; then + ASSUMPTION_ERR="assumption check failed for $full_rel: gated in $MANIFEST_FILE, but no non-open Lean leg in $LEDGER claims '$full_rel' (in .artifact or .support_files)" + return 1 + fi + + local role tid leg_status axioms_json decls_json + for row in "${leg_rows[@]}"; do + IFS=$'\x1f' read -r role tid leg_status axioms_json decls_json <<<"$row" + if [[ "$axioms_json" == "null" ]]; then + ASSUMPTION_ERR="$full_rel ($tid): leg .axioms must be a JSON array" + return 1 + fi + + local allowed_axioms=() + local a_entry + while IFS= read -r a_entry; do + [[ -n "$a_entry" ]] && allowed_axioms+=("$a_entry") + done < <(jq -r '.[]' <<<"$axioms_json") + + if [[ "${#allowed_axioms[@]}" -gt 0 ]] && array_contains "sorryAx" "${allowed_axioms[@]}"; then + ASSUMPTION_ERR="$full_rel ($tid): 'sorryAx' is an incomplete-proof marker and is never permitted in .axioms" + return 1 + fi + if [[ "$leg_status" == "proven" && "${#allowed_axioms[@]}" -gt 0 ]]; then + ASSUMPTION_ERR="$full_rel ($tid): status is 'proven' (zero axioms permitted) but .axioms lists: ${allowed_axioms[*]}" + return 1 + fi + if [[ "$leg_status" == "proven-with-postulates" && "${#allowed_axioms[@]}" -eq 0 ]]; then + ASSUMPTION_ERR="$full_rel ($tid): status is 'proven-with-postulates' but .axioms is empty" + return 1 + fi + + if [[ "$role" == "support" ]]; then + # Support modules are compiled to .olean above; check that simply importing + # the module succeeds cleanly, while the primary artifact probes the + # recorded declarations' transitive axiom closure (which includes every + # imported support module). + local sup_probe="$work_root/__AssumptionsSupportProbe.lean" + local sup_out sup_rc + printf 'import %s\n' "$mod_path" >"$sup_probe" + set +e + sup_out="$(cd "$work_root" && LEAN_PATH="$work_root:$LEAN_LIBDIR${LEAN_PATH:+:$LEAN_PATH}" lean "$sup_probe" 2>&1)" + sup_rc=$? + set -e + rm -f "$sup_probe" + append_receipt_section "--- [Lean support import] $full_rel ($tid :: $mod_path) --- +\$ import ${mod_path} +${sup_out:-}" + if [[ "$sup_rc" -ne 0 ]] || grep -qE 'error:' <<<"$sup_out"; then + ASSUMPTION_ERR="$full_rel ($tid): importing support module '$mod_path' failed (exit $sup_rc): +$sup_out" + return 1 + fi + continue + fi + + local target_decls=() + local d_entry + while IFS= read -r d_entry; do + [[ -n "$d_entry" ]] && target_decls+=("$d_entry") + done < <(jq -r '.[]' <<<"$decls_json") + + if [[ "${#target_decls[@]}" -eq 0 ]]; then + ASSUMPTION_ERR="$full_rel ($tid): no target declarations recorded in statement_formal.declarations or leg.declarations" + return 1 + fi + + local probe_file="$work_root/__AssumptionsProbe.lean" + { + printf 'import %s\n' "$mod_path" + local decl + for decl in "${target_decls[@]}"; do + if ! is_valid_ident "$decl"; then + rm -f "$probe_file" + ASSUMPTION_ERR="$full_rel ($tid): declaration '$decl' is not a valid Lean identifier — map Agda anchors to Lean identifiers in legs[].declarations" + return 1 + fi + printf '#print axioms %s\n' "$decl" + done + } >"$probe_file" + + local probe_out probe_rc + set +e + probe_out="$(cd "$work_root" && LEAN_PATH="$work_root:$LEAN_LIBDIR${LEAN_PATH:+:$LEAN_PATH}" lean "$probe_file" 2>&1)" + probe_rc=$? + set -e + rm -f "$probe_file" + + append_receipt_section "--- [#print axioms] $full_rel ($tid :: $mod_path) --- +recorded-axioms: ${axioms_json} +declarations: $(printf '%s ' "${target_decls[@]}") +${probe_out}" + + if [[ "$probe_rc" -ne 0 ]] || grep -qE 'error:' <<<"$probe_out"; then + ASSUMPTION_ERR="$full_rel ($tid): Lean assumption probe failed (exit $probe_rc): +$probe_out" + return 1 + fi + + local verdict_count=0 + local seen_leg_axioms=() + local pline pdecl pax_csv pax + local re_clean="^([^']+:[[:space:]]*info:[[:space:]]*)?'([^']+)' does not depend on any axioms[[:space:]]*$" + local re_ax="^([^']+:[[:space:]]*info:[[:space:]]*)?'([^']+)' depends on axioms: \\[([^]]+)\\][[:space:]]*$" + + while IFS= read -r pline; do + [[ -z "${pline//[[:space:]]/}" ]] && continue + if [[ "$pline" =~ $re_clean ]]; then + verdict_count=$((verdict_count + 1)) + elif [[ "$pline" =~ $re_ax ]]; then + pdecl="${BASH_REMATCH[2]}" + pax_csv="${BASH_REMATCH[3]}" + verdict_count=$((verdict_count + 1)) + local raw_list=() + IFS=',' read -r -a raw_list <<<"$pax_csv" + for pax in "${raw_list[@]}"; do + pax="${pax#"${pax%%[![:space:]]*}"}" + pax="${pax%"${pax##*[![:space:]]}"}" + [[ -z "$pax" ]] && continue + if [[ "$pax" == "sorryAx" ]]; then + ASSUMPTION_ERR="$full_rel ($tid): '$pdecl' depends on 'sorryAx' — incomplete proof in $full_rel or an imported module" + return 1 + fi + if [[ "${#allowed_axioms[@]}" -eq 0 ]] || ! array_contains "$pax" "${allowed_axioms[@]}"; then + ASSUMPTION_ERR="$full_rel ($tid): '$pdecl' depends on undeclared axiom '$pax' (ledger allows: [${allowed_axioms[*]:-none}])" + return 1 + fi + seen_leg_axioms+=("$pax") + done + else + ASSUMPTION_ERR="$full_rel ($tid): unexpected output line from Lean #print axioms probe: + $pline" + return 1 + fi + done <<<"$probe_out" + + if [[ "$verdict_count" -ne "${#target_decls[@]}" ]]; then + ASSUMPTION_ERR="$full_rel ($tid): expected ${#target_decls[@]} '#print axioms' verdict(s), got $verdict_count: +$probe_out" + return 1 + fi + + local lax + for lax in ${allowed_axioms[@]+"${allowed_axioms[@]}"}; do + if [[ "${#seen_leg_axioms[@]}" -eq 0 ]] || ! array_contains "$lax" "${seen_leg_axioms[@]}"; then + ASSUMPTION_ERR="$full_rel ($tid): ledger .axioms lists '$lax', but '#print axioms' did not report '$lax' on any recorded declaration — remove stale axioms (or promote status to 'proven' if axiom-free)" + return 1 + fi + done + done + + return 0 +} + +fails=0 +unexpected_pass=0 +gated_count=0 +quarantine_count=0 + +while IFS='|' read -r root rel status note; do + [[ -z "${root// }" ]] && continue + case "${root#"${root%%[![:space:]]*}"}" in \#*) continue ;; esac + printf ' %-30s %-24s ' "$root" "$rel" + full_rel="$(normalize_rel_path "$root" "$rel")" + printf '%s\n' "$full_rel" >>"$listed_tmp" + + case "$status" in + gated) + gated_count=$((gated_count + 1)) + ;; + quarantine) + quarantine_count=$((quarantine_count + 1)) + ;; + *) + echo "FAIL — unknown MANIFEST status '${status}'" + echo " $MANIFEST_FILE accepts only 'gated' or 'quarantine'; anything else" + echo " would otherwise be read as quarantine and hide a broken module." + fails=$((fails + 1)) + continue + ;; + esac + + if [[ "$status" == "gated" ]] && { [[ "$PROVER" == "coq" ]] || [[ "$PROVER" == "lean4" ]]; } && [[ -f "$LEDGER" ]]; then + ledger_prover="$PROVER" + [[ "$PROVER" == "coq" ]] && ledger_prover="rocq" + missing_dep="$(jq -r --arg prover "$ledger_prover" --arg file "$full_rel" ' + [ .theorems[]? | .legs[]? + | select(.prover == $prover and (.status == "proven" or .status == "proven-with-postulates") and .artifact == $file) + | (.support_files // [])[] ] | unique[] + ' "$LEDGER" 2>/dev/null | while IFS= read -r sf; do + [[ -z "$sf" ]] && continue + if ! grep -Fxq -- "$sf" "$compiled_gated_tmp" 2>/dev/null; then + printf '%s\n' "$sf" + fi + done)" + if [[ -n "$missing_dep" ]]; then + echo "FAIL (manifest-order)" + while IFS= read -r sf; do + [[ -z "$sf" ]] && continue + echo " support_file '$sf' must appear as 'gated' BEFORE '$full_rel' in $MANIFEST_FILE (MANIFEST compiles in dependency order)" + done <<<"$missing_dep" + fails=$((fails + 1)) + continue + fi + fi + + if check_one "$root" "$rel"; then + if [[ "$status" == "gated" ]]; then + ASSUMPTION_ERR="" + if [[ "$PROVER" == "coq" ]]; then + work_root="$(stage_source_root "$root")" + if ! verify_coq_assumptions "$root" "$rel" "$work_root"; then + echo "FAIL (assumptions)" + printf '%s\n' "${ASSUMPTION_ERR//$'\n'/$'\n '}" | sed '1s/^/ /' + fails=$((fails + 1)) + continue + fi + elif [[ "$PROVER" == "lean4" ]]; then + work_root="$(stage_source_root "$root")" + if ! verify_lean_assumptions "$root" "$rel" "$work_root"; then + echo "FAIL (assumptions)" + printf '%s\n' "${ASSUMPTION_ERR//$'\n'/$'\n '}" | sed '1s/^/ /' + fails=$((fails + 1)) + continue + fi + fi + printf '%s\n' "$full_rel" >>"$compiled_gated_tmp" + 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 ----------------------------- +echo +echo "=== manifest coverage ($PROOF_DIR) ===" +listed="$(sort -u "$listed_tmp")" +found="$(cd "$ROOT" && find_proof_files "$PROOF_DIR" | sed 's|^\./||' | 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:" + while IFS= read -r u; do + [[ -n "$u" ]] && printf ' %s\n' "$u" + done <<<"$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):" + while IFS= read -r m; do + [[ -n "$m" ]] && printf ' %s\n' "$m" + done <<<"$missing" + fails=$((fails + 1)) +fi +if [[ -z "${unlisted//[[:space:]]/}${missing//[[:space:]]/}" ]]; then + echo " all $(printf '%s\n' "$found" | grep -c . || true) .$EXT file(s) accounted for" +fi + +echo +if [[ "$fails" -gt 0 ]] || [[ "$unexpected_pass" -gt 0 ]]; then + echo "RESULT: FAIL ($fails failure(s), $unexpected_pass unexpected pass(es))" + write_receipt "FAIL" "$gated_count" "$quarantine_count" "$fails failure(s), $unexpected_pass unexpected pass(es)" + exit 1 +fi +echo "RESULT: PASS -- gated modules compile and satisfy recorded kernel assumptions; quarantined modules still fail as recorded" +write_receipt "PASS" "$gated_count" "$quarantine_count" "all gated modules compiled and passed kernel assumption checks" diff --git a/scripts/proof-scan-dangerous.sh b/scripts/proof-scan-dangerous.sh new file mode 100755 index 0000000..86259ea --- /dev/null +++ b/scripts/proof-scan-dangerous.sh @@ -0,0 +1,298 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Banned-pattern scan for hosted proofs. +# +# Two policies meet here, and this scan is deliberately the union of them: +# +# * this repository's PROOF-NEEDS.adoc bans every escape hatch outright, and +# * the estate docs/TRUSTED-BASE-REDUCTION-POLICY.adoc (enforced estate-wide by +# standards scripts/check-trusted-base.sh via governance-reusable.yml) names +# the *core tier* that must be documented at minimum: +# Coq Axiom | Admitted | admit. +# Lean axiom | sorry +# Agda postulate +# Idris2 believe_me | really_believe_me | assert_total | partial +# F* assume val | admit_p +# Rust/Haskell unsafeCoerce | unsafePerformIO (soundness-relevant use) +# +# A repository may be stricter than the estate floor and may not be looser. This +# one is stricter: in proof sources, a core-tier marker fails *even when +# documented*, because the policy's disposition track exists to make escapes +# visible where a repo tolerates them, not to license them here. The disposition +# markers (TRUSTED:, AXIOM:, OWED:, JUSTIFIED:, DEBT:) and the debt register are +# checked by the estate script and by docs/proof-debt.md; this scan's job is the +# narrower, harder one. +# +# 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] +# bash scripts/proof-scan-dangerous.sh --scan-file PATH # one file, exit 1 on a hit +# bash scripts/proof-scan-dangerous.sh --patterns # the pattern string +# +# `--scan-file` is the control surface: it scans the path it is given even if +# `.trusted-base-ignore` exempts it, because a fixture that must stay detectable +# cannot be tested through the tree scan. `--patterns` exists so the ledger gate +# can *use* this list instead of keeping a second copy of it. + +set -uo pipefail + +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +cd "$ROOT" || exit 1 + +# Both trees: the hosted proofs, and the instrument's own fixtures. A scan +# that covers only the first would miss a real escape hatch planted in the second, +# and the estate checker scans the whole repository. +SCAN_DIRS="verification tests" +RECEIPT="" + +SCAN_FILE="" +SHOW_PATTERNS=0 +while [ "$#" -gt 0 ]; do + case "$1" in + --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 ;; + --patterns) SHOW_PATTERNS=1; shift ;; + -h|--help) sed -n '2,34p' "$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. +# Core tier of the estate policy, plus this repo's own extras (Obj.magic). +# `\b` keeps prose such as "postulates" out; the scan strips comments first, so a +# documented `AXIOM:` note is a comment and a real declaration is not. +# `admit` is written bare, not as `admit[.]`: the alternation is closed by a +# trailing \b, and the full stop in Coq's `admit.` is a non-word character, so +# `admit[.]\b` could never match — the dot and the boundary exclude each other. +# Bare `admit` still cannot reach prose such as "admits", because \b holds on +# both sides of the word. +PATTERNS='\b(believe_me|really_believe_me|assert_total|postulate|sorry|Admitted|Axiom|axiom|admit_p|admit|unsafeCoerce|unsafePerformIO|%default[[:space:]]+partial|assume[[:space:]]+val)\b|\bObj[.]magic\b' + +if [ "$SHOW_PATTERNS" -eq 1 ]; then + printf '%s\n' "$PATTERNS" + exit 0 +fi + +# The receipt is part of the evidence, so it cannot be best-effort. `just +# proof-scan-dangerous` passes target/proof-receipts/dangerous-patterns.txt on a +# fresh checkout where that directory does not exist yet; the redirect failed, the +# scan still exited 0, and the receipt a reader would look for was never written. +if [ -n "$RECEIPT" ]; then + if ! mkdir -p "$(dirname "$RECEIPT")" 2>/dev/null; then + echo "FAIL: cannot create the receipt directory for $RECEIPT" >&2 + exit 1 + fi +fi + +# write_receipt [extra line...] — a receipt write failure is a failure. +write_receipt() { + local status="$1"; shift + [ -n "$RECEIPT" ] || return 0 + { + 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: $status" + printf '%s\n' "$@" + } >"$RECEIPT" || { echo "FAIL: cannot write receipt $RECEIPT" >&2; exit 1; } +} + +echo "=== Scanning for dangerous patterns in proofs ===" +echo "patterns: $PATTERNS" +echo "scope: $SCAN_DIRS" + +# Print $1 with the comment syntax of ITS language removed, and string literals +# masked, preserving line numbers. Three things matter here: +# +# * One comment syntax for every language is wrong in the dangerous direction. +# `(*` is a comment in Coq and TLA+ but ordinary text in Lean, so a Lean file +# containing `(* ... Axiom ... *)` had the Axiom treated as commented-out and +# the scan called it clean. The delimiters are now chosen per extension. +# * Lean is not one of the languages with `//` comments: `{x // p x}` is +# subtype notation, so treating `//` as a comment would cut the line short +# and hide whatever followed on it. Lean takes `--` and `/- -/` only. +# * A comment marker inside a string is not a comment. Masks keep `"--"` in a +# string from opening one, and keep a banned word inside a string from being +# counted as code. Only double-quoted strings are masked: a prime is part of +# an ordinary identifier in Agda and Idris, and masking from it would hide +# the rest of the line. +# * For an unknown extension, comments are left intact and double-quoted +# strings are masked; no comment syntax is guessed. +# +# Nested block comments are not supported; an unclosed block comment runs to the +# end of the file. Delimiters are matched after string masking, so `"(*"` is +# text. Comment *text* is dropped rather than blanked, which keeps `grep -n` +# line numbers aligned with the file. +strip_comments() { + local f="$1" mode + case "$f" in + *.agda|*.lagda|*.lagda.md|*.lagda.rst|*.lagda.tex) mode=agda ;; + *.idr) mode=idris ;; + *.lean) mode=lean ;; + *.v) mode=coq ;; + *.tla) mode=tla ;; + *.fst|*.fstar) mode=fstar ;; + *) mode=raw ;; + esac + awk -v mode="$mode" ' + BEGIN { + lop1 = ""; lop2 = ""; bop = ""; bcl = "" + if (mode == "agda" || mode == "idris") { lop1 = "--"; bop = "{-"; bcl = "-}" } + else if (mode == "lean") { lop1 = "--"; bop = "/-"; bcl = "-/" } + else if (mode == "coq") { bop = "(*"; bcl = "*)" } + else if (mode == "tla") { lop1 = "\\*"; bop = "(*"; bcl = "*)" } + else if (mode == "fstar") { lop2 = "//"; bop = "(*"; bcl = "*)" } + block = 0 + } + { + line = $0; out = ""; i = 1; n = length(line); instr = "" + while (i <= n) { + c = substr(line, i, 1); two = substr(line, i, 2) + if (instr != "") { + if (c == "\\") { out = out " "; i += 2; continue } + if (c == instr) { instr = ""; out = out c; i += 1; continue } + out = out " "; i += 1; continue + } + if (block == 1) { + if (two == bcl) { block = 0; i += 2 } else { i += 1 } + continue + } + if (c == "\"") { instr = c; out = out c; i += 1; continue } + if (lop1 != "" && two == lop1) { break } + if (lop2 != "" && two == lop2) { break } + if (bop != "" && two == bop) { block = 1; i += 2; continue } + out = out c; i += 1 + } + print out + } + ' "$f" +} + +if [ -n "$SCAN_FILE" ]; then + [ -f "$SCAN_FILE" ] || { echo "BLOCKED: --scan-file target does not exist: $SCAN_FILE" >&2; exit 2; } + hits="$(strip_comments "$SCAN_FILE" | grep -nE -- "$PATTERNS" || true) +$(case "$SCAN_FILE" in + *.idr) strip_comments "$SCAN_FILE" | grep -nE '^[[:space:]]*(partial|%default[[:space:]]+partial)\b' || true ;; + *.fst|*.fstar) strip_comments "$SCAN_FILE" | grep -nE '^[[:space:]]*(assume|admit)\b' || true ;; + esac)" + hits="$(printf '%s' "$hits" | grep -v '^$' || true)" + if [ -n "$hits" ]; then + echo "FAIL: escape hatches in $SCAN_FILE" + printf '%s\n' "$hits" + exit 1 + fi + echo "PASS: no escape hatches in $SCAN_FILE" + exit 0 +fi + +FILES_SCANNED=0 +HITS=0 +REPORT="" +EXEMPTED=0 + +# Per-file scan. Split out so the exemption check and the scan cannot drift +# apart: everything that decides "is this file clean" lives here. +scan_one() { + local f="$1" matches + FILES_SCANNED=$((FILES_SCANNED + 1)) + # `partial` is only a core-tier marker as an Idris2 top-level modifier, and a + # bare `assume` only in F*; both are anchored to keep identifiers and prose out. + matches="$(strip_comments "$f" | grep -nE -- "$PATTERNS" || true) +$(case "$f" in + *.idr) strip_comments "$f" | grep -nE '^[[:space:]]*(partial|%default[[:space:]]+partial)\b' || true ;; + *.fst|*.fstar) strip_comments "$f" | grep -nE '^[[:space:]]*(assume|admit)\b' || true ;; + esac)" + matches="$(printf '%s' "$matches" | grep -v '^$' || true)" + if [ -n "$matches" ]; then + echo " BANNED PATTERN: $f" + printf '%s\n' "$matches" | sed 's/^/ line /' + REPORT+="$f"$'\n'"$matches"$'\n' + HITS=$((HITS + 1)) + else + echo " clean: $f" + fi +} + +IGNORE_FILE=".trusted-base-ignore" +IGNORE_PATTERNS=() +if [ -f "$IGNORE_FILE" ]; then + while IFS= read -r line; do + case "$line" in ''|'#'*) continue ;; esac + IGNORE_PATTERNS+=("$line") + done < <(sed 's/[[:space:]]*$//' "$IGNORE_FILE") +fi + +# Return success if the path contains any non-empty ignore pattern as a literal +# substring, or 1 if none matches. +is_ignored() { + local f="$1" p + for p in "${IGNORE_PATTERNS[@]:-}"; do + [ -z "$p" ] && continue + case "$f" in *"$p"*) return 0 ;; esac + done + return 1 +} + +EXEMPTED=0 + +while IFS= read -r f; do + [ -z "$f" ] && continue + # A path exempted in .trusted-base-ignore is not scanned. The file exists for + # fixtures that must stay detectable and for whole-path exemptions with a + # written rationale; the estate checker reads the same file, so the two gates + # cannot disagree about what is exempt. + if is_ignored "$f"; then EXEMPTED=$((EXEMPTED + 1)); continue; fi + scan_one "$f" +done < <(find $SCAN_DIRS -type f \ + \( -name '*.agda' -o -name '*.lagda' -o -name '*.lagda.*' -o -name '*.idr' \ + -o -name '*.lean' -o -name '*.v' -o -name '*.tla' \ + -o -name '*.fst' -o -name '*.fstar' -o -name '*.hs' -o -name '*.ml' -o -name '*.rs' \) \ + | 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" + write_receipt FAIL "reason: zero files scanned" + exit 1 +fi + +if [ "$HITS" -gt 0 ]; then + echo "FAIL: $HITS file(s) contain banned proof escape hatches" + write_receipt FAIL "files-scanned: $FILES_SCANNED" "files-with-hits: $HITS" "$REPORT" + exit 1 +fi + +# Estate policy docs/TRUSTED-BASE-REDUCTION-POLICY.adoc: a proof-bearing +# repository maintains a proof-debt register, and every escape hatch is one of +# discharged / budgeted / necessary-axiom / debt. This repo tolerates none, so +# the register is expected to be empty — but it must exist, because "no file" +# and "not examined" look identical from outside. The estate checker enforces the +# same rule with the same file, so the two gates agree. +# Only the register itself counts. PROOF-NEEDS is a statement of what the proofs +# need, not a table of dispositions, so it is not accepted as a substitute: a +# fallback that quietly selected it made a deleted register look like a examined +# one. +DEBT_DOC="" +for c in docs/proof-debt.md docs/proof-debt.adoc; do + [ -f "$c" ] && { DEBT_DOC="$c"; break; } +done +if [ -z "$DEBT_DOC" ]; then + echo "FAIL: no proof-debt register (docs/proof-debt.md) — TRUSTED-BASE-REDUCTION-POLICY requires one in a proof-bearing repo" + write_receipt FAIL "reason: no proof-debt register" + exit 1 +fi + +echo "PASS: $FILES_SCANNED proof source(s) scanned, no banned patterns outside comments" +echo " exempted by .trusted-base-ignore: $EXEMPTED; proof-debt register: $DEBT_DOC" +write_receipt PASS "files-scanned: $FILES_SCANNED" "files-with-hits: 0" +exit 0 diff --git a/tests/e2e.sh b/tests/e2e.sh index 7c8cdf7..20a91a2 100755 --- a/tests/e2e.sh +++ b/tests/e2e.sh @@ -120,10 +120,15 @@ echo "" # if ! curl -sf "$VERISIM_URL/health" >/dev/null 2>&1; then # skip_test "VeriSimDB integration" "gateway not available" # else -# STATUS=$(curl -s -o /dev/null -w "%{http_code}" -X POST "$VERISIM_URL/api/v1/hexads" \ +# # The endpoint is /api/v1/octads (8 modal witnesses); "HEXAD" is only the +# # legacy VCL keyword for the octad source, not a route. +# # OctadRequest is deny_unknown_fields: only the fields it declares are +# # accepted (title, body, embedding, types, relationships, tensor, +# # provenance, spatial, metadata). tool/modality/content would 422. +# STATUS=$(curl -s -o /dev/null -w "%{http_code}" -X POST "$VERISIM_URL/api/v1/octads" \ # -H "Content-Type: application/json" \ -# -d '{"tool":"NEXTGEN_TYPING","modality":"document","content":"e2e test"}') -# check_status "hexad POST" "201" "$STATUS" +# -d '{"title":"NEXTGEN_TYPING","body":"e2e test"}') +# check_status "octad POST" "201" "$STATUS" # fi # ═══════════════════════════════════════════════════════════════════════ 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/ControlCommentAxiom.v b/tests/proofs/control/ControlCommentAxiom.v new file mode 100644 index 0000000..4d4bd18 --- /dev/null +++ b/tests/proofs/control/ControlCommentAxiom.v @@ -0,0 +1,9 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* INSTRUMENT CONTROL — CLEAN (must be accepted). + A real Coq comment that mentions Axiom and admit. Nothing here is code, so + refusing this file would be a false positive and would teach people to + distrust the scan rather than the fixture. *) +(* Axiom mentioned_in_a_comment : False. *) +(* And a sentence containing admit, written in prose. *) +Theorem comment_control : forall n : nat, n = n. +Proof. reflexivity. Qed. diff --git a/tests/proofs/control/ControlImportedAxiom.lean b/tests/proofs/control/ControlImportedAxiom.lean new file mode 100644 index 0000000..123a731 --- /dev/null +++ b/tests/proofs/control/ControlImportedAxiom.lean @@ -0,0 +1,7 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- INSTRUMENT CONTROL — NOT an estate proof. +-- Exercises imported-axiom detection (nextgen-typing#131): contains NO banned +-- lexical token, yet `Classical.em` depends on `propext`, `Classical.choice`, +-- and `Quot.sound` from core Init. Must fail check-proofs.sh when `axioms: []` +-- and pass when `proven-with-postulates` names all three axioms. +theorem imported_em (P : Prop) : P ∨ ¬ P := Classical.em P diff --git a/tests/proofs/control/ControlImportedAxiom.v b/tests/proofs/control/ControlImportedAxiom.v new file mode 100644 index 0000000..8d0756e --- /dev/null +++ b/tests/proofs/control/ControlImportedAxiom.v @@ -0,0 +1,9 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* INSTRUMENT CONTROL — NOT an estate proof. + Exercises imported-axiom detection (nextgen-typing#131): contains NO banned + lexical token, yet depends on `Coq.Logic.Classical_Prop.classic` across a + module import. Must fail check-proofs.sh when `axioms: []` and pass when + `proven-with-postulates` names `Coq.Logic.Classical_Prop.classic`. *) +From Coq Require Import Logic.Classical_Prop. +Theorem imported_em : forall P : Prop, P \/ ~ P. +Proof. exact classic. Qed. diff --git a/tests/proofs/control/PlantedAdmit.v b/tests/proofs/control/PlantedAdmit.v new file mode 100644 index 0000000..bbba400 --- /dev/null +++ b/tests/proofs/control/PlantedAdmit.v @@ -0,0 +1,11 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* INSTRUMENT CONTROL — PLANTED VIOLATION (must be rejected). + Coq's `admit.` closes a goal without proving it. It is named in the scanner's + pattern list, and this file exists to show that the pattern can actually reach + it: a trailing \\b after the full stop made the alternative unfirable, so the + scan called this file clean. Not a proof; a control. *) +Theorem planted_admit : forall n : nat, n = n. +Proof. + intros n. + admit. +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/PlantedAxiom.v b/tests/proofs/control/PlantedAxiom.v new file mode 100644 index 0000000..43b00d0 --- /dev/null +++ b/tests/proofs/control/PlantedAxiom.v @@ -0,0 +1,8 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* INSTRUMENT CONTROL — PLANTED VIOLATION (must be rejected). + `Axiom` is a Coq escape hatch in the estate policy's CORE tier + (docs/TRUSTED-BASE-REDUCTION-POLICY.adoc) — a proposition asserted rather + than proved. It is in this file, not in a proof, so that the scanner can be + shown to catch it; the file is exempted by path in .trusted-base-ignore for + that reason. *) +Axiom planted_axiom : False. diff --git a/tests/proofs/control/PlantedLeanBlockText.lean b/tests/proofs/control/PlantedLeanBlockText.lean new file mode 100644 index 0000000..9cb8091 --- /dev/null +++ b/tests/proofs/control/PlantedLeanBlockText.lean @@ -0,0 +1,7 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- INSTRUMENT CONTROL — PLANTED VIOLATION (must be rejected). +-- `(* ... *)` is not a comment in Lean. A scanner that stripped Coq's block +-- delimiters in every language would treat this axiom as commented out and call +-- the file clean, so this fixture keeps the per-language rule honest. +(* Axiom planted_lean_block_text : False *) +theorem planted_lean_block_text : True := trivial diff --git a/tests/proofs/control/PlantedLeanSubtype.lean b/tests/proofs/control/PlantedLeanSubtype.lean new file mode 100644 index 0000000..b2243db --- /dev/null +++ b/tests/proofs/control/PlantedLeanSubtype.lean @@ -0,0 +1,6 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- INSTRUMENT CONTROL — PLANTED VIOLATION (must be rejected). +-- Lean has no `//` comment: `{ n // n = 0 }` is subtype notation. A stripper +-- that treated `//` as a line comment would cut this line before the sorry and +-- report the file clean, so the sorry sits after the subtype on purpose. +def planted_lean_subtype : { n : Nat // n = 0 } × Nat := (⟨0, rfl⟩, sorry) 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..f3e02aa --- /dev/null +++ b/tests/proofs/run-controls.sh @@ -0,0 +1,440 @@ +#!/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. +# +# metadatastician/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. +# +# This script runs the verification in three parts: +# +# 1. run-ledger-controls.sh — 51 controls over RECORDED claims, MANIFEST status, +# reconciliation vocabulary, and comment-aware lexical scanning (no prover +# needed; runs everywhere). +# 2. K1–K5: direct kernel sanity checks (`coqc`/`coqtop`/`lean`) confirming +# the installed toolchains distinguish closed proofs from `Admitted`/`sorry`. +# 3. K6–K15: end-to-end `scripts/check-proofs.sh` compiled-witness assumption +# controls (nextgen-typing#131) exercising `coqchk -silent -o`, generated +# `Print Assumptions` drivers, and generated Lean `#print axioms` probes +# BOTH WAYS — clean witnesses, stdlib-imported axioms (`Classical_Prop.classic`, +# `Classical.em`), cross-module helper `Axiom` and imported `sorryAx`, +# `proven-with-postulates` pass/stale-axiom mismatch, missing declarations, +# clean working-tree staging, and verbatim assumption receipts. +# +# Exit: 0 every control behaved as required; 1 an expectation was violated; +# 2 BLOCKED — a prover tool 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" +CHECK_PROOFS="$ROOT/scripts/check-proofs.sh" +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 "" + +# --- 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. the kernel half: absent means BLOCKED, never a pass ----------------- +echo "=== Kernel & compiled-witness assumption controls (need coqc, coqchk, coqtop, lean) ===" +missing=() +for tool in coqc coqchk coqtop lean jq; do + command -v "$tool" >/dev/null 2>&1 || missing+=("$tool") +done +if [[ "${#missing[@]}" -gt 0 ]]; then + 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 "coqchk: $(coqchk --version 2>&1 | head -1)" +echo "lean: $(lean --version 2>/dev/null | head -1)" +echo "" + +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 "K1. coqc accepts the closed control (Control.v)" +else + 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 "K2. Print Assumptions reports the closed control as closed" +else + 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 + echo " ℹ️ coqc accepts the planted Admitted control — exit code alone is not evidence (informational, not counted)" +else + echo " ℹ️ coqc rejected the planted Admitted control outright (informational, not counted)" +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 "K3. the kernel reported the Admitted control as closed — axiom tracking is blind" +else + ok "K3. the kernel does not report the Admitted control as closed" +fi + +lean_clean="$( cd "$CONTROLS" && lean Control.lean 2>&1 )" +lean_clean_rc=$? +if [[ "$lean_clean_rc" -eq 0 ]] && printf '%s' "$lean_clean" | grep -q "does not depend on any axioms"; then + ok "K4. lean exits 0 and #print axioms reports the closed Lean control as axiom-free" +else + viol "K4. lean exited $lean_clean_rc or #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 "K5. #print axioms exposes sorryAx in the planted Lean control" +else + viol "K5. #print axioms did not expose sorryAx — Lean axiom tracking is blind" + printf '%s\n' "$lean_planted" | sed 's/^/ /' | head -20 +fi + +# --- 3. end-to-end compiled-witness assumption controls (#131) -------------- +write_fixture_ledger() { + # $1=ledger_file $2=prover(rocq|lean4) $3=status $4=artifact $5=support_json $6=decls_json $7=axioms_json + local lfile="$1" prover="$2" st="$3" art="$4" sup_json="$5" decls_json="$6" ax_json="$7" + mkdir -p "$(dirname "$lfile")" + jq -n \ + --arg prover "$prover" \ + --arg st "$st" \ + --arg art "$art" \ + --argjson sup "$sup_json" \ + --argjson decls "$decls_json" \ + --argjson ax "$ax_json" \ + '{ + schema: "hyperpolymath/proof-ledger/1", + theorems: [ + { + id: "CTRL-1", + kind: "theory", + grade: "2i", + statement_formal: { + declarations: [ + { name: "TP-ECHO-1", type: "True" } + ] + }, + legs: [ + { + prover: $prover, + family: "dtt", + status: $st, + route: "re-proved", + reproof_reason: "instrument control", + artifact: $art, + support_files: $sup, + declarations: $decls, + axioms: $ax, + statement_compared: "instrument control" + } + ] + } + ] + }' > "$lfile" +} + +# K6: Rocq clean witness passes check-proofs.sh coq, writes verbatim coqchk + +# Print Assumptions output to receipt, and leaves zero .vo/.glob in source tree. +k6="$WORK/k6" +mkdir -p "$k6/verification/proofs/coq" +cat > "$k6/verification/proofs/coq/CleanWitness.v" <<'EOF' +(* INSTRUMENT CONTROL *) +Theorem tp_echo_1 : True. Proof. exact I. Qed. +Theorem tp_echo_2 : True. Proof. exact I. Qed. +EOF +printf 'verification/proofs/coq|CleanWitness.v|gated|clean witness\n' > "$k6/verification/proofs/coq/MANIFEST" +write_fixture_ledger "$k6/verification/proofs/LEDGER.json" "rocq" "proven" \ + "verification/proofs/coq/CleanWitness.v" "null" '["tp_echo_1","tp_echo_2"]' '[]' +if bash "$CHECK_PROOFS" coq --root "$k6" --receipt "$k6/receipt.txt" >"$k6/out.log" 2>&1 \ + && grep -qF "CONTEXT SUMMARY" "$k6/receipt.txt" \ + && grep -qF "Closed under the global context" "$k6/receipt.txt" \ + && [[ -z "$(find "$k6/verification/proofs/coq" \( -name '*.vo' -o -name '*.glob' \) 2>/dev/null)" ]]; then + ok "K6. check-proofs.sh coq accepts a closed Rocq witness, writes verbatim coqchk + Print Assumptions receipt, and keeps worktree clean" +else + viol "K6. check-proofs.sh coq failed on a closed Rocq witness or omitted verbatim receipt" + sed 's/^/ /' "$k6/out.log" | tail -20 + [[ -f "$k6/receipt.txt" ]] && sed 's/^/ [receipt] /' "$k6/receipt.txt" | tail -25 +fi + +# K7: Rocq witness importing Classical_Prop.classic (lexically clean) is REFUSED when axioms: []. +k7="$WORK/k7" +mkdir -p "$k7/verification/proofs/coq" +cp "$CONTROLS/ControlImportedAxiom.v" "$k7/verification/proofs/coq/ControlImportedAxiom.v" +printf 'verification/proofs/coq|ControlImportedAxiom.v|gated|imported classic\n' > "$k7/verification/proofs/coq/MANIFEST" +write_fixture_ledger "$k7/verification/proofs/LEDGER.json" "rocq" "proven" \ + "verification/proofs/coq/ControlImportedAxiom.v" "null" '["imported_em"]' '[]' +if bash "$CHECK_PROOFS" coq --root "$k7" --receipt "$k7/receipt.txt" >"$k7/out.log" 2>&1; then + viol "K7. check-proofs.sh coq ACCEPTED an undeclared imported stdlib axiom (Classical_Prop.classic)" +elif grep -qF "classic" "$k7/out.log"; then + ok "K7. check-proofs.sh coq refuses an undeclared imported stdlib axiom (Classical_Prop.classic) that lexical scan cannot see" +else + viol "K7. check-proofs.sh coq failed on imported stdlib axiom for the wrong reason" + sed 's/^/ /' "$k7/out.log" | tail -20 +fi + +# K8: Same Rocq witness with proven-with-postulates naming Coq.Logic.Classical_Prop.classic PASSES. +k8="$WORK/k8" +mkdir -p "$k8/verification/proofs/coq" +cp "$CONTROLS/ControlImportedAxiom.v" "$k8/verification/proofs/coq/ControlImportedAxiom.v" +printf 'verification/proofs/coq|ControlImportedAxiom.v|gated|declared classic\n' > "$k8/verification/proofs/coq/MANIFEST" +write_fixture_ledger "$k8/verification/proofs/LEDGER.json" "rocq" "proven-with-postulates" \ + "verification/proofs/coq/ControlImportedAxiom.v" "null" '["imported_em"]' '["Coq.Logic.Classical_Prop.classic"]' +if bash "$CHECK_PROOFS" coq --root "$k8" --receipt "$k8/receipt.txt" >"$k8/out.log" 2>&1 \ + && grep -qF "Coq.Logic.Classical_Prop.classic" "$k8/receipt.txt"; then + ok "K8. check-proofs.sh coq accepts proven-with-postulates when the imported Rocq axiom matches LEDGER.json and records it in receipt" +else + viol "K8. check-proofs.sh coq rejected a properly declared Rocq axiom in proven-with-postulates" + sed 's/^/ /' "$k8/out.log" | tail -20 + [[ -f "$k8/receipt.txt" ]] && sed 's/^/ [receipt] /' "$k8/receipt.txt" | tail -25 +fi + +# K9: Cross-module local helper Axiom imported by a clean surface witness is REFUSED when unrecorded. +k9="$WORK/k9" +mkdir -p "$k9/verification/proofs/coq" +cat > "$k9/verification/proofs/coq/HelperAx.v" <<'EOF' +(* INSTRUMENT CONTROL *) +Axiom helper_ax : True. +EOF +cat > "$k9/verification/proofs/coq/SurfaceClean.v" <<'EOF' +(* INSTRUMENT CONTROL *) +Require Import HelperAx. +Theorem tp_from_helper : True. Proof. exact helper_ax. Qed. +EOF +cat > "$k9/verification/proofs/coq/MANIFEST" <<'EOF' +verification/proofs/coq|HelperAx.v|gated|support module +verification/proofs/coq|SurfaceClean.v|gated|surface witness +EOF +write_fixture_ledger "$k9/verification/proofs/LEDGER.json" "rocq" "proven" \ + "verification/proofs/coq/SurfaceClean.v" '["verification/proofs/coq/HelperAx.v"]' '["tp_from_helper"]' '[]' +if bash "$CHECK_PROOFS" coq --root "$k9" >"$k9/out.log" 2>&1; then + viol "K9. check-proofs.sh coq ACCEPTED a cross-module helper Axiom under axioms: []" +elif grep -qF "helper_ax" "$k9/out.log"; then + ok "K9. check-proofs.sh coq refuses a cross-module helper Axiom imported into a clean surface witness" +else + viol "K9. check-proofs.sh coq failed on cross-module helper Axiom for the wrong reason" + sed 's/^/ /' "$k9/out.log" | tail -20 +fi + +# K10: Axiom-free Rocq witness missing a recorded target declaration is REFUSED by Print Assumptions probe. +k10="$WORK/k10" +mkdir -p "$k10/verification/proofs/coq" +cat > "$k10/verification/proofs/coq/PartialWitness.v" <<'EOF' +(* INSTRUMENT CONTROL *) +Theorem tp_echo_1 : True. Proof. exact I. Qed. +EOF +printf 'verification/proofs/coq|PartialWitness.v|gated|partial witness\n' > "$k10/verification/proofs/coq/MANIFEST" +write_fixture_ledger "$k10/verification/proofs/LEDGER.json" "rocq" "proven" \ + "verification/proofs/coq/PartialWitness.v" "null" '["tp_echo_1","tp_echo_missing"]' '[]' +if bash "$CHECK_PROOFS" coq --root "$k10" >"$k10/out.log" 2>&1; then + viol "K10. check-proofs.sh coq ACCEPTED a witness missing a recorded declaration" +elif grep -qF "Print Assumptions failed" "$k10/out.log"; then + ok "K10. check-proofs.sh coq refuses an axiom-free witness that omits a recorded declaration" +else + viol "K10. check-proofs.sh coq failed on missing declaration for the wrong reason" + sed 's/^/ /' "$k10/out.log" | tail -20 +fi + +# K11: Lean clean witness passes check-proofs.sh lean4, writes verbatim #print axioms receipt, +# and leaves zero .olean files in the source tree. +k11="$WORK/k11" +mkdir -p "$k11/verification/proofs/lean4" +cat > "$k11/verification/proofs/lean4/CleanWitness.lean" <<'EOF' +-- INSTRUMENT CONTROL +theorem tp_echo_1 : True := True.intro +theorem tp_echo_2 : True := True.intro +EOF +printf 'verification/proofs/lean4|CleanWitness.lean|gated|clean witness\n' > "$k11/verification/proofs/lean4/MANIFEST" +write_fixture_ledger "$k11/verification/proofs/LEDGER.json" "lean4" "proven" \ + "verification/proofs/lean4/CleanWitness.lean" "null" '["tp_echo_1","tp_echo_2"]' '[]' +if bash "$CHECK_PROOFS" lean4 --root "$k11" --receipt "$k11/receipt.txt" >"$k11/out.log" 2>&1 \ + && grep -qF "does not depend on any axioms" "$k11/receipt.txt" \ + && [[ -z "$(find "$k11/verification/proofs/lean4" -name '*.olean' 2>/dev/null)" ]]; then + ok "K11. check-proofs.sh lean4 accepts a closed Lean witness, writes verbatim #print axioms receipt, and keeps worktree clean" +else + viol "K11. check-proofs.sh lean4 failed on a closed Lean witness or omitted verbatim receipt" + sed 's/^/ /' "$k11/out.log" | tail -20 + [[ -f "$k11/receipt.txt" ]] && sed 's/^/ [receipt] /' "$k11/receipt.txt" | tail -25 +fi + +# K12: Lean witness using Classical.em (lexically clean) is REFUSED when axioms: []. +k12="$WORK/k12" +mkdir -p "$k12/verification/proofs/lean4" +cp "$CONTROLS/ControlImportedAxiom.lean" "$k12/verification/proofs/lean4/ControlImportedAxiom.lean" +printf 'verification/proofs/lean4|ControlImportedAxiom.lean|gated|imported classical\n' > "$k12/verification/proofs/lean4/MANIFEST" +write_fixture_ledger "$k12/verification/proofs/LEDGER.json" "lean4" "proven" \ + "verification/proofs/lean4/ControlImportedAxiom.lean" "null" '["imported_em"]' '[]' +if bash "$CHECK_PROOFS" lean4 --root "$k12" --receipt "$k12/receipt.txt" >"$k12/out.log" 2>&1; then + viol "K12. check-proofs.sh lean4 ACCEPTED undeclared Classical.em axioms under axioms: []" +elif grep -qF "undeclared axiom" "$k12/out.log"; then + ok "K12. check-proofs.sh lean4 refuses undeclared Classical.em axioms that lexical scan cannot see" +else + viol "K12. check-proofs.sh lean4 failed on Classical.em for the wrong reason" + sed 's/^/ /' "$k12/out.log" | tail -20 +fi + +# K13: Same Lean witness with proven-with-postulates naming propext, Classical.choice, Quot.sound PASSES. +k13="$WORK/k13" +mkdir -p "$k13/verification/proofs/lean4" +cp "$CONTROLS/ControlImportedAxiom.lean" "$k13/verification/proofs/lean4/ControlImportedAxiom.lean" +printf 'verification/proofs/lean4|ControlImportedAxiom.lean|gated|declared classical\n' > "$k13/verification/proofs/lean4/MANIFEST" +write_fixture_ledger "$k13/verification/proofs/LEDGER.json" "lean4" "proven-with-postulates" \ + "verification/proofs/lean4/ControlImportedAxiom.lean" "null" '["imported_em"]' '["propext","Classical.choice","Quot.sound"]' +if bash "$CHECK_PROOFS" lean4 --root "$k13" --receipt "$k13/receipt.txt" >"$k13/out.log" 2>&1 \ + && grep -qF "Classical.choice" "$k13/receipt.txt"; then + ok "K13. check-proofs.sh lean4 accepts proven-with-postulates when all Lean axioms match LEDGER.json and records them in receipt" +else + viol "K13. check-proofs.sh lean4 rejected a properly declared Lean axiom set in proven-with-postulates" + sed 's/^/ /' "$k13/out.log" | tail -20 + [[ -f "$k13/receipt.txt" ]] && sed 's/^/ [receipt] /' "$k13/receipt.txt" | tail -25 +fi + +# K14: Cross-module imported sorry (sorryAx) is REFUSED both when axioms: [] and when axioms: ["sorryAx"]. +k14="$WORK/k14" +mkdir -p "$k14/verification/proofs/lean4" +cat > "$k14/verification/proofs/lean4/HelperSorry.lean" <<'EOF' +-- INSTRUMENT CONTROL +theorem helper_hole : False := sorry +EOF +cat > "$k14/verification/proofs/lean4/SurfaceViaHole.lean" <<'EOF' +-- INSTRUMENT CONTROL +import HelperSorry +theorem surface_claim : False := helper_hole +EOF +cat > "$k14/verification/proofs/lean4/MANIFEST" <<'EOF' +verification/proofs/lean4|HelperSorry.lean|gated|helper with sorry +verification/proofs/lean4|SurfaceViaHole.lean|gated|clean-looking surface +EOF +write_fixture_ledger "$k14/verification/proofs/LEDGER.json" "lean4" "proven" \ + "verification/proofs/lean4/SurfaceViaHole.lean" '["verification/proofs/lean4/HelperSorry.lean"]' '["surface_claim"]' '[]' +bash "$CHECK_PROOFS" lean4 --root "$k14" >"$k14/out-empty.log" 2>&1 +rc_empty=$? +write_fixture_ledger "$k14/verification/proofs/LEDGER.json" "lean4" "proven-with-postulates" \ + "verification/proofs/lean4/SurfaceViaHole.lean" '["verification/proofs/lean4/HelperSorry.lean"]' '["surface_claim"]' '["sorryAx"]' +bash "$CHECK_PROOFS" lean4 --root "$k14" >"$k14/out-listed.log" 2>&1 +rc_listed=$? +if [[ "$rc_empty" -ne 0 && "$rc_listed" -ne 0 ]] \ + && grep -qF "sorryAx" "$k14/out-empty.log" \ + && grep -qF "sorryAx" "$k14/out-listed.log"; then + ok "K14. check-proofs.sh lean4 refuses cross-module imported sorryAx whether unrecorded or listed in .axioms" +else + viol "K14. check-proofs.sh lean4 did not refuse cross-module sorryAx in both modes (rc_empty=$rc_empty, rc_listed=$rc_listed)" + sed 's/^/ /' "$k14/out-empty.log" "$k14/out-listed.log" | tail -20 +fi + +# K15: Stale/padded axioms in .axioms on an actually closed witness are REFUSED in both Rocq and Lean. +k15="$WORK/k15" +mkdir -p "$k15/coq/verification/proofs/coq" "$k15/lean/verification/proofs/lean4" +printf '(* INSTRUMENT CONTROL *)\nTheorem tp_echo_1 : True. Proof. exact I. Qed.\n' > "$k15/coq/verification/proofs/coq/Clean.v" +printf 'verification/proofs/coq|Clean.v|gated|clean\n' > "$k15/coq/verification/proofs/coq/MANIFEST" +write_fixture_ledger "$k15/coq/verification/proofs/LEDGER.json" "rocq" "proven-with-postulates" \ + "verification/proofs/coq/Clean.v" "null" '["tp_echo_1"]' '["Coq.Logic.Classical_Prop.classic"]' +bash "$CHECK_PROOFS" coq --root "$k15/coq" >"$k15/coq.log" 2>&1 +rc_coq_stale=$? + +printf -- '-- INSTRUMENT CONTROL\ntheorem tp_echo_1 : True := True.intro\n' > "$k15/lean/verification/proofs/lean4/Clean.lean" +printf 'verification/proofs/lean4|Clean.lean|gated|clean\n' > "$k15/lean/verification/proofs/lean4/MANIFEST" +write_fixture_ledger "$k15/lean/verification/proofs/LEDGER.json" "lean4" "proven-with-postulates" \ + "verification/proofs/lean4/Clean.lean" "null" '["tp_echo_1"]' '["propext"]' +bash "$CHECK_PROOFS" lean4 --root "$k15/lean" >"$k15/lean.log" 2>&1 +rc_lean_stale=$? + +if [[ "$rc_coq_stale" -ne 0 && "$rc_lean_stale" -ne 0 ]] \ + && grep -qF "stale axioms" "$k15/coq.log" \ + && grep -qF "stale axioms" "$k15/lean.log"; then + ok "K15. check-proofs.sh refuses stale/padded .axioms entries on closed witnesses in both Rocq and Lean" +else + viol "K15. check-proofs.sh accepted stale/padded .axioms entries (coq=$rc_coq_stale, lean=$rc_lean_stale)" + sed 's/^/ /' "$k15/coq.log" "$k15/lean.log" | tail -20 +fi + +# K16: An incomplete Rocq proof closed with `Admitted.` is REFUSED by the kernel +# check even when its full qualified name (`AdmittedWitness.tp_echo_1`) is listed +# in `legs[].axioms` under `proven-with-postulates` (matching Lean's sorryAx ban). +k16="$WORK/k16" +mkdir -p "$k16/verification/proofs/coq" +cat > "$k16/verification/proofs/coq/AdmittedWitness.v" <<'EOF' +(* INSTRUMENT CONTROL *) +Theorem tp_echo_1 : False. +Proof. Admitted. +EOF +cat > "$k16/verification/proofs/coq/MANIFEST" <<'EOF' +verification/proofs/coq|AdmittedWitness.v|gated|admitted control +EOF +write_fixture_ledger "$k16/verification/proofs/LEDGER.json" "rocq" "proven-with-postulates" \ + "verification/proofs/coq/AdmittedWitness.v" "null" '["tp_echo_1"]' '["AdmittedWitness.tp_echo_1"]' +bash "$CHECK_PROOFS" coq --root "$k16" >"$k16/out.log" 2>&1 +rc_k16=$? +if [[ "$rc_k16" -ne 0 ]] && grep -qF "FAIL (assumptions)" "$k16/out.log"; then + ok "K16. check-proofs.sh coq refuses an Admitted theorem even when its full qualified name is listed in .axioms" +else + viol "K16. check-proofs.sh coq accepted an Admitted theorem listed in .axioms (rc=$rc_k16)" + sed 's/^/ /' "$k16/out.log" | tail -20 +fi + +# K17: Multi-file MANIFEST out of dependency order (importer listed before its +# support_files module) is REFUSED with a manifest-order diagnostic. +k17="$WORK/k17" +mkdir -p "$k17/verification/proofs/coq" +cat > "$k17/verification/proofs/coq/HelperClean.v" <<'EOF' +(* INSTRUMENT CONTROL *) +Theorem helper_true : True. Proof. exact I. Qed. +EOF +cat > "$k17/verification/proofs/coq/SurfaceFirst.v" <<'EOF' +(* INSTRUMENT CONTROL *) +Require Import HelperClean. +Theorem surface_true : True. Proof. exact helper_true. Qed. +EOF +cat > "$k17/verification/proofs/coq/MANIFEST" <<'EOF' +verification/proofs/coq|SurfaceFirst.v|gated|importer listed too early +verification/proofs/coq|HelperClean.v|gated|support module listed too late +EOF +write_fixture_ledger "$k17/verification/proofs/LEDGER.json" "rocq" "proven" \ + "verification/proofs/coq/SurfaceFirst.v" '["verification/proofs/coq/HelperClean.v"]' '["surface_true"]' '[]' +bash "$CHECK_PROOFS" coq --root "$k17" >"$k17/out.log" 2>&1 +rc_k17=$? +if [[ "$rc_k17" -ne 0 ]] && grep -qF "FAIL (manifest-order)" "$k17/out.log"; then + ok "K17. check-proofs.sh refuses a multi-file MANIFEST listing an importer before its support_files module" +else + viol "K17. check-proofs.sh did not diagnose out-of-order support_files in MANIFEST (rc=$rc_k17)" + sed 's/^/ /' "$k17/out.log" | tail -20 +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 ($CHECKS kernel & witness expectation(s); the" +echo " ledger-form controls reported their own count above)." +if [[ -n "${GITHUB_ACTIONS:-}" ]]; then + echo "::notice::proof-witness kernel & assumption controls verified both ways (§7, #131): $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..b8310ed --- /dev/null +++ b/tests/proofs/run-ledger-controls.sh @@ -0,0 +1,544 @@ +#!/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 (metadatastician/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