[formal-spec] intent-attribution-compliance/README.md — Formal model & test suite — 2026-08-22

[github-actions]

Summary

specs/intent-attribution-compliance/README.md defines the three normative compliance fixtures (explicit-intent-wins, ambiguous-root-closing-issues, unlinked-pr-fail-closed) for the Intent Attribution & Agent Governance spec, and formally specifies the guard-ordered Resolve(a) attribution function plus fail-closed policy compilation. An existing formal test suite (pkg/intent/compliance_fixtures_formal_test.go) already covers predicates F1–F7. This run extends the formalization with two additional predicates (F8, F9) that were implicit in the spec's prose but not previously encoded as standalone tests: fail-closed short-circuiting must ignore even a matching permissive rule, and explicit-intent precedence must hold even when competing label signals are independently resolvable.

Specification

• File: specs/intent-attribution-compliance/README.md
• Focus area: Intent attribution resolution order and fail-closed governance policy compilation (pkg/intent.Resolver, pkg/intent.PolicyCompiler)
• Formal notation used: TLA+ (guard-ordered Resolve function) / Z3-style guard conjunction (predicate implications)

Formal Model

Predicates and invariants (illustrative notation)

Let:
  a ∈ PullRequestArtifact
  Explicit(a)  — optional explicit intent metadata attached to a
  Closing(a)   — ordered list of linked closing issues for a
  Labels(a)    — pull-request labels on a
  Resolve(a)   — attribution result (status, source, intent_key?)
  Compile(Resolve(a), R) — execution policy produced by PolicyCompiler given rule set R

Resolve(a) ≜
  IF Explicit(a) ≠ null THEN (mapped, explicit_metadata, Explicit(a).key)
  ELSE IF |Closing(a)| = 1 THEN FromClosingIssue(Closing(a)[0])
  ELSE IF |Closing(a)| > 1 THEN (ambiguous, closing_issue, null)
  ELSE IF |Labels(a)| > 0 THEN FromArtifactLabels(Labels(a))
  ELSE (unlinked, none, null)

F1_ExplicitIntentWins(a) ≜
  Explicit(a) ≠ null ⇒ Resolve(a).source = explicit_metadata
  [source: "Attribution uses explicit metadata as the sole source"]

F2_AmbiguousRootStatus(a) ≜
  Explicit(a) = null ∧ |Closing(a)| > 1 ⇒
    Resolve(a).status = ambiguous ∧ Resolve(a).source = closing_issue
  [source: "Ambiguous root issue set → status: ambiguous, source: closing_issue"]

F3_UnlinkedFailsClosed(a) ≜
  Explicit(a) = null ∧ |Closing(a)| = 0 ∧ |Labels(a)| = 0 ⇒
    Resolve(a).status = unlinked ∧ Resolve(a).source = none
  [source: "Unlinked pull request fails closed"]

F4_SafestPolicyOnIndeterminate(a) ≜
  Resolve(a).status ∈ {ambiguous, unlinked} ⇒
    Compile(Resolve(a), ∅) =
      (propose_only, none, approval_required=true, auto_merge=false, max_attempts=1)
  [source: "Governance resolves to the safest policy"]

F5_MappedStatusPermitsRelaxedPolicy(a) ≜
  Resolve(a).status = mapped ⇒ ∃R. Compile(Resolve(a), R) ≠ safest_policy
  [source: converse of fail-closed; mapped status is not universally forced fail-closed]

F6_PolicyDeterminism(a) ≜
  Resolve(a) = Resolve(a) ∧ Compile(Resolve(a), R) = Compile(Resolve(a), R)
  [source: implicit determinism requirement of a pure resolution function]

F7_SingleSourcePerRecord(a) ≜
  Resolve(a).source ∈ {explicit_metadata, closing_issue, none, artifact_labels}
  ∧ Resolve(a) is attributed to exactly one source
  [source: "the fixture-level compliance README" — each fixture ⇒ single source]

F8_FailClosedIgnoresRuleConfig(a) ≜        [NEW — this run]
  Resolve(a).status ∈ {ambiguous, unlinked} ⇒
    ∀ rule sets R (including R containing a matching permissive/wildcard rule).
      Compile(Resolve(a), R) = safest_policy
  [source: PolicyCompiler.Compile doc: "Unlinked and ambiguous records always
   receive the safest policy regardless of configured rules (fail-closed)" —
   the short-circuit occurs BEFORE rule matching, so even a matching wildcard
   rule cannot leak a relaxed policy]

