[formal-spec] compiler-threat-detection-compliance/README.md — Formal model & test suite — 2026-08-23

[github-actions]

Summary

This run extends the prior formalization of specs/compiler-threat-detection-compliance/README.md (2026-08-15, catalog-level bijection predicates only) by formalizing the suppression lifecycle norms (§6.4 False-Positive Handling, T-CTR-024/025/029) and the rule deprecation lifecycle (§5.4 Deprecation Policy) from the parent specification specs/compiler-threat-detection-spec.md. These norms govern how workflow authors suppress false-positive CTR-* diagnostics, how those suppressions are audited and expire, and how a CTR-* rule is formally retired without breaking historical traceability.

Specification

• File: specs/compiler-threat-detection-compliance/README.md (cross-referencing specs/compiler-threat-detection-spec.md §5.4, §6.4)
• Focus area: Suppression validation/audit/expiration lifecycle and rule deprecation lifecycle
• Formal notation used: Z3-style guard conjunction / small state-machine (deprecation status transition)

Formal Model

Predicates and invariants (illustrative notation)

; P1 SuppressionRequiresRuleAndReason  (T-CTR-024)
; source: "A suppression without a `reason` MUST NOT be accepted by the
;          compiler; the compiler MUST emit a validation error if `reason`
;          is absent or empty."
(assert (forall ((s Suppression))
  (=> (valid s)
      (and (matches (rule s) "^CTR-\\d{3}$")
           (> (str.len (trim (reason s))) 0)))))

; P2 SuppressionRuleFormatWellFormed (T-CTR-024)
; source: same paragraph — rule field "the CTR-* identifier"
(assert (forall ((s Suppression))
  (=> (valid s) (matches (rule s) "^CTR-\\d{3}$"))))

; P3 SuppressionExpiresISO8601OrAbsent (T-CTR-024)
; source: "optional `expires` field (ISO 8601 date after which the
;          suppression is no longer valid)"
(assert (forall ((s Suppression))
  (=> (valid s)
      (or (absent (expires s)) (iso8601-date (expires s))))))

; P4 ActiveSuppressionRetainsAuditFields (T-CTR-025)
; source: "Every active suppression annotation MUST be recorded in the
;          compiled lock file ... MUST include the full `rule`, `reason`,
;          and `expires` values for each suppression."
(assert (forall ((s Suppression))
  (=> (active s now)
      (and (= (audit-rule s)   (rule s))
           (= (audit-reason s) (reason s))
           (= (audit-expires s)(expires s))))))

; P5 ExpiredSuppressionTreatedAsAbsent (T-CTR-029)
; source: "expired suppressions MUST be treated by the compiler as if they
;          do not exist."
(assert (forall ((s Suppression) (t Date))
  (=> (and (present (expires s)) (< (expires s) t))
      (not (suppressed-at s t)))))

; P6 SuppressionBoundaryDayStillActive (T-CTR-029, edge case)
; derived corollary: expires is inclusive of its own calendar day
(assert (forall ((s Suppression) (t Date))
  (=> (= (expires s) t) (suppressed-at s t))))

; P7 DiagnosticSuppressionRequiresMatchingRule (T-CTR-024/025)
; derived: suppression scope is per-rule, not global
(assert (forall ((d Diagnostic) (s Suppression) (t Date))
  (=> (diagnostic-suppressed d s t)
      (= (diagnostic-rule d) (rule s)))))

;; --- TLA+-style state machine: §5.4 Deprecation Policy ---
;; States: Active -> Deprecated  (one-way, monotonic; no un-deprecation)
;;
;; P8 DeprecatedRuleRetainsCatalogRow (§5.4)
;; source: "The rule catalog entry MUST be retained (not deleted) with a
;;          deprecation notice indicating the version ... and the reason."
;; Init  == status \in [CTR_Rules -> {"Active"}]
;; Next  == \E r \in CTR_Rules :
;;            /\ status[r] = "Active"
;;            /\ status' = [status EXCEPT ![r] = "Deprecated"]
;;            /\ r \in DOMAIN status'          \* row retained, never removed
;;
;; P9 DeprecatedRuleExcludedFromRequiredGate (§5.4, §5.3)
;; source: "All test IDs mapped to the deprecated rule ... MUST be marked
;;          [DEPRECATED] and MUST NOT be required for conformance after the
;;          deprecation version."
;; Invariant == \A r \in CTR_Rules :
;;                status[r] = "Deprecated" => r \notin RequiredConformanceGate

