Address the open issue set: CI truth, proof gates, scanner precision, toolchain policy (21 issues fixed, 3 filed)

.github/workflows/abi-codegen-drift.yml

@@ -54,14 +54,13 @@ jobs:
         uses: actions/cache@v6.1.0
         with:
           path: |
-            /usr/local/bin/idris2
-            /usr/local/bin/idris2_app
-            /usr/local/lib/idris2
             ~/.idris2
           # Same key as verify-proofs.yml on purpose: this job shares that
           # workflow's warm cache rather than paying a second ~20-min
-          # bootstrap. Keep the `-2` suffix in step with it.
-          key: idris2-${{ env.IDRIS2_VERSION }}-${{ runner.os }}-2
+          # bootstrap. Keep the suffix in step with it. `-3` = the
+          # single-prefix layout (#820); `-2` and earlier entries are the
+          # split-prefix caches and must not be restored.
+          key: idris2-${{ env.IDRIS2_VERSION }}-${{ runner.os }}-3
 
       - name: Build Idris 2 from source
         if: steps.cache-idris.outputs.cache-hit != 'true'
@@ -71,9 +70,15 @@ jobs:
             https://github.com/idris-lang/Idris2 /tmp/idris2
           cd /tmp/idris2
           make bootstrap SCHEME=chezscheme
-          sudo make install PREFIX=/usr/local
+          # ONE prefix (#820), same as verify-proofs.yml: install where the
+          # bootstrap-built binary already looks ($HOME/.idris2), so
+          # `idris2 --libdir` and the install trees cannot disagree.
+          make install PREFIX="$HOME/.idris2"
           idris2 --version
 
+      - name: Put Idris 2 on PATH
+        run: echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+
       - name: Verify Idris is on PATH
         run: idris2 --version
 
@@ -117,6 +122,14 @@ jobs:
       # on a cache hit, so this job never mutates the shared entry and redoes
       # the clone+build each run. Do not "optimise" that away -- two workflows
       # writing one cache key is how the poisoned cache of -1 happened.
+      #
+      # #820 SEQUENCING: the bootstrap above now installs ONE prefix, so a
+      # correct install makes this step's repair branch unreachable and it
+      # prints "support installation already complete". That line is the
+      # measurement #820 AC4 asks for. Once a green run shows it (the first
+      # run after the -3 cache lands), this whole step can be deleted -- it
+      # exists to prove the artefacts are present, and deleting the proof
+      # before the measurement is exactly what the issue forbids.
       - name: Ensure the Idris2 support installation is complete
         run: |
           set -euo pipefail

.github/workflows/actions.lock

@@ -14,7 +14,7 @@ workflows:
         - 'actions/setup-node@v7.0.0'
         - 'actions/upload-artifact@v7.0.1'
         - 'dtolnay/rust-toolchain@v1'
-        - 'taiki-e/install-action@v2.87.16'
+        - 'taiki-e/install-action@v2.87.18'
     '.github/workflows/ci-health-sweep.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/ci.yml':
@@ -26,7 +26,7 @@ workflows:
         - 'haskell-actions/hlint-setup@v2.4.10'
         - 'haskell-actions/setup@v2.12.0'
         - 'swatinem/rust-cache@v2.9.2'
-        - 'taiki-e/install-action@v2.87.16'
+        - 'taiki-e/install-action@v2.87.18'
     '.github/workflows/clusterfuzzlite.yml':
         - 'actions/checkout@v7.0.1'
         - 'google/clusterfuzzlite@v1'
@@ -100,8 +100,8 @@ workflows:
         - 'dtolnay/rust-toolchain@v1'
         - 'github/codeql-action@b96794f015dfd88f77b49b1c93e0fa7110f94c63'
         - 'gitleaks/gitleaks-action@v3.0.0'
-        - 'taiki-e/install-action@v2.87.16'
-        - 'trufflesecurity/trufflehog@v3.97.5'
+        - 'taiki-e/install-action@v2.87.18'
+        - 'trufflesecurity/trufflehog@v3.97.6'
     '.github/workflows/tests.yml':
         - 'actions/cache@v6.1.0'
         - 'actions/checkout@v7.0.1'
@@ -112,7 +112,7 @@ workflows:
         - 'dtolnay/rust-toolchain@v1'
         - 'erlef/setup-beam@v1.24.1'
         - 'swatinem/rust-cache@v2.9.2'
-        - 'taiki-e/install-action@v2.87.16'
+        - 'taiki-e/install-action@v2.87.18'
     '.github/workflows/verify-proofs.yml':
         - 'actions/cache@v6.1.0'
         - 'actions/checkout@v7.0.1'
