ci: require the monad-execution pin to be on execution main

[maxkozlovsky]

Problem

The monad-execution gitlink is a bare commit SHA, and nothing in git makes it follow a branch. Two ways that goes wrong today, neither caught before merge:

• The commit stops existing. Pin an execution PR head, that branch gets force-pushed or deleted, and the commit is orphaned. GitHub keeps serving orphans until GC, so the breakage surfaces weeks later as git submodule update failing for everyone on master. category-labs/monad merges by rebase, which makes this the expected path rather than an edge case: merging an execution PR rewrites its commits, so a pin taken from a PR head is permanently unreachable from main afterwards.
• The commit goes backwards. A gitlink has no readable diff, so a mistaken conflict resolution can resurrect an older pin. Reachability checks can't see this — the older pin is a perfectly valid commit on execution main.

What this adds

exec-pin.sh, run by exec-pin.yml, reads the gitlink in HEAD and requires both:

1. Reachability — the pin is identical/behind execution main.
2. Progression — the pin is not behind the pin already on master.

Both go through the GitHub API, so no submodule checkout is needed — deliberate, since a recursive checkout dies on precisely the unfetchable pin the job exists to report. Failures separate "the pin is wrong" from "the check could not run": only a definitive 404 is reported as a missing commit, and gh's stderr is kept in the log.

Rationale, including why the off-the-shelf action can't serve as a required check here, is in docs/0004_submodule_pin_gating.md.

Testing

There are no automated tests — the repo has no shell-test infrastructure, and .github/workflows/license.sh is the untested-merge-gate precedent this mirrors. CI cannot exercise the classification logic either, so it was driven by hand against real SHAs in throwaway repos. Each case and the behaviour it pins down:

Case	Expected
Pin on execution main	pass, reports how far behind tip
Head of an open execution PR	fail, names the PR
Head of a merged PR (rebase-orphaned)	fail, names the merge_commit_sha to re-pin to
Commit merged into a non-main execution branch	fail, names that branch
Force-push orphan (no PR claims it)	fail, says it will be GC'd
Unknown SHA	fail, "does not exist"
Bad token / bad EXEC_BASE / API error	CI fault, not blamed on the pin
Pin unchanged / moved forward / moved backward	skip / pass / fail
git ls-tree fails, or gitlink moved to another path	fail closed (earlier revision passed green here)
$GITHUB_STEP_SUMMARY unwritable	good pin still exits 0

Not verifiable locally, and the reason this is worth one careful look in review: the merge_group path, and that the CI GITHUB_TOKEN rather than a personal PAT can read category-labs/monad. Both are public repos and contents: read should suffice, but the first real run is the proof.

Follow-up

This only has teeth once Execution pin is added as a required status check on master — a branch-protection change, not in this PR. It is written to work in the merge queue (it never parses the event payload), which is why it carries a merge_group trigger.

Independent of #3266 (Dependabot submodule bumps); either can merge first.

🤖 Generated with Claude Code

[Copilot]

🟡 Changes recommended

Unresolved critical and moderate findings affect the reliability and integrity of the pin-validation gate.

Get a fresh assessment by requesting another Copilot review.

Pull request overview

Adds CI gating to ensure the monad-execution submodule pin is reachable from execution main and does not regress.

Changes:

• Adds API-based pin validation.
• Runs checks for pull requests and merge queues.
• Documents the gating design and failure modes.

File summaries

File	Description
docs/0004_submodule_pin_gating.md	Documents the pin-gating policy and rationale.
.github/workflows/exec-pin.yml	Runs validation for pull requests and merge queues.
.github/workflows/exec-pin.sh	Validates pin reachability, progression, and diagnostics.

Review details

Suppressed comments (2)

.github/workflows/exec-pin.sh:165

• other includes closed, unmerged PRs as well as PRs merged into another branch, so this message says the pin “belongs to no execution PR” while listing one. For a closed unmerged PR, that wording and the subsequent force-push/GC explanation are misleading; describe it as belonging to an execution PR that was not merged into the selected base.

    fail "$path is pinned to $short, which is not on $EXEC_REPO $EXEC_BASE and was never merged there." \
        "$(printf '%s\n' "It belongs to:" "$other" "" \
            "Re-pin to a commit on $EXEC_BASE.")"

.github/workflows/exec-pin.sh:89

• The progression baseline is read at the current PR path. If a PR changes .gitmodules to move the gitlink, git ls-tree FETCH_HEAD -- "$path" finds no pin on master, and lines 60–62 warn and allow the PR to proceed; an older valid execution commit can therefore bypass the rollback check. Reject an unexpected path change or compare the base branch's original path instead of treating a missing baseline as success.

url=$(git config -f .gitmodules --get "submodule.$SUBMODULE.url") || url=
path=$(git config -f .gitmodules --get "submodule.$SUBMODULE.path") || path=

• Files reviewed: 3/3 changed files
• Comments generated: 5
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.