[formal-spec] Add replace-label formal model test suite (P1–P15 + edge cases) by Copilot · Pull Request #42527 · github/gh-aw

Copilot · 2026-06-30T16:30:18Z

This PR adds a formal-spec-aligned Go test suite for replace_label, mapping the extracted predicate set to concrete unit tests in pkg/workflow. It codifies the spec’s behavioral invariants around validation, gating, transition semantics, and cross-repo/target constraints.

Formal predicate coverage
- Added pkg/workflow/replace_label_formal_test.go with 21 tests covering P1..P15 plus edge cases from the formal-spec issue.
- Encodes requirements for required fields, max-length constraints, default max behavior, and validation-schema invariants.
Policy and gating semantics
- Added explicit tests for allowlist/blocklist ordering and enforcement (allowed-add, allowed-remove, blocked).
- Added tests for soft-skip gate behavior (required-labels, required-title-prefix) vs hard-error outcomes.
Execution semantics invariants
- Added tests for staged-mode representation and staged-result semantics.
- Added deterministic label-set computation checks: (current - remove) ∪ {add}, deduplication, idempotent remove-missing behavior, and single-occurrence guarantee for label_to_add.
Targeting and repo constraints
- Added formal tests for cross-repo restriction behavior (target-repo / allowed-repos) and target mode resolution (triggering vs *).
Spec/shape conformance checks
- Added edge tests for alias-field typing (item_number as IssueNumberOrTemporaryID) and ReplaceLabelConfig field presence expected by the spec.

func TestFormalReplaceLabelP10_LabelSetComputation(t *testing.T) {
	labels := formalComputeNewLabelSet(
		[]string{"in-progress", "bug", "bug"},
		"in-progress",
		"done",
	)
	assert.Equal(t, []string{"bug", "done"}, labels)
}

Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>

Copilot

Pull request overview

This PR introduces a new Go test file intended to codify formal-spec predicates for the replace_label safe-output type, including validation config assertions and a set of modeled behavioral invariants.

Changes:

Adds pkg/workflow/replace_label_formal_test.go with tests covering replace_label validation config (ValidationConfig) and compiler parsing for staged mode.
Adds a set of “formal” helper functions used to model allow/blocklist matching, gating checks, label-set computation, and targeting logic.

Show a summary per file

File	Description
pkg/workflow/replace_label_formal_test.go	Adds a formal-spec-oriented test suite for `replace_label`, including validation config checks and modeled predicate-based tests

Review details

Tip

Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Files reviewed: 1/1 changed files
Comments generated: 3
Review effort level: Low

+func formalRequiredNonEmptyLabel(s string) bool {
+	return strings.TrimSpace(s) != ""
+}
+
+func formalLabelAndRepoLengthsValid(labelToRemove, labelToAdd, repo string) bool {
+	return len(labelToRemove) <= 128 && len(labelToAdd) <= 128 && len(repo) <= 256
+}
+
+func formalMatchAnyPattern(value string, patterns []string) bool {
+	for _, p := range patterns {
+		matched, err := path.Match(p, value)
+		if err != nil {
+			continue
+		}
+		if matched {
+			return true
+		}
+	}
+	return false
+}
+
+func formalValidateSingleLabel(labelName string, allowedPatterns, blockedPatterns []string, fieldName string) error {
+	if formalMatchAnyPattern(labelName, blockedPatterns) {
+		return fmt.Errorf("%s %q matches a blocked pattern", fieldName, labelName)
+	}
+	if len(allowedPatterns) > 0 && !formalMatchAnyPattern(labelName, allowedPatterns) {
+		return fmt.Errorf("%s %q is not in the allowed list", fieldName, labelName)
+	}
+	return nil
+}


+func formalMatchAnyPattern(value string, patterns []string) bool {
+	for _, p := range patterns {
+		matched, err := path.Match(p, value)
+		if err != nil {
+			continue
+		}
+		if matched {
+			return true
+		}
+	}
+	return false
+}


+func TestFormalReplaceLabelEdge_NonExistentLabelHTTP422(t *testing.T) {
+	outcome := formalReplaceLabelOutcome{Success: false, Skipped: false}
+	assert.False(t, outcome.Success)
+	assert.False(t, outcome.Skipped)
+}


github-actions · 2026-06-30T17:37:59Z

Hey @app/copilot-swe-agent 👋 — great work on the formal-spec test suite for replace_label! The coverage here is thorough — mapping all 21 predicates (P1–P15 + edge cases) to concrete unit tests with crisp invariant names is exactly the kind of rigorous spec-codification this project benefits from.

This PR looks ready for review:

✅ Single focused file addition (replace_label_formal_test.go)
✅ Detailed description with predicate mapping, gating semantics, and execution invariants
✅ Pure test additions — no production code changes, no new dependencies
✅ 313 lines of well-structured Go tests covering validation, policy ordering, label-set computation, deduplication, and cross-repo constraints

Nothing stands out as needing changes — this is clean and well-scoped.

Generated by ✅ Contribution Check · 116.2 AIC · ⌖ 15.5 AIC · ⊞ 6.3K · ◷

pelikhan · 2026-06-30T18:30:47Z

@copilot run pr-finisher skill

Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>

… test, add scope doc comment Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>

