Formalize §4.6 effective-integrity model with executable compliance tests

pkg/workflow/github_mcp_effective_integrity_formal_test.go

@@ -0,0 +1,309 @@
+//go:build !integration
+
+package workflow
+
+import (
+	"slices"
+	"strings"
+	"testing"
+
+	"github.com/stretchr/testify/assert"
+)
+
+type formalIntegrityItem struct {
+	AuthorLogin   string
+	BaseIntegrity string
+	Labels        []string
+}
+
+type formalIntegrityGuardConfig struct {
+	BlockedUsers   []string
+	TrustedUsers   []string
+	ApprovalLabels []string
+	MinIntegrity   string
+}
+
+type formalIntegrityDecision struct {
+	allow     bool
+	errorCode int
+}
+
+func TestFormal_BlockedTerminatesElevation(t *testing.T) {
+	cfg := formalIntegrityGuardConfig{
+		BlockedUsers:   []string{"bad-actor"},
+		TrustedUsers:   []string{"bad-actor"},
+		ApprovalLabels: []string{"human-reviewed"},
+		MinIntegrity:   "none",
+	}
+	item := formalIntegrityItem{AuthorLogin: "bad-actor", BaseIntegrity: "none", Labels: []string{"human-reviewed"}}
+
+	effective := formalEffectiveIntegrity(item, cfg)
+	decision := formalIntegrityAccessDecision(item, cfg)
+
+	assert.Equal(t, "blocked", effective)
+	assert.False(t, decision.allow)
+	assert.Equal(t, formalErrorBlockedUser, decision.errorCode)
+}
+
+func TestFormal_TrustedUserElevatesToApproved(t *testing.T) {
+	cfg := formalIntegrityGuardConfig{TrustedUsers: []string{"trusted-user"}}
+
+	assert.Equal(t, "approved", formalEffectiveIntegrity(formalIntegrityItem{AuthorLogin: "trusted-user", BaseIntegrity: "none"}, cfg))
+	assert.Equal(t, "approved", formalEffectiveIntegrity(formalIntegrityItem{AuthorLogin: "trusted-user", BaseIntegrity: "unapproved"}, cfg))
+	assert.Equal(t, "approved", formalEffectiveIntegrity(formalIntegrityItem{AuthorLogin: "trusted-user", BaseIntegrity: "approved"}, cfg))
+	assert.Equal(t, "merged", formalEffectiveIntegrity(formalIntegrityItem{AuthorLogin: "trusted-user", BaseIntegrity: "merged"}, cfg))
+}
+
+func TestFormal_ApprovalLabelElevatesToApproved(t *testing.T) {
+	cfg := formalIntegrityGuardConfig{ApprovalLabels: []string{"human-reviewed"}, MinIntegrity: "approved"}
+	item := formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "unapproved", Labels: []string{"human-reviewed"}}
+
+	assert.Equal(t, "approved", formalEffectiveIntegrity(item, cfg))
+	assert.True(t, formalIntegrityAccessDecision(item, cfg).allow)
+}
+
+func TestFormal_DefaultIsBaseIntegrity(t *testing.T) {
+	cfg := formalIntegrityGuardConfig{}
+	levels := []string{"none", "unapproved", "approved", "merged"}
+
+	for _, level := range levels {
+		t.Run(level, func(t *testing.T) {
+			item := formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: level, Labels: []string{"no-match"}}
+			assert.Equal(t, level, formalEffectiveIntegrity(item, cfg))
+		})
+	}
+}
+
+func TestFormal_ElevationNeverLowersIntegrity(t *testing.T) {
+	levels := []string{"none", "unapproved", "approved", "merged"}
+	configs := []formalIntegrityGuardConfig{
+		{TrustedUsers: []string{"trusted"}},
+		{ApprovalLabels: []string{"human-reviewed"}},
+		{TrustedUsers: []string{"trusted"}, ApprovalLabels: []string{"human-reviewed"}},
+	}
+
+	for _, cfg := range configs {
+		for _, level := range levels {
+			item := formalIntegrityItem{AuthorLogin: "trusted", BaseIntegrity: level, Labels: []string{"human-reviewed"}}
+			effective := formalEffectiveIntegrity(item, cfg)
+			assert.GreaterOrEqual(t, formalEffectiveIntegrityRank(effective), formalEffectiveIntegrityRank(level))
+		}
+	}
+}
+
+func TestFormal_IntegrityAccessDecisionTable(t *testing.T) {
+	cases := []struct {
+		name          string
+		cfg           formalIntegrityGuardConfig
+		item          formalIntegrityItem
+		wantIntegrity string
+		wantAllow     bool
+		wantCode      int
+	}{
+		{
+			name:          "blocked user denied regardless of label",
+			cfg:           formalIntegrityGuardConfig{BlockedUsers: []string{"spam-bot"}, ApprovalLabels: []string{"human-reviewed"}, MinIntegrity: "none"},
+			item:          formalIntegrityItem{AuthorLogin: "spam-bot", BaseIntegrity: "merged", Labels: []string{"human-reviewed"}},
+			wantIntegrity: "blocked",
+			wantAllow:     false,
+			wantCode:      formalErrorBlockedUser,
+		},
+		{
+			name:          "trusted user elevates and passes min approved",
+			cfg:           formalIntegrityGuardConfig{TrustedUsers: []string{"partner"}, MinIntegrity: "approved"},
+			item:          formalIntegrityItem{AuthorLogin: "partner", BaseIntegrity: "none"},
+			wantIntegrity: "approved",
+			wantAllow:     true,
+		},
+		{
+			name:          "approval label elevates and passes min approved",
+			cfg:           formalIntegrityGuardConfig{ApprovalLabels: []string{"human-reviewed"}, MinIntegrity: "approved"},
+			item:          formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "unapproved", Labels: []string{"human-reviewed"}},
+			wantIntegrity: "approved",
+			wantAllow:     true,
+		},
+		{
+			name:          "no elevation fails min approved",
+			cfg:           formalIntegrityGuardConfig{MinIntegrity: "approved"},
+			item:          formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "unapproved"},
+			wantIntegrity: "unapproved",
+			wantAllow:     false,
+			wantCode:      formalErrorIntegrityTooLow,
+		},
+		{
+			name:          "merged remains merged and passes min merged",
+			cfg:           formalIntegrityGuardConfig{TrustedUsers: []string{"maintainer"}, MinIntegrity: "merged"},
+			item:          formalIntegrityItem{AuthorLogin: "maintainer", BaseIntegrity: "merged"},
+			wantIntegrity: "merged",
+			wantAllow:     true,
+		},
+	}
+
+	for _, tc := range cases {
+		t.Run(tc.name, func(t *testing.T) {
+			effective := formalEffectiveIntegrity(tc.item, tc.cfg)
+			decision := formalIntegrityAccessDecision(tc.item, tc.cfg)
+
+			assert.Equal(t, tc.wantIntegrity, effective)
+			assert.Equal(t, tc.wantAllow, decision.allow)
+			if !tc.wantAllow {
+				assert.Equal(t, tc.wantCode, decision.errorCode)
+			}
+		})
+	}
+}
+
+func TestFormal_EmptyTrustedUsersAndLabelsTreatedAsOmitted(t *testing.T) {
+	cfg := formalIntegrityGuardConfig{TrustedUsers: []string{}, ApprovalLabels: []string{}, MinIntegrity: "approved"}
+	item := formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "unapproved", Labels: []string{"human-reviewed"}}
+
+	assert.Equal(t, "unapproved", formalEffectiveIntegrity(item, cfg))
+	decision := formalIntegrityAccessDecision(item, cfg)
+	assert.False(t, decision.allow)
+	assert.Equal(t, formalErrorIntegrityTooLow, decision.errorCode)
+}
+
+func TestFormal_CaseInsensitiveUserMatching(t *testing.T) {
+	blockedCfg := formalIntegrityGuardConfig{BlockedUsers: []string{"Bad-Actor"}, MinIntegrity: "none"}
+	blockedItem := formalIntegrityItem{AuthorLogin: "bad-actor", BaseIntegrity: "merged"}
+
+	assert.Equal(t, "blocked", formalEffectiveIntegrity(blockedItem, blockedCfg))
+	assert.False(t, formalIntegrityAccessDecision(blockedItem, blockedCfg).allow)
+
+	trustedCfg := formalIntegrityGuardConfig{TrustedUsers: []string{"Trusted-Partner"}, MinIntegrity: "approved"}
+	trustedItem := formalIntegrityItem{AuthorLogin: "trusted-partner", BaseIntegrity: "none"}
+
+	assert.Equal(t, "approved", formalEffectiveIntegrity(trustedItem, trustedCfg))
+	assert.True(t, formalIntegrityAccessDecision(trustedItem, trustedCfg).allow)
+}
+
+func TestFormal_UnsetMinIntegrityAlwaysAllowsNonBlocked(t *testing.T) {
+	cfg := formalIntegrityGuardConfig{BlockedUsers: []string{"blocked"}}
+
+	assert.True(t, formalIntegrityAccessDecision(formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "none"}, cfg).allow)
+	assert.True(t, formalIntegrityAccessDecision(formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "unapproved"}, cfg).allow)
+	assert.True(t, formalIntegrityAccessDecision(formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "approved"}, cfg).allow)
+	assert.True(t, formalIntegrityAccessDecision(formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "merged"}, cfg).allow)
+
+	blocked := formalIntegrityAccessDecision(formalIntegrityItem{AuthorLogin: "blocked", BaseIntegrity: "merged"}, cfg)
+	assert.False(t, blocked.allow)
+	assert.Equal(t, formalErrorBlockedUser, blocked.errorCode)
+}
+
+func TestFormal_EffectiveIntegrity_InvalidMinIntegrityConfigDenied(t *testing.T) {
+	cfg := formalIntegrityGuardConfig{MinIntegrity: "invalid"}
+	item := formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "merged"}
+
+	decision := formalIntegrityAccessDecision(item, cfg)
+	assert.False(t, decision.allow)
+	assert.Equal(t, formalErrorIntegrityTooLow, decision.errorCode)
+}
+
+func TestFormal_UnknownBaseIntegrityDefaultsToNone(t *testing.T) {
+	cfg := formalIntegrityGuardConfig{MinIntegrity: "approved"}
+	item := formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "unknown-level"}
+
+	assert.Equal(t, "none", formalEffectiveIntegrity(item, cfg))
+	decision := formalIntegrityAccessDecision(item, cfg)
+	assert.False(t, decision.allow)
+	assert.Equal(t, formalErrorIntegrityTooLow, decision.errorCode)
+}
+
+func TestFormal_CaseInsensitiveApprovalLabelMatching(t *testing.T) {
+	cfg := formalIntegrityGuardConfig{ApprovalLabels: []string{"Human-Reviewed"}, MinIntegrity: "approved"}
+	item := formalIntegrityItem{AuthorLogin: "external", BaseIntegrity: "none", Labels: []string{"human-reviewed"}}
+
+	assert.Equal(t, "approved", formalEffectiveIntegrity(item, cfg))
+	assert.True(t, formalIntegrityAccessDecision(item, cfg).allow)
+}
+
+func formalEffectiveIntegrity(item formalIntegrityItem, cfg formalIntegrityGuardConfig) string {
+	if formalContainsFold(cfg.BlockedUsers, item.AuthorLogin) {
+		return "blocked"
+	}
+
+	effectiveRank := formalEffectiveIntegrityRank(item.BaseIntegrity)
+	if effectiveRank < 0 {
+		effectiveRank = formalEffectiveIntegrityRank("none")
+	}
+
+	if formalContainsFold(cfg.TrustedUsers, item.AuthorLogin) {
+		effectiveRank = max(effectiveRank, formalEffectiveIntegrityRank("approved"))
+	}
+	if formalIntersectsFold(cfg.ApprovalLabels, item.Labels) {
+		effectiveRank = max(effectiveRank, formalEffectiveIntegrityRank("approved"))
+	}
+
+	return formalIntegrityLevelFromRank(effectiveRank)
+}
+
+func formalIntegrityAccessDecision(item formalIntegrityItem, cfg formalIntegrityGuardConfig) formalIntegrityDecision {
+	effective := formalEffectiveIntegrity(item, cfg)
+	if effective == "blocked" {
+		return formalIntegrityDecision{allow: false, errorCode: formalErrorBlockedUser}
+	}
+
+	if strings.TrimSpace(cfg.MinIntegrity) == "" {
+		return formalIntegrityDecision{allow: true}
+	}
+
+	minRank := formalEffectiveIntegrityRank(cfg.MinIntegrity)
+	if minRank < 0 {
+		return formalIntegrityDecision{allow: false, errorCode: formalErrorIntegrityTooLow}
+	}
+	if formalEffectiveIntegrityRank(effective) < minRank {
+		return formalIntegrityDecision{allow: false, errorCode: formalErrorIntegrityTooLow}
+	}
+
+	return formalIntegrityDecision{allow: true}
+}
+
+func formalEffectiveIntegrityRank(level string) int {
+	switch strings.ToLower(strings.TrimSpace(level)) {
+	case "none":
+		return 0
+	case "unapproved":
+		return 1
+	case "approved":
+		return 2
+	case "merged":
+		return 3
+	default:
+		return -1
+	}
+}
+
+func formalIntegrityLevelFromRank(rank int) string {
+	switch rank {
+	case 3:
+		return "merged"
+	case 2:
+		return "approved"
+	case 1:
+		return "unapproved"
+	case 0:
+		return "none"
+	default:
+		return "none"
+	}
+}
+
+func formalContainsFold(values []string, needle string) bool {
+	return slices.ContainsFunc(values, func(value string) bool {
+		return strings.EqualFold(strings.TrimSpace(value), strings.TrimSpace(needle))
+	})
+}
+
+func formalIntersectsFold(a, b []string) bool {
+	normalized := make(map[string]struct{}, len(b))
+	for _, right := range b {
+		normalized[strings.ToLower(strings.TrimSpace(right))] = struct{}{}
+	}
+
+	for _, left := range a {
+		if _, ok := normalized[strings.ToLower(strings.TrimSpace(left))]; ok {
+			return true
+		}
+	}
+	return false
+}

