[formal-spec] awf-config-sources-compliance/README.md — Formal model & test suite — 2026-08-19

[github-actions]

Summary

specs/awf-config-sources-compliance/README.md defines the DriftRecord conformance fixture index (T-DR-001..010, T-DR-SAFE-001..004) for the AWF Config Canonical Sources Specification. This run formalizes the README's conformance-registry meta-process itself — the "Adding New Conformance Tests" / "Adding New Safeguard Conformance Tests" instructions — rather than re-deriving the already-covered DriftRecord schema predicates (P1–P10 covered by pkg/workflow/awf_config_drift_test.go and safeguard predicates covered by pkg/workflow/awf_config_safeguards_formal_test.go). This builds on prior formal notes from 2026-07-26 by extending the model with ID-registry invariants (monotonicity, uniqueness, format, disjoint series, routing rules).

Specification

• File: specs/awf-config-sources-compliance/README.md
• Focus area: T-DR-xxx / T-DR-SAFE-xxx conformance test ID registry and row-authoring process
• Formal notation used: TLA+ / Z3-style guard conjunction

Formal Model

Predicates and invariants (illustrative notation)

P1 TestIDMonotonicity(existing) ≜
 nextID(existing) > max({ n : "T-DR-" + n ∈ existing.ID })
 — source: "Assign a new T-DR-xxx identifier (increment from the last used ID)."

P2 TestIDNoDuplicates(rows) ≜
 ∀ r1, r2 ∈ rows : r1 ≠ r2 ⇒ r1.ID ≠ r2.ID
 — source: registry table implies unique keys per row.

P3 TestIDFormatWellFormed(id) ≜
 id ∈ L(T-DR-\d{3,}) ∨ id ∈ L(T-DR-SAFE-\d{3,})
 — source: observed ID shapes T-DR-001..010, T-DR-SAFE-001..004.

P4 PlaceholderIDRejectedAsFinal(id) ≜
 id = "T-DR-NNN" ⇒ ¬WellFormed(id)
 — source: "use a placeholder such as T-DR-NNN in drafts until the table
 above confirms the exact next ID."

P5 RowHasRequirementReference(row) ≜
 row.RequirementRef ≠ ∅ ∧ "§" ∈ row.RequirementRef
 — source: "Add a row ... with the test ID, requirement reference (§ number)."

P6 RowHasImplementationFile(row) ≜
 row.TestFile ≠ ∅ ∧ "pkg/workflow/" ∈ row.TestFile
 — source: "Implement the test in the conformance test file listed above."

P7 SafeguardRowRoutingDecision(row) ≜
 row.SpansSchemaAndDrift ⇒ row.TestFile = drift_test_file
 ∧ ¬row.SpansSchemaAndDrift ⇒ row.TestFile = safeguards_test_file
 — source: "Implement the test in pkg/workflow/awf_config_safeguards_formal_test.go
 when it exercises safeguard behavior, or in the closest AWF config drift
 test file when the safeguard spans drift output and schema validation."

P8 SpecCrossReferenceRequired(row) ≜
 row.Added ⇒ CrossReferencedFrom(row.ID, "specs/awf-config-sources-spec.md")
 — source: "Cross-reference the new test ID from the relevant subsection of
 specs/awf-config-sources-spec.md."

P9 DriftSeriesVsSafeguardSeriesDisjoint ≜
 { id : id ∈ DriftSeries } ∩ { id : id ∈ SafeguardSeries } = ∅
 — source: observed disjoint T-DR-xxx vs T-DR-SAFE-xxx numbering.

