[formal-spec] compiler-threat-detection-changelog.md — Formal model & test suite — 2026-09-13

### Summary

`specs/compiler-threat-detection-changelog.md` records dated mapping audits for the compiler threat detection specification. This run formalizes the CTR-027 "Allowlisted Bot Synchronization Provenance" control, whose authorization logic is described in the changelog's 2026-09-11 mapping audit paragraph (and cross-referenced in `specs/compiler-threat-detection-spec.md` §5.1). The control gates bot-driven pull-request `synchronize` events behind a conjunction of provenance checks so that a bot's presence on an allowlist alone can never authorize a confused-deputy-style trigger.

### Specification

- **File**: `specs/compiler-threat-detection-changelog.md`
- **Focus area**: CTR-027 Allowlisted Bot Synchronization Provenance (2026-09-11 mapping audit paragraph)
- **Formal notation used**: TLA+-style state predicates / Z3-style guard conjunction

### Formal Model

Predicates and invariants (illustrative notation)

```
--------------------------- MODULE CTR027Provenance ---------------------------
(* Source: specs/compiler-threat-detection-changelog.md, Mapping Audit (2026-09-11):
"Authorization is permitted only for pull_request or pull_request_target
synchronize events when repository IDs match (or the head repository name
matches the base repository if IDs are unavailable), the original PR author
satisfies on.roles, the bot is installed and active, and the actor is not
dependabot[bot]. Missing provenance, fork PRs, untrusted authors, inactive
bots, and Dependabot author mismatches fail closed." *)

CONSTANTS Repos, Bots, Roles, Actors
VARIABLES event, action, headRepo, baseRepo, authorRole, botAllowlisted,
botInstalled, botActive, actor

\* P1 EventGuard
EventGuard == action = "synchronize"
/\ event \in {"pull_request", "pull_request_target"}

\* P2 RepoProvenanceMatch — Z3-style guard conjunction with ID-then-name fallback
RepoProvenanceMatch ==
IF headRepo.id # NULL /\ baseRepo.id # NULL
THEN headRepo.id = baseRepo.id
ELSE headRepo.name # NULL /\ baseRepo.name # NULL /\ headRepo.name = baseRepo.name

\* P3 AuthorRoleSatisfied
AuthorRoleSatisfied == authorRole \in ConfiguredRoles

\* P4 BotInstalledActive
BotInstalledActive == botInstalled = TRUE /\ botActive = TRUE

\* P5 ActorNotDependabot — unconditional safety net
ActorNotDependabot == actor # "dependabot[bot]"

\* P6 FailClosedOnMissingData — safety property (temporal "always")
FailClosedOnMissingData ==
[](\/ headRepo.id = NULL /\ headRepo.name = NULL
\/ baseRepo.id = NULL /\ baseRepo.name = NULL
\/ actor = NULL
=> ~Authorized)

\* P7 AllowlistNotOverride — allowlist is necessary, never sufficient
AllowlistNotOverride ==
botAllowlisted = TRUE /\ ~(EventGuard /\ RepoProvenanceMatch /\ AuthorRoleSatisfied
/\ BotInstalledActive /\ ActorNotDependabot)
=> ~Authorized

\* P8 AuditNoSecretLeak — logged fields exclude credentials/payload bodies
AuditNoSecretLeak ==
\A f \in LoggedFields : f \notin {"token", "credential", "payload_body"}

\* Top-level authorization predicate (conjunction of P1-P5)
Authorized == EventGuard /\ RepoProvenanceMatch /\ AuthorRoleSatisfied
/\ BotInstalledActive /\ ActorNotDependabot /\ botAllowlisted = TRUE
================================================================================
```

### Behavioral Coverage Map