F9_ExplicitLabelsDoNotOverrideMappedSource(a) ≜   [NEW — this run]
  Explicit(a) ≠ null ⇒ Resolve(a).source = explicit_metadata
    even when |Labels(a)| > 0 and Labels(a) would independently satisfy
    FromArtifactLabels(Labels(a)) in isolation
  [source: guard-ordered Resolve function — Explicit(a) ≠ null is the FIRST
   guard and short-circuits all subsequent branches, so label-signal strength
   is irrelevant once explicit metadata is present]

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
F1_ExplicitIntentWins	TestFormalFixture_ExplicitIntentWinsOverLinkedIssues (existing)	Explicit intent metadata resolves as the sole attribution source
F2_AmbiguousRootStatus	TestFormalFixture_AmbiguousRootIssueSet (existing)	2+ closing issues, no explicit intent → ambiguous/closing_issue
F3_UnlinkedFailsClosed	TestFormalFixture_UnlinkedPullRequestFailsClosed (existing)	No signals at all → unlinked/none
F4_SafestPolicyOnIndeterminate	TestFormalFixture_AmbiguousResolvesToSafestPolicy / TestFormalFixture_UnlinkedResolvesToSafestPolicy (existing)	Indeterminate status compiles to the safest policy tuple
F8_FailClosedIgnoresRuleConfig (ambiguous)	TestFormalFixture_AmbiguousIgnoresPermissiveRuleConfig	Ambiguous status ignores a matching permissive wildcard rule that grants bounded autonomy, any_branch writes, and auto-merge
F8_FailClosedIgnoresRuleConfig (unlinked)	TestFormalFixture_UnlinkedIgnoresPermissiveRuleConfig	Unlinked status ignores the same permissive wildcard rule
F9_ExplicitLabelsDoNotOverrideMappedSource	TestFormalFixture_ExplicitIntentWinsEvenWithMatchingLabels	Explicit intent source and mapped status hold even when independently-resolvable labels (bug, priority-high) are attached
F5_MappedStatusPermitsRelaxedPolicy (converse, empty-rule edge)	TestFormalFixture_NoRulesMatchYieldsSafestPolicyForMappedStatus	Mapped status with zero matching rules still falls back to the safest default (no rule ⇒ no relaxation)

Generated Test Suite

📄 `pkg/intent/intent_compliance_extended_formal_test.go`

// Formal predicates encoded by this suite (see specs/intent-attribution-compliance/README.md):
//
//   F8_FailClosedIgnoresRuleConfig(a):
//     Resolve(a).status ∈ {ambiguous, unlinked} ⇒
//       ∀ rules R. Compile(Resolve(a), R) = safest_policy
//     (fail-closed short-circuits BEFORE any rule matching is attempted, even when a
//     permissive wildcard/no-condition rule is present that would otherwise match).
//
//   F9_ExplicitLabelsDoNotOverrideMappedSource(a):
//     Explicit(a) ≠ null ⇒ Resolve(a).source = explicit_metadata
//     even when |Labels(a)| > 0 and the labels would independently resolve via
//     FromArtifactLabels — explicit intent precedence is absolute, not merely
//     "first non-empty signal wins".
//
// These are additive to the existing pkg/intent/compliance_fixtures_formal_test.go
// suite; they exercise the fail-closed short-circuit against a permissive rule set
// (rather than an empty one) and confirm label-signal presence does not leak into
// mapped-status resolution.
package intent_test

import (
	"testing"

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

	"github.com/github/gh-aw/pkg/intent"
)

// permissiveWildcardRule matches every record unconditionally and grants the most
// relaxed policy in every ranked dimension. If fail-closed short-circuiting were
// broken, this rule would leak a relaxed policy into ambiguous/unlinked records.
func permissiveWildcardRule() intent.PolicyRule {
	autoMerge := true
	return intent.PolicyRule{
		ID: "permissive-wildcard",
		// Zero-value PolicyCondition matches everything (all fields empty).
		When: intent.PolicyCondition{},
		Set: intent.ExecutionPolicy{
			Autonomy:              "bounded",
			WriteScope:            "any_branch",
			HumanApprovalRequired: false,
			AutoMergeAllowed:      &autoMerge,
			MaxAttempts:           5,
		},
	}
}

