[formal-spec] specs/intent-attribution-compliance/README.md — Formal model & test suite — 2026-07-25

### Summary

This issue formalizes the **Intent Attribution Compliance Fixture** specification (`specs/intent-attribution-compliance/README.md`), which defines the minimum conformance scenarios for the Intent Attribution & Agent Governance system. The spec mandates three deterministic behaviors: explicit intent metadata wins over any other source, multiple ambiguous closing issues must yield `status: "ambiguous"`, and unlinked pull requests must fail closed to the safest execution policy. The formal model captures these as invariants and preconditions over the `Resolver` and `PolicyCompiler` types already implemented in `pkg/intent/`, and translates them into a complete Go testify suite.

### Specification

- **File**: `specs/intent-attribution-compliance/README.md`
- **Focus area**: Intent attribution resolution order, ambiguous-root handling, and fail-closed governance policy
- **Formal notation used**: TLA+ (state-transition invariants) / F* (pre/post contracts)

### Formal Model

<details>
<summary><b>Predicates and invariants (illustrative notation)</b></summary>

**P1 — ExplicitIntentWins** *(TLA+, §Attribution-Resolution Order)*
```tla
INVARIANT ExplicitIntentWins ==
  ∀ pr ∈ PullRequests :
    pr.ExplicitIntent ≠ NULL
    ⟹ Resolve(pr).Source = "explicit_metadata"
```
Source: "An implementation MUST NOT skip earlier sources in favor of later sources unless the earlier source is unavailable or explicitly absent."

**P2 — SingleClosingIssueAttributed** *(TLA+)*
```tla
INVARIANT SingleClosingIssueAttributed ==
  ∀ pr ∈ PullRequests :
    pr.ExplicitIntent = NULL ∧ |pr.ClosingIssues| = 1
    ⟹ Resolve(pr).Source = "closing_issue"
       ∧ Resolve(pr).Status ∈ {"mapped", "unmapped"}
```
Source: "A single closing issue linked to the pull request."

**P3 — AmbiguousOnMultipleRoots** *(TLA+)*
```tla
INVARIANT AmbiguousOnMultipleRoots ==
  ∀ pr ∈ PullRequests :
    pr.ExplicitIntent = NULL ∧ |pr.ClosingIssues| ≥ 2
    ⟹ Resolve(pr).Status = "ambiguous"
       ∧ Resolve(pr).Source = "closing_issue"
```
Source: "An implementation MUST produce an ambiguous attribution when two or more distinct closing issues are linked."

**P4 — NoArbitraryAmbiguityResolution** *(F*)*
```fstar
val resolve_pr : pr:PullRequestData -> Tot IntentRecord
  (requires pr.ExplicitIntent = None /\ List.length pr.ClosingIssues >= 2)
  (ensures fun r -> r.Status = Ambiguous /\ not (r.Status = Mapped))
```
Source: "An implementation MUST NOT resolve ambiguity by arbitrary selection."

**P5 — LabelFallbackWhenNoClosingIssue** *(TLA+)*
```tla
INVARIANT LabelFallback ==
  ∀ pr ∈ PullRequests :
    pr.ExplicitIntent = NULL ∧ |pr.ClosingIssues| = 0 ∧ |pr.Labels| > 0
    ⟹ Resolve(pr).Source = "artifact_labels"
```
Source: "Pull request labels used as an artifact-label fallback when no closing issue is present."

**P6 — UnlinkedWhenNoSource** *(F*)*
```fstar
val resolve_pr : pr:PullRequestData -> Tot IntentRecord
  (requires pr.ExplicitIntent = None
            /\ List.length pr.ClosingIssues = 0
            /\ List.length pr.Labels = 0)
  (ensures fun r -> r.Status = Unlinked /\ r.Source = SourceNone)
```
Source: "An implementation MUST apply the safest available execution policy when the intent is unlinked."

**P7 — FailClosedForUnlinked** *(TLA+)*
```tla
INVARIANT FailClosedPolicy ==
  ∀ intent ∈ IntentRecords :
    intent.Status ∈ {"unlinked", "ambiguous"}
    ⟹ SafestPolicy.Autonomy = "propose_only"
       ∧ SafestPolicy.WriteScope = "none"
       ∧ SafestPolicy.HumanApprovalRequired = TRUE
       ∧ SafestPolicy.AutoMergeAllowed = FALSE
       ∧ SafestPolicy.MaxAttempts = 1
```
Source: "The safest available policy MUST be: autonomy propose_only, write scope none, human_approval_required: true, auto_merge_allowed: false, max_attempts: 1."

