Repository navigation
Spec/descriptile v1 #172
Workflow file for this run
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 | |
| # This workflow is managed by gh actions-lock. | |
| # ECHIDNA proof verification — formal verification of Agda and Idris2 proofs. | |
| # | |
| # Scope: | |
| # - lol/proofs/theories/**/*.agda | |
| # - a2ml/src/A2ML/Proofs.idr | |
| # - avow-protocol/avow-lib/src/abi/*.idr | |
| # | |
| # Dogfooding: standards repo defines ECHIDNA trust pipeline; this workflow | |
| # applies that pipeline to the repo's own proofs. | |
| name: ECHIDNA Proof Verification | |
| on: | |
| push: | |
| branches: [main] | |
| paths: | |
| - 'lol/proofs/**' | |
| - 'a2ml/src/**/*.idr' | |
| - 'a2ml/a2ml-core.ipkg' | |
| - 'avow-protocol/avow-lib/src/abi/*.idr' | |
| - '.github/workflows/echidna-verify.yml' | |
| # NO path filter on pull_request, deliberately. `Idris2 - a2ml proofs` is a | |
| # REQUIRED context, and a workflow-level path filter means the whole workflow | |
| # never triggers for a PR that touches nothing else - so the context never | |
| # reports and the PR deadlocks. Filtering moved to job level below: the | |
| # workflow always starts, and the expensive jobs skip when no proofs changed. | |
| # A job skipped by `if:` still emits a check run whose conclusion GitHub | |
| # accepts for a required status check. | |
| pull_request: | |
| schedule: | |
| # Weekly re-verification to catch stale-proof drift | |
| - cron: '0 6 * * 1' | |
| workflow_dispatch: | |
| # Estate guardrail: cancel superseded runs so re-pushes / rebased PR | |
| # updates do not pile up queued runs against the shared account-wide | |
| # Actions concurrency pool. Applied only to read-only check workflows | |
| # (no publish/mutation), so cancelling a superseded run is always safe. | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| permissions: | |
| actions: read | |
| contents: read | |
| jobs: | |
| detect-proof-changes: | |
| timeout-minutes: 5 | |
| name: Detect proof changes | |
| runs-on: ubuntu-latest | |
| outputs: | |
| proofs: ${{ steps.check.outputs.proofs }} | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: Did this change touch any proof source? | |
| id: check | |
| shell: bash | |
| run: | | |
| # Non-PR events (push, schedule, dispatch) always verify. | |
| if [ "${{ github.event_name }}" != "pull_request" ]; then | |
| echo "proofs=true" >> "$GITHUB_OUTPUT"; exit 0 | |
| fi | |
| base="${{ github.event.pull_request.base.sha }}" | |
| head="${{ github.event.pull_request.head.sha }}" | |
| changed=$(git diff --name-only "$base" "$head" 2>/dev/null || true) | |
| if printf '%s\n' "$changed" | grep -qE '^(lol/proofs/|a2ml/src/.*\.idr$|a2ml/a2ml-core\.ipkg$|avow-protocol/avow-lib/src/abi/.*\.idr$|\.github/workflows/echidna-verify\.yml$)'; then | |
| echo "proofs=true" >> "$GITHUB_OUTPUT" | |
| else | |
| echo "proofs=false" >> "$GITHUB_OUTPUT" | |
| fi | |
| agda-lol: | |
| name: Agda — lol/proofs | |
| needs: detect-proof-changes | |
| if: needs.detect-proof-changes.outputs.proofs == 'true' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 20 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| submodules: recursive | |
| - name: Install Agda | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install -y agda agda-stdlib | |
| agda --version | |
| - name: Type-check proofs | |
| id: typecheck | |
| run: | | |
| set -e | |
| echo "=== Agda proofs under lol/proofs ===" | |
| find lol/proofs/theories -name '*.agda' -print | |
| cd lol/proofs | |
| for f in $(find theories -name '*.agda'); do | |
| echo "--- checking $f ---" | |
| agda --safe "$f" 2>&1 | tee -a ../../agda-verify.log || true | |
| done | |
| - name: Postulate audit | |
| run: | | |
| echo "=== Postulate usage in lol/proofs ===" | |
| grep -rn "postulate" lol/proofs/theories/ || echo "No postulates found" | |
| - name: Upload log | |
| if: always() | |
| uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| with: | |
| name: agda-verify-log | |
| path: agda-verify.log | |
| if-no-files-found: ignore | |
| idris2-a2ml: | |
| name: Idris2 — a2ml proofs | |
| needs: detect-proof-changes | |
| if: needs.detect-proof-changes.outputs.proofs == 'true' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 20 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| submodules: recursive | |
| - name: Cache pack | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v4 | |
| with: | |
| path: | | |
| ~/.pack | |
| ~/.idris2 | |
| key: ${{ runner.os }}-idris2-pack-${{ hashFiles('**/pack.toml', '**/*.ipkg') }} | |
| restore-keys: | | |
| ${{ runner.os }}-idris2-pack- | |
| - name: Install Idris2 via pack | |
| run: | | |
| set -e | |
| if command -v idris2 >/dev/null 2>&1; then | |
| echo "idris2 already present: $(idris2 --version)" | |
| exit 0 | |
| fi | |
| # Bootstrap: install pack, which installs idris2. | |
| sudo apt-get update | |
| sudo apt-get install -y build-essential libgmp-dev chezscheme | |
| # Clone pack bootstrap | |
| git clone --depth 1 https://github.com/stefan-hoeck/idris2-pack.git "$HOME/idris2-pack" | |
| cd "$HOME/idris2-pack" | |
| # Use the bootstrap script in non-interactive mode | |
| # pack's install.bash prompts for the scheme binary; feeding newlines | |
| # makes the prompt take its detected default (chezscheme) instead of | |
| # hitting EOF (which aborts the bootstrap and leaves pack uninstalled). | |
| yes '' | bash install.bash || echo "::warning::pack install had warnings" | |
| # pack installs its launcher into ~/.local/bin (newer layout) and/or | |
| # ~/.pack/bin (older); add both so `pack` resolves on PATH. | |
| echo "$HOME/.local/bin" >> "$GITHUB_PATH" | |
| echo "$HOME/.pack/bin" >> "$GITHUB_PATH" | |
| export PATH="$HOME/.local/bin:$HOME/.pack/bin:$PATH" | |
| # `install-api` is not a pack subcommand; `install-app idris2` | |
| # installs the idris2 executable into the pack bin dir so the | |
| # subsequent `idris2 --check` resolves. The base library (Prelude, | |
| # base, contrib) ships with idris2, so no .ipkg is needed for a | |
| # standalone --check. | |
| pack install-app idris2 | |
| idris2 --version | |
| - name: Type-check normative A2ML core | |
| run: | | |
| set -euo pipefail | |
| export PATH="$HOME/.pack/bin:$PATH" | |
| cd a2ml | |
| # Use the package target: per-file `--check` can exit successfully | |
| # when an imported module is missing and therefore is not a real | |
| # gate for the authoritative module set (standards#556). | |
| idris2 --version | tee ../idris2-a2ml.log | |
| idris2 --typecheck a2ml-core.ipkg 2>&1 | tee -a ../idris2-a2ml.log | |
| - name: Upload log | |
| if: always() | |
| uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| with: | |
| name: idris2-a2ml-log | |
| path: idris2-a2ml.log | |
| if-no-files-found: ignore | |
| idris2-avow: | |
| name: Idris2 — AVOW consent proofs | |
| needs: detect-proof-changes | |
| if: needs.detect-proof-changes.outputs.proofs == 'true' | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 20 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| with: | |
| submodules: recursive | |
| - name: Cache pack | |
| uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v4 | |
| with: | |
| path: | | |
| ~/.pack | |
| ~/.idris2 | |
| key: ${{ runner.os }}-idris2-pack-${{ hashFiles('**/pack.toml', '**/*.ipkg') }} | |
| restore-keys: | | |
| ${{ runner.os }}-idris2-pack- | |
| - name: Install Idris2 via pack | |
| run: | | |
| set -e | |
| if command -v idris2 >/dev/null 2>&1; then | |
| echo "idris2 already present: $(idris2 --version)" | |
| exit 0 | |
| fi | |
| sudo apt-get update | |
| sudo apt-get install -y build-essential libgmp-dev chezscheme | |
| git clone --depth 1 https://github.com/stefan-hoeck/idris2-pack.git "$HOME/idris2-pack" | |
| cd "$HOME/idris2-pack" | |
| # pack's install.bash prompts for the scheme binary; feeding newlines | |
| # makes the prompt take its detected default (chezscheme) instead of | |
| # hitting EOF (which aborts the bootstrap and leaves pack uninstalled). | |
| yes '' | bash install.bash || echo "::warning::pack install had warnings" | |
| # pack installs its launcher into ~/.local/bin (newer layout) and/or | |
| # ~/.pack/bin (older); add both so `pack` resolves on PATH. | |
| echo "$HOME/.local/bin" >> "$GITHUB_PATH" | |
| echo "$HOME/.pack/bin" >> "$GITHUB_PATH" | |
| export PATH="$HOME/.local/bin:$HOME/.pack/bin:$PATH" | |
| # `install-api` is not a pack subcommand; `install-app idris2` | |
| # installs the idris2 executable into the pack bin dir so the | |
| # subsequent `idris2 --check` resolves. The base library (Prelude, | |
| # base, contrib) ships with idris2, so no .ipkg is needed for a | |
| # standalone --check. | |
| pack install-app idris2 | |
| idris2 --version | |
| - name: Type-check AVOW proofs | |
| run: | | |
| export PATH="$HOME/.pack/bin:$PATH" | |
| # The per-file `if [ -f ]` guard below was written to tolerate absent | |
| # proofs, but the `cd` ahead of it was NOT guarded, so a missing | |
| # directory killed the step before the guard could ever run. In this | |
| # repo avow-protocol/ holds only BINDING.adoc - the proofs live in the | |
| # avow-protocol repository - so the cd always failed and this job was | |
| # permanently red. It only became visible once the workflow began | |
| # running on pull requests. | |
| if [ ! -d avow-protocol/avow-lib ]; then | |
| echo "::notice title=AVOW proofs::avow-protocol/avow-lib is not present here (this repo carries only the BINDING). Nothing to type-check." | |
| exit 0 | |
| fi | |
| cd avow-protocol/avow-lib | |
| for f in src/abi/Consent.idr src/abi/Unsubscribe.idr src/abi/Types.idr; do | |
| if [ -f "$f" ]; then | |
| echo "--- checking $f ---" | |
| idris2 --check "$f" 2>&1 | tee -a ../../idris2-avow.log | |
| fi | |
| done | |
| - name: Upload log | |
| if: always() | |
| uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 | |
| with: | |
| name: idris2-avow-log | |
| path: idris2-avow.log | |
| if-no-files-found: ignore | |
| trust-summary: | |
| timeout-minutes: 10 | |
| name: Trust pipeline summary | |
| needs: [detect-proof-changes, agda-lol, idris2-a2ml, idris2-avow] | |
| runs-on: ubuntu-latest | |
| if: always() | |
| steps: | |
| - name: Summarise | |
| run: | | |
| echo "## ECHIDNA Trust Summary" >> "$GITHUB_STEP_SUMMARY" | |
| echo "" >> "$GITHUB_STEP_SUMMARY" | |
| echo "| Target | Result |" >> "$GITHUB_STEP_SUMMARY" | |
| echo "|---|---|" >> "$GITHUB_STEP_SUMMARY" | |
| echo "| Agda lol/proofs | ${{ needs.agda-lol.result }} |" >> "$GITHUB_STEP_SUMMARY" | |
| echo "| Idris2 a2ml | ${{ needs.idris2-a2ml.result }} |" >> "$GITHUB_STEP_SUMMARY" | |
| echo "| Idris2 avow | ${{ needs.idris2-avow.result }} |" >> "$GITHUB_STEP_SUMMARY" | |
| echo "" >> "$GITHUB_STEP_SUMMARY" | |
| echo "See artefacts for verification logs." >> "$GITHUB_STEP_SUMMARY" |