P10 EmptyRegistryNextIDIsFirst ≜
 existing = ∅ ⇒ nextID(existing) = "T-DR-001"
 — source: base case implied by the monotonic-increment rule.

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
P1_TestIDMonotonicity	TestFormalConformanceRegistry_P1_TestIDMonotonicity	Next assigned ID (T-DR-011) strictly exceeds the max of the existing 10-row registry
P10_EmptyRegistryNextIDIsFirst	TestFormalConformanceRegistry_P1_EmptyRegistryStartsAtOne	An empty registry's next-ID computation starts at T-DR-001
P2_TestIDNoDuplicates	TestFormalConformanceRegistry_P2_TestIDNoDuplicates	No two rows in the combined drift+safeguard registry share an ID
P3_TestIDFormatWellFormed	TestFormalConformanceRegistry_P3_TestIDFormatWellFormed	Table-driven check of valid/invalid ID shapes (case, digit count, prefix)
P4_PlaceholderIDRejectedAsFinal	TestFormalConformanceRegistry_P4_PlaceholderIDRejectedAsFinal	The documented T-DR-NNN draft placeholder is rejected as a well-formed final ID
P5_RowHasRequirementReference	TestFormalConformanceRegistry_P5_RowHasRequirementReference	Every row in both series cites a non-empty §-marked requirement reference
P6_RowHasImplementationFile	TestFormalConformanceRegistry_P6_RowHasImplementationFile	Every row maps to a concrete pkg/workflow/ test file path
P7_SafeguardRowRoutingDecision	TestFormalConformanceRegistry_P7_SafeguardRowRoutingDecision	Routing decision between the drift test file and safeguards test file based on schema-span flag
P8_SpecCrossReferenceRequired	TestFormalConformanceRegistry_P8_SpecCrossReferenceRequired	A row cross-referenced from the parent spec passes; one that is not, fails
P9_DriftSeriesVsSafeguardSeriesDisjoint	TestFormalConformanceRegistry_P9_DriftSeriesVsSafeguardSeriesDisjoint	The T-DR-xxx and T-DR-SAFE-xxx numbering series never collide
Edge case: four-digit ID rollover	TestFormalConformanceRegistry_EdgeCase_FourDigitRollover	ID formatting beyond 999 (T-DR-1000) remains well-formed, no truncation
Edge case: safeguard-only registry isolation	TestFormalConformanceRegistry_EdgeCase_SafeguardOnlyRegistryDoesNotAffectPlainSeries	Next-ID computation for the plain series ignores T-DR-SAFE-xxx entries entirely
Edge case: missing implementation file	TestFormalConformanceRegistry_EdgeCase_MissingImplementationFileIsInvalid	A row with an empty TestFile fails the pkg/workflow/ implementation requirement

Generated Test Suite

📄 `pkg/workflow/awf_config_conformance_registry_formal_test.go`

(go/redacted):build !integration

// Formal test suite generated from specs/awf-config-sources-compliance/README.md.
//
// This suite formalizes the *conformance-registry* meta-process described in the
// README's "Adding New Conformance Tests" and "Adding New Safeguard Conformance
// Tests" sections, as a complement to the DriftRecord-schema tests already in
// pkg/workflow/awf_config_drift_test.go and the safeguard tests already in
// pkg/workflow/awf_config_safeguards_formal_test.go.
//
// Formal predicates encoded (illustrative TLA+ / Z3-style guard-conjunction
// notation — see the issue body for the full formal model):
//
//	P1 TestIDMonotonicity — next T-DR-xxx ID strictly greater than max existing ID
//	P2 TestIDNoDuplicates — no two conformance rows share a T-DR-xxx ID
//	P3 TestIDFormatWellFormed — every assigned ID matches ^T-DR-\d{3}$ (or documented placeholder)
//	P4 PlaceholderIDRejectedAsFinal — "T-DR-NNN" (or any non-numeric placeholder) MUST NOT be
//	 treated as an assigned/final ID
//	P5 RowHasRequirementReference — every conformance row cites a "§" section reference
//	P6 RowHasImplementationFile — every conformance row maps to a concrete Go test file path
//	P7 SafeguardRowRoutingDecision — safeguard behavior spanning drift output AND schema
//	 validation routes to the drift test file; pure safeguard
//	 behavior routes to the safeguards test file
//	P8 SpecCrossReferenceRequired — a newly added row MUST be cross-referenced from the
//	 corresponding subsection of specs/awf-config-sources-spec.md
//	P9 DriftSeriesVsSafeguardSeriesDisjoint — T-DR-001..010 (DriftRecord) and T-DR-SAFE-001..004
//	 (safeguards) are disjoint numbering series and MUST NOT collide
//	P10 EmptyRegistryNextIDIsFirst — an empty registry's next-ID computation starts at T-DR-001
package workflow_test

