[formal-spec] replace-label-spec.md — Formal model & test suite — 2026-08-07

[github-actions]

Summary

This run formalizes the security/error-handling tail of specs/replace-label-spec.md, the W3C-style specification for the replace-label safe-output type. Most core predicates (schema validation, allow/blocklist evaluation, staged mode, label-set computation, count gate, target resolution, transitions) are already covered by pkg/workflow/replace_label_formal_test.go and pkg/workflow/replace_label_transitions_formal_test.go. This formalization targets the remaining under-tested surface: input sanitization, rate-limit retry semantics, REST label-array correctness, hard-error handling for REST/label-existence failures, server-side-only enforcement of allow/blocklists (agents cannot self-bypass), and minimum token scope requirements.

Specification

• File: specs/replace-label-spec.md
• Focus area: replace-label safe-output type — REST interface, error handling (§7), security considerations (§8)
• Formal notation used: TLA+ / Z3-style guard conjunction

Formal Model

Predicates and invariants (illustrative notation)

P1  SanitizedLabelValue
    ∀ label ∈ Message. sanitize(label) = trim(strip_control_chars(label))
    Source: RL-007 "the handler MUST sanitize the string values of label_to_remove
    and label_to_add against the standard gh-aw safe-output string sanitization rules"

P2  RateLimitRetryEligible
    RetryEligible(status, hasRetryAfter) ≡
        status = 429 ∨ (status = 403 ∧ hasRetryAfter)
    Source: RL-037/RL-048 "MUST apply the RATE_LIMIT_RETRY_CONFIG retry policy ...
    covers secondary rate-limit responses (HTTP 403 with Retry-After header) and
    primary rate-limit responses (HTTP 429)"

P3  RateLimitRetryBoundedRetries
    □ (attempts ≤ maxAttempts) ∧
      (◇ success ∨ (attempts = maxAttempts ∧ ¬success ⇒ HardError))
    Source: RL-037 combined with RL-045 "MUST surface hard errors (REST call
    failure, rate-limit exhaustion) as core.error() entries"

P4  NewLabelSetContainsAddExactlyOnce
    count(NewLabelSet, label_to_add) = 1 ∧ label_to_remove ∉ NewLabelSet
    where NewLabelSet = dedup((CurrentLabels ∖ {label_to_remove}) ∪ {label_to_add})
    Source: RL-041/RL-042 "label_to_add MUST always appear exactly once in the
    labels array (after deduplication)"

P5  RESTFailureIsHardError
    HTTPStatus ∉ [200,300) ⇒ HandlerResult = {success: false, error: msg}
    Source: RL-046 "When the setLabels REST call fails ... MUST log a core.error()
    entry and MUST return { success: false, error: <message> }"

P6  LabelMustPreExist
    label_to_add ∉ RepoLabels ⇒ Operation = HardError ∧ ¬Created(label_to_add)
    Source: RL-052 "MUST NOT create new labels on behalf of an AI agent ... the
    operation MUST fail with a hard error"

P7  ServerSideEnforcementOnly
    ∀ msg. Decision(label, allowed, blocked) is independent of msg.bypassFlag
    Source: RL-049 "Allowlist and blocklist evaluation MUST be performed
    server-side ... Agents MUST NOT be trusted to self-enforce label restrictions"

P8  TokenScopeMinimum
    ValidToken(scopes) ≡ "issues:write" ∈ scopes
    Source: RL-054/RL-051 "The GitHub token used by replace-label MUST have the
    issues: write permission ... minimum required scope"

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
SanitizedLabelValue (RL-007)	TestFormalSec_P1_SanitizedLabelValue	Verifies trimming and control-character stripping of label values before use
RateLimitRetryEligible (RL-037/RL-048)	TestFormalSec_P2_RateLimitRetryEligible	Verifies 429 always retries, 403 only retries with Retry-After header, 422/500 never retry
RateLimitRetryBoundedRetries (RL-037)	TestFormalSec_P3_RateLimitRetryBoundedRetries	Verifies eventual success within budget, hard-fail on exhaustion, short-circuit on non-retryable errors
NewLabelSetContainsAddExactlyOnce (RL-041/RL-042)	TestFormalSec_P4_NewLabelSetContainsAddExactlyOnce	Verifies label_to_add appears exactly once, label_to_remove excluded, dedup handles add==remove edge case
RESTFailureIsHardError (RL-046)	TestFormalSec_P5_RESTFailureIsHardError	Verifies non-2xx setLabels responses yield success:false with non-empty error
LabelMustPreExist (RL-052)	TestFormalSec_P6_LabelMustPreExist	Verifies hard failure (no label creation) when label_to_add is absent from the repo
ServerSideEnforcementOnly (RL-049)	TestFormalSec_P7_ServerSideEnforcementOnly	Verifies an agent-claimed bypass flag has zero effect on allow/blocklist outcome
TokenScopeMinimum (RL-054/RL-051)	TestFormalSec_P8_TokenScopeMinimum	Verifies token scope check requires issues:write, rejects tokens lacking it

Generated Test Suite

📄 pkg/workflow/replace_label_security_formal_test.go

(go/redacted):build !integration

// Package workflow_test — formal test suite for specs/replace-label-spec.md
//
// This file encodes a subset of the replace-label specification NOT already
// covered by replace_label_formal_test.go / replace_label_transitions_formal_test.go:
// input sanitization (RL-007), rate-limit retry semantics (RL-037/RL-048),
// label-array correctness for the setLabels REST payload (RL-041/RL-042),
// hard-error handling for REST/label-existence failures (RL-046, RL-052),
// server-side (not agent-side) enforcement of allow/blocklists (RL-049),
// and minimum token scope / cross-repo token requirements (RL-050/RL-051/RL-054/RL-055).
//
// Formal predicates encoded (illustrative TLA+ / Z3-style notation):
//
//	P1 SanitizedLabelValue        — sanitize(label) removes control chars / trims; matches RL-007
//	P2 RateLimitRetryEligible     — HTTP 403 w/ Retry-After OR HTTP 429 ⇒ retry eligible (RL-037/RL-048)
//	P3 RateLimitRetryBoundedRetries — retry count bounded by max attempts, then hard failure
//	P4 NewLabelSetContainsAddExactlyOnce — label_to_add ∈ labels, count == 1 (RL-041/RL-042)
//	P5 RESTFailureIsHardError     — setLabels HTTP failure ⇒ {success:false, error} + core.error() (RL-046)
//	P6 LabelMustPreExist          — label_to_add not in repo ⇒ hard error, no label creation (RL-052)
//	P7 ServerSideEnforcementOnly  — allow/blocklist evaluated in handler, agent-supplied bypass flag ignored (RL-049)
//	P8 TokenScopeMinimum          — token permission set must include "issues:write" (RL-054/RL-051)
package workflow_test

