[formal-spec] awf-config-sources-spec.md — Formal model & test suite — 2026-09-16

### Summary

`specs/awf-config-sources-spec.md` defines the canonical AWF (gh-aw-firewall) configuration sources that gh-aw agents and schema-reconciliation workflows MUST consult, the `DriftRecord` structured-output schema for detected configuration drift, the fetch-compare-report drift detection procedure (§7), CR-01–CR-06a conformance requirements (dual-source consultation, drift classification, SLA remediation windows, escalation ownership), and §8 safeguards for canonical-source unavailability (snapshot freshness, degraded mode). This run rotated the spec back to `awf-config-sources-spec.md` (prior notes already cover P1–P24) and extended the formal model with three new predicates — **P25–P27** — closing a gap where T-DR-005, T-DR-008, and T-DR-009 (DriftRecord schema strictness and corrective-PR payload completeness, §3.1.1/§7.5.1) were previously exercised only by the non-formal `awf_config_drift_test.go` suite, not by the dedicated formal predicate/test series.

### Specification

- **File**: `specs/awf-config-sources-spec.md`
- **Focus area**: DriftRecord schema strictness (`additionalProperties: false`) and corrective-PR payload completeness in the AWF config drift-detection procedure
- **Formal notation used**: TLA+-style predicate logic / Z3-style guard conjunction (consistent with prior runs on this spec)

### Formal Model

Predicates and invariants (illustrative notation)

```
// P25 — T-DR-005 (Section 3.1.1: "additionalProperties": false)
// Source: 'A `DriftRecord` represents a single detected configuration drift
// item ... "additionalProperties": false'
∀ json ∈ DriftRecordWireFormat.
StrictDecode(json) ≠ ⊥
⟺ fields(json) = {property_path, drift_category, suggested_action, detected_at}

formalDriftRecordNoAdditionalProperties(raw) :=
let dec := JSONDecoder(raw) with DisallowUnknownFields
in dec.Decode(FormalDriftRecordWire) succeeds
⟺ raw contains exactly the four required keys

// P26 — T-DR-008 (Section 7.5.1: "The corrective PR description MUST embed
// the full DriftRecord list as JSON")
// Source: '... the detecting automation MUST open a corrective PR (CR-05;
// T-DR-006) ... The corrective PR description MUST embed the full
// DriftRecord list as JSON (T-DR-008).'
∀ records : List[DriftRecord].
json.Unmarshal(CorrectivePRBody(records)) = records // exact round-trip
∧ CorrectivePRBody([]) = "[]" // empty ⇒ "[]", never null

// P27 — T-DR-009 (Section 7.5.1: an empty DriftRecord list is a valid Step-5
// output)
// Source: 'The drift detection procedure (Section 7.2, Step 5) MUST produce
// a list of zero or more DriftRecord objects (schema: Section 3.1; T-DR-009).'
∀ records : List[DriftRecord], slaExceeded : Bool.
records = [] ⟹ ¬RequiresCorrectivePR(records) ∧ ¬RequiresEscalation(records, slaExceeded)

RequiresCorrectivePR(records) := ∃ r ∈ records. r.drift_category ∈ {missing_in_ghaw, spec_mismatch}
RequiresEscalation(records, slaExceeded) := RequiresCorrectivePR(records) ∧ slaExceeded
```

**Prior predicates P1–P24 (already formalized in earlier runs, referenced for continuity, not re-emitted here):** `formalDualSourceConsulted` (CR-01), `formalNoUndocumentedFieldGeneration` (CR-03), `formalDriftRecordStructuralValidity` (§3.1), `formalDriftCategoryExhaustiveness`, `formalSchemaOnlyPropertyFlaggedAsDrift` (CR-02), `formalCorrectionPRForActionableDrift` (CR-05), `formalSLARemediationWindow` (CR-06), `formalEscalationIssueStructure` (CR-06), `formalSafeguardDegradedModeOnUnavailability` (§8), `formalDriftReportEmittedOnDetection` (§7.2 Step 5), `formalSnapshotExpiry`/`formalSnapshotStoragePath` (§8), `formalEscalationOwnerAssignment`/`formalEscalationOwnerNonEmpty`/`formalEscalationAcknowledgementWindow` (CR-06a), `formalCoverageVerificationEveryRun` (CR-04), `formalEscalationLabelPairComplete`/`formalEscalationTitlePrefix`/`formalEscalationTemplateFieldsComplete` (§7.4.1), `formalAutomationTriggerCondition` (§7.1), `formalScheduledRunFailsOnMissingInGhaw`/`formalPRSummaryCommentRequired`/`formalScheduledTrackingIssueOnDrift`/`formalAutomationExitCodeMonotone` (§7.4).

