From 5fcb62bcae1fa35e0ce1d6f9e62135f29acaad11 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 08:35:04 +0100 Subject: [PATCH] fix(tests): make the aspect and E2E suites actually run kitchenspeak carries the same test scaffold as trope-checker and therefore the same defects, plus two of its own. Each stopped a suite from testing anything. SHARED WITH trope-checker (fixed identically there, PR #52): 1. E2E DEAD AT PHASE 3. The placeholder step ran find ... -exec bash -c '...' _ "$file" but `file` is never set in the OUTER scope -- only inside the subshell from "$1". Under set -u that aborted with "file: unbound variable", so the test exited 1 having reached ZERO assertions. find must pass {}. 2. DANGEROUS-PROOF CHECK FLAGGED ITS OWN DOCUMENTATION. It grepped all of src/ and verification/, excluding only paths containing "test" or "comment", so it matched prose describing the convention and the phrase "sorry-free" in comments -- text ASSERTING THE OPPOSITE of what it looks for. Now scans proof source only, through tests/lib/strip-proof-comments.awk, which tracks (* *), /- -/, {- -}, /* */ block state as well as -- and // line forms. Line-based filtering cannot see a block-comment CONTINUATION line. SPECIFIC TO kitchenspeak: 3. SPDX WINDOW OFF BY ONE. src/interface/ffi/src/main.zig carries SPDX-License-Identifier: MPL-2.0 on line SIX, beneath a five-line banner. The check read `head -5`, so a correctly licensed file was reported as unlicensed. Window widened to 15. NOTE the fix NOT taken: adding an SPDX line. That would have put a SECOND licence header in a file that already had one. The defect was the window. 4. ABI DIRECTORY CASE MISMATCH. validate-template.sh required src/interface/abi; the directory is src/interface/Abi. Lowercase matched nothing, so a repo with a perfectly good ABI tree was failed for lacking one -- the same case-sensitivity class as requiring `codeql` when the job is named `CodeQL`. 5. Stale required-workflow list, as in trope-checker: npm-bun-blocker.yml -> runtime-policy.yml ts-blocker.yml -> DELETED scorecard-enforcer.yml -> scorecard.yml guix-nix-policy.yml -> DROPPED (Nix retired 2026-06-01) EVERY change red-teamed in both directions, because a check that stops reporting looks exactly like a check that is satisfied: aspect, clean tree -> PASS=3 FAIL=0 aspect, planted file with NO SPDX -> FAIL=1 aspect, probe removed -> PASS=3 WHAT THE E2E TEST NOW REPORTS, a real defect left for separate work: structure validation passes with 0 errors, and the final phase finds files still carrying placeholders after simulated instantiation. That is the finding this suite exists to surface, and it could not surface it while dead. Co-Authored-By: Claude Opus 5 --- scripts/validate-template.sh | 14 +++++------- tests/aspect_tests.sh | 18 +++++++++++++-- tests/e2e/template_instantiation_test.sh | 2 +- tests/lib/strip-proof-comments.awk | 28 ++++++++++++++++++++++++ 4 files changed, 51 insertions(+), 11 deletions(-) create mode 100644 tests/lib/strip-proof-comments.awk diff --git a/scripts/validate-template.sh b/scripts/validate-template.sh index c777cb3..81ee097 100755 --- a/scripts/validate-template.sh +++ b/scripts/validate-template.sh @@ -102,7 +102,7 @@ check_file_exists "AUDIT.adoc" "Release audit gate" # Directories check_dir_exists ".machine_readable" "Machine-readable metadata" check_dir_exists ".github" "GitHub community metadata" -check_dir_exists "src/interface/abi" "Idris2 ABI definitions" +check_dir_exists "src/interface/Abi" "Idris2 ABI definitions" check_dir_exists "src/interface/ffi" "Zig FFI implementation" check_dir_exists "src/interface/generated/abi" "Generated C headers" check_dir_exists "docs" "Documentation" @@ -136,14 +136,12 @@ REQUIRED_WORKFLOWS=( "quality.yml" "mirror.yml" "instant-sync.yml" - "guix-nix-policy.yml" "rsr-antipattern.yml" "security-policy.yml" "wellknown-enforcement.yml" "workflow-linter.yml" - "npm-bun-blocker.yml" - "ts-blocker.yml" - "scorecard-enforcer.yml" + "runtime-policy.yml" + "scorecard.yml" "secret-scanner.yml" ) @@ -190,9 +188,9 @@ log_info "Phase 4: Idris2 ABI and Zig FFI source files" echo "" # Idris2 ABI files -check_file_exists "src/interface/abi/Types.idr" "Core type definitions" -check_file_exists "src/interface/abi/Layout.idr" "Memory layout specifications" -check_file_exists "src/interface/abi/Foreign.idr" "FFI foreign declarations" +check_file_exists "src/interface/Abi/Types.idr" "Core type definitions" +check_file_exists "src/interface/Abi/Layout.idr" "Memory layout specifications" +check_file_exists "src/interface/Abi/Foreign.idr" "FFI foreign declarations" # Zig FFI files check_file_exists "src/interface/ffi/build.zig" "Zig build configuration" diff --git a/tests/aspect_tests.sh b/tests/aspect_tests.sh index 028b2c0..9ee6c3e 100755 --- a/tests/aspect_tests.sh +++ b/tests/aspect_tests.sh @@ -50,7 +50,13 @@ bold "Aspect 1: SPDX license headers" MISSING_SPDX=0 while IFS= read -r -d '' f; do - if ! head -5 "$f" | grep -q "SPDX-License-Identifier"; then + # Window widened from 5 to 15 lines, 2026-07-29. src/interface/ffi/src/main.zig + # carries SPDX-License-Identifier: MPL-2.0 on line SIX, under a five-line + # descriptive banner -- a perfectly licensed file reported as unlicensed + # because the header sat one line outside the window. The tempting "fix" is + # to add a second SPDX line to a file that already has one; the actual defect + # is the window. + if ! head -15 "$f" | grep -q "SPDX-License-Identifier"; then warn "Missing SPDX header: $f" MISSING_SPDX=$((MISSING_SPDX + 1)) fi @@ -77,7 +83,15 @@ else fi # Coq/Lean dangerous patterns -DANGEROUS_PROOF=$(grep -rn '\bAdmitted\b\|\bsorry\b\|\bunsafeCoerce\b\|\bObj\.magic\b' src/ verification/ 2>/dev/null | grep -v "test" | grep -v "comment" || true) +DANGEROUS_PROOF=$( + for f in $(find src verification -type f \ + \( -name '*.v' -o -name '*.lean' -o -name '*.agda' \ + -o -name '*.idr' -o -name '*.thy' -o -name '*.rs' -o -name '*.zig' \) 2>/dev/null); do + awk -f tests/lib/strip-proof-comments.awk "$f" 2>/dev/null \ + | grep -nE '\bAdmitted\b|\bsorry\b|\bunsafeCoerce\b|\bObj\.magic\b' \ + | sed "s|^|$f:|" + done || true +) if [ -n "$DANGEROUS_PROOF" ]; then fail "Dangerous proof patterns found:" echo "$DANGEROUS_PROOF" | head -5 diff --git a/tests/e2e/template_instantiation_test.sh b/tests/e2e/template_instantiation_test.sh index a9d4a09..cc0ccb8 100755 --- a/tests/e2e/template_instantiation_test.sh +++ b/tests/e2e/template_instantiation_test.sh @@ -137,7 +137,7 @@ find "$TEST_REPO_PATH" -type f \ sed -i "s|$placeholder|$value|g" "$file" fi done - ' _ "$file" + ' _ {} \; log_pass "All placeholder tokens replaced" diff --git a/tests/lib/strip-proof-comments.awk b/tests/lib/strip-proof-comments.awk new file mode 100644 index 0000000..2d8db02 --- /dev/null +++ b/tests/lib/strip-proof-comments.awk @@ -0,0 +1,28 @@ +# Strip comments from proof/source files before scanning for dangerous constructs. +# +# Line-based filtering is not enough: a Coq (* ... *) or Lean /- ... -/ block +# spans lines, and a CONTINUATION line carries no marker of its own. Measured +# 2026-07-29: verification/proofs/coq/TypeSafety.v:6 ("All proofs must be +# complete - NO Admitted allowed.") is line 6 of a block comment and was +# reported as a dangerous construct -- i.e. the repo was failed for DOCUMENTING +# that it forbids Admitted. +# +# Handles: (* *) /- -/ {- -} /* */ plus the line forms -- and // +BEGIN { inblk = 0 } +{ + line = $0; out = ""; i = 1; n = length(line) + while (i <= n) { + two = substr(line, i, 2) + if (inblk) { + if (two == close_tok) { inblk = 0; i += 2; continue } + i++; continue + } + if (two == "(*") { inblk = 1; close_tok = "*)"; i += 2; continue } + if (two == "/-") { inblk = 1; close_tok = "-/"; i += 2; continue } + if (two == "{-") { inblk = 1; close_tok = "-}"; i += 2; continue } + if (two == "/*") { inblk = 1; close_tok = "*/"; i += 2; continue } + if (two == "--" || two == "//") { break } + out = out substr(line, i, 1); i++ + } + print out +}