|
| 1 | +#!/bin/sh |
| 2 | +# SPDX-License-Identifier: PMPL-1.0-or-later |
| 3 | +# (MPL-2.0 is automatic legal fallback until PMPL is formally recognised) |
| 4 | +# |
| 5 | +# kernel-guard.sh — enforce the EchoKernel funext-free certificate and |
| 6 | +# keep docs/echo-types/echo-kernel-note.adoc honest. |
| 7 | +# |
| 8 | +# Two independent checks (both must pass; POSIX sh, coreutils only): |
| 9 | +# |
| 10 | +# A. Funext-free certificate (kernel-cone integrity) |
| 11 | +# The in-repo kernel cone is exactly { Echo, EchoKernel }. Assert: |
| 12 | +# * both carry `--safe --without-K` and no safety-relaxing flag; |
| 13 | +# * neither contains a postulate / escape pragma (defence in |
| 14 | +# depth — `--safe` already blocks these, but we want a |
| 15 | +# legible failure, not an Agda backtrace); |
| 16 | +# * neither *imports* Axiom.Extensionality / a funext module |
| 17 | +# (comments mentioning "funext" are fine — only import lines |
| 18 | +# are scanned); |
| 19 | +# * Echo imports zero in-repo modules (stdlib-only root); |
| 20 | +# * EchoKernel's in-repo imports are a subset of { Echo }. |
| 21 | +# The certificate is then: kernel cone = these two files + stdlib, |
| 22 | +# none of which can reach funext. |
| 23 | +# |
| 24 | +# B. Classification-drift lint (reverse dependency on the note) |
| 25 | +# Every proofs/agda/Echo*.agda module must be named in |
| 26 | +# echo-kernel-note.adoc. A new Echo* module that imports outside |
| 27 | +# the kernel (i.e. any derived module) therefore *cannot* land |
| 28 | +# without being classified there — the note stays the SoT. |
| 29 | +# |
| 30 | +# Usage: scripts/kernel-guard.sh (run from repo root; exit 0 = pass) |
| 31 | + |
| 32 | +set -eu |
| 33 | + |
| 34 | +AGDA_DIR="proofs/agda" |
| 35 | +NOTE="docs/echo-types/echo-kernel-note.adoc" |
| 36 | +ECHO_SRC="$AGDA_DIR/Echo.agda" |
| 37 | +KERNEL_SRC="$AGDA_DIR/EchoKernel.agda" |
| 38 | + |
| 39 | +fail() { printf 'kernel-guard: FAIL: %s\n' "$1" >&2; exit 1; } |
| 40 | +note() { printf 'kernel-guard: %s\n' "$1"; } |
| 41 | + |
| 42 | +for f in "$ECHO_SRC" "$KERNEL_SRC" "$NOTE"; do |
| 43 | + [ -f "$f" ] || fail "expected file missing: $f" |
| 44 | +done |
| 45 | + |
| 46 | +# --- Import extraction ------------------------------------------------- |
| 47 | +# Real import lines only (not comments): `open import M ...` / `import M`. |
| 48 | +# Prints the dotted module token following the `import` keyword. |
| 49 | +imports_of() { |
| 50 | + grep -E '^[[:space:]]*(open[[:space:]]+import|import)[[:space:]]' "$1" \ |
| 51 | + | awk '{ for (i = 1; i <= NF; i++) if ($i == "import") { print $(i+1); break } }' |
| 52 | +} |
| 53 | + |
| 54 | +# Is dotted module name an in-repo module (a file under proofs/agda)? |
| 55 | +is_in_repo() { |
| 56 | + _p=$(printf '%s' "$1" | tr '.' '/') |
| 57 | + [ -f "$AGDA_DIR/$_p.agda" ] |
| 58 | +} |
| 59 | + |
| 60 | +in_repo_imports_of() { |
| 61 | + imports_of "$1" | while IFS= read -r m; do |
| 62 | + [ -n "$m" ] || continue |
| 63 | + if is_in_repo "$m"; then printf '%s\n' "$m"; fi |
| 64 | + done |
| 65 | +} |
| 66 | + |
| 67 | +# ====================================================================== |
| 68 | +# Check A — funext-free certificate |
| 69 | +# ====================================================================== |
| 70 | +note "A. funext-free certificate (kernel cone = Echo + EchoKernel)" |
| 71 | + |
| 72 | +for src in "$ECHO_SRC" "$KERNEL_SRC"; do |
| 73 | + head -1 "$src" | grep -q -- '--safe' \ |
| 74 | + || fail "$src: missing --safe in the OPTIONS pragma" |
| 75 | + head -1 "$src" | grep -q -- '--without-K' \ |
| 76 | + || fail "$src: missing --without-K in the OPTIONS pragma" |
| 77 | + |
| 78 | + # No safety-relaxing flag, anywhere. |
| 79 | + if grep -nE -- '--(type-in-type|cubical|rewriting|sized-types|guardedness|injective-type-constructors|no-positivity-check|no-termination-check|allow-unsolved-metas)' "$src" >/dev/null; then |
| 80 | + fail "$src: a safety-relaxing OPTIONS flag is present" |
| 81 | + fi |
| 82 | + |
| 83 | + # No postulate / escape construct in *code* (skip --comment lines). |
| 84 | + if grep -vE '^[[:space:]]*--' "$src" \ |
| 85 | + | grep -nE '(^|[^A-Za-z_])(postulate|believe_me|primTrustMe|primEraseEquality)([^A-Za-z_]|$)|\{-#[[:space:]]*(TERMINATING|NON_TERMINATING|NO_POSITIVITY_CHECK|NO_TERMINATION_CHECK|INJECTIVE)' >/dev/null; then |
| 86 | + fail "$src: postulate/escape construct present (breaks the certificate)" |
| 87 | + fi |
| 88 | + |
| 89 | + # No funext *import* (import lines only — prose is allowed). |
| 90 | + if imports_of "$src" | grep -qiE '(^|\.)Extensionality$|(^|\.)Funext$|Axiom\.Extensionality'; then |
| 91 | + fail "$src: imports a funext/Extensionality module — certificate void" |
| 92 | + fi |
| 93 | +done |
| 94 | + |
| 95 | +# Echo is the stdlib-only root: zero in-repo imports. |
| 96 | +echo_repo_imports=$(in_repo_imports_of "$ECHO_SRC" | sort -u) |
| 97 | +if [ -n "$echo_repo_imports" ]; then |
| 98 | + fail "Echo.agda must import zero in-repo modules; found: $(echo "$echo_repo_imports" | tr '\n' ' ')" |
| 99 | +fi |
| 100 | + |
| 101 | +# EchoKernel's in-repo imports ⊆ { Echo }. |
| 102 | +bad_kernel_imports=$(in_repo_imports_of "$KERNEL_SRC" | sort -u | grep -vx 'Echo' || true) |
| 103 | +if [ -n "$bad_kernel_imports" ]; then |
| 104 | + fail "EchoKernel.agda may only import Echo in-repo; offending: $(echo "$bad_kernel_imports" | tr '\n' ' ')" |
| 105 | +fi |
| 106 | +note " ok: cone is { Echo, EchoKernel }, no funext / postulate / escape" |
| 107 | + |
| 108 | +# ====================================================================== |
| 109 | +# Check B — classification-drift lint |
| 110 | +# ====================================================================== |
| 111 | +note "B. classification-drift lint (every Echo*.agda named in the note)" |
| 112 | + |
| 113 | +missing="" |
| 114 | +for f in "$AGDA_DIR"/Echo*.agda; do |
| 115 | + [ -e "$f" ] || continue |
| 116 | + mod=$(basename "$f" .agda) |
| 117 | + # The note must name the module as a whole identifier (inside a |
| 118 | + # backticked token, a path, or prose — any explicit mention counts; |
| 119 | + # the word-boundary stops EchoGraded matching EchoGradedComonad). |
| 120 | + if ! grep -qE "(^|[^A-Za-z0-9_])$mod([^A-Za-z0-9_]|\$)" "$NOTE"; then |
| 121 | + missing="$missing $mod" |
| 122 | + fi |
| 123 | +done |
| 124 | +if [ -n "$missing" ]; then |
| 125 | + fail "unclassified Echo* module(s) — add to $NOTE (and MAP.adoc tag):$missing" |
| 126 | +fi |
| 127 | + |
| 128 | +# Soft: note names a module that no longer exists (stale entry → warn). |
| 129 | +stale="" |
| 130 | +for mod in $(grep -oE '\`Echo[A-Za-z0-9_]*\`' "$NOTE" | tr -d '\`' | sort -u); do |
| 131 | + [ -f "$AGDA_DIR/$mod.agda" ] || stale="$stale $mod" |
| 132 | +done |
| 133 | +[ -n "$stale" ] && note " warning: note references absent module(s):$stale" |
| 134 | +note " ok: all Echo*.agda modules are classified in the note" |
| 135 | + |
| 136 | +note "PASS — funext-free certificate enforced; classification in sync." |
0 commit comments