feat(spec): formal model & test suite for safe-output-outcome-evaluation (P1–P12)#45781
Conversation
…ion spec (P1–P12) - Append Formal Model section (TLA+/F*/Z3 invariants for 12 predicates) to specs/safe-output-outcome-evaluation.md - Append Behavioral Coverage Map and Generated Test Suite sections - Add closeStickyGHAPIGet var to outcome_eval_generic.go for test isolation - Add pkg/cli/outcome_eval_formal_test.go with 12 formal test functions (TestFormalOutcomeDomainInvariant, TestFormalAPIFailurePending, TestFormal404Classification, TestFormalBotActorProvenance, TestFormalPRMergeAcceptance, TestFormalIssueBotCloseLifecycle, TestFormalLabelStickiness, TestFormalUpdateSnapshotComparison, TestFormalCloseStickyReopenRejection, TestFormalDerivedMetricsConsistency, TestFormalOTelGracefulDegradation, TestFormalConformanceClassCoverage) Closes #45780 Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
…t and lifecycle TODO - Add OutcomeLifecycleClose OutcomeResult constant to outcome_eval.go (spec defines lifecycle_close as one of the six observable outcomes) - Include OutcomeLifecycleClose in P1 formal test domain verification - Add TODO comment to P6 test referencing future OutcomeStatusLifecycle constant Co-authored-by: pelikhan <4175913+pelikhan@users.noreply.github.com>
|
🧠 Matt Pocock Skills Reviewer has completed the skills-based review. ✅ |
|
✅ Test Quality Sentinel completed test quality analysis. |
|
✅ Design Decision Gate 🏗️ completed the design decision gate check. |
|
✅ PR Code Quality Reviewer completed the code quality review. |
There was a problem hiding this comment.
Pull request overview
Adds formal specifications and conformance tests for safe-output outcome evaluation.
Changes:
- Documents TLA+, F*, and SMT-based predicates P1–P12.
- Adds the
lifecycle_closeoutcome constant and a mockable API seam. - Introduces predicate-focused Go tests.
Show a summary per file
| File | Description |
|---|---|
specs/safe-output-outcome-evaluation.md |
Adds formal models and coverage mapping. |
pkg/cli/outcome_eval.go |
Adds OutcomeLifecycleClose. |
pkg/cli/outcome_eval_generic.go |
Makes close-state API calls mockable. |
pkg/cli/outcome_eval_formal_test.go |
Adds P1–P12 conformance tests. |
Review details
Tip
Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
- Files reviewed: 4/4 changed files
- Comments generated: 13
- Review effort level: Medium
| OutcomePending OutcomeResult = "pending" | ||
| OutcomeUnknown OutcomeResult = "unknown" | ||
| OutcomeLifecycle OutcomeResult = "lifecycle" | ||
| OutcomeLifecycleClose OutcomeResult = "lifecycle_close" |
| // Internal states that are valid at the evaluator level but must be | ||
| // normalized to a spec-defined category before external emission. | ||
| internalOnly := map[string]bool{ | ||
| "unknown": true, | ||
| "error": true, |
| report := evalCloseSticky(item, "owner/repo") | ||
| assert.NotEqual(t, OutcomeAccepted, report.Result, | ||
| "P3: 404 API error must not yield accepted") |
| report := OutcomeReport{ | ||
| Type: "create_pull_request", | ||
| Result: tc.result, | ||
| Detail: tc.detail, | ||
| } |
| report := OutcomeReport{ | ||
| Type: "create_issue", | ||
| Result: tc.result, | ||
| Detail: tc.detail, | ||
| } |
| // ok = classAExists(evaluator) ∧ classCExists(evaluator)) | ||
| // | ||
| // Specification reference: specs/safe-output-outcome-evaluation.md §Conformance →§Conformance Safeguard Coverage Requirements | ||
| func TestFormalConformanceClassCoverage(t *testing.T) { |
| (declare-const accepted Int) | ||
| (declare-const rejected Int) | ||
| (declare-const total Int) | ||
| (assert (>= accepted 0)) | ||
| (assert (>= rejected 0)) | ||
| (assert (>= total (+ accepted rejected))) | ||
| (assert (=> (> (+ accepted rejected) 0) | ||
| (= acceptance_rate (/ accepted (+ accepted rejected))))) | ||
| (assert (=> (> total 0) | ||
| (= waste_rate (/ rejected total)))) | ||
| (assert (=> (= (+ accepted rejected) 0) (= acceptance_rate 0.0))) | ||
| (assert (=> (= total 0) (= waste_rate 0.0))) |
| current.state = "closed" ⟹ result = "accepted" ∧ | ||
| current.state = "open" ⟹ result = "rejected" |
|
|
||
| ## Formal Model | ||
|
|
||
| The outcome evaluation engine is encoded as a state machine with invariants using TLA+, F* pre/post contracts, and Z3/SMT-LIB arithmetic bounds. |
| | Notation | Predicates | Purpose | | ||
| |---|---|---| | ||
| | TLA+ state-machine invariants | P1, P4, P5, P6, P9 | State transition correctness | | ||
| | F* pre/post contracts | P2, P3, P7, P8, P11, P12 | Function-level contracts | |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
Skills-Based Review 🧠
Applied /tdd and /grill-with-docs — requesting changes on three test completeness gaps.
📋 Key Themes & Highlights
Issues Found
- P6 TODO without tracking reference (line ~322) — the
OutcomeStatusLifecycleworkaround assertion will silently pass forever without a linked issue ort.Skip. - P9 lifecycle_close path untested (line ~408) — the coverage map claims this path is covered; the test omits it entirely.
- P11 single-evaluator scope (line ~612) — the F* postcondition describes all evaluators but only
evalCloseStickyis exercised;evalUpdateIssueand others are unguarded. - P12 Class B incomplete (line ~665) — human-override scenarios are absent from the conformance class coverage test.
Positive Highlights
- ✅ Excellent use of the established
*GHAPIGetinjection pattern forcloseStickyGHAPIGet - ✅ Formal notation cross-references (TLA+/F*/Z3) are well-structured and map cleanly to test functions
- ✅ Division-by-zero guards for derived metrics are thoroughly tested (P10)
- ✅
OutcomeLifecycleCloseconstant correctly completes the six-value spec domain - ✅ The behavioral coverage map is a great navigation aid — consider keeping it co-located with the spec long-term
🧠 Reviewed using Matt Pocock's skills by Matt Pocock Skills Reviewer · 42.9 AIC · ⌖ 4.88 AIC · ⊞ 6.7K
Comment /matt to run again
| t.Run(tc.name, func(t *testing.T) { | ||
| report := OutcomeReport{ | ||
| Type: "create_issue", | ||
| Result: tc.result, |
There was a problem hiding this comment.
[/tdd] The TODO for OutcomeStatusLifecycle means P6 is asserting a workaround (OutcomeStatusUnknown) rather than the intended spec behaviour — this gap should be tracked as an issue, not left as an in-code comment.
💡 Suggestion
Either open a follow-up issue for introducing OutcomeStatusLifecycle and link it here, or skip this sub-case with t.Skip plus an issue URL so the CI gap is explicit:
// TODO(#XXXX): OutcomeStatusLifecycle constant not yet defined; skip until implemented.
t.Skip("OutcomeStatusLifecycle not yet available — tracked in #XXXX")Leaving a TODO without a tracking reference makes it invisible to the team and risks the workaround assertion becoming permanent.
@copilot please address this.
| // the three mandatory conformance safeguard classes defined in the spec: | ||
| // | ||
| // - Class A: standard accepted/rejected/ignored/pending state transitions | ||
| // - Class B: human override and lifecycle outcome paths |
There was a problem hiding this comment.
[/tdd] P11 (TestFormalOTelGracefulDegradation) only exercises evalCloseSticky, but the F* postcondition claims it covers all evaluators. Evaluators like evalUpdateIssue could silently discard outcomes on transport failure without being caught by this test.
💡 Suggestion
Add at least one evalUpdateIssue transport-failure case to verify the postcondition holds across evaluators:
oldUpdate := outcomeUpdateGHAPIGet
t.Cleanup(func() { outcomeUpdateGHAPIGet = oldUpdate })
outcomeUpdateGHAPIGet = func(endpoint, repo string) (map[string]any, error) {
return nil, errors.New("transport error: connection refused")
}
item := CreatedItemReport{
Type: "update_issue", Number: 3, Repo: "owner/repo",
BeforeState: map[string]any{"title": "Old"},
AfterState: map[string]any{"title": "New"},
}
report := evalUpdateIssue(item, "owner/repo")
assert.True(t, validResults[report.Result], "P11: evalUpdateIssue must emit valid result on transport failure")@copilot please address this.
| // | ||
| // Formal predicate (F*): | ||
| // | ||
| // val compareUpdateSnapshot : |
There was a problem hiding this comment.
[/tdd] P9's behavioral coverage map entry says "lifecycle bot closed → lifecycle_close", but TestFormalCloseStickyReopenRejection only tests accepted and rejected transitions — the lifecycle_close path is completely uncovered.
💡 Suggestion
Add a third case for the lifecycle_close path. Based on the spec and the new OutcomeLifecycleClose constant, this would be when evalCloseSticky detects a bot-closed-not-planned scenario:
{"lifecycle_close → lifecycle_close outcome", "closed", OutcomeLifecycleClose, "lifecycle_close"},If the evalCloseSticky path that emits OutcomeLifecycleClose is not yet implemented, add a t.Skip with a tracking issue reference rather than omitting the test entirely.
@copilot please address this.
| }) | ||
|
|
||
| t.Run("Class B: lifecycle bot-close carries lifecycle signal", func(t *testing.T) { | ||
| report := OutcomeReport{ |
There was a problem hiding this comment.
[/tdd] P12 Class B is represented by a single test (bot-lifecycle signal), but the spec defines Class B as covering human override and lifecycle outcome paths. No human-override scenario (e.g. a human reopening a bot-closed issue) is tested, leaving this conformance class structurally incomplete.
💡 Suggestion
Add a human-override case for Class B, for example:
t.Run("Class B: human override reopens bot-closed issue → rejected", func(t *testing.T) {
report := OutcomeReport{
Type: "close_issue",
Result: OutcomeRejected,
Detail: "closed as not planned",
}
eval := normalizeOutcomeEvaluation(report)
assert.Equal(t, OutcomeStatusRejected, eval.OutcomeStatus,
"P12 Class B: human-overridden close must yield rejected")
})@copilot please address this.
🧪 Test Quality Sentinel Report✅ Test Quality Score: 87/100 — Excellent
📊 Metrics (12 tests)
|
🏗️ Design Decision Gate — ADR RequiredThis PR makes significant changes to core business logic (715 new lines in 📄 Draft ADR committed:
📋 What to do next
Once an ADR is linked in the PR body, this gate will re-run and verify the implementation matches the decision. ❓ Why ADRs MatterADRs create a searchable, permanent record of why the codebase looks the way it does. Future contributors (and your future self) will thank you. 📋 Michael Nygard ADR Format ReferenceAn ADR must contain these four sections to be considered complete:
All ADRs are stored in
|
There was a problem hiding this comment.
Review: feat(spec): formal model & test suite for safe-output-outcome-evaluation (P1–P12)
Good overall structure — the spec additions, formal model notation, and 12-test suite are well-organized. However, there is a single root correctness issue with two cascading consequences that need to be resolved before merge.
Blocking issue: OutcomeLifecycleClose is a dead constant
Root cause (pkg/cli/outcome_eval_generic.go): evalCloseSticky has no bot-actor provenance check and never returns OutcomeLifecycleClose. The spec (§8, §9) explicitly requires this outcome when a lifecycle/noop bot is the close actor.
Consequence 1 (pkg/cli/outcome_eval.go line 192): ComputeOutcomeSummary doesn't count OutcomeLifecycleClose — the switch only handles OutcomeLifecycle. Any future code path that emits lifecycle_close will be silently dropped from the summary totals.
Consequence 2 (pkg/cli/outcome_eval_formal_test.go — TestFormalCloseStickyReopenRejection): The behavioral coverage map claims P9 covers "lifecycle bot closed→lifecycle_close", but the test has no such case. The spec table and test are inconsistent with each other and with the production code.
Non-blocking observation
normalizeOutcomeEvaluation in outcome_evaluation.go also has no case for OutcomeLifecycleClose in its result-fallback switch (lines 95–105). This won't cause failures today since the constant is never emitted, but should be handled when the production path is added.
Suggested resolution: Either (a) implement the bot-actor check in evalCloseSticky, add the OutcomeLifecycleClose counter in ComputeOutcomeSummary, and add the corresponding P9 test case, or (b) defer lifecycle_close emission to a follow-up, remove it from the P9 coverage map description, and add a TODO comment on the declared constant.
🧵 Reviewed using Impeccable skills by Impeccable Skills Reviewer · 74 AIC · ⌖ 5.64 AIC · ⊞ 5K
Comments that could not be inline-anchored
pkg/cli/outcome_eval.go:192
OutcomeLifecycleClose is silently dropped from the Lifecycle counter.
The new OutcomeLifecycleClose = "lifecycle_close" constant is added in this PR, but the aggregation switch in ComputeOutcomeSummary only handles OutcomeLifecycle:
switch r.Result {
case OutcomeLifecycle:
s.Lifecycle++
case OutcomeError:
s.Errors++
}Any report with Result = OutcomeLifecycleClose falls through without being counted, causing summary.Lifecycle to under-count spec-defined `l…
pkg/cli/outcome_eval_generic.go:38
evalCloseSticky never emits OutcomeLifecycleClose, making the new constant a dead value.
The spec (§8 close_issue, §9 close_pull_request, and the behavioral coverage map P9) states:
> Issue still closed and close actor is github-actions[bot] or configured lifecycle bot → lifecycle_close
But evalCloseSticky only checks state == "closed" (→ accepted) vs. anything else (→ rejected). There is no actor/bot-provenance check, so OutcomeLifecycleClose can never be returned by this …
pkg/cli/outcome_eval_formal_test.go:462
P9 behavioral coverage map claim does not match the test body.
The behavioral coverage map (specs/safe-output-outcome-evaluation.md) says:
> P9 CloseSticky-Reopen-Rejection — Reopened object→rejected; lifecycle bot closed→lifecycle_close
But TestFormalCloseStickyReopenRejection only exercises two cases: "closed" → accepted and "open" → rejected. There is no test case that verifies the bot-close → lifecycle_close path. Because evalCloseSticky also never emits `OutcomeLifec…
There was a problem hiding this comment.
Two issues to fix before merge
One correctness bug in the test suite itself (will cause false failures), one coverage gap that lets a real bug hide from the formal predicate it is supposed to prove.
Details
High — P11 validResults omits OutcomeLifecycleClose (line 611–613 of the new test file)
The P1 domain invariant explicitly adds OutcomeLifecycleClose to the known-outcome set, but P11 does not include it in validResults. Any code path that returns the new constant will make P11 assert failure — the opposite of graceful degradation. Fix: add OutcomeLifecycleClose: true to the map.
Medium — P2 only covers closeStickyGHAPIGet; outcomeUpdateGHAPIGet is untested
The formal predicate claims that all API 5xx/429 errors never produce terminal outcomes, but only the evalCloseSticky path is exercised. evalUpdateIssue could silently return OutcomeAccepted on a 5xx and P2 would not catch it.
🔎 Code quality review by PR Code Quality Reviewer · 51.7 AIC · ⌖ 4.68 AIC · ⊞ 5.6K
Comment /review to run again
| // | ||
| // - Class A: standard accepted/rejected/ignored/pending state transitions | ||
| // - Class B: human override and lifecycle outcome paths | ||
| // - Class C: API degradation (5xx, 404, rate-limit) |
There was a problem hiding this comment.
OutcomeLifecycleClose missing from P11 valid-results set — assertion will spuriously fail for the new constant.
The validResults map (lines 611–613) enumerates all recognized OutcomeResult values but omits the newly-added OutcomeLifecycleClose. If evalCloseSticky (or any future eval path) returns OutcomeLifecycleClose, the P11 assertion will fire a false failure — directly contradicting the invariant it's meant to prove.
💡 Suggested fix
Add OutcomeLifecycleClose to the map:
validResults := map[OutcomeResult]bool{
OutcomeAccepted: true, OutcomeRejected: true, OutcomeIgnored: true,
OutcomePending: true, OutcomeLifecycle: true, OutcomeLifecycleClose: true,
OutcomeUnknown: true, OutcomeError: true,
}This matches the allResults slice in P1 (line 86–89), which already includes OutcomeLifecycleClose.
|
|
||
| // Transient target: "no engagement" maps to ignored (transient 404 classification). | ||
| t.Run("transient target no engagement → ignored", func(t *testing.T) { | ||
| report := OutcomeReport{ |
There was a problem hiding this comment.
P2 predicate scope is narrower than its title implies — outcomeUpdateGHAPIGet path is not covered.
TestFormalAPIFailurePending only injects failures through closeStickyGHAPIGet. The formal predicate states the property for all API failures (5xx, 429), but evalUpdateIssue goes through outcomeUpdateGHAPIGet. If that path has a bug where a 5xx yields OutcomeAccepted, P2 won't catch it.
💡 Suggested fix
Add a second sub-table or sub-test that injects API errors into outcomeUpdateGHAPIGet and calls evalUpdateIssue, then asserts the same non-terminal constraints:
t.Run("update_issue "+tc.name, func(t *testing.T) {
old := outcomeUpdateGHAPIGet
t.Cleanup(func() { outcomeUpdateGHAPIGet = old })
outcomeUpdateGHAPIGet = func(endpoint, repo string) (map[string]any, error) {
return nil, errors.New(tc.errText)
}
item := CreatedItemReport{
Type: "update_issue", Number: 1, Repo: "owner/repo",
BeforeState: map[string]any{"title": "Old"},
AfterState: map[string]any{"title": "New"},
}
report := evalUpdateIssue(item, "owner/repo")
assert.NotEqual(t, OutcomeAccepted, report.Result)
assert.NotEqual(t, OutcomeRejected, report.Result)
})
|
|
|
@copilot merge pr-finisher skill |
Ran the
Hand-off: CI must be re-triggered by a maintainer (close/reopen PR, Still needed: Human CI re-trigger and final merge approval. |
|
🎉 This pull request is included in a new release. Release: |
Implements the formal model section and executable conformance test suite for
specs/safe-output-outcome-evaluation.md, covering all 12 predicates from the behavioral coverage map.Spec additions (
specs/safe-output-outcome-evaluation.md)Three sections appended:
Production changes
outcome_eval.go— addsOutcomeLifecycleClose OutcomeResult = "lifecycle_close"(the sixth spec-defined observable outcome was missing as a typed constant)outcome_eval_generic.go— extractscloseStickyGHAPIGet = ghAPIGetsoevalCloseStickyis mockable in unit tests, consistent with the existinggenericOutcomeGHAPIGet/outcomeUpdateGHAPIGetpatternTest file (
pkg/cli/outcome_eval_formal_test.go)12
//go:build !integrationtests, one per predicate:TestFormalOutcomeDomainInvariantOutcomeResultconstants in spec domainTestFormalAPIFailurePendingcloseStickyGHAPIGetmockTestFormal404ClassificationnormalizeOutcomeEvaluationdetail routingTestFormalBotActorProvenanceisBotUsertable-drivenTestFormalPRMergeAcceptancenormalizeOutcomeEvaluationfor merged/closed/openTestFormalIssueBotCloseLifecycleTestFormalLabelStickinesscompareRetainedUpdateStatelabel monotonicityTestFormalUpdateSnapshotComparisoncompareRetainedUpdateStatepure-function (after/before/diverged)TestFormalCloseStickyReopenRejectionevalCloseStickyvia mockTestFormalDerivedMetricsConsistencyComputeOutcomeSummaryformulas + zero-division guardsTestFormalOTelGracefulDegradationTestFormalConformanceClassCoverage