import (
	"strings"
	"testing"

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

// --- stub — replace with real implementation -------------------------------
// These helpers mirror the intended behavior of the JS handler described in
// specs/replace-label-spec.md §5 and §7. They are minimal Go re-implementations
// used only to make the formal predicates independently testable in Go.

// formalSecSanitizeLabel mirrors RL-007: trims whitespace and strips ASCII
// control characters (0x00-0x1F, 0x7F) from a label value prior to use.
func formalSecSanitizeLabel(raw string) string {
	var b strings.Builder
	for _, r := range raw {
		if r == 0x7F || (r < 0x20 && r != '\t') {
			continue
		}
		b.WriteRune(r)
	}
	return strings.TrimSpace(b.String())
}

// formalSecRetryEligible mirrors RL-037/RL-048: rate-limit retry policy.
func formalSecRetryEligible(statusCode int, hasRetryAfterHeader bool) bool {
	if statusCode == 429 {
		return true
	}
	if statusCode == 403 && hasRetryAfterHeader {
		return true
	}
	return false
}

// formalSecRetryWithBackoff simulates bounded retries: attempts up to maxAttempts
// while the failure is retry-eligible; returns final success flag and attempt count.
func formalSecRetryWithBackoff(maxAttempts int, outcomes []int, retryAfter []bool) (bool, int) {
	attempts := 0
	for i, code := range outcomes {
		attempts++
		if code == 200 {
			return true, attempts
		}
		eligible := formalSecRetryEligible(code, retryAfter[i])
		if !eligible {
			return false, attempts
		}
		if attempts >= maxAttempts {
			return false, attempts
		}
	}
	return false, attempts
}

// formalSecNewLabelSet mirrors RL-041/RL-042: current − remove + add, deduplicated,
// with label_to_add guaranteed to appear exactly once.
func formalSecNewLabelSet(current []string, labelToRemove, labelToAdd string) []string {
	seen := map[string]struct{}{}
	result := make([]string, 0, len(current)+1)
	for _, l := range current {
		if l == labelToRemove {
			continue
		}
		if _, ok := seen[l]; ok {
			continue
		}
		seen[l] = struct{}{}
		result = append(result, l)
	}
	if _, ok := seen[labelToAdd]; !ok {
		result = append(result, labelToAdd)
	}
	return result
}

// formalSecCountOccurrences counts how many times target appears in list.
func formalSecCountOccurrences(list []string, target string) int {
	count := 0
	for _, v := range list {
		if v == target {
			count++
		}
	}
	return count
}

type formalSecHandlerResult struct {
	Success bool
	Error   string
}

// formalSecRESTCallResult mirrors RL-046: any non-2xx setLabels response is a
// hard error; the call is all-or-nothing.
func formalSecRESTCallResult(httpStatus int, errMsg string) formalSecHandlerResult {
	if httpStatus >= 200 && httpStatus < 300 {
		return formalSecHandlerResult{Success: true}
	}
	return formalSecHandlerResult{Success: false, Error: errMsg}
}

// formalSecLabelMustPreExist mirrors RL-052: label_to_add must already exist in
// the repository; the implementation MUST NOT create it. Simulated as a 422.
func formalSecLabelMustPreExist(repoLabels []string, labelToAdd string) formalSecHandlerResult {
	for _, l := range repoLabels {
		if l == labelToAdd {
			return formalSecRESTCallResult(200, "")
		}
	}
	return formalSecRESTCallResult(422, "replace_label: label '"+labelToAdd+"' does not exist in target repository")
}

// formalSecServerSideAllowlistCheck mirrors RL-049: allow/blocklist evaluation
// happens strictly server-side; any client/agent-supplied "bypassValidation"
// flag on the message MUST be ignored.
func formalSecServerSideAllowlistCheck(label string, allowed, blocked []string, agentClaimsBypass bool) bool {
	// agentClaimsBypass is intentionally never consulted below — this is the
	// point of the predicate: the flag must have zero effect on the outcome.
	_ = agentClaimsBypass
	for _, b := range blocked {
		if b == label {
			return false
		}
	}
	if len(allowed) == 0 {
		return true
	}
	for _, a := range allowed {
		if a == label {
			return true
		}
	}
	return false
}

// formalSecTokenHasMinimumScope mirrors RL-054/RL-051: the token used MUST
// include "issues:write" permission.
func formalSecTokenHasMinimumScope(scopes []string) bool {
	for _, s := range scopes {
		if s == "issues:write" {
			return true
		}
	}
	return false
}

// --- Tests -------------------------------------------------------------

func TestFormalSec_P1_SanitizedLabelValue(t *testing.T) {
	cases := []struct {
		name     string
		input    string
		expected string
	}{
		{"plain label unchanged", "bug", "bug"},
		{"leading/trailing whitespace trimmed", "  needs-triage  ", "needs-triage"},
		{"embedded control char stripped", "bug\x00report", "bugreport"},
		{"newline stripped", "bug\nreport", "bugreport"},
		{"del char stripped", "bug\x7freport", "bugreport"},
	}
	for _, c := range cases {
		t.Run(c.name, func(t *testing.T) {
			got := formalSecSanitizeLabel(c.input)
			assert.Equal(t, c.expected, got, "sanitized label must strip control chars and trim whitespace per RL-007: case %q", c.name)
		})
	}
}

func TestFormalSec_P2_RateLimitRetryEligible(t *testing.T) {
	assert.True(t, formalSecRetryEligible(429, false), "HTTP 429 must always be retry-eligible per RL-048")
	assert.True(t, formalSecRetryEligible(403, true), "HTTP 403 with Retry-After header must be retry-eligible per RL-048")
	assert.False(t, formalSecRetryEligible(403, false), "HTTP 403 without Retry-After header must NOT be treated as rate-limit retry-eligible")
	assert.False(t, formalSecRetryEligible(422, false), "HTTP 422 is not a rate-limit response and must NOT be retry-eligible")
	assert.False(t, formalSecRetryEligible(500, false), "generic HTTP 500 must NOT be retried under the rate-limit policy")
}

func TestFormalSec_P3_RateLimitRetryBoundedRetries(t *testing.T) {
	t.Run("succeeds after transient rate limit", func(t *testing.T) {
		ok, attempts := formalSecRetryWithBackoff(5, []int{429, 429, 200}, []bool{false, false, false})
		assert.True(t, ok, "operation must eventually succeed once rate limit clears")
		assert.Equal(t, 3, attempts, "must record exactly 3 attempts before success")
	})
	t.Run("exhausts retries and hard-fails", func(t *testing.T) {
		ok, attempts := formalSecRetryWithBackoff(3, []int{429, 429, 429, 429}, []bool{false, false, false, false})
		assert.False(t, ok, "operation must hard-fail once retry budget is exhausted per RL-037")
		assert.LessOrEqual(t, attempts, 3, "attempts must not exceed the configured maximum retry budget")
	})
	t.Run("non-retry-eligible error short-circuits immediately", func(t *testing.T) {
		ok, attempts := formalSecRetryWithBackoff(5, []int{422}, []bool{false})
		assert.False(t, ok, "a non-rate-limit error must not be retried")
		assert.Equal(t, 1, attempts, "must fail on first attempt without retrying a non-rate-limit error")
	})
}

func TestFormalSec_P4_NewLabelSetContainsAddExactlyOnce(t *testing.T) {
	t.Run("standard replace", func(t *testing.T) {
		result := formalSecNewLabelSet([]string{"pending", "triage"}, "pending", "in-review")
		require.Contains(t, result, "in-review", "label_to_add must be present in the computed label set per RL-041")
		assert.Equal(t, 1, formalSecCountOccurrences(result, "in-review"), "label_to_add must appear exactly once per RL-042")
		assert.NotContains(t, result, "pending", "label_to_remove must be excluded from the computed set")
	})
	t.Run("label_to_add already present is deduplicated", func(t *testing.T) {
		result := formalSecNewLabelSet([]string{"pending", "in-review"}, "pending", "in-review")
		assert.Equal(t, 1, formalSecCountOccurrences(result, "in-review"), "duplicate label_to_add must be deduplicated to exactly one occurrence per RL-042")
	})
	t.Run("identical add and remove labels", func(t *testing.T) {
		result := formalSecNewLabelSet([]string{"same"}, "same", "same")
		assert.Equal(t, 1, formalSecCountOccurrences(result, "same"), "when label_to_add equals label_to_remove, final set must still contain exactly one occurrence")
	})
}

func TestFormalSec_P5_RESTFailureIsHardError(t *testing.T) {
	ok := formalSecRESTCallResult(200, "")
	assert.True(t, ok.Success, "HTTP 200 response must yield success:true")

	fail := formalSecRESTCallResult(422, "Validation Failed")
	assert.False(t, fail.Success, "non-2xx setLabels response must yield success:false per RL-046")
	assert.NotEmpty(t, fail.Error, "hard error result must carry a non-empty error message per RL-046")
}

func TestFormalSec_P6_LabelMustPreExist(t *testing.T) {
	t.Run("label exists in repo", func(t *testing.T) {
		result := formalSecLabelMustPreExist([]string{"bug", "enhancement"}, "bug")
		assert.True(t, result.Success, "operation must succeed when label_to_add already exists in the repository")
	})
	t.Run("label does not exist in repo", func(t *testing.T) {
		result := formalSecLabelMustPreExist([]string{"bug", "enhancement"}, "nonexistent-label")
		assert.False(t, result.Success, "operation must hard-fail when label_to_add does not pre-exist per RL-052 (no label creation on agent's behalf)")
		assert.Contains(t, result.Error, "does not exist", "error message must explain the missing-label reason")
	})
}

func TestFormalSec_P7_ServerSideEnforcementOnly(t *testing.T) {
	blocked := []string{"do-not-touch"}
	allowed := []string{"bug", "enhancement"}

	assert.False(t,
		formalSecServerSideAllowlistCheck("do-not-touch", allowed, blocked, true),
		"an agent-claimed bypass flag MUST NOT override server-side blocklist enforcement per RL-049")
	assert.False(t,
		formalSecServerSideAllowlistCheck("do-not-touch", allowed, blocked, false),
		"blocklist must reject regardless of bypass flag value")
	assert.True(t,
		formalSecServerSideAllowlistCheck("bug", allowed, blocked, false),
		"an allowed label not in blocklist must be permitted")
	assert.False(t,
		formalSecServerSideAllowlistCheck("unlisted", allowed, blocked, true),
		"a label absent from a non-empty allowlist must be rejected even when the agent claims a bypass")
}

func TestFormalSec_P8_TokenScopeMinimum(t *testing.T) {
	assert.True(t, formalSecTokenHasMinimumScope([]string{"issues:write", "contents:read"}),
		"token with issues:write scope must satisfy the minimum requirement per RL-054")
	assert.False(t, formalSecTokenHasMinimumScope([]string{"contents:read"}),
		"token lacking issues:write scope must NOT satisfy the minimum requirement for replace-label operations per RL-051/RL-054")
	assert.False(t, formalSecTokenHasMinimumScope([]string{}),
		"a token with no scopes must not satisfy the minimum requirement")
}

Usage

1. File already added at pkg/workflow/replace_label_security_formal_test.go in this repo.
2. Replace any // stub interfaces with real implementations calling into pkg/workflow/replace_label.go and the JS handler under actions/ where applicable.
3. Run: go test ./pkg/workflow/... -run TestFormalSec -v

Context

• Spec processed: specs/replace-label-spec.md
• Formal notation: TLA+ / Z3-style guard conjunction
• Run: https://github.com/github/gh-aw/actions/runs/31193680617

Notes

• Existing coverage: schema validation, count gate, target resolution, glob allow/blocklist matching, staged mode, label-set computation, gate checks (required-labels/title-prefix), cross-repo restriction, and label transitions are already tested in replace_label_formal_test.go and replace_label_transitions_formal_test.go — this run intentionally focused on the previously untested §7/§8 error-handling and security predicates to avoid duplicate coverage.
• Build verification note: this sandbox's Go toolchain (1.25.12) could not satisfy the repo's go 1.26.5 directive due to a blocked toolchain download, so the new test file was validated via gofmt (parses successfully, no formatting diffs) rather than go build/go test. Recommend running go test ./pkg/workflow/... -run TestFormalSec in CI to confirm.

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 · 82.5 AIC · ⊞ 10K · ◷

• expires on Aug 14, 2026, 7:48 AM UTC-08:00