echidna-validation.yml

# 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@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
      - 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