Skip to content

Commit 74ae3c7

Browse files
hyperpolymathclaude
andcommitted
ci: also strip Idris2 ||| docstrings in security-envelope badge check
The comment-stripping pre-pass in security-envelope.mjs §4 (believe_me / assert_total / postulate badge accuracy check) handled `--` line comments and `{- ... -}` block comments, but not Idris2 `|||` docstrings. `src/abi/TypedWasm/ABI/Proofs.idr:1427` has a docstring: ||| Total, no `believe_me`, no `assert_total`. …which *describes* the absence of those constructs but was being matched as actual code. False-positive: README badge claims 0 believe_me / 0 assert_total, source files agree, but the docstrings about the absence trip the detector. Add `src.replace(/\|\|\|[^\n]*/g, "")` to the strip pass. Local verification: `node tests/aspect/security-envelope.mjs` reports 10 passed / 0 failed (was 8 / 2). Same root cause shape as the nextgen-languages allowlist fix in the prior commit: aspect-test false positive that masked the real signal. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 402dcfd commit 74ae3c7

1 file changed

Lines changed: 4 additions & 0 deletions

File tree

tests/aspect/security-envelope.mjs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -166,6 +166,10 @@ if (!badgeClaimsZero) {
166166
let src = readFileSync(path, "utf8");
167167
// Strip block comments {- ... -} (non-nested, conservative)
168168
src = src.replace(/\{-[\s\S]*?-\}/g, "");
169+
// Strip Idris2 docstrings ||| ... to end of line (badge claims like
170+
// "Total, no `believe_me`, no `assert_total`" live in docstrings and
171+
// describe what's *absent* — not actual code uses).
172+
src = src.replace(/\|\|\|[^\n]*/g, "");
169173
// Strip line comments -- ... to end of line
170174
src = src.replace(/--[^\n]*/g, "");
171175
for (const tok of Object.keys(offenders)) {

0 commit comments

Comments
 (0)