Behavioral Coverage Map

Predicate / Invariant	Test Function	Description
SuppressionRequiresRuleAndReason	TestFormal_SuppressionRequiresRuleAndReason	Rejects suppressions with empty, whitespace-only, or missing reason; accepts a well-formed one
SuppressionRuleFormatWellFormed	TestFormal_SuppressionRuleFormatWellFormed	Rejects malformed/empty rule identifiers not matching CTR-\d{3}
SuppressionExpiresISO8601OrAbsent	TestFormal_SuppressionExpiresISO8601OrAbsent	Accepts absent/valid ISO 8601 expires; rejects non-ISO or invalid calendar dates
ActiveSuppressionRetainsAuditFields	TestFormal_ActiveSuppressionRetainsAuditFields	Confirms parsed suppression retains exact rule, reason, expires for audit
ExpiredSuppressionTreatedAsAbsent	TestFormal_ExpiredSuppressionTreatedAsAbsent	A suppression with a past expires date is reported as not-suppressed
SuppressionBoundaryDayStillActive	TestFormal_SuppressionBoundaryDayStillActive	Suppression remains active on its own expires day; expires the next day (edge case)
DiagnosticSuppressionRequiresMatchingRule	TestFormal_DiagnosticSuppressionRequiresMatchingRule	A suppression for one rule does not suppress a diagnostic for a different rule (edge case)
DeprecatedRuleRetainsCatalogRow	TestFormal_DeprecatedRuleRetainsCatalogRow	Deprecated rule's catalog row/status is retained, not deleted (stub)
DeprecatedRuleExcludedFromRequiredGate	TestFormal_DeprecatedRuleExcludedFromRequiredGate	Deprecated rule is excluded from the required conformance gate; active rule remains required (stub)

Generated Test Suite

📄 pkg/workflow/threat_detection_suppression_lifecycle_formal_test.go

// Package workflow provides formal-model-derived tests (internal test package,
// required for access to unexported suppression-parsing helpers) for the
// Section 5.4 Deprecation Policy and Section 6.4 False-Positive Handling
// (suppression lifecycle) norms of specs/compiler-threat-detection-spec.md,
// as summarized in specs/compiler-threat-detection-compliance/README.md.
//
// Formal predicates encoded (see issue body "Formal Model" for full notation):
//
//   P1  SuppressionRequiresRuleAndReason      (T-CTR-024)
//   P2  SuppressionRuleFormatWellFormed       (T-CTR-024)
//   P3  SuppressionExpiresISO8601OrAbsent     (T-CTR-024)
//   P4  ActiveSuppressionRetainsAuditFields   (T-CTR-025)
//   P5  ExpiredSuppressionTreatedAsAbsent     (T-CTR-029)
//   P6  SuppressionBoundaryDayStillActive     (T-CTR-029, edge case)
//   P7  DiagnosticSuppressionRequiresMatchingRule (T-CTR-024/025)
//   P8  DeprecatedRuleRetainsCatalogRow        (§5.4, illustrative)
//   P9  DeprecatedRuleExcludedFromRequiredGate (§5.4, illustrative)
//
// P8/P9 are specified normatively in §5.4 as documentation/process
// obligations on the specification and mapping tables, not as a Go runtime
// API in pkg/workflow; they are encoded here against a minimal stub
// interface pending a concrete deprecation-registry implementation.
package workflow