**P8 — PolicyDeterminism** *(TLA+)*
```tla
INVARIANT PolicyDeterminism ==
  ∀ i1, i2 ∈ IntentRecords :
    i1 = i2 ⟹ Compile(i1) = Compile(i2)
```
Source: "A policy decision MUST be deterministic: given identical attribution inputs, the same policy MUST always be produced."

**P9 — SuggestedNotOfficial** *(F*)*
```fstar
val attribute : pr:PullRequestData -> Tot IntentRecord
  (ensures fun r -> r.Status = Suggested ==> r.Source = SourceSuggestion
                    /\ not (official_metric r))
```
Source: "Suggested attribution does not contribute to official metrics or policy decisions."

**P10 — MixingSourcesForbidden** *(TLA+)*
```tla
INVARIANT SingleSource ==
  ∀ r ∈ IntentRecords :
    |{src : Source | r.Source = src}| = 1
```
Source: "Each record MUST be attributed to exactly one source."

</details>

### Behavioral Coverage Map

| Predicate / Invariant | Test Function | Description |
|---|---|---|
| `ExplicitIntentWins` (P1) | `TestFormal_ExplicitIntentWins` | Explicit metadata overrides all other sources |
| `SingleClosingIssueAttributed` (P2) | `TestFormal_SingleClosingIssue` | One closing issue → source is closing_issue |
| `AmbiguousOnMultipleRoots` (P3) | `TestFormal_MultipleClosingIssuesAmbiguous` | Two+ closing issues → status ambiguous |
| `NoArbitraryAmbiguityResolution` (P4) | `TestFormal_AmbiguousNeverMapped` | Ambiguous records never become mapped |
| `LabelFallbackWhenNoClosingIssue` (P5) | `TestFormal_LabelFallback` | Labels used as fallback when no closing issue |
| `UnlinkedWhenNoSource` (P6) | `TestFormal_UnlinkedWhenNoSource` | No source → status unlinked |
| `FailClosedForUnlinked` (P7) | `TestFormal_SafestPolicyFields` | Safest policy has required field values |
| `PolicyDeterminism` (P8) | `TestFormal_PolicyDeterminism` | Same input always yields same policy |
| `SuggestedNotOfficial` (P9) | `TestFormal_ExplicitOverridesSuggested` | Explicit wins; suggested status is never returned |
| `MixingSourcesForbidden` (P10) | `TestFormal_SingleSourcePerRecord` | Each record has exactly one attribution source |

### Generated Test Suite

<details>
<summary><b>📄 <code>pkg/intent/intent_formal_test.go</code></b></summary>

