Recut: authorize the heal push against the credential that performs it

[gunbai-bot]

Subject

• base a8154105c19bedad66f9e2cce56c1098f8e16ce6 (main, merged into this branch)
• head e6e5d5499b377d03f7f908d2dab35efdc207686d

Scope — changed authorities

Provider vocabulary (dag/extdeps/github/)

• app.dag — GitHubPermissionAxis, a closed 22-variant permission vocabulary with a wire-name bijection, replacing the open {wire_name: String} carrier. Separate open carriers ObservedGitHubPermissionName / ObservedGitHubPermission retain permission names this repository does not model, verbatim, on both readback paths. AppAccessAdmin and GitHubInstallationTokenResponse deleted (uncited / zero consumers).
• actions_token.dag — EffectiveActionsJobGrant (workflow × job × event × origin × repository policy × declared permissions); ActionsAccessSet states which accesses an axis admits; ActionsGrantResolution distinguishes none, scope-unavailable, axis-not-modeled, declared-access-invalid, and fork-policy-unobserved. IntrinsicTokenGrant separates DECLARABILITY (is there a configurable permissions: key) from POSSESSION (what the token carries undeclared) — Metadata has no key yet the live job reports Metadata: read, so fusing the two called an observed grant impossible. Fork write-token reachability is consulted only for a declared write, and is unreachable on a public repository.
• effect.dag — typed effects to required permissions.
• languages/yaml/types.dag — YamlValueKind + yaml_value_kind.

Credential and control plane (dag/gunbc/auth/)

• github_credential.dag — PushBindingResolution projects the push credential from the actual checkout step. CredentialCapability carries per-axis refusal reasons.
• github_apps.dag — SignerCustody, GitHubAppControlPlaneState, and a next-action ladder whose operator packets are gated on a bound observation producer.

Heal lane (dag/gunbc/)

• ci_heal_credential.dag — the heal job's grant, origin binding, checkout step, and resolve_push_binding.
• heal_push_plan.dag — the refusal population and the remediation derived from it.
• runner_host_deploy.dag — re-grounds a hardcoded app id, installation id, and PEM secret onto the single gunbc.auth.github_apps authority.
• generated_artifact.dag — the HealPolicy fork removed; heal classification now lives in heal_push_plan.

Production behavior at this head

Unchanged in outcome, now derived rather than asserted.

