fix(agda): resolve the two unsolved metas in EchoHaplotypeCollapsing (#329)

[hyperpolymath]

Measured

• Agda on main has been red since 1f67753 (PR feat(applications): haplotype collapsing as Echo fiber #327, 2026-09-27): agda -i proofs/agda proofs/agda/All.agda dies with exit 42, "Unsolved metas" at proofs/agda/EchoHaplotypeCollapsing.agda:153,17-33 and :159,33-49, both aggregate-values countAggregator ….
• Reproduced locally, verbatim, before touching anything: agda 2.6.4.3 (/usr/bin/agda), agda-stdlib v2.3 (shallow clone), absolute-zero pinned 3ff5cee7f3fd002378089cd02f0c90a3747b45f0 — the exact pins agda.yml uses — invoked exactly as CI does (agda -i proofs/agda proofs/agda/All.agda from the repo root, with ~/.agda/libraries/defaults built the same way the "Register libraries for Agda" step builds them).

/…/proofs/agda/All.agda:101,1-36
Unsolved metas at the following locations:
  /…/proofs/agda/EchoHaplotypeCollapsing.agda:153,17-33
  /…/proofs/agda/EchoHaplotypeCollapsing.agda:159,33-49
when scope checking the declaration
  open import EchoHaplotypeCollapsing

Root cause

countAggregator : ∀ {K V : Set} → GroupAggregator K V sumMonoid (EchoAggregation.agda). K — the group-by key — is genuinely phantom: GroupAggregator's only field, agg : V → Monoid.Elem M, never mentions K, and countAggregator = record { agg = λ _ → 1 } doesn't either. aggregate-values's type doesn't pin K down from V, M, or the result type either. So at both call sites (aggregate-values countAggregator example-clones / … cs) nothing in scope determines K — it's not merely "hard to infer", there is no information anywhere that fixes it, so Agda leaves it as an unsolved meta.

Change

Supply K explicitly as Haplotype at both sites — the key this module actually groups clones by (the "Count clones per haplotype … (the GROUP BY analogue)" comment right above count-clones-per-haplotype names it), so this is the semantically honest choice, not an arbitrary placeholder:

-example-count : aggregate-values countAggregator example-clones ≡ 2
+example-count : aggregate-values {K = Haplotype} countAggregator example-clones ≡ 2
 example-count = refl

 -- Count clones per haplotype via monoid fold (the GROUP BY analogue).
 -- In production: groupByKey + fold, not filter + length, to stay O(n).
 count-clones-per-haplotype : List Clone → ℕ
-count-clones-per-haplotype cs = aggregate-values countAggregator cs
+count-clones-per-haplotype cs = aggregate-values {K = Haplotype} countAggregator cs

No postulates, no pragmas, no holes, EchoHaplotypeCollapsing stays imported from All.agda exactly as before.

Evidence

Before (unfixed, verbatim):

/…/proofs/agda/All.agda:101,1-36
Unsolved metas at the following locations:
  /…/proofs/agda/EchoHaplotypeCollapsing.agda:153,17-33
  /…/proofs/agda/EchoHaplotypeCollapsing.agda:159,33-49
when scope checking the declaration
  open import EchoHaplotypeCollapsing

After (fixed), the CI check job's full recipe, run locally against the same pins — every step exits 0 with no "Unsolved"/"error" text:

• agda -i proofs/agda proofs/agda/All.agda — RC=0
• agda -i proofs/agda proofs/agda/Smoke.agda — RC=0
• agda -i proofs/agda proofs/agda/characteristic/All.agda — RC=0
• agda -i proofs/agda proofs/agda/examples/All.agda — RC=0
• agda -i proofs/agda proofs/agda/EchoImageFactorizationPropCubical.agda — RC=0

Mutant: reverted only the example-count site back to aggregate-values countAggregator example-clones (leaving count-clones-per-haplotype fixed) and re-ran agda -i proofs/agda proofs/agda/All.agda:

RC=42
/…/proofs/agda/All.agda:101,1-36 (via Smoke.agda:885,13-36)
Unsolved metas at the following locations:
  /…/proofs/agda/EchoHaplotypeCollapsing.agda:153,17-33

Exactly the mutated line reappears as unsolved; count-clones-per-haplotype (line 159/167 post-fix) does not. File then restored byte-identical to the fixed version (cmp clean) before committing.

#328's startup_failure (run 36357715429)

Not an actions.lock/uses: mismatch. The run page's own annotation is unambiguous:

Error — Actor is not allowed to trigger Actions workflows. Workflow file: .github/workflows/agda.yml.

And it's not Agda-specific: on that same head (6044971, PR #328 by arena-ai-coding-agent), every GitHub-Actions-triggered workflow — CodeQL Security Analysis, Governance, Secret Scanner, Hypatia Security Scan, and Agda — recorded STARTUP_FAILURE with status: COMPLETED (confirmed via GraphQL checkSuites on the PR's head commit). A per-workflow lock/uses: defect would not take down five unrelated workflows identically; a repo/org Actions policy refusing to run workflows for that actor on a pull_request event explains all five at once. That's a caller-side actor-permission gate, not something fixable inside agda.yml — filing #330 with acceptance criteria rather than guessing at a workflow-file change with no evidence behind it.

Acceptance criteria (#329)

1. agda.yml green on main at the curing commit, both jobs (cold-check, check), EchoHaplotypeCollapsing still imported from All.agda, metas resolved by supplying the argument — done, evidence above.
2. The curing PR's own Agda run is green before merge — pending this PR's CI (polling below); local reproduction of both jobs' full recipes is clean.
3. The startup_failure on fix(agda): restore main typecheck — carry the fiber invariant in FiberBundle #328's head explained and, if a lock/uses: mismatch, fixed here; otherwise documented as a caller defect with its own issue — explained above, filed as arena-ai-coding-agent PRs get zero CI signal: all 5 Actions workflows STARTUP_FAILURE (actor not allowed to trigger workflows) — #328 merged on this #330 (actor-permission gate, not a lock/uses: mismatch, so out of scope for this PR).

🤖 Generated with Claude Code

https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57

[coderabbitai]

Navigate logical layers of code changes, visualize relationships, and explore their blast radius.

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: d5d92941-f527-4de5-b2af-9eab15b600d5

📥 Commits

Reviewing files that changed from the base of the PR and between 39a7a99 and 56b8189.

📒 Files selected for processing (1)

• proofs/agda/EchoHaplotypeCollapsing.agda

Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.

📜 Recent review details

⏰ Context from checks skipped due to timeout. (18)

• GitHub Check: governance / Debt ratchet
• GitHub Check: governance / Code quality + docs
• GitHub Check: governance / Workflow security linter
• GitHub Check: governance / Trusted-base reduction policy
• GitHub Check: governance / Live Actions policy (credentialed advisory)
• GitHub Check: governance / Language / package anti-pattern policy
• GitHub Check: governance / Guix packaging policy (Nix retired)
• GitHub Check: governance / Check Workflow Staleness
• GitHub Check: governance / Well-Known (RFC 9116 + RSR)
• GitHub Check: governance / Actions lockfile verify
• GitHub Check: governance / Exemption ratchet
• GitHub Check: governance / Licence consistency
• GitHub Check: scan / gitleaks
• GitHub Check: analyze (actions, none)
• GitHub Check: check
• GitHub Check: cold-check
• GitHub Check: Hypatia Neurosymbolic Analysis
• GitHub Check: semgrep-cloud-platform/scan

⚠️ CI failures not shown inline (6)

GitHub Actions: Secret Scanner / 0_scan _ gitleaks.txt: fix(agda): resolve the two unsolved metas in EchoHaplotypeCollapsing (#329)

Conclusion: failure

View job details

##[group]Run set -euo pipefail
 �[36;1mset -euo pipefail�[0m
 �[36;1m�[0m
 �[36;1m# A repo-local baseline wins outright — it is expected to `[extend]`�[0m
 �[36;1m# the estate one, so "wins" still means "inherits". This mirrors what�[0m
 �[36;1m# the AsciiDoc pass below already did, which was inconsistent with�[0m
 �[36;1m# this step until now.�[0m
 �[36;1mCONFIG=".gitleaks-estate.toml"�[0m
 �[36;1mif [ -f .gitleaks.toml ]; then�[0m
 �[36;1m  CONFIG=".gitleaks.toml"�[0m
 �[36;1m  echo "Using repository .gitleaks.toml (extending the estate baseline)."�[0m
 �[36;1melse�[0m
 �[36;1m  echo "Using estate baseline allowlist."�[0m
 �[36;1mfi�[0m
 �[36;1m�[0m
 �[36;1m"$RUNNER_TEMP/gitleaks" detect \�[0m
 �[36;1m  --source . \�[0m
 �[36;1m  --no-git \�[0m
 �[36;1m  --redact \�[0m
 �[36;1m  --no-banner \�[0m
 �[36;1m  --verbose \�[0m
 �[36;1m  --config "$CONFIG" \�[0m
 �[36;1m  --exit-code 1�[0m
 shell: /usr/bin/bash -e {0}
 ##[endgroup]
 Using estate baseline allowlist.
 Finding:     authoritative-text = "�[1;3;mREDACTED�[0m § Observation G"
 ***REDACTED_SECRET_ASSIGNMENT***
 RuleID:      generic-api-key
 Entropy:     3.576618
 File:        .machine_readable/6a2/STATE.a2ml
 Line:        261
 Fingerprint: .machine_readable/6a2/STATE.a2ml:generic-api-key:261
 �[90m11:00AM�[0m �[32mINF�[0m scan completed in 257ms
 �[90m11:00AM�[0m �[31mWRN�[0m leaks found: 1
 ##[error]Process completed with exit code 1.

---

GitHub Actions: Secret Scanner / scan _ gitleaks: fix(agda): resolve the two unsolved metas in EchoHaplotypeCollapsing (#329)

Conclusion: failure

View job details

##[group]Run set -euo pipefail
 �[36;1mset -euo pipefail�[0m
 �[36;1m�[0m
 �[36;1m# A repo-local baseline wins outright — it is expected to `[extend]`�[0m
 �[36;1m# the estate one, so "wins" still means "inherits". This mirrors what�[0m
 �[36;1m# the AsciiDoc pass below already did, which was inconsistent with�[0m
 �[36;1m# this step until now.�[0m
 �[36;1mCONFIG=".gitleaks-estate.toml"�[0m
 �[36;1mif [ -f .gitleaks.toml ]; then�[0m
 �[36;1m  CONFIG=".gitleaks.toml"�[0m
 �[36;1m  echo "Using repository .gitleaks.toml (extending the estate baseline)."�[0m
 �[36;1melse�[0m
 �[36;1m  echo "Using estate baseline allowlist."�[0m
 �[36;1mfi�[0m
 �[36;1m�[0m
 �[36;1m"$RUNNER_TEMP/gitleaks" detect \�[0m
 �[36;1m  --source . \�[0m
 �[36;1m  --no-git \�[0m
 �[36;1m  --redact \�[0m
 �[36;1m  --no-banner \�[0m
 �[36;1m  --verbose \�[0m
 �[36;1m  --config "$CONFIG" \�[0m
 �[36;1m  --exit-code 1�[0m
 shell: /usr/bin/bash -e {0}
 ##[endgroup]
 Using estate baseline allowlist.
 Finding:     authoritative-text = "�[1;3;mREDACTED�[0m § Observation G"
 ***REDACTED_SECRET_ASSIGNMENT***
 RuleID:      generic-api-key
 Entropy:     3.576618
 File:        .machine_readable/6a2/STATE.a2ml
 Line:        261
 Fingerprint: .machine_readable/6a2/STATE.a2ml:generic-api-key:261
 �[90m11:00AM�[0m �[32mINF�[0m scan completed in 257ms
 �[90m11:00AM�[0m �[31mWRN�[0m leaks found: 1
 ##[error]Process completed with exit code 1.

---

GitHub Actions: Secret Scanner / 1_scan _ rust-secrets.txt: fix(agda): resolve the two unsolved metas in EchoHaplotypeCollapsing (#329)

Conclusion: failure

View job details

##[group]Run TODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}"
 �[36;1mTODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}"�[0m
 �[36;1m�[0m
 �[36;1m# An unparseable cutoff would pick the warn branch forever, silently�[0m
 �[36;1m# disarming the widened scan. Refuse to run instead.�[0m
 �[36;1mrequire_date() {�[0m
 �[36;1m  case "$2" in�[0m
 �[36;1m    [0-9][0-9][0-9][0-9]-[0-1][0-9]-[0-3][0-9]) : ;;�[0m
 �[36;1m    *) echo "::error::rust-secrets: $1='$2' is not YYYY-MM-DD."�[0m

---

GitHub Actions: Secret Scanner / scan _ rust-secrets: fix(agda): resolve the two unsolved metas in EchoHaplotypeCollapsing (#329)

Conclusion: failure

View job details

##[group]Run TODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}"
 �[36;1mTODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}"�[0m
 �[36;1m�[0m
 �[36;1m# An unparseable cutoff would pick the warn branch forever, silently�[0m
 �[36;1m# disarming the widened scan. Refuse to run instead.�[0m
 �[36;1mrequire_date() {�[0m
 �[36;1m  case "$2" in�[0m
 �[36;1m    [0-9][0-9][0-9][0-9]-[0-1][0-9]-[0-3][0-9]) : ;;�[0m
 �[36;1m    *) echo "::error::rust-secrets: $1='$2' is not YYYY-MM-DD."�[0m

---

GitHub Actions: Secret Scanner / 2_scan _ shell-secrets.txt: fix(agda): resolve the two unsolved metas in EchoHaplotypeCollapsing (#329)

Conclusion: failure

View job details

##[group]Run # Patterns: an `export FOO=` or `FOO=` with a quoted literal of meaningful length.
 �[36;1m# Patterns: an `export FOO=` or `FOO=` with a quoted literal of meaningful length.�[0m
 �[36;1m# Restricted to *_TOKEN / *_KEY / *_SECRET / PASSWORD to keep false-positives low.�[0m
 �[36;1mPATTERNS=(�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*TOKEN[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{20,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*API_KEY[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{20,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*SECRET[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{16,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?***"'"'"'][^"'"'"']{6,}["'"'"']'�[0m
 �[36;1m)�[0m
 �[36;1m�[0m
 �[36;1m# Inline pragma patterns — suppress a hit when found on the same or�[0m
 �[36;1m# immediately preceding line.�[0m
 �[36;1mPRAGMA_RE='(scanner-allow:[[:space:]]*shell-secrets|hypatia:[[:space:]]*allow[[:space:]]+security_errors/secret_detected)'�[0m
 �[36;1m�[0m
 �[36;1m# Param-expansion RHS pattern — assignments whose value is a variable�[0m
 �[36;1m# reference rather than a literal are never real secrets.�[0m
 �[36;1m# Matches: ="$VAR"  ="${VAR}"  ="${VAR:-…}"  ="${VAR:?…}"  ='${VAR}'  =$VAR�[0m
 �[36;1mPARAM_EXPANSION_RE='=['"'"'"'"'"']?\$\{?[A-Za-z_][A-Za-z0-9_]*(:[?-][^}]*)?\}?['"'"'"'"'"']?[[:space:]]*(#.*)?$'�[0m
 �[36;1m�[0m
 �[36;1m# Load per-repo ignore globs from .shell-secrets-ignore if present.�[0m
 �[36;1mIGNORE_GLOBS=()�[0m
 �[36;1mif [[ -f .shell-secrets-ignore ]]; then�[0m
 �[36;1m  while IFS= read -r line || [[ -n "$line" ]]; do�[0m
 �[36;1m    # Skip blank lines and comments�[0m
 �[36;1m    [[ -z "$line" || "$line" == \#* ]] && continue�[0m
 �[36;1m    IGNORE_GLOBS+=("$line")�[0m
 �[36;1m  done < .shell-secrets-ignore�[0m
 �[36;1mfi�[0m
 �[36;1m�[0m
 �[36;1m# is_ignored <filepath> — returns 0 (true) if path matches any ignore glob.�[0m
 �[36;1mis_ignored() {�[0m
 �[36;1m  local path="$1"�[0m
 �[36;1m  for glob in "${IGNORE_GLOBS[@]}"; do�[0m
 �[36;1m    #...

---

GitHub Actions: Secret Scanner / scan _ shell-secrets: fix(agda): resolve the two unsolved metas in EchoHaplotypeCollapsing (#329)

Conclusion: failure

View job details

##[group]Run # Patterns: an `export FOO=` or `FOO=` with a quoted literal of meaningful length.
 �[36;1m# Patterns: an `export FOO=` or `FOO=` with a quoted literal of meaningful length.�[0m
 �[36;1m# Restricted to *_TOKEN / *_KEY / *_SECRET / PASSWORD to keep false-positives low.�[0m
 �[36;1mPATTERNS=(�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*TOKEN[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{20,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*API_KEY[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{20,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?[A-Z_]*SECRET[A-Z_]*=["'"'"'][A-Za-z0-9_./+=-]{16,}["'"'"']'�[0m
 �[36;1m  '(export[[:space:]]+)?***"'"'"'][^"'"'"']{6,}["'"'"']'�[0m
 �[36;1m)�[0m
 �[36;1m�[0m
 �[36;1m# Inline pragma patterns — suppress a hit when found on the same or�[0m
 �[36;1m# immediately preceding line.�[0m
 �[36;1mPRAGMA_RE='(scanner-allow:[[:space:]]*shell-secrets|hypatia:[[:space:]]*allow[[:space:]]+security_errors/secret_detected)'�[0m
 �[36;1m�[0m
 �[36;1m# Param-expansion RHS pattern — assignments whose value is a variable�[0m
 �[36;1m# reference rather than a literal are never real secrets.�[0m
 �[36;1m# Matches: ="$VAR"  ="${VAR}"  ="${VAR:-…}"  ="${VAR:?…}"  ='${VAR}'  =$VAR�[0m
 �[36;1mPARAM_EXPANSION_RE='=['"'"'"'"'"']?\$\{?[A-Za-z_][A-Za-z0-9_]*(:[?-][^}]*)?\}?['"'"'"'"'"']?[[:space:]]*(#.*)?$'�[0m
 �[36;1m�[0m
 �[36;1m# Load per-repo ignore globs from .shell-secrets-ignore if present.�[0m
 �[36;1mIGNORE_GLOBS=()�[0m
 �[36;1mif [[ -f .shell-secrets-ignore ]]; then�[0m
 �[36;1m  while IFS= read -r line || [[ -n "$line" ]]; do�[0m
 �[36;1m    # Skip blank lines and comments�[0m
 �[36;1m    [[ -z "$line" || "$line" == \#* ]] && continue�[0m
 �[36;1m    IGNORE_GLOBS+=("$line")�[0m
 �[36;1m  done < .shell-secrets-ignore�[0m
 �[36;1mfi�[0m
 �[36;1m�[0m
 �[36;1m# is_ignored <filepath> — returns 0 (true) if path matches any ignore glob.�[0m
 �[36;1mis_ignored() {�[0m
 �[36;1m  local path="$1"�[0m
 �[36;1m  for glob in "${IGNORE_GLOBS[@]}"; do�[0m
 �[36;1m    #...

---

📝 Summary

Summary by CodeRabbit

• Documentation
  • The haplotype-counting example now explicitly identifies the grouping key used for aggregation. Its demonstrated result remains 2, and the counting function continues to return the aggregate count for a list of clones. These clarifications do not change the example’s output or the counting behaviour.

Walkthrough

The Agda example and counting function now pass Haplotype explicitly as the group key to countAggregator. The example’s expected result remains 2.

Changes

Haplotype counting

Layer / File(s)	Summary
Explicit haplotype group key proofs/agda/EchoHaplotypeCollapsing.agda	Comments explain why Agda cannot infer the phantom group key. example-count and count-clones-per-haplotype now pass Haplotype to countAggregator.

Priority: ⬇️ Low

Estimated code review effort: 2 (Simple) | ~5 minutes

Change: Bug fix

Merge Risk: ⚪ Minimal · up to 56b81

The change resolves the ambiguous aggregation key without changing counting behavior. No actionable merge-blocking risk remains after normal checks.

Architecture Summary

Architecture risk: 🔵 Low · up to 56b81

The change affects 1 system.

Changed systems: proofs

Architecture concerns
No architecture-level concerns identified.

Review details

Systems and components

• observed — proofs (service) was modified; 1 changed file maps to changed impact.

Before / after behavior

• observed — Modified behavior in proofs/agda/EchoHaplotypeCollapsing.agda: example-count now supplies Haplotype as the explicit group key to countAggregator; its expected result remains 2.
• observed — Modified behavior in proofs/agda/EchoHaplotypeCollapsing.agda: Comments now document that the group key is phantom in GroupAggregator and countAggregator, so Agda cannot infer it, and identify Haplotype as the key used here.
• observed — Modified behavior in proofs/agda/EchoHaplotypeCollapsing.agda: count-clones-per-haplotype now supplies Haplotype as the explicit group key when aggregating clones.

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title clearly identifies the Agda fix and the two unsolved metas addressed by the changes.
Description check	✅ Passed	The description is directly related to the changeset. It explains the root cause, the explicit Haplotype key, validation evidence, and the scope of the workflow issue.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff. Analyzed 0 functions across 0…
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

✨ Finishing Touches 💡 1

🛠️ Fix failing CI checks 💡

• Commit to this branch
• Create a new PR

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{A rabbit checks the counting key,
And sets Haplotype explicitly.
Two clones hop into the sum,
The example says the count is two.
Then off the rabbit bounds anew.}

_{Comment @coderabbitai help to get the list of available commands.}

[github-actions]

🔍 Hypatia Security Scan

Findings: 56 issues detected

Severity	Count
🔴 Critical	6
🟠 High	15
🟡 Medium	35

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": "label-triage.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage"
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": "labels.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync"
  },
  {
    "reason": "Required file missing (condition: public_repo)",
    "type": "missing_requirement",
    "file": "SECURITY.md",
    "action": "create",
    "rule_module": "cicd_rules",
    "severity": "high"
  },
  {
    "line": 39,
    "reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/labels.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "warn"
  },
  {
    "line": 46,
    "reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/push-email-notify.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "warn"
  },
  {
    "line": 87,
    "reason": "job in .github/workflows/hypatia-scan.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/hypatia-scan.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "warn"
  },
  {
    "line": 53,
    "reason": "job in .github/workflows/label-triage.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/label-triage.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "warn"
  },
  {
    "line": 34,
    "reason": "workflow .github/workflows/labels.yml:34 job `sync` has no `timeout-minutes:` — defaults to 360 min on hang",
    "type": "WH006",
    "file": ".github/workflows/labels.yml",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "warn"
  },
  {
    "line": 48,
    "reason": "workflow .github/workflows/label-triage.yml:48 job `triage` has no `timeout-minutes:` — defaults to 360 min on hang",
    "type": "WH006",
    "file": ".github/workflows/label-triage.yml",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "warn"
  },
  {
    "line": 27,
    "reason": "workflow .github/workflows/scorecard.yml:27 uses `secrets: inherit` — forwards every caller secret to the reusable workflow",
    "type": "WH008",
    "file": ".github/workflows/scorecard.yml",
    "action": "report",
    "rule_module": "workflow_hardening",
    "severity": "warn"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence

[hyperpolymath]

This PR's only red is Secret Scanner / scan / gitleaks. That finding is a generic-api-key false positive in .machine_readable/6a2/STATE.a2ml, a line reading authoritative-text = ... § Observation G. The same false positive is red on main.

#332 deletes that file under the owner's 2026-09-30 ruling. Its own red is the Agda metas this PR fixes. So each PR cures the other's red.

#332 is now rebased onto this PR's head 56b8189. It will land with a merge commit once every check is green. This commit then reaches main unchanged and GitHub marks this PR merged. #329 closes only after the Agda run on the merge commit on main is green.

🤖 Generated with Claude Code

https://claude.ai/code/session_01QYY8Gp4v4x2J7iSNn1vZ57