ci: Lean via elan in ECHIDNA + drop duplicate trufflehog --fail (#161)

Round 2 of Phase 0 CI hygiene — two reds that only surfaced *after* #159
landed on main.

## 1. ECHIDNA `Install proof provers` — apt exit 100
#159 dropped `isabelle`, but the dispatched run on main then failed on
`E: Unable to locate package lean`. Ubuntu 24.04 (noble) packages
neither `lean` nor `isabelle`. This installs Lean 4 via **elan** (pinned
to `v3.1.1`, sha256-verified — identical to `lean-verification.yml`),
keeping coq/agda/z3 from apt. Isabelle stays absent;
`validate-with-echidna.sh` reports SKIP for absent provers.

## 2. Secret Scanner `trufflehog` job — duplicate `--fail`
#159's permission grant fixed the reusable `scan/*` jobs — **they now
pass on main** (rust-secrets, gitleaks, shell-secrets all green). But
the separate `trufflehog` job then ran for the first time and failed
with `flag 'fail' cannot be repeated`: the trufflehog action injects
`--fail` itself, so `extra_args` must not repeat it. Now
`--only-verified` only.

## Verification
- `scan/*` + `trufflehog` will prove themselves on this PR.
- I'll re-dispatch **ECHIDNA Validation** on main after merge to confirm
the elan path builds and `echidna list-provers` succeeds.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/echidna-validation.yml

@@ -51,18 +51,20 @@ jobs:
           echo "/tmp/echidna/target/release" >> $GITHUB_PATH
 
       - name: Install proof provers
-        # `isabelle` is not packaged in Ubuntu 24.04 (noble); requesting it
-        # fails the whole job with apt exit 100. validate-with-echidna.sh
-        # reports SKIP for absent provers, so Isabelle proofs are skipped
-        # rather than blocking the pipeline.
+        # 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 \
-            lean \
-            coq \
-            agda \
-            z3
+          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

.github/workflows/secret-scanner.yml

@@ -30,4 +30,7 @@ jobs:
       - name: TruffleHog Secret Scan
         uses: trufflesecurity/trufflehog@00155c9dc586f34d189adc83d3ac2698c2ec551f # v3.93.3
         with:
-          extra_args: --only-verified --fail
+          # The action already appends `--fail` internally; repeating it here
+          # makes the trufflehog binary abort with "flag 'fail' cannot be
+          # repeated". Pass only `--only-verified`.
+          extra_args: --only-verified