diff --git a/dag/gunbc/runner/runner_bound_attempt_receipt.dag b/dag/gunbc/runner/runner_bound_attempt_receipt.dag index 483c49caf6f..cff6bd29fbd 100644 --- a/dag/gunbc/runner/runner_bound_attempt_receipt.dag +++ b/dag/gunbc/runner/runner_bound_attempt_receipt.dag @@ -2,7 +2,9 @@ module gunbc.runner.runner_bound_attempt_receipt import std.types { Bool, Int, List, NonEmptyStr, String } import std.dissolution { dissolution_description } -import gunbc.runner_jit_mint { plan_jit_mint_consumer_frontier } +import gunbc.runner.runner_jit_perform { + jit_mint_effect_transport_frontier, host_side_jit_fetch_deletion_frontier, +} import gunbc.runner.runner_jit_admission { ExpiryAxis, JitAdmissionAxis, axis_mint_observability, MintExpiresAtCoverage, MintUnobservableDeclaredBoundary, @@ -161,7 +163,8 @@ data still_open: List = concat( concat( still_open_from_live_census(census: duplicate_jitconfig_name_409_coverage), [ - dissolution_description(condition: plan_jit_mint_consumer_frontier) as NonEmptyStr, + dissolution_description(condition: jit_mint_effect_transport_frontier) as NonEmptyStr, + dissolution_description(condition: host_side_jit_fetch_deletion_frontier) as NonEmptyStr, dissolution_description(condition: host_image_placeability_wet_probe_frontier) as NonEmptyStr, placeability_standing_open_item(outcome: host_image_placeability_standing), "host init still prints these axes as unchecked; standing is gunbc.runner.runner_jit_admission, not this receipt", diff --git a/dag/gunbc/runner/runner_jit_mint.dag b/dag/gunbc/runner/runner_jit_mint.dag index 9cdefbed97b..ae6ccb5b5d0 100644 --- a/dag/gunbc/runner/runner_jit_mint.dag +++ b/dag/gunbc/runner/runner_jit_mint.dag @@ -2,7 +2,6 @@ module gunbc.runner_jit_mint import std.types { String, NonEmptyStr, Bool, Int, List } import std.disposition { Disposition, SingleAuthority } -import std.dissolution { DissolutionCondition, unbound_dissolution } import extdeps.github.effect { GitHubEffect, GenerateOrganizationJitConfig, GitHubOrganizationRef } import extdeps.github.actions_jit_runner { JitRunnerConfigRequest, JitRunnerName, JitRunnerGroupId, JitRunnerLabel, JitWorkFolder, @@ -22,10 +21,6 @@ import gunbc.runner_microvm_attempt { data runner_jit_mint_disposition: Disposition = SingleAuthority -// §3c: plan_jit_mint IS NOT CALLED FROM PRODUCTION YET. Witnesses exercise the refusals; the -// named later consumer is the mint performer that posts generate-jitconfig from JitMintAuthorized. -data plan_jit_mint_consumer_frontier: DissolutionCondition = unbound_dissolution(description: "NAMED CONSUMER: gunbc.runner.runner_jit_perform (or successor) calls plan_jit_mint and posts generate-jitconfig from JitMintAuthorized. TRIGGER: that import and call exist. SUFFICIENT FOR deleting this row. NOT satisfied by another witness importing plan_jit_mint." as NonEmptyStr) - // THE MINT IS PLANNED, NOT PERFORMED, AND THE SPLIT IS THE POINT. // // Two facts have to be true before a credential exists at all: the cell must be OWNED (otherwise a diff --git a/dag/gunbc/runner/runner_jit_perform.dag b/dag/gunbc/runner/runner_jit_perform.dag new file mode 100644 index 00000000000..8a71e526ae8 --- /dev/null +++ b/dag/gunbc/runner/runner_jit_perform.dag @@ -0,0 +1,268 @@ +module gunbc.runner.runner_jit_perform + +import std.types { String, NonEmptyStr, Bool, Int, List } +import std.disposition { Disposition, SingleAuthority } +import std.dissolution { DissolutionCondition, unbound_dissolution } +import extdeps.github.app { GitHubAppInstallationId } +import extdeps.github.effect { GitHubOrganizationRef } +import extdeps.github.actions_jit_runner { + JitRunnerConfigRequest, JitRunnerGroupId, JitRunnerLabel, EncodedJitConfig, + JitConfigMintOutcome, JitConfigMinted, JitConfigMintRefused, JitConfigMintNotFound, + JitConfigMintConflict, JitConfigMintValidationFailed, +} +import extdeps.github.org_admin_auth { github_app_installation_access_token_url } +import gunbc.auth.github_apps { GitHubAppControlPlaneState } +import gunbc.auth.github_credential { + GitHubCredentialAuthority, ActionsJobCredential, ManagedAppInstallationCredential, + CredentialCapability, +} +import gunbc.runner.runner_jit_admission { JitAdmissionAxisStanding } +import gunbc.runner_microvm_attempt { MicroVmAttempt, MicroVmCellBinding } +import gunbc.runner_jit_mint { + JitMintPlan, JitMintAuthorized, JitMintRefusedCellNotOwned, JitMintRefusedCredential, + JitMintRefusedAttemptUnbound, plan_jit_mint, +} + +data runner_jit_perform_disposition: Disposition = SingleAuthority + +// THIS MODULE IS THE NAMED CONSUMER OF gunbc.runner_jit_mint.plan_jit_mint, and landing it is what +// deleted that module's consumer frontier. It performs no I/O and claims none: the two folds below +// sit on either side of a transport this repository does not yet have, and the frontier at the foot +// of this module says so rather than letting a green witness read as a working mint. +// +// THE DIRECTION IS PUSH, AND THAT IS THE WHOLE POINT OF SPLITTING THE FOLD IN TWO. +// +// The gap this addresses (gunbc#10733) is that a host fetches its JIT config from an endpoint on +// the segment, so whichever host reaches it first takes the registration. The repair is not a better +// endpoint: it is that no endpoint exists to ask. A credential is minted control-plane-side, against +// a cell whose ownership was already proven, and its only destination is the drive path the proving +// arm itself named. +// +// So the ordering has to be unwritable rather than documented. dispatch_jit_mint is the only way to +// obtain a JitMintDispatchAuthorized, and it produces one only from JitMintAuthorized -- which +// gunbc.runner_jit_mint produces only after BOTH cell ownership and the credential's organization +// self-hosted-runners write capability hold. receive_jit_mint then requires that value to reach a +// delivered credential. A caller therefore cannot mint first and prove ownership afterwards: the +// value that names where the credential may go does not exist until both facts are established. +// +// A SINGLE FOLD TAKING THE MINT OUTCOME AS A PARAMETER WOULD HAVE INVERTED EXACTLY THAT. Its +// caller would have had to call GitHub before the fold ran, which is mint-first-check-after with +// the check moved after the spend -- the ordering gunbc.runner_jit_mint exists to make unwritable. +// +// THE INSTALLATION TOKEN IS NAMED, NEVER CARRIED. The dispatch holds the URL that mints the +// installation access token and does not hold the token; nothing in this module has a field a +// bearer secret could occupy. gunbc.credential_argv_exposure measures what this fleet already paid +// for rendering a credential into a place other processes can read, and a token field here would be +// that class re-opened one layer up from the argv it warns about. + +// WHY THE REFUSALS ARE RE-PROJECTED RATHER THAN PASSED THROUGH AS A JitMintPlan. +// +// The decision stays in gunbc.runner_jit_mint and is not re-derived here -- these arms report which +// PLANNED refusal stopped the push, carrying that arm's own payload unchanged. Passing the plan +// itself would make JitMintAuthorized representable inside a value whose name says nothing was +// dispatched, which is a writable contradiction (DESIGN §4b). The projection is produced by an +// exhaustive match on JitMintPlan, so a new plan arm fails to compile here rather than falling into +// a default that silently reports the wrong cause. +type JitDispatchRefusal + = DispatchRefusedCellNotOwned { cause: String } + | DispatchRefusedCredential { + organization: NonEmptyStr + unsatisfied: List + } + | DispatchRefusedAttemptUnbound { cause: String } + | DispatchRefusedNoInstallationCredential { cause: String } + +// THE FOURTH REFUSAL IS A TOTALITY ARM AND IS DELIBERATELY NOT ENROLLED AS COVERAGE. +// +// The mint is the two-step App path gunbc.runner.runner_jit_admission names: an installation access +// token, then generate-jitconfig with it. Step one presupposes an INSTALLATION, and the fold must +// say what it does when the authorized credential names none -- so the arm exists, and it refuses +// rather than reaching for some other credential, which would be the absorbing fallback DESIGN §5 +// forbids and would put a job-scoped token where an installation token belongs. +// +// NO WITNESS ASSERTS IT, BECAUSE NO INPUT REACHES IT. The only authority without an installation is +// ActionsJobCredential, and extdeps.github.actions_token maps OrganizationSelfHostedRunnersAxis to +// IntrinsicTokenGrantAbsent, hence ActionsGrantScopeUnavailable and CredentialKindCannotSatisfy -- +// so such a credential is refused by plan_jit_mint's own credential join before this branch is +// reached, 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 here as a totality arm and counted as none. +type JitMintDispatch + = JitMintDispatchAuthorized { + attempt: MicroVmAttempt + installation_token_url: String + endpoint_path: String + request: JitRunnerConfigRequest + drive_destination: String + } + | JitMintDispatchRefused { refusal: JitDispatchRefusal } + +fn authority_installation(authority: GitHubCredentialAuthority) -> GitHubAppInstallationId? { + match authority { + ActionsJobCredential { grant: _ } => none + ManagedAppInstallationCredential { app: _, installation: i, profile: _ } => Present { value: i } + } +} + +fn dispatch_jit_mint( + binding: MicroVmCellBinding, + authority: GitHubCredentialAuthority, + control_plane: GitHubAppControlPlaneState, + organization: GitHubOrganizationRef, + runner_group_id: JitRunnerGroupId, + labels: List, + attempt_binding: JitAdmissionAxisStanding +) -> JitMintDispatch { + match plan_jit_mint( + binding: binding, + authority: authority, + control_plane: control_plane, + organization: organization, + runner_group_id: runner_group_id, + labels: labels, + attempt_binding: attempt_binding, + ) { + JitMintRefusedCellNotOwned { cause: c } => + JitMintDispatchRefused { refusal: DispatchRefusedCellNotOwned { cause: c } } + JitMintRefusedAttemptUnbound { cause: c } => + JitMintDispatchRefused { refusal: DispatchRefusedAttemptUnbound { cause: c } } + JitMintRefusedCredential { organization: org, unsatisfied: u } => + JitMintDispatchRefused { + refusal: DispatchRefusedCredential { organization: org, unsatisfied: u }, + } + JitMintAuthorized { + attempt: attempt, + endpoint_path: path, + request: request, + drive_destination: destination, + } => + match authority_installation(authority: authority) { + Absent => + JitMintDispatchRefused { + refusal: DispatchRefusedNoInstallationCredential { + cause: "the authorized credential names no App installation, so no installation access token can be minted and the two-step generate-jitconfig path cannot be taken", + }, + } + Present { value: installation } => + JitMintDispatchAuthorized { + attempt: attempt, + installation_token_url: github_app_installation_access_token_url( + installation_id: installation.value, + ), + endpoint_path: path, + request: request, + drive_destination: destination, + } + } + } +} + +// THE DELIVERY IS WHERE THE CREDENTIAL AND ITS DESTINATION BECOME INSEPARABLE. +// +// An EncodedJitConfig is obtainable from this module only alongside the drive path the ownership +// proof produced, so there is no value here that hands a caller a credential it may send anywhere +// it likes. That is the structural form of "there is no endpoint a host may ask": the credential is +// not addressable independently of the attempt it belongs to. +// +// THE NOT-CREATED ARM CARRIES GitHub's OWN OUTCOME VALUE UNCHANGED. Re-coining upstream's four +// failure shapes here would be a second authority for what GitHub answered (DESIGN §3), and those +// shapes are upstream's to change. The cost is stated rather than hidden: JitConfigMinted is +// representable inside an arm whose name says nothing was created. This fold never constructs that +// state -- the match below sends every minted outcome to the delivered arm -- so the class sits at +// mitigatable, and its next-rung trigger is a substrate capability for naming a sum minus one of +// its arms, which does not exist today. Duplicating the vocabulary to reach rung four would trade a +// state no fold writes for a fork that drifts. +type JitCredentialDelivery + = JitCredentialBoundToDrive { + attempt: MicroVmAttempt + drive_destination: String + credential: EncodedJitConfig + runner_id: Int + } + | JitCredentialNotDispatched { refusal: JitDispatchRefusal } + | JitCredentialMintNotCreated { outcome: JitConfigMintOutcome } + +fn receive_jit_mint( + dispatch: JitMintDispatch, + outcome: JitConfigMintOutcome +) -> JitCredentialDelivery { + match dispatch { + JitMintDispatchRefused { refusal: r } => JitCredentialNotDispatched { refusal: r } + JitMintDispatchAuthorized { + attempt: attempt, + installation_token_url: _, + endpoint_path: _, + request: _, + drive_destination: destination, + } => + match outcome { + JitConfigMinted { config: config, runner_id: runner_id } => + JitCredentialBoundToDrive { + attempt: attempt, + drive_destination: destination, + credential: config, + runner_id: runner_id, + } + JitConfigMintRefused { status: s, reason: reason } => + JitCredentialMintNotCreated { + outcome: JitConfigMintRefused { status: s, reason: reason }, + } + JitConfigMintNotFound { reason: reason } => + JitCredentialMintNotCreated { outcome: JitConfigMintNotFound { reason: reason } } + JitConfigMintConflict { reason: reason } => + JitCredentialMintNotCreated { outcome: JitConfigMintConflict { reason: reason } } + JitConfigMintValidationFailed { reason: reason } => + JitCredentialMintNotCreated { + outcome: JitConfigMintValidationFailed { reason: reason }, + } + } + } +} + +fn jit_credential_delivered(delivery: JitCredentialDelivery) -> Bool { + match delivery { + JitCredentialBoundToDrive { + attempt: _, + drive_destination: _, + credential: _, + runner_id: _, + } => true + JitCredentialNotDispatched { refusal: _ } => false + JitCredentialMintNotCreated { outcome: _ } => false + } +} + +// §3c: THESE FOLDS ARE NOT EXECUTED BY PRODUCTION, AND SAYING SO IS THE POINT OF THIS ROW. +// +// What stands between them is a transport: nothing in gunbc performs a GitHubEffect. A census of +// the corpus finds GitHubEffect in exactly two places -- gunbc.auth.github_credential, which +// decides authorization, and gunbc.runner_jit_mint, which plans -- and no realization anywhere +// posts either step of this path. So the witnesses enrolled for this module are FIXTURE-ONLY and +// establish the fold's discrimination, never that a credential has ever been minted this way. +// +// The trigger names the CAPABILITY rather than an artifact, because a trigger naming less than the +// capability is satisfied while the capability stays dead (DESIGN §4b(3)). What is required is a +// realization that PERFORMS a GitHubEffect and returns its typed outcome, sufficient for +// receive_jit_mint to be reached with a JitConfigMintOutcome that GitHub produced. A curl argv is +// not that capability and would not discharge this row: the installation token would ride in an +// argv, which is the exposure gunbc.credential_argv_exposure already measures, so the effect +// realization this names is blocked behind the declared input TYPE on v2.std.operation_argv +// ShellTransportOperationRow that extdeps.github.actions_jit_runner names for the same reason. +data jit_mint_effect_transport_frontier: DissolutionCondition = unbound_dissolution(description: "NAMED CONSUMER: a realization that performs a GitHubEffect and returns JitConfigMintOutcome, reaching receive_jit_mint with an outcome GitHub produced. TRIGGER: that realization exists and this module's delivery is executed through it. SUFFICIENT FOR deleting this row. NOT satisfied by a witness, nor by an argv-rendered token, which re-opens gunbc.credential_argv_exposure." as NonEmptyStr) + +// §3c: THE HOST-SIDE FETCH IS STILL STANDING AND THIS CHANGE DID NOT DELETE IT. +// +// An inverted push with the pull still reachable is TWO authorities for one credential, and the +// segment race survives in the one that is still answerable -- so this row exists to keep the +// deletion countable rather than to imply it happened. It was not attempted here because the fetch +// has no subject in source control: docs/plans/microvm-launch-displacement-analysis.md establishes, +// by a code search carried with a positive 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_store records as not resilient, with no +// source to rebuild it from, and that document routes recovering it to the operator as an +// accepted-risk decision rather than a lane's choice. +// +// So the trigger is the recovery, not this module: no amount of pushing closes a pull that is still +// listening. +data host_side_jit_fetch_deletion_frontier: DissolutionCondition = unbound_dissolution(description: "NAMED SUCCESSOR: the Mt. Collins host boot path stops fetching a JIT credential, and no endpoint on the segment serves one. TRIGGER: the boot script is recovered into source control and the fetch is deleted from it, SUFFICIENT FOR the pull surface being gone rather than merely unused. NOT satisfied by this module's push existing beside it." as NonEmptyStr) diff --git a/dag/test/claim/github_app_registry_witness_test.dag b/dag/test/claim/github_app_registry_witness_test.dag index 55ecc558124..fd962955956 100644 --- a/dag/test/claim/github_app_registry_witness_test.dag +++ b/dag/test/claim/github_app_registry_witness_test.dag @@ -13,8 +13,11 @@ import gunbc.runner_microvm_attempt { MicroVmCellBinding, VmUnboundCellNotOwned, MicroVmAttemptResult, MicroVmAttemptAccepted, MicroVmAttemptRefused, microvm_attempt, bind_owned_attempt, runner_microvm_attempt_unit_name, + runner_microvm_attempt_jit_drive_path, +} +import extdeps.github.actions_jit_runner { + JitRunnerGroupId, JitRunnerLabel, JitConfigMintOutcome, jit_config_mint_outcome, } -import extdeps.github.actions_jit_runner { JitRunnerGroupId, JitRunnerLabel } import gunbc.runner.runner_jit_admission { jit_admission_axis_standing, AttemptBindingAxis, AxisDeferred, } @@ -23,6 +26,15 @@ import gunbc.runner_jit_mint { JitMintRefusedAttemptUnbound, plan_jit_mint, } +import gunbc.runner.runner_jit_perform { + JitMintDispatch, JitMintDispatchAuthorized, JitMintDispatchRefused, + JitDispatchRefusal, DispatchRefusedCellNotOwned, DispatchRefusedCredential, + DispatchRefusedAttemptUnbound, + JitCredentialDelivery, JitCredentialBoundToDrive, JitCredentialNotDispatched, + JitCredentialMintNotCreated, + dispatch_jit_mint, receive_jit_mint, jit_credential_delivered, +} + import extdeps.uri { Uri, uri_https } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -1017,3 +1029,163 @@ test fn witness_jit_mint_refuses_when_attempt_binding_is_deferred() -> Bool { _ => false } } + +// --------------------------------------------------------------------------------------------- +// JIT MINT DISPATCH AND DELIVERY. gunbc.runner.runner_jit_perform is the consumer that closed +// plan_jit_mint's frontier, and these witnesses are FIXTURE-ONLY BY CONSTRUCTION: nothing in gunbc +// performs a GitHubEffect, so no input here was produced by GitHub. What they establish is that the +// fold discriminates -- and, in the delivery arms, that a credential cannot be obtained apart from +// the drive destination the ownership proof named. They establish nothing about a live mint, and +// runner_jit_perform's own transport frontier is what records that. + +fn dispatched(owned: Bool, perms: List) -> JitMintDispatch { + dispatch_jit_mint( + binding: jit_binding(owned: owned), + authority: app_credential, + control_plane: observed_grant(perms: perms), + organization: gunbai_org_ref, + runner_group_id: JitRunnerGroupId { value: 1 }, + labels: [JitRunnerLabel { value: "self-hosted" }], + attempt_binding: jit_admission_axis_standing(axis: AttemptBindingAxis), + ) +} + +// A MINTED 201 IS THE ONLY OUTCOME THAT MAY DELIVER, and it is built through upstream's own +// outcome fold rather than by constructing JitConfigMinted here -- a fixture that assembled the +// success arm directly would keep passing if that fold stopped recognising a 201. +data minted_outcome: JitConfigMintOutcome = jit_config_mint_outcome( + status: 201, + encoded: "ZmFrZS1qaXQtY29uZmln", + runner_id: 4242, + error_body: "", +) + +data conflicting_outcome: JitConfigMintOutcome = jit_config_mint_outcome( + status: 409, + encoded: "", + runner_id: 0, + error_body: "a runner with this name already exists", +) + +// RED 1 -- AN UNOWNED CELL REFUSES BEFORE ANY CREDENTIAL IS NAMED. The credential here is fully +// sufficient, so a dispatcher that consulted it first would name an installation token URL for a +// cell this host does not own, which is a live runner identity minted against someone else's +// resources. The refusal must come from the cell, and it must carry the cell's own cause. +test fn witness_jit_dispatch_refuses_an_unowned_cell_before_naming_a_token_url() -> Bool { + match dispatched(owned: false, perms: runner_grant) { + JitMintDispatchRefused { refusal: DispatchRefusedCellNotOwned { cause: c } } => + string_contains(s: c, pattern: "not owned") + _ => false + } +} + +// RED 2 -- A CREDENTIAL WITHOUT organization self-hosted-runners write REFUSES, cell owned, so the +// permission join is the only thing that can produce it. The unsatisfied list must survive the +// projection: collapsing it to a bare cause would erase which capability was missing, and that is +// the whole content of the refusal. +test fn witness_jit_dispatch_refuses_a_credential_missing_the_runner_permission() -> Bool { + match dispatched(owned: true, perms: full_workflow_grant) { + JitMintDispatchRefused { + refusal: DispatchRefusedCredential { organization: org, unsatisfied: u }, + } => (org as String) == "gunb-ai" && count(u) > 0 + _ => false + } +} + +// RED 3 -- AN UNBOUND ATTEMPT REFUSES. A deferred attempt-binding standing means the mint name +// would not be the attempt's identity, so the credential could not be reconciled to a host. Cell +// and credential are both good here, so nothing else can produce this arm. +test fn witness_jit_dispatch_refuses_when_the_attempt_binding_is_deferred() -> Bool { + match dispatch_jit_mint( + binding: jit_binding(owned: true), + authority: app_credential, + control_plane: observed_grant(perms: runner_grant), + organization: gunbai_org_ref, + runner_group_id: JitRunnerGroupId { value: 1 }, + labels: [JitRunnerLabel { value: "self-hosted" }], + attempt_binding: AxisDeferred { + trigger: "fixture: deferred standing must refuse a dispatch that would not carry the attempt identity" as NonEmptyStr, + }, + ) { + JitMintDispatchRefused { refusal: DispatchRefusedAttemptUnbound { cause: _ } } => true + _ => false + } +} + +// POSITIVE CONTROL. Without it the three reds above are satisfied by a dispatcher that refuses +// unconditionally. It also pins the two-step shape: the installation token URL is derived from the +// credential's own installation id rather than spelled, and the second step is the org-derived +// generate-jitconfig path, so a dispatch cannot address another organization's runners. +test fn witness_jit_dispatch_authorizes_and_names_both_steps_of_the_app_path() -> Bool { + match dispatched(owned: true, perms: runner_grant) { + JitMintDispatchAuthorized { + attempt: a, + installation_token_url: token_url, + endpoint_path: path, + request: req, + drive_destination: dest, + } => + token_url == "https://api.github.com/app/installations/999/access_tokens" + && path == "/orgs/gunb-ai/actions/runners/generate-jitconfig" + && (req.name.value as String) == (runner_microvm_attempt_unit_name(attempt: a) as String) + && string_contains(s: dest, pattern: "/jit.img") + _ => false + } +} + +// RED 4 -- A REFUSED DISPATCH CANNOT DELIVER A CREDENTIAL EVEN WHEN GITHUB MINTED ONE. +// +// This is the arm the inversion exists for. The mint outcome here is a real 201 carrying a +// credential, and the cell is not owned: a delivery that consulted the outcome alone would write a +// live credential to a destination no ownership proof produced, which is the segment race moved +// inside the process. The refusal must survive, and it must still say WHICH refusal it was. +test fn witness_a_refused_dispatch_delivers_nothing_even_from_a_minted_credential() -> Bool { + let delivery = receive_jit_mint( + dispatch: dispatched(owned: false, perms: runner_grant), + outcome: minted_outcome, + ) + !jit_credential_delivered(delivery: delivery) + && match delivery { + JitCredentialNotDispatched { refusal: DispatchRefusedCellNotOwned { cause: _ } } => true + _ => false + } +} + +// RED 5 -- A NON-201 IS A REFUSAL AND NOT AN EMPTY CREDENTIAL. An authorized dispatch whose mint +// conflicted must not deliver: a guest handed an empty drive boots healthy and sits waiting for +// work it can never be assigned, burning its whole deadline. +test fn witness_an_authorized_dispatch_delivers_nothing_when_the_mint_was_not_created() -> Bool { + let delivery = receive_jit_mint( + dispatch: dispatched(owned: true, perms: runner_grant), + outcome: conflicting_outcome, + ) + !jit_credential_delivered(delivery: delivery) + && match delivery { + JitCredentialMintNotCreated { outcome: _ } => true + _ => false + } +} + +// DELIVERY POSITIVE CONTROL, and it pins the property the push direction rests on: the credential +// is reachable ONLY beside the attempt's own drive destination. There is no value in this module's +// vocabulary that hands a caller a credential it may address anywhere else, which is the structural +// form of "there is no endpoint a host may ask". +test fn witness_a_minted_credential_is_bound_to_the_attempts_own_drive_destination() -> Bool { + let delivery = receive_jit_mint( + dispatch: dispatched(owned: true, perms: runner_grant), + outcome: minted_outcome, + ) + jit_credential_delivered(delivery: delivery) + && match delivery { + JitCredentialBoundToDrive { + attempt: a, + drive_destination: dest, + credential: c, + runner_id: id, + } => + dest == runner_microvm_attempt_jit_drive_path(attempt: a) + && (c.encoded as String) == "ZmFrZS1qaXQtY29uZmln" + && id == 4242 + _ => false + } +}