Foundational layer: A2ML v1.1 (profiles + base vocab + citations + hashing) and K9-SVC 1.0 hardening #21
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 | |
| # 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' | |
| - 'avow-protocol/avow-lib/src/abi/*.idr' | |
| - '.github/workflows/echidna-verify.yml' | |
| pull_request: | |
| paths: | |
| - 'lol/proofs/**' | |
| - 'a2ml/src/**/*.idr' | |
| - 'avow-protocol/avow-lib/src/abi/*.idr' | |
| 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: | |
| contents: read | |
| jobs: | |
| agda-lol: | |
| name: Agda — lol/proofs | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 20 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 | |
| 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@834a144ee995460fba8ed112a2fc961b36a5ec5a # v4.3.6 | |
| with: | |
| name: agda-verify-log | |
| path: agda-verify.log | |
| if-no-files-found: ignore | |
| idris2-a2ml: | |
| name: Idris2 — a2ml proofs | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 20 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 | |
| with: | |
| submodules: recursive | |
| - name: Cache pack | |
| uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # 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 A2ML core (Proofs + v1.1 profiles/base-vocab) | |
| run: | | |
| export PATH="$HOME/.pack/bin:$PATH" | |
| cd a2ml | |
| idris2 --check src/A2ML/Proofs.idr 2>&1 | tee ../idris2-a2ml.log | |
| # v1.1 additive core: checking Profiles.idr transitively type-checks | |
| # BaseVocab.idr and TypedCore.idr (its imports). | |
| idris2 --check src/A2ML/Profiles.idr 2>&1 | tee -a ../idris2-a2ml.log | |
| - name: Upload log | |
| if: always() | |
| uses: actions/upload-artifact@834a144ee995460fba8ed112a2fc961b36a5ec5a # v4.3.6 | |
| with: | |
| name: idris2-a2ml-log | |
| path: idris2-a2ml.log | |
| if-no-files-found: ignore | |
| idris2-avow: | |
| name: Idris2 — AVOW consent proofs | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 20 | |
| steps: | |
| - name: Checkout | |
| uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 | |
| with: | |
| submodules: recursive | |
| - name: Cache pack | |
| uses: actions/cache@668228422ae6a00e4ad889ee87cd7109ec5666a7 # 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" | |
| 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@834a144ee995460fba8ed112a2fc961b36a5ec5a # v4.3.6 | |
| with: | |
| name: idris2-avow-log | |
| path: idris2-avow.log | |
| if-no-files-found: ignore | |
| trust-summary: | |
| name: Trust pipeline summary | |
| needs: [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" |