import (
	"testing"
	"time"

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

// deprecationRegistry is a stub — replace with real implementation.
// It models §5.4: a deprecated rule's catalog row/status MUST be retained
// (not deleted) and MUST be excluded from the required conformance gate.
type deprecationRegistry struct {
	statuses map[string]string // ruleID -> "Active" | "Deprecated"
}

func (r *deprecationRegistry) Status(ruleID string) (string, bool) {
	s, ok := r.statuses[ruleID]
	return s, ok
}

func (r *deprecationRegistry) IsRequiredForConformance(ruleID string) bool {
	s, ok := r.statuses[ruleID]
	return ok && s != "Deprecated"
}

func newStubRegistry() *deprecationRegistry {
	return &deprecationRegistry{
		statuses: map[string]string{
			"CTR-001": "Active",
			"CTR-999": "Deprecated", // hypothetical retired rule, row retained
		},
	}
}

// mustParseDate is a small test helper for building time.Time values from
// "YYYY-MM-DD" without importing extra packages into the assertions.
func mustParseDate(t *testing.T, s string) time.Time {
	t.Helper()
	tm, err := time.Parse("2006-01-02", s)
	require.NoError(t, err, "test helper date %q must parse as ISO 8601", s)
	return tm
}

// P1: SuppressionRequiresRuleAndReason (T-CTR-024)
// "A suppression without a `reason` MUST NOT be accepted by the compiler;
// the compiler MUST emit a validation error if `reason` is absent or empty."
func TestFormal_SuppressionRequiresRuleAndReason(t *testing.T) {
	t.Parallel()
	cases := []struct {
		name        string
		suppression map[string]any
		wantErr     bool
	}{
		{
			name:        "valid rule and reason accepted",
			suppression: map[string]any{"rule": "CTR-001", "reason": "reviewed and safe in this workflow"},
			wantErr:     false,
		},
		{
			name:        "empty reason rejected",
			suppression: map[string]any{"rule": "CTR-001", "reason": ""},
			wantErr:     true,
		},
		{
			name:        "whitespace-only reason rejected",
			suppression: map[string]any{"rule": "CTR-001", "reason": "   "},
			wantErr:     true,
		},
		{
			name:        "missing reason field rejected",
			suppression: map[string]any{"rule": "CTR-001"},
			wantErr:     true,
		},
	}
	for _, tc := range cases {
		tc := tc
		t.Run(tc.name, func(t *testing.T) {
			t.Parallel()
			_, err := parseThreatDetectionSuppressions([]any{tc.suppression})
			if tc.wantErr {
				assert.Error(t, err, "case %q: expected validation error for missing/empty reason", tc.name)
			} else {
				assert.NoError(t, err, "case %q: expected valid suppression to be accepted", tc.name)
			}
		})
	}
}

// P2: SuppressionRuleFormatWellFormed (T-CTR-024)
// Rule identifiers referenced by a suppression MUST match the CTR-\d{3}
// pattern defined for the rule catalog; an unrecognized/malformed rule ID
// MUST be rejected rather than silently accepted.
func TestFormal_SuppressionRuleFormatWellFormed(t *testing.T) {
	t.Parallel()
	cases := []struct {
		name    string
		rule    string
		wantErr bool
	}{
		{name: "well-formed three-digit rule ID", rule: "CTR-015", wantErr: false},
		{name: "malformed rule ID missing digits", rule: "CTR-1", wantErr: true},
		{name: "malformed rule ID wrong prefix", rule: "XTR-015", wantErr: true},
		{name: "empty rule ID rejected", rule: "", wantErr: true},
	}
	for _, tc := range cases {
		tc := tc
		t.Run(tc.name, func(t *testing.T) {
			t.Parallel()
			_, err := parseThreatDetectionSuppressions([]any{
				map[string]any{"rule": tc.rule, "reason": "test reason"},
			})
			if tc.wantErr {
				assert.Error(t, err, "case %q: malformed rule ID %q must be rejected", tc.name, tc.rule)
			} else {
				assert.NoError(t, err, "case %q: well-formed rule ID %q must be accepted", tc.name, tc.rule)
			}
		})
	}
}

// P3: SuppressionExpiresISO8601OrAbsent (T-CTR-024)
// The optional `expires` field MUST be an ISO 8601 date when present, and
// suppressions without it MUST be treated as never-expiring at parse time.
func TestFormal_SuppressionExpiresISO8601OrAbsent(t *testing.T) {
	t.Parallel()
	cases := []struct {
		name    string
		expires string
		wantErr bool
	}{
		{name: "absent expires accepted", expires: "", wantErr: false},
		{name: "valid ISO 8601 date accepted", expires: "2026-12-31", wantErr: false},
		{name: "non-ISO date format rejected", expires: "12/31/2026", wantErr: true},
		{name: "invalid calendar date rejected", expires: "2026-13-40", wantErr: true},
	}
	for _, tc := range cases {
		tc := tc
		t.Run(tc.name, func(t *testing.T) {
			t.Parallel()
			suppression := map[string]any{"rule": "CTR-001", "reason": "test reason"}
			if tc.expires != "" {
				suppression["expires"] = tc.expires
			}
			_, err := parseThreatDetectionSuppressions([]any{suppression})
			if tc.wantErr {
				assert.Error(t, err, "case %q: expires %q must be rejected", tc.name, tc.expires)
			} else {
				assert.NoError(t, err, "case %q: expires %q must be accepted", tc.name, tc.expires)
			}
		})
	}
}

// P4: ActiveSuppressionRetainsAuditFields (T-CTR-025)
// "Every active suppression annotation MUST be recorded ... The lock file
// MUST include the full `rule`, `reason`, and `expires` values."
func TestFormal_ActiveSuppressionRetainsAuditFields(t *testing.T) {
	t.Parallel()
	suppressions, err := parseThreatDetectionSuppressions([]any{
		map[string]any{"rule": "CTR-001", "reason": "false positive in generated fixture", "expires": "2027-01-01"},
	})
	require.NoError(t, err, "well-formed suppression must parse without error")
	require.Len(t, suppressions, 1, "exactly one suppression must be parsed")

	got := suppressions[0]
	assert.Equal(t, "CTR-001", got.Rule, "audit trail must retain the exact rule ID")
	assert.Equal(t, "false positive in generated fixture", got.Reason, "audit trail must retain the exact reason text")
	assert.Equal(t, "2027-01-01", got.Expires, "audit trail must retain the exact expires date")
}

// P5: ExpiredSuppressionTreatedAsAbsent (T-CTR-029)
// "A suppression MUST be re-evaluated and explicitly renewed if the
// `expires` date passes; expired suppressions MUST be treated by the
// compiler as if they do not exist."
func TestFormal_ExpiredSuppressionTreatedAsAbsent(t *testing.T) {
	t.Parallel()
	suppressions, err := parseThreatDetectionSuppressions([]any{
		map[string]any{"rule": "CTR-001", "reason": "temporary suppression", "expires": "2025-01-01"},
	})
	require.NoError(t, err, "suppression with past expires must still parse successfully")

	now := mustParseDate(t, "2026-01-01")
	suppressed := isThreatDetectionRuleSuppressed(suppressions, "CTR-001", now)
	assert.False(t, suppressed, "an expired suppression MUST be treated as absent, not as active")
}

// P6 (edge case): SuppressionBoundaryDayStillActive (T-CTR-029)
// A suppression whose `expires` date equals "today" (in UTC) is still
// within its final active calendar day and MUST remain active; only the
// following day MUST it be treated as expired.
func TestFormal_SuppressionBoundaryDayStillActive(t *testing.T) {
	t.Parallel()
	suppressions, err := parseThreatDetectionSuppressions([]any{
		map[string]any{"rule": "CTR-002", "reason": "boundary day check", "expires": "2026-06-15"},
	})
	require.NoError(t, err, "suppression must parse successfully")

	sameDay := mustParseDate(t, "2026-06-15")
	assert.True(t, isThreatDetectionRuleSuppressed(suppressions, "CTR-002", sameDay),
		"suppression must still be active on its own expires day")

	nextDay := mustParseDate(t, "2026-06-16")
	assert.False(t, isThreatDetectionRuleSuppressed(suppressions, "CTR-002", nextDay),
		"suppression must be inactive the day after its expires date")
}

// P7: DiagnosticSuppressionRequiresMatchingRule (T-CTR-024/025)
// A diagnostic error for rule X MUST only be suppressed by an active
// suppression whose `rule` field matches X; a suppression for a different
// rule MUST NOT suppress an unrelated diagnostic (no accidental cross-rule
// suppression / no silent false-negative from a mismatched rule ID).
func TestFormal_DiagnosticSuppressionRequiresMatchingRule(t *testing.T) {
	t.Parallel()
	suppressions, err := parseThreatDetectionSuppressions([]any{
		map[string]any{"rule": "CTR-003", "reason": "only CTR-003 is suppressed"},
	})
	require.NoError(t, err, "suppression must parse successfully")

	now := time.Now().UTC()
	assert.True(t, isThreatDetectionRuleSuppressed(suppressions, "CTR-003", now),
		"the exact rule referenced by the suppression must be reported as suppressed")
	assert.False(t, isThreatDetectionRuleSuppressed(suppressions, "CTR-004", now),
		"an unrelated rule ID must never be treated as suppressed by another rule's suppression entry")
}

// P8 (stub): DeprecatedRuleRetainsCatalogRow (§5.4)
// "The rule catalog entry MUST be retained (not deleted) with a
// deprecation notice indicating the version in which the rule was retired
// and the reason." Encoded against a stub registry pending a concrete
// deprecation-tracking implementation in pkg/workflow.
func TestFormal_DeprecatedRuleRetainsCatalogRow(t *testing.T) {
	t.Parallel()
	reg := newStubRegistry()

	status, ok := reg.Status("CTR-999")
	require.True(t, ok, "a deprecated rule's catalog row MUST still be present, not deleted")
	assert.Equal(t, "Deprecated", status, "a retired rule MUST be marked Deprecated, not removed from the catalog")

	activeStatus, ok := reg.Status("CTR-001")
	require.True(t, ok, "an active rule's catalog row must be present")
	assert.Equal(t, "Active", activeStatus, "a non-retired rule must remain marked Active")
}

// P9 (stub): DeprecatedRuleExcludedFromRequiredGate (§5.4, §5.3)
// "All test IDs mapped to the deprecated rule ... MUST NOT be required for
// conformance after the deprecation version." Encoded against a stub
// registry pending a concrete deprecation-tracking implementation.
func TestFormal_DeprecatedRuleExcludedFromRequiredGate(t *testing.T) {
	t.Parallel()
	reg := newStubRegistry()

	assert.False(t, reg.IsRequiredForConformance("CTR-999"),
		"a deprecated rule MUST NOT be required for the conformance gate")
	assert.True(t, reg.IsRequiredForConformance("CTR-001"),
		"an active rule MUST remain required for the conformance gate")
}

Usage

1. Copy the test file to pkg/workflow/threat_detection_suppression_lifecycle_formal_test.go.
2. Replace the deprecationRegistry stub (P8/P9) with a real deprecation-tracking implementation once one exists in pkg/workflow (no such registry currently exists; §5.4 is presently a documentation/process obligation on the spec and Section 7.1 mapping table rather than a runtime API).
3. Run: go test ./pkg/workflow/ -run TestFormal_Suppression -run TestFormal_Deprecated (or go test ./pkg/workflow/ -run Formal for the full formal suite).

Context

• Spec processed: specs/compiler-threat-detection-compliance/README.md (cross-referencing specs/compiler-threat-detection-spec.md §5.4, §6.4)
• Formal notation: Z3-style guard conjunction / TLA+-style state machine (illustrative only)
• Run: https://github.com/github/gh-aw/actions/runs/32648830428

Generated by 🔬 Daily Formal Spec Verifier · auto · 86.5 AIC · ⌖ 16.1 AIC · ⊞ 10.3K · ◷

• expires on Aug 30, 2026, 7:41 AM UTC-08:00