valence-shell/.github/workflows/echidna-validation.yml at main · hyperpolymath/valence-shell · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
# SPDX-License-Identifier: MPL-2.0
name: ECHIDNA Validation

on:
  push:
    paths:
      - 'proofs/**'
      - 'impl/rust-cli/src/**'
      - 'impl/rust-cli/tests/**'
      - 'scripts/validate-with-echidna.sh'
      - '.github/workflows/echidna-validation.yml'
  pull_request:
    paths:
      - 'proofs/**'
      - 'impl/rust-cli/**'
  schedule:
    - cron: '0 6 * * 1'  # Weekly on Monday at 06:00 UTC
  workflow_dispatch:

permissions:
  actions: read
  contents: read

jobs:
  echidna-verify:
    name: ECHIDNA Proof Verification
    # Keep this integration check out of required PR CI until ECHIDNA verify
    # supports project roots for Lean, Coq, and Agda. The pinned revision makes
    # scheduled results reproducible while that upstream contract is repaired.
    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
    runs-on: ubuntu-latest
    timeout-minutes: 30
    steps:
      - name: Checkout code
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v6.0.2

      - name: Install Rust toolchain
        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7  # stable
        with:
          components: rustfmt, clippy

      - name: Cache Rust dependencies
        uses: Swatinem/rust-cache@f0d9c3887740aee45f6153b24b3a6b815192ec16  # v2
        with:
          workspaces: impl/rust-cli

      - name: Build ECHIDNA from source
        env:
          ECHIDNA_REF: e1347cd3552ac6ec7c404da3d941baee3bb51817
        run: |
          git init /tmp/echidna
          cd /tmp/echidna
          git remote add origin https://github.com/hyperpolymath/echidna.git
          git fetch --depth 1 origin "$ECHIDNA_REF"
          git checkout --detach FETCH_HEAD
          test "$(git rev-parse HEAD)" = "$ECHIDNA_REF"
          cargo build --release --bin echidna
          echo "/tmp/echidna/target/release" >> "$GITHUB_PATH"

      - name: Install proof provers
        # Ubuntu 24.04 (noble) packages neither `lean` nor `isabelle`, and
        # apt-get exits 100 on any unknown package. Lean 4 comes via elan
        # (pinned + checksum-verified, same as lean-verification.yml).
        # Isabelle stays uninstalled; validate-with-echidna.sh reports SKIP
        # for absent provers rather than failing.
        run: |
          set -euo pipefail
          sudo apt-get update
          sudo apt-get install -y --no-install-recommends coq agda z3
          curl -sSfL https://raw.githubusercontent.com/leanprover/elan/v3.1.1/elan-init.sh -o elan-init.sh
          echo "f5d473c923c093759ae3839073bec2a58e82cb8bc0e4083930e76090da75b310  elan-init.sh" | sha256sum -c -
          sh elan-init.sh -y
          rm -f elan-init.sh
          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"

      - name: Verify ECHIDNA available
        run: echidna list-provers

      - name: Run ECHIDNA validation pipeline
        run: bash scripts/validate-with-echidna.sh --verbose
        env:
          ECHIDNA_BIN: /tmp/echidna/target/release/echidna

  correspondence:
    name: Lean 4 ↔ Rust Correspondence
    runs-on: ubuntu-latest
    timeout-minutes: 30
    steps:
      - name: Checkout code
        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v6.0.2

      - name: Install Rust toolchain
        uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7  # stable

      - name: Cache Rust dependencies
        uses: Swatinem/rust-cache@f0d9c3887740aee45f6153b24b3a6b815192ec16  # v2
        with:
          workspaces: impl/rust-cli

      - name: Run correspondence tests
        working-directory: impl/rust-cli
        run: cargo test --test correspondence_tests --verbose

      - name: Run property correspondence tests
        working-directory: impl/rust-cli
        run: cargo test --test property_tests --verbose

      - name: Run security tests
        working-directory: impl/rust-cli
        run: cargo test --test security_tests --verbose

      - name: Count proof holes
        run: |
          echo "=== Proof Hole Audit ==="
          echo ""
          echo "--- Lean 4 (sorry) ---"
          grep -rn "sorry" proofs/lean4/ || echo "(none)"
          echo ""
          echo "--- Coq (Admitted) ---"
          grep -rn "Admitted" proofs/coq/ || echo "(none)"
          echo ""
          echo "--- Agda (postulate) ---"
          grep -rn "postulate" proofs/agda/ || echo "(none)"
          echo ""
          LEAN_HOLES=$(grep -r "sorry" proofs/lean4/ 2>/dev/null | wc -l || echo 0)
          COQ_HOLES=$(grep -r "Admitted" proofs/coq/ 2>/dev/null | wc -l || echo 0)
          AGDA_HOLES=$(grep -r "postulate" proofs/agda/ 2>/dev/null | wc -l || echo 0)
          TOTAL=$((LEAN_HOLES + COQ_HOLES + AGDA_HOLES))
          echo "Total proof holes: $TOTAL (Lean: $LEAN_HOLES, Coq: $COQ_HOLES, Agda: $AGDA_HOLES)"
          echo ""
          if [ "$TOTAL" -gt 35 ]; then
            echo "WARNING: Proof holes increased beyond baseline (31). Investigate."
            exit 1
          fi