docs: resync status claims with the verified state of the repo (#72) #112
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # SPDX-License-Identifier: MPL-2.0 | |
| name: ECHIDNA Validation | |
| on: | |
| push: | |
| paths: | |
| - 'ochrance-core/**' | |
| - 'modules/**' | |
| - 'src/abi/**' | |
| - 'ffi/zig/**' | |
| - 'tests/**' | |
| - '.github/workflows/echidna-validation.yml' | |
| pull_request: | |
| paths: | |
| - 'ochrance-core/**' | |
| - 'modules/**' | |
| - 'src/abi/**' | |
| schedule: | |
| - cron: '0 6 * * 1' # Weekly on Monday at 06:00 UTC | |
| permissions: | |
| contents: read | |
| jobs: | |
| echidna-totality: | |
| name: ECHIDNA Totality & Safety Audit | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 15 | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 | |
| - name: Dangerous pattern scan (Idris2) | |
| run: | | |
| echo "=== Idris2 Dangerous Pattern Scan (code only; comments excluded) ===" | |
| ISSUES=0 | |
| for pattern in "believe_me" "assert_total" "assert_smaller" "unsafePerformIO"; do | |
| # Strip doc comments (||| ...) and line comments (-- ...) before | |
| # matching, so documentation that merely names a pattern is not | |
| # flagged: only genuine uses in code count. Without this, a doc | |
| # string like "this proof needs no assert_smaller" would fail the gate. | |
| MATCHES="" | |
| for f in $(find ochrance-core/ src/abi/ -name "*.idr" 2>/dev/null); do | |
| M=$(sed -e 's/|||.*$//' -e 's/--.*$//' "$f" | grep -n "$pattern" | sed "s|^|$f:|" || true) | |
| [ -n "$M" ] && MATCHES="${MATCHES}${M}"$'\n' | |
| done | |
| N=$(printf '%s' "$MATCHES" | grep -c . || true) | |
| if [ "$N" -gt 0 ]; then | |
| echo "CRITICAL: Found $N use(s) of '$pattern' in code:" | |
| printf '%s\n' "$MATCHES" | |
| ISSUES=$((ISSUES + N)) | |
| fi | |
| done | |
| echo "Total dangerous patterns (in code): $ISSUES" | |
| echo "dangerous_count=$ISSUES" >> $GITHUB_OUTPUT | |
| if [ "$ISSUES" -gt 0 ]; then | |
| echo "FAIL: Dangerous patterns detected in Idris2 code" >&2 | |
| exit 1 | |
| fi | |
| - name: Totality enforcement check | |
| run: | | |
| echo "=== Totality Enforcement ===" | |
| MISSING=0 | |
| for f in $(find ochrance-core/ src/abi/ -name "*.idr" 2>/dev/null); do | |
| if ! grep -q "%default total" "$f"; then | |
| echo "WARNING: $f missing '%default total'" | |
| MISSING=$((MISSING + 1)) | |
| fi | |
| done | |
| echo "Modules missing %default total: $MISSING" | |
| if [ "$MISSING" -gt 0 ]; then | |
| echo "WARNING: Some modules lack totality enforcement" | |
| fi | |
| - name: Partial function check | |
| run: | | |
| echo "=== Partial Function Check ===" | |
| PARTIAL=$(grep -rn "^partial" ochrance-core/ src/abi/ --include="*.idr" 2>/dev/null | wc -l || echo 0) | |
| echo "Explicitly partial functions: $PARTIAL" | |
| if [ "$PARTIAL" -gt 0 ]; then | |
| echo "Review required:" | |
| grep -rn "^partial" ochrance-core/ src/abi/ --include="*.idr" 2>/dev/null | |
| fi | |
| - name: FFI stub status | |
| run: | | |
| echo "=== FFI Stub Status ===" | |
| echo "Checking ochrance-core/Ochrance/FFI/Echidna.idr..." | |
| if grep -q "FFI not yet implemented" ochrance-core/Ochrance/FFI/Echidna.idr 2>/dev/null; then | |
| echo "INFO: Echidna FFI still stubbed (echidnaProve/echidnaVerify return defaults)" | |
| else | |
| echo "INFO: Echidna FFI may be implemented — verify libechidna.so linkage" | |
| fi | |
| - name: Zig FFI safety check | |
| if: hashFiles('ffi/zig/src/*.zig') != '' | |
| run: | | |
| echo "=== Zig FFI Safety Check ===" | |
| for pattern in "@intToPtr" "@ptrToInt"; do | |
| FOUND=$(grep -rn "$pattern" ffi/zig/src/ --include="*.zig" 2>/dev/null | wc -l || echo 0) | |
| if [ "$FOUND" -gt 0 ]; then | |
| echo "WARNING: Found $FOUND instances of '$pattern' in Zig FFI" | |
| grep -rn "$pattern" ffi/zig/src/ --include="*.zig" 2>/dev/null | |
| fi | |
| done | |
| - name: Summary | |
| run: | | |
| echo "## ECHIDNA Validation Results" >> $GITHUB_STEP_SUMMARY | |
| echo "" >> $GITHUB_STEP_SUMMARY | |
| echo "- Scanned: ochrance-core/, src/abi/, ffi/zig/" >> $GITHUB_STEP_SUMMARY | |
| echo "- Checks: dangerous patterns (believe_me etc), totality enforcement, partial functions, FFI stub status, Zig safety" >> $GITHUB_STEP_SUMMARY | |
| echo "" >> $GITHUB_STEP_SUMMARY | |
| echo "*Powered by ECHIDNA neurosymbolic verification*" >> $GITHUB_STEP_SUMMARY |