func TestFormalFixture_AmbiguousIgnoresPermissiveRuleConfig(t *testing.T) {
	fixture := loadIntentComplianceFixture(t, "ambiguous-root-closing-issues.yaml")
	rec := matchingResolver().ResolvePullRequest(buildFixturePullRequest(fixture))

	compiler := intent.PolicyCompiler{Rules: []intent.PolicyRule{permissiveWildcardRule()}}
	policy := compiler.Compile(rec, intent.RepositoryContext{})

	assert.Equal(t, "propose_only", policy.Autonomy, "ambiguous status must fail closed even against a matching permissive rule")
	assert.Equal(t, "none", policy.WriteScope, "ambiguous status must fail closed on write scope even against a matching permissive rule")
	assert.True(t, policy.HumanApprovalRequired, "ambiguous status must require approval even against a matching permissive rule")
	require.NotNil(t, policy.AutoMergeAllowed)
	assert.False(t, *policy.AutoMergeAllowed, "ambiguous status must deny auto-merge even against a matching permissive rule")
	assert.Equal(t, 1, policy.MaxAttempts, "ambiguous status must cap attempts at 1 even against a matching permissive rule")
}

func TestFormalFixture_UnlinkedIgnoresPermissiveRuleConfig(t *testing.T) {
	fixture := loadIntentComplianceFixture(t, "unlinked-pr-fail-closed.yaml")
	rec := matchingResolver().ResolvePullRequest(buildFixturePullRequest(fixture))

	compiler := intent.PolicyCompiler{Rules: []intent.PolicyRule{permissiveWildcardRule()}}
	policy := compiler.Compile(rec, intent.RepositoryContext{})

	assert.Equal(t, "propose_only", policy.Autonomy, "unlinked status must fail closed even against a matching permissive rule")
	assert.Equal(t, "none", policy.WriteScope, "unlinked status must fail closed on write scope even against a matching permissive rule")
	assert.True(t, policy.HumanApprovalRequired, "unlinked status must require approval even against a matching permissive rule")
	require.NotNil(t, policy.AutoMergeAllowed)
	assert.False(t, *policy.AutoMergeAllowed, "unlinked status must deny auto-merge even against a matching permissive rule")
	assert.Equal(t, 1, policy.MaxAttempts, "unlinked status must cap attempts at 1 even against a matching permissive rule")
}

func TestFormalFixture_ExplicitIntentWinsEvenWithMatchingLabels(t *testing.T) {
	fixture := loadIntentComplianceFixture(t, "explicit-intent-wins.yaml")
	pr := buildFixturePullRequest(fixture)

	// Attach labels that, in isolation (no explicit intent, no closing issues),
	// would independently resolve via FromArtifactLabels. Explicit intent must
	// still win — precedence is absolute, not merely "labels are a weaker signal".
	pr.Labels = append(pr.Labels, "bug", "priority-high")

	rec := matchingResolver().ResolvePullRequest(pr)

	assert.Equal(t, string(intent.SourceExplicitMetadata), string(rec.Source), "explicit intent must remain the sole attribution source even when independently-resolvable labels are present")
	assert.Equal(t, string(intent.AttributionMapped), string(rec.Status), "status must remain mapped when explicit intent is present regardless of label signals")
}

func TestFormalFixture_NoRulesMatchYieldsSafestPolicyForMappedStatus(t *testing.T) {
	fixture := loadIntentComplianceFixture(t, "explicit-intent-wins.yaml")
	rec := matchingResolver().ResolvePullRequest(buildFixturePullRequest(fixture))

	// Empty rule set: even though status is mapped (not fail-closed by status),
	// the compiler's "no match" branch must still return the safest default,
	// since no rule granted a relaxed policy.
	compiler := intent.PolicyCompiler{}
	policy := compiler.Compile(rec, intent.RepositoryContext{})

	assert.Equal(t, "propose_only", policy.Autonomy, "mapped status with zero matching rules must fall back to safest default autonomy")
	assert.Equal(t, "none", policy.WriteScope, "mapped status with zero matching rules must fall back to safest default write scope")
	assert.True(t, policy.HumanApprovalRequired, "mapped status with zero matching rules must fall back to safest default approval requirement")
}

Usage

1. Copy the test file to pkg/intent/intent_compliance_extended_formal_test.go.
2. No stubs are required; the suite reuses the real pkg/intent.Resolver and pkg/intent.PolicyCompiler, plus fixture helpers already defined in pkg/intent/compliance_fixtures_formal_test.go (matchingResolver, loadIntentComplianceFixture, buildFixturePullRequest).
3. Run: go test ./pkg/intent/... -run FormalFixture

Context

• Spec processed: specs/intent-attribution-compliance/README.md
• Formal notation: TLA+ / Z3-style guard conjunction
• Run: https://github.com/github/gh-aw/actions/runs/32581918601

Generated by 🔬 Daily Formal Spec Verifier · auto · 63.2 AIC · ⌖ 8.06 AIC · ⊞ 10.3K · ◷

• expires on Aug 29, 2026, 7:39 AM UTC-08:00