From 447aaebc554784772a2b5bdde63046e0ff630b40 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 17 Sep 2026 20:09:03 +0000 Subject: [PATCH] =?UTF-8?q?fix(ci):=20echidna-verify=20=E2=80=94=20honest?= =?UTF-8?q?=20absence=20guards=20for=20agda-lol=20&=20idris2-a2ml=20jobs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both jobs crashed on proof corpora that were permanently evicted from this repo (agda-lol: find/cd lol/proofs failed at the Type-check step after the apt install; idris2-a2ml: cd a2ml failed AFTER an ~18-minute pack bootstrap, every run). idris2-avow got the 'Nothing to type-check' in-step guard long ago; these two never did (issue #748). Each job now opens with a presence Guard right after checkout that emits a honest ::notice and sets present=false; the toolchain-install, type-check and audit steps (a2ml: cache/install/type-check) run only when the corpus is present. If the corpora ever return, the jobs verify them again, unchanged. Job outcome is green-but-honest, not silently-so: the notice says the corpus is absent. Corrected CICD-WORKFLOW-CATALOG.md: the row claimed 'Echidna smart contract verification' — this workflow is the ECHIDNA trust pipeline (Agda/Idris2 proofs), not the smart-contract fuzzer — and now documents the guard behaviour. Validation: PyYAML parse, bash -n on both guard blocks, diff = 2 files +44/-1, working tree clean of foreign edits. Refs #748 --- .github/workflows/echidna-verify.yml | 43 ++++++++++++++++++++++++++++ CICD-WORKFLOW-CATALOG.md | 2 +- 2 files changed, 44 insertions(+), 1 deletion(-) diff --git a/.github/workflows/echidna-verify.yml b/.github/workflows/echidna-verify.yml index 923f3d3c4..09a785152 100644 --- a/.github/workflows/echidna-verify.yml +++ b/.github/workflows/echidna-verify.yml @@ -7,6 +7,13 @@ # - a2ml/src/A2ML/Proofs.idr # - avow-protocol/avow-lib/src/abi/*.idr # +# Proof-corpus status (issue #748): all three corpora are EVICTED from this +# repo and live in their own repos today. Each job therefore opens with a +# presence Guard that bows out honestly ("Nothing to type-check", green, +# toolchain spend skipped) instead of crashing deep in the job; if a corpus +# ever returns, the job verifies it again unchanged. The jobs stay so the +# check names keep reporting on every proof-touching run. +# # Dogfooding: standards repo defines ECHIDNA trust pipeline; this workflow # applies that pipeline to the repo's own proofs. @@ -87,7 +94,23 @@ jobs: with: submodules: recursive + - name: Guard — proofs are evicted from this repo + id: guard + run: | + # Same honesty guard idris2-avow got (see its Type-check step), + # placed BEFORE the toolchain install so the weekly cron stops + # spending minutes bootstrapping for a directory that does not + # exist. lol/proofs moved to the lol repository; if the corpus ever + # returns here, this job verifies again, unchanged (issue #748). + if [ ! -d lol/proofs ]; then + echo "::notice title=Agda proofs::lol/proofs is absent here — proofs were evicted to the lol repository. Nothing to type-check; remaining steps skipped." + echo "present=false" >> "$GITHUB_OUTPUT" + else + echo "present=true" >> "$GITHUB_OUTPUT" + fi + - name: Install Agda + if: steps.guard.outputs.present == 'true' run: | sudo apt-get update sudo apt-get install -y agda agda-stdlib @@ -95,6 +118,7 @@ jobs: - name: Type-check proofs id: typecheck + if: steps.guard.outputs.present == 'true' run: | set -e echo "=== Agda proofs under lol/proofs ===" @@ -106,6 +130,7 @@ jobs: done - name: Postulate audit + if: steps.guard.outputs.present == 'true' run: | echo "=== Postulate usage in lol/proofs ===" grep -rn "postulate" lol/proofs/theories/ || echo "No postulates found" @@ -130,7 +155,23 @@ jobs: with: submodules: recursive + - name: Guard — proofs are evicted from this repo + id: guard + run: | + # This job used to burn ~18 minutes bootstrapping Idris2 via pack + # and THEN `cd a2ml` into a directory that does not exist (the + # A2ML proof corpus lives in the a2ml repository now). Guard first, + # before any toolchain spend; if the corpus returns, the job + # verifies again, unchanged (issue #748). + if [ ! -d a2ml ]; then + echo "::notice title=Idris2 a2ml proofs::a2ml/ is absent here — the proof corpus was evicted to the a2ml repository. Nothing to type-check; remaining steps skipped." + echo "present=false" >> "$GITHUB_OUTPUT" + else + echo "present=true" >> "$GITHUB_OUTPUT" + fi + - name: Cache pack + if: steps.guard.outputs.present == 'true' uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v4 with: path: | @@ -141,6 +182,7 @@ jobs: ${{ runner.os }}-idris2-pack- - name: Install Idris2 via pack + if: steps.guard.outputs.present == 'true' run: | set -e if command -v idris2 >/dev/null 2>&1; then @@ -172,6 +214,7 @@ jobs: idris2 --version - name: Type-check normative A2ML core + if: steps.guard.outputs.present == 'true' run: | set -euo pipefail export PATH="$HOME/.pack/bin:$PATH" diff --git a/CICD-WORKFLOW-CATALOG.md b/CICD-WORKFLOW-CATALOG.md index 7f86cca03..c6ccd7929 100644 --- a/CICD-WORKFLOW-CATALOG.md +++ b/CICD-WORKFLOW-CATALOG.md @@ -120,7 +120,7 @@ These workflows only run when manually triggered. |----------|-------------|--------|----------| | `elixir-ci.yml` | Elixir build and test | rsr-template-repo | No | | `elixir-ci-reusable.yml` | Reusable Elixir CI | standards | Yes | -| `echidna-verify.yml` | Echidna smart contract verification | standards | Yes | +| `echidna-verify.yml` | ECHIDNA trust-pipeline proof verification (Agda/Idris2). NOT the smart-contract fuzzer. As of #748 all proof corpora are evicted to their own repos; each job starts with a presence Guard and passes green-but-honest ("Nothing to type-check") until a corpus returns — it is dormant, not broken. | standards | Yes | ### Julia | Workflow | Description | Source | Reusable? |