### Behavioral Coverage Map

| Predicate / Invariant | Test Function | Description |
|---|---|---|
| `formalDriftRecordNoAdditionalProperties` (P25 / T-DR-005) | `TestFormal_P25_DriftRecordNoAdditionalProperties` | Valid 4-field DriftRecord JSON decodes; a payload with one extra field is rejected |
| `formalDriftRecordNoAdditionalProperties` (P25 / T-DR-005) | `TestFormal_P25_DriftRecordNoAdditionalProperties_MultipleExtraFields` | Rejection holds even with multiple additional properties present simultaneously |
| `formalCorrectivePREmbedsFullDriftList` (P26 / T-DR-008) | `TestFormal_P26_CorrectivePREmbedsFullDriftList` | Corrective PR body round-trips a populated, multi-record DriftRecord list without truncation or re-ordering |
| `formalCorrectivePREmbedsFullDriftList` (P26 / T-DR-008 ∧ T-DR-009) | `TestFormal_P26_CorrectivePREmbedsFullDriftList_EmptyList` | Empty and nil DriftRecord slices both serialize to JSON `"[]"`, never `null` |
| `formalEmptyDriftListValidNoTrigger` (P27 / T-DR-009) | `TestFormal_P27_EmptyDriftListValidNoTrigger` | Nil and empty (non-nil) DriftRecord lists never require a corrective PR or SLA escalation, even past the SLA window |
| `formalEmptyDriftListValidNoTrigger` (P27 / T-DR-009, sanity) | `TestFormal_P27_EmptyDriftListValidNoTrigger_NonEmptyStillTriggers` | Sanity check: a non-empty actionable-category list still requires a corrective PR, and requires escalation only once the SLA window is exceeded |
| `formalDriftRecordStructuralValidity` (P3, cross-check) | asserted inside `TestFormal_P25_DriftRecordNoAdditionalProperties` | Strictly-decoded record also satisfies the pre-existing P3 structural-validity predicate |

### Generated Test Suite

📄 pkg/workflow/awf_config_drift_extended_formal_test.go

