ci: resolve Hypatia findings at source (dependabot, scorecard perms, false-positive suppressions)

Foundational, in-repo remediation so the advisory Hypatia scan stops
re-flagging known issues:

Real fixes (close genuine findings):
- Add .github/dependabot.yml (github-actions ecosystem, weekly) — closes
  the OSSF Scorecard "Dependency-Update-Tool" / DependencyUpdate finding.
  Scoped to github-actions only: echo-types has no Cargo/npm/mix/pip
  manifests, and Dependabot has no native Nix ecosystem.
- scorecard.yml: grant the analysis job the permissions the
  scorecard-reusable contract documents (contents:read, security-events:
  write, id-token:write) — closes scorecard_wrapper_missing_job_permissions.

Verified false positives, suppressed via the sanctioned .hypatia-ignore
mechanism (code_safety rules route through ScannerSuppression):
- code_safety/agda_postulate on proofs/agda/Smoke.agda (the "critical"):
  the rule is a naive \bpostulate\b regex with no comment stripping; the
  only matches are comments documenting the postulate-free discipline.
  The repo guardrail (check-guardrails.sh) strips comments and is the
  real gate; the one real postulate module is isolated and not in the
  trusted base.
- code_safety/js_http_url_in_code on tools/banner/build-banner.mjs:
  the URL is the SVG XML namespace `xmlns="http://www.w3.org/2000/svg"`,
  a constant namespace URI, never fetched (must stay http://).

Not fixable in-repo (upstream rule/standards-reusable issues; documented
in the PR for follow-up): honest_completion/no_tests (Agda proof suite
not recognised as tests) and workflow_audit/missing_timeout_minutes on
reusable-workflow callers (timeout-minutes is invalid on `uses:` jobs;
the real fix is adding timeouts inside the standards reusables and making
the rule skip caller jobs).

https://claude.ai/code/session_01Jxr3Wy4ngpkbc2QwjEam82

Author: claude

.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/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

.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