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

[github-actions]

Summary

Formal verification model and Go testify unit-test suite for specs/replace-label-spec.md — the W3C-style spec for the replace-label safe-output type. This spec defines atomic label transitions on GitHub issues/PRs via a single REST PUT /issues/{n}/labels call. Fifteen predicates were extracted from 56 normative requirements (RL-001..RL-056) and mapped to 21 Go test functions covering schema validation, allowlist/blocklist enforcement, gate checks, staged mode, label-set computation, idempotency, and cross-repo restrictions.

Specification

• File: specs/replace-label-spec.md
• Focus area: replace-label safe-output type — atomic label replacement via single REST call
• Formal notation used: TLA+ (state machines), Z3/SMT (constraint predicates), Lean 4 (type invariants)

Formal Model

Predicates and invariants (illustrative notation)

-- P1: FieldRequired (RL-004, RL-005)
PREDICATE FieldRequired(msg) := TRIM(msg.label_to_remove) ≠ "" ∧ TRIM(msg.label_to_add) ≠ ""

-- P2: FieldMaxLength (RL-004..RL-006)
PREDICATE FieldMaxLength(msg) := |msg.label_to_remove| ≤ 128 ∧ |msg.label_to_add| ≤ 128 ∧ |msg.repo| ≤ 256

-- P3: DefaultMaxFive (RL-012)
INVARIANT DefaultMaxFive := ValidationConfig["replace_label"].DefaultMax = 5

-- P4: AllowlistEnforcement (RL-021, RL-022)
PREDICATE AddAllowed(label, allowed) := allowed = ∅ ∨ ∃ p ∈ allowed. GlobMatch(p, label)

-- P5: BlocklistPriority (RL-003) — blocked overrides allowlist (security boundary)
INVARIANT BlocklistPriority := (∃ p ∈ blocked. GlobMatch(p, label)) → ¬AddAllowed(label, allowed)

-- P6: RemoveAllowlist (RL-021, RL-025)
PREDICATE RemoveAllowed(label, allowed) := allowed = ∅ ∨ ∃ p ∈ allowed. GlobMatch(p, label)

-- P7: RequiredLabelsGate (RL-024, RL-026) — failure → {success:false, skipped:true}
PREDICATE RequiredLabelsGate(current, required) := required ⊆ current

-- P8: TitlePrefixGate (RL-025, RL-026) — failure → {success:false, skipped:true}
PREDICATE TitlePrefixGate(title, prefix) := prefix = "" ∨ title.startsWith(prefix)

-- P9: StagedMode (RL-027, RL-028) — no writes; result {success:true, staged:true}
INVARIANT StagedNoWrites(staged, writes) := staged → writes = ∅

-- P10: LabelSetComputation (RL-029)
FUNCTION computeNewLabelSet(current, rm, add) := (current \ {rm}) ∪ {add}  -- deduplicated

-- P11: IdempotentMissingRemove (RL-034) — rm absent → add-only, success:true
INVARIANT IdempotentMissing(rm, current) := rm ∉ current → result = current ∪ {add}

-- P12: LabelToAddAlwaysPresent (RL-041, RL-042)
INVARIANT LabelToAddPresent(result, add) := COUNT(add, result) = 1

-- P13: HardVsSoftErrors (RL-044..RL-046)
-- Gate failure → {skipped:true}; REST failure → hard error {success:false, error:...}

-- P14: CrossRepoRestriction (RL-015, RL-050)
PREDICATE CrossRepoAllowed(repo, allowedRepos) := allowedRepos = ∅ ∨ repo ∈ allowedRepos

-- P15: TargetModeEnforcement (RL-018..RL-020)
PREDICATE TargetAllowed(mode, trig, resolved) :=
    CASE mode: "triggering" → resolved = trig | "*" → true | n:Int → resolved = n

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
P1-FieldRequired	TestFormalReplaceLabelP1_FieldRequired	label_to_remove/label_to_add required, non-empty (RL-004, RL-005)
P2-FieldMaxLength	TestFormalReplaceLabelP2_FieldMaxLength	128-char label limits, 256-char repo limit (RL-004..RL-006)
P3-DefaultMaxFive	TestFormalReplaceLabelP3_DefaultMaxFive	ValidationConfig DefaultMax = 5 (RL-012)
P3-ValidationConfig	TestFormalReplaceLabelP3_ValidationConfigFields	Field rules (Required, Type, MaxLength, Sanitize) match spec §4.2.1
P4-AllowlistEnforcement	TestFormalReplaceLabelP4_AllowlistEnforcement	label_to_add accepted/rejected by allowed-add globs (RL-020..RL-022)
P5-BlocklistPriority	TestFormalReplaceLabelP5_BlocklistPriority	blocked rejects label even when matching allowed-add (RL-003)
P6-RemoveAllowlist	TestFormalReplaceLabelP6_RemoveAllowlist	label_to_remove accepted/rejected by allowed-remove (RL-021, RL-025)
P7-RequiredLabelsGate	TestFormalReplaceLabelP7_RequiredLabelsGate	ALL required-labels present → proceed; missing → skipped:true (RL-024, RL-026)
P8-TitlePrefixGate	TestFormalReplaceLabelP8_TitlePrefixGate	Title must begin with prefix; else skipped:true (RL-025, RL-026)
P9-StagedFlag	TestFormalReplaceLabelP9_StagedFlagOnConfig	staged=true stored as TemplatableBool on config (RL-027)
P9-StagedResult	TestFormalReplaceLabelP9_StagedHandlerResult	Staged returns {success:true, staged:true} (RL-028)
P10-LabelSetComputation	TestFormalReplaceLabelP10_LabelSetComputation	new = (current − rm) ∪ {add}, deduplicated (RL-029)
P11-IdempotentMissingRemove	TestFormalReplaceLabelP11_IdempotentMissingRemove	rm absent → add-only, labelRemoved=null, success:true (RL-034, RL-039)
P12-LabelToAddAlwaysPresent	TestFormalReplaceLabelP12_LabelToAddAlwaysPresent	label_to_add exactly once in result (RL-041, RL-042)
P13-HardVsSoftErrors	TestFormalReplaceLabelP13_HardVsSoftErrors	Gate → skipped:true; REST failure → hard error (RL-026, RL-044, RL-046)
P14-CrossRepoRestriction	TestFormalReplaceLabelP14_CrossRepoRestriction	repo ∉ allowed-repos rejected (RL-015, RL-050)
P15-TargetModeEnforcement	TestFormalReplaceLabelP15_TargetModeEnforcement	"triggering" → triggering item only; "*" → any (RL-018, RL-020)
Edge-IdenticalLabels	TestFormalReplaceLabelEdge_BothLabelsIdentical	label_to_remove == label_to_add → deduplicated to one occurrence
Edge-HTTP422	TestFormalReplaceLabelEdge_NonExistentLabelHTTP422	Missing label_to_add → hard error, not soft skip (RL-052)
Edge-AliasFields	TestFormalReplaceLabelEdge_ItemNumberAliasFields	item_number typed IssueNumberOrTemporaryID for alias resolution (RL-016)
Edge-ConfigStruct	TestFormalReplaceLabelEdge_ReplaceLabelConfigStructFieldsPresent	All §4.1.1 config fields present on ReplaceLabelConfig

Generated Test Suite

📄 `pkg/workflow/replace_label_formal_test.go` (1,043 lines, committed to repo)

(go/redacted):build !integration
package workflow

// Stubs — replace with real implementations:
type replaceLabelMessage struct { LabelToRemove, LabelToAdd string; ItemNumber *int; Repo string }
func validateReplaceLabelMessage(m replaceLabelMessage) string { /* RL-004..RL-007 */ }
func matchesGlobList(label string, patterns []string) bool     { /* gobwas/glob semantics */ }
func computeNewLabelSet(current []string, rm, add string) []string { /* RL-029, RL-034 */ }
type replaceLabelHandlerResult struct { Success, Staged, Skipped bool; LabelRemoved, LabelAdded, ErrorMsg string }

// 21 Test* functions cover predicates P1-P15 and 3 edge cases.
// Run: go test ./pkg/workflow/... -run FormalReplaceLabel

Full file: pkg/workflow/replace_label_formal_test.go

Usage

1. Confirm pkg/workflow/replace_label_formal_test.go is present (committed this run).
2. Replace // stub helpers with real gobwas/glob and handler implementations.
3. Run: go test ./pkg/workflow/... -run FormalReplaceLabel

Context

• Spec processed: specs/replace-label-spec.md
• Formal notation: TLA+, Z3/SMT, Lean 4 (illustrative)
• Predicates formalized: 15 | Test functions: 21
• Requirements covered: RL-003..RL-007, RL-012, RL-015..RL-016, RL-018..RL-022, RL-024..RL-029, RL-034, RL-039, RL-041..RL-042, RL-044, RL-046, RL-050, RL-052
• Run: https://github.com/github/gh-aw/actions/runs/28458847505

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 · 165.1 AIC · ⌖ 21.7 AIC · ⊞ 1.8K · ◷

• expires on Jul 7, 2026, 8:30 AM UTC-08:00