specs/github-mcp-access-control-compliance/README.md

@@ -46,6 +46,10 @@ Where:
 
 The denial code is selected by the first failing guard in the evaluation order above.
 
+The integrity evaluator in §4.6 (effective integrity computation for `trusted-users` and
+`approval-labels`, with `blocked-users` precedence) is modeled separately in
+`pkg/workflow/github_mcp_effective_integrity_formal_test.go`.
+
 ## Behavioral Coverage Map
 
 | Predicate / Invariant | Test Function | Description |
@@ -66,6 +70,20 @@ The denial code is selected by the first failing guard in the evaluation order a
 | `SAFETY_NoSpuriousAllow` | `TestFormal_NoSpuriousAllowInvariant` | Safety: no allow decision when any guard fails |
 | `P5_NotBlocked + P6_IntegrityMet` (combined) | `TestFormal_FixtureRunner` | P5 fires before P6 in evaluation order; blocked user denied with -32005 even when P6 would also fail; scenarios executed dynamically by the fixture runner |
 
+### Effective Integrity Model Coverage (§4.6)
+
+| Predicate / Invariant | Test Function | Description |
+|---|---|---|
+| `EQ1_BlockedTerminates` / `PREC1_BlockedOverTrusted` | `TestFormal_BlockedTerminatesElevation` | Blocked author always gets effective integrity `blocked`, even with trusted-user and approval-label matches |
+| `EQ2_TrustedElevatesToApproved` | `TestFormal_TrustedUserElevatesToApproved` | Trusted-user base integrity is elevated to at least `approved` and never lowered from `merged` |
+| `EQ3_LabelElevatesToApproved` | `TestFormal_ApprovalLabelElevatesToApproved` | Approval label elevates to `approved` before `min-integrity` is checked |
+| `EQ4_DefaultIsBase` | `TestFormal_DefaultIsBaseIntegrity` | No blocked/trusted/label match leaves base integrity unchanged |
+| `MONO_ElevationNeverLowers` | `TestFormal_ElevationNeverLowersIntegrity` | Trusted-user / approval-label elevation is monotonic via `max()` |
+| `DECISION_AccessDecision` | `TestFormal_IntegrityAccessDecisionTable` | Table-driven access decision cases for blocked/trusted/label/default combinations |
+| Edge case: empty arrays | `TestFormal_EmptyTrustedUsersAndLabelsTreatedAsOmitted` | Empty (non-nil) `trusted-users` and `approval-labels` behave as omitted |
+| Edge case: case-insensitive matching | `TestFormal_CaseInsensitiveUserMatching`, `TestFormal_CaseInsensitiveApprovalLabelMatching` | `blocked-users`, `trusted-users`, and `approval-labels` matching is case-insensitive |
+| Edge case: unset `min-integrity` | `TestFormal_UnsetMinIntegrityAlwaysAllowsNonBlocked` | Unset `min-integrity` allows all non-blocked content; blocked users are still denied |
+
 ## Fixture Files
 
 | Filename | Scenario | Spec Coverage |