@@ -317,13 +317,13 @@ dependencies:
         commit: 'sha1-6323deb102c322ba6fcbdcafc7e3dddab59af2b6'
         owner_id: 580492
         repo_id: 298565987
-    'taiki-e/install-action@v2.87.16':
-        ref: 'v2.87.16'
-        commit: 'sha1-9114bf4d891761788c546334fd37538eae1bf8b3'
+    'taiki-e/install-action@v2.87.18':
+        ref: 'v2.87.18'
+        commit: 'sha1-dfae9bf3d6f6c6f20ef4ebb3486c01a51341ff12'
         owner_id: 43724913
         repo_id: 442947557
-    'trufflesecurity/trufflehog@v3.97.5':
-        ref: 'v3.97.5'
-        commit: 'sha1-f714bf454f350590f4a24c3ddb1aef02c35bf5b6'
+    'trufflesecurity/trufflehog@v3.97.6':
+        ref: 'v3.97.6'
+        commit: 'sha1-64d939a56362f519781c53ea09b27f8d1dc0140a'
         owner_id: 79229934
         repo_id: 77726177

.github/workflows/ci.yml

@@ -2,7 +2,9 @@
 # SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
 # Main CI workflow for hypatia
-# Tests Rust (adapters, cli, fixer, data), Haskell (registry), and Logtalk (engine)
+# Tests Rust (adapters, cli, fixer, data) and the Elixir rules. The Haskell
+# (registry) jobs below are dormant-gated on the tree's absence; the Logtalk
+# rule engine was retired 2026-03-06 (absorbed into lib/rules/*.ex).
 
 name: CI
 
@@ -48,11 +50,16 @@ jobs:
           workspaces: ". -> target"
           cache-on-failure: true
 
+      # Every cargo invocation in this workflow passes --locked: the committed
+      # Cargo.lock is a hard constraint, not a hint (#841). A failure reading
+      # "the lock file ... needs to be updated but --locked was passed" means
+      # Cargo.lock is out of date w.r.t. the manifests -- regenerate it
+      # deliberately and commit it; never drop --locked to get green.
       - name: Run cargo check
-        run: cargo check --workspace --all-targets
+        run: cargo check --workspace --all-targets --locked
 
       - name: Run clippy
-        run: cargo clippy --workspace --all-targets -- -D warnings
+        run: cargo clippy --workspace --all-targets --locked -- -D warnings
 
   rust-fmt:
     name: Rust Format
@@ -92,10 +99,10 @@ jobs:
           cache-on-failure: true
 
       - name: Run tests
-        run: cargo test --workspace --all-targets
+        run: cargo test --workspace --all-targets --locked
 
       - name: Run doc tests
-        run: cargo test --workspace --doc
+        run: cargo test --workspace --doc --locked
 
   rust-test-coverage:
     name: Rust Coverage

.github/workflows/governance.yml

@@ -1,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
 name: Governance
 

.github/workflows/hypatia-scan.yml

@@ -1,5 +1,5 @@
 # This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # This workflow is managed by gh actions-lock.
 name: Hypatia Security Scan
 

.github/workflows/language-blockers.yml

@@ -1,8 +1,5 @@
 # This workflow is managed by gh actions-lock.
 # SPDX-License-Identifier: MPL-2.0
-# This workflow is managed by gh actions-lock.
-# Consolidated workflow (behaviour-preserving merge).
-# Merged from: npm-bun-blocker.yml, ts-blocker.yml
 name: Language Policy Blockers
 
 on:
@@ -15,38 +12,78 @@ concurrency:
 
 permissions: read-all
 
+# ============================================================================
+# Enforces hyperpolymath/standards 3-practice/LANGUAGE-POLICY.adoc in this
+# repo (issue #832). The doctrine, verbatim: "bun is the runtime; python,
+# deno, rescript and typescript are banned." This workflow previously
+# enforced the INVERSE of that policy — it failed any build carrying
+# `bun.lockb` with the message "npm/bun artifacts detected. Use Deno
+# instead", and its TS gate was structurally incapable of failing (it
+# diffed against HEAD~1 on a depth-1 checkout and swallowed the error).
+# Both are superseded per LANGUAGE-POLICY §1.1/§1.2.
+#
+# Every check prints its denominator; a check that looked at nothing must
+# not read as a pass.
+# ============================================================================
+
 jobs:
-  check:
+  language-policy:
+    name: Language Policy
     runs-on: ubuntu-latest
     timeout-minutes: 30
     permissions:
       contents: read
     steps:
       - uses: actions/checkout@v7.0.1
-      - name: Block npm/bun
+
+      - name: Deno is banned
         run: |