```go
(go/redacted):build !integration

// Formal model extension for specs/awf-config-sources-spec.md.
//
// This file extends the P1-P24 predicate series already present in
// awf_config_drift_formal_test.go, awf_config_safeguards_formal_test.go,
// awf_config_escalation_template_formal_test.go, and
// awf_config_automation_trigger_formal_test.go with three additional
// predicates covering DriftRecord schema strictness and corrective-PR
// payload obligations (Section 3.1.1, Section 7.5) that were previously
// exercised only by the non-formal awf_config_drift_test.go suite:
//
// - P25 formalDriftRecordNoAdditionalProperties — T-DR-005: DriftRecord
// JSON MUST NOT carry properties beyond the four required fields
// (Section 3.1.1 "additionalProperties": false).
// - P26 formalCorrectivePREmbedsFullDriftList — T-DR-008: a corrective PR
// description MUST embed the complete DriftRecord list as JSON,
// including empty and multi-record lists, without truncation or
// re-ordering (Section 7.5.1).
// - P27 formalEmptyDriftListValidNoTrigger — T-DR-009: an empty
// DriftRecord list is a valid Step-5 output and MUST NOT trigger a
// corrective PR or SLA escalation (Section 7.5.1).
package workflow

import (
"bytes"
"encoding/json"
"testing"

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

// formalDriftRecordJSON mirrors the Section 3.1.1 JSON schema field names
// (snake_case) for strict decoding. FormalDriftRecord itself (defined in
// awf_config_drift_formal_test.go) has no json tags, so it round-trips only
// through Go-style field names; this local type is used solely to validate
// the wire-format "additionalProperties: false" constraint.
type formalDriftRecordJSON struct {
PropertyPath string `json:"property_path"`
DriftCategory string `json:"drift_category"`
SuggestedAction string `json:"suggested_action"`
DetectedAt string `json:"detected_at"`
}

// formalDriftRecordNoAdditionalProperties re-validates T-DR-005 within the
// formal predicate series: a DriftRecord JSON payload MUST decode into
// exactly the four schema-defined fields (property_path, drift_category,
// suggested_action, detected_at) and MUST reject any additional property.
func formalDriftRecordNoAdditionalProperties(raw []byte) (FormalDriftRecord, error) {
dec := json.NewDecoder(bytes.NewReader(raw))
dec.DisallowUnknownFields()

var wire formalDriftRecordJSON
if err := dec.Decode(&wire); err != nil {
return FormalDriftRecord{}, err
}
return FormalDriftRecord{
PropertyPath: wire.PropertyPath,
DriftCategory: wire.DriftCategory,
SuggestedAction: wire.SuggestedAction,
DetectedAt: wire.DetectedAt,
}, nil
}

// formalCorrectivePREmbedsFullDriftList mirrors the production contract of
// Section 7.5.1: a corrective PR body MUST embed the *entire* DriftRecord
// list, serialized as JSON, with field order and content preserved
// round-trip. An empty slice serializes to "[]" (T-DR-009 companion case).
func formalCorrectivePREmbedsFullDriftList(records []FormalDriftRecord) (string, error) {
if records == nil {
records = []FormalDriftRecord{}
}
body, err := json.Marshal(records)
if err != nil {
return "", err
}
return string(body), nil
}

// formalEmptyDriftListValidNoTrigger asserts T-DR-009: an empty DriftRecord
// list is a conformant Step-5 output, and MUST NOT, by itself, require a
// corrective PR or SLA escalation regardless of elapsed time.
func formalEmptyDriftListValidNoTrigger(records []FormalDriftRecord, slaWindowExceeded bool) (requiresCorrectivePR, requiresEscalation bool) {
for _, r := range records {
if formalCorrectionPRForActionableDrift(r.DriftCategory) {
requiresCorrectivePR = true
}
}
requiresEscalation = requiresCorrectivePR && slaWindowExceeded
return
}

func TestFormal_P25_DriftRecordNoAdditionalProperties(t *testing.T) {
valid := []byte(`{"property_path":"apiProxy.anthropicAutoCache","drift_category":"missing_in_ghaw","suggested_action":"Add coverage","detected_at":"2026-06-08T00:00:00Z"}`)
record, err := formalDriftRecordNoAdditionalProperties(valid)
require.NoError(t, err, "a DriftRecord with exactly the four schema fields must decode successfully")
assert.Equal(t, "apiProxy.anthropicAutoCache", record.PropertyPath, "property_path must round-trip through strict decoding")
assert.True(t, formalDriftRecordStructuralValidity(record), "strictly-decoded record must also satisfy P3 structural validity")

withExtra := []byte(`{"property_path":"x","drift_category":"missing_in_ghaw","suggested_action":"y","detected_at":"2026-06-08T00:00:00Z","extra_field":"nope"}`)
_, err = formalDriftRecordNoAdditionalProperties(withExtra)
assert.Error(t, err, "T-DR-005: a DriftRecord with any additional property MUST be rejected")
}

func TestFormal_P25_DriftRecordNoAdditionalProperties_MultipleExtraFields(t *testing.T) {
withExtras := []byte(`{"property_path":"x","drift_category":"spec_mismatch","suggested_action":"y","detected_at":"2026-06-08T00:00:00Z","note":"should not exist","severity":"high"}`)
_, err := formalDriftRecordNoAdditionalProperties(withExtras)
assert.Error(t, err, "T-DR-005: rejection must hold even when multiple additional properties are present, not just one")
}

func TestFormal_P26_CorrectivePREmbedsFullDriftList(t *testing.T) {
records := []FormalDriftRecord{
{
PropertyPath: "apiProxy.anthropicAutoCache",
DriftCategory: "missing_in_ghaw",
SuggestedAction: "Add coverage for apiProxy.anthropicAutoCache",
DetectedAt: "2026-06-08T00:00:00Z",
},
{
PropertyPath: "container.dockerHostPathPrefix",
DriftCategory: "spec_mismatch",
SuggestedAction: "Reconcile CLI mapping table",
DetectedAt: "2026-06-09T00:00:00Z",
},
}

body, err := formalCorrectivePREmbedsFullDriftList(records)
require.NoError(t, err, "marshaling a populated DriftRecord list must not error")

var decoded []FormalDriftRecord
require.NoError(t, json.Unmarshal([]byte(body), &decoded), "corrective PR body must be valid JSON")
assert.Equal(t, records, decoded, "T-DR-008: corrective PR body MUST embed the complete DriftRecord list without truncation or re-ordering")
}

func TestFormal_P26_CorrectivePREmbedsFullDriftList_EmptyList(t *testing.T) {
body, err := formalCorrectivePREmbedsFullDriftList([]FormalDriftRecord{})
require.NoError(t, err, "marshaling an empty DriftRecord list must not error")
assert.Equal(t, "[]", body, "an empty DriftRecord list must serialize to the JSON empty array, not null or omitted")

bodyFromNil, err := formalCorrectivePREmbedsFullDriftList(nil)
require.NoError(t, err, "marshaling a nil DriftRecord slice must not error")
assert.Equal(t, "[]", bodyFromNil, "a nil DriftRecord slice must normalize to the JSON empty array, matching the non-nil empty-slice case")
}

func TestFormal_P27_EmptyDriftListValidNoTrigger(t *testing.T) {
requiresPR, requiresEscalation := formalEmptyDriftListValidNoTrigger(nil, true)
assert.False(t, requiresPR, "T-DR-009: an empty DriftRecord list MUST NOT require a corrective PR, even when the SLA window is exceeded")
assert.False(t, requiresEscalation, "T-DR-009: an empty DriftRecord list MUST NOT trigger SLA escalation")

requiresPR, requiresEscalation = formalEmptyDriftListValidNoTrigger([]FormalDriftRecord{}, true)
assert.False(t, requiresPR, "an explicitly empty (non-nil) slice must behave identically to a nil slice for trigger purposes")
assert.False(t, requiresEscalation, "an explicitly empty (non-nil) slice must not trigger escalation")
}

func TestFormal_P27_EmptyDriftListValidNoTrigger_NonEmptyStillTriggers(t *testing.T) {
actionable := []FormalDriftRecord{{PropertyPath: "apiProxy.foo", DriftCategory: "missing_in_ghaw", SuggestedAction: "fix", DetectedAt: "2026-06-08T00:00:00Z"}}

requiresPR, requiresEscalation := formalEmptyDriftListValidNoTrigger(actionable, true)
assert.True(t, requiresPR, "sanity check: a non-empty actionable-category list must still require a corrective PR")
assert.True(t, requiresEscalation, "sanity check: a non-empty actionable-category list past the SLA window must still require escalation")

requiresPR, requiresEscalation = formalEmptyDriftListValidNoTrigger(actionable, false)
assert.True(t, requiresPR, "corrective PR obligation is independent of SLA window state")
assert.False(t, requiresEscalation, "escalation must not fire before the SLA window is exceeded, even with actionable drift present")
}
```

