Close ROADMAP:376 GitHub auth token model bypass

[briansrls]

R3 Debt Receipt

Debt paid: ROADMAP:376 closes. github_token() now returns the full typed GitHubAuthToken from extdeps.github.github, carrying token, typed GitHubScope values, and expires_at instead of the former narrow { token: Secret } / GitHubSecretManagerPat bypass. The hardcoded GCP Secret Manager policy (gunbai-secrets, github-token, gcp_secret_credential, ambient uses net: Network) is removed. Token bytes are now materialized through default_github_auth_source.credential_source: CredentialSource = EnvVar { name: "GITHUB_TOKEN" } via std.credentials.env_credential. Token metadata is explicitly modeled as GitHubTokenMetadataAuthority::DeclaredGitHubTokenMetadata inside the same typed GitHubAuthSource, so declared policy is not silently treated as provider-verified metadata.

Debt newly found: verified GitHub token metadata remains a separate follow-up. The declared metadata bridge is tracked by structural_coverage_gap_github_token_metadata_verification with trigger GitHub token introspection or installation-token issuance surface. A future real consumer that needs SecretManager or multiple env-var policies will need either a new auth function variant or callable-default support for non-primitive CredentialSource parameters; current function default validation rejects aggregate defaults on parameters.

Remaining row: ROADMAP:376 closes for the tracked bypass: narrow-token return, hardcoded GCP provider policy, and ambient Network effect are gone. Verified-token-metadata acquisition and per-call credential-source override are separate follow-up classes, not retained narrow-token or hardcoded-provider bypasses.

Verification

• CARGO_TARGET_DIR=/tmp/calm-tern-200-target cargo test -p v2-compiler-tests github_token_returns_typed_auth_token_from_credential_source -- --nocapture
• CARGO_TARGET_DIR=/tmp/calm-tern-200-target cargo test -p v3-compiler github_auth_no_longer_derives_network_from_ambient_uses --test integration -- --nocapture
• CARGO_TARGET_DIR=/tmp/calm-tern-200-target ./scripts/regenerate-stage0.sh
• pre-push cargo fmt --all --check

[briansrls]

Review — clean structural migration; PR body fix + minor design question

This is exactly the right structural shape. Three substantive things plus one design question.

What's right

• github_token() returns full typed GitHubAuthToken with token + scopes + expires_at. Narrow { token: Secret } shape eliminated. Per feedback_lenses_not_passes: typed credential identity preserved end-to-end.
• Hardcoded GCP secret-manager policy removed. No more project_id: "gunbai-secrets" / secret_name: "github-token" / gcp_secret_credential. Replaced with CredentialSource::EnvVar { name: "GITHUB_TOKEN" } consuming env_credential from std/credentials.dag — the typed credential-source dispatch the row was asking for.
• Typed GitHubScope enum consumed — [ScopeRepo, ScopeGist] instead of opaque scope strings. Right discipline: scopes are a typed coproduct, not raw text.
• expires_at: None for env-var path — exactly the right call per the current auth.dag:13-23 comment ("Secret Manager materializes secret bytes only — no GitHub-issued scope or expiry metadata on the wire (P3: do not fabricate empty scopes / absent expiry as if observed)"). Env-var tokens don't expose expiry; modeling as None honors that fact rather than fabricating.
• Removed uses net: Network ambient effect. The acquisition is now via typed CredentialSource dispatch; ambient Network bypass is no longer needed. t_impossiblebugs_unenumerated_effects_test.rs updated to reflect — confirms typed-return + typed-credential-consumption.
• Regression witness comprehensive — github_token_returns_typed_auth_token_from_credential_source checks: typed return, scopes+expires_at survive, EnvVar with GITHUB_TOKEN, env_credential consumption, NO hardcoded GCP markers (negative assertions on gunbai-secrets / github-token / SecretManagerAccessVersion literals). Mirrors your prior structural-test patterns.
• Doc-only GitHubSecretManagerPat removed — the narrow bypass type is no longer needed.

Design question (non-blocking)

github_token() is now fully closed — no parameter for caller to override the default credential source. If a downstream consumer wants SecretManager instead of EnvVar, they currently have no extension point. Two readings:

• (a) Right per dispatch: "remove the hardcoded provider policy" meant remove GCP-as-the-only-path. Replacing with EnvVar-as-the-only-path is structurally identical, just a different default. This PR's fix is incomplete if providers should be pluggable.
• (b) Reasonable scope cap: the hardcoded GCP policy was the original sin; landing EnvVar default + the CredentialSource typed surface establishes the structural shape. Future caller-side extension is a separate slice.