-          if [ -f "package-lock.json" ] || [ -f "bun.lockb" ] || [ -f ".npmrc" ]; then
-            echo "❌ npm/bun artifacts detected. Use Deno instead."
+          set -euo pipefail
+          hits=$(git ls-files | grep -E '(^|/)deno\.jsonc?$' || true)
+          n=$(printf '%s' "$hits" | grep -c . || true)
+          echo "deno manifests in tree: ${n}"
+          if [ "$n" -gt 0 ]; then
+            echo "::error::Deno is banned (LANGUAGE-POLICY §1.3, owner ruling 2026-09-22). Found:"
+            printf '%s\n' "$hits"
             exit 1
           fi
-          echo "✅ No npm/bun violations"
+          echo "✅ No Deno manifests"
 
-  ts_check:
-    runs-on: ubuntu-latest
-    timeout-minutes: 30
-    permissions:
-      contents: read
-    steps:
-      - uses: actions/checkout@v7.0.1
-      - name: Block new TypeScript/JavaScript
+      - name: TypeScript/ReScript are banned (AffineScript is the destination)
         run: |
-          NEW_TS=$(git diff --name-only --diff-filter=A HEAD~1 2>/dev/null | grep -E '\.(ts|tsx)$' | grep -v '\.gen\.' || true)
-          NEW_JS=$(git diff --name-only --diff-filter=A HEAD~1 2>/dev/null | grep -E '\.(js|jsx)$' | grep -v '\.res\.js$' | grep -v '\.gen\.' | grep -v 'node_modules' || true)
-
-          if [ -n "$NEW_TS" ] || [ -n "$NEW_JS" ]; then
-            echo "❌ New TS/JS files detected. Use AffineScript instead."
-            [ -n "$NEW_TS" ] && echo "$NEW_TS"
-            [ -n "$NEW_JS" ] && echo "$NEW_JS"
+          set -euo pipefail
+          # Whole-tree, not new-files-only: this repo tracks zero .ts/.tsx/.res
+          # files (measured 2026-09-26), so the stronger check is free — and
+          # the old `git diff HEAD~1` gate could never fire at all.
+          hits=$(git ls-files '*.ts' '*.tsx' '*.res' '*.resi' '*.res.js' | grep -v '\.gen\.' || true)
+          n=$(printf '%s' "$hits" | grep -c . || true)
+          echo "ts/tsx/res files in tree: ${n}"
+          if [ "$n" -gt 0 ]; then
+            echo "::error::TypeScript/ReScript are banned (LANGUAGE-POLICY §1.2/§3). New application code is AffineScript. Found:"
+            printf '%s\n' "$hits"
+            exit 1
+          fi
+          echo "✅ No TypeScript/ReScript sources"
+
+      - name: Banned runtimes are not provisioned in mise.toml
+        run: |
+          set -euo pipefail
+          # #832 AC5: a banned runtime cannot be reintroduced to mise.toml
+          # silently. Checked here (the language-ban workflow) rather than as
+          # a bespoke grep somewhere new.
+          banned='python|denojs|deno|rescript'
+          hits=$(grep -nE "^(${banned})[[:space:]]*=" mise.toml || true)
+          n=$(printf '%s' "$hits" | grep -c . || true)
+          echo "banned runtimes in mise.toml [tools]: ${n}"
+          if [ "$n" -gt 0 ]; then
+            echo "::error::mise.toml provisions banned runtime(s) (LANGUAGE-POLICY; issue #832). Remove them and any tool that only they can run:"
+            printf '%s\n' "$hits"
+            exit 1
+          fi
+          pyenv=$(grep -nE '^PYTHON' mise.toml || true)
+          if [ -n "$pyenv" ]; then
+            echo "::error::mise.toml still carries PYTHON* env entries with no Python toolchain to read them (#832):"
+            printf '%s\n' "$pyenv"
             exit 1
           fi
-          echo "✅ ReScript policy enforced"
+          echo "✅ mise.toml provisions no banned runtime"

.github/workflows/mirror.yml

@@ -12,11 +12,95 @@ permissions:
   actions: read
   contents: read
 
