// awfconfig_formal_test.go
//
// Formal specification: specs/awf-config-sources-spec.md
// Version: 0.1.0
//
// Encoded predicates (see Formal Model section in the companion GitHub issue):
// P1 DualSourceConsultation — agents must consult both spec and schema
// P2 NoUndocumentedFields — generated fields must be schema/spec-declared
// P3 DriftDetectionTrigger — drift runs on schema changes, schedules, explicit requests
// P4 DriftCategoryExhaustive — exactly three valid drift_category values
// P5 DriftRecordRequiredFields — all four required fields must be non-empty
// P6 CorrectionPROnDrift — PR required for missing_in_ghaw / spec_mismatch
// P7 SLARemediationWindow — remediation within 5 business days
// P8 EscalationIssueRequired — escalation issue within 1 day of SLA miss
// P9 EscalationOwnerAssigned — escalation issue must have non-empty owner
// P10 DegradedModeOnSourceFailure — destructive actions skipped when sources unavailable
// P11 SchemaPropertyCoverage — all top-level schema props covered in gh-aw refs
// P12 PropertyPathDotNotation — property_path non-empty, no leading/trailing dots
// P13 NoAdditionalProperties — DriftRecord has exactly four fields when serialized
package awfconfig_test
import (
"encoding/json"
"strings"
"testing"
"time"
"github.com/stretchr/testify/assert"
"github.com/stretchr/testify/require"
)
// ---------------------------------------------------------------------------
// stub — replace with real implementation
// ---------------------------------------------------------------------------
// DriftCategory enumerates the three exhaustive drift categories (P4).
type DriftCategory string
const (
DriftCategoryMissingInGhaw DriftCategory = "missing_in_ghaw"
DriftCategoryMissingInSchema DriftCategory = "missing_in_schema"
DriftCategorySpecMismatch DriftCategory = "spec_mismatch"
)
// DriftRecord is the formal schema from §6.5.1 of the spec.
type DriftRecord struct {
PropertyPath string `json:"property_path"`
DriftCategory DriftCategory `json:"drift_category"`
SuggestedAction string `json:"suggested_action"`
DetectedAt time.Time `json:"detected_at"`
}
// ConfigAction models a single config-generation or validation action consulted sources.
type ConfigAction struct {
ConsultedSources []string
GeneratedFields []string
}
// DriftTriggerEvent is the kind of event that must trigger drift detection (§6.1).
type DriftTriggerEvent string
const (
DriftTriggerSchemaChanged DriftTriggerEvent = "schema_file_changed"
DriftTriggerScheduledRun DriftTriggerEvent = "scheduled_run"
DriftTriggerAgentConfigReq DriftTriggerEvent = "agent_config_request"
)
// RunState models the state of a drift-detection workflow run.
type RunState struct {
CanonicalSourceAvailable bool
DestructiveActionsSkipped bool
Status string
CorrectivePROpened bool
DriftIssueOpened bool
}
// EscalationIssue models a CR-06 escalation tracking issue.
type EscalationIssue struct {
Owner string
OpenedAt time.Time
OwnerAckAt time.Time
}
// stub functions — replace with real implementation
// consultsRequiredSources returns true iff the action consulted both canonical sources (P1).
func consultsRequiredSources(action ConfigAction) bool {
required := map[string]bool{
"docs/awf-config-spec.md": false,
"docs/awf-config.schema.json": false,
}
for _, s := range action.ConsultedSources {
if _, ok := required[s]; ok {
required[s] = true
}
}
for _, found := range required {
if !found {
return false
}
}
return true
}
// allFieldsDocumented returns true iff every generated field appears in schemaFields ∪ specFields (P2).
func allFieldsDocumented(generated, schemaFields, specFields []string) bool {
allowed := make(map[string]struct{})
for _, f := range schemaFields {
allowed[f] = struct{}{}
}
for _, f := range specFields {
allowed[f] = struct{}{}
}
for _, f := range generated {
if _, ok := allowed[f]; !ok {
return false
}
}
return true
}
// driftTriggerRequired returns true iff the given event type mandates drift detection (P3).
func driftTriggerRequired(event DriftTriggerEvent) bool {
switch event {
case DriftTriggerSchemaChanged, DriftTriggerScheduledRun, DriftTriggerAgentConfigReq:
return true
}
return false
}
// isValidDriftCategory returns true iff category is one of the three allowed values (P4).
func isValidDriftCategory(cat DriftCategory) bool {
switch cat {
case DriftCategoryMissingInGhaw, DriftCategoryMissingInSchema, DriftCategorySpecMismatch:
return true
}
return false
}
// validateDriftRecord returns true iff all required fields are non-empty (P5).
func validateDriftRecord(r DriftRecord) bool {
return r.PropertyPath != "" &&
isValidDriftCategory(r.DriftCategory) &&
r.SuggestedAction != "" &&
!r.DetectedAt.IsZero()
}
// correctivePRRequired returns true iff any record demands a corrective PR (P6).
func correctivePRRequired(records []DriftRecord) bool {
for _, r := range records {
if r.DriftCategory == DriftCategoryMissingInGhaw || r.DriftCategory == DriftCategorySpecMismatch {
return true
}
}
return false
}
// slaDeadline returns the business-day deadline for remediating a drift record.
// For simplicity in tests, business days are modeled as calendar days * 1
// (replace with real business-day calendar in production).
func slaDeadline(detectedAt time.Time) time.Time {
// 5 business days — simplified to 7 calendar days to account for weekends in a worst-case scenario.
return detectedAt.Add(7 * 24 * time.Hour)
}
// slaBreachAt returns the deadline itself (same as slaDeadline for stub).
func slaBreachAt(detectedAt time.Time) time.Time { return slaDeadline(detectedAt) }
// escalationDeadline returns the deadline for opening an escalation issue after SLA miss.
func escalationDeadline(slaBreachTime time.Time) time.Time {
return slaBreachTime.Add(24 * time.Hour) // 1 business day
}
// degradedModeSafe returns true iff the run correctly applies degraded-mode safeguards (P10).
func degradedModeSafe(run RunState) bool {
if !run.CanonicalSourceAvailable {
return run.DestructiveActionsSkipped &&
run.Status == "degraded" &&
!run.CorrectivePROpened &&
!run.DriftIssueOpened
}
return true
}
// schemaPropertiesCovered returns true iff every schema property has a matching ref in ghawRefs (P11).
func schemaPropertiesCovered(schemaProps, ghawRefs []string) bool {
refs := make(map[string]struct{})
for _, r := range ghawRefs {
refs[r] = struct{}{}
}
for _, p := range schemaProps {
if _, ok := refs[p]; !ok {
return false
}
}
return true
}
// isValidPropertyPath returns true iff path is non-empty and uses valid dot-notation (P12).
func isValidPropertyPath(path string) bool {
if path == "" {
return false
}
if strings.HasPrefix(path, ".") || strings.HasSuffix(path, ".") {
return false
}
parts := strings.Split(path, ".")
for _, part := range parts {
if part == "" {
return false // consecutive dots
}
}
return true
}
// driftRecordJSONKeys returns the set of JSON keys present in a marshalled DriftRecord (P13).
func driftRecordJSONKeys(r DriftRecord) (map[string]struct{}, error) {
data, err := json.Marshal(r)
if err != nil {
return nil, err
}
var raw map[string]json.RawMessage
if err := json.Unmarshal(data, &raw); err != nil {
return nil, err
}
keys := make(map[string]struct{}, len(raw))
for k := range raw {
keys[k] = struct{}{}
}
return keys, nil
}
// ---------------------------------------------------------------------------
// Tests
// ---------------------------------------------------------------------------
// TestDualSourceConsultation encodes P1: config actions must consult both canonical sources.
func TestDualSourceConsultation(t *testing.T) {
cases := []struct {
name string
sources []string
want bool
}{
{
name: "both sources present",
sources: []string{"docs/awf-config-spec.md", "docs/awf-config.schema.json", "docs/environment.md"},
want: true,
},
{
name: "only spec consulted",
sources: []string{"docs/awf-config-spec.md"},
want: false,
},
{
name: "only schema consulted",
sources: []string{"docs/awf-config.schema.json"},
want: false,
},
{
name: "no sources consulted",
sources: []string{},
want: false,
},
}
for _, tc := range cases {
t.Run(tc.name, func(t *testing.T) {
action := ConfigAction{ConsultedSources: tc.sources}
got := consultsRequiredSources(action)
assert.Equal(t, tc.want, got, "P1 DualSourceConsultation: expected %v for sources %v", tc.want, tc.sources)
})
}
}
// TestNoUndocumentedFieldsGenerated encodes P2: generated fields must be in schema ∪ spec.
func TestNoUndocumentedFieldsGenerated(t *testing.T) {
schemaFields := []string{"apiProxy.anthropicAutoCache", "apiProxy.models", "container.dockerHostPathPrefix"}
specFields := []string{"apiProxy.anthropicCacheTailTtl", "apiProxy.maxRuns"}
cases := []struct {
name string
generated []string
want bool
}{
{
name: "all fields documented",
generated: []string{"apiProxy.anthropicAutoCache", "apiProxy.maxRuns"},
want: true,
},
{
name: "undocumented field present",
generated: []string{"apiProxy.unknownField"},
want: false,
},
{
name: "empty generated set",
generated: []string{},
want: true,
},
}
for _, tc := range cases {
t.Run(tc.name, func(t *testing.T) {
got := allFieldsDocumented(tc.generated, schemaFields, specFields)
assert.Equal(t, tc.want, got, "P2 NoUndocumentedFields: generated=%v", tc.generated)
})
}
}
// TestDriftTriggerConditions encodes P3: drift detection must run for required event types.
func TestDriftTriggerConditions(t *testing.T) {
cases := []struct {
event DriftTriggerEvent
want bool
}{
{DriftTriggerSchemaChanged, true},
{DriftTriggerScheduledRun, true},
{DriftTriggerAgentConfigReq, true},
{"pull_request_opened", false},
{"push_to_main", false},
}
for _, tc := range cases {
t.Run(string(tc.event), func(t *testing.T) {
got := driftTriggerRequired(tc.event)
assert.Equal(t, tc.want, got, "P3 DriftTrigger: event %q should trigger=%v", tc.event, tc.want)
})
}
}
// TestDriftCategoryValues encodes P4: only three valid drift_category values exist.
func TestDriftCategoryValues(t *testing.T) {
valid := []DriftCategory{
DriftCategoryMissingInGhaw,
DriftCategoryMissingInSchema,
DriftCategorySpecMismatch,
}
for _, cat := range valid {
assert.True(t, isValidDriftCategory(cat), "P4: %q should be a valid DriftCategory", cat)
}
invalid := []DriftCategory{"", "unknown", "MISSING_IN_GHAW", "missing-in-ghaw"}
for _, cat := range invalid {
assert.False(t, isValidDriftCategory(cat), "P4: %q should NOT be a valid DriftCategory", cat)
}
}
// TestDriftRecordRequiredFields encodes P5: all four required fields must be non-empty.
func TestDriftRecordRequiredFields(t *testing.T) {
base := DriftRecord{
PropertyPath: "apiProxy.anthropicAutoCache",
DriftCategory: DriftCategoryMissingInGhaw,
SuggestedAction: "Add coverage in pkg/workflow/",
DetectedAt: time.Now(),
}
t.Run("valid record", func(t *testing.T) {
assert.True(t, validateDriftRecord(base), "P5: a fully-populated DriftRecord should be valid")
})
t.Run("missing property_path", func(t *testing.T) {
r := base
r.PropertyPath = ""
assert.False(t, validateDriftRecord(r), "P5: empty property_path must be invalid")
})
t.Run("missing suggested_action", func(t *testing.T) {
r := base
r.SuggestedAction = ""
assert.False(t, validateDriftRecord(r), "P5: empty suggested_action must be invalid")
})
t.Run("zero detected_at", func(t *testing.T) {
r := base
r.DetectedAt = time.Time{}
assert.False(t, validateDriftRecord(r), "P5: zero detected_at must be invalid")
})
t.Run("invalid drift_category", func(t *testing.T) {
r := base
r.DriftCategory = "bogus"
assert.False(t, validateDriftRecord(r), "P5: unknown drift_category must be invalid")
})
}
// TestCorrectionPRRequired encodes P6: a corrective PR must be opened for actionable drift.
func TestCorrectionPRRequired(t *testing.T) {
cases := []struct {
name string
records []DriftRecord
want bool
}{
{
name: "missing_in_ghaw triggers PR",
records: []DriftRecord{
{PropertyPath: "apiProxy.models", DriftCategory: DriftCategoryMissingInGhaw},
},
want: true,
},
{
name: "spec_mismatch triggers PR",
records: []DriftRecord{
{PropertyPath: "container.dockerHostPathPrefix", DriftCategory: DriftCategorySpecMismatch},
},
want: true,
},
{
name: "missing_in_schema does not trigger PR",
records: []DriftRecord{
{PropertyPath: "apiProxy.undocumentedExtra", DriftCategory: DriftCategoryMissingInSchema},
},
want: false,
},
{
name: "empty record list — no PR",
records: []DriftRecord{},
want: false,
},
{
name: "mixed: at least one actionable record",
records: []DriftRecord{
{PropertyPath: "apiProxy.undocumentedExtra", DriftCategory: DriftCategoryMissingInSchema},
{PropertyPath: "apiProxy.models", DriftCategory: DriftCategoryMissingInGhaw},
},
want: true,
},
}
for _, tc := range cases {
t.Run(tc.name, func(t *testing.T) {
got := correctivePRRequired(tc.records)
assert.Equal(t, tc.want, got, "P6 CorrectionPRRequired: records=%v", tc.records)
})
}
}
// TestSLARemediationWindow encodes P7: drift must be remediated within the SLA window.
func TestSLARemediationWindow(t *testing.T) {
base := time.Date(2026, 7, 1, 0, 0, 0, 0, time.UTC)
t.Run("within window is not yet breached", func(t *testing.T) {
now := base.Add(3 * 24 * time.Hour)
deadline := slaDeadline(base)
assert.True(t, now.Before(deadline), "P7: 3 days after detection should be within the 5-bd SLA window")
})
t.Run("exactly at deadline is not yet breached", func(t *testing.T) {
deadline := slaDeadline(base)
assert.False(t, base.After(deadline), "P7: detection time must not exceed its own deadline")
})
t.Run("past deadline is breached", func(t *testing.T) {
now := base.Add(8 * 24 * time.Hour)
deadline := slaDeadline(base)
assert.True(t, now.After(deadline), "P7: 8 days after detection should exceed the 5-bd SLA window")
})
}
// TestEscalationIssueOnSLABreach encodes P8: escalation issue must open within 1 day of SLA miss.
func TestEscalationIssueOnSLABreach(t *testing.T) {
detectedAt := time.Date(2026, 7, 1, 0, 0, 0, 0, time.UTC)
breach := slaBreachAt(detectedAt)
t.Run("escalation within 1 day of breach is timely", func(t *testing.T) {
escalationOpenedAt := breach.Add(12 * time.Hour) // within 1 business day
deadline := escalationDeadline(breach)
assert.True(t, escalationOpenedAt.Before(deadline) || escalationOpenedAt.Equal(deadline),
"P8: escalation opened 12h after breach should be within the 1-day escalation window")
})
t.Run("escalation more than 1 day after breach is late", func(t *testing.T) {
escalationOpenedAt := breach.Add(36 * time.Hour)
deadline := escalationDeadline(breach)
assert.True(t, escalationOpenedAt.After(deadline),
"P8: escalation opened 36h after breach should exceed the 1-day escalation deadline")
})
}
// TestEscalationOwnerAssigned encodes P9: escalation issue must have a non-empty owner.
func TestEscalationOwnerAssigned(t *testing.T) {
base := time.Date(2026, 7, 1, 0, 0, 0, 0, time.UTC)
t.Run("owner assigned and acked in time", func(t *testing.T) {
issue := EscalationIssue{
Owner: "octocat",
OpenedAt: base,
OwnerAckAt: base.Add(12 * time.Hour),
}
require.NotEmpty(t, issue.Owner, "P9: escalation issue must have an owner")
assert.True(t, issue.OwnerAckAt.Before(issue.OpenedAt.Add(24*time.Hour)),
"P9: owner must acknowledge within 1 business day of issue opening")
})
t.Run("unassigned escalation issue is invalid", func(t *testing.T) {
issue := EscalationIssue{Owner: "", OpenedAt: base}
assert.Empty(t, issue.Owner, "P9: this test confirms an unassigned escalation is caught")
// The predicate fails for empty owner
assert.False(t, issue.Owner != "", "P9: empty owner should not satisfy assignment requirement")
})
t.Run("late acknowledgement violates P9", func(t *testing.T) {
issue := EscalationIssue{
Owner: "octocat",
OpenedAt: base,
OwnerAckAt: base.Add(48 * time.Hour), // 2 business days — too late
}
require.NotEmpty(t, issue.Owner, "P9: owner is present")
assert.False(t, issue.OwnerAckAt.Before(issue.OpenedAt.Add(24*time.Hour)),
"P9: acknowledgement after 48h should violate the 1-bd ack window")
})
}
// TestDegradedModeOnCanonicalSourceFailure encodes P10: destructive actions must be skipped when sources are unavailable.
func TestDegradedModeOnCanonicalSourceFailure(t *testing.T) {
t.Run("degraded mode prevents destructive actions", func(t *testing.T) {
run := RunState{
CanonicalSourceAvailable: false,
DestructiveActionsSkipped: true,
Status: "degraded",
CorrectivePROpened: false,
DriftIssueOpened: false,
}
assert.True(t, degradedModeSafe(run), "P10: proper degraded-mode run must be safe")
})
t.Run("destructive action while degraded is unsafe", func(t *testing.T) {
run := RunState{
CanonicalSourceAvailable: false,
DestructiveActionsSkipped: false, // violation
Status: "degraded",
CorrectivePROpened: true, // violation
}
assert.False(t, degradedModeSafe(run), "P10: corrective PR opened during degraded mode violates safeguard")
})
t.Run("normal run with sources available is not constrained", func(t *testing.T) {
run := RunState{
CanonicalSourceAvailable: true,
DestructiveActionsSkipped: false,
Status: "success",
CorrectivePROpened: true,
}
assert.True(t, degradedModeSafe(run), "P10: normal run is not subject to degraded-mode constraint")
})
}
// TestSchemaPropertyFullCoverage encodes P11: all top-level schema properties must be in gh-aw refs.
func TestSchemaPropertyFullCoverage(t *testing.T) {
schemaProps := []string{
"apiProxy.anthropicAutoCache",
"apiProxy.anthropicCacheTailTtl",
"apiProxy.models",
"container.dockerHostPathPrefix",
}
t.Run("full coverage", func(t *testing.T) {
ghawRefs := []string{
"apiProxy.anthropicAutoCache",
"apiProxy.anthropicCacheTailTtl",
"apiProxy.models",
"container.dockerHostPathPrefix",
"apiProxy.maxRuns", // extra refs are fine
}
assert.True(t, schemaPropertiesCovered(schemaProps, ghawRefs),
"P11: all schema properties covered in gh-aw refs")
})
t.Run("missing coverage", func(t *testing.T) {
ghawRefs := []string{
"apiProxy.anthropicAutoCache",
"apiProxy.models",
// apiProxy.anthropicCacheTailTtl and container.dockerHostPathPrefix missing
}
assert.False(t, schemaPropertiesCovered(schemaProps, ghawRefs),
"P11: missing schema property coverage must be detected")
})
t.Run("empty schema — trivially covered", func(t *testing.T) {
assert.True(t, schemaPropertiesCovered([]string{}, []string{}),
"P11: empty schema is trivially fully covered")
})
}
// TestDriftRecordPropertyPathFormat encodes P12: property_path must be valid dot-notation.
func TestDriftRecordPropertyPathFormat(t *testing.T) {
cases := []struct {
path string
valid bool
}{
{"apiProxy.anthropicAutoCache", true},
{"container.dockerHostPathPrefix", true},
{"apiProxy.auth.token", true},
{"topLevelOnly", true},
{"", false},
{".leadingDot", false},
{"trailingDot.", false},
{"double..dot", false},
{"apiProxy.", false},
{".apiProxy", false},
}
for _, tc := range cases {
t.Run(tc.path, func(t *testing.T) {
got := isValidPropertyPath(tc.path)
assert.Equal(t, tc.valid, got,
"P12 PropertyPathDotNotation: path=%q expected valid=%v", tc.path, tc.valid)
})
}
}
// TestDriftRecordNoExtraFields encodes P13: serialized DriftRecord must contain exactly the four declared fields.
func TestDriftRecordNoExtraFields(t *testing.T) {
r := DriftRecord{
PropertyPath: "apiProxy.models",
DriftCategory: DriftCategoryMissingInGhaw,
SuggestedAction: "Add coverage",
DetectedAt: time.Date(2026, 7, 1, 0, 0, 0, 0, time.UTC),
}
keys, err := driftRecordJSONKeys(r)
require.NoError(t, err, "P13: DriftRecord must serialize without error")
expected := map[string]struct{}{
"property_path": {},
"drift_category": {},
"suggested_action": {},
"detected_at": {},
}
assert.Equal(t, expected, keys,
"P13 NoAdditionalProperties: serialized DriftRecord must contain exactly the four declared fields")
}
Summary
specs/awf-config-sources-spec.mddefines the canonical AWF configuration source-of-truth contract forgithub/gh-aw: which documents agents MUST consult, how schema drift is detected and categorized, theDriftRecordentity schema, SLA obligations for remediation, and safeguard behavior when canonical sources are unavailable. This formalization models the specification as a state machine (TLA+), a set of typed contracts (F*), and arithmetic/constraint predicates (Z3), covering all conformance requirements (CR-01 through CR-06a) and theDriftRecordschema invariants.Specification
specs/awf-config-sources-spec.mdDriftRecordlifecycleFormal Model
Predicates and invariants (illustrative notation)
P1 — DualSourceConsultation (TLA+)
P2 — NoDriftFieldGeneration (TLA+)
P3 — DriftDetectionTrigger (TLA+)
P4 — DriftCategoryExhaustive (Z3 / SMT)
P5 — DriftRecordRequiredFields (Z3 / SMT)
P6 — CorrectionPROnDrift (F)*
P7 — SLARemediationWindow (TLA+ / temporal)
P8 — EscalationIssueRequired (TLA+ / temporal)
P9 — EscalationOwnerAssigned (F)*
P10 — DegradedModeOnSourceFailure (TLA+)
P11 — SchemaPropertyCoverage (F)*
P12 — PropertyPathDotNotation (Z3)
P13 — NoAdditionalProperties (Z3)
Behavioral Coverage Map
DualSourceConsultation(P1)TestDualSourceConsultationNoUndocumentedFields(P2)TestNoUndocumentedFieldsGeneratedDriftDetectionTrigger(P3)TestDriftTriggerConditionsDriftCategoryExhaustive(P4)TestDriftCategoryValuesDriftRecordRequiredFields(P5)TestDriftRecordRequiredFieldsCorrectionPROnDrift(P6)TestCorrectionPRRequiredSLARemediationWindow(P7)TestSLARemediationWindowEscalationIssueRequired(P8)TestEscalationIssueOnSLABreachEscalationOwnerAssigned(P9)TestEscalationOwnerAssignedDegradedModeOnSourceFailure(P10)TestDegradedModeOnCanonicalSourceFailureSchemaPropertyCoverage(P11)TestSchemaPropertyFullCoveragePropertyPathDotNotation(P12)TestDriftRecordPropertyPathFormatNoAdditionalProperties(P13)TestDriftRecordNoExtraFieldsGenerated Test Suite
📄 `pkg/awfconfig/awfconfig_formal_test.go`
Usage
pkg/awfconfig/awfconfig_formal_test.go(create the package directory if absent).// stubinterfaces and functions with real implementations frompkg/workflow/oractions/setup/.go test ./pkg/awfconfig/... -run FormalContext
specs/awf-config-sources-spec.md