Skip to content

Commit 0a35a28

Browse files
author
Claude
committed
fix(ci): make ECHIDNA dangerous-pattern scan ignore comments
The scan grepped for literal tokens (believe_me, assert_total, assert_smaller, unsafePerformIO) anywhere in *.idr — including inside comments. So legitimate documentation (e.g. a proof's doc string noting it needs 'no assert_smaller') would fail the gate. Strip doc (|||) and line (--) comments before matching, so only genuine code uses count. Also drop the deleted modules/ path. Verified locally: clean tree scans 0; a pattern named in a ||| or -- comment is ignored while a real use in code is still caught and fails the gate.
1 parent 4a17409 commit 0a35a28

1 file changed

Lines changed: 20 additions & 11 deletions

File tree

.github/workflows/echidna-validation.yml

Lines changed: 20 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -31,17 +31,26 @@ jobs:
3131

3232
- name: Dangerous pattern scan (Idris2)
3333
run: |
34-
echo "=== Idris2 Dangerous Pattern Scan ==="
34+
echo "=== Idris2 Dangerous Pattern Scan (code only; comments excluded) ==="
3535
ISSUES=0
3636
for pattern in "believe_me" "assert_total" "assert_smaller" "unsafePerformIO"; do
37-
FOUND=$(grep -rn "$pattern" ochrance-core/ modules/ src/abi/ --include="*.idr" 2>/dev/null | wc -l || echo 0)
38-
if [ "$FOUND" -gt 0 ]; then
39-
echo "CRITICAL: Found $FOUND instances of '$pattern'"
40-
grep -rn "$pattern" ochrance-core/ modules/ src/abi/ --include="*.idr" 2>/dev/null
41-
ISSUES=$((ISSUES + FOUND))
37+
# Strip doc comments (||| ...) and line comments (-- ...) before
38+
# matching, so documentation that merely names a pattern is not
39+
# flagged: only genuine uses in code count. Without this, a doc
40+
# string like "this proof needs no assert_smaller" would fail the gate.
41+
MATCHES=""
42+
for f in $(find ochrance-core/ src/abi/ -name "*.idr" 2>/dev/null); do
43+
M=$(sed -e 's/|||.*$//' -e 's/--.*$//' "$f" | grep -n "$pattern" | sed "s|^|$f:|" || true)
44+
[ -n "$M" ] && MATCHES="${MATCHES}${M}"$'\n'
45+
done
46+
N=$(printf '%s' "$MATCHES" | grep -c . || true)
47+
if [ "$N" -gt 0 ]; then
48+
echo "CRITICAL: Found $N use(s) of '$pattern' in code:"
49+
printf '%s\n' "$MATCHES"
50+
ISSUES=$((ISSUES + N))
4251
fi
4352
done
44-
echo "Total dangerous patterns: $ISSUES"
53+
echo "Total dangerous patterns (in code): $ISSUES"
4554
echo "dangerous_count=$ISSUES" >> $GITHUB_OUTPUT
4655
4756
if [ "$ISSUES" -gt 0 ]; then
@@ -53,7 +62,7 @@ jobs:
5362
run: |
5463
echo "=== Totality Enforcement ==="
5564
MISSING=0
56-
for f in $(find ochrance-core/ modules/ src/abi/ -name "*.idr" 2>/dev/null); do
65+
for f in $(find ochrance-core/ src/abi/ -name "*.idr" 2>/dev/null); do
5766
if ! grep -q "%default total" "$f"; then
5867
echo "WARNING: $f missing '%default total'"
5968
MISSING=$((MISSING + 1))
@@ -67,11 +76,11 @@ jobs:
6776
- name: Partial function check
6877
run: |
6978
echo "=== Partial Function Check ==="
70-
PARTIAL=$(grep -rn "^partial" ochrance-core/ modules/ src/abi/ --include="*.idr" 2>/dev/null | wc -l || echo 0)
79+
PARTIAL=$(grep -rn "^partial" ochrance-core/ src/abi/ --include="*.idr" 2>/dev/null | wc -l || echo 0)
7180
echo "Explicitly partial functions: $PARTIAL"
7281
if [ "$PARTIAL" -gt 0 ]; then
7382
echo "Review required:"
74-
grep -rn "^partial" ochrance-core/ modules/ src/abi/ --include="*.idr" 2>/dev/null
83+
grep -rn "^partial" ochrance-core/ src/abi/ --include="*.idr" 2>/dev/null
7584
fi
7685
7786
- name: FFI stub status
@@ -100,7 +109,7 @@ jobs:
100109
run: |
101110
echo "## ECHIDNA Validation Results" >> $GITHUB_STEP_SUMMARY
102111
echo "" >> $GITHUB_STEP_SUMMARY
103-
echo "- Scanned: ochrance-core/, modules/, src/abi/, ffi/zig/" >> $GITHUB_STEP_SUMMARY
112+
echo "- Scanned: ochrance-core/, src/abi/, ffi/zig/" >> $GITHUB_STEP_SUMMARY
104113
echo "- Checks: dangerous patterns (believe_me etc), totality enforcement, partial functions, FFI stub status, Zig safety" >> $GITHUB_STEP_SUMMARY
105114
echo "" >> $GITHUB_STEP_SUMMARY
106115
echo "*Powered by ECHIDNA neurosymbolic verification*" >> $GITHUB_STEP_SUMMARY

0 commit comments

Comments
 (0)