e2e.yml

# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
#
# proven — E2E + Safety Aspect + Bench
#
# Tests the full proof chain: Idris2 → Zig FFI → integration.
# Safety aspects verify no dangerous patterns escape into production.

name: E2E + Safety + Bench
env:
  FORCE_JAVASCRIPT_ACTIONS_TO_NODE24: true
on:
  push:
    branches: [main, master, develop]
    paths:
      - 'src/**'
      - 'ffi/**'
      - 'tests/**'
      - 'bindings/**'
      - '.github/workflows/e2e.yml'
  pull_request:
    branches: [main, master]
    paths:
      - 'src/**'
      - 'ffi/**'
      - 'tests/**'
      - 'bindings/**'
  workflow_dispatch:
permissions: read-all
  actions: read
concurrency:
  group: e2e-${{ github.ref }}
  cancel-in-progress: true
jobs:
  e2e-ffi:
    name: E2E — Zig FFI Build + Integration
    runs-on: ubuntu-latest
    timeout-minutes: 15
    steps:
      - name: Checkout
        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
      - name: Install Zig
        uses: mlugg/setup-zig@e7d1537c378b83b8049f65dda471d87a2f7b2df2 # v1
        with:
          version: '0.15.2'
      # Build the standalone pure-Zig FFI surface (src/main.zig only) -- no
      # Idris2 RefC / idris2_zig_ffi dependency. The full Idris->RefC->Zig
      # pipeline needs the private nextgen-languages/language-bridges repo,
      # which CI cannot fetch as a path dependency; see PR #149.
      - name: Build FFI (standalone Zig surface)
        run: cd ffi/zig && zig build --build-file build_standalone.zig
      - name: Run FFI tests (standalone)
        run: cd ffi/zig && zig build test --build-file build_standalone.zig
      - name: Verify library output
        run: ls -la ffi/zig/zig-out/lib/libproven_ffi.* || echo "Library output check"
  safety-aspects:
    name: Aspect — Safety Invariants
    runs-on: ubuntu-latest
    timeout-minutes: 10
    steps:
      - name: Checkout
        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
      - name: No dangerous Idris2 patterns
        run: |
          # Match actual usage, not doc-comment mentions. The matched line
          # must (a) contain the pattern, (b) not start (after whitespace)
          # with `|||` (Idris doc comment) or `--` (regular comment).
          DANGEROUS=$(grep -rn 'believe_me\|assert_total\|really_believe_me' src/ 2>/dev/null \
                       | grep -v test \
                       | grep -vE '^[^:]+:[0-9]+:[[:space:]]*(\|\|\||--)' \
                       || true)
          if [ -n "$DANGEROUS" ]; then
            echo "FAIL: Dangerous patterns found in src/ (excluding comments)"
            echo "$DANGEROUS"
            exit 1
          fi
          echo "PASS: No believe_me/assert_total in src/ (comments OK)"
      - name: No @panic in Zig production code
        run: |
          PANICS=$(grep -rn '@panic' ffi/zig/src/ 2>/dev/null | grep -v test || true)
          if [ -n "$PANICS" ]; then
            echo "FAIL: @panic in FFI production code"
            echo "$PANICS"
            exit 1
          fi
          echo "PASS: No @panic in Zig production code"
      - name: No panic-prone patterns in bindings
        run: |
          # NB: the bare `unsafe` keyword is NOT a violation — it is required
          # by Rust to call FFI (e.g. `unsafe { ffi::proven_safe_add(...) }`).
          # What IS forbidden is anything that can crash on bad input:
          #
          #   * Rust:     .unwrap()  .expect(  panic!(  unreachable!(  todo!(  unimplemented!(
          #   * ReScript: getExn      Obj.magic
          #   * Haskell:  unsafePerformIO  unsafeCoerce
          #
          # Notes:
          #   * The Haskell `error "..."` partial function and `undefined` are
          #     intentionally NOT listed here — they collide with the English
          #     word "error" and the ECMAScript `undefined` literal, producing
          #     too many false positives. They are caught by per-language
          #     linters (HLint, etc.) in their own CI.
          #   * Restricted to source extensions; READMEs, JSON manifests, and
          #     docs are not scanned (mentions in docs are not code usage).
          #   * Test code excluded.
          if [ -d "bindings" ]; then
            UNSAFE=$(find bindings -type f \
                       \( -name '*.rs' -o -name '*.res' -o -name '*.resi' \
                          -o -name '*.hs' -o -name '*.lhs' \
                          -o -name '*.ml' -o -name '*.mli' \
                          -o -name '*.idr' \) \
                       -not -path '*/test/*' -not -path '*/tests/*' \
                       -print0 2>/dev/null \
                     | xargs -0 grep -nE '\.unwrap\(\)|\.expect\(|panic!\(|unreachable!\(|todo!\(|unimplemented!\(|getExn|Obj\.magic|unsafePerformIO|unsafeCoerce' 2>/dev/null \
                     | grep -vE ':[0-9]+:[[:space:]]*(--|//|\(\*|\*[^/]|///)' \
                     || true)
            if [ -n "$UNSAFE" ]; then
              echo "FAIL: Panic-prone patterns in bindings (excluding comments and tests)"
              echo "$UNSAFE" | head -20
              exit 1
            fi
          fi
          echo "PASS: No panic-prone patterns in bindings (FFI 'unsafe { }' blocks are allowed)"
      - name: SPDX headers present
        run: |
          MISSING=0
          for f in $(find src/ -name "*.idr" 2>/dev/null | head -50); do
            if ! head -5 "$f" | grep -q "SPDX"; then
              echo "MISSING: $f"
              MISSING=$((MISSING + 1))
            fi
          done
          if [ "$MISSING" -gt 0 ]; then
            echo "WARN: $MISSING files missing SPDX headers"
          else
            echo "PASS: All checked files have SPDX headers"
          fi
  benchmarks:
    name: Bench — FFI Performance
    runs-on: ubuntu-latest
    timeout-minutes: 15
    steps:
      - name: Checkout
        uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4
      - name: Install Zig
        uses: mlugg/setup-zig@e7d1537c378b83b8049f65dda471d87a2f7b2df2 # v1
        with:
          version: '0.15.2'
      - name: Build and bench FFI
        run: cd ffi/zig && zig build bench --build-file build_standalone.zig 2>&1 | tee /tmp/bench-results.txt || echo "No bench target yet"
      - name: Upload benchmark results
        if: always()
        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
        with:
          name: benchmark-results
          path: /tmp/bench-results.txt
          retention-days: 30