diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index e786971..9eb7566 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -13,6 +13,8 @@ # stackcert — Lean 4, toolchain pinned by src/stackcert/lean-toolchain. # `bash tests/run_stackcert.sh` = core `#print axioms cert_sound` # + `lake build` + positive fixture + four negative controls. +# agda — the core Agda proofs (R-1..R-6) and expected rejections, +# `bash scripts/check-agda.sh` on Agda 2.6.4.3. # occ-idris — Idris 2 v0.7.0 built from source over Chez Scheme. # `bash src/occ/check-rejections.sh` = the accepts compile and # the four expected-rejection controls are rejected. @@ -21,19 +23,35 @@ # because this repository's Actions allow-list posture is under investigation # (issue #6) and a step referencing a non-allow-listed action dies at startup # with jobs=0 — a gate that cannot start must not be trusted to say "green". -name: Proofs (R0-B Occ, R1 stackcert) +name: Proofs (Agda core, R0-B Occ, R1 stackcert) on: workflow_dispatch: push: branches: [main, master] paths: + - 'src/OccupancyTypes/**' + - 'tests/reject/**' + - 'scripts/check-agda.sh' + - 'scripts/scan-postulates.pl' + - 'tests/scan_postulates_test.sh' + - 'tests/check_agda_find_failure_test.sh' + - 'scripts/fetch-siblings.sh' + - 'occupancy-types.agda-lib' - 'src/stackcert/**' - 'src/occ/**' - 'tests/run_stackcert.sh' - '.github/workflows/proofs.yml' pull_request: paths: + - 'src/OccupancyTypes/**' + - 'tests/reject/**' + - 'scripts/check-agda.sh' + - 'scripts/scan-postulates.pl' + - 'tests/scan_postulates_test.sh' + - 'tests/check_agda_find_failure_test.sh' + - 'scripts/fetch-siblings.sh' + - 'occupancy-types.agda-lib' - 'src/stackcert/**' - 'src/occ/**' - 'tests/run_stackcert.sh' @@ -48,6 +66,32 @@ permissions: contents: read jobs: + agda: + name: Agda core proofs and expected rejections + # The reclamation law (R-1..R-6) had no CI here: typed-wasm's kernel + # gate was the only runner. Same prover as resource-algebra's proofs.yml: + # the Debian agda-bin package at the pinned version, under the + # PROOF-POLICY §2.1 invocation in scripts/check-agda.sh. + runs-on: ubuntu-latest + container: debian:trixie-slim + timeout-minutes: 30 + steps: + - name: Install the pinned prover + run: | + apt-get update + apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2 + - uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + - name: Verify the checked Agda version + run: test "$(agda --version)" = 'Agda version 2.6.4.3' + - name: Postulate scanner tests + run: bash tests/scan_postulates_test.sh + - name: Gate stops when find cannot list the import cone + run: bash tests/check_agda_find_failure_test.sh + - name: Core proofs and expected rejections (fetches resource-algebra at its pin) + run: bash scripts/check-agda.sh + stackcert: name: R1 stackcert (Lean 4) runs-on: ubuntu-latest diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index ea67ed5..bf5ddee 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -1,9 +1,12 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 = occupancy-types — Proof Status -:revdate: 2026-10-12 +:revdate: 2026-11-09 -Statuses: PROVEN / TESTED / ASSUMED / DESIGNED / OPEN. All modules are -`--safe --without-K --no-libraries`, `--double-check`, no postulates. +Statuses are the closed vocabulary of PROOF-POLICY §5 (`metadatastician/standards` +`3-practice/PROOF-POLICY.adoc`): PROVEN / PROVEN-WITH-AXIOMS / TESTED / ASSUMED / +OPEN. Every module checks under the §2.1 invocation, +`--safe --without-K --cubical-compatible`, with `--no-libraries +--ignore-interfaces --double-check` (`scripts/check-agda.sh`); no postulates. Sibling: resource-algebra (same kernel), pinned in `scripts/fetch-siblings.sh`. == The occupancy algebra @@ -12,7 +15,7 @@ Sibling: resource-algebra (same kernel), pinned in `scripts/fetch-siblings.sh`. |=== | ID | Claim | Status | O-1 | The high-water-mark algebra (peak, drift, drift ≤ peak; sequence = `max (peak a) (drift a + peak b)`) is a resource algebra and a dioid; it has no annihilating zero | PROVEN in resource-algebra (`Instances/HWM.agda`); this repo adopts it as its occupancy algebra -| O-2 | It is this repo's own R2–R3 definition | DESIGNED — adopted today from the resource-algebra proposal; the operational model's "live bytes" reading is its intended semantics; a signed drift (terms that consume more than they allocate) is the first extension +| O-2 | It is this repo's own R2–R3 definition | ASSUMED — a definition this repo adopts (`Reclaim.agda` and `Witness.agda` import `Instances.HWM`), not a theorem. That the operational model's "live bytes" reading is its semantics is the v0 → typed bridge, OPEN (see Open); a signed drift (terms that consume more than they allocate) is the first extension |=== == Reclamation at a cut (Reclaim.agda) @@ -25,7 +28,7 @@ Sibling: resource-algebra (same kernel), pinned in `scripts/fetch-siblings.sh`. | R-3 | *Occupancy ≤ cost*: `peak (xs ++ ys) ≤ peak xs + peak ys` | PROVEN (`occupancy≤cost`, `protocol-occupancy≤cost`) | R-4 | Equality iff nothing is reclaimed: with drift = peak the occupancy is the cost (`no-reclaim`); with drift < peak and a non-trivial suffix it is strictly less (`reclaimed`) | PROVEN | R-5 | Two readings of one protocol: occupancy 4, cost 7 (`Witness`) | PROVEN -| R-6 | Reading occupancy as cost, or drift as peak, is refused (`CostIsOccupancy`, `DriftIsPeak`) | PROVEN +| R-6 | Reading occupancy as cost, or drift as peak, is refused (`CostIsOccupancy`, `DriftIsPeak`) | TESTED (`tests/reject/`: each is refused at its invalid declaration by `scripts/check-agda.sh`) |=== == Separation from siblings (criterion 2 of the family bar) @@ -52,4 +55,34 @@ threads (choreographic-types A-3), occupancy has two theorems of its own. typed bridge). * TYPE-CONNECTIONS registration (rows supplied in resource-algebra's cross-repo notes). -* CI: DESIGNED until first green run on the pinned prover. +* CI: `proofs.yml` job `agda` runs `scripts/check-agda.sh` on Agda 2.6.4.3 + (added 2026-11-09). Before, only typed-wasm's kernel gate checked these + proofs, at typed-wasm's pin and Agda 2.6.3. + +== Proof Witness Grades (PROOF-POLICY §8) + +R-1 to R-5 are *theory* (PROOF-POLICY §1): Agda is the source, and §2 owes +a Rocq recheck and a Lean recheck for each. R-6 is a refusal (TESTED), not +a theorem, and is not graded. + +* *Agda leg.* Route: source. Invocation: `scripts/check-agda.sh`, i.e. + `agda --safe --without-K --cubical-compatible --no-libraries + --ignore-interfaces --double-check -i src -i /src`, on + Agda 2.6.4.3 (`proofs.yml`, job `agda`). No standard library. Import cone: + `src/OccupancyTypes/` and resource-algebra's `src/` at the commit + `scripts/fetch-siblings.sh` pins. Axioms (§8.4.6): `--safe` refuses + `postulate`, and `scripts/check-agda.sh` also scans the cone for + `postulate` outside comments, so the postulate count is 0. The receipt is + the `proofs.yml` run on the commit in question. +* *Rocq leg.* OPEN for R-1 to R-5: not started. +* *Lean leg.* OPEN for R-1 to R-5: not started. The Lean files here + (`src/stackcert/`, `verification/proofs/lean4/CostStateSeparation.lean`) + state other theorems (R1 stackcert, the W2.2 separation); none is a + restatement of R-1 to R-5, so none is their Lean leg (§3). + +Grade, derived as §8.4 requires: R-1 to R-5 are `PWG-3` at a commit whose +`proofs.yml` job `agda` passed, and `ungraded` at any commit without that +receipt. Checks before 2026-11-09 used `--safe --without-K` without +`--cubical-compatible`, and ran only in typed-wasm; §2.1 counts them as +historical evidence. None is `PWG-2i` or better, and none is +`+foundation-diverse`. diff --git a/occupancy-types.agda-lib b/occupancy-types.agda-lib index 86e9cb7..c3eec08 100644 --- a/occupancy-types.agda-lib +++ b/occupancy-types.agda-lib @@ -1,4 +1,4 @@ name: occupancy-types include: src depend: resource-algebra -flags: --safe --without-K +flags: --safe --without-K --cubical-compatible diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index fc5de29..9b87e95 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -11,7 +11,24 @@ if [ -z "${RESOURCE_ALGEBRA_SRC:-}" ]; then bash scripts/fetch-siblings.sh fi test -d "$ra" || { echo "ERROR: resource-algebra sources not found at $ra" >&2; exit 1; } -flags=(--safe --without-K --no-libraries --ignore-interfaces --double-check -i src -i "$ra") +flags=(--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -i src -i "$ra") +# PROOF-POLICY §8.4.6: a comment-aware postulate scan of the import cone +# (src/ and the pinned resource-algebra sources), alongside --safe. +# scripts/scan-postulates.pl reads each file in source order (nested block +# comments, line comments, strings) and fails on a file it cannot read. +# find runs to a file, not a process substitution, so its own failure (a +# directory it cannot read) stops the gate instead of leaving a partial cone. +cone_list="$(mktemp)" +trap 'rm -f "$cone_list"' EXIT +find src "$ra" -name '*.agda' -print0 > "$cone_list" \ + || { echo "ERROR: could not list the import cone (src/, $ra)" >&2; exit 1; } +mapfile -d '' cone < "$cone_list" +(( ${#cone[@]} > 0 )) || { echo "ERROR: no Agda sources in the import cone" >&2; exit 1; } +if ! perl scripts/scan-postulates.pl "${cone[@]}"; then + echo "ERROR: postulate in the import cone (src/, $ra), or an unreadable file" >&2 + exit 1 +fi +echo "PASS: no postulate in the import cone (src/, resource-algebra)" "$prover" "${flags[@]}" src/OccupancyTypes/All.agda mkdir -p _build/check-logs shopt -s nullglob diff --git a/scripts/check-proofs.sh b/scripts/check-proofs.sh index 0135dfe..d4b8a05 100755 --- a/scripts/check-proofs.sh +++ b/scripts/check-proofs.sh @@ -82,7 +82,7 @@ check_one() { 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 "$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 diff --git a/scripts/scan-postulates.pl b/scripts/scan-postulates.pl new file mode 100755 index 0000000..83b87c4 --- /dev/null +++ b/scripts/scan-postulates.pl @@ -0,0 +1,69 @@ +#!/usr/bin/env perl +# SPDX-License-Identifier: MPL-2.0 +# scan-postulates.pl FILE... (PROOF-POLICY §8.4.6) +# +# Reports every `postulate` in Agda code, reading each file in source order +# so a comment cannot hide code: `--` comments run to the end of the line, +# `{- -}` comments nest, string and character literals are skipped. A +# `{-` inside a line comment opens nothing, and a `-}` inside a string +# closes nothing. +# +# Exit 0: no postulate. Exit 1: at least one (each printed). Exit 2: a file +# could not be read, or no file was given. A scan that could not read its +# input must never pass. +use strict; +use warnings; + +@ARGV or do { print STDERR "scan-postulates: no files given\n"; exit 2 }; +my $found = 0; +for my $file (@ARGV) { + open(my $fh, '<:raw', $file) + or do { print STDERR "scan-postulates: cannot read $file: $!\n"; exit 2 }; + my $src = do { local $/; <$fh> }; + defined $src + or do { print STDERR "scan-postulates: cannot read $file: $!\n"; exit 2 }; + close $fh; + my ($i, $n, $depth, $line, $code) = (0, length $src, 0, 1, ''); + while ($i < $n) { + my $two = substr($src, $i, 2); + my $c = substr($src, $i, 1); + $line++ if $c eq "\n"; + if ($two eq '{-') { $depth++; $i += 2; next } + if ($depth > 0) { + if ($two eq '-}') { $depth--; $i += 2 } else { $i++ } + $code .= "\n" if $c eq "\n"; + next; + } + if ($two eq '--') { + my $eol = index($src, "\n", $i); + $i = $eol < 0 ? $n : $eol; + next; + } + if ($c eq "'" && $i + 2 < $n && substr($src, $i + 2, 1) eq "'") { + $code .= ' '; $i += 3; next; # a character literal such as '"' + } + if ($c eq '"') { + $i++; + while ($i < $n) { + my $d = substr($src, $i, 1); + if ($d eq '\\') { $i += 2; next } + $i++; + last if $d eq '"'; + $code .= "\n" if $d eq "\n"; + } + $code .= ' '; + next; + } + $code .= $c; + $i++; + } + my $ln = 1; + for my $text (split /\n/, $code, -1) { + if ($text =~ /(? "$stub/find" <<'FAKE_FIND' +#!/usr/bin/env bash +printf 'src/OccupancyTypes/All.agda\0' +echo "find: 'src/locked': Permission denied" >&2 +exit 1 +FAKE_FIND +chmod +x "$stub/find" +# Point at an existing directory so the gate does not fetch the sibling. +export RESOURCE_ALGEBRA_SRC="$PWD/src" +out=$(PATH="$stub:$PATH" bash scripts/check-agda.sh 2>&1); rc=$? +if [[ $rc -eq 0 ]] || grep -q 'PASS: no postulate' <<<"$out"; then + printf 'FAIL: gate passed although find failed (exit %s)\n%s\n' "$rc" "$out" >&2 + exit 1 +fi +if ! grep -q 'could not list the import cone' <<<"$out"; then + printf 'FAIL: gate stopped for another reason (exit %s)\n%s\n' "$rc" "$out" >&2 + exit 1 +fi +echo "PASS: a find failure stops the gate (exit $rc) before the postulate scan passes" diff --git a/tests/scan_postulates_test.sh b/tests/scan_postulates_test.sh new file mode 100755 index 0000000..348e75b --- /dev/null +++ b/tests/scan_postulates_test.sh @@ -0,0 +1,28 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# scripts/scan-postulates.pl reads Agda in source order: a comment cannot +# hide code, a string cannot fake a comment, and an unreadable input fails. +set -uo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." +scan=scripts/scan-postulates.pl +d=$(mktemp -d); trap 'rm -rf "$d"' EXIT +fail=0 +check() { # check WANT-EXIT NAME CONTENT + printf '%b' "$3" > "$d/$2" + perl "$scan" "$d/$2" >/dev/null 2>&1; got=$? + if [[ "$got" -eq "$1" ]]; then echo "PASS: $2 -> $got"; else echo "FAIL: $2 -> $got, want $1"; fail=1; fi +} +check 0 clean.agda 'module A where\nx = 1\n' +check 1 real.agda 'module B where\npostulate p : Set\n' +check 1 linehide.agda 'module C where\n-- {-\npostulate p : Set\n-- -}\n' +check 0 nested.agda 'module D where\n{- {- -} postulate -}\n' +check 0 string.agda 'module E where\ns = "postulate -} {-"\n' +check 0 comment.agda 'module F where\n{-# OPTIONS --safe #-}\n-- postulate\n' +check 0 charlit.agda "module G where\nc = '\"'\n-- \"\nx = 1\n" +mkdir -p "$d/with space" +check 1 'with space/s.agda' 'postulate q : Set\n' +perl "$scan" "$d/missing.agda" >/dev/null 2>&1; got=$? +if [[ "$got" -eq 2 ]]; then echo "PASS: unreadable file -> 2"; else echo "FAIL: unreadable file -> $got, want 2"; fail=1; fi +perl "$scan" >/dev/null 2>&1; got=$? +if [[ "$got" -eq 2 ]]; then echo "PASS: no files -> 2"; else echo "FAIL: no files -> $got, want 2"; fail=1; fi +exit $fail