ci: harden workflows + resolve Hypatia findings at source (#178)

Adds codeql.yml (javascript-typescript + actions), secret-scanner.yml,
and .github/dependabot.yml; pins the governance reusable to a SHA; adds
timeout-minutes to the real-step jobs; grants scorecard's analysis job
the documented caller permissions; and adds .hypatia-ignore for two
verified false positives (agda_postulate on Smoke.agda comments;
SVG-namespace http URL in build-banner.mjs).

Advisory Hypatia scan after these changes: Critical 0. Remaining items
are upstream rule limitations (hypatia/standards), addressed by a
separate patch. No proofs/Agda/core files touched. All 21 checks green.

https://claude.ai/code/session_01Jxr3Wy4ngpkbc2QwjEam82

Author: hyperpolymath

.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,6 +27,10 @@ permissions: read-all
 jobs:
   check:
     runs-on: ubuntu-latest
+    # 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
@@ -148,6 +152,9 @@ jobs:
     # given the documented WSL git-object-corruption risk). Runs in
     # parallel with `check`; both must pass.
     runs-on: ubuntu-latest
+    # 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

.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@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Initialize CodeQL
+        uses: github/codeql-action/init@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3
+        with:
+          languages: ${{ matrix.language }}
+          build-mode: ${{ matrix.build-mode }}
+
+      - name: Perform CodeQL Analysis
+        uses: github/codeql-action/analyze@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3
+        with:
+          category: "/language:${{ matrix.language }}"

.github/workflows/governance.yml

@@ -30,4 +30,8 @@ permissions:
 
 jobs:
   governance:
-    uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@main
+    # 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

.github/workflows/hypatia-scan.yml

@@ -43,6 +43,9 @@ jobs:
   scan:
     name: Hypatia Neurosymbolic Analysis
     runs-on: ubuntu-latest
+    # 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

.github/workflows/scorecard.yml

@@ -8,9 +8,18 @@ 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
     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

.hypatia-ignore

@@ -0,0 +1,35 @@
+# SPDX-License-Identifier: MPL-2.0
+#
+# .hypatia-ignore — per-rule scanner exemptions for echo-types.
+#
+# Format (one entry per line; `#` for comments):
+#   <rule_module>/<rule_type>:<path-fragment>
+# The path fragment is substring-matched against each finding's
+# repo-relative path. Consumed by the Hypatia scanner
+# (lib/hypatia/scanner_suppression.ex). Only content-pattern rule
+# modules (e.g. code_safety) are routed through this suppression path;
+# structural rules (workflow_audit / honest_completion / scorecard) are
+# not, and must be addressed by a real fix or an upstream rule change.
+#
+# Each entry below is a verified FALSE POSITIVE. Real findings are not
+# silenced here.
+
+# ── code_safety/agda_postulate on Smoke.agda — FALSE POSITIVE ──────────────
+# The rule is a naive `\bpostulate\b` regex over raw file content that does
+# NOT strip comments. The only "postulate" tokens in Smoke.agda are in
+# COMMENTS documenting the suite's postulate-free discipline ("Zero
+# postulates", "never a postulate", "no funext"); there is no `postulate`
+# declaration. The repo's own guardrail tools/check-guardrails.sh strips
+# comments before checking and passes — it is the real gate (a genuine
+# postulate in Smoke.agda would fail it). The single real postulate in
+# proofs/agda (EchoImageFactorizationPropPostulated.agda) is isolated,
+# guardrail-exempt by design, and not imported by All.agda or Smoke.agda.
+# Upstream fix: agda_postulate should strip comments (see PR notes).
+code_safety/agda_postulate:proofs/agda/Smoke.agda
+
+# ── code_safety/js_http_url_in_code on build-banner.mjs — FALSE POSITIVE ───
+# The flagged `http://` is the SVG XML namespace identifier
+# `xmlns="http://www.w3.org/2000/svg"` — a constant namespace URI that is
+# never dereferenced over the network. It MUST remain http:// (changing it
+# to https would be semantically wrong and break SVG handling). Not CWE-319.
+code_safety/js_http_url_in_code:tools/banner/build-banner.mjs