### Usage

1. Copy the test file to `pkg/workflow/awf_config_drift_extended_formal_test.go`.
2. No stubs to replace — `FormalDriftRecord` (from `awf_config_drift_formal_test.go`) and `formalCorrectionPRForActionableDrift` (from the same file) are reused directly; all 8 test functions already pass against these existing types (verified locally with `go test ./pkg/workflow/ -run 'TestFormal_P2[567]'`, and `go build ./pkg/workflow/...` succeeds).
3. Run: `go test ./pkg/workflow/... -run Formal`

### Context

- Spec processed: `specs/awf-config-sources-spec.md`
- Formal notation: TLA+-style predicate logic / Z3-style guard conjunction
- Prior predicates P1–P24 unchanged; this run adds P25–P27 closing the T-DR-005/T-DR-008/T-DR-009 formal-coverage gap
- Run: https://github.com/github/gh-aw/actions/runs/35115609786

> Generated by [🔬 Daily Formal Spec Verifier](https://github.com/github/gh-aw/actions/runs/35115609786) · copilot · auto · 140.2 AIC · ⌖ 8.14 AIC · ⊞ 10.5K · [◷](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 Sep 23, 2026, 7:42 AM UTC-08:00

Start with pkg/workflow/awf_config_drift_extended_formal_test.go, then read the related formal tests named in its comments and specs/awf-config-sources-spec.md §§3.1.1 and 7.5.1. Run the formal workflow tests and verify P25 rejects unknown fields, P26 preserves complete DriftRecord lists, and P27 treats empty lists as valid without triggering remediation.

Written by the indexing model from the issue text.