@@ -128,7 +146,9 @@ and no error is returned.
 
 ## Usage
 
-1. Copy or verify the test file at `pkg/workflow/github_mcp_access_control_formal_test.go`.
+1. Copy or verify the test files:
+   - `pkg/workflow/github_mcp_access_control_formal_test.go`
+   - `pkg/workflow/github_mcp_effective_integrity_formal_test.go`
 2. No stub interfaces are needed — all types and helpers are self-contained in the file.
 3. Run predicate-mapped tests:
 
@@ -148,9 +168,12 @@ Formal conformance tests are implemented in:
 
 `pkg/workflow/github_mcp_access_control_formal_test.go`
 
+`pkg/workflow/github_mcp_effective_integrity_formal_test.go`
+
 The test suite includes:
 - **Predicate-mapped tests** (`TestFormal_*`) — each test maps to a specific guard predicate (P1–P6) or invariant documented in the Formal Model section above.
 - **Fixture runner** (`TestFormal_FixtureRunner`) — loads every YAML fixture file from this directory and drives each scenario through the formal evaluator. This ensures the fixture files, error codes, and expected decisions remain consistent with the formal model.
+- **Effective integrity model tests** (`TestFormal_*` in `github_mcp_effective_integrity_formal_test.go`) — formalizes §4.6 precedence and elevation semantics for `blocked-users`, `trusted-users`, and `approval-labels`.
 
 The `combined-blocked-integrity.yaml` fixture verifies that the runner returns P5's `-32005`
 before P6's `-32006` when both guards fail.