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
# 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:
  contents: read

jobs:
  echidna-verify:
    name: ECHIDNA Proof Verification
    # This job builds the external ECHIDNA repository from its current default
    # branch. Keep that moving integration check out of required PR CI so
    # valence-shell changes are not blocked by an unrelated upstream breakage.
    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
    runs-on: ubuntu-latest
    timeout-minutes: 30
    steps:
      - name: Checkout code
        uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # 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@7e35be21c2b94d972b1143087fabc27d7dc881ef  # v2
        with:
          workspaces: impl/rust-cli

      - name: Build ECHIDNA from source
        run: |
          git clone --depth 1 https://github.com/hyperpolymath/echidna.git /tmp/echidna
          cd /tmp/echidna
          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@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0  # v6.0.2

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

      - name: Cache Rust dependencies
        uses: Swatinem/rust-cache@7e35be21c2b94d972b1143087fabc27d7dc881ef  # 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