(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")
}
Summary
The
specs/github-mcp-access-control-compliance/README.mdfixture 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 howtrusted-usersandapproval-labelsinteract withblocked-usersandmin-integrityto 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
specs/github-mcp-access-control-compliance/README.md(cross-referencing §4.4.6, §4.4.7, §4.6 ofscratchpad/github-mcp-access-control-specification.md, pinned at commit2c1cfd71010a2d1ab9d9149118beb076d2098d7d)trusted-users/approval-labels/blocked-usersprecedence and elevation semantics)Formal Model
Predicates and invariants (illustrative notation)
Each predicate is annotated with its source paragraph in §4.6.2/§4.6.3 of the normative specification. The integrity hierarchy is:
Behavioral Coverage Map
EQ1_BlockedTerminates/PREC1_BlockedOverTrustedTestFormal_BlockedTerminatesElevationblocked, even if also intrusted-userswith a matching approval labelEQ2_TrustedElevatesToApprovedTestFormal_TrustedUserElevatesToApprovedapproved; never lowered frommergedEQ3_LabelElevatesToApprovedTestFormal_ApprovalLabelElevatesToApprovedapproved; applies before themin-integritycheckEQ4_DefaultIsBaseTestFormal_DefaultIsBaseIntegrityMONO_ElevationNeverLowersTestFormal_ElevationNeverLowersIntegritymax()never produces a level below the item's baseDECISION_AccessDecisionTestFormal_IntegrityAccessDecisionTableTestFormal_EmptyTrustedUsersAndLabelsTreatedAsOmittedtrusted-users/approval-labelsarrays behave as if omitted — no elevationTestFormal_CaseInsensitiveUserMatchingblocked-usersandtrusted-usersmatching is case-insensitivemin-integrityTestFormal_UnsetMinIntegrityAlwaysAllowsNonBlockedmin-integrityconfigured, any non-blocked level is allowed; blocked users still deniedGenerated Test Suite
📄 `pkg/workflow/github_mcp_effective_integrity_formal_test.go`
Usage
pkg/workflow/github_mcp_effective_integrity_formal_test.go(already created in this repository during this run).contentItem/integrityGuardConfigstub types with real implementation types once thetrusted-users/approval-labelseffective-integrity computation is wired into the gateway (currently only parsed and passed through as env vars incompiler_github_mcp_steps.go; no runtime evaluator exists yet).go test ./pkg/workflow/... -run TestFormal_Context
specs/github-mcp-access-control-compliance/README.md(cross-referencingscratchpad/github-mcp-access-control-specification.md§4.4.6, §4.4.7, §4.6)github_mcp_access_control_formal_test.gofully covered guards P1–P6, but this run identified that the effective-integrity computation (§4.6) involvingtrusted-usersandapproval-labelselevation was not yet formalized or tested — closed with this new test file.Warning
Firewall blocked 1 domain
The following domain was blocked by the firewall during workflow execution:
proxy.golang.orgTo allow these domains, add them to the
network.allowedlist in your workflow frontmatter:See Network Configuration for more information.