(go/redacted):build !integration
package cli
// Formal compliance tests for the safe output outcome evaluation engine.
//
// These tests cover predicates P1–P12 derived from the formal model in
// specs/safe-output-outcome-evaluation.md.
//
// Formal notation cross-references:
// - TLA+ state-machine invariants: P1, P4, P5, P6, P9
// - Z3/SMT-LIB arithmetic predicates: P10
// - F* pre/post contracts: P2, P3, P7, P8, P11, P12
import (
"errors"
"testing"
"github.com/github/gh-aw/pkg/github"
"github.com/stretchr/testify/assert"
"github.com/stretchr/testify/require"
)
// TestFormalOutcomeDomainInvariant (P1 — TLA+: OutcomeDomain)
// Verifies every OutcomeResult constant is in the spec domain or a recognized internal state,
// and that ComputeOutcomeSummary counts each category correctly.
func TestFormalOutcomeDomainInvariant(t *testing.T) {
specDomain := map[string]bool{
"accepted": true, "rejected": true, "ignored": true,
"pending": true, "lifecycle": true, "lifecycle_close": true,
}
internalOnly := map[string]bool{"unknown": true, "error": true}
allResults := []OutcomeResult{
OutcomeAccepted, OutcomeRejected, OutcomeIgnored, OutcomePending,
OutcomeLifecycle, OutcomeLifecycleClose, OutcomeUnknown, OutcomeError,
}
for _, r := range allResults {
s := string(r)
assert.True(t, specDomain[s] || internalOnly[s],
"P1: OutcomeResult %q must be in spec domain or recognized internal state", s)
}
reports := []OutcomeReport{
{Type: "create_pull_request", Result: OutcomeAccepted},
{Type: "create_issue", Result: OutcomeRejected},
{Type: "add_comment", Result: OutcomeIgnored},
{Type: "add_labels", Result: OutcomePending},
{Type: "close_issue", Result: OutcomeLifecycle},
}
summary := ComputeOutcomeSummary(reports, github.DefaultObjectiveMapping())
assert.Equal(t, 5, summary.Total, "P1: total must equal five non-internal outcomes")
assert.Equal(t, 1, summary.Accepted, "P1: one accepted")
assert.Equal(t, 1, summary.Rejected, "P1: one rejected")
assert.Equal(t, 1, summary.Ignored, "P1: one ignored")
assert.Equal(t, 1, summary.Pending, "P1: one pending")
assert.Equal(t, 1, summary.Lifecycle, "P1: one lifecycle")
}
// TestFormalAPIFailurePending (P2 — F*: evaluateWithAPIError)
// 5xx and rate-limit API errors must never yield accepted or rejected.
func TestFormalAPIFailurePending(t *testing.T) {
old := closeStickyGHAPIGet
t.Cleanup(func() { closeStickyGHAPIGet = old })
apiErrors := []struct{ name, errText string }{
{"503 server error", "gh api: 503 Service Unavailable"},
{"429 rate limit", "gh api: 429 Too Many Requests"},
{"502 bad gateway", "gh api: 502 Bad Gateway"},
{"500 internal error", "gh api: 500 Internal Server Error"},
}
for _, tc := range apiErrors {
t.Run(tc.name, func(t *testing.T) {
closeStickyGHAPIGet = func(endpoint, repo string) (map[string]any, error) {
return nil, errors.New(tc.errText)
}
item := CreatedItemReport{Type: "close_issue", Number: 99, Repo: "owner/repo"}
report := evalCloseSticky(item, "owner/repo")
assert.NotEqual(t, OutcomeAccepted, report.Result,
"P2: API error %q must not yield accepted", tc.errText)
assert.NotEqual(t, OutcomeRejected, report.Result,
"P2: API error %q must not yield rejected", tc.errText)
})
}
}
// TestFormal404Classification (P3 — TLA+: NotFoundClassification)
// 404 on persistent objects → rejected; transient targets → ignored; never accepted.
func TestFormal404Classification(t *testing.T) {
t.Run("persistent object deleted → rejected", func(t *testing.T) {
report := OutcomeReport{Type: "create_issue", Result: OutcomeRejected, Detail: "deleted"}
eval := normalizeOutcomeEvaluation(report)
assert.Equal(t, OutcomeStatusRejected, eval.OutcomeStatus,
"P3: 404 on persistent object (deleted) must yield rejected")
assert.Equal(t, "deleted", eval.Signal,
"P3: deleted signal must be set for persistent 404")
})
t.Run("transient target no engagement → ignored", func(t *testing.T) {
report := OutcomeReport{Type: "add_comment", Result: OutcomeIgnored, Detail: "no engagement"}
eval := normalizeOutcomeEvaluation(report)
assert.Equal(t, OutcomeStatusIgnored, eval.OutcomeStatus,
"P3: transient target with no engagement must yield ignored")
})
t.Run("404 API error must not yield accepted", func(t *testing.T) {
old := closeStickyGHAPIGet
t.Cleanup(func() { closeStickyGHAPIGet = old })
closeStickyGHAPIGet = func(endpoint, repo string) (map[string]any, error) {
return nil, errors.New("gh api: 404 Not Found")
}
item := CreatedItemReport{Type: "close_issue", Number: 99, Repo: "owner/repo"}
report := evalCloseSticky(item, "owner/repo")
assert.NotEqual(t, OutcomeAccepted, report.Result,
"P3: 404 API error must not yield accepted")
})
}
// TestFormalBotActorProvenance (P4 — TLA+: BotActorProvenance)
// [bot]-suffix and known bot logins → bot; human logins → non-bot.
func TestFormalBotActorProvenance(t *testing.T) {
botLogins := []string{
"github-actions[bot]", "dependabot[bot]",
"copilot-swe-agent", "github-actions", "some-custom-app[bot]",
}
for _, login := range botLogins {
assert.True(t, isBotUser(login),
"P4: login %q must be identified as bot actor", login)
}
humanLogins := []string{"octocat", "alice", "john-smith", "github-actions-user"}
for _, login := range humanLogins {
assert.False(t, isBotUser(login),
"P4: login %q must be identified as non-bot actor", login)
}
}
// TestFormalPRMergeAcceptance (P5 — TLA+: PRMergeAcceptance)
// merged → accepted; closed+!merged → rejected; open → pending.
func TestFormalPRMergeAcceptance(t *testing.T) {
cases := []struct {
name, result, detail string
wantStatus OutcomeStatus
wantSignal string
}{
{"merged PR → accepted", string(OutcomeAccepted), "merged", OutcomeStatusAccepted, "merged"},
{"closed PR without merge → rejected", string(OutcomeRejected), "closed without merge", OutcomeStatusRejected, "closed_without_merge"},
{"open PR → pending", string(OutcomePending), "open", OutcomeStatusPending, "open"},
}
for _, tc := range cases {
t.Run(tc.name, func(t *testing.T) {
report := OutcomeReport{Type: "create_pull_request", Result: OutcomeResult(tc.result), Detail: tc.detail}
eval := normalizeOutcomeEvaluation(report)
assert.Equal(t, tc.wantStatus, eval.OutcomeStatus,
"P5: PR state (%q) must yield OutcomeStatus=%s", tc.detail, tc.wantStatus)
assert.Equal(t, tc.wantSignal, eval.Signal,
"P5: PR state (%q) must set signal %q", tc.detail, tc.wantSignal)
})
}
}
// TestFormalIssueBotCloseLifecycle (P6 — TLA+: IssueBotCloseLifecycle)
// Bot closes not_planned → lifecycle; human → rejected; completed → accepted.
func TestFormalIssueBotCloseLifecycle(t *testing.T) {
cases := []struct {
name, result, detail string
wantStatus OutcomeStatus
wantSignal string
}{
{"bot closed not_planned → lifecycle signal", string(OutcomeLifecycle), "closed by bot (lifecycle)", OutcomeStatusUnknown, "lifecycle"},
{"human closed not_planned → rejected", string(OutcomeRejected), "closed as not planned", OutcomeStatusRejected, "closed_not_planned"},
{"resolved as completed → accepted", string(OutcomeAccepted), "completed", OutcomeStatusAccepted, "completed"},
}
for _, tc := range cases {
t.Run(tc.name, func(t *testing.T) {
report := OutcomeReport{Type: "create_issue", Result: OutcomeResult(tc.result), Detail: tc.detail}
eval := normalizeOutcomeEvaluation(report)
assert.Equal(t, tc.wantStatus, eval.OutcomeStatus,
"P6: %s must yield OutcomeStatus=%s", tc.name, tc.wantStatus)
assert.Equal(t, tc.wantSignal, eval.Signal,
"P6: %s must set signal %q", tc.name, tc.wantSignal)
})
}
}
// TestFormalLabelStickiness (P7 — F*: labelRetentionMonotonicity)
// All labels retained → accepted; any removal → Reverted/Replaced non-empty.
func TestFormalLabelStickiness(t *testing.T) {
cases := []struct {
name string
before, after, current []any
wantRetained bool
}{
{"all added labels retained", []any{"triage"}, []any{"triage", "bug"}, []any{"triage", "bug"}, true},
{"added label removed", []any{"triage"}, []any{"triage", "bug"}, []any{"triage"}, false},
{"all labels removed", []any{"triage"}, []any{"triage", "bug"}, []any{}, false},
}
for _, tc := range cases {
t.Run(tc.name, func(t *testing.T) {
before := map[string]any{"labels": tc.before}
after := map[string]any{"labels": tc.after}
current := map[string]any{"labels": tc.current}
comparison := compareRetainedUpdateState(before, after, current, []string{"labels"})
require.Len(t, comparison.Changed, 1, "P7: label delta must be detected as changed field")
if tc.wantRetained {
assert.Len(t, comparison.Retained, 1, "P7: when all labels retained, Retained must contain labels field")
assert.Empty(t, comparison.Reverted, "P7: when all labels retained, Reverted must be empty")
} else {
assert.Empty(t, comparison.Retained, "P7: when any label removed, Retained must be empty")
assert.True(t, len(comparison.Reverted) > 0 || len(comparison.Replaced) > 0,
"P7: when any label removed, Reverted or Replaced must be non-empty")
}
})
}
}
// TestFormalUpdateSnapshotComparison (P8 — F*: compareUpdateSnapshot)
// current=after → retained; current=before → reverted; diverged → replaced.
func TestFormalUpdateSnapshotComparison(t *testing.T) {
before := map[string]any{"title": "Old title"}
after := map[string]any{"title": "New title"}
t.Run("current = after → all retained", func(t *testing.T) {
current := map[string]any{"title": "New title"}
c := compareRetainedUpdateState(before, after, current, []string{"title"})
require.Len(t, c.Changed, 1, "P8: title change must be detected")
assert.Len(t, c.Retained, len(c.Changed), "P8: current=after must have all Changed in Retained")
assert.Empty(t, c.Reverted, "P8: current=after must have no reverted fields")
assert.Empty(t, c.Replaced, "P8: current=after must have no replaced fields")
})
t.Run("current = before → all reverted", func(t *testing.T) {
current := map[string]any{"title": "Old title"}
c := compareRetainedUpdateState(before, after, current, []string{"title"})
require.Len(t, c.Changed, 1, "P8: title change must be detected")
assert.Len(t, c.Reverted, len(c.Changed), "P8: current=before must have all Changed in Reverted")
assert.Empty(t, c.Retained, "P8: current=before must have no retained fields")
assert.Empty(t, c.Replaced, "P8: current=before must have no replaced fields")
})
t.Run("current diverged → all replaced", func(t *testing.T) {
current := map[string]any{"title": "Diverged title"}
c := compareRetainedUpdateState(before, after, current, []string{"title"})
require.Len(t, c.Changed, 1, "P8: title change must be detected")
assert.NotEmpty(t, c.Replaced, "P8: diverged state must have replaced fields")
assert.Empty(t, c.Retained, "P8: diverged state must have no retained fields")
assert.Empty(t, c.Reverted, "P8: diverged state must have no reverted fields")
})
}
// TestFormalCloseStickyReopenRejection (P9 — TLA+: CloseStickyReopenRejection)
// Still-closed → accepted; reopened → rejected.
func TestFormalCloseStickyReopenRejection(t *testing.T) {
cases := []struct {
name, state string
wantResult OutcomeResult
wantDetail string
}{
{"closed → accepted", "closed", OutcomeAccepted, "still closed"},
{"reopened → rejected", "open", OutcomeRejected, "reopened"},
}
for _, tc := range cases {
t.Run(tc.name, func(t *testing.T) {
old := closeStickyGHAPIGet
t.Cleanup(func() { closeStickyGHAPIGet = old })
closeStickyGHAPIGet = func(endpoint, repo string) (map[string]any, error) {
return map[string]any{"state": tc.state}, nil
}
item := CreatedItemReport{Type: "close_issue", Number: 99, Repo: "owner/repo"}
report := evalCloseSticky(item, "owner/repo")
assert.Equal(t, tc.wantResult, report.Result,
"P9: state=%q must yield %s", tc.state, tc.wantResult)
assert.Equal(t, tc.wantDetail, report.Detail,
"P9: state=%q must set detail %q", tc.state, tc.wantDetail)
})
}
}
// TestFormalDerivedMetricsConsistency (P10 — Z3/SMT-LIB bounds)
// acceptance_rate and waste_rate formulas; division-by-zero safe.
func TestFormalDerivedMetricsConsistency(t *testing.T) {
t.Run("acceptance_rate = accepted / (accepted + rejected)", func(t *testing.T) {
reports := []OutcomeReport{
{Type: "create_pull_request", Result: OutcomeAccepted},
{Type: "create_pull_request", Result: OutcomeAccepted},
{Type: "create_issue", Result: OutcomeRejected},
}
summary := ComputeOutcomeSummary(reports, github.DefaultObjectiveMapping())
assert.InDelta(t, 2.0/3.0, summary.AcceptanceRate, 1e-9,
"P10: acceptance_rate must equal accepted/(accepted+rejected)")
})
t.Run("waste_rate = rejected / total", func(t *testing.T) {
reports := []OutcomeReport{
{Type: "create_pull_request", Result: OutcomeAccepted},
{Type: "create_issue", Result: OutcomeRejected},
{Type: "add_comment", Result: OutcomeIgnored},
{Type: "add_labels", Result: OutcomePending},
}
summary := ComputeOutcomeSummary(reports, github.DefaultObjectiveMapping())
assert.InDelta(t, 0.25, summary.WasteRate, 1e-9,
"P10: waste_rate must equal rejected/total")
})
t.Run("division-by-zero safety: empty report set", func(t *testing.T) {
summary := ComputeOutcomeSummary(nil, github.DefaultObjectiveMapping())
assert.InDelta(t, 0.0, summary.AcceptanceRate, 1e-12,
"P10: acceptance_rate must be 0.0 when total=0")
assert.InDelta(t, 0.0, summary.WasteRate, 1e-12,
"P10: waste_rate must be 0.0 when total=0")
})
t.Run("division-by-zero safety: only pending outcomes", func(t *testing.T) {
reports := []OutcomeReport{
{Type: "add_labels", Result: OutcomePending},
{Type: "add_labels", Result: OutcomePending},
}
summary := ComputeOutcomeSummary(reports, github.DefaultObjectiveMapping())
assert.InDelta(t, 0.0, summary.AcceptanceRate, 1e-12,
"P10: acceptance_rate must be 0.0 when accepted+rejected=0")
})
}
// TestFormalOTelGracefulDegradation (P11 — F*: evaluateOutcome)
// Transport failure still produces valid, non-discardable OutcomeReport with OTel attributes.
func TestFormalOTelGracefulDegradation(t *testing.T) {
old := closeStickyGHAPIGet
t.Cleanup(func() { closeStickyGHAPIGet = old })
closeStickyGHAPIGet = func(endpoint, repo string) (map[string]any, error) {
return nil, errors.New("transport error: connection refused")
}
validResults := map[OutcomeResult]bool{
OutcomeAccepted: true, OutcomeRejected: true, OutcomeIgnored: true,
OutcomePending: true, OutcomeLifecycle: true, OutcomeUnknown: true, OutcomeError: true,
}
items := []CreatedItemReport{
{Type: "close_issue", Number: 1, Repo: "owner/repo"},
{Type: "close_pull_request", Number: 2, Repo: "owner/repo"},
}
for _, item := range items {
t.Run(item.Type, func(t *testing.T) {
report := evalCloseSticky(item, "owner/repo")
assert.NotEmpty(t, report.Type,
"P11: report.Type must be set regardless of transport availability")
assert.True(t, validResults[report.Result],
"P11: result %q must be a recognized OutcomeResult when transport fails", report.Result)
eval := normalizeOutcomeEvaluation(report)
assert.NotEmpty(t, string(eval.OutcomeStatus),
"P11: OutcomeStatus must be non-empty so audit log entry can be written")
assert.NotEmpty(t, string(eval.EvidenceStrength),
"P11: EvidenceStrength must be non-empty so audit log entry can be written")
})
}
}
// TestFormalConformanceClassCoverage (P12 — F*: conformanceClassCoverage)
// Class A (state transitions), Class B (lifecycle/human), Class C (API degradation).
func TestFormalConformanceClassCoverage(t *testing.T) {
t.Run("Class A: close_issue accepted state transition", func(t *testing.T) {
old := closeStickyGHAPIGet
t.Cleanup(func() { closeStickyGHAPIGet = old })
closeStickyGHAPIGet = func(endpoint, repo string) (map[string]any, error) {
return map[string]any{"state": "closed"}, nil
}
report := evalCloseSticky(CreatedItemReport{Type: "close_issue", Number: 1, Repo: "o/r"}, "o/r")
assert.Equal(t, OutcomeAccepted, report.Result,
"P12 Class A: still-closed issue must be accepted")
})
t.Run("Class A: close_issue rejected state transition", func(t *testing.T) {
old := closeStickyGHAPIGet
t.Cleanup(func() { closeStickyGHAPIGet = old })
closeStickyGHAPIGet = func(endpoint, repo string) (map[string]any, error) {
return map[string]any{"state": "open"}, nil
}
report := evalCloseSticky(CreatedItemReport{Type: "close_issue", Number: 1, Repo: "o/r"}, "o/r")
assert.Equal(t, OutcomeRejected, report.Result,
"P12 Class A: reopened issue must be rejected")
})
t.Run("Class B: lifecycle bot-close carries lifecycle signal", func(t *testing.T) {
report := OutcomeReport{Type: "close_issue", Result: OutcomeLifecycle, Detail: "closed by bot (lifecycle)"}
eval := normalizeOutcomeEvaluation(report)
assert.Equal(t, "lifecycle", eval.Signal,
"P12 Class B: bot-closed outcome must carry the lifecycle signal")
})
t.Run("Class C: API 5xx for close_issue", func(t *testing.T) {
old := closeStickyGHAPIGet
t.Cleanup(func() { closeStickyGHAPIGet = old })
closeStickyGHAPIGet = func(endpoint, repo string) (map[string]any, error) {
return nil, errors.New("gh api: 500 Internal Server Error")
}
report := evalCloseSticky(CreatedItemReport{Type: "close_issue", Number: 1, Repo: "o/r"}, "o/r")
assert.NotEqual(t, OutcomeAccepted, report.Result,
"P12 Class C: 5xx error must not yield accepted")
assert.NotEqual(t, OutcomeRejected, report.Result,
"P12 Class C: 5xx error must not yield rejected")
})
t.Run("Class C: rate limit for update_issue", func(t *testing.T) {
old := outcomeUpdateGHAPIGet
t.Cleanup(func() { outcomeUpdateGHAPIGet = old })
outcomeUpdateGHAPIGet = func(endpoint, repo string) (map[string]any, error) {
return nil, errors.New("gh api: 429 Too Many Requests")
}
item := CreatedItemReport{
Type: "update_issue", Number: 1, Repo: "o/r",
BeforeState: map[string]any{"title": "Old"},
AfterState: map[string]any{"title": "New"},
}
report := evalUpdateIssue(item, "o/r")
assert.NotEqual(t, OutcomeAccepted, report.Result,
"P12 Class C: rate limit must not yield accepted")
assert.NotEqual(t, OutcomeRejected, report.Result,
"P12 Class C: rate limit must not yield rejected")
})
}
Summary
The
safe-output-outcome-evaluation.mdspecification defines the exact evaluation logic for every safe output type in the gh-aw system — what observable GitHub state constitutes acceptance, rejection, ignoring, or pending status for each action. It establishes outcome categories, OTel attribute contracts, API failure safeguards (5xx/404/rate-limit), bot-actor provenance rules, a complete conformance test table, and derived metrics (acceptance_rate, waste_rate, zero_touch_rate). This formalization session analyzed the spec through TLA+ state-machine invariants, F* pre/post contracts, and Z3/SMT-LIB arithmetic bounds, and produced (and verified against the existing) a 12-predicate Go testify suite atpkg/cli/outcome_eval_formal_test.go.Specification
specs/safe-output-outcome-evaluation.mdFormal Model
Predicates and invariants (illustrative notation)
TLA+ — State Machine Invariants
F — Pre/Post Contracts*
Z3/SMT-LIB — Derived Metrics Arithmetic Safety
Behavioral Coverage Map
P1OutcomeDomainTestFormalOutcomeDomainInvariantP2APIFailureNeverTerminalTestFormalAPIFailurePendingpending/error, neveraccepted/rejectedP3NotFoundClassificationTestFormal404Classificationrejected; on transient target →ignored; neveracceptedP4BotActorProvenanceTestFormalBotActorProvenance[bot]-suffix and known bot logins → bot; human logins → non-botP5PRMergeAcceptanceTestFormalPRMergeAcceptancemerged=true→ accepted;closed+!merged→ rejected;open→ pendingP6IssueBotCloseLifecycleTestFormalIssueBotCloseLifecyclenot_planned→ lifecycle; human → rejected;completed→ acceptedP7LabelRetentionMonotonicityTestFormalLabelStickinessP8UpdateSnapshotComparisonTestFormalUpdateSnapshotComparisoncurrent=after→ retained;current=before→ reverted; diverged → replacedP9CloseStickyReopenRejectionTestFormalCloseStickyReopenRejectionP10DerivedMetricsConsistencyTestFormalDerivedMetricsConsistencyacceptance_rateandwaste_rateformulas correct; division-by-zero safe for empty setsP11OTelGracefulDegradationTestFormalOTelGracefulDegradationP12ConformanceClassCoverageTestFormalConformanceClassCoverageGenerated Test Suite
📄 `pkg/cli/outcome_eval_formal_test.go`
Usage
pkg/cli/outcome_eval_formal_test.go.go test ./pkg/cli/ -run TestFormalAPIFailurePending -vContext
specs/safe-output-outcome-evaluation.mdpkg/cli/outcome_eval_formal_test.go(705 lines, 12 test functions)