```go
// Package intent_test encodes the formal compliance predicates derived from
// specs/intent-attribution-compliance/README.md and the parent specification
// specs/intent-attribution-agent-governance.md.
//
// Formal predicates encoded:
//   P1  ExplicitIntentWins            — explicit metadata always wins
//   P2  SingleClosingIssueAttributed  — single closing issue → source=closing_issue
//   P3  AmbiguousOnMultipleRoots      — 2+ closing issues → status=ambiguous
//   P4  NoArbitraryAmbiguityResolution — ambiguous never resolves to mapped
//   P5  LabelFallbackWhenNoClosingIssue — PR labels used when no closing issue
//   P6  UnlinkedWhenNoSource          — no labels, no issues → unlinked
//   P7  FailClosedForUnlinked         — safest policy has required fields
//   P8  PolicyDeterminism             — same input → same policy output
//   P9  SuggestedNotOfficial          — suggested status is not returned by explicit path
//   P10 MixingSourcesForbidden        — each record has exactly one source
package intent_test

import (
	"testing"

	"github.com/github/gh-aw/pkg/intent"
	"github.com/stretchr/testify/assert"
	"github.com/stretchr/testify/require"
)

// safestPolicy returns an ExecutionPolicy populated with the values mandated by
// the Fail-Closed Behavior section of the spec.
func safestPolicy() intent.ExecutionPolicy {
	f := false
	return intent.ExecutionPolicy{
		Autonomy:              "propose_only",
		WriteScope:            "none",
		HumanApprovalRequired: true,
		AutoMergeAllowed:      &f,
		MaxAttempts:           1,
	}
}

// newResolver returns a Resolver that treats any label starting with 'p' as a
// configured intent label.
func newResolver() intent.Resolver {
	return intent.Resolver{
		ResolverVersion: "test-v1",
		MatchLabels: func(labels []string) []string {
			var matched []string
			for _, l := range labels {
				if len(l) > 0 && l[0] == 'p' {
					matched = append(matched, l)
				}
			}
			return matched
		},
	}
}

// TestFormal_ExplicitIntentWins — P1
func TestFormal_ExplicitIntentWins(t *testing.T) {
	r := newResolver()
	explicit := &intent.IntentRecord{
		Status: intent.AttributionMapped,
		Source: intent.SourceExplicitMetadata,
		Rule:   "explicit",
	}
	cases := []struct {
		name string
		pr   intent.PullRequestData
	}{
		{
			name: "explicit with no closing issues",
			pr:   intent.PullRequestData{NodeID: "PR_1", ExplicitIntent: explicit},
		},
		{
			name: "explicit with one closing issue",
			pr: intent.PullRequestData{
				NodeID:         "PR_2",
				ExplicitIntent: explicit,
				ClosingIssues:  []intent.RootReference{{NodeID: "I_1"}},
			},
		},
		{
			name: "explicit with multiple closing issues",
			pr: intent.PullRequestData{
				NodeID:         "PR_3",
				ExplicitIntent: explicit,
				ClosingIssues:  []intent.RootReference{{NodeID: "I_1"}, {NodeID: "I_2"}},
			},
		},
	}
	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			got := r.ResolvePullRequest(tc.pr)
			assert.Equal(t, intent.SourceExplicitMetadata, got.Source,
				"P1: explicit metadata must be the attribution source")
			assert.Equal(t, intent.AttributionMapped, got.Status,
				"P1: explicit metadata must preserve the supplied status")
		})
	}
}

// TestFormal_SingleClosingIssue — P2
func TestFormal_SingleClosingIssue(t *testing.T) {
	r := newResolver()
	pr := intent.PullRequestData{
		NodeID: "PR_10",
		ClosingIssues: []intent.RootReference{
			{NodeID: "I_10", Type: "issue", URL: "https://github.com/org/repo/issues/10", Labels: []string{"p1"}},
		},
	}
	got := r.ResolvePullRequest(pr)
	assert.Equal(t, intent.SourceClosingIssue, got.Source,
		"P2: single closing issue must be the attribution source")
	assert.NotEqual(t, intent.AttributionAmbiguous, got.Status,
		"P2: single closing issue must not produce ambiguous status")
	assert.NotEqual(t, intent.AttributionUnlinked, got.Status,
		"P2: single closing issue must not produce unlinked status")
	assert.Equal(t, "I_10", got.RootNodeID,
		"P2: root node ID must reference the closing issue")
}

// TestFormal_MultipleClosingIssuesAmbiguous — P3
func TestFormal_MultipleClosingIssuesAmbiguous(t *testing.T) {
	r := newResolver()
	cases := []struct {
		name   string
		issues []intent.RootReference
	}{
		{
			name:   "two closing issues",
			issues: []intent.RootReference{{NodeID: "I_A", Labels: []string{"p0"}}, {NodeID: "I_B", Labels: []string{"p1"}}},
		},
		{
			name:   "three closing issues",
			issues: []intent.RootReference{{NodeID: "I_A"}, {NodeID: "I_B"}, {NodeID: "I_C"}},
		},
	}
	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			pr := intent.PullRequestData{NodeID: "PR_20", ClosingIssues: tc.issues}
			got := r.ResolvePullRequest(pr)
			assert.Equal(t, intent.AttributionAmbiguous, got.Status,
				"P3: multiple closing issues must produce status=ambiguous")
			assert.Equal(t, intent.SourceClosingIssue, got.Source,
				"P3: ambiguous record source must be closing_issue")
			assert.NotEqual(t, intent.AttributionMapped, got.Status,
				"P4: ambiguous attribution must never resolve to mapped")
			assert.Empty(t, got.RootNodeID,
				"P4: ambiguous attribution must not arbitrarily select a root node")
		})
	}
}

// TestFormal_AmbiguousNeverMapped — P4
func TestFormal_AmbiguousNeverMapped(t *testing.T) {
	r := newResolver()
	pr := intent.PullRequestData{
		NodeID:        "PR_21",
		ClosingIssues: []intent.RootReference{{NodeID: "I_X", Labels: []string{"p0"}}, {NodeID: "I_Y", Labels: []string{"p0"}}},
	}
	got := r.ResolvePullRequest(pr)
	require.Equal(t, intent.AttributionAmbiguous, got.Status,
		"P4 precondition: resolver must produce ambiguous status")
	assert.NotEqual(t, intent.AttributionMapped, got.Status,
		"P4: ambiguous must not equal mapped")
}

// TestFormal_LabelFallback — P5
func TestFormal_LabelFallback(t *testing.T) {
	r := newResolver()
	cases := []struct {
		name      string
		labels    []string
		wantSrc   intent.AttributionSource
		wantNotSt intent.AttributionStatus
	}{
		{"single configured label", []string{"p1"}, intent.SourceArtifactLabels, intent.AttributionUnlinked},
		{"unconfigured label", []string{"documentation"}, intent.SourceArtifactLabels, intent.AttributionUnlinked},
		{"multiple labels", []string{"p0", "security"}, intent.SourceArtifactLabels, intent.AttributionAmbiguous},
	}
	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			got := r.ResolvePullRequest(intent.PullRequestData{NodeID: "PR_30", Labels: tc.labels})
			assert.Equal(t, tc.wantSrc, got.Source,
				"P5: label fallback must use artifact_labels source")
			assert.NotEqual(t, tc.wantNotSt, got.Status,
				"P5: label fallback must not produce status=%v", tc.wantNotSt)
		})
	}
}

// TestFormal_UnlinkedWhenNoSource — P6
func TestFormal_UnlinkedWhenNoSource(t *testing.T) {
	r := newResolver()
	got := r.ResolvePullRequest(intent.PullRequestData{NodeID: "PR_40"})
	assert.Equal(t, intent.AttributionUnlinked, got.Status,
		"P6: PR with no source must have status=unlinked")
	assert.Equal(t, intent.SourceNone, got.Source,
		"P6: PR with no source must have source=none")
}

// TestFormal_SafestPolicyFields — P7
func TestFormal_SafestPolicyFields(t *testing.T) {
	p := safestPolicy()
	assert.Equal(t, "propose_only", p.Autonomy,
		"P7: safest policy autonomy must be propose_only")
	assert.Equal(t, "none", p.WriteScope,
		"P7: safest policy write_scope must be none")
	assert.True(t, p.HumanApprovalRequired,
		"P7: safest policy must require human approval")
	require.NotNil(t, p.AutoMergeAllowed,
		"P7: AutoMergeAllowed must be explicitly set (not nil)")
	assert.False(t, *p.AutoMergeAllowed,
		"P7: safest policy must not allow auto-merge")
	assert.Equal(t, 1, p.MaxAttempts,
		"P7: safest policy max_attempts must be 1")
}

// TestFormal_PolicyDeterminism — P8
func TestFormal_PolicyDeterminism(t *testing.T) {
	r := newResolver()
	pr := intent.PullRequestData{
		NodeID:        "PR_50",
		ClosingIssues: []intent.RootReference{{NodeID: "I_50", Labels: []string{"p1"}}},
	}
	const runs = 5
	results := make([]intent.IntentRecord, runs)
	for i := range results {
		results[i] = r.ResolvePullRequest(pr)
	}
	for i := 1; i < runs; i++ {
		assert.Equal(t, results[0].Status, results[i].Status,
			"P8: run %d status must equal run 0", i)
		assert.Equal(t, results[0].Source, results[i].Source,
			"P8: run %d source must equal run 0", i)
		assert.Equal(t, results[0].Rule, results[i].Rule,
			"P8: run %d rule must equal run 0", i)
	}
}

// TestFormal_ExplicitOverridesSuggested — P9
func TestFormal_ExplicitOverridesSuggested(t *testing.T) {
	r := newResolver()
	explicit := &intent.IntentRecord{
		Status: intent.AttributionMapped,
		Source: intent.SourceExplicitMetadata,
		Rule:   "explicit",
	}
	pr := intent.PullRequestData{
		NodeID:         "PR_60",
		ExplicitIntent: explicit,
		ClosingIssues:  []intent.RootReference{{NodeID: "I_60", Labels: []string{"p0"}}},
	}
	got := r.ResolvePullRequest(pr)
	assert.NotEqual(t, intent.AttributionSuggested, got.Status,
		"P9: explicit intent must not result in suggested status")
	assert.Equal(t, intent.SourceExplicitMetadata, got.Source,
		"P9: explicit intent must retain explicit_metadata as source")
}

// TestFormal_SingleSourcePerRecord — P10
func TestFormal_SingleSourcePerRecord(t *testing.T) {
	r := newResolver()
	explicit := &intent.IntentRecord{Status: intent.AttributionMapped, Source: intent.SourceExplicitMetadata}
	validSources := map[intent.AttributionSource]bool{
		intent.SourceExplicitMetadata: true, intent.SourceClosingIssue: true,
		intent.SourceParentIssue: true, intent.SourceReferencedIssue: true,
		intent.SourceProject: true, intent.SourceMilestone: true,
		intent.SourceIssueLabels: true, intent.SourceArtifactLabels: true,
		intent.SourceSuggestion: true, intent.SourceNone: true,
	}
	cases := []struct {
		name string
		pr   intent.PullRequestData
	}{
		{"explicit", intent.PullRequestData{NodeID: "PR_70", ExplicitIntent: explicit}},
		{"single closing issue", intent.PullRequestData{NodeID: "PR_71", ClosingIssues: []intent.RootReference{{NodeID: "I_71", Labels: []string{"p1"}}}}},
		{"label fallback", intent.PullRequestData{NodeID: "PR_72", Labels: []string{"p1"}}},
		{"unlinked", intent.PullRequestData{NodeID: "PR_73"}},
		{"ambiguous", intent.PullRequestData{NodeID: "PR_74", ClosingIssues: []intent.RootReference{{NodeID: "I_A"}, {NodeID: "I_B"}}}},
	}
	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			got := r.ResolvePullRequest(tc.pr)
			assert.True(t, validSources[got.Source],
				"P10: source %q must be a known single-source constant", got.Source)
		})
	}
}
```