| Predicate / Invariant | Test Function | Description |
|---|---|---|
| `P1 EventGuard` | `TestFormal_P1_EventGuard` | Only `pull_request`/`pull_request_target` `synchronize` events are in scope; other events/actions are denied. |
| `P2 RepoProvenanceMatch` | `TestFormal_P2_RepoProvenanceMatch` | Head/base repo IDs must match, falling back to name comparison only when both IDs are unavailable; partial-ID cases fail closed. |
| `P3 AuthorRoleSatisfied` | `TestFormal_P3_AuthorRoleSatisfied` | Original PR author's association must be in the configured `on.roles` allowlist; an empty allowlist denies everyone. |
| `P4 BotInstalledActive` | `TestFormal_P4_BotInstalledActive` | Bot must be both installed and active; a suspended/inactive install is denied even if nominally "installed". |
| `P5 ActorNotDependabot` | `TestFormal_P5_ActorNotDependabot` | `dependabot[bot]` as actor is denied unconditionally, even if all other predicates hold (confused-deputy safety net). |
| `P6 FailClosedOnMissingData` | `TestFormal_P6_FailClosedOnMissingData` | Missing actor login or missing repo identifiers on both sides deny rather than silently authorizing. |
| `P7 AllowlistNotOverride` | `TestFormal_P7_AllowlistNotOverride` | Bot allowlist membership alone does not override a failed repo-provenance check; non-allowlisted bots are denied outright. |
| `P8 AuditNoSecretLeak` | `TestFormal_P8_AuditNoSecretLeak` | Decision log records event/actor/outcome/reason but never token, credential, or payload-body fields. |
| `Authorized (conjunction)` | `TestFormal_FullyValidInput_IsAuthorized` | End-to-end sanity check: a fully valid input satisfying P1-P5 and P7 yields authorization with no denial reason. |

### Generated Test Suite

📄 pkg/workflow/ctr027_formal_test.go

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

// Package workflow_test provides a formal-model-derived test suite for the
// "Allowlisted Bot Synchronization Provenance" control described in:
//
// specs/compiler-threat-detection-changelog.md (Mapping Audit 2026-09-11, CTR-027 paragraph)
// specs/compiler-threat-detection-spec.md (Section 5.1, CTR-027)
//
// Formal predicates encoded (see issue body "Formal Model" section for the
// full TLA+ / Z3-style notation):
//
// P1 EventGuard — trigger event must be pull_request or pull_request_target `synchronize`.
// P2 RepoProvenanceMatch — head/base repository IDs (or names, if IDs unavailable) must match.
// P3 AuthorRoleSatisfied — the original PR author must satisfy configured `on.roles`.
// P4 BotInstalledActive — the acting bot must be installed and active (not merely allowlisted).
// P5 ActorNotDependabot — the synchronizing actor must not be `dependabot[bot]`.
// P6 FailClosedOnMissingData — any missing provenance datum causes denial, never silent allow.
// P7 AllowlistNotOverride — allowlist membership alone (without P1-P5) MUST NOT authorize.
// P8 AuditNoSecretLeak — the decision log records inputs/outcome but never credentials or payload bodies.
package workflow_test