+# ============================================================================
+# The seven forge mirrors live in hyperpolymath/standards'
+# mirror-reusable.yml (see its header for the per-forge configuration
+# contract). The pin below was deliberately bumped 2026-09-26 from
+# 571cc734 to 2479cf76 (issue #845): the old revision carried three faults
+# this repo's runs were reddening on every push —
+#
+#   1. mirror-gitea ran `ssh-keyscan ... ${{ vars.GITEA_HOST }}` with NO
+#      non-empty assertion, so an unset variable expanded to an empty
+#      argument and the job died at ssh-keyscan usage — a silent
+#      empty-variable expansion that reads exactly like an auth failure.
+#   2. mirror-disroot / mirror-bitbucket presented deploy keys the forges
+#      rejected (Permission denied / Could not read from remote).
+#   3. no run-level accounting: a forge deliberately left unconfigured was
+#      indistinguishable from one that mirrored.
+#
+# The pinned revision asserts every host/fingerprint variable is non-empty
+# and well-formed BEFORE use (naming the variable on failure), verifies the
+# SSH host key against a pinned SHA256 fingerprint per forge, and prints an
+# explicit "Skipped (... not configured)" notice per forge instead of
+# failing obscurely. Fault 2 is OWNER-side (register the public keys on
+# Disroot/Bitbucket, or leave those vars disabled) — the skip notices make
+# the current state legible either way. Per-forge enablement remains the
+# vars.<FORGE>_MIRROR_ENABLED contract; a forge that is not wanted should
+# be left disabled (skip notice) rather than enabled-and-failing.
+# ============================================================================
+
 jobs:
   mirror:
-    uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd
+    uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@2479cf769ed5f0481ccf64860a2ab954514c2b59
     secrets: inherit
     permissions:
       actions: read
       contents: read
       security-events: write
+
+  # #845 AC3: a run must state the denominator — mirrors enabled out of the
+  # seven configured forge integrations — so an unconfigured forge reads as
+  # "skipped", never as a mirror. Push verification by remote SHA (AC5) needs
+  # remote read access per forge and is tracked on the issue; this job
+  # reports what THIS repo has actually configured.
+  mirror-coverage:
+    name: Mirror coverage
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    needs: mirror
+    if: always()
+    steps:
+      - name: Report configured forge mirrors
+        env:
+          GITLAB: ${{ vars.GITLAB_MIRROR_ENABLED }}
+          BITBUCKET: ${{ vars.BITBUCKET_MIRROR_ENABLED }}
+          CODEBERG: ${{ vars.CODEBERG_MIRROR_ENABLED }}
+          SOURCEHUT: ${{ vars.SOURCEHUT_MIRROR_ENABLED }}
+          DISROOT: ${{ vars.DISROOT_MIRROR_ENABLED }}
+          GITEA: ${{ vars.GITEA_MIRROR_ENABLED }}
+          RADICLE: ${{ vars.RADICLE_MIRROR_ENABLED }}
+          GITEA_HOST: ${{ vars.GITEA_HOST }}
+        run: |
+          set -euo pipefail
+          enabled=0
+          total=7
+          report() {
+            name="$1"; val="$2"; note="$3"
+            if [ "$val" = "true" ]; then
+              enabled=$((enabled + 1))
+              echo "- ${name}: ENABLED ${note}"
+            else
+              echo "- ${name}: skipped (vars.${name}_MIRROR_ENABLED != 'true') ${note}"
+            fi
+          }
+          {
+            echo "## Forge mirror coverage"
+            echo ""
+            report GITLAB "$GITLAB" ""
+            report BITBUCKET "$BITBUCKET" "(deploy key must be registered on the forge or the job skips)"
+            report CODEBERG "$CODEBERG" ""
+            report SOURCEHUT "$SOURCEHUT" ""
+            report DISROOT "$DISROOT" "(deploy key must be registered on the forge or the job skips)"
+            if [ "$GITEA" = "true" ] && [ -z "$GITEA_HOST" ]; then
+              echo "- GITEA: ENABLED but vars.GITEA_HOST is empty — the reusable will refuse the push and name the variable (#845)"
+            fi
+            report GITEA "$GITEA" "(needs vars.GITEA_HOST + vars.GITEA_SSH_FINGERPRINT)"
+            report RADICLE "$RADICLE" ""
+            echo ""
+            echo "forge mirrors enabled: ${enabled} of ${total}"
+          } | tee -a "$GITHUB_STEP_SUMMARY"
+          echo "forge mirrors enabled: ${enabled} of ${total}"
+          # An empty denominator is a configuration death, not a clean run.
+          if [ "$enabled" -eq 0 ]; then
+            echo "::notice::0 of ${total} forge mirrors configured on this repo. Nothing is mirrored; this is legible, not a failure."
+          fi

.github/workflows/quality.yml

@@ -117,9 +117,13 @@ jobs:
           toolchain: stable
           components: rust-docs
 
+      # --locked: the committed Cargo.lock is a hard constraint (#841). A
+      # failure reading "the lock file ... needs to be updated but --locked
+      # was passed" means Cargo.lock is out of date w.r.t. the manifests --
+      # regenerate it deliberately; never drop --locked to get green.
       - name: Generate Rust API documentation
         run: |
-          cargo doc --workspace --no-deps --document-private-items
+          cargo doc --workspace --no-deps --document-private-items --locked
           cp -r target/doc/* _site/api/
 
       # NOTE: a "Generate Haskell API documentation" step (working-directory: