[formal-spec] github-mcp-access-control-compliance/README.md — Formal model & test suite — 2026-08-14

[github-actions]

Summary

The specs/github-mcp-access-control-compliance/README.md fixture directory already has a complete, executable formal test suite (github_mcp_access_control_formal_test.go, 542 lines) covering the six access guards (P1–P6) and their combined/error-code invariants. However, the effective integrity computation algorithm defined in §4.6 of the normative specification (scratchpad/github-mcp-access-control-specification.md) — which governs how trusted-users and approval-labels interact with blocked-users and min-integrity to derive an item's effective trust level — is not yet covered by any executable test. This run formalizes §4.6 (Integrity Level Model) and generates a new, self-contained Go testify suite closing that gap.

Specification

• File: specs/github-mcp-access-control-compliance/README.md (cross-referencing §4.4.6, §4.4.7, §4.6 of scratchpad/github-mcp-access-control-specification.md, pinned at commit 2c1cfd71010a2d1ab9d9149118beb076d2098d7d)
• Focus area: Effective integrity computation (trusted-users / approval-labels / blocked-users precedence and elevation semantics)
• Formal notation used: TLA+ / Z3-style guard conjunction (illustrative)

Formal Model

Predicates and invariants (illustrative notation)

EQ1_BlockedTerminates(item) ≜
  author(item) ∈ blocked-users ⇒ EffectiveIntegrity(item) = blocked
  (§4.6.2 step 2: terminates; cannot be overridden by trusted-users or approval-labels)

EQ2_TrustedElevatesToApproved(item) ≜
  author(item) ∉ blocked-users ∧ author(item) ∈ trusted-users
    ⇒ EffectiveIntegrity(item) = max(base(item), approved)
  (§4.6.2 step 3)

EQ3_LabelElevatesToApproved(item) ≜
  author(item) ∉ blocked-users ∧ author(item) ∉ trusted-users ∧ labels(item) ∩ approval-labels ≠ ∅
    ⇒ EffectiveIntegrity(item) = max(base(item), approved)
  (§4.6.2 step 4)

EQ4_DefaultIsBase(item) ≜
  author(item) ∉ blocked-users ∧ author(item) ∉ trusted-users ∧ labels(item) ∩ approval-labels = ∅
    ⇒ EffectiveIntegrity(item) = base(item)
  (§4.6.2 step 5)

MONO_ElevationNeverLowers(item) ≜
  EffectiveIntegrity(item) ≥ base(item)
  (§4.6.2 note: steps 3-4 only raise; an item already at merged stays at merged)

PREC1_BlockedOverTrusted(item) ≜
  author(item) ∈ blocked-users ∧ author(item) ∈ trusted-users ⇒ EffectiveIntegrity(item) = blocked
  (§4.6.2: step 2 precedes steps 3-4; blocked-users cannot be promoted)

DECISION_AccessDecision(item, minIntegrity) ≜
  EffectiveIntegrity(item) = blocked ⇒ DENY ∧
  (minIntegrity set ∧ EffectiveIntegrity(item) < minIntegrity) ⇒ DENY ∧
  otherwise ⇒ ALLOW
  (§4.6.3)

Each predicate is annotated with its source paragraph in §4.6.2/§4.6.3 of the normative specification. The integrity hierarchy is:

blocked (-1) < none (0) < unapproved (1) < approved (2) < merged (3)

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
EQ1_BlockedTerminates / PREC1_BlockedOverTrusted	TestFormal_BlockedTerminatesElevation	Blocked author's effective integrity is always blocked, even if also in trusted-users with a matching approval label
EQ2_TrustedElevatesToApproved	TestFormal_TrustedUserElevatesToApproved	Trusted-user's base integrity raised to at least approved; never lowered from merged
EQ3_LabelElevatesToApproved	TestFormal_ApprovalLabelElevatesToApproved	Matching approval label elevates to approved; applies before the min-integrity check
EQ4_DefaultIsBase	TestFormal_DefaultIsBaseIntegrity	No blocked/trusted/label match leaves base integrity unchanged, across all four levels
MONO_ElevationNeverLowers	TestFormal_ElevationNeverLowersIntegrity	Trusted-users and approval-labels elevation via max() never produces a level below the item's base
DECISION_AccessDecision	TestFormal_IntegrityAccessDecisionTable	Table-driven test reproducing the five worked examples from the §4.6.3 decision table
Edge case: empty arrays	TestFormal_EmptyTrustedUsersAndLabelsTreatedAsOmitted	Empty (non-nil) trusted-users/approval-labels arrays behave as if omitted — no elevation
Edge case: case-insensitive matching	TestFormal_CaseInsensitiveUserMatching	blocked-users and trusted-users matching is case-insensitive
Edge case: unset min-integrity	TestFormal_UnsetMinIntegrityAlwaysAllowsNonBlocked	With no min-integrity configured, any non-blocked level is allowed; blocked users still denied

Generated Test Suite

📄 `pkg/workflow/github_mcp_effective_integrity_formal_test.go`

(go/redacted):build !integration

// Formal conformance tests for the effective-integrity computation model defined in
// scratchpad/github-mcp-access-control-specification.md §4.6 (Integrity Level Model),
// cross-referenced by specs/github-mcp-access-control-compliance/README.md.
//
// This file formalizes and tests the interaction between `trusted-users`,
// `approval-labels`, and `blocked-users` when computing an item's effective integrity
// level, which is NOT covered by github_mcp_access_control_formal_test.go (that file
// only tests the already-computed ContentIntegrity value against min-integrity).
//
// Formal predicates encoded (illustrative TLA+ / Z3-style notation):
//
//   EQ1_BlockedTerminates(item) ≜
//     author(item) ∈ blocked-users ⇒ EffectiveIntegrity(item) = blocked
//     (§4.6.2 step 2: terminates; cannot be overridden by trusted-users or approval-labels)
//
//   EQ2_TrustedElevatesToApproved(item) ≜
//     author(item) ∉ blocked-users ∧ author(item) ∈ trusted-users
//       ⇒ EffectiveIntegrity(item) = max(base(item), approved)
//     (§4.6.2 step 3)
//
//   EQ3_LabelElevatesToApproved(item) ≜
//     author(item) ∉ blocked-users ∧ author(item) ∉ trusted-users ∧ labels(item) ∩ approval-labels ≠ ∅
//       ⇒ EffectiveIntegrity(item) = max(base(item), approved)
//     (§4.6.2 step 4)
//
//   EQ4_DefaultIsBase(item) ≜
//     author(item) ∉ blocked-users ∧ author(item) ∉ trusted-users ∧ labels(item) ∩ approval-labels = ∅
//       ⇒ EffectiveIntegrity(item) = base(item)
//     (§4.6.2 step 5)
//
//   MONO_ElevationNeverLowers(item) ≜
//     EffectiveIntegrity(item) ≥ base(item)
//     (§4.6.2 note: steps 3-4 only raise; an item already at merged stays at merged)
//
//   PREC1_BlockedOverTrusted(item) ≜
//     author(item) ∈ blocked-users ∧ author(item) ∈ trusted-users ⇒ EffectiveIntegrity(item) = blocked
//     (§4.6.2 note: step 2 precedes steps 3-4)
//
//   PREC2_TrustedOverLabel(item) ≜
//     author(item) ∈ trusted-users ⇒ approval-labels are not separately consulted
//     (§4.6.2: steps evaluated in order; step 3 short-circuits before step 4)
//
//   DECISION_AccessDecision(item, minIntegrity) ≜
//     EffectiveIntegrity(item) = blocked ⇒ DENY ∧
//     (minIntegrity set ∧ EffectiveIntegrity(item) < minIntegrity) ⇒ DENY ∧
//     otherwise ⇒ ALLOW
//     (§4.6.3)
package workflow_test

import (
	"testing"

	"github.com/stretchr/testify/assert"
)

// integrityLevel models the total order defined in §4.6.1:
//
//	blocked (-1) < none (0) < unapproved (1) < approved (2) < merged (3)
type integrityLevel int

const (
	integrityBlocked    integrityLevel = -1
	integrityNone       integrityLevel = 0
	integrityUnapproved integrityLevel = 1
	integrityApproved   integrityLevel = 2
	integrityMerged     integrityLevel = 3
)

// contentItem is a stub — replace with real implementation. It models the minimal
// shape of a GitHub content item (issue, PR, comment) relevant to integrity
// computation, per §4.6.2.
type contentItem struct {
	author string
	labels []string
	base   integrityLevel
}

// integrityGuardConfig is a stub — replace with real implementation. It mirrors the
// `blocked-users`, `trusted-users`, `approval-labels`, and `min-integrity` gateway
// fields described in §§4.4.4-4.4.7.
type integrityGuardConfig struct {
	blockedUsers  []string
	trustedUsers  []string
	approvalLabel []string
	minIntegrity  *integrityLevel // nil means "not set"
}

func containsFold(values []string, needle string) bool {
	for _, v := range values {
		if strings_EqualFold(v, needle) {
			return true
		}
	}
	return false
}

// strings_EqualFold avoids importing "strings" twice under different aliases across
// this test file; a thin wrapper keeps the predicate definitions above self-contained.
func strings_EqualFold(a, b string) bool {
	if len(a) != len(b) {
		return false
	}
	for i := 0; i < len(a); i++ {
		ca, cb := a[i], b[i]
		if 'A' <= ca && ca <= 'Z' {
			ca += 'a' - 'A'
		}
		if 'A' <= cb && cb <= 'Z' {
			cb += 'a' - 'A'
		}
		if ca != cb {
			return false
		}
	}
	return true
}

func hasAnyLabel(itemLabels, approvalLabels []string) bool {
	for _, l := range itemLabels {
		if containsFold(approvalLabels, l) {
			return true
		}
	}
	return false
}

func maxIntegrity(a, b integrityLevel) integrityLevel {
	if a > b {
		return a
	}
	return b
}

// computeEffectiveIntegrity implements the §4.6.2 algorithm:
//
//	1. Start with the item's base integrity level.
//	2. IF author ∈ blocked-users: effective ← blocked (terminates).
//	3. ELSE IF author ∈ trusted-users: effective ← max(base, approved).
//	4. ELSE IF any label ∈ approval-labels: effective ← max(base, approved).
//	5. ELSE: effective ← base.
func computeEffectiveIntegrity(item contentItem, cfg integrityGuardConfig) integrityLevel {
	if containsFold(cfg.blockedUsers, item.author) {
		return integrityBlocked
	}
	if containsFold(cfg.trustedUsers, item.author) {
		return maxIntegrity(item.base, integrityApproved)
	}
	if hasAnyLabel(item.labels, cfg.approvalLabel) {
		return maxIntegrity(item.base, integrityApproved)
	}
	return item.base
}

// evaluateIntegrityDecision implements the §4.6.3 access decision rule.
func evaluateIntegrityDecision(effective integrityLevel, minIntegrity *integrityLevel) bool {
	if effective == integrityBlocked {
		return false
	}
	if minIntegrity != nil && effective < *minIntegrity {
		return false
	}
	return true
}

func approvedPtr() *integrityLevel {
	l := integrityApproved
	return &l
}

func nonePtr() *integrityLevel {
	l := integrityNone
	return &l
}

// TestFormal_BlockedTerminatesElevation verifies EQ1_BlockedTerminates and
// PREC1_BlockedOverTrusted: a blocked author's effective integrity is always
// `blocked`, even if the same author also appears in trusted-users or the item
// bears an approval label.
func TestFormal_BlockedTerminatesElevation(t *testing.T) {
	cfg := integrityGuardConfig{
		blockedUsers:  []string{"bot"},
		trustedUsers:  []string{"bot"}, // same user in both lists (§4.6.2 precedence test)
		approvalLabel: []string{"approved"},
	}
	item := contentItem{author: "bot", labels: []string{"approved"}, base: integrityMerged}

	got := computeEffectiveIntegrity(item, cfg)
	assert.Equal(t, integrityBlocked, got, "blocked-users must terminate evaluation regardless of trusted-users or approval-labels membership")
	assert.False(t, evaluateIntegrityDecision(got, approvedPtr()), "a blocked effective integrity must always deny, independent of min-integrity")
}

// TestFormal_TrustedUserElevatesToApproved verifies EQ2_TrustedElevatesToApproved:
// a non-blocked author in trusted-users has their base integrity raised to at
// least `approved`.
func TestFormal_TrustedUserElevatesToApproved(t *testing.T) {
	cfg := integrityGuardConfig{trustedUsers: []string{"contractor-1"}}

	cases := []struct {
		name string
		base integrityLevel
		want integrityLevel
	}{
		{"below approved is raised", integrityNone, integrityApproved},
		{"unapproved is raised", integrityUnapproved, integrityApproved},
		{"already approved stays approved", integrityApproved, integrityApproved},
		{"merged is not lowered", integrityMerged, integrityMerged},
	}

	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			item := contentItem{author: "contractor-1", base: tc.base}
			got := computeEffectiveIntegrity(item, cfg)
			assert.Equal(t, tc.want, got, "trusted-users elevation must raise base=%v to at least approved, never lower it", tc.base)
		})
	}
}

// TestFormal_ApprovalLabelElevatesToApproved verifies EQ3_LabelElevatesToApproved:
// an item bearing at least one approval-labels entry is raised to `approved`,
// applied before the min-integrity check (§4.4.7).
func TestFormal_ApprovalLabelElevatesToApproved(t *testing.T) {
	cfg := integrityGuardConfig{approvalLabel: []string{"human-reviewed", "safe-to-process"}}

	elevated := computeEffectiveIntegrity(contentItem{author: "alice", labels: []string{"human-reviewed"}, base: integrityNone}, cfg)
	assert.Equal(t, integrityApproved, elevated, "an item with a matching approval label must be elevated to approved")

	notElevated := computeEffectiveIntegrity(contentItem{author: "alice", labels: []string{"unrelated-label"}, base: integrityNone}, cfg)
	assert.Equal(t, integrityNone, notElevated, "an item without a matching approval label keeps its base integrity")

	// Elevation must happen before the min-integrity check succeeds (§4.4.7: "applies before the min-integrity check").
	minApproved := approvedPtr()
	assert.True(t, evaluateIntegrityDecision(elevated, minApproved), "a label-elevated item must satisfy min-integrity: approved even though its base was none")
}

// TestFormal_DefaultIsBaseIntegrity verifies EQ4_DefaultIsBase: when an author is
// neither blocked nor trusted, and no approval label is present, the effective
// integrity equals the item's base integrity unchanged.
func TestFormal_DefaultIsBaseIntegrity(t *testing.T) {
	cfg := integrityGuardConfig{}
	for _, base := range []integrityLevel{integrityNone, integrityUnapproved, integrityApproved, integrityMerged} {
		item := contentItem{author: "regular-user", base: base}
		got := computeEffectiveIntegrity(item, cfg)
		assert.Equal(t, base, got, "with no blocked/trusted/label configuration, effective integrity must equal base integrity")
	}
}

// TestFormal_ElevationNeverLowersIntegrity verifies MONO_ElevationNeverLowers: the
// trusted-users and approval-labels elevation paths use max() and can never
// decrease an item's integrity level below its base.
func TestFormal_ElevationNeverLowersIntegrity(t *testing.T) {
	trustedCfg := integrityGuardConfig{trustedUsers: []string{"vip"}}
	labelCfg := integrityGuardConfig{approvalLabel: []string{"reviewed"}}

	bases := []integrityLevel{integrityNone, integrityUnapproved, integrityApproved, integrityMerged}
	for _, base := range bases {
		trustedItem := contentItem{author: "vip", base: base}
		assert.GreaterOrEqual(t, int(computeEffectiveIntegrity(trustedItem, trustedCfg)), int(base),
			"trusted-users elevation must never produce a level below the item's base (base=%v)", base)

		labelItem := contentItem{author: "someone", labels: []string{"reviewed"}, base: base}
		assert.GreaterOrEqual(t, int(computeEffectiveIntegrity(labelItem, labelCfg)), int(base),
			"approval-labels elevation must never produce a level below the item's base (base=%v)", base)
	}
}

// TestFormal_IntegrityAccessDecisionTable verifies DECISION_AccessDecision using the
// worked examples from §4.6.3's decision table.
func TestFormal_IntegrityAccessDecisionTable(t *testing.T) {
	cases := []struct {
		name         string
		cfg          integrityGuardConfig
		item         contentItem
		minIntegrity *integrityLevel
		wantAllow    bool
	}{
		{
			name:         "label promotion satisfies min-integrity approved",
			cfg:          integrityGuardConfig{approvalLabel: []string{"approved"}},
			item:         contentItem{author: "alice", labels: []string{"approved"}, base: integrityNone},
			minIntegrity: approvedPtr(),
			wantAllow:    true,
		},
		{
			name:         "blocked user denied even with matching approval label",
			cfg:          integrityGuardConfig{blockedUsers: []string{"bot"}, approvalLabel: []string{"approved"}},
			item:         contentItem{author: "bot", labels: []string{"approved"}, base: integrityNone},
			minIntegrity: approvedPtr(),
			wantAllow:    false,
		},
		{
			name:         "no elevation, base below min-integrity denied",
			cfg:          integrityGuardConfig{},
			item:         contentItem{author: "alice", base: integrityNone},
			minIntegrity: approvedPtr(),
			wantAllow:    false,
		},
		{
			name:         "min-integrity none allows base none",
			cfg:          integrityGuardConfig{},
			item:         contentItem{author: "alice", base: integrityNone},
			minIntegrity: nonePtr(),
			wantAllow:    true,
		},
		{
			name:         "merged already exceeds approved via label promotion",
			cfg:          integrityGuardConfig{approvalLabel: []string{"approved"}},
			item:         contentItem{author: "alice", labels: []string{"merged"}, base: integrityMerged},
			minIntegrity: approvedPtr(),
			wantAllow:    true,
		},
	}

	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			effective := computeEffectiveIntegrity(tc.item, tc.cfg)
			got := evaluateIntegrityDecision(effective, tc.minIntegrity)
			assert.Equal(t, tc.wantAllow, got, "%s: decision mismatch (effective=%v)", tc.name, effective)
		})
	}
}

// TestFormal_EmptyTrustedUsersAndLabelsTreatedAsOmitted covers an edge case from
// §4.4.6/§4.4.7: an empty (but non-nil) trusted-users or approval-labels array is
// semantically equivalent to omitting the field — no elevation should occur.
func TestFormal_EmptyTrustedUsersAndLabelsTreatedAsOmitted(t *testing.T) {
	cfg := integrityGuardConfig{trustedUsers: []string{}, approvalLabel: []string{}}
	item := contentItem{author: "alice", labels: []string{"any-label"}, base: integrityNone}

	got := computeEffectiveIntegrity(item, cfg)
	assert.Equal(t, integrityNone, got, "empty trusted-users/approval-labels arrays must behave identically to omitted fields (no elevation)")
}

// TestFormal_CaseInsensitiveUserMatching covers an edge case implied by §4.4.5/§4.4.6:
// blocked-users and trusted-users matching is case-insensitive (mirrors §4.4.5
// "Matching is case-insensitive" for blocked-users, applied consistently to trusted-users).
func TestFormal_CaseInsensitiveUserMatching(t *testing.T) {
	blockedCfg := integrityGuardConfig{blockedUsers: []string{"Bad-Actor"}}
	blockedItem := contentItem{author: "bad-actor", base: integrityMerged}
	assert.Equal(t, integrityBlocked, computeEffectiveIntegrity(blockedItem, blockedCfg), "blocked-users matching must be case-insensitive")

	trustedCfg := integrityGuardConfig{trustedUsers: []string{"Contractor-1"}}
	trustedItem := contentItem{author: "contractor-1", base: integrityNone}
	assert.Equal(t, integrityApproved, computeEffectiveIntegrity(trustedItem, trustedCfg), "trusted-users matching must be case-insensitive")
}

// TestFormal_UnsetMinIntegrityAlwaysAllowsNonBlocked covers an edge case: when
// min-integrity is not configured (nil), any non-blocked effective integrity level
// is allowed, regardless of how low the base integrity is.
func TestFormal_UnsetMinIntegrityAlwaysAllowsNonBlocked(t *testing.T) {
	item := contentItem{author: "alice", base: integrityNone}
	got := computeEffectiveIntegrity(item, integrityGuardConfig{})
	assert.True(t, evaluateIntegrityDecision(got, nil), "with no min-integrity configured, a non-blocked item at any base level must be allowed")

	blockedItem := contentItem{author: "bot", base: integrityMerged}
	gotBlocked := computeEffectiveIntegrity(blockedItem, integrityGuardConfig{blockedUsers: []string{"bot"}})
	assert.False(t, evaluateIntegrityDecision(gotBlocked, nil), "blocked-users must deny even when min-integrity is unset")
}

Usage

1. Copy the test file to pkg/workflow/github_mcp_effective_integrity_formal_test.go (already created in this repository during this run).
2. Replace the contentItem / integrityGuardConfig stub types with real implementation types once the trusted-users / approval-labels effective-integrity computation is wired into the gateway (currently only parsed and passed through as env vars in compiler_github_mcp_steps.go; no runtime evaluator exists yet).
3. Run: go test ./pkg/workflow/... -run TestFormal_

Context

• Spec processed: specs/github-mcp-access-control-compliance/README.md (cross-referencing scratchpad/github-mcp-access-control-specification.md §4.4.6, §4.4.7, §4.6)
• Formal notation: TLA+ / Z3-style guard conjunction
• Prior run (2026-07-31) found the existing github_mcp_access_control_formal_test.go fully covered guards P1–P6, but this run identified that the effective-integrity computation (§4.6) involving trusted-users and approval-labels elevation was not yet formalized or tested — closed with this new test file.
• Run: https://github.com/github/gh-aw/actions/runs/31815397994

Warning

Firewall blocked 1 domain

The following domain was blocked by the firewall during workflow execution:

• proxy.golang.org

To allow these domains, add them to the network.allowed list in your workflow frontmatter:

network:
  allowed:
    - defaults
    - "proxy.golang.org"

See Network Configuration for more information.

Generated by 🔬 Daily Formal Spec Verifier · auto · 70 AIC · ⌖ 13.2 AIC · ⊞ 9.9K · ◷

• expires on Aug 21, 2026, 7:46 AM UTC-08:00

[github-actions]

This issue was automatically closed because it expired on 2026-08-21T15:46:55.514Z.

Closed by Workflow