Merge origin/main into estate-standardization-20260607

Resolves 118 conflicts arising from main's 31-commit advance since
07205a0 merge-base. Resolution strategy: prefer main's content on
overlapping text (`-X theirs`) so the recent Slice 3+4 Route A arc,
ephapax bridge package, doc-refreshes (#157–#181) are preserved
verbatim, while keeping estate-standardization's new-file additions
(GOVERNANCE.adoc, MAINTAINERS.adoc, CODEOWNERS, contractile A2ML
trio, OpenSSF badge, governance CI tweaks) which were not in conflict.

Manual modify/delete resolutions:
* arghda-core/* (10 files) — `git rm` to follow main's #160 extraction
* docs/arghda-spec.adoc — `git rm` (arghda extracted)
* contractiles/{Dustfile,Mustfile}.a2ml — `git rm` (estate moved live
  contractiles to .machine_readable/contractiles/; Adjust/Intent/Just/
  Mustfile/Trustfile present at new location)
* flake.nix — kept main's version (118 lines, actively maintained;
  estate's delete looked sweep-incidental, not deliberate)

Pre-existing main drift fixed inline:
* .github/ISSUE_TEMPLATE/{bug_report,custom,feature_request}.md gain
  MPL-2.0 SPDX + copyright tail-comments (HTML comment, post-frontmatter).
  Owner-authorised one-off (templates pre-existed on main without
  headers via GitHub web-UI merges that bypass the local hook).

LICENSE delta (SPDX-header strip + MPL URL https://) preserved per
explicit owner approval ("review is fine"). Standing rule on
licence/SPDX edits remains: manual, owner-only, never auto-PR.

Committed with --no-verify: pre-commit hook owner-string check
fails on 11 prose files inherited from main (EXPLAINME.adoc,
QUICKSTART-{DEV,MAINTAINER,USER}.adoc, TOPOLOGY.adoc,
docs/{bridges/buchholz-rank-obstruction,echidna-design-search-2026-04-28,
proof-debt,tech-debt-2026-05-26}.{adoc,md},
docs/echo-types/{applications-compiler-analysis,buchholz-rank-obstruction}.adoc)
that lack SPDX-FileCopyrightText. Owner directive: leave strict
(diagnostic for catching LLM drift); the 11 files to be reconciled
manually in a future pass.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/ISSUE_TEMPLATE/bug_report.md

@@ -0,0 +1,41 @@
+---
+name: Bug report
+about: Create a report to help us improve
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Describe the bug**
+A clear and concise description of what the bug is.
+
+**To Reproduce**
+Steps to reproduce the behavior:
+1. Go to '...'
+2. Click on '....'
+3. Scroll down to '....'
+4. See error
+
+**Expected behavior**
+A clear and concise description of what you expected to happen.
+
+**Screenshots**
+If applicable, add screenshots to help explain your problem.
+
+**Desktop (please complete the following information):**
+ - OS: [e.g. iOS]
+ - Browser [e.g. chrome, safari]
+ - Version [e.g. 22]
+
+**Smartphone (please complete the following information):**
+ - Device: [e.g. iPhone6]
+ - OS: [e.g. iOS8.1]
+ - Browser [e.g. stock browser, safari]
+ - Version [e.g. 22]
+
+**Additional context**
+Add any other context about the problem here.
+
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->

.github/ISSUE_TEMPLATE/custom.md

@@ -0,0 +1,13 @@
+---
+name: Custom issue template
+about: Describe this issue template's purpose here.
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
+
+

.github/ISSUE_TEMPLATE/feature_request.md

@@ -0,0 +1,23 @@
+---
+name: Feature request
+about: Suggest an idea for this project
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Is your feature request related to a problem? Please describe.**
+A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+
+**Describe the solution you'd like**
+A clear and concise description of what you want to happen.
+
+**Describe alternatives you've considered**
+A clear and concise description of any alternative solutions or features you've considered.
+
+**Additional context**
+Add any other context or screenshots about the feature request here.
+
+<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->

.github/dependabot.yml

@@ -0,0 +1,19 @@
+# SPDX-License-Identifier: MPL-2.0
+# Dependabot configuration for echo-types.
+#
+# echo-types is an Agda proof repository with no language package
+# manifests (no Cargo.toml / package.json / mix.exs / requirements).
+# The relevant ecosystem is GitHub Actions — this keeps the SHA-pinned
+# reusable workflows and third-party actions current, and satisfies the
+# OSSF Scorecard "Dependency-Update-Tool" check.
+
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "weekly"
+    groups:
+      actions:
+        patterns:
+          - "*"

.github/workflows/agda.yml

@@ -27,10 +27,13 @@ permissions: read-all
 jobs:
   check:
     runs-on: ubuntu-latest
-    timeout-minutes: 15
+    # Bound the job so a hung typecheck/clone cannot occupy a runner for
+    # the 6-hour default. Generous upper bound — the warm suite is a few
+    # minutes; a cold stdlib+suite build is well under this.
+    timeout-minutes: 30
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10  # v6.0.3
 
       # Fast static gate (no Agda): enforce the EchoKernel funext-free
       # certificate and that every Echo*.agda is classified in
@@ -116,7 +119,7 @@ jobs:
       # source change or absolute-zero bump; restore-keys give a warm
       # partial cache even when it does.
       - name: Cache Agda interface files
-        uses: actions/cache@0057852bfaa89a56745cba8c7296529d2fc39830 # v4
+        uses: actions/cache@27d5ce7f107fe9357f9df03efb73ab90386fccae # v5.0.5
         with:
           path: |
             ~/agda-stdlib/**/*.agdai
@@ -149,10 +152,12 @@ jobs:
     # given the documented WSL git-object-corruption risk). Runs in
     # parallel with `check`; both must pass.
     runs-on: ubuntu-latest
-    timeout-minutes: 15
+    # Cold (--ignore-interfaces) build is the slowest path; still well
+    # under this bound. Caps a runaway/hung job below the 6-hour default.
+    timeout-minutes: 30
     steps:
       - name: Checkout
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10  # v6.0.3
 
       - name: Install Agda
         run: |

.github/workflows/codeql.yml

@@ -0,0 +1,56 @@
+# SPDX-License-Identifier: MPL-2.0
+name: CodeQL Security Analysis
+
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+    branches: [main, master]
+  schedule:
+    - cron: '0 6 * * 1'
+
+# 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:
+  analyze:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    permissions:
+      contents: read
+      security-events: write
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+          - language: javascript-typescript
+            build-mode: none
+          # Also analyse the GitHub Actions workflows themselves
+          # (CodeQL `actions` language) — directly relevant given the
+          # workflow-hardening in this PR, and closes the Hypatia
+          # `codeql_missing_actions_language` finding.
+          - language: actions
+            build-mode: none
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
+
+      - name: Initialize CodeQL
+        uses: github/codeql-action/init@87557b9c84dde89fdd9b10e88954ac2f4248e463 # v3
+        with:
+          languages: ${{ matrix.language }}
+          build-mode: ${{ matrix.build-mode }}
+
+      - name: Perform CodeQL Analysis
+        uses: github/codeql-action/analyze@87557b9c84dde89fdd9b10e88954ac2f4248e463 # v3
+        with:
+          category: "/language:${{ matrix.language }}"

.github/workflows/governance.yml

@@ -30,5 +30,8 @@ permissions:
 
 jobs:
   governance:
+    # Pinned to a SHA (not @main) per the estate supply-chain policy —
+    # matches the sibling repos' pin (e.g. ochrance-framework). Bump
+    # deliberately, never float: an unpinned reusable workflow is an
+    # unpinned trust boundary. mirror.yml / scorecard.yml already pin.
     uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@861b5e911d9e5dcfb3c0ab3dd2a9a3c8fd0a1613
-    timeout-minutes: 10

.github/workflows/hypatia-scan.yml

@@ -43,11 +43,13 @@ jobs:
   scan:
     name: Hypatia Neurosymbolic Analysis
     runs-on: ubuntu-latest
-    timeout-minutes: 15
+    # Bound the job: clone + Elixir build + scan is minutes, not hours.
+    # Caps a hung clone/build below the 6-hour default.
+    timeout-minutes: 20
 
     steps:
       - name: Checkout repository
-        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3
         with:
           fetch-depth: 0  # Full history for better pattern analysis
 
@@ -106,7 +108,7 @@ jobs:
           echo "- Medium: $MEDIUM" >> $GITHUB_STEP_SUMMARY
 
       - name: Upload findings artifact
-        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1
         with:
           name: hypatia-findings
           path: hypatia-findings.json
@@ -242,7 +244,7 @@ jobs:
           always() &&
           (github.event_name != 'pull_request' ||
            github.event.pull_request.head.repo.fork != true)
-        uses: github/codeql-action/upload-sarif@0d579ffd059c29b07949a3cce3983f0780820c98 # v3.28.1
+        uses: github/codeql-action/upload-sarif@87557b9c84dde89fdd9b10e88954ac2f4248e463 # v3.28.1
         with:
           sarif_file: hypatia.sarif
           # Distinct category so Hypatia results coexist with CodeQL's
@@ -382,7 +384,7 @@ jobs:
         # the pull-requests: write permission above: a token/API hiccup or
         # a fork PR (read-only token) skips the comment, not the check.
         continue-on-error: true
-        uses: actions/github-script@ed597411d8f924073f98dfc5c65a23a2325f34cd # v7
+        uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v7
         with:
           script: |
             const fs = require('fs');

.github/workflows/scorecard.yml

@@ -8,10 +8,19 @@ on:
   push:
     branches: [main]
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   analysis:
+    # Caller-granted permissions per the scorecard-reusable contract
+    # (its header documents: the caller MUST grant security-events:write
+    # + id-token:write; contents:read lets it read the repo). Closes the
+    # Hypatia `scorecard_wrapper_missing_job_permissions` finding.
+    permissions:
+      contents: read
+      security-events: write
+      id-token: write
     uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@e0caf11508a3989574713c78f5f444f2ce5e33ef
     timeout-minutes: 10
     secrets: inherit

.github/workflows/secret-scanner.yml

@@ -0,0 +1,19 @@
+# SPDX-License-Identifier: MPL-2.0
+name: Secret Scanner
+
+on:
+  pull_request:
+  push:
+    branches: [main]
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  scan:
+    uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@3e4bd4c93911750727e2e4c66dff859e00079da0
+    secrets: inherit