spec: Darwin cache population and a requireable Darwin PR gate (#795, #785)

[NickSeagull]

Gate 1 — spec only. The diff is the contract: docs/changes/007-darwin-cache-population-and-pr-gating.md + ADR-0075. No implementation, no workflow edits yet.

Closes the aarch64-darwin cache gap that #795 step 1–2 and #785 both report, in one coherent caching change. Scope is broad per gate nh-5rh (Nick, 2026-08-17): this change owns both the CI dev-shell closure and the released-neo consumer closure. #795 AC4–AC6 (scheduled flake updates, cadence, auto-merge policy) stay with nh-5dz / #810.

What the spec promises

1. test-macos.yml pushes the aarch64-darwin dev-shell closure — via a new cachix-push-macos job gated at job level on push + exact refs/heads/main + same repository. The token is never materialized in a job that runs PR-controlled code (GitHub won't let secrets be read from a step-level if:, so the honest-skip idiom needs a job-level env: — hence a separate job, following the cache-populate / check_release_rehearsal precedent).
2. Push paths: gain flake.nix + flake.lock — otherwise the one event that invalidates the whole Darwin cache is the one event that never repopulates it.
3. A Darwin PR gate that can actually be required — no workflow-level paths: on pull_request, diff-scoping in a changes job, and an if: always() test-macos-gate aggregate. Third instance of the neo-ci-gate / installer-ci-gate pattern. core/** is deliberately out of PR scope.
4. neo-ci.yml's cache-populate gains an aarch64-apple-darwin leg (matrix, fail-fast: false, both ./dev neo-consumer-contract and ./dev cache-prime retained per leg, trust guard untouched) — the Neo onboarding SLO misses Cachix and exceeds 600s on clean runners #785 half.
5. scripts/workflow-check freezes the new credential surface — check_test_macos() plus matrix assertions on check_cache_populate(). test-macos.yml is referenced nowhere else in the repo and is about to hold a secret; every other token-bearing workflow already has a freeze check.

Criteria

12 criteria: C1–C7 unit (all provable in CI on this PR, via ./dev workflow-check --self-test fixtures with a mutation per clause), C8–C12 integration (operational evidence — post-merge run pairs and an SLO dispatch evidence artifact). Each names the exact artifact that discharges it.

The spec enumerates the full event space (fork PR / same-repo PR / draft / push main / push elsewhere / dispatch) as the token-isolation argument, nine failure modes (F-1…F-9), and four concurrency cases (X-1…X-4). No property-based criterion applies, and the spec says why: the contract is a finite set of static assertions over a fixed YAML document, and the one quantified claim ranges over a closed six-element event space, so C2 discharges it exhaustively.

Two things a maintainer must decide or do

• Branch protection: test-macos-gate must be marked a required check, or Flake inputs are unmanaged and drifting — close the macOS cache gap before automating updates #795 AC3 ships as decoration. Agents can't change repo settings.
• Security review routing gap: ci-cd carries no security-sensitive tag, so ./dev spec-check --plan routed no design review for a change that moves a cache-write credential onto a new runner platform. That's a gap in the tagging, not a clearance — the spec requests a manual neohaskell-security-design-review (local-only record, ADR-0069) and recommends tagging ci-cd as a follow-up.

Known residual (named, not hidden)

cache-prime primes the closure of the neo built from the branch; the SLO measures a released neo pinned to its own embedded compatibility revision. If those differ, cachix.observed_use stays false on both platforms no matter how much is pushed (F-9). Diagnosis path is in the spec; the fix is a separate change to cache-prime.

Gates

• ./dev spec-check — OK (8 specs valid)
• ./dev spec-check --criteria-tests origin/main — OK
• ./dev spec-drift — OK (empty signature delta; no Haskell surface)
• ./dev adr-check — OK (75 ADRs indexed)
• ./dev workflow-check — OK (17 workflows)

Continue signal: a maintainer @claude comment approving the spec.

🤖 Generated with Claude Code

[coderabbitai]

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Path: .coderabbit.yaml

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: de8dcb04-61d3-4481-8f3a-30b2bccb8d9c

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

---

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

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

[NickSeagull]

Closing: this spec draft belongs to the retired pre-ADR-0075 process (20-step formula, draft-PR spec gate). The beads state was reset and the change process rebuilt (#837) — if this work is still wanted, it re-enters as a fresh request through the change formula v2.