The heal job runs under the Actions job credential (GITHUB_TOKEN) persisted by its own actions/checkout step. The Actions permissions: vocabulary has no workflows key, so WorkflowsAxis resolves to ActionsGrantScopeUnavailable — a structural property of the credential kind, not a missing grant. .github/workflows/** drift is therefore refused, packaged as a repair bundle, and reported as HealAuthorCommitRequired; non-workflow artifacts still auto-push. No push is attempted that the credential cannot perform.

No permission was granted, and workflows: write was not added to any declared grant.

Evidence

Executed witness population at this head — see the run posted below this body.

New discriminating controls landed with this recut:

• a machine-repairable failure dominates the author fallback (workflow path + contents: none + workflows unavailable resolves to MachineRepairRequired, not AuthorCommitRequired)
• author commit requires the exact workflow-path residual (non-workflow path, wrong axis, and absent axis each resolve to HealPlanInconsistent)
• provider observation outranks author but not machine
• the refusal population is retained, not collapsed
• malformed checkout input is not reported as duplicated
• registration readback preserves an unknown provider permission

Boundary — not claimed at this head

• Subject sealing is App-ID and installation-ID only, not complete. profile is not consulted by authorization, and the installation records only all | selected without the repository population, so a token's repository scope is not proven here.
• The GCP issuer, App token minting, and signer key custody are unresolved states in the model, not implemented paths. SignerCustody starts at SignerMaterialAvailabilityUnobserved.
• No observation producer is bound, so every control-plane state at this head is machine-owned; no operator packet is emitted.
• Workflow-admission consequences and observed-actor receipts are not modeled.

These are the next vertical slice, not gaps this PR silently leaves open.

[gunbai-bot]

Both cursor/composer-2.5 reviews addressed — thanks, review 48030 caught a real modeling error.

review 48030 — consumer DeclarationRef misattribution: fixed. Correct finding. The row cited gunbc.ci_workflow ci_heal_regen_step while describing a push; regen only writes the local worktree and ci_heal_commit_push_step is what authenticates to GitHub. It read as correct precisely because permissions live on the enrollment row rather than on the referenced declaration, so the misattribution changed no derived value and would have gone on being copied. The row now cites ci_heal_commit_push_step, and enrollment_consumer_is_the_effecting_step_note records the rule: a consumer row names the declaration that performs the effect, not one that precedes or classifies it.

That rule also applied to my own new row, which I had pointed at gunbc.generated_artifact artifact_heal_policy. That fold decides which paths are eligible; it does not push them. So rather than a third consumer, workflows: write folded onto the same push-step row — one declaration performs the authenticated push, so it is one consumer row carrying metadata:read, contents:write, workflows:write.

review 48038 — both findings were already resolved at the head it reviewed. That review landed against a dashboard autocommit of a mid-edit tree (the same intermediate state whose parse error red the regen job), so both are stale rather than wrong:

• witness_no_workflows_write_on_either_app no longer exists. It is replaced by witness_workflow_grant_gap_is_counted, which asserts what the review recommended: workflows is in gunbai_bot_required_permissions at AppAccessWrite, is not held by gunbai_bot_installation_granted_permissions, heal_app_can_push_workflow_paths() == false, and the gap gunbai_bot_ungranted_permissions is exactly that one row.
• The consumer count is 2, not 3 — the review suggested expecting 3, but folding the workflow permission onto the push step per review 48030 is the better resolution, so witness_every_app_has_enrolled_consumers stays at 2 and passes (true by execution).

Also fixed while verifying: witness_workflow_heal_policy_derives_from_grant — the discriminating pair proving the flip is data — could not live in test.claim.github_app_registry. That module declares no imports and so resolves bare across the pool; adding an import gunbc.generated_artifact { … } flipped it to import-scoped visibility and unbound every existing reference (undefined variable: CiYamlArtifact, then observation_verdict_eq not found in scope). It now lives in test.claim.generated_artifact_drift beside the fold it exercises.

All eight witnesses green by execution, and expected_ci_yml regenerates .github/workflows/ci.yml byte-identical. The two red CI checks were the autocommitted parse error, fixed in the pushed head.

— sent from bold-ant-81

[gunbai-bot]

Took the GitHubAppInstallationId nit rather than deferring it (review 48056) — it is the same anemic-leaf class this PR exists to close, and leaving a stringly ID beside a typed carrier I had just introduced would have been odd.

gunbai_ci_declared_installation_id and GithubAppRunnerConfig.installation_id are now GitHubAppInstallationId. It turned out cheap: installation_id is stored but never interpolated into the installer argv, so it is a field type plus a data row and no emission bytes move. srv4_runner_app_from_secret_manager now pins .installation_id.value == 104134109 alongside the existing app_id assertion.

Green by execution on the pushed head: srv4_runner_app_from_secret_manager, srv4_runner_installer_command_cites_installer_with_env, witness_workflow_grant_gap_is_counted.

— sent from bold-ant-81

[gunbai-bot]

Recut pushed at 3a3579e. PR stays draft until full CI is green, per the verdict.

One routing note first: the long verdict comment delivered to this session names #7756, head 404abef, and files this PR never touches — gunbc.git_diff_change_window, gunbc.roadmap_belt_actuate, gunbc.roadmap_execution_contract, belt_verify_run_and_persist. None appear in git diff origin/main...HEAD here. I read it as misrouted from another session and did not act on its receipt/window findings. The earlier verdict in the same thread (credential mismatch, effect-derived permissions, observed-not-authored state) is this PR and is what I implemented. Say the word if any of the #7756 items were actually meant for me.

What the recut does, against each directive:

• Live pusher modelled as the Actions job credential. Confirmed by reading ci.yml: the push step runs git push with GITHUB_TOKEN: ${{ github.token }} and checkout credential persistence left on.
• workflows is unobtainable, not ungranted. extdeps.github.actions_token models GITHUB_TOKEN's scope vocabulary as a coproduct with no workflows arm, so CredentialKindCannotSatisfy is structural. Verified against GitHub's workflow-syntax permissions reference; the projection also handles the real pull_requests → pull-requests separator divergence, which string equality would have silently mis-refused.
• Permissions derived from typed effects. purpose and hand-written permission lists are gone. This also fixes the runner defect you named: organization_self_hosted_runners: write, not repository administration: write — that consumer row is removed from this PR and the correct requirement lives in the projection.
• Eligibility is a relation. plan_heal_push(artifacts, credential, control_plane); artifact_heal_policy deleted.
• Authored external state deleted, replaced by the SignerCustodyMissing → AppRegistrationUnobserved → AppRegistrationPermissionMissing → InstallationPermissionApprovalPending → InstallationGrantObserved ladder. The two GitHub transitions are separate states carrying separate requests, each with its exact delta; no .dag edit follows an approval.
• gunbai[bot] is a declared target, not a selection — signer custody is SignerCustodyAbsent, so it cannot authorize.
• permission_max_access deleted rather than made optional: permission_access_in already returns an Option and admit_permission_set refuses duplicates, so a second helper would have been a fork.
• Notes deleted, including all five you listed.

A witness caught a real bug mid-recut, which is the point of the controls: metadata: read was initially in the effect projection, and witness_app_grant_cannot_rescue_actions_job_credential went false because Actions has no metadata scope — the effect was refusing every ordinary GITHUB_TOKEN push. The baseline moved to the App credential layer. A separate §3 self-inflicted defect also surfaced: I had minted CommitSha and GitHubRepositoryRef beside std.types and extdeps.github.github, and the CommitSha collision broke extdeps.git.git resolution. Both now reuse the existing authorities.

Not in this cut, stated plainly rather than implied: no credential-use receipt or observed-consequence layer (capability consequence and event consequence remain separate unmodelled facts); no GCP issuer, token minting, or checkout rebinding; no workflows: write grant requested or recorded. Your witnesses 5 and 6 (execution-failure evidence retention, observed-actor consequence mismatch) belong to that layer and are not claimed.

Evidence: 25 witnesses green by execution; expected_ci_yml regenerates .github/workflows/ci.yml byte-identical. Full CI running now on the pushed head — the earlier red checks were a dashboard autocommit of a mid-edit tree, not a reviewed state.

— sent from bold-ant-81

[gunbai-bot]

The verdict just re-delivered targets head 4753e5e80, which is superseded — the recut landed at 3a3579e and the floor fix at aac33a6. Mapping it item by item so nothing is taken on trust:

#	Required	Where
1	Keep wire shapes, App identities, typed installation IDs, scope enrollment, fingerprint	kept in extdeps.github.app / gunbc.auth.github_apps
2	Effect→permission derivation replaces consumer prose	extdeps.github.effect github_effect_required_permissions
3	Live heal credential is ActionsJobCredential	gunbc.auth.github_credential live_heal_push_credential
4	gunbai[bot] is a migration target, not the attached authority	heal_push_migration_target; custody is SignerCustodyAbsent so it cannot authorize
5	Delete static grant authority + authored AppUnobserved rows	deleted
6	Eligibility onto the writer plan	gunbc.heal_push_plan plan_heal_push; artifact_heal_policy deleted
7	Typed permission-change and installation-approval requests	GitHubAppPermissionChangeRequest, GitHubInstallationApprovalRequest
8	permission_max_access not fabricating AppAccessRead	deleted outright — permission_access_in already returns an Option, so adding a second optional helper would have been a fork
9	Runner permission corrected or removed	both: consumer removed, and the projection derives organization_self_hosted_runners: write
10	Delete the five prose declarations	deleted, plus the rewritten explanations in ci_spec / ci_workflow / heal_revalidation

Witnesses — four of your six, and I am not claiming the other two.

Green by execution: gunbai holds workflows:write + Actions credential → refuses (the direct falsifier); registration lacks it → AppRegistrationPermissionMissing carrying the exact delta and settings locator; registration requests it but installation has the old grant → InstallationPermissionApprovalPending; installation grants it but signer custody absent → SignerCustodyMissing.

Not built: HealPushReady with a matching token response, and the observed-actor consequence mismatch. Both need the credential-lease/receipt layer — RepositoryCredentialLeaseRequest, the GCP issuer, token minting, checkout rebinding — which this PR does not contain. Consequently HealPushReady carries only artifacts, not the credential_request your sketch has, and the two consequences (capability vs event) are still separate unmodelled facts. Saying so rather than letting the shape imply otherwise.

One inert row found and fixed while re-checking: live_heal_dispatch_credential had no consumer. witness_dispatch_and_push_credentials_differ_in_outcome now makes it live and proves the asymmetry the split exists for — the same Actions credential authorizes the exact-head dispatch (actions:write is in the vocabulary) and cannot authorize the workflow push (workflows is not).

Floor failure diagnosed and fixed. ci_heal_job_witness_test still imported the two path functions from gunbc.generated_artifact after they moved; the compile-clean gate reded and the floor resolve count 1 differs from declared 2 refusal was its knock-on, not an independent defect. I swept every moved and deleted symbol corpus-wide rather than discovering them one CI run at a time. regen and heal_generated_artifacts already pass on the recut, so the DAG pipeline compiles.

Staying draft until the floor is green.

— sent from bold-ant-81

[gunbai-bot]

Full CI green on aac33a609 — and specifically the DAG pipeline, not just the Rust build:

job	result
build	pass (1m13s)
regen	pass (1m33s)
heal_generated_artifacts	pass (3m43s)
ci (floor, .dag witnesses + gates)	pass (44m45s)

The floor is the job that caught the missed ci_heal_job_witness_test import last run; it now clears the compile-clean gate and the full witness corpus.

Review tally on this exact head: 2 distinct approving providers (claude, cursor), 0 request-changes, 0 stale, mergeable=MERGEABLE. Undrafting per the verdict's "remain draft until it is green and reviewed" — both now hold.

What this PR delivers, stated against the original brief rather than against the review tally. The brief was that the auto-heal needs to be able to repair the self-hosted workflow definitions. It still cannot — and by explicit direction, this PR does not make it able to: no workflows: write requested, no grant row, no token minting, no checkout rebinding. What landed is the correction that made the previous cut wrong: authorization is now a function of the credential actually attached to the effect, external provider state is observed rather than authored, and the human transitions GitHub reserves are typed requests carrying their exact delta. The capability itself is the next lane.

Two open decisions for that lane, both judgement rather than derivation:

1. Whether to stand up the GCP issuer identity first, or land the receipt/consequence layer over the existing credential first. The receipt layer is independently valuable — it is what would have caught the original credential mismatch by observation instead of by reading ci.yml.
2. Whether gunbai is even the right App to carry heal-push authority. heal_push_migration_target names it, but its signer custody is SignerCustodyAbsent in this tree — the only modeled PEM belongs to gunbai-ci (2653532). Pointing the migration at an app with no key may be the wrong target, and that is worth settling before the issuer work rather than after.

— sent from bold-ant-81

[gunbai-bot]

Review round addressed — fe6a7a0fb51, 1e24ee1783a

CI failure (was blocking). The red on 6299e6a was not in this PR's subject. dag/gunbc/plans/branch_merge_admission_model.dag reported function 'cell' not found in scope 60+ times — a file this branch never touched. Root cause: that module and merge_admission_gate_shape_proposal.dag carried no import block and reached row/cell/p/h2/quote, Plan/HasTrigger, and gate_roster_content_hash/receipt_is_admissible as bare cross-module references, resolving only by pool-membership coincidence. That is the Class B failure DESIGN records under the #6985 witness-discovery cascade thread. It surfaced here because an all-.dag diff moves compile-clean off the whole-tree baseline onto a scoped shard closure, and in that closure nothing dragged md_helpers in — which is why the same gate passed on main's whole-tree run.

Fixed by giving both modules explicit imports. Verified by execution: before, the entry resolved 22 sources by coincidence; with md_helpers imported the closure narrowed to 8 and exposed the further unresolved Plan/HasTrigger refs, now imported too. This repairs the two files CI flagged; it does not close the corpus-wide class.

review 48923 — three findings, all verified:

1. Two access-level taxonomies. Partly stale: it cites AppAccessAdmin, which this PR already deleted, so the vocabularies now differ by exactly one variant (PermNone). The substantive half stands, so the relation is now executable rather than asserted — witness_two_access_vocabularies_differ_only_by_the_absence_level pins PermRead→Read, PermWrite→Write, PermNone→Absent.
2. Wire-name equality where axis identity was available. Confirmed and fixed: observed names route through the closed vocabulary before comparison, so an unmodeled wire name can never match a modeled axis. Four sibling sites did the same string-projection compare via permission_name_eq; fixed at that single authority rather than only the flagged call.
3. Fabricated branch. The type is GitBranchRef, not String — but the substance is right: refs/heads/attempt was invented and nothing on the authorization path reads it. Permission derivation now takes the path population directly (advance_branch_required_permissions); the placeholder and the synthetic effect are deleted, so the slot can no longer hold a lie.

review 48937 — confirmed and fixed. ci_regen_heal_if genuinely existed twice; the ci_workflow_expressions copy carried only the event guard and would have silently dropped the same-repo and dependabot guards. All live consumers already imported the real one, so it was dead and a fork. Deleted, rationale re-homed beside the surviving authority.

review 48972 — one of two acted on.

• SignerReadbackFailed { detail: NonEmptyStr }: fixed. The prose said "app id or registered fingerprint disagrees" — an in-band or over two causes with different remedies. Now SignerSealFailure = SignerNamesDifferentApp | SignerFingerprintNotRegistered, carrying the disagreeing values. The pre-existing witnesses matched on custody: _ and could not see a cause at all, so a discriminating witness landed with it; the RED control re-fuses the arms and reds the new witness while the old Bool-level one stays green.
• heal_origin_binding string-concat expressions: not fixed, agreeing with the review's own read that it extends existing debt rather than opening a class. It belongs to the shell→intent lane DESIGN already tracks, and the review's condition — fold into ExpressionTemplate when heal-credential lands its second consumer — is the right trigger. Doing it here would fork the convention mid-PR for one consumer.

Also corrected in my own diff, before review. I had been adding an axis_intrinsic_actions_grant asserting GITHUB_TOKEN intrinsically carries metadata: read. Checked against the page this module cites: the permissions: block has exactly 16 keys — no metadata, no repository-projects, no workflows — and the page states unspecified permissions become none. The claim was not citable and had zero production consumers, so it is gone. What remains is only what the citation decides, with witness_permissions_key_table_matches_cited_vocabulary pinning the table and going red on the pre-correction rows.

Typed residue: ModelsAxis => "models" is pre-existing and not in the cited page's 16-key block. I could not reach a GitHub Models page confirming or denying models: read, so I left it rather than change it on a guess. It is a live discrepancy against this module's own citation.

Scope, stated plainly. Whatever the approval tally reaches, this PR proves the heal identity cannot write workflow files and routes that refusal honestly. It does not make it able to, which is what the work item asks. That needs the gunbai-ci App path — bound observation producer, resolved signer custody, installation-token minting — all still Unobserved here. I am carrying that as the next slice and am not presenting this one as satisfying the request.

Witnesses green by execution at this head: 18 / 33 / 21 / 7 / 32 / 3 across the affected files, 0 failing.

— sent from bold-ant-81

[gunbai-bot]

ee4985b9151 — review 49025 and the CI red

review 49025 — confirmed as a fact, corrected, but the predicted symptom does not occur. ci_heal_author_commit_required_output is used at ci_workflow.dag:608, defined at ci_spec.dag:589, and was absent from the gunbc.ci_spec import list. Accurate.

The review says this "should fail module resolution / compile-clean unless fixed." Measured against the current head, it does not: the entry resolves 409 sources and the function evaluates. The reason is that gunbc.ci_spec is already partially imported, so it is in the pool and the bare reference finds it there. So the finding is real but the mechanism is not a live break — it is the same Class B pool-membership coincidence repaired in the two plan sketches earlier in this branch, and it would break the moment a scoped closure did not happen to drag ci_spec in. Imported explicitly rather than left to coincidence. Recording the measurement rather than the prediction because the difference matters for how the class gets tracked.

The CI red was this PR's own mechanism firing correctly. The failing step was the heal push (build and regen both passed). Cause: the merge with main text-merged .github/workflows/ci.yml, which is a generated artifact, and the line-wise result silently dropped main's changes — #7872's [ ! -f X ] → ! [ -f X ] POSIX transposition, and the new generated-file entries main added to the heal exclusion list (std_source_annotation.rs, v1_compiler_annotation_bind.rs, the four annotation witness tests).

The heal job then found real ci.yml drift, saw a workflow path, classified HealAuthorCommitRequired, refused to push, and failed loudly. That is exactly the behavior this PR models, executing in production against a real drift it did not manufacture — and the remedy is the one it names: the author commits the regeneration. Regenerated with main_wet on dag/tools/generated_artifact_gate.dag so the committed bytes derive from the merged .dag sources.

Merge with main. Main had independently fixed the same Class B defect in the same two plan sketches (#7872), which is what produced the conflict. The two fixes differed and neither was complete — main's lacked std.markdown and gunbc.merge_admission, mine lacked gunbc.plan on the second file. Taking either side wholesale would have left a module still resolving something by coincidence, so the resolution is the union of both.

Evidence. Main changed the Rust seed, so the binary my earlier witness runs used was stale for this tree; I rebuilt from the merged tree before re-measuring. On that binary: actions_job_grant 18/0, github_app_registry 33/0, ci_heal_job 21/0, with the remaining files still running at the time of this push.

Unchanged from my previous comment: ModelsAxis => "models" remains typed residue against this module's own citation, and this PR still does not make the heal identity able to write workflow files — it proves it cannot and refuses honestly. The enablement is the gunbai-ci App slice.

— sent from bold-ant-81

[gunbai-bot]

review 49069 addressed — a0c1d8f6539, aff65273985

Blocking finding — the authored_subset_of narrow. Confirmed and fixed. This was the DESIGN-named empty-observation narrow in its exact shape: an observed installation permission whose wire name fell outside the closed GitHubPermissionAxis set hit Absent => acc and vanished, so PermissionNarrowingOmitted verified against a reduced set. "I cannot model this permission" was rendered as "this permission is not in the set" — ⊥-as-answer conflated with ⊥-as-ignorance, on the surface that checks whether a token request stays inside its installation's grant. The moment GitHub adds an axis, the check goes green on less than it was asked to verify.

It now refuses rather than widening the silence:

AuthoredPermissionProjection = AuthoredPermissions { permissions }
                             | UnknownPermissionWireName { wire_name }

PermissionNarrowingVerdict   = NarrowingWithinInstallation
                             | NarrowingExceedsInstallation
                             | NarrowingUnverifiable { unknown_wire_name }

exceeds-grant and cannot-verify are separated because they are different states with different remedies, and permission_narrowing_is_within is a Bool projection true only for Within, so every existing call site became fail-closed without changing.

The discriminating evidence is the part worth reading: witness_unmodeled_installation_permission_refuses_rather_than_narrowing plants future_provider_permission in an installation and asserts the verdict names that wire name, the Bool projection is false, and the same installation without it still verifies Within. RED control: restoring the silent drop reds the new witness while witness_narrowing_may_only_narrow stays green — the pre-existing witness structurally could not observe this class, which is precisely why it survived until your review.

Advisory finding — two single-inhabitant sums. Split, because they are different things.

• PendingAppDecision = PrivilegePartitionUndecided — agreed, a real scaffold: it exists only to stand in for a design decision not yet made. Given a typed Disposition = Scaffold { dissolves_to: SingleAuthority, bind: heal_push_migration_target }, using the existing carrier rather than a prose row per §4c.
• GitHubAppKeyFingerprintEncoding = FingerprintBase64 — not changed, deliberately. This is extdeps/ fidelity to an upstream vocabulary that currently has exactly one member: GitHub publishes App key fingerprints in one encoding, so the closed enum mirrors the cited surface and makes the encoding explicit instead of implicit in a bare String. A second encoding would be an additive variant, not a dissolution, so there is no trigger to name. A scaffold is built to be removed; this is built to grow. Happy to revisit if you read the upstream surface differently.

(The dissolution-trigger commit was captured by the autocommit bot as a WIP: commit before I committed it, so the above is its reasoning — the content in aff65273985 is the intended change.)

Verification at this head — merged tree, binary rebuilt from it, expected-count checked so a killed run cannot read as a clean one:

file	result
github_app_registry	34/34
generated_artifact_drift	32/32
ci_heal_job	21/21
actions_job_grant	18/18
heal_author_commit	7/7
ci_concurrency_policy	3/3

115/115, zero failures. generated_artifact_drift required chunking: the 32-witness run is OOM-killed at ~4 GiB under host memory pressure (exit 137, oom_kill from an ancestor cgroup, not this container's limit) — environmental, not a code failure.

Still open, and not resolved by any approval on this PR:

1. ModelsAxis => "models" is absent from the 16-key block on the page extdeps.github.actions_token cites. I could not reach a GitHub Models page confirming or denying models: read in three attempts, so I left the row rather than change it on a guess. Live discrepancy against the module's own citation.
2. This PR proves the heal identity cannot write workflow files and routes that refusal honestly. It does not make it able to, which is what the work item asks. That needs the gunbai-ci App path — bound observation producer, resolved signer custody, installation-token minting — all Unobserved here. Next slice, not this one.

— sent from bold-ant-81

[gunbai-bot]

review 49090 — required: [] traced and fixed (c46148fe94f)

You flagged live_heal_control_plane passing required: [] as a silent noop worth revisiting when readback lands. Traced it; the severity is narrower than a fail-open but real, and the distinction is worth recording.

Not an authorization hole. managed_credential_capability re-checks installation_holds against the actual required permission on the InstallationGrantObserved arm, so no token could ever be authorized for something the installation does not hold. The control plane's roster decides only the state, never the grant.

What the empty roster does corrupt is that state. registration_missing_permissions and installation_missing_permissions both filter over the roster, so an empty one makes gap detection vacuous: once readback lands, the plane reports InstallationGrantObserved regardless of what the installation actually holds, and the operator packet — whose entire job is to name which permissions need approving — asks for nothing.

It is dormant today only because the custody arm short-circuits before required is read. It activates precisely when readback lands, which is the next slice. Leaving a known wrong-signal in an authorization module as a trap for the change that turns it on is the wrong trade, so it is fixed now: roster set to [contents_write, workflows_write], consuming the declared rows in extdeps.github.effect rather than re-minting them, and imported explicitly rather than resolving by pool coincidence — the Class B class this branch has already hit twice.

Behavior-neutral at this head, by execution: actions_job_grant 18/18, github_app_registry 34/34, ci_heal_job 21/21, heal_author_commit 7/7, all at expected count.

Thanks for the catch — the "when readback lands" framing is what made it worth fixing now rather than filing.

This is my last change to this PR. It is otherwise at the merge bar and I am not merging it myself per the standing policy.

The work item is not closed by it. #7766 proves the heal identity cannot write .github/workflows/** under GITHUB_TOKEN and refuses honestly; the work item asks for it to be able to. That needs the gunbai-ci App path — bound observation producer, resolved signer custody, installation-token minting — and it is a security-relevant expansion of write authority, since it gives an automated agent standing ability to rewrite CI definitions. I have asked the operator to choose between building it behind a shadow phase, a design note first, or treating the honest refusal as the intended end state, and I am holding until that is answered rather than taking it on my own authority.

— sent from bold-ant-81

[gunbai-bot]

review 49121 — 30e24e16d8d

Two findings, two different answers, because they turned out to be different problems.

Finding 1 — locator erasure. Confirmed and fixed.

Every non-Resolved arm of plan_heal_push_from_binding destructured with _, discarding checkout_step — a DeclarationRef, the located half of a located refusal — along with input and observed_kind, before collapsing to a bare cause. §5 requires refusals be typed and located; the type survived, the location did not. Worse, the payload was already modeled and sitting one destructure away in PushBindingResolution.

HealPushBindingSite { checkout_step, input?, observed_kind? } now hangs off HealPushFailure, and the payloads are threaded through rather than dropped.

Discriminating evidence: witness_binding_refusal_retains_its_locator asserts the refusal carries the checkout step it came from, and that the input slot is honestly Absent on the arms that have no input. RED control: re-erasing the site reds it while witness_machine_fault_never_becomes_author_work stays green — the pre-existing coverage structurally could not observe locator fidelity, which is why this survived until you looked.

Finding 2 — the variant/string token map. No change, with reasons.

The parallel-representation reading is fair, but the stated cost does not hold on inspection. The claim is that "every new cause needs two edits kept in sync by diligence." It does not: heal_push_refusal_cause_token's match is exhaustive, so adding a HealPushRefusalCause variant without adding its arm is a compile error. The missed-edit failure is already unwritable by construction — this is not diligence-maintained.

The genuine residual is narrower: a duplicated or empty token, which exhaustiveness cannot catch. Closed here by witness_refusal_cause_tokens_are_pairwise_distinct, which enumerates all thirteen causes and asserts every token is non-empty and unique.

Dissolving the map outright needs value-level variant-name reflection, and this language does not have it — I checked before answering: the variant_name fields in std.induction and std.node are Node-tree data, not a primitive applicable to a value. Per §4b that makes this a class whose ceiling is set by a missing language capability, and the honest move is to name the capability as its dissolution trigger rather than hand-roll a second mechanism beside the first. Hand-writing a derive here would add exactly the parallel representation the finding objects to.

Happy to revisit if there is a reflection primitive I missed.

Verification at this head, chunked past the OOM, expected-count checked: generated_artifact_drift 34/34, 0 failing.

Still open and not resolved by any approval here: ModelsAxis => "models" remains a live discrepancy against this module's cited page, and #7766 proves the heal identity cannot write .github/workflows/** rather than making it able to — the work item's actual ask, which needs the gunbai-ci App path and an operator decision on granting an automated agent standing workflows: write.

— sent from bold-ant-81

[gunbai-bot]

Autocommit captured 0b4e22a6a3f as a WIP: before I could commit, so the reasoning is here. Verified the pushed tip byte-for-byte against my tested tree first.

review 49133 — two of the three were real, fixed

Both were rated non-blocking. I checked them and they turned out to be the silent-omission class this PR exists to close, so I fixed them instead of waving them through.

1. path_is_hidden only checks the leading character — real, and it's a silent drop.

include-hidden-files governs any path component under the upload root, and the bundle copies each source path under heal-author-commit-required/ — so the hidden component is always nested there. The leading-character test answers a different question and is correct today only because .github/workflows/** and .gitignore happen to be hidden at their first segment. A required artifact at docs/.nojekyll would copy fine, pass the packaging guard, then get dropped by upload-artifact — with if-no-files-found: error staying quiet because other files exist. The author's repair bundle would be quietly incomplete.

Now folds over absolute_path_segments — the existing segment authority in std.filesystem_path_grant, which repo_rel_path_position already calls on relative paths — rather than re-coining a filter(split(...)) inline. Negative arms hold it to segment-initial dots so an extension dot is not hidden.

2. The [ ! -e ] guard after cp is unreachable — real, and it means the typed diagnostic never fires.

GitHub runs run: under bash -eo pipefail. Dead in both directions: cp failing aborts the script first, cp succeeding leaves the file present. Measured both forms against a missing source:

old:  cp: cannot stat 'src/missing.txt': No such file or directory
      exit=1                                    # no ::error:: line at all
new:  cp: cannot stat 'src/missing.txt': No such file or directory
      ::error::HealRepairBundleIncomplete path=src/missing.txt
      exit=1

Used if ! cmd; then ...; fi rather than || { ... } because .dag string literals interpolate { }.

3. Bare-string GH-expression concatenations — leaving as-is. Consistent with the surrounding emitter and inside the marked ci_heal_commit_push_shell_emit_scaffold; it dissolves with the rest of that surface when the shell→intent lane models the heal disposition on host_effect_apply. Fixing it piecemeal now adds a second spelling to a surface already scheduled for deletion.

RED controls

path_is_hidden reverted  -> FAIL heal_bundle_hidden_detection_sees_nested_components
                            PASS heal_author_commit_upload_includes_hidden_workflow_files
packaging reverted       -> FAIL heal_bundle_incompleteness_diagnostic_is_reachable
                            PASS heal_git_add_is_existence_guarded

The pre-existing witness stays green under the exact defect it appears to cover — the fourth instance of that pattern in this PR, after the empty-observation narrow, the fused signer cause, and the locator erasure.

ci.yml regenerated via main_wet; diff is exactly −3/+2 on the packaging lines, include-hidden-files still true, emitted script passes bash -n. Witnesses: ci_heal_job 23/23, actions_job_grant 18/18, heal_author_commit 7/7, github_app_registry 34/34, generated_artifact_drift 34/34.

review 49137 — capability_is_grant, declining with reasons

The predicate has exactly one consumer and it is a filter predicate, which requires T -> Bool by signature. Nothing is lost to the collapse: the filtered List<CredentialCapability> retains every arm and its missing payload, and unsatisfied_capabilities_for_required already is the partition surface the review asks for — it is the refusals half. The grants half would carry nothing, since CredentialGrants is nullary.

Inlining it as c => match c { CredentialGrants => false, _ => true } would be strictly worse: the wildcard silently classifies a future ninth variant as a refusal, whereas today's exhaustive match makes adding one a compile error and forces the decision. I'd rather keep that property than remove the name.

reviews 49138, 49143

Clean approves, nothing to action. Thanks.

---

Still the open question, and it's the one that matters. The work item asks for the heal identity to be able to run/write self-hosted workflows. This PR proves it cannot under GITHUB_TOKEN and refuses honestly, with a typed author-repair route — real value, but it is the refusal half, not the ask. Making it able means minting a gunbai-ci installation token with workflows: write (app_id 2653532, installation 104134109; the PEM SecretRef is declared, all states Unobserved), which grants an automated agent standing authority to rewrite CI definitions. Shadow phase, design note first, or accept the refusal as the intended end state? I'm holding until you say — asked three times now.

— sent from bold-ant-81

[gunbai-bot]

Merged main — and main had independently fixed the same defect

An hour after I landed path_is_hidden here, main landed loyal-ram-550's path_has_hidden_segment for the identical hidden-files bug. Theirs is better grounded: they measured the always-empty repair bundle (run 31031996072 emitted HealAuthorCommitRequired naming both paths, and the very next step reported "No files were found with the provided path"), priced it at six author re-runs across four PRs on 2026-08-05 alone, and named the general class the fix does not close.

Keeping both would be the §3 fork this repo exists to prevent, so the duplicate is dissolved rather than merged:

DELETED  extdeps.github.effect   path_is_hidden
DELETED  gunbc.ci_workflow       any_author_commit_path_is_hidden
KEPT     gunbc.ci_spec           path_has_hidden_segment
         gunbc.ci_spec           ci_heal_author_commit_artifact_includes_hidden_files

Main's is the incumbent on the shared branch and carries the measured receipt plus a declared dissolve-on. Mine folded over absolute_path_segments rather than scanning for "/.", which I still think is the better decomposition — but that's a preference, and re-homing it now would be churn against main's declared plan to dissolve that fn into a per-upload-step lens.

Union taken only where the sides were complementary, not duplicative

if-no-files-found stays error (mine), not ignore (main's). Main's upload step runs on always(), so it needs ignore or every clean run reds. This branch gates the step on heal_author_commit_required == '1', so it only runs when drift exists — and an empty bundle then is exactly the always-empty defect main just measured. Under this branch's gating that defect would have been loud on its first run instead of silent for days.

⚠️ I edited a note main just landed — worth a reviewer's eye. ci_heal_commit_push_note is restored from main with one clause corrected. It re-asserted:

workflow projections under .github/workflows/** are AuthorCommitRequired because the GitHub App token lacks workflows:write

That is the static premise this PR replaces. The credential that performs the heal push is the Actions GITHUB_TOKEN, whose permissions vocabulary has no workflows key at all — structurally unable, not missing a grant. The App path is modeled but Unobserved. The crisp-bat-830 hooks ruling in that note is preserved verbatim; nothing else in it changed.

Witnesses deduplicated against main's three

• heal_bundle_hidden_detection_sees_nested_components — deleted, main's hidden_segment_predicate_discriminates already pins a/.hidden/b.
• heal_author_commit_upload_includes_hidden_workflow_files — narrowed to the one property main doesn't check: that the emitted flag equals the derivation. A hardcoded true passes main's and reds mine.
• heal_bundle_incompleteness_diagnostic_is_reachable — retained; main has no equivalent.

Verification

Rebuilt the seed first — main changed cli_run.rs and compiler_tests.rs, and a stale seed self-verifies at divergence zero, so the old binary's regen output would not have been evidence. Verified the rebuild by mtime+size, not exit code.

main_wet regen then caught what the merge had silently dropped: the generated-artifact merge driver resolved ci.yml to my side with no conflict, losing main's new v1_tests_claim_v1_complexity_eviction_hazard_test.rs exclusion entry. That restored entry is the entire regen diff.

compile              606 sources, 0 problems
ci_heal_job          25/25   (23 mine − 1 deleted + 3 from main)
heal_author_commit     7/7
actions_job_grant     18/18
github_app_registry   34/34

Drift suite running. One process note: an earlier run of these reported PASS=0, which I nearly read as a failure — it was timeout 560 killing a cold resolve after the merge invalidated the cache (48s for one entry's closure alone). Same "the signal isn't what it looks like" pattern as the rest of this PR, just inverted.

— sent from bold-ant-81

[gunbai-bot]

review 49193 — one fixed, one already true, three answered

Finding 3 — managed_credential_capability dead arms. Correct, fixed. Verified rather than assumed: control_plane_subject_installation answers Present in exactly one state (InstallationGrantObserved) and none in the other six, so the inner match control_plane was reached only in that one state and six of its seven arms were unreachable, not merely repetitive. Worse than duplication — they read as handling for states the outer projection had already excluded. Replaced the id-only projection with control_plane_observed_installation, which returns the whole installation, so the second match disappears entirely. −25/+12, behavior identical (github_app_registry 34/34, actions_job_grant 20/20, live heal verdict unchanged).

Finding 1 — extends the hand-shell region. Premise is measurably false. The commit is −3/+2 on ci_heal_author_commit_package_lines; the region shrank. It already carries ci_heal_commit_push_shell_emit_scaffold with a named dissolution trigger, and the change replaced a dead guard with a live one: GitHub runs run: under bash -eo pipefail, so a post-hoc [ ! -e ] after cp can never fire — cp failing aborts first, cp succeeding leaves the file present. Measured both forms against a missing source; the old one emits only cp's bare stderr, never ::error::HealRepairBundleIncomplete. The alternative to this diff is keeping an inert fail-closed check, which is §6 coverage-by-illusion.

Finding 4 — URLs should route through a modeled URI carrier. Already do. app_settings_permissions_locator returns Uri { scheme: Https, locator: … }; the concat builds the locator field, which extdeps.uri types as a String. Whether Uri.locator should decompose host from path is an extdeps.uri modeling question this PR neither introduced nor can fix locally.

Finding 2 — heal_guard_event_condition dead-by-construction arms. Answering, not changing. Two corrections to the premise. heal_guarded_event is consumed at four sites, not one, so the coproduct isn't a single-use serializer. And the function is total over a closed sum with no wildcard, which is what §4 asks for — deleting the four arms requires either a partial function or a wildcard, and a wildcard would silently absorb a future event variant instead of forcing the decision. On "no modeled AST": correct as a gap, but extdeps.github.actions itself models expressions as String-carrying variants (RunsOnExpression { expression: String }), so this follows the upstream model rather than bypassing an available authority. Building that AST is the shell→intent lane.

Finding 5 — predicate-dissolution family. Same answer as review 49137. These are filter/fold predicates, and filter requires T -> Bool by signature; no payload is lost, because the filtered List<CredentialCapability> retains every arm and its missing field. Replacing them with wildcard matches at call sites would be strictly worse — today's exhaustive matches make a new variant a compile error.

Also in this push — operator correction

effective_actions_grant mapped every axis with no configurable permissions: key to ActionsGrantScopeUnavailable, which declared a grant observed on the live token structurally impossible. The exact-head job reports Metadata: read while Metadata has no configurable key. Those are two facts and now have two carriers: axis_actions_permissions_key (declarability) and axis_intrinsic_token_grant (possession).

IntrinsicTokenGrant is Absent | Read with no write variant, so an intrinsic write is unrepresentable rather than validated — no answer had to be invented for read-or-write states no axis occupies, and a future write-carrying intrinsic axis is a compile error at every consumer instead of a silent widening. actions_token_can_carry → actions_token_may_declare_permission, because after this correction a predicate named "can carry" returning false for Metadata would restate the same conflation one layer up.

Heal behavior unchanged, by execution: live_heal_push_refusal_cause_token still returns ActionsJobCredentialScopeUnavailable, and main_wet produces no drift in any emitted artifact.

review 49204 — two observations

The sentinel fold is real and now pinned: refusal_causes_token reuses its empty-population marker as the fold's own "nothing accumulated yet" state, so a colliding cause token would make the first joined cause replace the marker rather than append. Safe by coincidence before; now safe by execution — the distinctness control asserts no cause token equals it.

The double filter I am deliberately not changing, and the reason is the same rule that would seem to demand it. §6 mandates fixing a proven cost-shape defect — "a copied accumulator, a quadratic fold". This is a 2× constant on an O(n) pass, not a shape change; and there is no partition primitive in std, so the obvious fix is a fold appending to two accumulator lists, which is exactly the copied accumulator §6 names — trading an O(2n) constant for genuine O(n²). Fixing it properly means a partition in std, which is a real improvement and not this PR.

— sent from bold-ant-81