Formal spec alignment for GitHub MCP access-control conformance docs and predicate mapping

[Copilot]

This updates the formal-spec artifacts for GitHub MCP access-control compliance so the documented model, coverage map, and execution instructions stay synchronized with the executable conformance suite. It also corrects a predicate label mismatch in the formal test commentary to match the defined P1–P6 ordering.

• Spec usage contract alignment

  • Replaced the generic “Running Compliance Tests” section with a focused Usage section in specs/github-mcp-access-control-compliance/README.md.
  • Usage now explicitly reflects the formal suite entrypoints and self-contained test-file contract.

• Predicate mapping consistency

  • Corrected the inline predicate reference in TestFormal_OmittedReposAllowAll from P1_RepoMatch to P2_RepoMatch in pkg/workflow/github_mcp_access_control_formal_test.go, matching the formal guard ordering (P1=ToolAllowed, P2=RepoMatch).

Example of the corrected predicate annotation:

func TestFormal_OmittedReposAllowAll(t *testing.T) {
	// P2_RepoMatch: omitted repos field means "no restriction" — all accessible repos are allowed (spec §4.4.1).
	...
}

• Fixes [formal-spec] github-mcp-access-control-compliance/README.md — Formal model & test suite — 2026-07-23 #47632

[github-actions]

🤖 PR Triage

Field	Value
Category	docs
Risk	🟡 Medium
Priority Score	50/100
Recommended Action	batch_review

Score breakdown: Impact 20 + Urgency 15 + Quality 15

Batch: batch-spec-docs with #47637

Rationale: Draft PR updating formal spec for GitHub MCP access-control compliance. Only 2 files (a Go test + README). No CI data. Groups with #47637 for a doc/spec batch review.

Generated by 🔧 PR Triage Agent · sonnet46 · 38.1 AIC · ⌖ 6.75 AIC · ⊞ 5.7K · ◷

[github-actions]

Great work on keeping the formal spec artifacts and conformance suite synchronized! 🎯 This correction to the predicate label mapping (P2_RepoMatch) and the Usage section update in the compliance README are important for maintainability.

Here's one thing that would strengthen this PR:

• Add conformance tests — The predicate mapping correction in TestFormal_OmittedReposAllowAll would benefit from additional test cases to verify the P1–P6 ordering holds across boundary conditions. Consider adding tests that exercise the redefined predicate sequence to ensure the fix is durable.

If you'd like to enhance this, you can assign this prompt to your coding agent:

Add unit tests for the GitHub MCP access-control formal predicate ordering (P1–P6) in pkg/workflow/github_mcp_access_control_formal_test.go.

The tests should verify:
1. P1 (ToolAllowed) evaluation occurs before P2 (RepoMatch)
2. When a repo is omitted, P2_RepoMatch correctly allows all accessible repos
3. The predicate sequence is consistent across all guard conditions

Ensure tests cover both positive cases (predicates pass) and negative cases (predicates fail at the expected stage).

Generated by ✅ Contribution Check · sonnet46 · 63.6 AIC · ⌖ 11 AIC · ⊞ 6.2K · ◷

[github-actions]

🤖 PR Triage — §30057272009

Field	Value
Category	docs
Risk	🟢 Low
Priority Score	28 / 100
Action	⏸ defer
CI	⬜ None (draft)
Review	None
Batch	spec-docs

Score breakdown: Impact 20 + Urgency 5 + Quality 3

Rationale: DRAFT PR. Formal spec alignment docs only. No CI, no reviews. Defer until undrafted and CI passes.

Next action: Undraft, ensure CI passes, then consider merging alongside #47637.

Generated by 🔧 PR Triage Agent · sonnet46 · 35.7 AIC · ⌖ 5.3 AIC · ⊞ 5.7K · ◷

[github-actions]

🧠 Matt Pocock Skills Reviewer has completed the skills-based review. ✅

[github-actions]

✅ Test Quality Sentinel completed test quality analysis.

No new or modified test functions detected. The PR only updates a comment ('P1_RepoMatch' → 'P2_RepoMatch') in an existing test. Test Quality Sentinel skipped.

[github-actions]

✅ PR Code Quality Reviewer completed the code quality review.

[Copilot]

Pull request overview

Aligns formal access-control documentation and predicate annotations with the executable conformance suite.

Changes:

• Updates usage instructions for running formal tests.
• Corrects the repository predicate label from P1 to P2.

Show a summary per file

File	Description
specs/github-mcp-access-control-compliance/README.md	Documents formal suite entrypoints and test-file contract.
pkg/workflow/github_mcp_access_control_formal_test.go	Corrects the omitted-repository predicate annotation.

Review details

Tip

Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

• Files reviewed: 2/2 changed files
• Comments generated: 0
• Review effort level: Medium

[github-actions]

✅ Design Decision Gate 🏗️ completed the design decision gate check.

No ADR enforcement needed: PR does not have the 'implementation' label and has ≤100 new lines of code in business logic directories (default_business_additions=1).

[github-actions]

No blocking issues. The predicate label correction (P1_RepoMatch to P2_RepoMatch) is accurate per the documented ordering (P1=ToolAllowed, P2=RepoMatch), and the README simplification is clean.

🔎 Code quality review by PR Code Quality Reviewer · sonnet46 · 13.2 AIC · ⌖ 4.46 AIC · ⊞ 5.7K
_{Comment /review to run again}

[github-actions]

Review

Changes look correct.

• Predicate fix: P1_RepoMatch → P2_RepoMatch is accurate given the defined ordering (P1=ToolAllowed, P2=RepoMatch).
• README simplification: Replacing the explicit long regex with TestFormal_ prefix is cleaner and future-proof as new tests are added.

Minor note: the removal of the TestValidateGitHubGuardPolicy run instructions from the README reduces discoverability for those §11.1.x tests, but this is a deliberate scope decision and not blocking.

🧵 Reviewed using Impeccable skills by Impeccable Skills Reviewer · sonnet46 · 18.1 AIC · ⌖ 4.49 AIC · ⊞ 5K

[github-actions]

Skills-Based Review 🧠

Applied /grill-with-docs — this is a clean, focused documentation and comment-fix PR. Approving.

📋 Summary

What changed

• Predicate label fix (P1_RepoMatch → P2_RepoMatch in TestFormal_OmittedReposAllowAll): Correctly aligns with the formal guard ordering defined in the spec (P1=ToolAllowed, P2=RepoMatch). Verified against the spec README lines 23–43.
• README simplification: Replaced a fragile exhaustive test-name list with the simpler TestFormal_ prefix pattern, which is less likely to drift as new tests are added.

Positive Highlights

• ✅ Predicate fix is accurate and traceable to the spec definition
• ✅ Simplified go test -run "TestFormal_" pattern is less fragile than the old exhaustive named list
• ✅ Numbered steps in the Usage section improve readability

🧠 Reviewed using Matt Pocock's skills by Matt Pocock Skills Reviewer · sonnet46 · 26.8 AIC · ⌖ 4.55 AIC · ⊞ 6.7K
_{Comment /matt to run again}

[pelikhan]

@copilot run pr-finishser skill

[github-actions]

🎉 This pull request is included in a new release.

Release: v0.83.2