import (
	"regexp"
	"testing"

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

// conformanceRow is a stub — replace with real implementation if/when the
// registry described in specs/awf-config-sources-compliance/README.md is
// materialized as structured data rather than a markdown table.
type conformanceRow struct {
	ID string // e.g. "T-DR-001" or "T-DR-SAFE-001"
	RequirementRef string // e.g. "§3.1"
	Description string
	TestFile string // e.g. "pkg/workflow/awf_config_drift_test.go"
	SpansSchemaAndDrift bool
}

var tdrIDPattern = regexp.MustCompile(`^T-DR-(SAFE-)?\d{3,}$`)

// nextConformanceID — stub — replace with real implementation. Mirrors the
// README's "increment from the last used ID" instruction (Adding New
// Conformance Tests, step 1) for the plain T-DR-xxx series only.
func nextConformanceID(existing []conformanceRow) string {
	maxNum := 0
	plain := regexp.MustCompile(`^T-DR-(\d{3,})$`)
	for _, r := range existing {
		if m := plain.FindStringSubmatch(r.ID); m != nil {
			n := 0
			for _, c := range m[1] {
				n = n*10 + int(c-'0')
			}
			if n > maxNum {
				maxNum = n
			}
		}
	}
	return formatTDR(maxNum + 1)
}

func formatTDR(n int) string {
	if n < 1000 {
		return "T-DR-0" + padTo2(n)
	}
	return "T-DR-" + itoa(n)
}

func padTo2(n int) string {
	s := itoa(n)
	for len(s) < 2 {
		s = "0" + s
	}
	return s
}

func itoa(n int) string {
	if n == 0 {
		return "0"
	}
	digits := ""
	for n > 0 {
		digits = string(rune('0'+n%10)) + digits
		n /= 10
	}
	return digits
}

// routeSafeguardRow — stub — replace with real implementation. Encodes the
// README's routing guidance: safeguard behavior spanning drift output AND
// schema validation goes to the drift test file; otherwise the safeguards file.
func routeSafeguardRow(spansSchemaAndDrift bool) string {
	if spansSchemaAndDrift {
		return "pkg/workflow/awf_config_drift_test.go"
	}
	return "pkg/workflow/awf_config_safeguards_formal_test.go"
}

// existingDriftRegistry models the T-DR-001..010 series from the README table.
func existingDriftRegistry() []conformanceRow {
	rows := []conformanceRow{}
	for i := 1; i <= 10; i++ {
		rows = append(rows, conformanceRow{
			ID: formatTDR(i),
			RequirementRef: "§3.1",
			Description: "DriftRecord conformance row",
			TestFile: "pkg/workflow/awf_config_drift_test.go",
		})
	}
	return rows
}

// existingSafeguardRegistry models the T-DR-SAFE-001..004 series.
func existingSafeguardRegistry() []conformanceRow {
	rows := []conformanceRow{}
	for i := 1; i <= 4; i++ {
		rows = append(rows, conformanceRow{
			ID: "T-DR-SAFE-00" + itoa(i),
			RequirementRef: "§8",
			Description: "Safeguard conformance row",
			TestFile: "pkg/workflow/awf_config_safeguards_formal_test.go",
		})
	}
	return rows
}

// P1: TestIDMonotonicity
func TestFormalConformanceRegistry_P1_TestIDMonotonicity(t *testing.T) {
	existing := existingDriftRegistry()
	next := nextConformanceID(existing)
	assert.Equal(t, "T-DR-011", next, "next assigned ID MUST strictly exceed the max existing T-DR-xxx ID (README: 'increment from the last used ID')")
}

func TestFormalConformanceRegistry_P1_EmptyRegistryStartsAtOne(t *testing.T) {
	// P10: EmptyRegistryNextIDIsFirst
	next := nextConformanceID([]conformanceRow{})
	assert.Equal(t, "T-DR-001", next, "an empty registry's next-ID computation MUST start at T-DR-001")
}

// P2: TestIDNoDuplicates
func TestFormalConformanceRegistry_P2_TestIDNoDuplicates(t *testing.T) {
	all := append(existingDriftRegistry(), existingSafeguardRegistry()...)
	seen := map[string]bool{}
	for _, row := range all {
		require.False(t, seen[row.ID], "duplicate conformance test ID detected: %s (no two rows may share an ID)", row.ID)
		seen[row.ID] = true
	}
	assert.Len(t, seen, len(all), "every row in the combined registry must contribute a unique ID")
}

// P3: TestIDFormatWellFormed
func TestFormalConformanceRegistry_P3_TestIDFormatWellFormed(t *testing.T) {
	tests := []struct {
		name string
		id string
		valid bool
	}{
		{"plain three digit", "T-DR-001", true},
		{"safe three digit", "T-DR-SAFE-004", true},
		{"four digit plain (still matches, overflow-safe)", "T-DR-1000", true},
		{"missing leading zero padding but numeric", "T-DR-11", false},
		{"lowercase prefix invalid", "t-dr-001", false},
		{"missing digits", "T-DR-", false},
	}
	for _, tc := range tests {
		t.Run(tc.name, func(t *testing.T) {
			got := tdrIDPattern.MatchString(tc.id)
			assert.Equal(t, tc.valid, got, "ID %q format validity mismatch (expected valid=%v)", tc.id, tc.valid)
		})
	}
}

// P4: PlaceholderIDRejectedAsFinal
func TestFormalConformanceRegistry_P4_PlaceholderIDRejectedAsFinal(t *testing.T) {
	// README explicitly instructs using "T-DR-NNN" as a placeholder in drafts
	// until the table confirms the exact next ID; NNN is non-numeric and MUST
	// never be treated as an assigned/final ID.
	placeholder := "T-DR-NNN"
	assert.False(t, tdrIDPattern.MatchString(placeholder), "placeholder ID %q MUST NOT be accepted as a well-formed, final conformance ID", placeholder)
}

// P5: RowHasRequirementReference
func TestFormalConformanceRegistry_P5_RowHasRequirementReference(t *testing.T) {
	all := append(existingDriftRegistry(), existingSafeguardRegistry()...)
	for _, row := range all {
		require.NotEmpty(t, row.RequirementRef, "row %s must cite a requirement reference", row.ID)
		assert.Contains(t, row.RequirementRef, "§", "row %s requirement reference must contain a section marker '§'", row.ID)
	}
}

// P6: RowHasImplementationFile
func TestFormalConformanceRegistry_P6_RowHasImplementationFile(t *testing.T) {
	all := append(existingDriftRegistry(), existingSafeguardRegistry()...)
	for _, row := range all {
		assert.NotEmpty(t, row.TestFile, "row %s must map to a concrete Go test file", row.ID)
		assert.Contains(t, row.TestFile, "pkg/workflow/", "row %s implementation file must live under pkg/workflow/", row.ID)
	}
}

// P7: SafeguardRowRoutingDecision
func TestFormalConformanceRegistry_P7_SafeguardRowRoutingDecision(t *testing.T) {
	cases := []struct {
		name string
		spansSchemaAndDrift bool
		wantFile string
	}{
		{"pure safeguard behavior", false, "pkg/workflow/awf_config_safeguards_formal_test.go"},
		{"spans drift output and schema validation", true, "pkg/workflow/awf_config_drift_test.go"},
	}
	for _, tc := range cases {
		t.Run(tc.name, func(t *testing.T) {
			got := routeSafeguardRow(tc.spansSchemaAndDrift)
			assert.Equal(t, tc.wantFile, got, "safeguard row routing decision mismatch for spansSchemaAndDrift=%v", tc.spansSchemaAndDrift)
		})
	}
}

// P8: SpecCrossReferenceRequired
func TestFormalConformanceRegistry_P8_SpecCrossReferenceRequired(t *testing.T) {
	// stub — replace with real implementation. Models the README requirement
	// (step 4 of both "Adding New..." sections) that a new row must be
	// cross-referenced from the parent spec file.
	crossReferenced := func(rowID string, specSubsections map[string]bool) bool {
		return specSubsections[rowID]
	}

	specSubsections := map[string]bool{
		"T-DR-011": true, // cross-referenced from specs/awf-config-sources-spec.md
		"T-DR-012": false, // NOT cross-referenced — must fail requirement
	}

	assert.True(t, crossReferenced("T-DR-011", specSubsections), "T-DR-011 must be cross-referenced from the parent spec")
	assert.False(t, crossReferenced("T-DR-012", specSubsections), "T-DR-012 lacking a spec cross-reference must be flagged as non-conformant")
}

// P9: DriftSeriesVsSafeguardSeriesDisjoint
func TestFormalConformanceRegistry_P9_DriftSeriesVsSafeguardSeriesDisjoint(t *testing.T) {
	driftIDs := map[string]bool{}
	for _, row := range existingDriftRegistry() {
		driftIDs[row.ID] = true
	}
	for _, row := range existingSafeguardRegistry() {
		require.False(t, driftIDs[row.ID], "safeguard ID %s must not collide with the DriftRecord series", row.ID)
	}
}

// Edge case 1: numbering rollover beyond 999 (four-digit ID) must still be well-formed.
func TestFormalConformanceRegistry_EdgeCase_FourDigitRollover(t *testing.T) {
	id := formatTDR(1000)
	assert.Equal(t, "T-DR-1000", id, "ID formatting at the 1000 boundary must not truncate or wrap")
	assert.True(t, tdrIDPattern.MatchString(id), "four-digit rollover ID must still satisfy the well-formed pattern")
}

// Edge case 2: a registry containing only safeguard IDs must not perturb the
// plain T-DR-xxx next-ID computation (the two series are independent).
func TestFormalConformanceRegistry_EdgeCase_SafeguardOnlyRegistryDoesNotAffectPlainSeries(t *testing.T) {
	next := nextConformanceID(existingSafeguardRegistry())
	assert.Equal(t, "T-DR-001", next, "plain T-DR-xxx next-ID computation must ignore T-DR-SAFE-xxx entries entirely")
}

// Edge case 3: a row description without an implementation file reference is
// invalid per the "Adding New Conformance Tests" checklist (steps 3-4).
func TestFormalConformanceRegistry_EdgeCase_MissingImplementationFileIsInvalid(t *testing.T) {
	row := conformanceRow{
		ID: "T-DR-011",
		RequirementRef: "§7.4.1",
		Description: "New SLA tracking row without an implementation yet",
		TestFile: "",
	}
	assert.Empty(t, row.TestFile, "sanity: this fixture intentionally omits an implementation file")
	// The conformance checklist requires step 3 (implement the test) before
	// the row can be considered complete; an empty TestFile signals an
	// incomplete/invalid registry entry.
	assert.NotContains(t, row.TestFile, "pkg/workflow/", "a row with no implementation file must not be treated as satisfying the pkg/workflow/ implementation requirement")
}

Usage

1. Copy the test file to pkg/workflow/awf_config_conformance_registry_formal_test.go.
2. Replace any // stub interfaces with real implementations if the conformance registry is materialized as structured data.
3. Run: go test ./pkg/workflow/... -run FormalConformanceRegistry

Context

• Spec processed: specs/awf-config-sources-compliance/README.md
• Formal notation: TLA+ / Z3-style guard conjunction
• Run: https://github.com/github/gh-aw/actions/runs/32270819989

Generated by 🔬 Daily Formal Spec Verifier · auto · 64.4 AIC · ⌖ 5.76 AIC · ⊞ 10.3K · ◷

• expires on Aug 26, 2026, 7:47 AM UTC-08:00