</details>

### Usage

1. Copy the test file to `pkg/intent/intent_formal_test.go`.
2. All types are real implementations — no stubs required.
3. Run: `go test ./pkg/intent/... -run Formal`

### Context

- Spec processed: `specs/intent-attribution-compliance/README.md`
- Formal notation: TLA+, F*
- Run: https://github.com/github/gh-aw/actions/runs/30164230224







> Generated by [🔬 Daily Formal Spec Verifier](https://github.com/github/gh-aw/actions/runs/30164230224) · sonnet46 · 96.1 AIC · ⌖ 13.1 AIC · ⊞ 7.2K · [◷](https://github.com/search?q=repo%3Agithub%2Fgh-aw+is%3Aissue+%22gh-aw-workflow-call-id%3A+github%2Fgh-aw%2Fdaily-formal-spec-verifier%22&type=issues)
> - [x] expires  on Aug 1, 2026, 7:57 AM UTC-08:00

Predicate / Invariant	Test Function	Description
`ExplicitIntentWins` (P1)	`TestFormal_ExplicitIntentWins`	Explicit metadata overrides all other sources
`SingleClosingIssueAttributed` (P2)	`TestFormal_SingleClosingIssue`	One closing issue → source is closing_issue
`AmbiguousOnMultipleRoots` (P3)	`TestFormal_MultipleClosingIssuesAmbiguous`	Two+ closing issues → status ambiguous
`NoArbitraryAmbiguityResolution` (P4)	`TestFormal_AmbiguousNeverMapped`	Ambiguous records never become mapped
`LabelFallbackWhenNoClosingIssue` (P5)	`TestFormal_LabelFallback`	Labels used as fallback when no closing issue
`UnlinkedWhenNoSource` (P6)	`TestFormal_UnlinkedWhenNoSource`	No source → status unlinked
`FailClosedForUnlinked` (P7)	`TestFormal_SafestPolicyFields`	Safest policy has required field values
`PolicyDeterminism` (P8)	`TestFormal_PolicyDeterminism`	Same input always yields same policy
`SuggestedNotOfficial` (P9)	`TestFormal_ExplicitOverridesSuggested`	Explicit wins; suggested status is never returned
`MixingSourcesForbidden` (P10)	`TestFormal_SingleSourcePerRecord`	Each record has exactly one attribution source

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[formal-spec] specs/intent-attribution-compliance/README.md — Formal model & test suite — 2026-07-25 #48035

Summary

Specification

Formal Model

Behavioral Coverage Map

Generated Test Suite

Usage

Context

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Uh oh!

[formal-spec] specs/intent-attribution-compliance/README.md — Formal model & test suite — 2026-07-25 #48035

Description

Summary

Specification

Formal Model

Behavioral Coverage Map

Generated Test Suite

Usage

Context

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions