audit: routing/rule-engine recon, Logtalk quarantine; Agda proofs re-checked under PROOF-POLICY §2.1

.echidnabot.toml

@@ -16,7 +16,6 @@ secondary_languages = ["julia", "affinescript", "idris2", "chapel", "spark"]
 
 [provers]
 # ECHIDNA is self-hosting - can verify its own Idris2 ABI definitions
-idris2 = { enabled = true, priority = "high" }
 
 # Can also use SMT solvers for property checking
 z3 = { enabled = true, priority = "medium" }
@@ -27,6 +26,8 @@ coq = { enabled = true, priority = "low" }
 lean = { enabled = true, priority = "low" }
 
 [provers.idris2]
+enabled = true
+priority = "high"
 package_file = "src/abi/echidnaabi.ipkg"
 source_dirs = ["src/abi"]
 totality_required = true

.github/hooks/validate-a2ml.sh

@@ -17,6 +17,7 @@
 # Exit codes:
 #   0 — All files valid (or only warnings in non-strict mode)
 #   1 — Validation errors found
+#   2 — Required input scan could not run
 
 set -euo pipefail
 
@@ -199,6 +200,12 @@ validate_a2ml() {
         if [[ "$line" =~ ^[[:space:]]*:schema-version[[:space:]] ]]; then
             has_version=true
         fi
+        # These are presence checks. Once both facts have witnesses, later
+        # corpus records cannot change them. Body/attestation checks below
+        # still inspect the complete file.
+        if [[ "$has_identity" == "true" && "$has_version" == "true" ]]; then
+            break
+        fi
     done < "$file"
 
     # AI manifest files (0-AI-MANIFEST.a2ml, 0.1-AI-MANIFEST.a2ml, etc.)
@@ -299,28 +306,39 @@ validate_a2ml() {
     local attestation_has_content=false
     line_num=0
 
-    while IFS= read -r line; do
-        line_num=$((line_num + 1))
-
-        # Detect attestation section start
-        if [[ "$line" =~ ^\[attestation\] ]] || [[ "$line" =~ ^##[[:space:]]+[Aa]ttestation ]] || [[ "$line" =~ ^##[[:space:]]+ATTESTATION ]]; then
-            in_attestation=true
-            attestation_line=$line_num
-            continue
-        fi
-
-        # Detect next section (ends attestation block)
-        if [[ "$in_attestation" == "true" ]]; then
-            if [[ "$line" =~ ^\[.+\] ]] || [[ "$line" =~ ^##[[:space:]] ]]; then
-                in_attestation=false
+    # A native grep scans the whole file before choosing whether the slower
+    # stateful shell walk is needed. Most large training corpora have no
+    # attestation section; no body or path is excluded from validation.
+    local attestation_probe=0
+    grep -qE '^\[attestation\]|^##[[:space:]]+([Aa]ttestation|ATTESTATION)' "$file" || attestation_probe=$?
+    if [[ "$attestation_probe" -gt 1 ]]; then
+        echo "::error::Cannot read $file; manifest validation NOT RUN"
+        exit 2
+    fi
+    if [[ "$attestation_probe" -eq 0 ]]; then
+        while IFS= read -r line; do
+            line_num=$((line_num + 1))
+
+            # Detect attestation section start
+            if [[ "$line" =~ ^\[attestation\] ]] || [[ "$line" =~ ^##[[:space:]]+[Aa]ttestation ]] || [[ "$line" =~ ^##[[:space:]]+ATTESTATION ]]; then
+                in_attestation=true
+                attestation_line=$line_num
                 continue
             fi
-            # Check for content in attestation block
-            if [[ "$line" =~ (proof|signature|verified|hash)[[:space:]]*= ]]; then
-                attestation_has_content=true
+
+            # Detect next section (ends attestation block)
+            if [[ "$in_attestation" == "true" ]]; then
+                if [[ "$line" =~ ^\[.+\] ]] || [[ "$line" =~ ^##[[:space:]] ]]; then
+                    in_attestation=false
+                    continue
+                fi
+                # Check for content in attestation block
+                if [[ "$line" =~ (proof|signature|verified|hash)[[:space:]]*= ]]; then
+                    attestation_has_content=true
+                fi
             fi
-        fi
-    done < "$file"
+        done < "$file"
+    fi
 
     if [[ $attestation_line -gt 0 && "$attestation_has_content" == "false" && "$is_manifest" == "false" ]]; then
         report_issue "warning" "$file" "$attestation_line" \
@@ -329,18 +347,20 @@ validate_a2ml() {
 
     # --- Check 4: Section heading syntax ---
     # Validate that [section] headings are well-formed (no unclosed brackets)
-    line_num=0
-    while IFS= read -r line; do
-        line_num=$((line_num + 1))
-        # Lines starting with [ should have a matching ]
-        if [[ "$line" =~ ^\[ && ! "$line" =~ ^\[.+\] ]]; then
-            # Exclude markdown-style links and multi-line values
-            if [[ ! "$line" =~ ^\[.*\]\( && ! "$line" =~ ^\[TODO && ! "$line" =~ ^\[YOUR ]]; then
-                report_issue "warning" "$file" "$line_num" \
-                    "Possibly malformed section heading: unclosed bracket"
-            fi
-        fi
-    done < "$file"
+    # Apply the same heading predicates in one native full-file pass. Preserve
+    # original line numbers, and fail if the scan itself cannot read the file.
+    local malformed_headings
+    if ! malformed_headings=$(awk '
+      /^\[/ && !/^\[.+\]/ && !/^\[.*\]\(/ && !/^\[TODO/ && !/^\[YOUR/ { print NR }
+    ' "$file"); then
+        echo "::error::Cannot scan headings in $file; manifest validation NOT RUN"
+        exit 2
+    fi
+    while IFS= read -r line_num; do
+        [[ -n "$line_num" ]] || continue
+        report_issue "warning" "$file" "$line_num" \
+            "Possibly malformed section heading: unclosed bracket"
+    done <<< "$malformed_headings"
 }
 
 # ---------------------------------------------------------------------------

.github/workflows/actions.lock

@@ -6,7 +6,6 @@ workflows:
     '.github/workflows/agda-meta-checker.yml':
         - 'actions/cache@v6.1.0'
         - 'actions/checkout@v7.0.1'
-        - 'haskell-actions/setup@v2.12.1'
     '.github/workflows/boj-build.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/bridge-gate.yml':
@@ -46,9 +45,9 @@ workflows:
         - 'actions/attest-build-provenance@v4.2.2'
         - 'actions/checkout@v7.0.1'
     '.github/workflows/governance.yml':
-        - 'metadatastician/standards@087f6bff5135ce3da6f287c83752256ce4a8efc1'
+        - 'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
     '.github/workflows/hypatia-scan.yml':
-        - 'metadatastician/standards@087f6bff5135ce3da6f287c83752256ce4a8efc1'
+        - 'metadatastician/standards@d3e4b485a2af90c92a8e18af0888cd19cb132cd9'
     '.github/workflows/idris2-abi-ci.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/label-triage.yml': []
@@ -58,7 +57,7 @@ workflows:
         - 'dtolnay/rust-toolchain@v1'
         - 'swatinem/rust-cache@v2.9.3'
     '.github/workflows/mirror.yml':
-        - 'metadatastician/standards@087f6bff5135ce3da6f287c83752256ce4a8efc1'
+        - 'metadatastician/standards@3c00687a5bbd0d881d351db8502417b5d0a8b0b0'
     '.github/workflows/mvp-smoke.yml':
         - 'actions/checkout@v7.0.1'
         - 'dtolnay/rust-toolchain@v1'
@@ -81,16 +80,17 @@ workflows:
         - 'swatinem/rust-cache@v2.9.3'
         - 'taiki-e/install-action@v2.87.32'
     '.github/workflows/scorecard.yml':
-        - 'metadatastician/standards@087f6bff5135ce3da6f287c83752256ce4a8efc1'
+        - 'metadatastician/standards@d3e4b485a2af90c92a8e18af0888cd19cb132cd9'
     '.github/workflows/secret-scanner.yml':
-        - 'metadatastician/standards@087f6bff5135ce3da6f287c83752256ce4a8efc1'
-    '.github/workflows/security-scan.yml': []
+        - 'hyperpolymath/proven-cicd@a12b2b4644db1a1250bc50b58fd24c99f89f564e'
+    '.github/workflows/security-scan.yml':
+        - 'hyperpolymath/panic-attack@be6ac46716eaf049570ec4966f4ae4699b319689'
     '.github/workflows/server-boot-gate.yml':
         - 'actions/checkout@v7.0.1'
         - 'dtolnay/rust-toolchain@v1'
         - 'swatinem/rust-cache@v2.9.3'
     '.github/workflows/spark-theatre-gate.yml':
-        - 'metadatastician/standards@087f6bff5135ce3da6f287c83752256ce4a8efc1'
+        - 'metadatastician/standards@d3e4b485a2af90c92a8e18af0888cd19cb132cd9'
     '.github/workflows/static-analysis-gate.yml':
         - 'actions/checkout@v7.0.1'
         - 'actions/download-artifact@v8.0.2'
@@ -99,12 +99,17 @@ workflows:
     '.github/workflows/verification-proofs-cron.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/workflow-linter.yml':
-        - 'actions/checkout@v7.0.1'
+        - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
     '.github/workflows/zig-ffi-ci.yml':
         - 'actions/checkout@v7.0.1'
         - 'hyperpolymath/cicd-suite@4c772eb235b04455307d5c03cbbc4f45130f7f0f'
         - 'mlugg/setup-zig@v2.2.1'
 dependencies:
+    'Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0':
+        ref: 'v2.9.3'
+        commit: 'sha1-d1527c8f67ef9af357290475d4af4b0fab8f12e0'
+        owner_id: 580492
+        repo_id: 298565987
     'actions/attest-build-provenance@v4.2.2':
         ref: 'v4.2.2'
         commit: 'sha1-4d101475d8b20a2381f78447822ac1eab6504dd8'
@@ -224,34 +229,61 @@ dependencies:
         commit: 'sha1-884713a6c30a92e5e8544c39945cd7cb630abcd1'
         owner_id: 1342004
         repo_id: 400046858
-    'haskell-actions/setup@v2.12.1':
-        ref: 'v2.12.1'
-        commit: 'sha1-0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d'
-        owner_id: 75048950
-        repo_id: 623796603
     'hyperpolymath/cicd-suite@4c772eb235b04455307d5c03cbbc4f45130f7f0f':
         ref: 'main'
         commit: 'sha1-4c772eb235b04455307d5c03cbbc4f45130f7f0f'
         owner_id: 6759885
         repo_id: 1326697643
-    'metadatastician/standards@087f6bff5135ce3da6f287c83752256ce4a8efc1':
-        ref: '087f6bff5135ce3da6f287c83752256ce4a8efc1'
-        commit: 'sha1-087f6bff5135ce3da6f287c83752256ce4a8efc1'
+    'hyperpolymath/panic-attack@be6ac46716eaf049570ec4966f4ae4699b319689':
+        ref: 'be6ac46716eaf049570ec4966f4ae4699b319689'
+        commit: 'sha1-be6ac46716eaf049570ec4966f4ae4699b319689'
+        owner_id: 6759885
+        repo_id: 1152434997
+        uses:
+            - 'Swatinem/rust-cache@d1527c8f67ef9af357290475d4af4b0fab8f12e0'
+            - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
+            - 'dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8'
+    'hyperpolymath/proven-cicd@a12b2b4644db1a1250bc50b58fd24c99f89f564e':
+        ref: 'a12b2b4644db1a1250bc50b58fd24c99f89f564e'
+        commit: 'sha1-a12b2b4644db1a1250bc50b58fd24c99f89f564e'
+        owner_id: 6759885
+        repo_id: 1446155688
+        uses:
+            - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
+    'metadatastician/standards@3c00687a5bbd0d881d351db8502417b5d0a8b0b0':
+        ref: '3c00687a5bbd0d881d351db8502417b5d0a8b0b0'
+        commit: 'sha1-3c00687a5bbd0d881d351db8502417b5d0a8b0b0'
+        owner_id: 297579217
+        repo_id: 1116521501
+        uses:
+            - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
+            - 'dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8'
+            - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555'
+    'metadatastician/standards@a797d308c0517d4e2d21cc7f1cb08d41f82b1a12':
+        ref: 'a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
+        commit: 'sha1-a797d308c0517d4e2d21cc7f1cb08d41f82b1a12'
         owner_id: 297579217
         repo_id: 1116521501
         uses:
             - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9'
             - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
-            - 'actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333'
-            - 'actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9'
             - 'denoland/setup-deno@22d081ff2d3a40755e97629de92e3bcbfa7cf2ed'
-            - 'dtolnay/rust-toolchain@683b588c487a69d01f6c6ddf40f036ff682cc2c8'
             - 'editorconfig-checker/action-editorconfig-checker@51f63319f592f97930c73d9c46184d20bd206393'
             - 'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124'
+            - 'oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6'
+    'metadatastician/standards@d3e4b485a2af90c92a8e18af0888cd19cb132cd9':
+        ref: 'd3e4b485a2af90c92a8e18af0888cd19cb132cd9'
+        commit: 'sha1-d3e4b485a2af90c92a8e18af0888cd19cb132cd9'
+        owner_id: 297579217
+        repo_id: 1116521501
+        uses:
+            - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9'
+            - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
+            - 'actions/download-artifact@9000827ccba6bdab643e8b6fd33ac0654aef8333'
+            - 'actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9'
+            - 'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124'
             - 'github/codeql-action@b96794f015dfd88f77b49b1c93e0fa7110f94c63'
             - 'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e'
-            - 'oven-sh/setup-bun@0c5077e51419868618aeaa5fe8019c62421857d6'
-            - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555'
     'mlugg/setup-zig@v2.2.1':
         ref: 'v2.2.1'
         commit: 'sha1-d1434d08867e3ee9daa34448df10607b98908d29'

.github/workflows/agda-meta-checker.yml

@@ -13,11 +13,16 @@ on:
     branches: [main]
     paths:
       - 'meta-checker/**'
+      - 'scripts/ci/*agda.sh'
+      - 'scripts/ci/check-receipt-controls.sh'
+      - '.github/workflows/agda-meta-checker.yml'
   # No paths-filter on pull_request: this is a REQUIRED status check, so it must
   # report on every PR (a path-filtered required check deadlocks PRs that don't
   # touch its paths). The "Detect relevant changes" step path-gates internally.
   pull_request:
     branches: [main]
+  schedule:
+    - cron: '30 2 * * *'
   workflow_dispatch:
 
 # Cause-B mitigation (#77): cancel superseded runs so stacked pushes
@@ -33,11 +38,14 @@ permissions:
 jobs:
   verify-proofs:
     name: Type-check Agda proofs
-    runs-on: ubuntu-latest
-    timeout-minutes: 15
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
     steps:
       - name: Checkout
         uses: actions/checkout@v7.0.1
+        with:
+          ref: ${{ github.event.pull_request.head.sha || github.sha }}
+          persist-credentials: false
 
       # Required-check shim: only the meta-checker/ tree needs the real proof
       # check. Non-PR events (push, workflow_dispatch) always run it.
@@ -47,61 +55,33 @@ jobs:
           GH_TOKEN: ${{ github.token }}
         run: |
           set -euo pipefail
-          PATTERN='^(meta-checker/|\.github/workflows/agda-meta-checker\.yml$)'
+          PATTERN='^(meta-checker/|scripts/ci/(setup-agda|check-agda|check-receipt-controls)\.sh$|\.github/workflows/agda-meta-checker\.yml$)'
           if [ "${{ github.event_name }}" = "pull_request" ]; then
             FILES=$(gh api "repos/${{ github.repository }}/pulls/${{ github.event.pull_request.number }}/files" \
                       --paginate --jq '.[].filename')
-            if printf '%s\n' "$FILES" | grep -qE "$PATTERN"; then
+            if printf '%s\n' "$FILES" | grep -E "$PATTERN" > /dev/null; then
               echo "relevant=true" >> "$GITHUB_OUTPUT"
               echo "meta-checker/ sources changed — running full Agda type-check."
             else
               echo "relevant=false" >> "$GITHUB_OUTPUT"
-              echo "No meta-checker changes — pass-through (required-check shim)."
+              echo "NOT APPLICABLE: proof source/tooling paths unchanged; compiler did not run."
             fi
           else
             echo "relevant=true" >> "$GITHUB_OUTPUT"
             echo "Non-PR event — running full Agda type-check."
           fi
 
-      - name: Setup Haskell
-        if: steps.detect.outputs.relevant == 'true'
-        uses: haskell-actions/setup@v2.12.1
-        with:
-          ghc-version: '9.6'
-          cabal-version: '3.10'
-
-      - name: Cache Agda
+      - name: Cache pinned Agda archives
         if: steps.detect.outputs.relevant == 'true'
         uses: actions/cache@v6.1.0
         with:
-          path: |
-            ~/.cabal
-            ~/.agda
-          key: agda-${{ runner.os }}-${{ hashFiles('meta-checker/**/*.agda') }}
+          path: ~/.cache/echidna/agda
+          key: agda-archives-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('scripts/ci/setup-agda.sh') }}
 
-      - name: Install Agda
+      - name: Install pinned Agda and standard library
         if: steps.detect.outputs.relevant == 'true'
-        run: |
-          cabal update
-          # --overwrite-policy=always: the cached ~/.cabal restore already
-          # carries the agda symlink, so a plain install aborts with
-          # "Path '.../bin/agda' already exists" on a warm cache.
-          cabal install Agda-2.7.0.1 --overwrite-policy=always
+        run: bash scripts/ci/setup-agda.sh
 
-      - name: Install Agda standard library
+      - name: Type-check meta-checker (PROOF-POLICY §2.1 canonical invocation)
         if: steps.detect.outputs.relevant == 'true'
-        run: |
-          mkdir -p ~/.agda
-          cd /tmp
-          wget -q https://github.com/agda/agda-stdlib/archive/refs/tags/v2.1.tar.gz
-          tar xzf v2.1.tar.gz
-          echo "/tmp/agda-stdlib-2.1/standard-library.agda-lib" > ~/.agda/libraries
-          echo "standard-library" > ~/.agda/defaults
-
-      - name: Type-check meta-checker
-        if: steps.detect.outputs.relevant == 'true'
-        run: |
-          cd meta-checker
-          echo "$PWD/echidna-meta.agda-lib" >> ~/.agda/libraries
-          agda --safe --without-K --cubical-compatible src/Echidna/MetaChecker.agda
-          echo "✓ Meta-checker passed with safe / without-K / cubical-compatible; proof assumptions require a separate audit"
+        run: bash scripts/ci/check-agda.sh