From 1396dab365117b6ea15451fce8dde9c521a7f61c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:29:15 +0000 Subject: [PATCH 1/6] =?UTF-8?q?ci(proofs):=20run=20the=20Agda=20core=20in?= =?UTF-8?q?=20CI=20under=20the=20PROOF-POLICY=20=C2=A72.1=20invocation?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The reclamation law (R-1..R-6) had no CI in this repository: only typed-wasm's kernel gate checked it, at typed-wasm's pin and Agda 2.6.3. proofs.yml gains an `agda` job that runs scripts/check-agda.sh on Agda 2.6.4.3 (Debian agda-bin, as resource-algebra's proofs.yml), triggered by changes to the Agda sources, rejects, gate scripts and agda-lib. scripts/check-agda.sh runs under `--safe --without-K --cubical-compatible` and scans the import cone (src/ and the pinned resource-algebra sources) for `postulate` outside comments (§8.4.6). The Agda leg of scripts/check-proofs.sh and the agda-lib flags use the same three flags. PROOF-STATUS uses the §5 vocabulary (O-2 ASSUMED: a definition, not a theorem; R-6 TESTED: a refusal) and records Proof Witness Grades: R-1..R-5 PWG-3 only at commits whose `agda` job passed; Rocq and Lean legs OPEN. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/proofs.yml | 36 ++++++++++++++++++++++++++++- PROOF-STATUS.adoc | 45 +++++++++++++++++++++++++++++++----- occupancy-types.agda-lib | 2 +- scripts/check-agda.sh | 11 ++++++++- scripts/check-proofs.sh | 2 +- 5 files changed, 86 insertions(+), 10 deletions(-) diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index e786971..dedf900 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,29 @@ # 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/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/fetch-siblings.sh' + - 'occupancy-types.agda-lib' - 'src/stackcert/**' - 'src/occ/**' - 'tests/run_stackcert.sh' @@ -48,6 +60,28 @@ 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: 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..5f3ecc7 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -11,7 +11,16 @@ 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. Line +# comments and {- -} blocks are stripped first, so a comment that mentions +# the word does not count. +if perl -0ne 's/\{-.*?-\}//gs; s/--[^\n]*//g; $hit = 1 if /\bpostulate\b/; END { exit($hit ? 0 : 1) }' $(find src "$ra" -name "*.agda"); then + echo "ERROR: postulate in the import cone (src/, $ra)" >&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 From 9e7011889b4d12837505bfb8a0b8b274fb1d2203 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:42:20 +0000 Subject: [PATCH 2/6] fix(proofs): scan for postulates in source order, and fail on unreadable input The postulate scan stripped `{- -}` blocks before line comments, so a `{-` inside a `--` comment could hide a following `postulate` up to a `-}` in a later comment. Its regex also mis-handled nested block comments, ignored string literals, split file names on spaces, and passed when perl could not read a file. scripts/scan-postulates.pl reads each file in source order: `--` comments run to the end of the line, `{- -}` comments nest, string and character literals are skipped. It exits 2 on an unreadable file or an empty file list. check-agda.sh passes the import cone to it as a NUL-separated list and refuses an empty cone. tests/scan_postulates_test.sh covers each case (comment-hidden, nested, string, character literal, path with a space, unreadable file, no files) and runs in proofs.yml before the gate. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/proofs.yml | 6 +++ scripts/check-agda.sh | 12 +++--- scripts/scan-postulates.pl | 69 +++++++++++++++++++++++++++++++++++ tests/scan_postulates_test.sh | 28 ++++++++++++++ 4 files changed, 110 insertions(+), 5 deletions(-) create mode 100755 scripts/scan-postulates.pl create mode 100755 tests/scan_postulates_test.sh diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index dedf900..07ad174 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -33,6 +33,8 @@ on: - 'src/OccupancyTypes/**' - 'tests/reject/**' - 'scripts/check-agda.sh' + - 'scripts/scan-postulates.pl' + - 'tests/scan_postulates_test.sh' - 'scripts/fetch-siblings.sh' - 'occupancy-types.agda-lib' - 'src/stackcert/**' @@ -44,6 +46,8 @@ on: - 'src/OccupancyTypes/**' - 'tests/reject/**' - 'scripts/check-agda.sh' + - 'scripts/scan-postulates.pl' + - 'tests/scan_postulates_test.sh' - 'scripts/fetch-siblings.sh' - 'occupancy-types.agda-lib' - 'src/stackcert/**' @@ -79,6 +83,8 @@ jobs: 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: Core proofs and expected rejections (fetches resource-algebra at its pin) run: bash scripts/check-agda.sh diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index 5f3ecc7..a5f6f73 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -13,11 +13,13 @@ fi test -d "$ra" || { echo "ERROR: resource-algebra sources not found at $ra" >&2; exit 1; } 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. Line -# comments and {- -} blocks are stripped first, so a comment that mentions -# the word does not count. -if perl -0ne 's/\{-.*?-\}//gs; s/--[^\n]*//g; $hit = 1 if /\bpostulate\b/; END { exit($hit ? 0 : 1) }' $(find src "$ra" -name "*.agda"); then - echo "ERROR: postulate in the import cone (src/, $ra)" >&2 +# (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. +mapfile -d '' cone < <(find src "$ra" -name '*.agda' -print0) +(( ${#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)" 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 =~ /(? "$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 From 9dccdaa4fb35bb05eded99931506b4e024163fdf Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:45:11 +0000 Subject: [PATCH 3/6] fix(proofs): stop the gate when find cannot list the import cone `mapfile < <(find ...)` ignored find's exit status, so a directory find could not read left a partial cone and the postulate scan could pass without seeing every source. find now writes to a temporary file and its failure stops the gate. Checked as an unprivileged user with an unreadable directory under the cone: the gate stops with "could not list the import cone". The scanner test uses [[ ]] for its comparisons. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- scripts/check-agda.sh | 8 +++++++- tests/scan_postulates_test.sh | 6 +++--- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index a5f6f73..9b87e95 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -16,7 +16,13 @@ flags=(--safe --without-K --cubical-compatible --no-libraries --ignore-interface # (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. -mapfile -d '' cone < <(find src "$ra" -name '*.agda' -print0) +# 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 diff --git a/tests/scan_postulates_test.sh b/tests/scan_postulates_test.sh index f28e77c..348e75b 100755 --- a/tests/scan_postulates_test.sh +++ b/tests/scan_postulates_test.sh @@ -10,7 +10,7 @@ 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 + 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' @@ -22,7 +22,7 @@ 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 +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 +if [[ "$got" -eq 2 ]]; then echo "PASS: no files -> 2"; else echo "FAIL: no files -> $got, want 2"; fail=1; fi exit $fail From fd13dcf8551c3d8d10a10500d0bd6098198e9c21 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:47:38 +0000 Subject: [PATCH 4/6] test(proofs): a find failure stops the Agda gate A stub find on PATH prints one real file of the import cone and exits non-zero, as find does on a directory it cannot read. CI can stage this even when it runs as root, which a chmod 000 directory cannot. The gate must exit non-zero, say it could not list the cone, and not report the postulate scan as passed. Against the previous check-agda.sh (find in a process substitution) the test fails: the scan passed on the partial list. Runs in proofs.yml after the scanner tests. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- .github/workflows/proofs.yml | 4 ++++ tests/check_agda_find_failure_test.sh | 29 +++++++++++++++++++++++++++ 2 files changed, 33 insertions(+) create mode 100755 tests/check_agda_find_failure_test.sh diff --git a/.github/workflows/proofs.yml b/.github/workflows/proofs.yml index 07ad174..9eb7566 100644 --- a/.github/workflows/proofs.yml +++ b/.github/workflows/proofs.yml @@ -35,6 +35,7 @@ on: - '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/**' @@ -48,6 +49,7 @@ on: - '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/**' @@ -85,6 +87,8 @@ jobs: 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 diff --git a/tests/check_agda_find_failure_test.sh b/tests/check_agda_find_failure_test.sh new file mode 100755 index 0000000..333ff20 --- /dev/null +++ b/tests/check_agda_find_failure_test.sh @@ -0,0 +1,29 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# scripts/check-agda.sh must stop when find cannot list the import cone. +# A stub find on PATH prints one real file of the cone and exits non-zero, +# as find does when it meets a directory it cannot read; CI can do this even +# as root. The gate must exit non-zero and must not report the postulate +# scan as passed. Before the fix, the scan passed on the partial list. +set -uo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." +stub=$(mktemp -d); trap 'rm -rf "$stub"' EXIT +cat > "$stub/find" <<'STUB' +#!/usr/bin/env bash +printf 'src/OccupancyTypes/All.agda\0' +echo "find: 'src/locked': Permission denied" >&2 +exit 1 +STUB +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" From e37c0912a09a978917e8aca163b4ae9066d4de13 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:10:36 +0000 Subject: [PATCH 5/6] test(proofs): name the fake find's heredoc FAKE_FIND, not STUB The estate code-hygiene gate (cicd-suite code-hygiene-check) reads a whole-word STUB as an untracked debt marker and failed the Central Estate CI/CD Audit on the heredoc delimiter. Rename it; the test is unchanged and still passes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- tests/check_agda_find_failure_test.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/check_agda_find_failure_test.sh b/tests/check_agda_find_failure_test.sh index 333ff20..563b734 100755 --- a/tests/check_agda_find_failure_test.sh +++ b/tests/check_agda_find_failure_test.sh @@ -8,12 +8,12 @@ set -uo pipefail cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." stub=$(mktemp -d); trap 'rm -rf "$stub"' EXIT -cat > "$stub/find" <<'STUB' +cat > "$stub/find" <<'FAKE_FIND' #!/usr/bin/env bash printf 'src/OccupancyTypes/All.agda\0' echo "find: 'src/locked': Permission denied" >&2 exit 1 -STUB +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" From 14276e2505bb9e14b512f92e977fd6de566cdbf6 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:39:03 +0000 Subject: [PATCH 6/6] docs: regenerate the repository map (PROOF-STATUS, agda-lib rows) estate-rules fails on main because the committed map is stale: the generator now lists PROOF-STATUS.adoc and occupancy-types.agda-lib, which the committed copy lacks. Regenerated with `just repo-map`; the output is identical under the default and C locales. Ported from occupancy-types#19 (b7d12c3). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Y6FD63UrriRBHqmhhEca9t --- docs/architecture/REPOSITORY-MAP.adoc | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index e09598a..5e13913 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -113,6 +113,10 @@ predecessors did. | yes | REUSE licence texts, dual-licence model (code MPL-2.0 / docs CC-BY-SA-4.0) +| `PROOF-STATUS.adoc` +| yes +| repo-local proof inventory with explicit evidence status + | `README.adoc` | yes | - @@ -157,6 +161,10 @@ predecessors did. | yes | pinned toolchains +| `occupancy-types.agda-lib` +| yes +| Agda library descriptor for the occupancy-types proof modules + | `rsr-template-repo_chora.deed` | yes | the repo deed: universal AI entry point; family-7 allocation manifest + ply tree folded in (standards#837 pilot). Filename carries the repo slug (deed dispatch _chora.deed), so repo-init renames it at mint