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..1513396 --- /dev/null +++ b/.github/workflows/proof-ci.yml @@ -0,0 +1,458 @@ +# 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) and +# audited for form here. The lane does not re-derive it. +# * §2: that statement must be rechecked in Rocq AND Lean — transported +# through Dedukti/Lambdapi or re-proved by hand, with the statement +# comparison recorded and no Mathlib. Those are the legs this lane +# examines. BOTH ARE CURRENTLY OPEN: no witness exists, so the lane +# compiles zero recheck modules and the gate prints the gap as a +# `POLICY GAP` line on every run. +# * §5/§6: status is the closed vocabulary (open | argued | tested-only | +# proven-with-postulates | proven); a grade must be supported by the legs +# behind it; axioms are tracked (`Print Assumptions`, `#print axioms`), not +# assumed; receipts are pinned to a commit. +# * §7: a gate must be verified BOTH WAYS. tests/proofs/run-controls.sh runs +# two halves: run-ledger-controls.sh (15 controls, no prover needed) plants +# a grade with no leg behind it, contradictory history, an unjustified +# regression, flag drift, statement drift, a missing escape-hatch mechanism, +# an unrecorded flag deviation, a non-existent anchor, a ghost source file +# and an unclaimed witness on disk — each must be refused for the stated +# reason, while an honest evidenced regression must still pass; and the +# kernel half requires a closed Rocq/Lean proof to be accepted with +# `Print Assumptions` / `#print axioms` reporting it closed, and the +# `Admitted` / `sorry` controls NOT to be reported closed. +# +# The Grade 3 claim itself is substantiated rather than labelled: the ledger +# names the Agda declarations that carry the statement (and the gate re-reads +# their types out of the file), records the flags in force (read out of the +# proof files and out of the instrument, not copied by hand), records the +# escape-hatch mechanism, and records the deviation from the configurations +# mathesis §5 names parenthetically. Any drift in those fails the run. +# +# What this lane refuses, and why it exists: before it, `just proof-check-all` +# was never invoked by CI and each recipe ended in +# `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 "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; } + 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 + bash tests/proofs/run-controls.sh 2>&1 | tee "$RUNNER_TEMP/proof-controls.log" + cp "$RUNNER_TEMP/proof-controls.log" "$PROOF_RECEIPT_DIR/controls.txt" + + # The CI target: audit the ledger, then compile every recheck leg the + # ledger declares. XP-1 declares Rocq and Lean 4, both `open`, so these + # compile zero modules — and the ledger gate refuses any claim that they + # compiled. The gate's receipt (census + POLICY GAP lines) is written to + # $PROOF_RECEIPT_DIR/ledger.txt by `just proof-ledger-check`. + - name: Ledger audit + declared recheck legs (Rocq, Lean 4) + run: | + set -o pipefail + just proof-witness-check 2>&1 | tee "$RUNNER_TEMP/proof-witness-check.log" + + # "PASS" from a per-prover step must never be reachable with nothing + # compiled. scripts/check-proofs.sh is the estate instrument and is used + # verbatim, so its zero-module case is closed around it here: if the ledger + # records a proven Rocq/Lean leg, that leg's MANIFEST must list at least one + # gated module. With no proven legs (today) zero compiled modules is the + # honest count and is stated as such, not glossed as a pass. + - name: Zero-work guard (a proven leg cannot compile nothing) + run: | + set -euo pipefail + LEDGER=verification/proofs/LEDGER.json + bad=0 + while IFS= read -r leg; do + [ -z "$leg" ] && continue + case "$leg" in + rocq|coq) dir=coq; prover="Rocq" ;; + lean4|lean) dir=lean4; prover="Lean 4" ;; + *) continue ;; + esac + gated="$(awk -F'|' '/^[[:space:]]*#/ || NF < 3 { next } $3 == "gated" { c++ } END { print c+0 }' "verification/proofs/$dir/MANIFEST")" + echo "$prover: ledger records a proven leg; $dir/MANIFEST lists $gated gated module(s)" + if [ "$gated" -lt 1 ]; then + echo "::error::zero-work: the ledger records a proven $prover leg but verification/proofs/$dir/MANIFEST lists no gated module" + bad=1 + fi + done < <(jq -r '.theorems[].legs[]? | select(.status == "proven" or .status == "proven-with-postulates") | .prover' "$LEDGER" | sort -u) + if [ "$bad" -ne 0 ]; then exit 1; fi + echo "no recheck leg is recorded proven, so zero compiled recheck modules is the honest count — not a pass" + + # The Agda SOURCE leg. PROOF-POLICY §1 makes Agda the source of truth; the + # ledger records it at a pinned commit and the audit checks that record. + # Typechecking it here keeps the recorded status true rather than assumed. + - name: Agda source leg (recorded in the ledger, re-typechecked here) + run: | + set -o pipefail + just proof-check-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 + LOG="$RUNNER_TEMP/proof-witness-check.log" + if [ ! -f "$LOG" ]; then + echo "::error::proof-witness-check produced no log (an earlier step failed); see the step logs above" + exit 0 + fi + # GitHub caps annotations at 10 per step and each annotation is + # single-line, so emit ONE annotation carrying the last 100 lines + # newline-encoded (%0A). That keeps the failing prover's own + # diagnostic attached to the check run, not buried in runner logs. + PAYLOAD="$(grep -vE '^[[:space:]]*$' "$LOG" | tail -n 100 | head -c 60000 | sed ':a;N;$!ba;s/\n/%0A/g')" + echo "::error::proof-witness-check failed. Log tail:%0A${PAYLOAD}" + { + echo "### proof-witness-check log tail (failure diagnostics)" + echo '```' + tail -n 60 "$LOG" + echo '```' + } >> "$GITHUB_STEP_SUMMARY" + + - 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..ba4b671 --- /dev/null +++ b/.trusted-base-ignore @@ -0,0 +1,12 @@ +# 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..d68c2ee 100644 --- a/Justfile +++ b/Justfile @@ -1335,147 +1335,149 @@ 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 examines the §2 recheck legs only — Rocq and Lean — +# and audits verification/proofs/LEDGER.json, which records every leg, its route, +# its axioms and the exact commit of the receipt. The Agda source leg is recorded +# and audited for form; it is not re-run in CI. +# +# No silent skips 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. +# Fatal if coqc is absent: a missing prover is never a skip. +# +# Compile the declared Rocq recheck witnesses (missing coqc = fatal) +proof-check-coq: + @bash scripts/check-proofs.sh coq + +# Compile Lean 4 recheck witnesses per verification/proofs/lean4/MANIFEST. +# Fatal if lean is absent: a missing prover is never a skip. +# +# Compile the declared Lean 4 recheck witnesses (missing lean = fatal) proof-check-lean4: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Lean4 proofs ===" - 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 -# Check Agda proofs +# Re-typecheck the Agda SOURCE leg locally. Not part of the CI target: under +# PROOF-POLICY §1 the ledger records this leg, CI audits the record. Needs the +# nextgen-typing, standard-library, echo-types and absolute-zero libraries +# registered in /libraries + defaults. +# +# Re-typecheck the Agda source leg locally (needs registered libraries) proof-check-agda: - #!/usr/bin/env bash - set -euo pipefail - echo "=== Checking Agda proofs ===" - 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 -# 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 -# 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 EXACTLY ONE proven recheck leg (Rocq or Lean), with its route\n" + + " (transported through Dedukti/Lambdapi, or re-proved by hand), the statement\n" + + " comparison against the Agda declarations, and the axiom query recorded.\n" + + " Proven today: 0. That is the whole of the work between here and 2i." + elif .grade == "3" then + " INCONSISTENT: a leg is proven while the grade still says 3 — the gate should\n" + + " have refused this ledger. Re-record the grade." + elif .grade == "2i" then + " grade 2ii needs TWO proven legs and one of them outside the DTT/CIC family.\n" + + " Agda, Rocq and Lean are all DTT, so a Rocq+Lean pair cannot reach 2ii: it needs\n" + + " a non-DTT leg such as Isabelle/HOL (proven non-DTT legs today: \(non_dtt))." + elif .grade == "2ii" then + " grade 1 needs the statement checked through a verified checker API — AXLE for\n" + + " Lean, coq-lsp for Rocq, isabelle-server for Isabelle — with the receipt recorded." + else + " grade 1 recorded: nothing higher is defined by the model." + end)), + "", + "Nothing here is a percentage: grades are recorded, never averaged (mathesis §6)."' "$LEDGER" # ═══════════════════════════════════════════════════════════════════════════════ # SESSION MANAGEMENT (THIN BINDINGS TO CENTRAL STANDARDS) diff --git a/PROOF-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..b0877fb 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -3,51 +3,574 @@ ____ Coordination repo. The only proofs tracked here are *cross-project* proofs (spanning ≥2 constituent repos). Single-project proof status is -tracked in the owning repos. Requirements: `+PROOF-NEEDS.md+`. +tracked in the owning repos. Requirements: `+PROOF-NEEDS.adoc+`. ____ -=== Summary +The machine-readable record of every proof is +`+verification/proofs/LEDGER.json+`. This page is a *summary of that ledger*; +where the two disagree the ledger is authoritative and +`+just proof-ledger-check+` fails. Nothing here is a percentage, a confidence +estimate, or a count of "done" work: mathesis §6 requires the exact form — +Open / Claimed, the grade, the axiom list, and the commit the receipt was taken +at. -[cols=",,,,",options="header",] +=== The one theorem + +[cols="10%,12%,9%,26%,21%,22%",options="header",] |=== -|Category |Total |Done |In Progress |Remaining -|Cross-project (XP) |1 |1 |0 |0 -|*Total* |*1* |*1* |*0* |*0* +|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 |=== -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+`). +`+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. + +Three 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.* -=== Proofs Present +* `+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 +---- -[width="100%",cols="12%,15%,15%,17%,13%,28%",options="header",] +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 +`+estate-mathematical-architecture+` **defines the grades** (§5) and the record +discipline (§6, §11); `+metadatastician/standards+` `+3-practice/PROOF-POLICY.adoc+` +(pinned at `+46ee1832+`, owner ruling 2026-10-26, amended 2026-11-01) says **where +a proof lives and how it is rechecked**. the standards document does not define the rungs +themselves, and mathesis does not say how a translation leg is rechecked; where +their examples differ, the standards document governs, because it +is the later owner ruling and §7 says only an owner ruling amends it. + +[cols="14%,34%,36%,16%",options="header",] |=== -|ID |Proof |Spans |Prover |File |Verified By -|XP-1 |Pipeline information-loss = echo-types fibers |echo-types ↔ -affinescript ↔ typed-wasm |Agda (`+--safe --without-K+`) -|`+verification/proofs/agda/EchoTyping.agda+` -|`+agda Verification.agda+` +|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 +retained 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+` |Exactly *one* independent system (Rocq or Lean) carrying the same +statement: `+transported+` through Dedukti/Lambdapi, or `+re-proved+` by hand, +with the statement comparison and the axiom query recorded; no Mathlib +|*0 of 2 legs.* This is the whole of the remaining work, and it is a proving +job — not a bookkeeping one. `+just proof-grade+` prints the same delta. + +|`+2ii+` |Two proven legs *and* one outside the DTT/CIC family (e.g. +Isabelle/HOL). Rocq + Lean cannot reach this rung: they are the same family as +Agda, so a translation between them proves interoperability, not independence +|Unreachable with the current legs, by construction + +|`+1+` |The statement machine-checked through a verified checker API — AXLE for +Lean, coq-lsp for Rocq, isabelle-server for Isabelle — with its receipt recorded +|Not wired up; nothing here claims it +|=== + +=== Moving XP-1 up one rung (to `+2i+`): the runbook + +. Pick *one* leg. Two half-done legs are worth less than one done leg: `+2i+` + needs exactly one. +. Write the witness under `+verification/proofs/coq/+` or + `+verification/proofs/lean4/+`, with *no Mathlib* and no axiom of convenience. +. Register it in that prover's `+MANIFEST+` as `+gated+`. +. Record the leg in `+LEDGER.json+`: `+status+`, `+route+` (`+transported+` or + `+re-proved+`), `+artifact+`, `+axioms+` from `+Print Assumptions+` (Rocq) or + `+#print axioms+` (Lean), `+statement_compared+` against the declarations in + `+statement_formal+`, and the receipt commit. +. Record the promotion in `+history+`: `+{target: "grade", from: "3", to: "2i", + evidence: , ...}+`. The gate requires the last history entry for a target + to equal that target's current value, so history cannot be rewritten. +. Register the file in both registries (`+[verification].allowed-proofs+` and + `+ALLOWED_PROOFS+`) and run `+just proof-witness-check+`. + +What will *not* be accepted as reaching `+2i+`: a compiler exit code with no +axiom query (Rocq accepts `+Admitted+`, Lean accepts `+sorry+`); a leg marked +`+proven+` with no artifact, no MANIFEST entry, no route, no statement +comparison or no axiom list; a Mathlib import; or a grade raised while the legs +stay `+open+`. Each of those is a control in `+tests/proofs/+`. + +=== Regressions and supersession + +mathesis §6 requires a proof's history to say when it is superseded or +regresses. The ledger's `+history+` array is checked rather than decorative: + +* every entry needs a date, a target (`+grade+` or a prover), a `+from+`, a + `+to+` and the evidence that showed the transition; +* the *last* entry for a target must equal that target's current value — a + downgrade cannot be quietly applied, and a record cannot be quietly dropped; +* a transition to a weaker state (a grade moving down the ladder, or a leg + returning to `+open+`) must carry a `+reason+`. + +An honest, evidenced regression passes: the rule cuts both ways, and +`+tests/proofs/run-ledger-controls.sh+` control 7 pins that. + +=== The recheck obligation, stated plainly + +`+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",] +|=== +|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. +|=== + +[[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. + +**Stated plainly, because the alternative is a reader assuming more than is +here:** the lane *compiles* the witnesses a MANIFEST gates and *audits the axiom +lists the ledger records*; the kernel-level axiom query (`+Print Assumptions+`, +`+#print axioms+`) is exercised today on the control fixtures in +`+tests/proofs/`+ and, when a leg is proven, on the declarations the ledger +names. It is not yet run against every compiled module, so an axiom *imported* +from another module rather than declared in the artifact would not be caught by +the compile step. That gap is recorded as issue #131 with the shape of the fix +(per-module `+coqchk -o+` / a generated `+Print Assumptions+` driver, and a Lean +probe that runs `+#print axioms+` per recorded declaration), and it is named here +rather than left to be discovered. + +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) +|=== + +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+` (15 controls, no prover +needed) plants a grade with no leg behind it, a history whose last entry +contradicts the ledger, a regression with no reason, flag drift, statement +drift, a missing escape-hatch mechanism, an unrecorded deviation, an anchor that +does not exist, a source file that is not on disk, and a witness on disk that no +ledger row claims — each must be refused *for the stated reason* — and confirms +that an honest, evidenced regression is still accepted. The kernel half feeds +the compilers a closed Rocq proof and a closed Lean proof (must be accepted, +`+Print Assumptions+` / `+#print axioms+` must report them closed and +axiom-free), plus `+Admitted+` and `+sorry+` controls the kernels must *not* +report as closed. A control that stops failing is a broken instrument, and the +run goes red. Where `+coqc+` or `+lean+` is absent the kernel half reports +**BLOCKED**, never a pass. + +|`+just proof-grade+` +|Prints, per theorem, what the recorded grade rests on and the exact delta to +the next rung, computed from the ledger — so "how far off `+2i+` are we?" is +answered by the record rather than by prose. + +|`+just proof-enrolment+` +(`+scripts/check-proof-enrolment.sh+`) +|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 2 (BLOCKED) when proofs for that prover are enrolled but the prover is +absent; exits 1 on any typecheck 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 |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..41512a3 --- /dev/null +++ b/docs/decisions/D-2026-11-01-policy-reconciliation.adoc @@ -0,0 +1,187 @@ +// 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` `estate-mathematical-architecture` +|*The grade ladder*: §5 Grade 3 / 2i / 2ii / 1 and the prover-family caveat; §6 +record discipline, axiom tracking, `Superseded`/`Regressed`; §11 no inflation. +|`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. + +== 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..7f0e977 --- /dev/null +++ b/docs/proof-debt.md @@ -0,0 +1,71 @@ + + + +# 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 `.source.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. 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..12b7d4a 100755 --- a/scripts/check-coordination-boundary.sh +++ b/scripts/check-coordination-boundary.sh @@ -45,7 +45,12 @@ is_allowed_proof() { if [ -d verification/proofs ]; then while IFS= read -r f; do case "$f" in - *.a2ml | *.adoc | *.md | *.gitkeep) continue ;; # docs/metadata are fine + # Proof METADATA is not a proof: the per-prover MANIFEST (the compile + # gate's input, scripts/check-proofs.sh) and LEDGER.json (the policy + # ledger, audited by scripts/check-proof-ledger.sh) are tracked here + # deliberately, but they are not hosted proofs. + *.a2ml | *.adoc | *.md | *.gitkeep) continue ;; + */MANIFEST | */LEDGER.json) continue ;; esac if ! is_allowed_proof "$f"; then err "Proof outside the cross-project allowlist: $f @@ -60,7 +65,30 @@ fi # --- 3. No implementation/proof source languages outside verification/proofs/ # The coordination repo holds docs, .a2ml, k9/ncl, shell, and CI — not Rust, # Zig, Idris, Agda, Lean, Coq, Isabelle, Haskell, or OCaml source. +# Narrow, self-policing exception: tests/proofs/control/ holds the both-ways +# controls for the proof gate (PROOF-POLICY §7). They exist to be pointed at the +# instrument, not to prove anything, so the allowance is deliberately tiny and +# each fixture must police itself: +# * it must declare what it is in a header comment ("INSTRUMENT CONTROL"), and +# * it must stay <= 20 lines. A fixture that grows into a real proof has +# escaped the boundary, which is precisely what this check exists to stop. +INSTRUMENT_MARKER='INSTRUMENT CONTROL' +INSTRUMENT_MAX_LINES=20 while IFS= read -r f; do + case "$f" in + tests/proofs/control/*) + if grep -qF "$INSTRUMENT_MARKER" "$f" \ + && [ "$(wc -l < "$f")" -le "$INSTRUMENT_MAX_LINES" ]; then + continue + fi + err "Instrument fixture outside its narrow allowance: $f + tests/proofs/control/ may hold only tiny self-declaring controls: a header + comment containing '$INSTRUMENT_MARKER' and at most $INSTRUMENT_MAX_LINES + lines. Anything larger, or undeclared, is proof code escaping the + coordination boundary — host it in the owning repo instead." + continue + ;; + esac err "Implementation source outside the coordination boundary: $f Compiler / kernel / proof code belongs in the owning project repo (see $ROUTE)." done < <( diff --git a/scripts/check-proof-enrolment.sh b/scripts/check-proof-enrolment.sh new file mode 100755 index 0000000..b4fbf4c --- /dev/null +++ b/scripts/check-proof-enrolment.sh @@ -0,0 +1,369 @@ +#!/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) 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" \ + | grep -Ev '\.(a2ml|adoc|md)$|(^|/)\.gitkeep$' \ + | grep -Ev '(^|/)MANIFEST$|(^|/)LEDGER\.json$' \ + | 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..e091d8c --- /dev/null +++ b/scripts/check-proof-ledger.sh @@ -0,0 +1,1115 @@ +#!/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. Block comments {- -} and (* *) and line comments +# -- and // are stripped before matching, with line numbers preserved. +# --------------------------------------------------------------------------- +scan_escape_hatches() { + # $1 = file. Prints "line:token:text" for each real hit. + # + # 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 "$(dirname "$0")/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"}' + +# --- 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. +jq -r ' + .theorems[] | + [ .id, + .kind, + (.grade | tostring), + ([.legs[]?.prover] | join(",")), + ([.legs[]? | select(.status != "open")] | length), + ([.legs[]? | select(.status == "proven" or .status == "proven-with-postulates")] | length) + ] | map(tostring) | join("\u001f")' "$LEDGER" > /tmp/proof-ledger-rows.$$.tsv +trap 'rm -f /tmp/proof-ledger-rows.$$.tsv' EXIT + +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) + if [ "$proven" -ne 1 ]; then + fail "$tid: grade 2i requires exactly one proven recheck leg, ledger records $proven (mathesis §5)" + fi + ;; + 2ii) + if [ "$proven" -lt 2 ]; then + fail "$tid: grade 2ii requires two proven legs, ledger records $proven (mathesis §5)" + fi + non_dtt="$(jq -r --argjson fam "$FAMILIES" --arg id "$tid" ' + [ .theorems[] | select(.id == $id) | .legs[]? + | select(.status == "proven" or .status == "proven-with-postulates") + | select($fam[.prover // ""] != null and $fam[.prover] != "dtt") ] | length' "$LEDGER")" + if [ "${non_dtt:-0}" -lt 1 ]; then + fail "$tid: grade 2ii needs one proven leg outside the DTT/CIC family (mathesis §5 — Agda, Rocq and Lean are the same family); none recorded" + fi + ;; + 1) + api="$(jq -r --arg id "$tid" ' + [ .theorems[] | select(.id == $id) | .legs[]? + | select(.status == "proven" or .status == "proven-with-postulates") + | .api_receipt.api // empty ] | length' "$LEDGER")" + if [ "${api:-0}" -lt 1 ]; then + fail "$tid: grade 1 requires a verified-checker API receipt (AXLE, coq-lsp, isabelle-server — mathesis §5); none recorded" + fi + ;; + esac + + if [ "$claimed" -gt 0 ]; then + GAPS+=("$tid: $claimed leg(s) carry a non-open status and MUST compile in this lane") + fi +done < /tmp/proof-ledger-rows.$$.tsv + +# --- 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) every source file must exist + IFS=',' read -r -a src_files <<< "$files_csv" + for f in "${src_files[@]}"; do + [ -z "$f" ] && continue + [ -f "$f" ] || fail "$tid: source file recorded but missing on disk: $f" + done + + # (c) flags: what the instrument passes, what the files declare, and the + # union the ledger claims must agree. Drift here silently changes what a + # Grade 3 claim means. + actual_file_opts="$(file_agda_options "${src_files[@]}")" + if [ "$rec_cli" != "$AGDA_CLI_FLAGS" ]; then + fail "$tid: flags drift — scripts/check-proofs.sh invokes 'agda ${AGDA_CLI_FLAGS}' but the ledger records CLI '${rec_cli:-}'" + fi + if [ "$rec_file_opts" != "$actual_file_opts" ]; then + fail "$tid: flags drift — the proof files declare '${actual_file_opts:-}' in {-# OPTIONS #-} but the ledger records '${rec_file_opts:-}'" + fi + effective_expected="$(printf '%s %s\n' "$actual_file_opts" "$AGDA_CLI_FLAGS" | tr ' ' '\n' | grep -v '^$' | sort -u | tr '\n' ' ' | sed 's/ *$//')" + if [ "$rec_effective" != "$effective_expected" ]; then + fail "$tid: effective safety flags recorded as '${rec_effective:-}' but the files+instrument actually apply '${effective_expected:-}'" + fi + case " $rec_effective " in + *" --safe "*) ;; + *) fail "$tid: '--safe' is not in the effective flags — postulates and other escape hatches are not ruled out, so the grade is unsupported (mathesis §5)" ;; + esac + + # (d) mathesis §5 names the Grade 3 configurations parenthetically + # (--safe --erasure, or Full --cubical). If the flags in force are neither, + # the deviation must be recorded rather than glossed over. + grade3_named=0 + case " $rec_effective " in *" --erasure "*) grade3_named=1 ;; esac + case " $rec_effective " in + *" --cubical "*) + case " $rec_effective " in + *" --cubical-compatible "*) ;; + *) grade3_named=1 ;; + esac + ;; + esac + if [ "$grade3_named" -eq 0 ]; then + deviation="$( + jq -r --arg id "$tid" '.theorems[] | select(.id == $id) | .grade_deviation // ""' "$LEDGER" + )" + if [ -z "${deviation// }" ]; then + fail "$tid: the flags in force ('$rec_effective') are neither of the configurations mathesis §5 names for grade 3 (--safe --erasure, or Full --cubical) — record the deviation in .grade_deviation instead of paraphrasing the policy" + fi + fi + + # (e) the statement must rest on named declarations that exist. A grade + # anchored to a file rather than a theorem is the "proof inflation" mathesis + # §11 rejects. + if [ -z "${anchor_ids// }" ]; then + fail "$tid: no .statement_anchor — a grade must point at the named declarations that carry the statement, not at a file" + else + IFS=',' read -r -a anchors <<< "$anchor_ids" + for a in "${anchors[@]}"; do + [ -z "${a// }" ] && continue + hit=0 + for f in "${src_files[@]}"; do + [ -f "$f" ] || continue + grep -qE "^[[:space:]]*${a//./\\.}[[:space:]]*:" "$f" && hit=1 + done + [ "$hit" -eq 1 ] || fail "$tid: statement anchor '$a' is not declared in any recorded source file (looked in: $files_csv)" + done + fi + + # (e2) PROOF-POLICY §2 needs a statement comparison between the Agda source + # and any recheck leg. That is impossible if the Agda statement is only prose, + # so each recorded declaration's TYPE must still be in the file, whitespace- + # normalised. When the Agda statement moves, this record has to move with it. + while IFS=$'\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 + *"$norm_type"*) found=1 ;; + esac + done + if [ "$found" -eq 0 ]; then + fail "$tid: statement drifted — statement_formal.$decl_name records the type + '$norm_type' + which no recorded source file contains any more. If the Agda statement + changed, re-record it here (and re-check any leg that was compared against + it) — PROOF-POLICY §2's statement comparison is void otherwise." + fi + done < <(jq -r --arg id "$tid" ' + .theorems[] | select(.id == $id) | .statement_formal.declarations[]? | + [ (.name // ""), (.type // "") ] | 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, +# 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 ! grep -vE '^[[:space:]]*(#|$)' "$mdir/MANIFEST" | grep -qF "|$(basename "$artifact")|"; then + fail "$tid/$prover: $artifact is not listed in $mdir/MANIFEST (unlisted witness)" + fi + fi + + # PROOF-POLICY §2.3: record the route; §2.1: without a statement comparison + # the leg is ASSUMED (argued), not PROVEN. + 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) + fail "$tid/$prover: '$status' requires a statement comparison (PROOF-POLICY §2.1); without it the leg is 'argued'" ;; + esac + fi + + # §5: axioms are named, and only proven-with-postulates may have any. + axiom_count="$(jq -r --arg id "$tid" --arg p "$prover" ' + [ .theorems[] | select(.id == $id) | .legs[]? | select(.prover == $p) + | (.axioms // []) | length ] | .[0] // -1' "$LEDGER")" + if [ "${axiom_count:--1}" -lt 0 ]; then + fail "$tid/$prover: 'axioms' must be recorded as a list (empty when none) — mathesis §6 axiom tracking" + elif [ "$status" = "proven" ] && [ "$axiom_count" -ne 0 ]; then + fail "$tid/$prover: status 'proven' but $axiom_count axiom(s) recorded; that is 'proven-with-postulates' (§5)" + elif [ "$status" = "proven-with-postulates" ] && [ "$axiom_count" -eq 0 ]; then + fail "$tid/$prover: status 'proven-with-postulates' with an empty axiom list (§5: list the axioms)" + fi + + # §2: no Mathlib. A proof that needs a large external library is a + # dependency, not a proof the estate owns. + if [ "$prover" = "lean4" ] && grep -qE '^[[:space:]]*import[[:space:]]+Mathlib' "$artifact"; then + fail "$tid/$prover: $artifact imports Mathlib, which PROOF-POLICY §2 forbids" + fi +done < <(jq -r ' + .theorems[] as $t | $t.legs[]? | 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 ------- +declare -A DECLARED_AXIOMS=() +while IFS=$'\x1f' read -r tid _p axioms; do + [ -z "$tid" ] && continue + case "$axioms" in + ""|null) continue ;; + esac + IFS=',' read -r -a ax_list <<<"$axioms" + for a in "${ax_list[@]}"; do + [ -n "$a" ] && DECLARED_AXIOMS["$a"]=1 + done +done < <(jq -r '.theorems[] as $t | $t.legs[]? | [ $t.id, .prover, ((.axioms // []) | join(",")) ] | map(tostring) | join("\u001f")' "$LEDGER") + +scan_one() { + local f="$1" hits + hits="$(scan_escape_hatches "$f")" + if [ -n "$hits" ]; then + fail "escape hatch in $f: +$(printf '%s\n' "$hits" | sed 's/^/ line /')" + fi + local ax + ax="$(scan_declared_axioms "$f")" + if [ -n "$ax" ]; then + while IFS= read -r line; do + [ -z "$line" ] && continue + name="$(printf '%s\n' "$line" | sed -E 's/^[0-9]+:[[:space:]]*(Axiom|Parameter|Conjecture|axiom)[[:space:]]+([A-Za-z0-9_′]+).*/\2/')" + if [ -z "${DECLARED_AXIOMS[$name]:-}" ]; then + fail "undeclared axiom in $f:$line — PROOF-POLICY §5 requires every axiom to be named in the ledger (proven-with-postulates)" + fi + done <<<"$ax" + fi +} + +if git rev-parse --is-inside-work-tree >/dev/null 2>&1; then + PROOF_FILES="$(git ls-files -- "$PROOFS_DIR" | grep -E '\.(agda|lagda|idr|v|lean|tla)$' | sort)" +else + PROOF_FILES="$(find "$PROOFS_DIR" -type f \( -name '*.agda' -o -name '*.idr' -o -name '*.v' -o -name '*.lean' -o -name '*.tla' \) 2>/dev/null | sort)" +fi +scanned=0 +while IFS= read -r f; do + [ -z "$f" ] && continue + scanned=$((scanned + 1)) + scan_one "$f" +done <<<"$PROOF_FILES" + +if [ "$scanned" -eq 0 ]; then + fail "zero-work: no proof source or witness was scanned under $PROOFS_DIR" +fi + +# --- 7. witnesses on disk must be claimed in the ledger ---------------------- +# Enumerated the same way as section 6: `git ls-files` inside a work tree, a +# plain `find` otherwise. Using git alone here would make the check silently +# vacuous in an exported tree (no .git) — a null check that reports OK, which is +# the exact failure mode the estate instrument exists to prevent. +list_witnesses() { # $1 = prover dir under $PROOFS_DIR, $2 = extension + if git rev-parse --is-inside-work-tree >/dev/null 2>&1; then + git ls-files -- "$PROOFS_DIR/$1" 2>/dev/null | grep -E "\.$2\$" | sort + else + find "$PROOFS_DIR/$1" -type f -name "*.$2" 2>/dev/null | sort + fi +} +LEDGER_ARTIFACTS="$(jq -r '.theorems[].legs[]?.artifact // empty' "$LEDGER" | sort -u)" +for dir in coq lean4; do + ext=v; [ "$dir" = "lean4" ] && ext=lean + while IFS= read -r f; do + [ -z "$f" ] && continue + if ! printf '%s\n' "$LEDGER_ARTIFACTS" | grep -Fxq -- "$f"; then + fail "witness on disk is not claimed in the ledger: $f + Add a leg row with artifact '$f' (route, axioms, statement comparison) — an + unclaimed witness is exactly the silent-drift case mathesis §11 rejects." + fi + done < <(list_witnesses "$dir" "$ext") +done + +# --- 8. cross-project registry: manifest <-> boundary allowlist <-> disk ----- +normalize_list_entries() { + sed 's/#.*//' | tr -d "\"' \t\r" | sed 's/,*$//' | grep -v '^$' | sort +} + +if [ -f "$MANIFEST_SOURCE" ] && [ -f "$BOUNDARY_SCRIPT" ]; then + manifest_list="$(awk ' + /^\[/ { in_section = ($0 ~ /^\[verification\]/); next } + in_section && /^[[:space:]]*allowed-proofs[[:space:]]*=[[:space:]]*\[/ { in_list = 1; next } + in_list && /^[[:space:]]*\][[:space:]]*$/ { in_list = 0; next } + in_list { print } + ' "$MANIFEST_SOURCE" | normalize_list_entries)" + + boundary_list="$(awk ' + /^ALLOWED_PROOFS=\(/ { in_list = 1; next } + in_list && /^\)/ { in_list = 0; next } + in_list { print } + ' "$BOUNDARY_SCRIPT" | normalize_list_entries)" + + [ -n "$manifest_list" ] || fail "cross-project registry is empty in $MANIFEST_SOURCE" + [ -n "$boundary_list" ] || fail "cross-project allowlist is empty in $BOUNDARY_SCRIPT" + + while IFS= read -r entry; do + [ -z "$entry" ] && continue + grep -Fxq -- "$entry" <<<"$boundary_list" \ + || fail "registry drift: '$entry' is in $MANIFEST_SOURCE but not in ALLOWED_PROOFS of $BOUNDARY_SCRIPT" + [ -e "$entry" ] || fail "stale registry entry: '$entry' is registered but absent from disk" + done <<<"$manifest_list" + + while IFS= read -r entry; do + [ -z "$entry" ] && continue + grep -Fxq -- "$entry" <<<"$manifest_list" \ + || fail "registry drift: '$entry' is in ALLOWED_PROOFS of $BOUNDARY_SCRIPT but not in $MANIFEST_SOURCE" + done <<<"$boundary_list" + + # Proof sources on disk must be registered (the anti-drift rule). + while IFS= read -r f; do + [ -z "$f" ] && continue + grep -Fxq -- "$f" <<<"$manifest_list" \ + || fail "unlisted proof source: $f + Register it in [verification].allowed-proofs of $MANIFEST_SOURCE AND in + ALLOWED_PROOFS of $BOUNDARY_SCRIPT." + done <<<"$PROOF_FILES" +else + fail "cross-project registry inputs missing ($MANIFEST_SOURCE / $BOUNDARY_SCRIPT)" +fi + +# --- 9. documentation must not claim a grade the ledger does not support ----- +if [ -f "$DOCS_STATUS" ]; then + grep -qF 'LEDGER.json' "$DOCS_STATUS" \ + || fail "$DOCS_STATUS does not point at the proof ledger (LEDGER.json): status prose is unanchored" + while IFS= read -r tid; do + [ -z "$tid" ] && continue + grep -qF -- "$tid" "$DOCS_STATUS" \ + || fail "$DOCS_STATUS does not mention theorem '$tid' from the ledger" + done < <(jq -r '.theorems[].id' "$LEDGER" | sort -u) + + # 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 + mkdir -p "$(dirname "$RECEIPT")" 2>/dev/null || true + { + echo "proof-ledger receipt" + echo "generated: $(date -u +%Y-%m-%dT%H:%M:%SZ)" + echo "commit: ${GITHUB_SHA:-$(git rev-parse HEAD 2>/dev/null || echo unknown)}" + echo "runner: ${RUNNER_NAME:-local}/${RUNNER_OS:-$(uname -s)}" + echo "status: $status" + echo "policy: $(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 "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..ed4d7a7 --- /dev/null +++ b/scripts/check-proofs.sh @@ -0,0 +1,217 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# check-proofs.sh prover in: idris2 | lean4 | agda | coq +# +# The single source of truth for "do the proofs in this repo compile?". +# build/just/proofs.just calls this (`just proof-check-`), and CI should +# too, so a green local run and a green CI run mean the same thing. +# +# It replaces four separate "checks that could not fail" that let non-compiling +# proofs sit in estate repos for months while every status file said "proved": +# +# 1. `command -v || { echo SKIP; exit 0; }` — a MISSING TOOLCHAIN +# reported success. A gate that cannot run must never report OK: it +# manufactures false confidence, which is worse than having no gate. +# 2. ` --check ` — Idris2 (and friends) derive the +# expected module name from the path they are handed, so a module checked +# from the wrong directory fails on a name mismatch rather than its real +# errors, and verdicts invert. Every module here is checked from its own +# SOURCE ROOT (declared in the MANIFEST). +# 3. Path-filtered CI that only looked at one directory — nothing checked the +# rest. Here, a proof file present on disk but absent from the MANIFEST is +# an ERROR, so new proofs are gated by default, not by remembering. +# 4. `idris2 --check X && ok` — `idris2 --check` EXITS 0 ON A MISSING IMPORT +# (verified against 0.7.0) while printing `Error: ...`. Testing the exit +# code alone is unsound; for idris2 we require exit 0 AND no `Error:` line. +# +# They share one shape: a null check that emits reassuring text. If you extend +# this script, the test to apply is not "does it pass?" but "have I watched it +# fail?". +# +# CONVENTION: proofs live under verification/proofs// ; the MANIFEST for +# a prover is verification/proofs//MANIFEST, one entry per line: +# +# ||gated|quarantine| +# +# source-root : directory the prover is invoked from, chosen so the module's +# declared name matches its path (getting this wrong is hole #2). +# gated : MUST compile. A failure fails this script and CI. +# quarantine : known-broken, tracked in docs/status/ROADMAP.adoc. Must CONTINUE to fail; +# if one starts compiling the script fails and tells you to +# promote it, so the list cannot rot into a permanent excuse. +# +# Blank lines and lines starting with # are ignored. +# +# Exit: 0 = every gated module compiles AND every quarantined module still fails +# AND every proof file on disk is listed; 1 = otherwise; 2 = misuse. + +set -euo pipefail + +PROVER="${1:-}" +case "$PROVER" in + idris2|lean4|agda|coq) ;; + *) echo "usage: $(basename "$0") " >&2; exit 2 ;; +esac + +# This script lives in /scripts/ ; run everything from the repo root. +cd "$(dirname "${BASH_SOURCE[0]}")/.." +ROOT="$PWD" +PROOF_DIR="verification/proofs/$PROVER" +MANIFEST_FILE="$PROOF_DIR/MANIFEST" + +# --- per-prover configuration ------------------------------------------------- +# CMD : executable that must be on PATH (absent => FAIL, never skip). +# EXT : file extension, for the "unlisted proof" coverage scan. +# ERROR_RE : if non-empty, output must not match it even when the exit code is 0. +# Only idris2 needs this (its --check exits 0 on a missing import); +# for lean4 it is a harmless belt-and-braces guard. +case "$PROVER" in + idris2) CMD=idris2; EXT=idr; ERROR_RE='^Error:' ;; + lean4) CMD=lean; EXT=lean; ERROR_RE='error:' ;; + agda) CMD=agda; EXT=agda; ERROR_RE='' ;; + coq) CMD=coqc; EXT=v; ERROR_RE='' ;; +esac + +check_one() { + # $1 source-root (rel to ROOT), $2 module (rel to source-root). + # Sets LAST_OUT to the tool output on failure; returns 0 iff the module compiles. + local root="$1" rel="$2" out rc + set +e + case "$PROVER" in + idris2) out="$(cd "$ROOT/$root" && idris2 --check "$rel" 2>&1)"; rc=$? ;; + lean4) out="$(cd "$ROOT/$root" && lean "$rel" 2>&1)"; rc=$? ;; + agda) out="$(cd "$ROOT/$root" && agda --safe --without-K --cubical-compatible "$rel" 2>&1)"; rc=$? ;; + coq) out="$(cd "$ROOT/$root" && coqc "$rel" 2>&1)"; rc=$? ;; + esac + set -e + if [ "$rc" -eq 0 ] && { [ -z "$ERROR_RE" ] || ! grep -qE "$ERROR_RE" <<<"$out"; }; then + LAST_OUT=""; return 0 + fi + LAST_OUT="$out"; return 1 +} + +echo "=== $PROVER proof check ===" + +# --- a repo with proofs but no MANIFEST is itself a failure ------------------- +if [ ! -f "$MANIFEST_FILE" ]; then + if [ -d "$PROOF_DIR" ] && [ -n "$(find "$PROOF_DIR" -name "*.$EXT" 2>/dev/null)" ]; then + echo "FAIL: $PROOF_DIR contains .$EXT proofs but has no MANIFEST." >&2 + echo " Create $MANIFEST_FILE listing each as 'gated' or 'quarantine'." >&2 + exit 1 + fi + echo "no $PROOF_DIR/*.$EXT proofs and no MANIFEST — nothing to check." + exit 0 +fi + +# --- nothing to check is not the same as a missing toolchain ----------------- +# The probe used to run first, so `just proof-check-idris2` demanded Idris2 even +# in a repository with no Idris proof and no idris2 MANIFEST. That made the +# advertised proof-check-all target impossible on a machine that has no reason +# to carry every prover, and taught people to read a red run as "expected". +# The order is now: is there any work? then: is the tool here? A toolchain that +# is missing while work exists is still fatal, never a skip. +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_DIR" -name "*.$EXT" -not -path '*/build/*' 2>/dev/null | head -1)" +if [ "$manifest_entries" -eq 0 ] && [ -z "$disk_proofs" ]; then + echo "no $PROOF_DIR/*.$EXT proofs and no MANIFEST entries — nothing to check." + exit 0 +fi + +# --- toolchain: absent means FAIL, never skip --------------------------------- +if ! command -v "$CMD" >/dev/null 2>&1; then + { + echo "FAIL: '$CMD' not found on PATH." + echo + echo "This is deliberately fatal. The previous recipe did 'exit 0' here with" + echo "\"SKIP: $CMD not installed\", so every $PROVER proof reported green on any" + echo "machine that could not check it. Install the $PROVER toolchain, or run" + echo "this in CI where the workflow installs it." + } >&2 + exit 1 +fi +"$CMD" --version 2>/dev/null | head -1 || true +echo + +fails=0 +unexpected_pass=0 +listed_tmp="$(mktemp)" +trap 'rm -f "$listed_tmp"' EXIT + +while IFS='|' read -r root rel status note; do + # skip blank lines and comments + [ -z "${root// }" ] && continue + case "${root#"${root%%[![:space:]]*}"}" in \#*) continue ;; esac + printf ' %-30s %-24s ' "$root" "$rel" + echo "$root/$rel" >>"$listed_tmp" + # Only the two documented tokens are statuses. Everything else used to fall + # into the `else` branch and be read as quarantine, so a misspelt 'gatde' made + # a broken module an *expected* failure and the run stayed green. + case "$status" in + gated|quarantine) ;; + *) + 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 check_one "$root" "$rel"; then + if [ "$status" = gated ]; then + echo "PASS" + else + echo "PASS -- UNEXPECTED (quarantined module now compiles)" + echo " Promote '$rel' to 'gated' in $MANIFEST_FILE and update docs/status/ROADMAP.adoc." + unexpected_pass=$((unexpected_pass + 1)) + fi + else + if [ "$status" = gated ]; then + echo "FAIL" + printf '%s\n' "${LAST_OUT//$'\n'/$'\n '}" | sed '1s/^/ /' + fails=$((fails + 1)) + else + echo "fail (quarantined, expected)" + [ -n "${note// }" ] && echo " reason:$note" + fi + fi +done < "$MANIFEST_FILE" + +# --- coverage: every proof on disk must be listed ----------------------------- +# The anti-recurrence rule: proofs went unchecked for months because nothing +# forced them onto anyone's list. A file absent from the MANIFEST is an error. +echo +echo "=== manifest coverage ($PROOF_DIR) ===" +listed="$(sort -u "$listed_tmp")" +found="$(cd "$ROOT" && find "$PROOF_DIR" -name "*.$EXT" -not -path '*/build/*' 2>/dev/null | sort)" +unlisted="$(comm -13 <(printf '%s\n' "$listed") <(printf '%s\n' "$found") || true)" +missing="$(comm -23 <(printf '%s\n' "$listed") <(printf '%s\n' "$found") || true)" + +if [ -n "${unlisted//[[:space:]]/}" ]; then + echo "FAIL: .$EXT proofs on disk but absent from $MANIFEST_FILE:" + printf ' %s\n' $unlisted + echo " List each as 'gated' or 'quarantine'; new proofs are gated by default." + fails=$((fails + 1)) +fi +if [ -n "${missing//[[:space:]]/}" ]; then + echo "FAIL: MANIFEST lists modules that do not exist (stale entries):" + printf ' %s\n' $missing + fails=$((fails + 1)) +fi +[ -z "${unlisted//[[:space:]]/}${missing//[[:space:]]/}" ] && \ + echo " all $(printf '%s\n' "$found" | grep -c .) .$EXT file(s) accounted for" + +echo +if [ "$fails" -gt 0 ] || [ "$unexpected_pass" -gt 0 ]; then + echo "RESULT: FAIL ($fails failure(s), $unexpected_pass unexpected pass(es))" + exit 1 +fi +echo "RESULT: PASS -- gated modules compile; quarantined modules still fail as recorded" diff --git a/scripts/proof-scan-dangerous.sh b/scripts/proof-scan-dangerous.sh new file mode 100755 index 0000000..dd78f5e --- /dev/null +++ b/scripts/proof-scan-dangerous.sh @@ -0,0 +1,296 @@ +#!/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. +# * An unknown extension is scanned RAW. Stripping nothing can only produce a +# false positive, which someone fixes; guessing a syntax can hide an escape +# hatch, which nobody sees again. +# +# 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 + +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 '*.idr' \ + -o -name '*.lean' -o -name '*.v' -o -name '*.tla' \) \ + | sed 's|^\./||' | sort) + +echo "" +if [ "$FILES_SCANNED" -eq 0 ]; then + echo "FAIL: no proof sources scanned — refusing to report a clean scan on zero work" + 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/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..969bbf7 --- /dev/null +++ b/tests/proofs/run-controls.sh @@ -0,0 +1,133 @@ +#!/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 whole verification in two halves: +# +# 1. run-ledger-controls.sh — 15 controls over the RECORDED claims (grades, +# statements, flags, history, unclaimed witnesses, escape hatches). No +# prover needed: that half runs everywhere. +# 2. the kernel controls below — a closed Rocq proof and a closed Lean proof +# must be accepted by their kernels, and Print Assumptions / #print axioms +# must report them closed and axiom-free. This half exists because a +# compiler's exit code is not evidence of a closed proof: Rocq accepts +# `Admitted` and Lean accepts `sorry` with status 0. +# +# The fixtures live in tests/proofs/control/. They are NOT estate proofs and +# they sit outside verification/proofs/, so no census, ledger or catalogue ever +# counts them as mathematics. +# +# Exit: 0 every control behaved as required; 1 an expectation was violated; +# 2 BLOCKED — a prover the controls need is not installed here. +# 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" +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/3. the kernel half: absent means BLOCKED, never a pass --------------- +echo "=== Kernel controls (need coqc, coqtop and lean) ===" +missing=() +for tool in coqc coqtop lean; do + command -v "$tool" >/dev/null 2>&1 || missing+=("$tool") +done +if [ "${#missing[@]}" -gt 0 ]; then + echo "BLOCKED: the kernel controls need ${missing[*]} on PATH, and the instrument" + echo " cannot be shown to work without them. This is NOT a pass (PROOF-POLICY §6)." + exit 2 +fi +echo "coqc: $(coqc --version 2>/dev/null | head -1)" +echo "lean: $(lean --version 2>/dev/null | head -1)" +echo "" + +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 + # Coq accepts Admitted at compile time; that is exactly why an exit code is + # not evidence. The scan must catch it (control L2), and the kernel must not + # report it closed (K3). + 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 )" +if printf '%s' "$lean_clean" | grep -q "does not depend on any axioms"; then + ok "K4. #print axioms reports the closed Lean control as axiom-free" +else + viol "K4. #print axioms did not report the closed Lean control as axiom-free" + printf '%s\n' "$lean_clean" | sed 's/^/ /' | head -20 +fi +lean_planted="$( cd "$CONTROLS" && lean PlantedSorry.lean 2>&1 )" +if printf '%s' "$lean_planted" | grep -q "sorryAx"; then + ok "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 + +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 expectation(s); the ledger-form" +echo " controls reported their own count above)." +# Machine-readable evidence: annotations are retrievable through the check-run +# API, so "how many expectations actually ran?" is answerable without the raw +# runner log (which GitHub does not serve to every client). +if [ -n "${GITHUB_ACTIONS:-}" ]; then + echo "::notice::proof-witness kernel controls verified both ways (§7): $CHECKS expectation(s), 0 violations, coqc $(coqc --version | head -1), lean $(lean --version | head -1)" +fi +exit 0 diff --git a/tests/proofs/run-ledger-controls.sh b/tests/proofs/run-ledger-controls.sh new file mode 100755 index 0000000..2c4271c --- /dev/null +++ b/tests/proofs/run-ledger-controls.sh @@ -0,0 +1,393 @@ +#!/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