import (
"testing"

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

// --- stub — replace with real implementation ---
//
// SyncProvenanceInput models the decision inputs described in the spec
// paragraph: event type, repository provenance, PR author role membership,
// bot installation/activity state, and the synchronizing actor's login.
type SyncProvenanceInput struct {
EventName string // "pull_request" | "pull_request_target" | other
EventAction string // "synchronize" | other
HeadRepoID string // empty means "unavailable"
BaseRepoID string // empty means "unavailable"
HeadRepoName string // fallback comparison when IDs are unavailable
BaseRepoName string // fallback comparison when IDs are unavailable
AuthorAssociation string // e.g. "OWNER", "MEMBER", "CONTRIBUTOR"
AllowedRoles []string // configured on.roles
BotAllowlisted bool // actor's login is in the CTR-027 bot allowlist
BotInstalled bool // bot app is installed on the repository
BotActive bool // bot app installation is active (not suspended)
ActorLogin string // synchronizing actor login
}

// DecisionOutcome is the fail-closed result of evaluating CTR-027.
type DecisionOutcome struct {
Authorized bool
Reason string // stable diagnostic reason when denied
}

// evaluateSyncProvenance is a stub reference model of the CTR-027 gate
// described in specs/compiler-threat-detection-changelog.md's 2026-09-11
// mapping audit paragraph. Replace with a call into the real compiler
// decision function once implemented/located in pkg/workflow.
func evaluateSyncProvenance(in SyncProvenanceInput) DecisionOutcome {
// P1 EventGuard
if in.EventAction != "synchronize" {
return DecisionOutcome{false, "event_not_synchronize"}
}
if in.EventName != "pull_request" && in.EventName != "pull_request_target" {
return DecisionOutcome{false, "event_not_pull_request_family"}
}

// P5 ActorNotDependabot (checked early — fail-closed, no exception path)
if in.ActorLogin == "dependabot[bot]" {
return DecisionOutcome{false, "actor_is_dependabot"}
}

// P7 AllowlistNotOverride — allowlist alone is necessary but insufficient.
if !in.BotAllowlisted {
return DecisionOutcome{false, "bot_not_allowlisted"}
}

// P4 BotInstalledActive
if !in.BotInstalled || !in.BotActive {
return DecisionOutcome{false, "bot_not_installed_or_inactive"}
}

// P2 RepoProvenanceMatch — prefer ID comparison, fall back to name comparison
// only when IDs are unavailable (both empty).
if in.HeadRepoID != "" || in.BaseRepoID != "" {
if in.HeadRepoID == "" || in.BaseRepoID == "" || in.HeadRepoID != in.BaseRepoID {
return DecisionOutcome{false, "repo_id_mismatch_or_missing"}
}
} else {
if in.HeadRepoName == "" || in.BaseRepoName == "" || in.HeadRepoName != in.BaseRepoName {
return DecisionOutcome{false, "repo_name_mismatch_or_missing"}
}
}

// P3 AuthorRoleSatisfied
roleMatched := false
for _, role := range in.AllowedRoles {
if role == in.AuthorAssociation {
roleMatched = true
break
}
}
if !roleMatched {
return DecisionOutcome{false, "author_role_not_satisfied"}
}

return DecisionOutcome{true, ""}
}

// redactDecisionLog is a stub reference model of P8 AuditNoSecretLeak: it
// returns only the fields that are safe to log (inputs relevant to the
// decision and the outcome), never a token/credential/payload body.
func redactDecisionLog(in SyncProvenanceInput, out DecisionOutcome) map[string]string {
return map[string]string{
"event": in.EventName + ":" + in.EventAction,
"actor": in.ActorLogin,
"authorized": boolToStr(out.Authorized),
"reason": out.Reason,
"author_assoc": in.AuthorAssociation,
}
}

func boolToStr(b bool) string {
if b {
return "true"
}
return "false"
}

// baseValidInput returns a fully-authorized baseline input so each test can
// mutate a single field to explore the corresponding predicate's boundary.
func baseValidInput() SyncProvenanceInput {
return SyncProvenanceInput{
EventName: "pull_request",
EventAction: "synchronize",
HeadRepoID: "1001",
BaseRepoID: "1001",
HeadRepoName: "acme/repo",
BaseRepoName: "acme/repo",
AuthorAssociation: "MEMBER",
AllowedRoles: []string{"MEMBER", "OWNER"},
BotAllowlisted: true,
BotInstalled: true,
BotActive: true,
ActorLogin: "trusted-sync-bot[bot]",
}
}

// TestFormal_P1_EventGuard covers the predicate that only pull_request /
// pull_request_target `synchronize` events are in scope for CTR-027.
func TestFormal_P1_EventGuard(t *testing.T) {
tests := []struct {
name string
eventName string
eventAction string
wantAuth bool
wantReason string
}{
{"pull_request synchronize authorized", "pull_request", "synchronize", true, ""},
{"pull_request_target synchronize authorized", "pull_request_target", "synchronize", true, ""},
{"pull_request opened denied", "pull_request", "opened", false, "event_not_synchronize"},
{"issue_comment synchronize denied", "issue_comment", "synchronize", false, "event_not_synchronize"},
}
for _, tc := range tests {
t.Run(tc.name, func(t *testing.T) {
in := baseValidInput()
in.EventName = tc.eventName
in.EventAction = tc.eventAction
out := evaluateSyncProvenance(in)
assert.Equal(t, tc.wantAuth, out.Authorized, "P1 EventGuard: authorization mismatch for %s/%s", tc.eventName, tc.eventAction)
if !tc.wantAuth {
assert.Equal(t, tc.wantReason, out.Reason, "P1 EventGuard: expected stable diagnostic reason")
}
})
}
}

// TestFormal_P2_RepoProvenanceMatch covers the predicate requiring head/base
// repository IDs (or names, when IDs are unavailable) to match, and fail
// closed when identifying data is missing (edge case).
func TestFormal_P2_RepoProvenanceMatch(t *testing.T) {
tests := []struct {
name string
headRepoID string
baseRepoID string
headRepoName string
baseRepoName string
wantAuth bool
wantReason string
}{
{"matching IDs authorized", "1001", "1001", "acme/repo", "acme/repo", true, ""},
{"mismatched IDs denied", "1001", "2002", "acme/repo", "acme/repo", false, "repo_id_mismatch_or_missing"},
{"fallback to matching names when IDs unavailable", "", "", "acme/repo", "acme/repo", true, ""},
{"fallback name mismatch denied", "", "", "acme/repo", "other/repo", false, "repo_name_mismatch_or_missing"},
// edge case: one ID present, one missing must fail closed, not fall back to names.
{"partial ID missing fails closed (edge case)", "1001", "", "acme/repo", "acme/repo", false, "repo_id_mismatch_or_missing"},
}
for _, tc := range tests {
t.Run(tc.name, func(t *testing.T) {
in := baseValidInput()
in.HeadRepoID = tc.headRepoID
in.BaseRepoID = tc.baseRepoID
in.HeadRepoName = tc.headRepoName
in.BaseRepoName = tc.baseRepoName
out := evaluateSyncProvenance(in)
assert.Equal(t, tc.wantAuth, out.Authorized, "P2 RepoProvenanceMatch: authorization mismatch for %s", tc.name)
if !tc.wantAuth {
assert.Equal(t, tc.wantReason, out.Reason, "P2 RepoProvenanceMatch: expected stable diagnostic reason")
}
})
}
}

// TestFormal_P3_AuthorRoleSatisfied covers the predicate requiring the
// original PR author to satisfy the configured on.roles allowlist.
func TestFormal_P3_AuthorRoleSatisfied(t *testing.T) {
tests := []struct {
name string
authorAssociation string
allowedRoles []string
wantAuth bool
}{
{"member role satisfied", "MEMBER", []string{"MEMBER", "OWNER"}, true},
{"owner role satisfied", "OWNER", []string{"MEMBER", "OWNER"}, true},
{"contributor not in allowlist denied", "CONTRIBUTOR", []string{"MEMBER", "OWNER"}, false},
{"empty allowlist denies everyone (edge case)", "OWNER", []string{}, false},
}
for _, tc := range tests {
t.Run(tc.name, func(t *testing.T) {
in := baseValidInput()
in.AuthorAssociation = tc.authorAssociation
in.AllowedRoles = tc.allowedRoles
out := evaluateSyncProvenance(in)
assert.Equal(t, tc.wantAuth, out.Authorized, "P3 AuthorRoleSatisfied: authorization mismatch for %s", tc.name)
if !tc.wantAuth {
assert.Equal(t, "author_role_not_satisfied", out.Reason, "P3 AuthorRoleSatisfied: expected stable diagnostic reason")
}
})
}
}

// TestFormal_P4_BotInstalledActive covers the predicate requiring the bot to
// be both installed and active — allowlisting alone is insufficient.
func TestFormal_P4_BotInstalledActive(t *testing.T) {
tests := []struct {
name string
botInstalled bool
botActive bool
wantAuth bool
}{
{"installed and active authorized", true, true, true},
{"not installed denied", false, true, false},
{"installed but inactive/suspended denied (edge case)", true, false, false},
{"neither installed nor active denied", false, false, false},
}
for _, tc := range tests {
t.Run(tc.name, func(t *testing.T) {
in := baseValidInput()
in.BotInstalled = tc.botInstalled
in.BotActive = tc.botActive
out := evaluateSyncProvenance(in)
assert.Equal(t, tc.wantAuth, out.Authorized, "P4 BotInstalledActive: authorization mismatch for %s", tc.name)
if !tc.wantAuth {
assert.Equal(t, "bot_not_installed_or_inactive", out.Reason, "P4 BotInstalledActive: expected stable diagnostic reason")
}
})
}
}

// TestFormal_P5_ActorNotDependabot covers the predicate that the
// synchronizing actor must never be dependabot[bot], regardless of any other
// satisfied condition (confused-deputy safety net).
func TestFormal_P5_ActorNotDependabot(t *testing.T) {
in := baseValidInput()
in.ActorLogin = "dependabot[bot]"
// Even with every other predicate satisfied, dependabot[bot] must be denied.
out := evaluateSyncProvenance(in)
require.False(t, out.Authorized, "P5 ActorNotDependabot: dependabot[bot] must never be authorized even when all other predicates hold")
assert.Equal(t, "actor_is_dependabot", out.Reason, "P5 ActorNotDependabot: expected stable diagnostic reason")
}

// TestFormal_P6_FailClosedOnMissingData covers the safety property that
// missing provenance data (fail-closed default) denies rather than silently
// allowing the synchronize event.
func TestFormal_P6_FailClosedOnMissingData(t *testing.T) {
tests := []struct {
name string
mutate func(in *SyncProvenanceInput)
reason string
}{
{"missing actor login denies", func(in *SyncProvenanceInput) { in.ActorLogin = "" }, ""},
{"missing repo identifiers on both sides denies", func(in *SyncProvenanceInput) {
in.HeadRepoID, in.BaseRepoID, in.HeadRepoName, in.BaseRepoName = "", "", "", ""
}, "repo_name_mismatch_or_missing"},
}
for _, tc := range tests {
t.Run(tc.name, func(t *testing.T) {
in := baseValidInput()
tc.mutate(&in)
out := evaluateSyncProvenance(in)
assert.False(t, out.Authorized, "P6 FailClosedOnMissingData: missing provenance data must deny, not silently allow, for %s", tc.name)
})
}
}

// TestFormal_P7_AllowlistNotOverride covers the invariant that bot allowlist
// membership alone (without event/repo/role/dependabot checks passing) MUST
// NOT authorize the synchronize event — the allowlist is necessary but never
// sufficient on its own.
func TestFormal_P7_AllowlistNotOverride(t *testing.T) {
in := baseValidInput()
in.BotAllowlisted = true
// Break repo provenance while keeping the bot allowlisted, installed, and active.
in.HeadRepoID = "1001"
in.BaseRepoID = "9999"
out := evaluateSyncProvenance(in)
assert.False(t, out.Authorized, "P7 AllowlistNotOverride: allowlist membership must not override a failed repo-provenance check")

// Also verify the non-allowlisted actor is denied outright.
in2 := baseValidInput()
in2.BotAllowlisted = false
out2 := evaluateSyncProvenance(in2)
assert.False(t, out2.Authorized, "P7 AllowlistNotOverride: non-allowlisted bot must be denied")
assert.Equal(t, "bot_not_allowlisted", out2.Reason, "P7 AllowlistNotOverride: expected stable diagnostic reason")
}

// TestFormal_P8_AuditNoSecretLeak covers the decision-logging requirement:
// the audit log records decision inputs and outcome but never credentials or
// event payload contents (e.g. tokens, comment bodies).
func TestFormal_P8_AuditNoSecretLeak(t *testing.T) {
in := baseValidInput()
out := evaluateSyncProvenance(in)
logEntry := redactDecisionLog(in, out)

_, hasToken := logEntry["token"]
_, hasCredential := logEntry["credential"]
_, hasPayloadBody := logEntry["payload_body"]
assert.False(t, hasToken, "P8 AuditNoSecretLeak: decision log must never contain a token field")
assert.False(t, hasCredential, "P8 AuditNoSecretLeak: decision log must never contain a credential field")
assert.False(t, hasPayloadBody, "P8 AuditNoSecretLeak: decision log must never contain an event payload body field")

require.Contains(t, logEntry, "authorized", "P8 AuditNoSecretLeak: decision log must record the authorization outcome")
require.Contains(t, logEntry, "reason", "P8 AuditNoSecretLeak: decision log must record the stable diagnostic reason")
assert.Equal(t, "true", logEntry["authorized"], "P8 AuditNoSecretLeak: baseline valid input should be recorded as authorized")
}

// TestFormal_FullyValidInput_IsAuthorized is an end-to-end sanity check that
// the conjunction of all predicates (P1-P5, P7) yields authorization,
// matching the changelog's 2026-09-11 CTR-027 provenance description.
func TestFormal_FullyValidInput_IsAuthorized(t *testing.T) {
in := baseValidInput()
out := evaluateSyncProvenance(in)
require.True(t, out.Authorized, "conjunction of all CTR-027 predicates on a fully valid input must authorize")
assert.Empty(t, out.Reason, "authorized outcome must carry no denial reason")
}
```

### Usage

1. Copy the test file to `pkg/workflow/ctr027_formal_test.go`.
2. Replace the `// stub — replace with real implementation` `SyncProvenanceInput`/`evaluateSyncProvenance`/`redactDecisionLog` block with a call into the real CTR-027 decision function once one exists in `pkg/workflow` (a targeted search of `role_checks.go`, `bot_aliases.go`, and `dependabot*.go` did not find a standalone implementation at the time of this run).
3. Run: `go test ./pkg/workflow/... -run Formal`

### Context

- Spec processed: `specs/compiler-threat-detection-changelog.md`
- Formal notation: TLA+-style state predicates / Z3-style guard conjunction
- Run: https://github.com/github/gh-aw/actions/runs/34765612595

> Generated by [🔬 Daily Formal Spec Verifier](https://github.com/github/gh-aw/actions/runs/34765612595) · copilot · auto · 98 AIC · ⌖ 20.5 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 20, 2026, 7:36 AM UTC-08:00

Read specs/compiler-threat-detection-changelog.md and specs/compiler-threat-detection-spec.md §5.1, then inspect pkg/workflow/ctr027_formal_test.go and locate the real decision entry point in pkg/workflow. Run the relevant Go tests to understand the current behavior. Done means the CTR-027 predicates and audit constraints are exercised against the real implementation, with the formal suite passing.

Written by the indexing model from the issue text.