Repository navigation
The JIT credential is planned against a proven cell and bound to that attempt's drive - #10924
Merged
Merged
Conversation
… attempt's drive gunbc.runner.runner_jit_perform is the named consumer plan_jit_mint's frontier was waiting for, so that row is deleted and runner_bound_attempt_receipt's still_open is rewired to its two successors. dispatch_jit_mint calls plan_jit_mint and, only from JitMintAuthorized, names both steps of the App path runner_jit_admission cites: the installation access token URL, derived from the credential's own installation id via extdeps.github.org_admin_auth, then the org-derived generate-jitconfig path carrying JitRunnerConfigRequest and nothing else. receive_jit_mint requires that authorized value to reach a credential at all. THE SPLIT INTO TWO FOLDS IS LOAD-BEARING. A single fold taking the mint outcome as a parameter would force its caller to call GitHub before ownership was proven, which is mint-first-check-after with the check moved after the spend -- the ordering runner_jit_mint exists to make unwritable. The value naming a drive destination does not exist until both the cell proof and the credential join have held. The installation token is named, never carried: no field here can hold a bearer secret. FIXTURE-ONLY REDS, STATED IN THOSE WORDS. Nothing in gunbc performs a GitHubEffect, so no input to these witnesses was produced by GitHub. Seven witnesses execute -- three dispatch refusals, two delivery refusals, and two positive controls -- and a mutation probe rewiring the cell-not-owned arm flipped the unowned-cell red and the refused-dispatch delivery red from true to false, so they discriminate rather than agree with themselves. The rung established on the delivery path is mitigatable. Nothing here establishes a live mint, and jit_mint_effect_transport_frontier records that. The fourth dispatch refusal is a totality arm with no witness: an ActionsJobCredential is the only authority without an installation, and actions_token maps OrganizationSelfHostedRunnersAxis to IntrinsicTokenGrantAbsent, so plan_jit_mint's credential join refuses it before that branch for every input including a fixture's. Its RED is not authorable where the check runs, so a witness over it would be permanently green and would be cited as coverage. THE HOST-SIDE FETCH IS STILL STANDING AND THIS DOES NOT DELETE IT. host_side_jit_fetch_deletion_frontier keeps that countable rather than implied: the fetch has no subject in source control, since the Mt. Collins host boot script is authored in no repository and exists as bytes inside a host image the store records as not resilient. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NWq1zh6gM6ebLqNhFwHcx5
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes the
plan_jit_mintconsumer frontier by landing its named consumer,gunbc.runner.runner_jit_perform. Item 1 of the jit-auth brief, per the ruling on this lane;items 2 and 3 are explicitly not in this PR and are accounted for below.
What it does
dispatch_jit_mintcallsplan_jit_mintand, only fromJitMintAuthorized, names both steps ofthe App path
gunbc.runner.runner_jit_admissioncites:extdeps.github.org_admin_auth.github_app_installation_access_token_urlgenerate-jitconfigpath, carryingJitRunnerConfigRequestand nothing elsereceive_jit_mintthen requires that authorized value to reach a credential at all.The split into two folds is load-bearing, not stylistic. A single fold taking the mint outcome
as a parameter would force its caller to call GitHub before ownership was proven — mint-first,
check-after, with the check moved after the spend, which is the ordering
gunbc.runner_jit_mintexists to make unwritable. The value that names a drive destination does not exist until both the
cell-ownership proof and the credential join have held.
The installation token is named, never carried: no field in this module can hold a bearer
secret, which is
gunbc.credential_argv_exposure's class one layer up from the argv it measures.The delivery side is where the push direction becomes structural: an
EncodedJitConfigisobtainable from this module only alongside the drive path the ownership proof produced. That is
the modeled form of "there is no endpoint a host may ask" — the credential is not addressable
independently of the attempt it belongs to.
The reds are fixture-only, in those words
Nothing in gunbc performs a
GitHubEffect, so no input to these witnesses was produced byGitHub. A census of the corpus finds
GitHubEffectin exactly two places —gunbc.auth.github_credential,which decides authorization, and
gunbc.runner_jit_mint, which plans. These witnesses establishthat the fold discriminates. They establish nothing about a live mint.
The rung established on the delivery path is
mitigatable. Not preventable, and this PR doesnot claim the credential path is closed.
jit_mint_effect_transport_frontierrecords the gap andnames the capability required to discharge it — a realization that performs a
GitHubEffectandreturns its typed outcome — rather than an artifact, since a trigger naming less than the capability
is satisfied while the capability stays dead (DESIGN §4b(3)).
Seven witnesses execute, in
test.claim.github_app_registry— which already owns every credentialfixture, so no second control-plane authority is built next door:
truefalsetruetruetruetruefalsetruetrueThe mutation column is what makes the greens worth reading. Rewiring the
JitMintRefusedCellNotOwnedarm to reportDispatchRefusedAttemptUnboundflipped RED 1 and RED 4to
false; the file restored byte-identical afterwards (md5 verified). Without that, a green onlysays the fold agrees with itself.
Re-derive:
gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/github_app_registry_witness_test.dag --function <name>— the refusal messagecarries the
Bool. Run from a tree-built binary, not the baked pin; mine was verified current onthe §4c annotation axis first.
RED 4 is the arm the inversion exists for: the mint outcome is a real 201 carrying a credential and
the cell is not owned. A delivery consulting the outcome alone would write a live credential to a
destination no ownership proof produced — the segment race moved inside the process.
One arm carries no coverage, deliberately
The fourth dispatch refusal (
DispatchRefusedNoInstallationCredential) is a totality arm with nowitness. The only authority without an installation is
ActionsJobCredential, andextdeps.github.actions_tokenmapsOrganizationSelfHostedRunnersAxistoIntrinsicTokenGrantAbsent→
ActionsGrantScopeUnavailable→CredentialKindCannotSatisfy— so such a credential is refused byplan_jit_mint's own credential join before that branch, for every input including a fixture's.DESIGN §4b says to ask whether a check's RED is authorable before writing the check. This one's
is not authorable anywhere the check can run, so a witness over it would be permanently green by
construction and worse than absent, because it would be cited as coverage. It is recorded as a
totality arm and counted as none.
What this PR does NOT do
The host-side fetch is still standing. An inverted push with the pull still reachable is two
authorities for one credential, and the segment race survives in the one still answerable — so
host_side_jit_fetch_deletion_frontierkeeps the deletion countable rather than implied.It was not attempted because the fetch has no subject in source control.
docs/plans/microvm-launch-displacement-analysis.mdestablishes, by a code search carried with apositive control and a per-repository reachability control, that the Mt. Collins host boot script is
authored in no repository: it exists as bytes inside a host image under the store
gunbc.runner.runner_host_image_storerecords asresilient: false, with no source to rebuild from.That document routes recovering it to the operator as an accepted-risk decision. The trigger is that
recovery, not this module — no amount of pushing closes a pull that is still listening.
Metered vCPU-minute receipts and same-transaction teardown are separate items and are untouched.
ReplayAxisremainsAxisDeferredwith its stated trigger. This PR claims no replay protection.Relationship to #10923
No dependency is taken on it, merged or not. #10923 (
gunbc.github_effect_perform) is the otherhalf of this path — it performs, this module decides — and it deliberately did not wire
plan_jit_mint. If it lands,jit_mint_effect_transport_frontieris discharged by the capabilityarriving and the fixture-only caveat narrows in a successor PR; nothing here needs rewriting either
way. I have not inspected its wet witnesses and make no claim about whether they ran — whoever wires
the two halves owns checking the witness footer reports them executing before describing the path as
real, since a batch entry with no functions runs zero witnesses and exits 0.
🤖 Generated with Claude Code
https://claude.ai/code/session_01NWq1zh6gM6ebLqNhFwHcx5