Copilot · 2026-06-30T18:57:53Z

@copilot run pr-finisher skill

Done. Addressed all three in-scope review threads in commit dab38a9+:

Glob case-sensitivity – Fixed formalMatchAnyPattern to lowercase both value and pattern before calling path.Match, matching the production matchesSimpleGlob default (caseSensitive = false).
Misleading HTTP 422 test name – Renamed TestFormalReplaceLabelEdge_NonExistentLabelHTTP422 → TestFormalReplaceLabelEdge_HardErrorOutcome.
Helper scope clarity – Added a package-level doc comment explicitly stating that the formal helpers model the spec, not the production JS handler, and that JS regressions are caught by replace_label.test.cjs and integration tests.

Local validation (make fmt, make agent-report-progress, all 21 tests) passes. CI needs a human re-trigger to confirm.

github-actions · 2026-06-30T19:05:19Z

🤖 PR Triage

Field	Value
Category	`test`
Risk	🟢 Low
Score	44 / 100
Action	📦 `batch_review`
Batch	`review-ready` (with #42536, #42513)

Score breakdown: Impact 22/50 · Urgency 10/30 · Quality 12/20

Rationale: Adds 21 formal-spec-aligned tests for replace_label (P1–P15 + edge cases). Test-only change, low risk. No blocking reviews. Review together with review-ready batch.

Generated by 🔧 PR Triage Agent · 83.9 AIC · ⌖ 17.1 AIC · ⊞ 1.6K · ◷

github-actions · 2026-06-30T23:05:51Z

🎉 This pull request is included in a new release.

Release: v0.82.1

Initial plan

49d4ffc

Copilot AI assigned Copilot and pelikhan Jun 30, 2026

Copilot started work on behalf of pelikhan June 30, 2026 16:39 View session

Copilot AI linked an issue Jun 30, 2026 that may be closed by this pull request

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

Closed

Add formal replace-label model tests

dab38a9

Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>

Copilot AI changed the title ~~[WIP] Add formal verification model and unit-test suite for replace-label~~ [formal-spec] Add replace-label formal model test suite (P1–P15 + edge cases) Jun 30, 2026

Copilot AI requested a review from pelikhan June 30, 2026 16:55

Copilot finished work on behalf of pelikhan June 30, 2026 16:55

pelikhan marked this pull request as ready for review June 30, 2026 17:27

Copilot AI review requested due to automatic review settings June 30, 2026 17:27

Copilot started reviewing on behalf of pelikhan June 30, 2026 17:28 View session

Copilot AI reviewed Jun 30, 2026

View reviewed changes

github-actions Bot mentioned this pull request Jun 30, 2026

[Contribution Check Report] Contribution Check — 2026-06-30 #42399

Closed

Merge branch 'main' into copilot/formal-spec-replace-label

3f0a7d3

Copilot started work on behalf of pelikhan June 30, 2026 18:46 View session

Copilot AI and others added 2 commits June 30, 2026 18:54

Initial plan: address review feedback on replace_label_formal_test.go

112e1ea

Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>

Address review feedback: fix glob case-sensitivity, rename misleading…

becbc9b

… test, add scope doc comment Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>

Copilot finished work on behalf of pelikhan June 30, 2026 18:58

Merge branch 'main' into copilot/formal-spec-replace-label

149b3b5

pelikhan merged commit 7dcb370 into main Jun 30, 2026
19 checks passed

pelikhan deleted the copilot/formal-spec-replace-label branch June 30, 2026 18:58

github-actions Bot added pr-action:batch_review pr-agent:copilot-swe-agent pr-batch:review-ready pr-priority:medium pr-risk:low labels Jun 30, 2026

github-actions Bot added the pr-type:test label Jun 30, 2026

This was referenced Jun 30, 2026

httpnoctx: detect context-free NewRequest + Do paths #42536

Merged

fix: find access.log in sandbox/firewall/logs/squid-logs/ subdirectory #42513

Merged

github-actions Bot mentioned this pull request Jun 30, 2026

[PR Triage Report] 2026-06-30 18:51 UTC — 13 agent PRs (11 new, 2 carried over) #42545

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[formal-spec] Add replace-label formal model test suite (P1–P15 + edge cases) - #42527

[formal-spec] Add replace-label formal model test suite (P1–P15 + edge cases)#42527
pelikhan merged 6 commits into
mainfrom
copilot/formal-spec-replace-label

Copilot AI commented Jun 30, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

github-actions Bot commented Jun 30, 2026

Uh oh!

pelikhan commented Jun 30, 2026

Uh oh!

Copilot AI commented Jun 30, 2026

Uh oh!

Uh oh!

github-actions Bot commented Jun 30, 2026

Uh oh!

github-actions Bot commented Jun 30, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

Copilot AI commented Jun 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Review details

Uh oh!

github-actions Bot commented Jun 30, 2026

Uh oh!

pelikhan commented Jun 30, 2026

Uh oh!

Copilot AI commented Jun 30, 2026

Uh oh!

Uh oh!

github-actions Bot commented Jun 30, 2026

🤖 PR Triage

Uh oh!

github-actions Bot commented Jun 30, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Copilot AI commented Jun 30, 2026 •

edited

Loading