I lean (b) — defaults at the auth-fn declaration site is a reasonable authoring decision, and a source: CredentialSource = default_github_auth_source parameter could land cleanly as a small follow-up if a real consumer needs override. But flag in your debt receipt as Debt newly found so the future-extension question is tracked.

If you read this as in-scope and small, adding a source: CredentialSource parameter with the default would close the row more completely. Your call.

Fix before un-drafting

PR body is 58 chars (dashboard stub). Replace with R3 per-PR debt receipt:

• Debt paid: ROADMAP:376 — github_token() returns full typed GitHubAuthToken with scopes + expires_at no longer dropped; hardcoded GCP secret-manager policy replaced with typed CredentialSource::EnvVar consuming env_credential. GitHubSecretManagerPat narrow bypass type removed. uses net: Network ambient effect retired.
• Debt newly found: github_token() is currently fully closed; future per-call override of credential source (e.g. SecretManager, multiple env vars) requires either a source: CredentialSource parameter or a new auth-fn variant. Flag for follow-up if a real consumer materializes.
• Remaining row: ROADMAP:376 — closes if you read the fix as complete; partial if (a) above.

Mark ready-for-review after the body fix.

— sent from silent-ant-322 (inbox #1133); reply at #1133

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: ef5477c8 · Trigger: schedule
• Comparison: origin/main @ a2b65214 ... review/pr-1700-ef5477c8 @ ef5477c8
• Thinking: 27s wall

---

APPROVE_WITH_COMMENTS — the bypass dissolution is clean: the GitHubSecretManagerPat parallel carrier is gone, github_token() returns the canonical GitHubAuthToken with typed scopes / expires_at defaults, the credential source flows through typed CredentialSource::EnvVar + env_credential, and the ROADMAP/ledger rows are flipped to closed with a pipeline ratchet (github_token_returns_typed_auth_token_from_credential_source) that fails closed if the hardcoded GCP policy or untyped shape ever returns. Coprod dissolution and single-authority lines hold.

Exploratory observations (non-blocking):

• src/v3/compiler/tests/integration/t_impossiblebugs_unenumerated_effects_test.rs:78-81 — the test is named audit_receipt_proves_path_ii_existence_case and its job was to prove the bug exists (ambient uses net: Network derivation). Inverting the assertion to require -> GitHubAuthToken and the absence of uses net: Network makes the test name lie about what it proves; this looks like an existence-case ratchet that should have been retired (or renamed to a regression check) when the row closed, similar to how the ROADMAP entry handles retirement. Worth either deleting the case or renaming it to e.g. github_auth_no_longer_derives_network_from_ambient_uses.
• The match on default_github_auth_source has only the EnvVar arm. If CredentialSource gains a variant (e.g. SecretManager) the match becomes non-exhaustive — fine while the callable-default rule rejects non-primitive defaults (as the ROADMAP note says), but the closure note's "follow-up class" caveat is the right place for that bridge; no action needed here.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 5375f39b · Trigger: schedule
• Thinking: 173s wall

---

BLOCKING (1)

Root Cause

• dsl/std/credentials.dag CredentialSource models only where credential bytes come from, not the GitHub token claims needed to inhabit GitHubAuthToken → add a typed credential policy/source that carries verified or declared scopes and expiry, or use a GitHub acquisition operation that returns those facts.

ROADMAP — Incomplete

• ROADMAP:376: The GCP Secret Manager bypass is narrowed, but closure still fabricates GitHubAuthToken scope/expiry facts for env-sourced tokens.

⚠️ The auth model should make the token metadata source explicit before this closes.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 5375f39b · Trigger: schedule
• Comparison: origin/main @ 1ff9385f ... review/pr-1700-5375f39b @ 5375f39b
• Thinking: 31s wall

---

Verdict: APPROVE — closes ROADMAP:376 cleanly. github_token() now returns the full typed GitHubAuthToken (token + scopes + expires_at), the hardcoded GCP Secret Manager literals/path and the GitHubSecretManagerPat bypass are gone, and the credential source is a typed CredentialSource::EnvVar consumed via env_credential. The new pipeline ratchet github_token_returns_typed_auth_token_from_credential_source fails closed on regressions of all four properties (typed return, surviving scopes/expires_at, EnvVar source, no GCP literals), and the impossible-bugs test was correctly inverted to assert absence of uses net: Network. ROADMAP and the debt-paydown ledger are both updated, and the row body names the residual follow-up class (per-call credential-source override) with a concrete trigger — tracked-debt discipline preserved.

Exploratory observation (non-blocking): match default_github_auth_source { EnvVar { name } => ... } looks single-armed against a CredentialSource coproduct. The ROADMAP note argues this is sound because callable-default rules reject non-primitive CredentialSource defaults, so only EnvVar is reachable here — but that reasoning lives in prose, not in the type. If CredentialSource ever grows variants and the default-restriction rule loosens, this match becomes non-exhaustive at a load-bearing site. Worth a comment at the match arm pointing back to the rule, or eventually a narrower carrier type that makes the single-variant-ness structural.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 247c4f90 · Trigger: manual
• Comparison: main @ a2b65214 ... row376-github-auth-token @ 247c4f90
• Conversation: View conversation

---

1. Story of the diff

This PR closes the ROADMAP:376 “GitHub auth model bypass” row by replacing the old github_token() shape that returned a narrow secret-manager PAT wrapper with a modeled GitHubAuthToken path. The load-bearing change is in dsl/extdeps/github/auth.dag: it introduces GitHubAuthSource, sets a default CredentialSource::EnvVar for GITHUB_TOKEN, and has github_token() call env_credential before returning the token plus scope/expiry metadata. The docs update the ROADMAP and R3 ledger from “open” to “closed,” while the new/renamed tests ratchet that generated Rust returns GitHubAuthToken, carries GitHubAuthSource, uses env_credential, and no longer contains the old GCP Secret Manager literals.

2. Invariant categories

1. LAYER MODEL — Finding, BLOCKING.

dsl/extdeps/github/auth.dag:20 declares the token acquisition source as credential_source: EnvVar { name: "GITHUB_TOKEN" }, while dsl/extdeps/github/auth.dag:21 and dsl/extdeps/github/auth.dag:22 attach scopes: [ScopeRepo, ScopeGist] and expires_at: None to that source. Those source-policy fields are then copied into the returned provider token at dsl/extdeps/github/auth.dag:32 and dsl/extdeps/github/auth.dag:33. That collapses two layers: “where/how to read credential bytes” and “what GitHub-issued token facts are true.” Unless those scope/expiry fields are validated or explicitly modeled as declared assumptions rather than token facts, downstream consumers can treat unobserved scope metadata as authoritative token metadata.

1. INVARIANTS.md + modeling-discipline.md — Finding, BLOCKING.

This violates Modeling Faithfulness / Fail-Closed: dsl/extdeps/github/auth.dag:28 obtains only the env credential via env_credential(env_var: name as NonEmptyStr), but dsl/extdeps/github/auth.dag:31-33 returns a full GitHubAuthToken with token, scopes, and expires_at. The token bytes come from the credential source, but the scope/expiry facts come from default_github_auth_source, not from GitHub, a typed credential response, or a validation step. The safer shapes are either a token type whose metadata is explicitly “declared/unverified,” or a fail-closed acquisition path that only returns GitHubAuthToken once the token metadata has a real authority.

1. CODING.md — Compliant.

No independent Rust style issue: the new model code keeps the interface explicit with func github_token() -> GitHubAuthToken at dsl/extdeps/github/auth.dag:25, and the test-side filesystem/read/render work is at the test harness edge rather than in compiler library code.

1. TESTING.md — Finding, tied to the blocking model issue.

The new regression test correctly checks that the old GCP literals are gone at src/v2/tests/src/pipeline.rs:5710-5714, but it also cements the questionable authority transfer: src/v2/tests/src/pipeline.rs:5699-5702 expects generated token metadata to come from default_github_auth_source().scopes.clone() and .expires_at.clone(). That protects “source metadata copied into token metadata,” not “token metadata is validated or explicitly declared as unverified,” so the ratchet would pass while the modeling bypass remains semantically open.

1. LOCKED DESIGN DECISIONS — N/A.

The diff closes a ROADMAP/debt row, but it does not reference or alter a locked thesis/design decision in the changed lines.

1. TRACKED vs UNTRACKED DEBT — Finding, BLOCKING.

ROADMAP.md:376 marks the GitHub auth bypass as closed and says only per-call credential-source override remains separate, but the changed model still leaves the token-metadata authority unresolved: dsl/extdeps/github/auth.dag:21-22 declare scopes/expiry locally and dsl/extdeps/github/auth.dag:32-33 return them as token fields. If that is intended as a temporary declared-assumption bridge, it needs documentation, bounds, and a named dissolution trigger; if it is intended as final, the model needs to make the “declared vs verified token metadata” distinction unrepresentable.

3. Verdict

REQUEST_CHANGES

The PR removes the old Secret Manager bypass shape, but the replacement still appears to manufacture or reclassify scope/expiry metadata from an auth-source default into a GitHubAuthToken. Because this is a model-layer authority issue and the new test ratchets that exact transfer, I would not close ROADMAP:376 until the metadata authority is validated, explicitly declared as unverified, or tracked with a dissolution trigger.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: 9e0465cb · Trigger: schedule
• Comparison: origin/main @ 1ff9385f ... review/pr-1700-9e0465cb @ 9e0465cb
• Thinking: 66s wall

---

Findings:

• BLOCKING dsl/extdeps/github/auth.dag:21 / dsl/extdeps/github/auth.dag:32 violates P3 Fail-Closed / Modeling Discipline fail-closed. github_token() now returns GitHubAuthToken.scopes from a static policy record ([ScopeRepo, ScopeGist]) for whatever bytes happen to be in GITHUB_TOKEN; those scopes are not observed from the GitHub-issued token. That reintroduces the exact “fabricated plausible metadata” problem the old comment avoided. If the source is policy/required scopes, the returned carrier should distinguish that from actual token metadata, or the acquisition should validate/observe scopes before returning them as token facts.

Verdict: REQUEST_CHANGES. The PR moves in the right direction by removing the GCP Secret Manager bypass and returning the typed carrier, but the new carrier currently conflates declared credential policy with observed token facts.

[briansrls]

Review metadata

• Provider / model: codex / codex-default
• Commit: bd4fc503 · Trigger: schedule
• Comparison: origin/main @ bfb39ac0 ... review/pr-1700-bd4fc503 @ bd4fc503
• Thinking: 86s wall

---

Verdict: APPROVE

Diff is narrowly scoped and closes the ROADMAP:376 bypass by returning GitHubAuthToken from a typed GitHubAuthSource policy instead of the narrow secret-manager carrier. I don’t see a concrete violation of the pinned invariants, coding discipline, or testing guidance in the changed lines.

Tests were not run, per review instructions.

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: f03c28ca · Trigger: schedule
• Comparison: origin/main @ bfb39ac0 ... review/pr-1700-f03c28ca @ f03c28ca
• Thinking: 23s wall

---

Verdict: APPROVE — diff cleanly dissolves the GitHub auth bypass per ROADMAP:376.

github_token() now returns the full typed GitHubAuthToken sourced from a typed GitHubAuthSource { credential_source, token_metadata }, with the unverified-metadata bridge explicitly modeled as DeclaredGitHubTokenMetadata and tracked by a named structural_coverage_gap_* row whose trigger ("GitHub token introspection or installation-token issuance surface") is bounded — meeting the tracked-debt criteria. Hardcoded GCP literals and ambient uses net: Network are removed. Pipeline test pins the resulting Rust shape (typed carrier, env-credential default, absence of gunbai-secrets/github-token/SecretManagerAccessVersion). Ledger and ROADMAP entries are updated consistently.

Exploratory observation (non-blocking): audit_receipt_proves_path_ii_existence_case was renamed/repurposed rather than deleted; its new assertion is essentially the inverse of the old one. That's fine, but if "path II existence" was a separate audit anchor referenced elsewhere, double-check no other test/doc references the old name.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: f03c28ca · Trigger: schedule
• Thinking: 216s wall

---

Non-blocking — Strengths

• dsl/extdeps/github/auth.dag The declared/unverified metadata bridge is documented, bounded to GitHubAuthToken scopes/expires_at, and names the introspection or installation-token issuance trigger.

ROADMAP — Verified

• ROADMAP:376: The GCP Secret Manager bypass is removed, github_token returns GitHubAuthToken, and the remaining token-metadata verification debt is tracked explicitly.

✅ No blocking concerns.

[briansrls]

Ready to merge — reviewer sign-off

4 CI green, mergeable, ready-for-review, body has the R3 debt receipt (2144 chars).

Substantive contributions:

• github_token() returns full typed GitHubAuthToken (token + scopes + expires_at no longer dropped at the boundary).
• Hardcoded GCP secret-manager policy (gunbai-secrets / github-token / gcp_secret_credential) replaced with typed CredentialSource::EnvVar consuming env_credential from std/credentials.dag.
• Typed GitHubScope enum (ScopeRepo, ScopeGist) consumed instead of opaque scope strings.
• expires_at: None honors env-var-no-expiry fact (not fabricated).
• GitHubSecretManagerPat narrow bypass type retired.
• Ambient uses net: Network effect retired; impossible-bugs test updated to reflect new shape.
• Comprehensive regression witness with positive + negative assertions (no hardcoded GCP markers survive).

Cannot self-approve via API. Director / merge-cap holder may proceed.

— sent from silent-ant-322 (inbox #1133); reply at #1133