diff --git a/dag/extdeps/github/git_database.dag b/dag/extdeps/github/git_database.dag index cb0e4f68918..fa0dd1869db 100644 --- a/dag/extdeps/github/git_database.dag +++ b/dag/extdeps/github/git_database.dag @@ -38,6 +38,8 @@ type GitRefObjectWire { sha: String } +type GitRefDeletedBody {} + type GitRefWire { ref: String object: GitRefObjectWire @@ -111,10 +113,21 @@ data git_blob_encoding_base64: NonEmptyStr = "base64" // so no caller of UpdateRefFastForward can express a forced update; a moved branch answers 422 // "Update is not a fast forward" and that refusal IS the compare-and-swap. A forced variant would be // a different operation with its own name and its own consumer. +// CreateRef AND DeleteRef (docs.github.com/en/rest/git/refs#create-a-reference and +// #delete-a-reference, read 2026-10-04). CreateRef takes the FULL ref name (`refs/tags/`) in its +// body and answers 201 with the reference; an existing ref answers 422 "Reference already exists", +// so creation never moves a ref and that 422 is the create-once refusal. DeleteRef takes the +// `tags/` form in its path and answers 204 with no body; a ref already gone answers 422 +// "Reference does not exist". Their consumer is gunbc.runner.runner_qualification_ref_pin (a create-once branch per qualification attempt and its removal). +// +// THE BEARER IS AN INPUT WHEN ONE IS GIVEN. Every operation already took `auth_token`; the service read +// only GITHUB_TOKEN. Declaring both lets a caller that holds an installation token present it, and a +// caller passing "" (gunbc.heal_publication) falls through to GITHUB_TOKEN exactly as before. service github.GitDatabase { config { endpoint: default_api_base auth: Bearer + auth_input: auth_token auth_source: EnvVar { name: "GITHUB_TOKEN" } } @@ -306,4 +319,58 @@ service github.GitDatabase { 5xx => GitHubErrorShape } } + + operation CreateRef { + requires Network + input { + auth_token: Secret + owner: String + repo: String + full_ref: String + sha: String + } + output { + reference: GitRefWire + } + transport rest { + method: POST, + path: "/repos/\{owner\}/\{repo\}/git/refs", + body: { ref: full_ref, sha: sha } + } + response { + 201 => GitRefWire + 401 => GitHubErrorShape + 403 => GitHubErrorShape + 404 => GitHubErrorShape + 409 => GitHubErrorShape + 422 => GitHubErrorShape + 5xx => GitHubErrorShape + } + } + + operation DeleteRef { + requires Network + input { + auth_token: Secret + owner: String + repo: String + ref: String + } + output { + result: GitRefDeletedBody + } + transport rest { + method: DELETE, + path: "/repos/\{owner\}/\{repo\}/git/refs/\{ref\}" + } + response { + 204 => GitRefDeletedBody + 401 => GitHubErrorShape + 403 => GitHubErrorShape + 404 => GitHubErrorShape + 409 => GitHubErrorShape + 422 => GitHubErrorShape + 5xx => GitHubErrorShape + } + } } diff --git a/dag/extdeps/github/org_actions.dag b/dag/extdeps/github/org_actions.dag index cf0a08e88b1..286880ccdd7 100644 --- a/dag/extdeps/github/org_actions.dag +++ b/dag/extdeps/github/org_actions.dag @@ -130,6 +130,16 @@ type OrgRunnerGroupListWire { data org_runner_groups_max_per_page: Int = 100 +// UpdateOrganizationRunnerGroupWorkflows: +// update a self-hosted runner group for an organization (docs.github.com/en/rest/actions/ +// self-hosted-runner-groups#update-a-self-hosted-runner-group-for-an-organization, REST +// 2022-11-28, read 2026-10-04): PATCH sets restricted_to_workflows and selected_workflows and +// answers 200 with the group. Each selected entry is `//@`; per +// docs.github.com/en/enterprise-cloud@latest/actions/how-tos/manage-runners/self-hosted-runners/ +// manage-access (read 2026-10-04), "Pin non-reusable workflows to a branch. Pin reusable +// workflows to a branch, tag, or full SHA" -- a dispatched (non-reusable) workflow is selectable +// only at a branch, which is why a qualification pin is a branch and not a SHA. Its consumer is +// gunbc.runner.runner_qualification_ref_pin, which writes only the dedicated qualification group. service github.OrgRunnerGroupsRest { config { endpoint: default_api_base @@ -161,4 +171,30 @@ service github.OrgRunnerGroupsRest { 5xx => GitHubErrorShape } } + + operation UpdateOrganizationRunnerGroupWorkflows { + requires Network + input { + installation_token: Secret + org: NonEmptyStr + runner_group_id: Int + selected_workflows: List + } + output { + result: OrgRunnerGroupWire + } + transport rest { + method: PATCH, + path: "/orgs/\{org\}/actions/runner-groups/\{runner_group_id\}", + body: { restricted_to_workflows: true, selected_workflows: selected_workflows } + } + response { + 200 => OrgRunnerGroupWire + 401 => GitHubErrorShape + 403 => GitHubErrorShape + 404 => GitHubErrorShape + 422 => GitHubErrorShape + 5xx => GitHubErrorShape + } + } } diff --git a/dag/extdeps/github/workflow_runs.dag b/dag/extdeps/github/workflow_runs.dag index 7deaed176de..27ce0b6aac4 100644 --- a/dag/extdeps/github/workflow_runs.dag +++ b/dag/extdeps/github/workflow_runs.dag @@ -168,24 +168,20 @@ fn workflow_job_attempt_filter_wire(f: WorkflowJobAttemptFilter) -> String { } } -// A THIRD FIELD WAS DELETED HERE AND STAYS DELETED, and this annotation is the second attempt to -// settle it. An earlier lane added runner_name because the vendor machine name is corroborating -- -// the Biome baseline job reports "depot-1mw2k81zm2" -- found nothing read it, and deleted it on the -// ground that interesting is not a consumer. This change put it back claiming a consumer had -// arrived, in prose, while the diff carried no import and no call site; it is deleted again on the -// original ground, which was right both times. DESIGN section 4c is the rule: an annotation is -// never evidence that a machine claim holds. +// THE RUNNER FIELDS RETURNED WHEN THEIR NAMED TRIGGER LANDED. An earlier lane added runner_name, +// found nothing read it, and deleted it on the ground that interesting is not a consumer; a second +// attempt claimed a consumer in prose with no import or call site and was deleted again. The trigger +// that was named is a fold that IMPORTS this module and reads the field, landing in the same change +// as the field: gunbc.runner.runner_qualification_dispatch job_ran_on is that fold, so the fields are +// here with their consumer in the same change. // -// The example survives the deletion because it is the part that was worth keeping. -// "depot-1mw2k81zm2" is neither GitHub-hosted nor self-hosted but a third party's fleet, so any -// provenance reading with two arms folds a paying provider customer in with a team running its own -// hardware. The trigger that brings the field back is a fold that IMPORTS this module and reads -// the field, landing in the same change as the field -- and that fold now has a further obligation -// this lane learned the hard way: a runs-on LABEL already has an authority in -// gunbc.runner.runner_label_resolution, backed by the per-provider catalogs +// The example that survived both deletions still governs the reading. "depot-1mw2k81zm2" is neither +// GitHub-hosted nor self-hosted but a third party's fleet, so any provenance reading with two arms +// folds a paying provider customer in with a team running its own hardware. A runs-on LABEL has an +// authority in gunbc.runner.runner_label_resolution, backed by the per-provider catalogs // gunbc.runner.runner_provider_survey enrolls, so a consumer may not re-answer the label question // with a fresh prefix roster. A runner NAME is a different vocabulary with no such authority, which -// is the one thing this field would genuinely add. +// is what these fields add. // // `name` is the only matrix-leg identifier this resource carries. The Jobs REST job object // (docs.github.com/en/rest/actions/workflow-jobs, X-GitHub-Api-Version 2026-03-10) publishes @@ -194,6 +190,12 @@ fn workflow_job_attempt_filter_wire(f: WorkflowJobAttemptFilter) -> String { // rendered name. The parenthetical of combination VALUES in axis order is the rendering this // tree observed on those names; it is not a REST field. Standing is TranscribedUncited until // GitHub's Jobs docs state that encoding. +// runner_id AND runner_name ARE WHICH RUNNER TOOK THE JOB, a third fact beside the declared runs-on +// and the observed labels: two runners can carry identical labels. runner_id is the exact identity +// GitHub returned when the JIT registration was minted (gunbc.runner.runner_qualification_dispatch +// job_ran_on joins on it); runner_name is corroboration, since one name can resolve to several ids. +// Upstream publishes both as nullable -- null until a runner takes the job -- and every record in +// this tree written before the fields existed carries none rather than a guessed value. type WorkflowJobRun { id: Int run_id: Int @@ -202,6 +204,8 @@ type WorkflowJobRun { status: WorkflowRunStatus conclusion: WorkflowRunConclusion? labels: List + runner_id: Int? + runner_name: String? created_at: Timestamp? started_at: Timestamp? completed_at: Timestamp? @@ -293,10 +297,17 @@ data structural_coverage_gap_workflow_run_codec_hand_rolled: List = [ // drops are execution that really happened and really occupied a runner. A caller measuring // occupancy needs "all"; a caller reading current state needs "latest"; neither is a property of // this operation, so the choice moves to the input with "latest" as the compatible default. +// THE BEARER IS THE CALLER'S auth_token WHEN ONE IS GIVEN. Every operation already took auth_token, +// and the service read only GITHUB_TOKEN, so a caller holding an installation token +// (gunbc.github_effect_perform read_run_with / read_attempt_jobs_with) was silently read under the +// ambient Actions credential. Declaring auth_input beside auth_source makes a non-empty auth_token the +// bearer; a caller passing "" (gunbc.pr_base_freshness, gunbc.fleet_desired_admission, +// gunbc.roadmap_launch_deployment_cli) falls through to GITHUB_TOKEN exactly as before. service github.WorkflowRuns { config { endpoint: default_api_base auth: Bearer + auth_input: auth_token auth_source: EnvVar { name: "GITHUB_TOKEN" } } diff --git a/dag/extdeps/github/workflows.dag b/dag/extdeps/github/workflows.dag index c0de4991178..dd7498019af 100644 --- a/dag/extdeps/github/workflows.dag +++ b/dag/extdeps/github/workflows.dag @@ -3,13 +3,9 @@ module extdeps.github.workflows import extdeps.ietf.http_semantics { POST } import extdeps.github.github { default_api_base } import extdeps.github.errors { GitHubErrorShape } -import std.credentials { EnvVar } -import std.types { CommitSha, List, NonEmptyStr } +import std.types { NonEmptyStr, Secret, String } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } -import std.roster_frontier { FrontierRow, frontier_row_decl } -import std.dissolution { unbound_dissolution } -import std.decl_ref { decl_ref } import std.resources { Network } import extdeps.ietf.http_semantics { POST } import extdeps.transports.rest { RestResult } @@ -42,40 +38,37 @@ type WorkflowDispatchReceipt { // WorkflowDispatchReceipt would fabricate a run that was refused. The owning workflow may be // retriggered after diagnosis; this operation never assumes a git push created a run. // -// FROZEN UPSTREAM SHAPE: tools.ci_heal_dispatch, the only production caller, is deleted. Restoring -// heal auto-dispatch does not consume this operation. `expected_healed_sha` is the `inputs` -// key GitHub accepts for this repository's workflow_dispatch contract; it is not a second heal -// policy and must not grow more heal-specific keys here. Disposition: -// create_dispatch_unconsumed_frontier_rows. - -data create_dispatch_unconsumed_frontier_rows: List = [ - frontier_row_decl( - ref: decl_ref(module_path: "extdeps.github.workflows", decl_name: "WorkflowDispatchReceipt"), - reason: "github.Workflows CreateDispatch and WorkflowDispatchReceipt are the cited REST shape with no production caller after tools.ci_heal_dispatch was deleted; frozen: no new heal-specific keys or auto-invoke rows", - dissolution: unbound_dissolution(description: "a production fold that is not heal auto-dispatch calls github.Workflows CreateDispatch, or CreateDispatch and WorkflowDispatchReceipt are deleted. NOT satisfied by restoring tools.ci_heal_dispatch, nor by a witness constructing WorkflowDispatchReceipt"), - ) -] - +// `inputs` IS THE UPSTREAM'S OWN SHAPE: an object of input name to value, at most 25 properties, +// each key a workflow_dispatch input the target workflow declares (extdeps.github.actions +// DispatchInput). It once carried exactly one key, expected_healed_sha, because the deleted +// tools.ci_heal_dispatch was its only caller -- a consumer's policy fused into the interface +// (DESIGN section 3). Which keys a dispatch carries is the dispatching workflow's fact, so the +// caller supplies the object and this module names no key. GitHub answers an undeclared key with +// 422, which is the refusal arm below, never a silently dropped input. +// +// THE CREDENTIAL IS AN INPUT, NOT AN AMBIENT VARIABLE. It once read GITHUB_TOKEN from the +// environment, which fixed the executing credential to whichever job happened to run the call. +// Which credential performs a dispatch is the caller's authorization fact (gunbc.auth), so the +// operation takes the bearer as auth_token, as the self-hosted-runner and gist services do. service github.Workflows { config { endpoint: default_api_base auth: Bearer - auth_source: EnvVar { name: "GITHUB_TOKEN" } + auth_input: auth_token } operation CreateDispatch { requires Network input { + auth_token: Secret owner: String repo: String workflow_id: String ref: String - expected_healed_sha: CommitSha + inputs: Map } output { - workflow_run_id: Int - run_url: NonEmptyStr - html_url: NonEmptyStr + result: WorkflowDispatchReceipt } transport rest { method: POST, @@ -83,7 +76,7 @@ service github.Workflows { headers: { "X-GitHub-Api-Version": workflows_api_version }, body: { ref: ref, - inputs: { expected_healed_sha: expected_healed_sha } + inputs: inputs } } response { diff --git a/dag/gunbc/auth/privileged_effect_census.dag b/dag/gunbc/auth/privileged_effect_census.dag index d6e24a2d7a4..742b06a9efd 100644 --- a/dag/gunbc/auth/privileged_effect_census.dag +++ b/dag/gunbc/auth/privileged_effect_census.dag @@ -409,6 +409,13 @@ data mtcollins1_hold_owning_roots: List = [ ] data privileged_effect_interlocks: List = [ + PrivilegedEffectInterlock { + site: site(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "dispatch_qualification_floor"), + hold: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof"), + refusal: site(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "dispatch_qualification_floor"), + premise: "the dispatch takes the slot host's unit hold proof and refuses DispatchHoldForAnotherHost unless the proof's admitted host is the slot's own; the root that acquires it is the route fold the dispatch leg owes (LegAuthorityImplemented wiring_owed), so no production root is rostered yet" as NonEmptyStr, + hold_owning_roots: [] as List, + }, PrivilegedEffectInterlock { site: site(module_path: "gunbc.spark.pair_serving_d0_door", decl_name: "d0_standing_grant_for"), hold: decl_ref(module_path: "gunbc.spark.pair_serving_d0", decl_name: "d0_claim_grant"), @@ -577,6 +584,60 @@ fn present_trigger_declarations() -> List { // committed standing grant covers is admitted by that grant, never filed to the broker. The selection // decides the pattern from the effect's parameters with the ruling as the witness discharge, conditional on // its interlock (D0's durable claim, rostered in privileged_effect_interlocks); the census does not assert it. +// THE OPERATOR'S 2026-10-03 RUNNER-LIFECYCLE RULING, VERBATIM, AND THE OPERATOR'S 2026-10-05 SCOPE +// RULING BESIDE IT. The 10-03 text names registration and deregistration and is never rewritten to +// say more. Its scope beyond those words is the operator's own second ruling, decided through +// escalation msg_5756a200-fcb5-470a-87eb-40867bfe9cdb: no agent's reading discharges a site (review +// 76234, DESIGN §5: approval is external to the diff, so the row cites where the operator decided). +// covers is the single source of the operator's scope: no census row may take the 10-03 discharge +// unless covers names its site. The converse does not hold, on purpose: a covered site whose effect +// the selection already federates on its own parameters -- registration, deregistration and the +// reversible branch create and delete -- does not consume the discharge, and only a consumer owes a +// rostered interlock. The dispatch, being irreversible, is the one consumer. +// THE DEDICATED GROUP'S SELECTED-WORKFLOW PIN IS NOT UNDER EITHER RULING. ensure_qualification_ref_pin +// is listed for its branch create; the group pin it performs in the same function is authorized by +// its own federated standing -- the census row's own parameters, selected without any discharge -- +// and the 10-03 and 10-05 rulings say nothing about it (eager-gull-22, 2026-10-05). The interlock is the +// host-generic unit hold (gunbc.managed_host_unit_hold UnitHoldProof): the dispatch takes the proof +// and refuses unless it is the slot's own host's. +data runner_lifecycle_operator_ruling: StandingDestructiveAuthorization = StandingDestructiveAuthorization { + ruling_text: "Runner registration and deregistration are PRE-APPROVED. Approval moves up to the workflow dispatcher (the fleet-converge run's own authorization). There is no per-registration approval step. Classify this through gunbc.auth.authorization_pattern_selection, recording that ruling rather than a per-effect ntfy approval. (operator decision, 2026-10-03)" as NonEmptyStr, + effect_subject: "ephemeral JIT runner lifecycle: registration and deregistration" as NonEmptyStr, + interlock: InterlockedBy { hold: decl_ref(module_path: "gunbc.managed_host_unit_hold", decl_name: "UnitHoldProof") }, +} + +type OperatorScopeRuling { + ruling: StandingDestructiveAuthorization + scope_text: NonEmptyStr + decided_on: NonEmptyStr + decided_through: NonEmptyStr + covers: List +} + +data runner_lifecycle_scope_ruling: OperatorScopeRuling = OperatorScopeRuling { + ruling: runner_lifecycle_operator_ruling, + scope_text: "decision: 'Yes, confirm the wider scope' (operator, 2026-10-05). Scope as relayed with it by quiet-stag-623 (msg_24760d96-078a-46cf-809e-2c92968dba31): the 2026-10-03 runner pre-approval covers registration, deregistration, the qualification CreateDispatch on that attempt's runner, and the per-attempt qualification/ branch create and delete" as NonEmptyStr, + decided_on: "2026-10-05" as NonEmptyStr, + decided_through: "escalation msg_5756a200-fcb5-470a-87eb-40867bfe9cdb" as NonEmptyStr, + covers: [ + decl_ref(module_path: "gunbc.runner.runner_jit_perform", decl_name: "dispatch_jit_mint"), + decl_ref(module_path: "gunbc.runner.runner_jit_deregistration", decl_name: "ensure_jit_runner_deregistered"), + decl_ref(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "dispatch_qualification_floor"), + decl_ref(module_path: "gunbc.runner.runner_qualification_ref_pin", decl_name: "ensure_qualification_ref_pin"), + decl_ref(module_path: "gunbc.runner.runner_qualification_ref_pin", decl_name: "remove_qualification_ref_pin"), + ], +} + +// A SITE IS DISCHARGED BY THE RULING ONLY WHILE THE OPERATOR'S SCOPE RULING NAMES IT. Removing a site +// from covers turns its discharge into NoWitnessDischarge, and the selection then decides it afresh. +fn ruling_discharge_for(scope: OperatorScopeRuling, site_ref: DeclarationRef) -> WitnessDischarge { + if declaration_ref_in_list(target: site_ref, refs: scope.covers) { + StandingRulingUnderInterlock { ruling: scope.ruling } + } else { + NoWitnessDischarge + } +} + // Printing spends material and moves hardware. A federated secret read alone is not // the selected authority for that irreversible effect; the common start gate also // verifies approval, observes IDLE and atomically claims the approved escalation. @@ -652,6 +713,54 @@ data privileged_effect_census: List = [ realized: RealizedFederatedGrant, divergence_reason: none, }, + PrivilegedEffectSite { + site: site(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "dispatch_qualification_floor"), + effect: PrivilegedEffect { + subject: "dispatch the generated fleet-converge workflow with the slot's attempt label as the input its floor job's runs-on reads, so only the JIT registration minted for that attempt can serve the job, under the gunbai-ci installation token whose App key is read over WIF, checked for actions: write" as NonEmptyStr, + frequency: EveryProvision, + reversibility: IrreversibleEffect { what_is_lost: "a dispatched run is durable: a second dispatch creates another run and does not undo the first, and a cancel stops it without unmaking it" as NonEmptyStr }, + surface: ApiSurface, + workload_identity: convergence_principal(), + minted_reach: MintsNoCredential, + billing: NoBillingConsequence, + witness_discharge: ruling_discharge_for( + scope: runner_lifecycle_scope_ruling, + site_ref: site(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "dispatch_qualification_floor"), + ), + }, + realized: RealizedFederatedGrant, + divergence_reason: none, + }, + PrivilegedEffectSite { + site: site(module_path: "gunbc.runner.runner_qualification_ref_pin", decl_name: "ensure_qualification_ref_pin"), + effect: PrivilegedEffect { + subject: "create the per-attempt branch refs/heads/qualification/ once at the pinned revision (CreateRef, never moved; 422 on an existing ref is refused), read it back, and pin the dedicated runner-qualification group's selected workflow to the qualification workflow at that branch, read back; under the gunbai-ci installation token, whose contents:write reaches every ref of the repository and whose organization self-hosted-runners write reaches every runner group -- the confinement to the prefix and to the dedicated group is this module's construction, not the token's scope" as NonEmptyStr, + frequency: EveryProvision, + reversibility: ReversibleByReapply, + surface: ApiSurface, + workload_identity: convergence_principal(), + minted_reach: MintsNoCredential, + billing: NoBillingConsequence, + witness_discharge: NoWitnessDischarge, + }, + realized: RealizedFederatedGrant, + divergence_reason: none, + }, + PrivilegedEffectSite { + site: site(module_path: "gunbc.runner.runner_qualification_ref_pin", decl_name: "remove_qualification_ref_pin"), + effect: PrivilegedEffect { + subject: "on every exit, delete the attempt's refs/heads/qualification/ branch and confirm it absent by readback, under the same installation token" as NonEmptyStr, + frequency: EveryProvision, + reversibility: ReversibleByReapply, + surface: ApiSurface, + workload_identity: convergence_principal(), + minted_reach: MintsNoCredential, + billing: NoBillingConsequence, + witness_discharge: NoWitnessDischarge, + }, + realized: RealizedFederatedGrant, + divergence_reason: none, + }, PrivilegedEffectSite { site: site(module_path: "gunbc.runner_group_restriction_ensure_run", decl_name: "microvm_runner_group_after_gate"), effect: PrivilegedEffect { diff --git a/dag/gunbc/census_closure_frontier.dag b/dag/gunbc/census_closure_frontier.dag index bd31e98983b..1b075493367 100644 --- a/dag/gunbc/census_closure_frontier.dag +++ b/dag/gunbc/census_closure_frontier.dag @@ -21,11 +21,11 @@ import extdeps.docker.container_stats { } import extdeps.docker.endpoint { endpoint_string_type_frontier_rows } import extdeps.github.merge_state { merge_state_graphql_transport_frontier_rows } +import gunbc.runner.runner_qualification_dispatch { qualification_instrument_extraction_frontier_rows } import extdeps.github.workflow_runs { conclusion_authority_consolidation_frontier_rows, } import extdeps.github.app { modeled_webhook_event_vocabulary_frontier_rows } -import extdeps.github.workflows { create_dispatch_unconsumed_frontier_rows } import gunbc.public_workload_census { public_workload_census_replay_consumer_frontier_rows, public_workload_census_run_attempt_consumer_frontier_rows, @@ -110,7 +110,7 @@ fn census_closure_frontier_row_groups() -> List> { endpoint_string_type_frontier_rows, merge_state_graphql_transport_frontier_rows, conclusion_authority_consolidation_frontier_rows, - create_dispatch_unconsumed_frontier_rows, + qualification_instrument_extraction_frontier_rows, modeled_webhook_event_vocabulary_frontier_rows, census_app_installation_route_frontier_rows, census_app_installation_population_frontier_rows, diff --git a/dag/gunbc/github_effect_perform.dag b/dag/gunbc/github_effect_perform.dag index 565bc4b9f86..cf9c5f33bd7 100644 --- a/dag/gunbc/github_effect_perform.dag +++ b/dag/gunbc/github_effect_perform.dag @@ -2,6 +2,7 @@ module gunbc.github_effect_perform import std.types { String, NonEmptyStr, Int, List, Secret, EpochSecs } import std.resources { Network } +import std.decl_ref { decl_ref } import std.dissolution { DissolutionCondition, unbound_dissolution } import extdeps.clock { clock_unix_millis_read, ClockUnixMillisObserved, ClockUnixMillisRefused, epoch_secs_of_millis, @@ -29,6 +30,14 @@ import extdeps.github.app import extdeps.github.actions_jit_runner import extdeps.github.actions_self_hosted_runners import extdeps.github.actions_self_hosted_runners { OrganizationRunnerListWire, OrganizationRunnerDeletedBody } +import extdeps.github.workflows +import extdeps.github.workflows { WorkflowDispatchReceipt } +import extdeps.github.workflow_runs +import extdeps.github.git_database +import extdeps.github.git_database { GitRefWire, GitRefDeletedBody } +import extdeps.github.org_actions +import extdeps.github.org_actions { OrgRunnerGroupWire } +import extdeps.github.workflow_runs { WorkflowRun, WorkflowJobRunList } import gunbc.auth.github_apps { DeclaredGitHubApp, gunbai_ci_declared } import extdeps.github.app { GitHubAppInstallationId } import gunbc.runner.runner_jit_perform { @@ -138,10 +147,17 @@ type JitMintAppJwt // same jit_config_mint_outcome every status goes through, so an empty blob under 201 is still // refused there; a non-2xx the remote DECIDED is a JitConfigMintOutcome refusal; an answer that // never arrived is commit-ambiguous and is NOT reported as a refusal. +// +// ADMITTED ONLY FROM THE PERFORM FUNCTION AND A CLAIM. This fold takes the dispatch and the answer +// separately, so an open call would mint a delivery for dispatch A from any 201 body; the perform +// function is the one caller whose answer is GitHub's response to dispatch.request. fn jit_mint_performance_of_generate( dispatch: JitMintDispatch, outcome: RestResult, -) -> JitMintPerformance { +) -> JitMintPerformance admit_callers: [ + decl_ref(module_path: "gunbc.github_effect_perform", decl_name: "perform_organization_jit_mint"), + decl_ref(module_path: "test.claim.github_effect_perform_witness", decl_name: "witness_generate_step_delivers_refuses_or_reports_ambiguity_by_what_github_answered"), +] { match outcome { RestAnswered { answer: created } => JitMintReceived { @@ -317,3 +333,105 @@ fn delete_runner_with(token: ControllerInstallationToken, organization: NonEmpty RestRefused { refusal } => RestRefused { refusal: refusal } } } + +// THE QUALIFICATION DISPATCH AND ITS READBACK, under the same controller installation token +// (gunbc.runner.runner_qualification_dispatch). Each answer is GitHub's RestResult, sealed so the +// decision module receives only what GitHub returned; the decision classifies a refusal as a read's +// or a mutation's (extdeps.transports.rest classify_rest_refusal), so for the dispatch a 5xx, a lost +// response or an undecodable 200 is commit-ambiguous rather than refused. +type WorkflowDispatchAnswer sole_constructor { + dispatch: RestResult +} + +fn dispatch_workflow_with( + token: ControllerInstallationToken, + owner: NonEmptyStr, + repo: NonEmptyStr, + workflow_id: NonEmptyStr, + git_ref: NonEmptyStr, + inputs: Map, +) -> WorkflowDispatchAnswer uses net: Network { + let answered = github.Workflows.CreateDispatch( + auth_token: token.token, + owner: owner as String, + repo: repo as String, + workflow_id: workflow_id as String, + ref: git_ref as String, + inputs: inputs, + ) + WorkflowDispatchAnswer { + dispatch: match answered { + RestAnswered { answer } => RestAnswered { answer: answer.result } + RestRefused { refusal } => RestRefused { refusal: refusal } + }, + } +} + +type WorkflowRunRead sole_constructor { + run: RestResult +} + +fn read_run_with(token: ControllerInstallationToken, owner: NonEmptyStr, repo: NonEmptyStr, run_id: Int) -> WorkflowRunRead uses net: Network { + let read = github.WorkflowRuns.GetRun(auth_token: token.token, owner: owner as String, repo: repo as String, run_id: run_id as String) + WorkflowRunRead { + run: match read { + RestAnswered { answer } => RestAnswered { answer: answer.run } + RestRefused { refusal } => RestRefused { refusal: refusal } + }, + } +} + +type WorkflowAttemptJobsRead sole_constructor { + jobs: RestResult +} + +fn read_attempt_jobs_with(token: ControllerInstallationToken, owner: NonEmptyStr, repo: NonEmptyStr, run_id: Int, attempt: Int) -> WorkflowAttemptJobsRead uses net: Network { + let read = github.WorkflowRuns.ListAttemptJobs(auth_token: token.token, owner: owner as String, repo: repo as String, run_id: run_id as String, attempt_number: attempt) + WorkflowAttemptJobsRead { + jobs: match read { + RestAnswered { answer } => RestAnswered { answer: answer.result } + RestRefused { refusal } => RestRefused { refusal: refusal } + }, + } +} + +// THE QUALIFICATION REF PIN'S EXCHANGES (gunbc.runner.runner_qualification_ref_pin), under the same +// controller installation token. Ref and group reads are reads; the create, delete and group write +// are mutations, so a lost answer is commit-ambiguous. Each answer is sealed for the same reason as +// the dispatch's: the decision module judges only what GitHub returned. +type GitRefRead sole_constructor { + reference: RestResult +} + +fn read_git_ref_with(token: ControllerInstallationToken, owner: NonEmptyStr, repo: NonEmptyStr, ref: NonEmptyStr) -> GitRefRead uses net: Network { + let read = github.GitDatabase.GetRef(auth_token: token.token, owner: owner as String, repo: repo as String, ref: ref as String) + GitRefRead { + reference: match read { + RestAnswered { answer } => RestAnswered { answer: answer.reference } + RestRefused { refusal } => RestRefused { refusal: refusal } + }, + } +} + +fn create_git_ref_with(token: ControllerInstallationToken, owner: NonEmptyStr, repo: NonEmptyStr, full_ref: NonEmptyStr, sha: String) -> RestResult uses net: Network { + match github.GitDatabase.CreateRef(auth_token: token.token, owner: owner as String, repo: repo as String, full_ref: full_ref as String, sha: sha) { + RestAnswered { answer } => RestAnswered { answer: answer.reference } + RestRefused { refusal } => RestRefused { refusal: refusal } + } +} + +fn delete_git_ref_with(token: ControllerInstallationToken, owner: NonEmptyStr, repo: NonEmptyStr, ref: NonEmptyStr) -> RestResult uses net: Network { + match github.GitDatabase.DeleteRef(auth_token: token.token, owner: owner as String, repo: repo as String, ref: ref as String) { + RestAnswered { answer } => RestAnswered { answer: answer.result } + RestRefused { refusal } => RestRefused { refusal: refusal } + } +} + +fn update_runner_group_workflows_with(token: ControllerInstallationToken, organization: NonEmptyStr, runner_group_id: Int, selected_workflows: List) -> RestResult uses net: Network { + match github.OrgRunnerGroupsRest.UpdateOrganizationRunnerGroupWorkflows( + installation_token: token.token, org: organization, runner_group_id: runner_group_id, selected_workflows: selected_workflows, + ) { + RestAnswered { answer } => RestAnswered { answer: answer.result } + RestRefused { refusal } => RestRefused { refusal: refusal } + } +} diff --git a/dag/gunbc/public_workload_census.dag b/dag/gunbc/public_workload_census.dag index 19d698ca403..ec11c28ce47 100644 --- a/dag/gunbc/public_workload_census.dag +++ b/dag/gunbc/public_workload_census.dag @@ -1020,6 +1020,8 @@ data candidate_biome_test: WorkloadCandidate = WorkloadCandidate { status: Completed, conclusion: Present { value: Success }, labels: ["depot-ubuntu-24.04-arm-16"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:32Z" }, completed_at: Present { value: "2026-09-04T16:08:13Z" }, @@ -1082,6 +1084,8 @@ data candidate_pdns_dnsdist_arm: WorkloadCandidate = WorkloadCandidate { status: Completed, conclusion: Present { value: Success }, labels: ["ubuntu-24.04-arm"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T09:57:28Z" }, completed_at: Present { value: "2026-09-04T10:07:09Z" }, @@ -1149,6 +1153,8 @@ data candidate_openobserve_arm_build: WorkloadCandidate = WorkloadCandidate { status: Completed, conclusion: Present { value: Success }, labels: ["ubicloud-standard-16-arm"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-01T10:02:21Z" }, completed_at: Present { value: "2026-09-01T10:27:44Z" }, @@ -1218,6 +1224,8 @@ data candidate_openobserve_amd64: WorkloadCandidate = WorkloadCandidate { status: Completed, conclusion: Present { value: Success }, labels: ["ubicloud-standard-8"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-01T10:02:15Z" }, completed_at: Absent, @@ -1271,6 +1279,8 @@ data candidate_openobserve_manifest: WorkloadCandidate = WorkloadCandidate { status: Completed, conclusion: Present { value: Success }, labels: ["ubicloud-standard-16-arm"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-01T10:28:12Z" }, completed_at: Absent, @@ -1324,6 +1334,8 @@ data candidate_biome_test_windows: WorkloadCandidate = WorkloadCandidate { status: Completed, conclusion: Present { value: Success }, labels: ["depot-windows-2022-16"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:31Z" }, completed_at: Present { value: "2026-09-04T16:13:50Z" }, @@ -1371,6 +1383,8 @@ data candidate_biome_test_macos: WorkloadCandidate = WorkloadCandidate { status: Completed, conclusion: Present { value: Success }, labels: ["depot-macos-latest"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:08:06Z" }, completed_at: Absent, @@ -1416,6 +1430,8 @@ data candidate_openobserve_summary: WorkloadCandidate = WorkloadCandidate { status: Completed, conclusion: Present { value: Success }, labels: ["ubuntu-latest"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-01T10:29:11Z" }, completed_at: Absent, diff --git a/dag/gunbc/recurring_failure_mode/qualification_floor_guard_skippable_by_a_workflow_file_edit.dag b/dag/gunbc/recurring_failure_mode/qualification_floor_guard_skippable_by_a_workflow_file_edit.dag new file mode 100644 index 00000000000..c5d3bf017db --- /dev/null +++ b/dag/gunbc/recurring_failure_mode/qualification_floor_guard_skippable_by_a_workflow_file_edit.dag @@ -0,0 +1,26 @@ +module gunbc.recurring_failure_mode.qualification_floor_guard_skippable_by_a_workflow_file_edit + +import std.types { NonEmptyStr } +import std.decl_ref { DeclarationRef, decl_ref } +import gunbc.recurring_failure_mode { RecurringFailureMode } + +data qualification_floor_guard_skippable_by_a_workflow_file_edit: RecurringFailureMode = RecurringFailureMode { + identity: "qualification_floor_guard_skippable_by_a_workflow_file_edit" as NonEmptyStr, + + receipts: [ + "**the qualification floor's revision guard is skippable by an edit to the workflow file on the qualification branch** (declared with sha-checkout, decision eager-gull-22 2026-10-04).", + + "INVALID STATE: a qualification run whose floor job executes code other than the pinned revision while the run reports the pinned head. The dispatch names the per-attempt branch refs/heads/qualification/; GitHub runs that branch's copy of the workflow file, and the guard that checks out inputs.qualification_revision and refuses on a mismatch is a step INSIDE that file (gunbc.runner.runner_qualification_dispatch qualification_floor_revision_guard_step). An actor who rewrites the workflow file on that branch -- deleting the guard, or adding steps before it -- runs other code on the attempt's runner.", + + "HARM: a qualification receipt measured on code that is not the pinned workload, on the dedicated host. Bounded by who can cause it: writing the branch's workflow file needs repository push (contents write), an actor already trusted to change any code in the repository, and the per-attempt branch is created by the route at the pinned revision immediately before dispatch.", + + "DISTINGUISHING FACTS: the guard's absence is caught by the floor contract only for the MODEL the subject mint reads (qualification_floor_admission refuses a floor job whose first step is not the guard, or whose later steps run past a failure); it is not caught for the file GitHub actually executes from the branch. The post-run check RunRevisionNotPinned (gunbc.runner.runner_qualification_dispatch decide_qualification_run) refuses a run whose head_sha is not the pinned revision, but an edit committed on the branch moves head_sha too, so that check catches a moved branch and not a rewritten file at the same head.", + + "RUNG: 2 for a moved branch (the guard and RunRevisionNotPinned each refuse, before any step and after the run). 1 for a rewritten workflow file at the branch head: contained by repository-push trust, not refused. CEILING: 3 needs the executed workflow file to be an identity the route admits rather than whatever the branch holds -- e.g. a reusable workflow selected by full SHA in the dedicated group (GitHub admits a SHA pin only for REUSABLE workflows), with the guard inside it. NEXT TRIGGER: the qualification mode lands in gunbc.fleet_converge_workflow (the dispatch leg's wiring_owed); deciding there whether the floor job is a SHA-selected reusable workflow is what would climb this row.", + ], + + evidence: [ + decl_ref(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "qualification_floor_revision_guard_step"), + decl_ref(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "qualification_floor_admission"), + ], +} diff --git a/dag/gunbc/runner/runner_attempt_launch.dag b/dag/gunbc/runner/runner_attempt_launch.dag index 653d94c7810..28f04976042 100644 --- a/dag/gunbc/runner/runner_attempt_launch.dag +++ b/dag/gunbc/runner/runner_attempt_launch.dag @@ -40,7 +40,7 @@ import gunbc.guarantee_rung { import extdeps.github.actions_jit_runner { EncodedJitConfig, JitRunnerName } import gunbc.github_effect_perform { JitMintPerformance, JitMintReceived } import gunbc.runner.runner_jit_perform { - JitCredentialDelivery, JitCredentialBoundToAttempt, + JitCredentialDelivery, JitCredentialBoundToAttempt, bound_jit_slot, } import gunbc.runner_jit_mint { jit_runner_name_for, JitSlot, MicroVmJitSlot } import gunbc.runner.runner_jit_admission { @@ -211,7 +211,10 @@ fn admit_jit_credential(attempt: MicroVmAttempt, mint: JitMintPerformance) -> Ji match mint { JitMintReceived { delivery: delivery } => match delivery { - JitCredentialBoundToAttempt { slot: bound, credential: c, runner_id: id } => + JitCredentialBoundToAttempt { bound: b } => { + let bound = bound_jit_slot(bound: b) + let c = b.credential + let id = b.runner_id if !host_mint_admission_is_required() { JitCredentialRefused { refusal: JitMintAdmissionAxisNotRequired } } else if bound != MicroVmJitSlot { attempt: attempt } { @@ -229,6 +232,7 @@ fn admit_jit_credential(attempt: MicroVmAttempt, mint: JitMintPerformance) -> Ji }, } } + } other => JitCredentialRefused { refusal: JitCredentialNotDelivered { delivery: other } } } other => JitCredentialRefused { refusal: JitMintNotReceived { performance: other } } diff --git a/dag/gunbc/runner/runner_jit_perform.dag b/dag/gunbc/runner/runner_jit_perform.dag index 90359964001..dc3058a8f09 100644 --- a/dag/gunbc/runner/runner_jit_perform.dag +++ b/dag/gunbc/runner/runner_jit_perform.dag @@ -138,6 +138,11 @@ fn dispatch_jit_mint( decl_ref(module_path: "gunbc.runner_microvm_slot_controller", decl_name: "attempt_dispatch"), decl_ref(module_path: "test.claim.github_app_registry", decl_name: "dispatched"), decl_ref(module_path: "test.claim.github_app_registry", decl_name: "witness_jit_dispatch_refuses_when_the_attempt_binding_is_deferred"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "the_real_mint_admits_the_attempt_through_the_sealed_subject"), + decl_ref(module_path: "test.claim.runner_attempt_launch_witness", decl_name: "planned_with"), + decl_ref(module_path: "test.claim.runner.runner_microvm_slot_controller_witness_test", decl_name: "delivered_mint"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "a_delivery_from_another_dispatch_on_the_same_slot_refuses"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "the_production_mint_over_todays_fleet_converge_workflow_refuses_at_the_attempt_input"), ] { match plan_jit_mint( binding: binding, @@ -201,29 +206,57 @@ fn dispatch_jit_mint( // 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. +// THE SUCCESSFUL DELIVERY IS SEALED, AND IT CARRIES THE WHOLE AUTHORIZED DISPATCH THAT PRODUCED IT. +// receive_jit_mint is its only constructor, so the credential, the runner id GitHub returned and the +// dispatch -- App, installation, organization and the complete request (name, runner group, labels, +// work folder) -- are one value no caller can re-assemble. An open arm holding these as separate +// fields let a holder of two deliveries rewrap one's credential with the other's dispatch; a consumer +// that needs to know which mint a credential came from (gunbc.runner.runner_qualification_dispatch) +// compares bound.dispatch with its own sealed dispatch, which covers the complete request. +type BoundJitCredential sole_constructor { + dispatch: AuthorizedJitMintDispatch + credential: EncodedJitConfig + runner_id: Int +} + +fn bound_jit_slot(bound: BoundJitCredential) -> JitSlot { + bound.dispatch.slot +} + type JitCredentialDelivery - = JitCredentialBoundToAttempt { - slot: JitSlot - credential: EncodedJitConfig - runner_id: Int - } + = JitCredentialBoundToAttempt { bound: BoundJitCredential } | JitCredentialNotDispatched { refusal: JitDispatchRefusal } | JitCredentialMintNotCreated { outcome: JitConfigMintOutcome } +// THE MINT IS ADMITTED ONLY WHERE A RESPONSE IS BOUND TO ITS REQUEST. receive_jit_mint pairs a +// dispatch with an outcome it is handed, so an open call relabels any delivery's credential under any +// authorized dispatch: receive_jit_mint(dispatch: A, outcome: JitConfigMinted { B's credential, B's +// runner id }) carries bound.dispatch == A and passes every equality on the dispatch. Production +// reaches it only through gunbc.github_effect_perform jit_mint_performance_of_generate, which is +// itself admitted only from the perform function that sends dispatch.request and decodes GitHub's +// answer to that request. Every other admitted caller is a claim returning Bool, or a fixture +// returning a value that carries no delivery, so no admitted edge hands a delivery back out. fn receive_jit_mint( dispatch: JitMintDispatch, outcome: JitConfigMintOutcome -) -> JitCredentialDelivery { +) -> JitCredentialDelivery admit_callers: [ + decl_ref(module_path: "gunbc.github_effect_perform", decl_name: "jit_mint_performance_of_generate"), + decl_ref(module_path: "test.claim.github_app_registry", decl_name: "witness_a_refused_dispatch_delivers_nothing_even_from_a_minted_credential"), + decl_ref(module_path: "test.claim.github_app_registry", decl_name: "witness_an_authorized_dispatch_delivers_nothing_when_the_mint_was_not_created"), + decl_ref(module_path: "test.claim.github_app_registry", decl_name: "witness_a_minted_credential_is_bound_to_the_dispatched_attempt"), + decl_ref(module_path: "test.claim.runner.runner_microvm_slot_controller_witness_test", decl_name: "delivered_mint"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "the_real_mint_admits_the_attempt_through_the_sealed_subject"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "the_production_mint_over_todays_fleet_converge_workflow_refuses_at_the_attempt_input"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "a_delivery_from_another_dispatch_on_the_same_slot_refuses"), + decl_ref(module_path: "test.claim.runner_attempt_launch_witness", decl_name: "planned_with"), +] { match dispatch { JitMintDispatchRefused { refusal: r } => JitCredentialNotDispatched { refusal: r } JitMintDispatchAuthorized { dispatch: authorized } => { - let slot = authorized.slot match outcome { JitConfigMinted { config: config, runner_id: runner_id } => JitCredentialBoundToAttempt { - slot: slot, - credential: config, - runner_id: runner_id, + bound: BoundJitCredential { dispatch: authorized, credential: config, runner_id: runner_id }, } JitConfigMintRefused { status: s, reason: reason } => JitCredentialMintNotCreated { @@ -244,11 +277,7 @@ fn receive_jit_mint( fn jit_credential_delivered(delivery: JitCredentialDelivery) -> Bool { match delivery { - JitCredentialBoundToAttempt { - slot: _, - credential: _, - runner_id: _, - } => true + JitCredentialBoundToAttempt { bound: _ } => true JitCredentialNotDispatched { refusal: _ } => false JitCredentialMintNotCreated { outcome: _ } => false } diff --git a/dag/gunbc/runner/runner_microvm_slot_controller.dag b/dag/gunbc/runner/runner_microvm_slot_controller.dag index 3dbce2f7117..db324b284a8 100644 --- a/dag/gunbc/runner/runner_microvm_slot_controller.dag +++ b/dag/gunbc/runner/runner_microvm_slot_controller.dag @@ -531,7 +531,7 @@ fn minted_registration(mint: JitMintPerformance) -> Int? { match mint { JitMintReceived { delivery: d } => match d { - JitCredentialBoundToAttempt { slot: _, credential: _, runner_id: id } => Present { value: id } + JitCredentialBoundToAttempt { bound: b } => Present { value: b.runner_id } JitCredentialNotDispatched { refusal: _ } => none JitCredentialMintNotCreated { outcome: _ } => none } diff --git a/dag/gunbc/runner/runner_qualification_dispatch.dag b/dag/gunbc/runner/runner_qualification_dispatch.dag new file mode 100644 index 00000000000..a5c097c0337 --- /dev/null +++ b/dag/gunbc/runner/runner_qualification_dispatch.dag @@ -0,0 +1,730 @@ +module gunbc.runner.runner_qualification_dispatch + +import std.types { Bool, CommitSha, Int, List, NonEmptyStr, String } +import std.resources { Network } +import std.roster_frontier { FrontierRow, frontier_row_decl } +import std.dissolution { unbound_dissolution } +import std.decl_ref { decl_ref } +import product.placement_supply { HostIdentity } +import extdeps.transports.rest { + RestResult, RestAnswered, RestRefused, RestReadExchange, RestMutationExchange, classify_rest_refusal, + RestExchangeRefusal, RestExchangeStatusRefused, + RestExchangeCommitAmbiguous, RestExchangeUnreached, RestExchangeUndecodable, +} +import extdeps.github.effect { GitHubEffect, DispatchWorkflow, GitHubWorkflowRef } +import extdeps.github.app { GitHubAppInstallationId } +import extdeps.github.actions { + Workflow, Job, DispatchInput, InputString, RunnerSpec, RunsOnExpression, HostedRunner, SelfHosted, + WorkflowDispatch, Push, PullRequest, Schedule, WorkflowCall, WorkflowRunCompleted, MergeGroup, + Step, RunStep, UsesStep, +} +import extdeps.languages.yaml.types { kv, yaml_string } +import extdeps.github.expressions { + ingest_template, context_name, Expression, Interpolation, LiteralText, + ContextAccess, FunctionCall, StringLiteral, LogicalOr, LogicalAnd, Equals, NotEquals, +} +import extdeps.github.workflows { WorkflowDispatchReceipt } +import extdeps.github.workflow_runs { + WorkflowRun, WorkflowRunStatus, Completed, WorkflowRunConclusion, WorkflowJobRun, WorkflowJobRunList, +} +import gunbc.repository { gunbc_repository } +import gunbc.auth.github_apps { DeclaredGitHubApp, GitHubAppControlPlaneState } +import gunbc.auth.github_credential { + GitHubCredentialAuthority, CredentialCapability, credential_authorizes, unsatisfied_capabilities, +} +import gunbc.runner_jit_mint { HostUnitJitSlot, MicroVmJitSlot } +import gunbc.runner.runner_jit_perform { AuthorizedJitMintDispatch, JitMintDispatchAuthorized, JitCredentialDelivery, JitCredentialBoundToAttempt, authority_installation } +import gunbc.runner.runner_jit_deregistration { JitRegistration, jit_registration_of } +import gunbc.managed_host_unit_hold { UnitHoldProof } +import gunbc.github_effect_perform { + ControllerInstallationToken, dispatch_workflow_with, read_run_with, read_attempt_jobs_with, +} +import gunbc.runner_throughput_qualification_route { QualificationInstrument, qualification_instruments } +import gunbc.runner.runner_qualification_ref_pin { + QualificationRefPin, QualificationBranchName, qualification_workflow_path, qualification_selected_workflow, +} + +// THE DISPATCH LEG OF THE QUALIFICATION ROUTE, AND THE COLLECT STAGE THAT READS ITS RUN BACK. +// +// The route registers one ephemeral JIT runner whose label set carries a per-boot attempt label +// (gunbc.runner_throughput_qualification_route ephemeral_slot_labels). Dispatching the floor to it is +// a workflow_dispatch whose input IS that attempt label, read by the floor job's runs-on, so no other +// registration can serve the job. This module is the production caller of extdeps.github.workflows +// github.Workflows CreateDispatch. +// +// THE SUBJECT IS SEALED AND ITS SCOPE IS FIXED BY CONSTRUCTION. QualificationDispatchSubject is +// minted only by qualification_dispatch_subject_over, and only from: +// - the sealed AuthorizedJitMintDispatch (gunbc.runner.runner_jit_perform), whose only mint is +// dispatch_jit_mint's authorized arm, its registration (jit_registration_of), and a credential +// delivered by THAT mint -- the delivery is a sealed BoundJitCredential carrying the dispatch that +// produced it, which must equal this dispatch over the complete request (App, installation, +// organization, name, runner group, labels, work folder); a rewrap is unconstructable -- so +// the attempt is the slot's own and the runner the collection joins on is that registration's; +// - the qualification workflow, which is not a parameter of the request: its path is the generated +// fleet-converge artifact (gunbc.generated_artifact FleetConvergeYamlArtifact) and production +// supplies its model as gunbc.fleet_converge_workflow fleet_converge_workflow, where the route's +// mode lands with the boot leg. A slot restricted to any other workflow refuses; +// - a floor job in that workflow whose runs-on is exactly the declared attempt input, so the job +// can be served by the attempt's runner and nothing else. A literal label, another input, or a +// composed expression refuses. +// The repository is gunbc_repository; a caller cannot name another. +// +// AUTHORIZATION. The dispatch runs under the gunbai-ci installation token the registration was +// minted with (gunbc.github_effect_perform ControllerInstallationToken, App key read over WIF); the +// credential is checked against the DispatchWorkflow effect (actions: write) before any request, and +// a token for another App or installation refuses. The operator's 2026-10-03 ruling, whose scope the +// operator confirmed on 2026-10-05 to cover this dispatch (gunbc.auth.privileged_effect_census +// runner_lifecycle_scope_ruling), stands only beside its interlock: +// dispatch_qualification_floor takes the host-generic unit hold proof +// (gunbc.managed_host_unit_hold UnitHoldProof) and refuses unless it is the slot's own host's. + +data qualification_attempt_dispatch_input: DispatchInput = DispatchInput { + name: "runner_attempt_label", + description: Present { value: "the per-boot attempt label the ephemeral qualification slot registered with; the floor job's runs-on reads it" }, + required: true, + default: none, + type: InputString, +} + +fn qualification_workflow_file_name() -> NonEmptyStr { + match last(split(qualification_workflow_path() as String, "/")) { + Present { value: f } => f as NonEmptyStr + Absent => qualification_workflow_path() + } +} + +// THE REVISION THE FLOOR RUNS IS AN INPUT TOO (decision: eager-gull-22, 2026-10-04 -- sha-checkout). +// A dispatch names a branch, and a branch can move between the pin's readback and the run; a ruleset +// could not stop a delete-then-recreate, and the App that would administer it could remove it. So the +// floor job itself checks out exactly this revision as its FIRST step and refuses before any other +// step on a mismatch (qualification_floor_revision_guard_step), and collection refuses a run whose +// head_sha is not the pinned revision (RunRevisionNotPinned). The residual -- an edit to the workflow +// file on the qualification branch can drop the guard -- needs repository push, and is declared as +// gunbc.recurring_failure_mode qualification_floor_guard_skippable_by_a_workflow_file_edit. +data qualification_revision_dispatch_input: DispatchInput = DispatchInput { + name: "qualification_revision", + description: Present { value: "the pinned revision the floor must run; the floor job's first step checks it out and refuses on a mismatch before any other step" }, + required: true, + default: none, + type: InputString, +} + +fn qualification_dispatch_inputs(attempt: NonEmptyStr, revision: CommitSha) -> Map { + map_insert( + m: map_insert(m: empty_map(), key: qualification_attempt_dispatch_input.name, value: attempt as String), + key: qualification_revision_dispatch_input.name, + value: revision as String, + ) +} + +// THE GUARD, AS THE ONE STEP THE FLOOR JOB MUST BEGIN WITH. It fetches and checks out the revision +// input into the runner's empty workspace and fails the job unless HEAD is exactly that revision; GitHub +// skips every later step of a failed job unless the step opts in with an if: condition, which the floor +// contract forbids (qualification_floor_admission). Its emission into the generated fleet-converge +// workflow is owed with the qualification mode (the dispatch leg's wiring_owed). +fn qualification_floor_revision_guard_step() -> Step { + RunStep { + name: Present { value: "Check out the pinned qualification revision and refuse on any mismatch" }, + id: Present { value: "qualification_revision_guard" }, + run: join([ + "set -euo pipefail", + "git init -q .", + "git remote add origin \"https://github.com/$GITHUB_REPOSITORY\"", + "git fetch -q --no-tags --depth=1 origin \"$QUALIFICATION_REVISION\"", + "git checkout -q --force --detach FETCH_HEAD", + "observed=\"$(git rev-parse HEAD)\"", + "if [ \"$observed\" != \"$QUALIFICATION_REVISION\" ]; then echo \"QualificationRevisionMismatch: expected=$QUALIFICATION_REVISION observed=$observed\" >&2; exit 1; fi", + ], "\n"), + shell: none, + env: Present { value: [kv(key: "QUALIFICATION_REVISION", value: yaml_string(s: "${{ inputs.qualification_revision }}"))] }, + working_directory: none, + if_condition: none, + continue_on_error: none, + timeout_minutes: none, + } +} + +fn step_runs_after_a_failure(step: Step) -> Bool { + match step { + RunStep { name: _, id: _, run: _, shell: _, env: _, working_directory: _, if_condition: c, continue_on_error: e, timeout_minutes: _ } => + (match c { Present { value: _ } => true Absent => false }) || (match e { Present { value: v } => v Absent => false }) + UsesStep { name: _, id: _, uses: _, with: _, env: _, if_condition: c, continue_on_error: e, timeout_minutes: _ } => + (match c { Present { value: _ } => true Absent => false }) || (match e { Present { value: v } => v Absent => false }) + } +} + +// ── THE SUBJECT ─────────────────────────────────────────────────────────────────────────────── + +type QualificationDispatchSubject sole_constructor { + registration: JitRegistration + host: HostIdentity + attempt: NonEmptyStr + runner_id: Int + pin: QualificationRefPin + floor_job_name: NonEmptyStr +} + +type QualificationSubjectRefusal + = SubjectCredentialNotDelivered { delivery: JitCredentialDelivery } + | SubjectNoRegistration + | SubjectMintedIntoAnotherGroup { minted_group: Int, pinned_group: Int } + | SubjectPinForAnotherAttempt { pin_attempt: NonEmptyStr, slot_attempt: NonEmptyStr } + | SubjectDeliveryForAnotherDispatch + | SubjectSlotNotHostUnit + | SubjectSlotForAnotherWorkflow { slot_workflow: NonEmptyStr, qualification_workflow: NonEmptyStr } + | SubjectAttemptInputUndeclared { input: String } + | SubjectFloorJobAbsent { job_id: NonEmptyStr } + | SubjectFloorRunsOnNotTheAttemptInput { job_id: NonEmptyStr, runs_on: String } + | SubjectFloorNameNotUnique { name: NonEmptyStr, jobs_with_name: Int } + | SubjectFloorRevisionGuardNotFirst { job_id: NonEmptyStr } + | SubjectFloorStepRunsPastTheGuard { job_id: NonEmptyStr } + +type QualificationSubjectStanding + = QualificationSubjectAdmitted { subject: QualificationDispatchSubject } + | QualificationSubjectRefused { refusal: QualificationSubjectRefusal } + +fn dispatch_inputs_declare(inputs: List, input: DispatchInput) -> Bool { + inputs |> any(i => i.name == input.name) +} + +fn workflow_declares_dispatch_input(workflow: Workflow, input: DispatchInput) -> Bool { + workflow.on |> any(t => + match t { + WorkflowDispatch { inputs: ins } => dispatch_inputs_declare(inputs: ins, input: input) + Push { branches: _, paths: _ } => false + PullRequest { branches: _, types: _ } => false + Schedule { cron: _ } => false + WorkflowCall { inputs: _ } => false + WorkflowRunCompleted { workflows: _, branches: _ } => false + MergeGroup => false + }) +} + +// EXACTLY `${{ inputs. }}` and nothing else: one interpolation segment reading the input. +fn runs_on_is_exactly_the_input(runner: RunnerSpec, input: DispatchInput) -> Bool { + match runner { + RunsOnExpression { expression: e } => + match ingest_template(src: e) { + Present { value: t } => + count(t.segments) == 1 && (t.segments |> all(s => + match s { + Interpolation { expression: e } => expression_reads_exactly_the_input(expression: e, input: input) + LiteralText { text: _ } => false + })) + Absent => false + } + HostedRunner { label: _ } => false + SelfHosted { labels: _ } => false + } +} + +fn expression_reads_exactly_the_input(expression: Expression, input: DispatchInput) -> Bool { + match expression { + ContextAccess { context: c, path: p } => context_name(context: c) == "inputs" && count(p) == 1 && (p |> all(x => x == input.name)) + FunctionCall { function: _, args: _ } => false + StringLiteral { value: _ } => false + LogicalOr { left: _, right: _ } => false + LogicalAnd { left: _, right: _ } => false + Equals { left: _, right: _ } => false + NotEquals { left: _, right: _ } => false + } +} + +fn runner_spec_text(runner: RunnerSpec) -> String { + match runner { + RunsOnExpression { expression: e } => e + HostedRunner { label: _ } => "a hosted runner label" + SelfHosted { labels: ls } => join(["self-hosted labels: ", join(ls, ",")], "") + } +} + +fn job_display_name(job: Job) -> NonEmptyStr { + match job.name { + Present { value: n } => n as NonEmptyStr + Absent => job.id as NonEmptyStr + } +} + +// THE SCOPE CHECKS ARE PURE, SO A CLAIM SUPPLIES THEIR INPUTS AS VALUES (DESIGN section 3: a witness +// discriminates at one interface). The subject mint below composes them and is their only +// production consumer; the witness exercises each one directly, and keeps ONE claim that runs the +// real mint end to end. + +// The slot must be registered for the qualification workflow at this branch. +fn qualification_slot_refusal(slot_workflow: NonEmptyStr, branch: NonEmptyStr) -> QualificationSubjectRefusal? { + if (slot_workflow as String) == (qualification_selected_workflow(branch: branch) as String) { + none + } else { + Present { value: SubjectSlotForAnotherWorkflow { slot_workflow: slot_workflow, qualification_workflow: qualification_selected_workflow(branch: branch) } } + } +} + +type QualificationFloorAdmission + = QualificationFloorAdmitted { floor_job_name: NonEmptyStr } + | QualificationFloorRefused { refusal: QualificationSubjectRefusal } + +// The workflow must declare the attempt input, and its floor job's runs-on must be exactly it. +fn qualification_floor_admission(workflow: Workflow, floor_job_id: NonEmptyStr) -> QualificationFloorAdmission { + if !workflow_declares_dispatch_input(workflow: workflow, input: qualification_attempt_dispatch_input) { + QualificationFloorRefused { refusal: SubjectAttemptInputUndeclared { input: qualification_attempt_dispatch_input.name } } + } else if !workflow_declares_dispatch_input(workflow: workflow, input: qualification_revision_dispatch_input) { + QualificationFloorRefused { refusal: SubjectAttemptInputUndeclared { input: qualification_revision_dispatch_input.name } } + } else { + match first(filter(workflow.jobs, j => j.id == (floor_job_id as String))) { + Absent => QualificationFloorRefused { refusal: SubjectFloorJobAbsent { job_id: floor_job_id } } + Present { value: job } => + if !runs_on_is_exactly_the_input(runner: job.runner, input: qualification_attempt_dispatch_input) { + QualificationFloorRefused { refusal: SubjectFloorRunsOnNotTheAttemptInput { job_id: floor_job_id, runs_on: runner_spec_text(runner: job.runner) } } + } else { + let name = job_display_name(job: job) + let sharing = workflow.jobs |> filter(j => (job_display_name(job: j) as String) == (name as String)) + if count(sharing) != 1 { + QualificationFloorRefused { refusal: SubjectFloorNameNotUnique { name: name, jobs_with_name: count(sharing) } } + } else { + match first(job.steps) { + Absent => QualificationFloorRefused { refusal: SubjectFloorRevisionGuardNotFirst { job_id: floor_job_id } } + Present { value: s0 } => + if s0 != qualification_floor_revision_guard_step() { + QualificationFloorRefused { refusal: SubjectFloorRevisionGuardNotFirst { job_id: floor_job_id } } + } else if job.steps |> any(st => step_runs_after_a_failure(step: st)) { + QualificationFloorRefused { refusal: SubjectFloorStepRunsPastTheGuard { job_id: floor_job_id } } + } else if match job.continue_on_error { Present { value: v } => v Absent => false } { + QualificationFloorRefused { refusal: SubjectFloorStepRunsPastTheGuard { job_id: floor_job_id } } + } else { + QualificationFloorAdmitted { floor_job_name: name } + } + } + } + } + } + } +} + +// THE PURE JOIN, OVER A SUPPLIED WORKFLOW MODEL. Production reaches it only through +// gunbc.runner.runner_qualification_production_subject qualification_dispatch_subject, which supplies +// fleet_converge_workflow; the witness claims supply a +// model carrying the floor job the boot leg's mode will add. An admit list constrains the call edge, +// not where the result goes, so every admitted witness entry is a `test fn` returning Bool. +fn qualification_dispatch_subject_over( + dispatch: AuthorizedJitMintDispatch, + delivery: JitCredentialDelivery, + workflow: Workflow, + floor_job_id: NonEmptyStr, + pin: QualificationRefPin, +) -> QualificationSubjectStanding + admit_callers: [ + decl_ref(module_path: "gunbc.runner.runner_qualification_production_subject", decl_name: "qualification_dispatch_subject"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "the_real_mint_admits_the_attempt_through_the_sealed_subject"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "a_delivery_from_another_dispatch_on_the_same_slot_refuses"), + ] +{ + match jit_registration_of(dispatch: JitMintDispatchAuthorized { dispatch: dispatch }) { + Absent => QualificationSubjectRefused { refusal: SubjectNoRegistration } + Present { value: registration } => + match delivery { + JitCredentialBoundToAttempt { bound: bound } => { + let runner_id = bound.runner_id + if bound.dispatch != dispatch { + QualificationSubjectRefused { refusal: SubjectDeliveryForAnotherDispatch } + } else { + match registration.slot { + MicroVmJitSlot { attempt: _ } => QualificationSubjectRefused { refusal: SubjectSlotNotHostUnit } + HostUnitJitSlot { slot: h } => + if (pin.name.attempt as String) != (h.attempt as String) { + QualificationSubjectRefused { refusal: SubjectPinForAnotherAttempt { pin_attempt: pin.name.attempt, slot_attempt: h.attempt } } + } else if dispatch.request.runner_group_id.value != pin.group.group.value { + QualificationSubjectRefused { refusal: SubjectMintedIntoAnotherGroup { minted_group: dispatch.request.runner_group_id.value, pinned_group: pin.group.group.value } } + } else { + match qualification_slot_refusal(slot_workflow: h.workflow, branch: pin.name.branch) { + Present { value: r } => QualificationSubjectRefused { refusal: r } + Absent => + match qualification_floor_admission(workflow: workflow, floor_job_id: floor_job_id) { + QualificationFloorRefused { refusal: r } => QualificationSubjectRefused { refusal: r } + QualificationFloorAdmitted { floor_job_name: n } => + QualificationSubjectAdmitted { + subject: QualificationDispatchSubject { + registration: registration, + host: h.host.host.host, + attempt: h.attempt, + runner_id: runner_id, + pin: pin, + floor_job_name: n, + }, + } + } + } + } + } + } + } + other => QualificationSubjectRefused { refusal: SubjectCredentialNotDelivered { delivery: other } } + } + } +} + +fn qualification_dispatch_effect(subject: QualificationDispatchSubject) -> GitHubEffect { + DispatchWorkflow { + repository: gunbc_repository, + workflow: GitHubWorkflowRef { file_name: qualification_workflow_file_name() }, + subject: subject.pin.revision, + } +} + +// ── THE DISPATCH ────────────────────────────────────────────────────────────────────────────── +// +// A DISPATCH IS A MUTATION AND HAS THREE STANDINGS, NOT TWO. GitHub's 2026-03-10 answer (200 with +// the run id) is the only one that mints a DispatchedQualificationRun. A decided 4xx is refused: no +// run exists. A 5xx, a request that got no response, or a 200 this client could not decode is +// commit-ambiguous (extdeps.transports.rest classify_rest_refusal over RestMutationExchange): a run +// may exist with no receipt here, so the standing keeps the subject for reconciliation and is not a +// refusal a caller may retry as if nothing were created. +// +// THE DISPATCHED RUN IS SEALED, AND THAT IS WHAT PUTS COLLECTION CAUSALLY AFTER DISPATCH: only +// dispatch_qualification_floor writes one, from a succeeded exchange, carrying the sealed subject. +type DispatchedQualificationRun sole_constructor { + subject: QualificationDispatchSubject + receipt: WorkflowDispatchReceipt +} + +type QualificationDispatchRefusal + = DispatchCredentialRefused { unsatisfied: List } + | DispatchTokenForAnotherInstallation + | DispatchAuthorityForAnotherInstallation { authority_app: DeclaredGitHubApp, authority_installation: GitHubAppInstallationId } + | DispatchAuthorityNotAnInstallation + | DispatchHoldForAnotherHost { held: HostIdentity, slot: HostIdentity } + | DispatchStatusRefused { status: Int, body: String } + +type QualificationDispatchStanding + = DispatchStandingSucceeded { receipt: WorkflowDispatchReceipt } + | DispatchStandingRefused { status: Int, body: String } + | DispatchStandingCommitAmbiguous { detail: NonEmptyStr } + +type QualificationDispatch + = QualificationDispatched { run: DispatchedQualificationRun } + | QualificationDispatchRefused { subject: QualificationDispatchSubject, refusal: QualificationDispatchRefusal } + | QualificationDispatchCommitAmbiguous { subject: QualificationDispatchSubject, detail: NonEmptyStr } + +// The standing of one dispatch exchange: GitHub's answer carries the receipt, and a refusal is +// decided by the mutation classifier and nothing else. An Unreached or Undecodable refusal is not +// produced for a mutation; were one ever passed here, it is the ambiguous side, never a refusal. +fn qualification_dispatch_standing(dispatch: RestResult) -> QualificationDispatchStanding { + match dispatch { + RestAnswered { answer: receipt } => DispatchStandingSucceeded { receipt: receipt } + RestRefused { refusal } => + match classify_rest_refusal(standing: RestMutationExchange { refusal: refusal }) { + RestExchangeStatusRefused { status: s, body: b } => DispatchStandingRefused { status: s as Int, body: b } + RestExchangeCommitAmbiguous { detail: d } => DispatchStandingCommitAmbiguous { detail: d } + RestExchangeUnreached { cause: c } => DispatchStandingCommitAmbiguous { detail: c } + RestExchangeUndecodable { status: _, cause: c } => DispatchStandingCommitAmbiguous { detail: c } + } + } +} + +// THE PERMISSION IS ASKED OF THE INSTALLATION THAT PERFORMS THE REQUEST. credential_authorizes answers +// for whatever authority it is given; the request is made with the controller token. So the +// authority must name the very App and installation the registration (and therefore the token) was +// minted under, or the actions:write it proves is some other installation's. An Actions job +// credential names no installation at all and cannot authorize an installation-token request. +fn dispatch_authority_refusal(authority: GitHubCredentialAuthority, app: DeclaredGitHubApp, installation: GitHubAppInstallationId) -> QualificationDispatchRefusal? { + match authority_installation(authority: authority) { + Absent => Present { value: DispatchAuthorityNotAnInstallation } + Present { value: held } => + if held.app == app && held.installation == installation { + none + } else { + Present { value: DispatchAuthorityForAnotherInstallation { authority_app: held.app, authority_installation: held.installation } } + } + } +} + +// THE INTERLOCK, as a pure comparison: the proof's admitted host against the slot's host. +fn hold_covers_slot_host(held: HostIdentity, slot_host: HostIdentity) -> Bool { + (held as String) == (slot_host as String) +} + +fn dispatch_qualification_floor( + subject: QualificationDispatchSubject, + hold: UnitHoldProof, + token: ControllerInstallationToken, + authority: GitHubCredentialAuthority, + control_plane: GitHubAppControlPlaneState, +) -> QualificationDispatch uses net: Network { + let effect = qualification_dispatch_effect(subject: subject) + if !hold_covers_slot_host(held: hold.subject.host.host, slot_host: subject.host) { + QualificationDispatchRefused { subject: subject, refusal: DispatchHoldForAnotherHost { held: hold.subject.host.host, slot: subject.host } } + } else if !token_names_registration(token_app: token.app, token_installation: token.installation, subject: subject) { + QualificationDispatchRefused { subject: subject, refusal: DispatchTokenForAnotherInstallation } + } else { + match dispatch_authority_refusal(authority: authority, app: subject.registration.app, installation: subject.registration.installation) { + Present { value: r } => QualificationDispatchRefused { subject: subject, refusal: r } + Absent => + if !credential_authorizes(authority: authority, control_plane: control_plane, effect: effect) { + QualificationDispatchRefused { + subject: subject, + refusal: DispatchCredentialRefused { unsatisfied: unsatisfied_capabilities(authority: authority, control_plane: control_plane, effect: effect) }, + } + } else { + let answer = dispatch_workflow_with( + token: token, + owner: gunbc_repository.owner as NonEmptyStr, + repo: gunbc_repository.name as NonEmptyStr, + workflow_id: qualification_workflow_file_name(), + git_ref: subject.pin.name.branch, + inputs: qualification_dispatch_inputs(attempt: subject.attempt, revision: subject.pin.revision), + ) + match qualification_dispatch_standing(dispatch: answer.dispatch) { + DispatchStandingSucceeded { receipt: r } => QualificationDispatched { run: DispatchedQualificationRun { subject: subject, receipt: r } } + DispatchStandingRefused { status: s, body: b } => QualificationDispatchRefused { subject: subject, refusal: DispatchStatusRefused { status: s, body: b } } + DispatchStandingCommitAmbiguous { detail: d } => QualificationDispatchCommitAmbiguous { subject: subject, detail: d } + } + } + } + } +} + +// ── COLLECT: THE RUN READ BACK, ENSURE-STYLE ────────────────────────────────────────────────── +// +// THE SUBJECT IS THE DISPATCHED RUN AT ITS FIRST ATTEMPT. A dispatch creates attempt 1; a re-run +// reuses the run id and mints attempt 2 with new jobs and a new conclusion. So the run read must +// carry the dispatched id, the workflow_dispatch event, the qualification workflow's path, the pinned +// revision and run_attempt 1; the jobs are read through the attempt-scoped endpoint for attempt 1 +// and every one must carry that run id and attempt. A run that has advanced past attempt 1 refuses: +// its conclusion is no longer the dispatch's. +// +// THE RUNNER IS JOINED BY IDENTITY, NOT BY LABEL. Two runners can carry the same labels, and a +// helper job on the attempt's runner says nothing about where the floor ran. So the collection takes +// the one job whose runner_name is the registration's minted name (job_ran_on), and requires it to +// be the floor job the subject fixed, and to have started. An ephemeral JIT runner takes exactly one +// job, so no job on it, several, or a different job are each a typed refusal carrying what was seen. +// +// THE CONCLUSION IS READ BACK AND CARRIED, NOT FILTERED: a failed floor on the attempt's runner is +// still a run of this host. The collected payload keeps the sealed dispatch and the whole observed +// WorkflowRun, so extraction and assessment read the revision, workflow, event and attempt from +// here rather than re-reading GitHub. + +type QualificationRunRefusal + = RunReadUnreadable { refusal: RestExchangeRefusal } + | RunCollectedUnderAnotherInstallation { token_app: DeclaredGitHubApp, token_installation: GitHubAppInstallationId } + | RunSubjectMismatch { observed_run_id: Int, observed_event: String, observed_path: String?, foreign_jobs: List } + | RunAdvancedPastDispatchedAttempt { observed_attempt: Int } + | RunRevisionNotPinned { pinned: CommitSha, observed: CommitSha } + | RunOnAnotherBranch { pinned: NonEmptyStr, observed: String? } + | RunNotCompleted { status: WorkflowRunStatus } + | RunCompletedWithoutConclusion + | RunJobsUnreadable { refusal: RestExchangeRefusal } + | RunJobsTruncated { returned: Int, total: Int } + | RunFloorJobNotUnique { floor_job_name: NonEmptyStr, matching: Int } + | RunNeverReachedAttemptRunner { registered_runner_id: Int, runner_ids_seen: List } + | RunRunnerNameDisagrees { registered_runner_id: Int, registered_runner: NonEmptyStr, observed_runner_name: String? } + | RunRegisteredRunnerRanAnotherJob { registered_runner: NonEmptyStr, job_name: String } + | RunFloorJobNotStarted { job_id: Int } + +// INSTRUMENT EXTRACTION IS A DECLARED FRONTIER, carried on the collected arm as the instruments the +// run was read for and not yet extracted from (qualification_instrument_extraction_frontier_rows). +type CollectedQualificationRun sole_constructor { + dispatched: DispatchedQualificationRun + run: WorkflowRun + floor_job: WorkflowJobRun + conclusion: WorkflowRunConclusion + instruments_unextracted: List +} + +type QualificationRunCollection + = QualificationRunCollected { collected: CollectedQualificationRun } + | QualificationRunRefused { run_id: Int, refusal: QualificationRunRefusal } + +data dispatched_run_attempt: Int = 1 + +fn optional_text_is(o: String?, expected: String) -> Bool { + match o { Present { value: v } => v == expected Absent => false } +} + +// THE ONE JOIN FROM A JOB TO A JIT REGISTRATION: the runner GitHub reports took the job is the +// name the authorized mint fixed (gunbc.runner.runner_jit_deregistration JitRegistration name). +// Labels cannot make this join -- two runners can carry identical labels. +fn job_ran_on(job: WorkflowJobRun, runner_id: Int) -> Bool { + match job.runner_id { Present { value: v } => v == runner_id Absent => false } +} + +fn job_started(job: WorkflowJobRun) -> Bool { + match job.started_at { Present { value: _ } => true Absent => false } +} + +// THE DECISION, WITHOUT I/O, over what was read. Its verdict carries the evidence and no sealed +// payload: minting CollectedQualificationRun is collect_qualification_run's alone, so this fold is +// open to supplied readbacks and has no success constructor to proxy. +type QualificationRunVerdict + = RunVerdictCollected { run: WorkflowRun, floor_job: WorkflowJobRun, conclusion: WorkflowRunConclusion } + | RunVerdictRefused { refusal: QualificationRunRefusal } + +// WHAT THE READBACK IS JUDGED AGAINST, as a plain value: the runner name the registration minted, +// the floor job the subject fixed, and the pinned revision. collect_qualification_run derives it from +// the sealed subject (qualification_run_expectation); a claim supplies it directly. +type QualificationRunExpectation { + registered_runner_id: Int + registered_runner: NonEmptyStr + floor_job_name: NonEmptyStr + revision: CommitSha + branch: NonEmptyStr +} + +fn qualification_run_expectation(subject: QualificationDispatchSubject) -> QualificationRunExpectation { + QualificationRunExpectation { + registered_runner_id: subject.runner_id, + registered_runner: subject.registration.name.value, + floor_job_name: subject.floor_job_name, + revision: subject.pin.revision, + branch: subject.pin.name.branch, + } +} + +fn decide_floor_job(subject: QualificationRunExpectation, run: WorkflowRun, conclusion: WorkflowRunConclusion, jobs: List) -> QualificationRunVerdict { + let on_runner = jobs |> filter(j => job_ran_on(job: j, runner_id: subject.registered_runner_id)) + match first(on_runner) { + Absent => RunVerdictRefused { refusal: RunNeverReachedAttemptRunner { registered_runner_id: subject.registered_runner_id, runner_ids_seen: jobs |> map(j => j.runner_id) } } + Present { value: job } => + if count(on_runner) != 1 { + RunVerdictRefused { refusal: RunFloorJobNotUnique { floor_job_name: subject.floor_job_name, matching: count(on_runner) } } + } else if !optional_text_is(o: job.runner_name, expected: subject.registered_runner as String) { + RunVerdictRefused { refusal: RunRunnerNameDisagrees { registered_runner_id: subject.registered_runner_id, registered_runner: subject.registered_runner, observed_runner_name: job.runner_name } } + } else if job.name != (subject.floor_job_name as String) { + RunVerdictRefused { refusal: RunRegisteredRunnerRanAnotherJob { registered_runner: subject.registered_runner, job_name: job.name } } + } else if !job_started(job: job) { + RunVerdictRefused { refusal: RunFloorJobNotStarted { job_id: job.id } } + } else { + RunVerdictCollected { run: run, floor_job: job, conclusion: conclusion } + } + } +} + +fn decide_qualification_run( + subject: QualificationRunExpectation, + run_id: Int, + run_read: RestResult, + jobs_read: RestResult, +) -> QualificationRunVerdict { + match run_read { + RestAnswered { answer: run } => + if run.id != run_id || run.event != "workflow_dispatch" || !optional_text_is(o: run.path, expected: qualification_workflow_path() as String) { + RunVerdictRefused { refusal: RunSubjectMismatch { observed_run_id: run.id, observed_event: run.event, observed_path: run.path, foreign_jobs: [] } } + } else if run.run_attempt != dispatched_run_attempt { + RunVerdictRefused { refusal: RunAdvancedPastDispatchedAttempt { observed_attempt: run.run_attempt } } + } else if !optional_text_is(o: run.head_branch, expected: subject.branch as String) { + RunVerdictRefused { refusal: RunOnAnotherBranch { pinned: subject.branch, observed: run.head_branch } } + } else if (run.head_sha as String) != (subject.revision as String) { + RunVerdictRefused { refusal: RunRevisionNotPinned { pinned: subject.revision, observed: run.head_sha } } + } else { + match run.status { + Completed => + match run.conclusion { + Absent => RunVerdictRefused { refusal: RunCompletedWithoutConclusion } + Present { value: conclusion } => + match jobs_read { + RestAnswered { answer: jobs } => + if count(jobs.jobs) != jobs.total_count { + RunVerdictRefused { refusal: RunJobsTruncated { returned: count(jobs.jobs), total: jobs.total_count } } + } else { + let foreign = jobs.jobs |> filter(j => j.run_id != run_id || j.run_attempt != dispatched_run_attempt) |> map(j => j.id) + if count(foreign) != 0 { + RunVerdictRefused { refusal: RunSubjectMismatch { observed_run_id: run.id, observed_event: run.event, observed_path: run.path, foreign_jobs: foreign } } + } else { + decide_floor_job(subject: subject, run: run, conclusion: conclusion, jobs: jobs.jobs) + } + } + RestRefused { refusal: r } => RunVerdictRefused { refusal: RunJobsUnreadable { refusal: classify_rest_refusal(standing: RestReadExchange { refusal: r }) } } + } + } + other => RunVerdictRefused { refusal: RunNotCompleted { status: other } } + } + } + RestRefused { refusal: r } => RunVerdictRefused { refusal: RunReadUnreadable { refusal: classify_rest_refusal(standing: RestReadExchange { refusal: r }) } } + } +} + +// THE READBACK IS PERFORMED UNDER THE INSTALLATION THAT DISPATCHED. A sealed controller token for some +// other App or installation could read a run and report it as installation A's; the token is joined +// to the registration before either read, exactly as at dispatch. +fn token_names_registration(token_app: DeclaredGitHubApp, token_installation: GitHubAppInstallationId, subject: QualificationDispatchSubject) -> Bool { + token_app == subject.registration.app && token_installation == subject.registration.installation +} + +// THE COLLECTION'S ADMISSION IS A PLAN, DECIDED WITHOUT I/O: the reads it will make, or the refusal +// that makes none. collect_qualification_run performs exactly the planned reads and nothing else, so +// "a token for another App or installation reads nothing" is a claim about this pure function a +// witness executes over a really minted subject (test.claim.runner_qualification_dispatch_witness +// the_real_mint_admits_the_attempt_through_the_sealed_subject), not a property of an effectful path +// no test can reach. +type QualificationCollectionRead + = ReadQualificationRun { run_id: Int } + | ReadQualificationAttemptJobs { run_id: Int, attempt: Int } + +type QualificationCollectionPlan + = CollectionRefusedBeforeAnyRead { refusal: QualificationRunRefusal } + | CollectionReadsPlanned { run_id: Int, attempt: Int } + +fn plan_qualification_collection(subject: QualificationDispatchSubject, run_id: Int, token_app: DeclaredGitHubApp, token_installation: GitHubAppInstallationId) -> QualificationCollectionPlan { + if !token_names_registration(token_app: token_app, token_installation: token_installation, subject: subject) { + CollectionRefusedBeforeAnyRead { + refusal: RunCollectedUnderAnotherInstallation { token_app: token_app, token_installation: token_installation }, + } + } else { + CollectionReadsPlanned { run_id: run_id, attempt: dispatched_run_attempt } + } +} + +fn planned_collection_reads(plan: QualificationCollectionPlan) -> List { + match plan { + CollectionRefusedBeforeAnyRead { refusal: _ } => [] + CollectionReadsPlanned { run_id: id, attempt: n } => + [ReadQualificationRun { run_id: id }, ReadQualificationAttemptJobs { run_id: id, attempt: n }] + } +} + +// ONE EFFECTFUL ENTRY, AND IT PERFORMS ONLY WHAT THE PLAN NAMES: the reads take their run id and +// attempt from the CollectionReadsPlanned arm, and the refusal arm reaches no read. The reads and the +// mint of CollectedQualificationRun live in that arm, so there is no second function that reads under +// an unchecked token (a split helper was exactly that bypass). +fn collect_qualification_run(dispatched: DispatchedQualificationRun, token: ControllerInstallationToken) -> QualificationRunCollection uses net: Network { + match plan_qualification_collection( + subject: dispatched.subject, run_id: dispatched.receipt.workflow_run_id, + token_app: token.app, token_installation: token.installation, + ) { + CollectionRefusedBeforeAnyRead { refusal: r } => + QualificationRunRefused { run_id: dispatched.receipt.workflow_run_id, refusal: r } + CollectionReadsPlanned { run_id: run_id, attempt: attempt } => { + let owner = gunbc_repository.owner as NonEmptyStr + let repo = gunbc_repository.name as NonEmptyStr + let read = read_run_with(token: token, owner: owner, repo: repo, run_id: run_id) + let jobs = read_attempt_jobs_with(token: token, owner: owner, repo: repo, run_id: run_id, attempt: attempt) + match decide_qualification_run( + subject: qualification_run_expectation(subject: dispatched.subject), + run_id: run_id, + run_read: read.run, + jobs_read: jobs.jobs, + ) { + RunVerdictRefused { refusal: r } => QualificationRunRefused { run_id: run_id, refusal: r } + RunVerdictCollected { run: run, floor_job: floor, conclusion: conclusion } => + QualificationRunCollected { + collected: CollectedQualificationRun { + dispatched: dispatched, + run: run, + floor_job: floor, + conclusion: conclusion, + instruments_unextracted: qualification_instruments, + }, + } + } + } + } +} + +// THE EXTRACTION FRONTIER, NAMED AT THE CAPABILITY GRAIN. Four instruments are run outputs and are +// reached through the run's artifacts and job logs; two are not run outputs at all and their sources +// are named here so the extraction leg does not go looking for them in the run. +data qualification_instrument_extraction_frontier_rows: List = [ + frontier_row_decl( + ref: decl_ref(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "CollectedQualificationRun"), + reason: "a collected qualification run carries every qualification_instrument as unextracted: extdeps.github has no Actions artifacts or job-logs read operation, no path that follows the logs redirect or opens the artifact archive, and no parser for the [floor-phase] and [floor-cgroup] log rows. Two instruments are not run outputs: GuestIdleMeminfoAndNproc comes from the boot leg's runner-host-up readback, and ConcurrentCohortSeatWindows from product.capacity.cohort_observation seal_cohort", + dissolution: unbound_dissolution(description: "the Actions artifacts and job-logs read path (list and download a run's artifacts, download a job's log text) plus the floor row parsers are SUFFICIENT to populate FloorPhaseRows, FloorCgroupRows, ClaimCostArtifactEvalSteps and CalibrationSpecimenWitnessLine from one collected run's floor job through the producer each instrument names, with GuestIdleMeminfoAndNproc read from the boot leg's runner-host-up readback and ConcurrentCohortSeatWindows from product.capacity.cohort_observation seal_cohort, so CollectedQualificationRun carries readings for every qualification_instrument and no unextracted list. NOT satisfied by an artifacts operation with no parser, nor by a parser exercised only on a fixture"), + ) +] diff --git a/dag/gunbc/runner/runner_qualification_production_subject.dag b/dag/gunbc/runner/runner_qualification_production_subject.dag new file mode 100644 index 00000000000..0c023599e94 --- /dev/null +++ b/dag/gunbc/runner/runner_qualification_production_subject.dag @@ -0,0 +1,48 @@ +module gunbc.runner.runner_qualification_production_subject + +import std.types { NonEmptyStr } +import gunbc.fleet_converge_workflow { fleet_converge_workflow, fleet_converge_dispatch_inputs } +import gunbc.runner.runner_jit_perform { AuthorizedJitMintDispatch, JitCredentialDelivery } +import gunbc.runner.runner_qualification_ref_pin { QualificationRefPin } +import gunbc.runner.runner_qualification_dispatch { + QualificationSubjectStanding, QualificationSubjectRefused, SubjectAttemptInputUndeclared, + dispatch_inputs_declare, qualification_attempt_dispatch_input, qualification_dispatch_subject_over, +} + +// THE PRODUCTION WIRING LIVES BESIDE THE FOLD, NOT INSIDE IT. gunbc.runner.runner_qualification_dispatch +// is the pure plan/perform/readback fold; this module alone binds it to the generated fleet-converge +// model. The split is a closure cut: fleet_converge_workflow reaches the host-effect realizations +// (extdeps.gunbc shell operations a rust emission cannot realize), so a module that imports it +// drags that reach into every fixture that imports the module. Keeping the import here keeps the +// fold's closure free of it, and the one claim that inhabits the production route imports this module. +// +// THE PRODUCTION MINT: the qualification workflow is the generated fleet-converge model. +// +// THE DECLARED INPUTS ARE READ BEFORE THE WORKFLOW IS BUILT. The model's workflow_dispatch inputs are +// their own declaration (gunbc.fleet_converge_workflow fleet_converge_dispatch_inputs), and the jobs +// are built by fleet_converge_jobs(); evaluating the whole fleet_converge_workflow builds every job of +// every mode, ~600k eval steps measured by the required floor, and the first check the mint makes +// reads only the inputs. So the wrapper asks that check of the inputs declaration directly and builds +// the workflow only when the inputs declare the attempt input -- the refusal is the same +// SubjectAttemptInputUndeclared the mint would reach, without the construction it would never read. +// Until the boot leg lands the qualification mode there, this refuses -- the wiring the route leg +// owes, refused rather than faked. +fn qualification_dispatch_subject( + dispatch: AuthorizedJitMintDispatch, + delivery: JitCredentialDelivery, + floor_job_id: NonEmptyStr, + pin: QualificationRefPin, +) -> QualificationSubjectStanding { + if !dispatch_inputs_declare(inputs: fleet_converge_dispatch_inputs, input: qualification_attempt_dispatch_input) { + QualificationSubjectRefused { refusal: SubjectAttemptInputUndeclared { input: qualification_attempt_dispatch_input.name } } + } else { + qualification_dispatch_subject_over( + dispatch: dispatch, + delivery: delivery, + workflow: fleet_converge_workflow, + floor_job_id: floor_job_id, + pin: pin, + ) + } +} + diff --git a/dag/gunbc/runner/runner_qualification_ref_pin.dag b/dag/gunbc/runner/runner_qualification_ref_pin.dag new file mode 100644 index 00000000000..13f1645beab --- /dev/null +++ b/dag/gunbc/runner/runner_qualification_ref_pin.dag @@ -0,0 +1,337 @@ +module gunbc.runner.runner_qualification_ref_pin + +import std.types { Bool, CommitSha, Int, List, NonEmptyStr, String } +import std.resources { Network } +import std.decl_ref { decl_ref } +import extdeps.transports.rest { + RestResult, RestAnswered, RestRefused, RestReadExchange, RestMutationExchange, classify_rest_refusal, + RestRefusal, RestExchangeRefusal, RestExchangeStatusRefused, + RestExchangeCommitAmbiguous, RestExchangeUnreached, RestExchangeUndecodable, +} +import gunbc.repository { gunbc_repository } +import gunbc.generated_artifact { artifact_path, FleetConvergeYamlArtifact } +import gunbc.fleet.org_actions_inspection { RunnerGroupListDecode, RunnerGroupListDecoded, RunnerGroupListDecodeRefused } +import gunbc.runner_group_restriction_observation { + MicrovmRunnerGroupStanding, RunnerGroupRestrictedToWorkflow, RunnerGroupRestrictionRefused, RestrictedRunnerGroup, + observe_runner_group_restriction, +} +import gunbc.github_effect_perform { + ControllerInstallationToken, GitRefRead, read_git_ref_with, create_git_ref_with, delete_git_ref_with, + read_runner_groups_with, update_runner_group_workflows_with, +} +import extdeps.github.git_database { GitRefWire, GitRefDeletedBody } + +// THE QUALIFICATION REF PIN: ONE CREATE-ONCE BRANCH PER ATTEMPT, AND THE DEDICATED GROUP PINNED TO IT. +// +// WHY A BRANCH. The floor must run the pinned revision and nothing else, and the runner that serves +// it must accept no other code. The JIT slot registers into a runner group restricted to one +// selected workflow, and GitHub selects a dispatched (non-reusable) workflow only at a branch +// ("Pin non-reusable workflows to a branch", extdeps.github.org_actions github.OrgRunnerGroupsRest); +// a SHA or tag pin is not available to it. So the pin is a branch created for this attempt at the +// pinned revision, and the dedicated qualification group is restricted to the qualification workflow +// at THAT branch. A dispatch can then only run the revision the branch was created at, and a run on +// any other ref -- the default branch after a move, another attempt's branch -- does not match the +// group, so the attempt's runner never takes it and collection ends RunNeverReachedAttemptRunner. +// +// CREATE-ONCE. The branch is created by CreateRef, which never moves an existing ref (422 "Reference +// already exists"); a branch already present before creation is refused, never adopted or moved, +// because its revision is not one this attempt pinned. Readback must show the exact revision. +// +// CONFINED BY CONSTRUCTION. Every ref this module touches is a QualificationBranchName, minted only by +// qualification_branch_name, which admits a single path segment under refs/heads/qualification/. +// Every group write goes through a QualificationGroupWriteTarget, minted only from a read whose name +// is qualification_runner_group_name -- the DEDICATED group; no other group can be written. +// +// REMOVED ON EVERY EXIT, by readback (remove_qualification_ref_pin), the same ensure shape as +// gunbc.runner.runner_jit_deregistration: absence is read, never inferred from a delete status. +// The group stays restricted to the deleted branch's path until the next attempt pins it: no run can +// match a branch that no longer exists, so the stale entry admits nothing. +// +// AUTHORIZATION, TWO FACTS. The per-attempt branch create and delete are pre-approved by the +// operator's 2026-10-03 ruling, whose scope the operator confirmed on 2026-10-05 +// (gunbc.auth.privileged_effect_census runner_lifecycle_scope_ruling). The dedicated group's +// selected-workflow pin is NOT under that ruling: it is authorized by its own federated standing, the +// census row's parameters selected without a ruling discharge, and is limited to the dedicated +// qualification group by this module's construction. The token is the gunbai-ci installation token +// (contents:write for the ref; organization self-hosted-runners write for the group). No workflow +// fires on creating the branch: see test.claim.runner_qualification_ref_pin_witness. + +data qualification_branch_prefix: NonEmptyStr = "qualification/" + +// THE QUALIFICATION WORKFLOW IS THE GENERATED FLEET-CONVERGE WORKFLOW, and the group selects it at +// the pin branch. These live here, beside the group write that consumes them; the dispatch module +// (gunbc.runner.runner_qualification_dispatch) imports them. +fn qualification_workflow_path() -> NonEmptyStr { + artifact_path(a: FleetConvergeYamlArtifact) as NonEmptyStr +} + +// The selected-workflow spelling a restricted runner group carries (owner/repo/path@ref), the same +// form gunbc.runner_group_restriction_observation microvm_shakedown_selected_workflow derives. +fn qualification_selected_workflow(branch: NonEmptyStr) -> NonEmptyStr { + join([gunbc_repository.full_name, "/", qualification_workflow_path() as String, "@refs/heads/", branch as String], "") as NonEmptyStr +} +data qualification_runner_group_name: NonEmptyStr = "runner-qualification" + +// ── THE BRANCH NAME ───────────────────────────────────────────────────────────────────────────── + +type QualificationBranchName sole_constructor { + attempt: NonEmptyStr + branch: NonEmptyStr +} + +type QualificationBranchNameStanding + = QualificationBranchNamed { name: QualificationBranchName } + | QualificationBranchNameRefused { attempt: String, cause: NonEmptyStr } + +// ONE PATH SEGMENT UNDER THE PREFIX. An attempt label carrying a slash, a `..`, whitespace, a ref +// metacharacter or a leading dot would address a ref outside refs/heads/qualification/ or an +// invalid one, so it refuses rather than being escaped. +fn attempt_is_one_ref_segment(attempt: String) -> Bool { + string_length(s: attempt) > 0 + && !starts_with(s: attempt, prefix: ".") + && !string_contains(s: attempt, pattern: "/") + && !string_contains(s: attempt, pattern: "..") + && !string_contains(s: attempt, pattern: " ") + && !string_contains(s: attempt, pattern: "~") + && !string_contains(s: attempt, pattern: "^") + && !string_contains(s: attempt, pattern: ":") + && !string_contains(s: attempt, pattern: "?") + && !string_contains(s: attempt, pattern: "*") + && !string_contains(s: attempt, pattern: "[") + && !string_contains(s: attempt, pattern: "\\") + && !string_contains(s: attempt, pattern: "@{") + && !ends_with(s: attempt, suffix: ".lock") +} + +fn qualification_branch_name(attempt: NonEmptyStr) -> QualificationBranchNameStanding { + if attempt_is_one_ref_segment(attempt: attempt as String) { + QualificationBranchNamed { + name: QualificationBranchName { attempt: attempt, branch: concat(qualification_branch_prefix as String, attempt as String) as NonEmptyStr }, + } + } else { + QualificationBranchNameRefused { attempt: attempt as String, cause: "the attempt label is not one ref segment, so the branch would leave refs/heads/qualification/" as NonEmptyStr } + } +} + +fn branch_full_ref(name: QualificationBranchName) -> NonEmptyStr { + concat("refs/heads/", name.branch as String) as NonEmptyStr +} + +fn branch_api_ref(name: QualificationBranchName) -> NonEmptyStr { + concat("heads/", name.branch as String) as NonEmptyStr +} + +// ── THE DEDICATED GROUP ───────────────────────────────────────────────────────────────────────── + +type QualificationGroupWriteTarget sole_constructor { + group_id: Int +} + +type QualificationGroupTargetStanding + = QualificationGroupTargeted { target: QualificationGroupWriteTarget } + | QualificationGroupNotTargetable { cause: NonEmptyStr } + +// The only group that may be written is the one whose name is the dedicated qualification group's, +// found exactly once in a complete read. Any other name -- the shakedown group, Default -- refuses. +fn qualification_group_target(requested: NonEmptyStr, listed: RunnerGroupListDecode) -> QualificationGroupTargetStanding { + if (requested as String) != (qualification_runner_group_name as String) { + QualificationGroupNotTargetable { cause: concat("only the dedicated qualification group may be written; refused: ", requested as String) as NonEmptyStr } + } else { + match listed { + RunnerGroupListDecodeRefused { reason: r } => QualificationGroupNotTargetable { cause: r } + RunnerGroupListDecoded { groups: gs } => { + let rows = gs |> filter(g => (g.name as String) == (requested as String)) + match first(rows) { + Absent => QualificationGroupNotTargetable { cause: "the dedicated qualification runner group does not exist" as NonEmptyStr } + Present { value: row } => + if count(rows) != 1 { + QualificationGroupNotTargetable { cause: "the dedicated qualification runner group name is duplicated" as NonEmptyStr } + } else { + QualificationGroupTargeted { target: QualificationGroupWriteTarget { group_id: row.id } } + } + } + } + } + } +} + +// ── THE PIN ───────────────────────────────────────────────────────────────────────────────────── + +type QualificationRefPin sole_constructor { + name: QualificationBranchName + revision: CommitSha + group: RestrictedRunnerGroup +} + +type QualificationRefPinRefusal + = PinBranchNameRefused { cause: NonEmptyStr } + | PinBranchPreexisting { observed_sha: String } + | PinBranchReadUnreadable { refusal: RestExchangeRefusal } + | PinBranchCreateRefused { status: Int, body: String } + | PinBranchCreateAmbiguous { detail: NonEmptyStr } + | PinBranchReadbackMismatch { pinned: CommitSha, observed: String } + | PinGroupNotTargetable { cause: NonEmptyStr } + | PinGroupWriteNotSucceeded { refusal: RestExchangeRefusal } + | PinGroupReadbackRefused { standing: MicrovmRunnerGroupStanding } + +type QualificationRefPinStanding + = QualificationRefPinned { pin: QualificationRefPin } + | QualificationRefPinRefused { attempt: NonEmptyStr, refusal: QualificationRefPinRefusal } + +// A REFUSED READ OF THE REF IS ABSENCE ONLY WHEN GITHUB DECIDED 404; every other refusal is unreadable. +fn branch_absent(refusal: RestExchangeRefusal) -> Bool { + match refusal { + RestExchangeStatusRefused { status: s, body: _ } => (s as Int) == 404 + RestExchangeCommitAmbiguous { detail: _ } => false + RestExchangeUnreached { cause: _ } => false + RestExchangeUndecodable { status: _, cause: _ } => false + } +} + +// THE CREATE'S STANDING, decided from the mutation classifier: only a created ref proceeds to +// readback; a 422 is the create-once refusal (the ref exists); an ambiguous answer is its own arm -- +// the ref may exist, so removal is still owed. +fn branch_create_refusal(created: RestResult) -> QualificationRefPinRefusal? { + match created { + RestAnswered { answer: _ } => none + RestRefused { refusal } => + match classify_rest_refusal(standing: RestMutationExchange { refusal: refusal }) { + RestExchangeStatusRefused { status: s, body: b } => + if (s as Int) == 422 { Present { value: PinBranchPreexisting { observed_sha: "(422 Reference already exists)" } } } + else { Present { value: PinBranchCreateRefused { status: s as Int, body: b } } } + RestExchangeCommitAmbiguous { detail: d } => Present { value: PinBranchCreateAmbiguous { detail: d } } + RestExchangeUnreached { cause: c } => Present { value: PinBranchCreateAmbiguous { detail: c } } + RestExchangeUndecodable { status: _, cause: c } => Present { value: PinBranchCreateAmbiguous { detail: c } } + } + } +} + +fn ref_read_refusal(refusal: RestRefusal) -> RestExchangeRefusal { + classify_rest_refusal(standing: RestReadExchange { refusal: refusal }) +} + +// THE PIN'S ONLY MINT, over values read back. Callers are admitted by name: the effectful ensure, and +// the witness claims that supply readbacks at this interface and return Bool. +fn qualification_ref_pin_of( + name: QualificationBranchName, + revision: CommitSha, + readback: RestResult, + group: MicrovmRunnerGroupStanding, +) -> QualificationRefPinStanding + admit_callers: [ + decl_ref(module_path: "gunbc.runner.runner_qualification_ref_pin", decl_name: "ensure_qualification_ref_pin"), + decl_ref(module_path: "test.claim.runner_qualification_ref_pin_witness", decl_name: "the_pin_is_minted_only_from_the_exact_revision_and_the_pinned_group"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "the_real_mint_admits_the_attempt_through_the_sealed_subject"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "a_delivery_from_another_dispatch_on_the_same_slot_refuses"), + decl_ref(module_path: "test.claim.runner_qualification_dispatch_witness", decl_name: "the_production_mint_over_todays_fleet_converge_workflow_refuses_at_the_attempt_input"), + ] +{ + match readback { + RestAnswered { answer: observed } => + if observed.object.sha != (revision as String) { + QualificationRefPinRefused { attempt: name.attempt, refusal: PinBranchReadbackMismatch { pinned: revision, observed: observed.object.sha } } + } else { + match group { + RunnerGroupRestrictedToWorkflow { restriction: r } => + QualificationRefPinned { pin: QualificationRefPin { name: name, revision: revision, group: r } } + other => QualificationRefPinRefused { attempt: name.attempt, refusal: PinGroupReadbackRefused { standing: other } } + } + } + RestRefused { refusal } => QualificationRefPinRefused { attempt: name.attempt, refusal: PinBranchReadUnreadable { refusal: ref_read_refusal(refusal: refusal) } } + } +} + +fn pin_refused(attempt: NonEmptyStr, refusal: QualificationRefPinRefusal) -> QualificationRefPinStanding { + QualificationRefPinRefused { attempt: attempt, refusal: refusal } +} + +fn ensure_qualification_ref_pin( + token: ControllerInstallationToken, + organization: NonEmptyStr, + attempt: NonEmptyStr, + revision: CommitSha, +) -> QualificationRefPinStanding uses net: Network { + let owner = gunbc_repository.owner as NonEmptyStr + let repo = gunbc_repository.name as NonEmptyStr + match qualification_branch_name(attempt: attempt) { + QualificationBranchNameRefused { attempt: _, cause: c } => pin_refused(attempt: attempt, refusal: PinBranchNameRefused { cause: c }) + QualificationBranchNamed { name: name } => { + let before = read_git_ref_with(token: token, owner: owner, repo: repo, ref: branch_api_ref(name: name)) + match before.reference { + RestAnswered { answer: existing } => pin_refused(attempt: attempt, refusal: PinBranchPreexisting { observed_sha: existing.object.sha }) + RestRefused { refusal: read_refusal } => + if !branch_absent(refusal: ref_read_refusal(refusal: read_refusal)) { + pin_refused(attempt: attempt, refusal: PinBranchReadUnreadable { refusal: ref_read_refusal(refusal: read_refusal) }) + } else { + match branch_create_refusal(created: create_git_ref_with(token: token, owner: owner, repo: repo, full_ref: branch_full_ref(name: name), sha: revision as String)) { + Present { value: r } => pin_refused(attempt: attempt, refusal: r) + Absent => { + let after = read_git_ref_with(token: token, owner: owner, repo: repo, ref: branch_api_ref(name: name)) + let selected = qualification_selected_workflow(branch: name.branch) + match qualification_group_target(requested: qualification_runner_group_name, listed: read_runner_groups_with(token: token, organization: organization)) { + QualificationGroupNotTargetable { cause: c } => pin_refused(attempt: attempt, refusal: PinGroupNotTargetable { cause: c }) + QualificationGroupTargeted { target: t } => + match update_runner_group_workflows_with(token: token, organization: organization, runner_group_id: t.group_id, selected_workflows: [selected as String]) { + RestAnswered { answer: _ } => + qualification_ref_pin_of( + name: name, + revision: revision, + readback: after.reference, + group: observe_runner_group_restriction(name: qualification_runner_group_name, selected_workflow: selected, listed: read_runner_groups_with(token: token, organization: organization)), + ) + RestRefused { refusal: w } => pin_refused(attempt: attempt, refusal: PinGroupWriteNotSucceeded { refusal: classify_rest_refusal(standing: RestMutationExchange { refusal: w }) }) + } + } + } + } + } + } + } + } +} + +// ── REMOVAL, ON EVERY EXIT ────────────────────────────────────────────────────────────────────── + +type QualificationRefPinRemoval + = QualificationBranchRemoved { name: QualificationBranchName, deleted: Bool } + | QualificationBranchRemovalRefused { name: QualificationBranchName, cause: QualificationBranchRemovalRefusal } + +type QualificationBranchRemovalRefusal + = BranchStillPresent { observed_sha: String, delete_refusal: RestExchangeRefusal? } + | BranchReadUnreadable { refusal: RestExchangeRefusal } + +// THE VERDICT READS THE READBACK AND NOTHING ELSE: a branch is removed when a read finds it absent. +// delete_refusal is the delete's own refusal when one was sent and refused, carried only to explain a +// branch still present; it never decides the verdict. +fn classify_branch_removal(name: QualificationBranchName, readback: RestResult, deleted: Bool, delete_refusal: RestExchangeRefusal?) -> QualificationRefPinRemoval { + match readback { + RestAnswered { answer: present } => QualificationBranchRemovalRefused { name: name, cause: BranchStillPresent { observed_sha: present.object.sha, delete_refusal: delete_refusal } } + RestRefused { refusal } => + if branch_absent(refusal: ref_read_refusal(refusal: refusal)) { + QualificationBranchRemoved { name: name, deleted: deleted } + } else { + QualificationBranchRemovalRefused { name: name, cause: BranchReadUnreadable { refusal: ref_read_refusal(refusal: refusal) } } + } + } +} + +fn delete_refusal_of(deleted: RestResult) -> RestExchangeRefusal? { + match deleted { + RestAnswered { answer: _ } => none + RestRefused { refusal } => Present { value: classify_rest_refusal(standing: RestMutationExchange { refusal: refusal }) } + } +} + +fn remove_qualification_ref_pin(token: ControllerInstallationToken, name: QualificationBranchName) -> QualificationRefPinRemoval uses net: Network { + let owner = gunbc_repository.owner as NonEmptyStr + let repo = gunbc_repository.name as NonEmptyStr + let before = read_git_ref_with(token: token, owner: owner, repo: repo, ref: branch_api_ref(name: name)) + match before.reference { + RestAnswered { answer: _ } => { + let delete = delete_git_ref_with(token: token, owner: owner, repo: repo, ref: branch_api_ref(name: name)) + let after = read_git_ref_with(token: token, owner: owner, repo: repo, ref: branch_api_ref(name: name)) + classify_branch_removal(name: name, readback: after.reference, deleted: true, delete_refusal: delete_refusal_of(deleted: delete)) + } + RestRefused { refusal } => classify_branch_removal(name: name, readback: RestRefused { refusal: refusal }, deleted: false, delete_refusal: none) + } +} diff --git a/dag/gunbc/runner/runner_throughput_qualification_route.dag b/dag/gunbc/runner/runner_throughput_qualification_route.dag index 6cbd6a16c41..0a3ddabe687 100644 --- a/dag/gunbc/runner/runner_throughput_qualification_route.dag +++ b/dag/gunbc/runner/runner_throughput_qualification_route.dag @@ -34,8 +34,9 @@ import gunbc.runner_throughput_qualification { // payload as a parameter) but nothing builds the derived runner image. The boot leg has no authority, and not for want of a landing: // the boot run on main (`gunbc.machine_intake_mtcollins1_boot_run`) boots exactly two media, the // census image and the stock installer, and its terminal is the census program's, so it cannot boot a -// runner and observe it ready. `extdeps.github.workflows CreateDispatch` has no production caller -// and a heal-specific input contract. The registration and deregistration legs have implemented authorities that nothing on the route calls yet. Each unbound leg names the CAPABILITY missing now and what it must be SUFFICIENT FOR +// runner and observe it ready. The registration, dispatch and deregistration legs have implemented +// authorities that nothing on the route calls yet. Each unbound leg names the CAPABILITY missing now +// and what it must be SUFFICIENT FOR // (section 4b(3)), never a pull request, because a pull request can merge while the capability stays // missing -- which is exactly what happened to the boot leg. @@ -229,15 +230,16 @@ data mtcollins1_image_leg: RouteLegStanding = LegAuthorityImplemented { // listing, with the host-side teardown carried by gunbc.runner.runner_teardown_receipt // RunnerTeardownRequest over a host-unit inventory. Both are pre-approved under the dispatching // run's authorization (operator ruling 2026-10-03), rowed in gunbc.auth.privileged_effect_census. -// Dispatch names the cited REST operation that has no production caller yet. +// Dispatch is gunbc.runner.runner_qualification_dispatch dispatch_qualification_floor: CreateDispatch +// with the attempt label as the workflow input, under the same run's authorization. data mtcollins1_registration_leg: RouteLegStanding = LegAuthorityImplemented { authority: decl_ref(module_path: "gunbc.runner.runner_jit_perform", decl_name: "dispatch_jit_mint"), wiring_owed: "a production fold on this route that binds gunbc.runner.runner_host_unit_slot host_unit_slot_for to the booted managed host, mints under an observed runner group restricted to the qualification workflow and performs it through gunbc.github_effect_perform perform_organization_jit_mint; SUFFICIENT FOR one ephemeral registration per attempt label actually existing in the organization when the route runs" as NonEmptyStr, } -data mtcollins1_dispatch_leg: RouteLegStanding = LegAwaitingAuthority { - lands_with: "a production fold calling extdeps.github.workflows github.Workflows CreateDispatch for the qualification workflow with the attempt label as its input -- which also dissolves that module's create_dispatch_unconsumed_frontier_rows" as NonEmptyStr, - sufficient_for: "dispatching the floor to the one registration whose runs-on names the attempt label, so the run is unservicable by any other runner" as NonEmptyStr, +data mtcollins1_dispatch_leg: RouteLegStanding = LegAuthorityImplemented { + authority: decl_ref(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "dispatch_qualification_floor"), + wiring_owed: "the gunbc.fleet_converge_workflow mode that lands with the boot leg: a floor job in fleet_converge_workflow whose runs-on is exactly the qualification_attempt_dispatch_input it declares and whose first step is qualification_floor_revision_guard_step over the declared qualification_revision_dispatch_input, with no step that runs past a failure, and a route fold that takes the slot host's unit hold, ensures the per-attempt pin (gunbc.runner.runner_qualification_ref_pin ensure_qualification_ref_pin: branch qualification/ at the revision, the dedicated group pinned to it), mints the registration into that group, builds qualification_dispatch_subject from the pin, calls dispatch_qualification_floor and then collect_qualification_run, reconciling a commit-ambiguous dispatch before any retry, and removes the pin on every exit; SUFFICIENT FOR the floor run of each attempt being served only by the runner minted for that attempt at the pinned revision and read back as collected or as a typed refusal" as NonEmptyStr, } data mtcollins1_deregistration_leg: RouteLegStanding = LegAuthorityImplemented { diff --git a/dag/test/claim/authorization_pattern_selection_witness_test.dag b/dag/test/claim/authorization_pattern_selection_witness_test.dag index 6697a259935..eed3ee074f7 100644 --- a/dag/test/claim/authorization_pattern_selection_witness_test.dag +++ b/dag/test/claim/authorization_pattern_selection_witness_test.dag @@ -10,7 +10,7 @@ import gunbc.auth.authorization_pattern_selection { MintsNoCredential, MintsResourceScopedCredential, MintsAccountWideCredential, ReversibleByReapply, IrreversibleEffect, BillsExternally, NoBillingConsequence, - NoWitnessDischarge, + NoWitnessDischarge, StandingRulingUnderInterlock, WitnessDischarge, InterlockedBy, FederatedScopedGrant, OperatorApprovedCapability, HumanOnlyStep, OperatorOwnSession, PastedOperatorToken, PatternSelected, ManualStepRequired, NoAdmissiblePattern, PatternSelectionNeedsEvidence, PatternSelectionNeedsPolicy, PatternSelectionRefused, @@ -24,13 +24,14 @@ import gunbc.auth.privileged_effect_census { site_verdict, Conforms, DivergesWithReason, Diverges, SiteNotDecidable, mtcollins1_boot_effect, privileged_effect_interlocks, interlocked_sites_missing_from_census, rulings_without_a_rostered_interlock, ruling_roots_missing_from_census, census_sites_outside_ruling_roots, + runner_lifecycle_scope_ruling, runner_lifecycle_operator_ruling, OperatorScopeRuling, ruling_discharge_for, RealizedFederatedGrant, RealizedRunSelected, RealizedApprovalCapability, RealizedHumanStep, RealizedOperatorSession, RealizedUnauthorized, } import std.human_intervention { HumanIntervention, HumanInterventionIdentity, FleetOnce, DeviceOnce, EveryProvision, BreakGlassOnly, NoDischargeSiteModeled, } -import std.decl_ref { declaration_ref_eq, declaration_ref_display_key } +import std.decl_ref { decl_ref, declaration_ref_eq, declaration_ref_display_key } import std.types { NonEmptyStr, String, Int, List } import std.logic { Bool } @@ -390,18 +391,78 @@ test fn every_root_of_the_standing_ruling_is_a_conforming_census_row() -> Bool { && any(privileged_effect_interlocks, i => declaration_ref_display_key(ref: i.site) == "gunbc.host_reset_return_run::host_reset_return_wet") } -// THE 2026-10-03 PRE-APPROVAL IS A SELECTION, NOT A NEW VOCABULARY. JIT deregistration is a -// recurring automated effect under the dispatching run's federated identity, so the selection must +// THE 2026-10-03 PRE-APPROVAL IS A SELECTION, NOT A NEW VOCABULARY. JIT registration, +// deregistration, the qualification dispatch and its per-attempt branch pin are each a +// recurring automated effect under the dispatching run's federated identity (the pin and its removal +// on their own parameters, with no ruling discharge), so the selection must // answer the federated scoped grant and the row must conform; rowing it as an approval capability or // a per-registration ntfy approval turns this red. -test fn the_jit_registration_and_deregistration_sites_select_the_federated_grant_and_conform() -> Bool { - ["dispatch_jit_mint", "ensure_jit_runner_deregistered"] |> all(name => +test fn the_jit_registration_deregistration_and_dispatch_sites_select_the_federated_grant_and_conform() -> Bool { + ["dispatch_jit_mint", "ensure_jit_runner_deregistered", "dispatch_qualification_floor", "ensure_qualification_ref_pin", "remove_qualification_ref_pin"] |> all(name => any(census_verdicts(), v => (v.site.decl_name as String) == name && selected_federated(s: v.selection) && match v.conformance { Conforms => true _ => false })) } +// THE OPERATOR'S SCOPE RULING IS THE ONE SOURCE OF WHERE THE RUNNER-LIFECYCLE DISCHARGE MAY APPLY: a +// census row takes it only when covers names its site, and every covered site is a census row. The +// red is a row claiming the ruling outside the operator's scope, or a covers entry naming no site. A +// covered row that does not consume the discharge is admitted: the selection federates it on its own +// parameters, so it owes no interlock (the converse direction is not a wall, by design). +fn discharged_by_runner_lifecycle_ruling(d: WitnessDischarge) -> Bool { + match d { + NoWitnessDischarge => false + StandingRulingUnderInterlock { ruling: g } => (g.ruling_text as String) == (runner_lifecycle_operator_ruling.ruling_text as String) + } +} + +test fn a_row_takes_the_runner_lifecycle_ruling_only_where_the_operator_scope_ruling_covers_it() -> Bool { + privileged_effect_census |> all(r => + !discharged_by_runner_lifecycle_ruling(d: r.effect.witness_discharge) + || any(runner_lifecycle_scope_ruling.covers, c => declaration_ref_eq(a: c, b: r.site))) + && runner_lifecycle_scope_ruling.covers |> all(c => any(privileged_effect_census, r => declaration_ref_eq(a: c, b: r.site))) +} + +// THE DISPATCH'S COVERAGE IS THE OPERATOR'S 2026-10-05 SCOPE RULING, NOT THE 10-03 TEXT. The census +// row's discharge reads runner_lifecycle_scope_ruling; narrowed to registration and deregistration -- +// the 10-03 ruling's own words -- the same irreversible dispatch effect is no longer discharged and +// the selection stops answering the federated grant. The 10-03 text is unchanged either way, and its +// interlock is the host-generic unit hold. +test fn the_dispatch_is_federated_only_while_the_scope_ruling_names_it() -> Bool { + let row = first(filter(privileged_effect_census, r => (r.site.decl_name as String) == "dispatch_qualification_floor")) + let narrowed = OperatorScopeRuling { + ruling: runner_lifecycle_operator_ruling, + scope_text: "narrowed to the 2026-10-03 ruling's own words" as NonEmptyStr, + decided_on: runner_lifecycle_scope_ruling.decided_on, + decided_through: runner_lifecycle_scope_ruling.decided_through, + covers: [ + decl_ref(module_path: "gunbc.runner.runner_jit_perform", decl_name: "dispatch_jit_mint"), + decl_ref(module_path: "gunbc.runner.runner_jit_deregistration", decl_name: "ensure_jit_runner_deregistered"), + ], + } + (runner_lifecycle_scope_ruling.decided_through as String) == "escalation msg_5756a200-fcb5-470a-87eb-40867bfe9cdb" + && match runner_lifecycle_operator_ruling.interlock { + InterlockedBy { hold: h } => (h.decl_name as String) == "UnitHoldProof" && (h.module_path as String) == "gunbc.managed_host_unit_hold" + _ => false + } + && match row { + Present { value: r } => + selected_federated(s: select_authorization_pattern(e: r.effect)) + && !selected_federated(s: select_authorization_pattern(e: PrivilegedEffect { + subject: r.effect.subject, + frequency: r.effect.frequency, + reversibility: r.effect.reversibility, + surface: r.effect.surface, + workload_identity: r.effect.workload_identity, + minted_reach: r.effect.minted_reach, + billing: r.effect.billing, + witness_discharge: ruling_discharge_for(scope: narrowed, site_ref: r.site), + })) + Absent => false + } +} + // THE R2 MINT CUSTODY CELLS ARE REALIZED BY THE FEDERATED GCP IAM ROUTE, NOT AN OPERATOR SESSION: // no census site remains in gunbc.cloudflare.r2_mint_secret_access (its gcloud converges were // deleted), and the gcp-iam-converge apply site that now grants them is a federated grant naming the diff --git a/dag/test/claim/github_app_registry_witness_test.dag b/dag/test/claim/github_app_registry_witness_test.dag index 2c6568c0a91..e94441897bd 100644 --- a/dag/test/claim/github_app_registry_witness_test.dag +++ b/dag/test/claim/github_app_registry_witness_test.dag @@ -1308,17 +1308,13 @@ test fn witness_a_minted_credential_is_bound_to_the_dispatched_attempt() -> Bool ) jit_credential_delivered(delivery: delivery) && match delivery { - JitCredentialBoundToAttempt { - slot: a, - credential: c, - runner_id: id, - } => + JitCredentialBoundToAttempt { bound: b } => match dispatched(owned: true, perms: runner_grant) { - JitMintDispatchAuthorized { dispatch: d } => a == d.slot + JitMintDispatchAuthorized { dispatch: d } => b.dispatch.slot == d.slot && b.dispatch == d _ => false } - && (c.encoded as String) == "ZmFrZS1qaXQtY29uZmln" - && id == 4242 + && (b.credential.encoded as String) == "ZmFrZS1qaXQtY29uZmln" + && b.runner_id == 4242 _ => false } } diff --git a/dag/test/claim/github_effect_perform_witness_test.dag b/dag/test/claim/github_effect_perform_witness_test.dag index b03664687eb..e175d7871a6 100644 --- a/dag/test/claim/github_effect_perform_witness_test.dag +++ b/dag/test/claim/github_effect_perform_witness_test.dag @@ -102,8 +102,8 @@ data created_body: JitConfigCreatedBody = JitConfigCreatedBody { test fn witness_generate_step_delivers_refuses_or_reports_ambiguity_by_what_github_answered() -> Bool { let d = dispatched(owned: true, perms: runner_grant) let delivered = match jit_mint_performance_of_generate(dispatch: d, outcome: RestAnswered { answer: created_body }) { - JitMintReceived { delivery: JitCredentialBoundToAttempt { slot: _, credential: c, runner_id: id } } => - (c.encoded as String) == "ZmFrZS1qaXQtY29uZmln" && id == 4242 + JitMintReceived { delivery: JitCredentialBoundToAttempt { bound: b } } => + (b.credential.encoded as String) == "ZmFrZS1qaXQtY29uZmln" && b.runner_id == 4242 _ => false } let conflicted = match jit_mint_performance_of_generate( diff --git a/dag/test/claim/public_workload_census_witness_test.dag b/dag/test/claim/public_workload_census_witness_test.dag index f54a2b9beb4..4fe3d2b016b 100644 --- a/dag/test/claim/public_workload_census_witness_test.dag +++ b/dag/test/claim/public_workload_census_witness_test.dag @@ -74,6 +74,8 @@ data candidate_biome_blob_mismatch_control: WorkloadCandidate = WorkloadCandidat status: Completed, conclusion: Present { value: Success }, labels: ["depot-ubuntu-24.04-arm-16"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:32Z" }, completed_at: Present { value: "2026-09-04T16:08:13Z" }, @@ -123,6 +125,8 @@ data candidate_biome_matrix_selector_mismatch_control: WorkloadCandidate = Workl status: Completed, conclusion: Present { value: Success }, labels: ["depot-ubuntu-24.04-arm-16"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:32Z" }, completed_at: Present { value: "2026-09-04T16:08:13Z" }, @@ -178,6 +182,8 @@ data candidate_pdns_axis_name_mismatch_control: WorkloadCandidate = WorkloadCand status: Completed, conclusion: Present { value: Success }, labels: ["ubuntu-24.04-arm"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T09:57:28Z" }, completed_at: Present { value: "2026-09-04T10:07:09Z" }, @@ -238,6 +244,8 @@ data candidate_pdns_axis_name_swap_control: WorkloadCandidate = WorkloadCandidat status: Completed, conclusion: Present { value: Success }, labels: ["ubuntu-24.04-arm"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T09:57:28Z" }, completed_at: Present { value: "2026-09-04T10:07:09Z" }, @@ -291,6 +299,8 @@ data candidate_biome_job_key_mismatch_control: WorkloadCandidate = WorkloadCandi status: Completed, conclusion: Present { value: Success }, labels: ["depot-ubuntu-24.04-arm-16"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:32Z" }, completed_at: Present { value: "2026-09-04T16:08:13Z" }, @@ -339,6 +349,8 @@ data candidate_biome_job_key_titlecase_uninspected_control: WorkloadCandidate = status: Completed, conclusion: Present { value: Success }, labels: ["depot-ubuntu-24.04-arm-16"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:32Z" }, completed_at: Present { value: "2026-09-04T16:08:13Z" }, @@ -387,6 +399,8 @@ data candidate_biome_multi_label_control: WorkloadCandidate = WorkloadCandidate status: Completed, conclusion: Present { value: Success }, labels: ["self-hosted", "linux", "arm64"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:32Z" }, completed_at: Present { value: "2026-09-04T16:08:13Z" }, @@ -435,6 +449,8 @@ data candidate_empty_labels_control: WorkloadCandidate = WorkloadCandidate { status: Completed, conclusion: Present { value: Success }, labels: [], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:32Z" }, completed_at: Present { value: "2026-09-04T16:08:13Z" }, @@ -483,6 +499,8 @@ data candidate_absent_conclusion_control: WorkloadCandidate = WorkloadCandidate status: Completed, conclusion: Absent, labels: ["depot-ubuntu-24.04-arm-16"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:32Z" }, completed_at: Present { value: "2026-09-04T16:08:13Z" }, @@ -531,6 +549,8 @@ data candidate_run_attempt_zero_control: WorkloadCandidate = WorkloadCandidate { status: Completed, conclusion: Present { value: Success }, labels: ["depot-ubuntu-24.04-arm-16"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:32Z" }, completed_at: Present { value: "2026-09-04T16:08:13Z" }, @@ -579,6 +599,8 @@ data candidate_empty_matrix_axes_control: WorkloadCandidate = WorkloadCandidate status: Completed, conclusion: Present { value: Success }, labels: ["depot-ubuntu-24.04-arm-16"], + runner_id: none, + runner_name: none, created_at: Absent, started_at: Present { value: "2026-09-04T16:03:32Z" }, completed_at: Present { value: "2026-09-04T16:08:13Z" }, diff --git a/dag/test/claim/runner/runner_attempt_launch_witness_test.dag b/dag/test/claim/runner/runner_attempt_launch_witness_test.dag index 962d432e01d..20c0fd288c1 100644 --- a/dag/test/claim/runner/runner_attempt_launch_witness_test.dag +++ b/dag/test/claim/runner/runner_attempt_launch_witness_test.dag @@ -1,5 +1,11 @@ module test.claim.runner_attempt_launch_witness +import gunbc.runner.runner_jit_perform { JitMintDispatchAuthorized, JitMintDispatchRefused, dispatch_jit_mint, receive_jit_mint } +import gunbc.runner_jit_mint { MicroVmSlotBinding } +import gunbc.runner_microvm_attempt { bind_owned_attempt } +import gunbc.runner.runner_jit_admission { jit_admission_axis_standing, AttemptBindingAxis } +import test.claim.github_app_registry { app_credential, observed_grant, runner_grant, gunbai_org_ref, restricted_group_1 } +import extdeps.github.actions_jit_runner { jit_config_mint_outcome } import gunbc.runner_attempt_launch { GitHubLaunchPayload, launch_payload_device } import std.types { String, Bool, Int, List, NonEmptyStr } @@ -135,18 +141,40 @@ fn minted_credential(encoded: String) -> List { // something that is not a whole credential, handed on as if it were. data short_blob: String = "ZmFrZS1qaXQtY29uZmln" -fn received_for(attempt: MicroVmAttempt, encoded: String) -> JitMintPerformance { - match minted_credential(encoded: encoded) { - Cons { head: c, tail: _ } => +// THE DELIVERY IS MINTED, NOT HAND-BUILT, AND IT NEVER LEAVES THIS FUNCTION. A successful delivery is +// a sealed BoundJitCredential that only receive_jit_mint constructs, carrying the authorized dispatch +// that produced it; this fixture takes the real route for the credential's attempt -- an owned cell +// binding, dispatch_jit_mint and receive_jit_mint over upstream's own 201 outcome fold, both of which +// admit this function by name -- and hands back only the PLAN the planner built from it. A fixture +// that returned the delivery would be a public proxy for the mint (an admitted call edge does not +// confine a value the caller hands back), so a plan, which carries no delivery, is the only egress. +// minted_for differs from attempt in the claim about a credential bound to a sibling attempt. +fn planned_with( + pair: IssuedPair, + account: MoneyAccount, + attempt: MicroVmAttempt, + minted_for: MicroVmAttempt, + encoded: String, + ground: AttemptGround, +) -> AttemptLaunchPlan { + let mint = match dispatch_jit_mint( + binding: MicroVmSlotBinding { binding: bind_owned_attempt(attempt: minted_for, owned: true) }, + authority: app_credential, + control_plane: observed_grant(perms: runner_grant), + organization: gunbai_org_ref, + runner_group: restricted_group_1(), + attempt_binding: jit_admission_axis_standing(axis: AttemptBindingAxis), + ) { + JitMintDispatchAuthorized { dispatch: d } => JitMintReceived { - delivery: JitCredentialBoundToAttempt { slot: MicroVmJitSlot { attempt: attempt }, credential: c, runner_id: registration_fixture_id }, + delivery: receive_jit_mint( + dispatch: JitMintDispatchAuthorized { dispatch: d }, + outcome: jit_config_mint_outcome(status: 201, encoded: encoded, runner_id: registration_fixture_id, error_body: ""), + ), } - Empty {} => JitMintAppJwtUnsigned { detail: "fixture: credential fixture did not mint" } + JitMintDispatchRefused { refusal: _ } => JitMintAppJwtUnsigned { detail: "fixture: the attempt's dispatch was refused" } } -} - -fn live_grant(attempt: MicroVmAttempt) -> JitMintPerformance { - received_for(attempt: attempt, encoded: doubled(s: "A", k: 10)) + plan_for(pair: pair, account: account, attempt: attempt, mint: mint, ground: ground) } fn plan_for( @@ -209,7 +237,7 @@ test fn a_below_floor_credential_stages_no_device_and_starts_no_vmm() -> Bool { Cons { head: pair, tail: _ } => match accepted_attempt(i: 1, id: "cred0") { Cons { head: a, tail: _ } => { - let plan = plan_for(pair: pair, account: pair.account, attempt: a, mint: received_for(attempt: a, encoded: short_blob), ground: GroundClear) + let plan = planned_with(pair: pair, account: pair.account, attempt: a, minted_for: a, encoded: short_blob, ground: GroundClear) no_device_no_vmm(plan: plan) && match refusal_of(plan: plan) { Cons { head: JitCredentialBelowFloor { bytes: n }, tail: _ } => byte_size_count(b: n) == 20 @@ -233,7 +261,7 @@ test fn a_credential_at_the_ceiling_in_code_points_but_over_it_in_bytes_is_refus match accepted_attempt(i: 7, id: "multibyte") { Cons { head: a, tail: _ } => { let wide = doubled(s: "\u{00e9}", k: 16) - let plan = plan_for(pair: pair, account: pair.account, attempt: a, mint: received_for(attempt: a, encoded: wide), ground: GroundClear) + let plan = planned_with(pair: pair, account: pair.account, attempt: a, minted_for: a, encoded: wide, ground: GroundClear) string_length(wide) == 65536 && byte_size_count(b: jit_drive_utf8_size(text: wide)) == 131072 && no_device_no_vmm(plan: plan) @@ -253,7 +281,7 @@ test fn an_above_ceiling_credential_stages_no_device_and_starts_no_vmm() -> Bool Cons { head: pair, tail: _ } => match accepted_attempt(i: 1, id: "credbig") { Cons { head: a, tail: _ } => { - let plan = plan_for(pair: pair, account: pair.account, attempt: a, mint: received_for(attempt: a, encoded: doubled(s: "A", k: 17)), ground: GroundClear) + let plan = planned_with(pair: pair, account: pair.account, attempt: a, minted_for: a, encoded: doubled(s: "A", k: 17), ground: GroundClear) no_device_no_vmm(plan: plan) && match refusal_of(plan: plan) { Cons { head: JitCredentialAboveCeiling { bytes: _ }, tail: _ } => true @@ -275,7 +303,7 @@ test fn a_credential_bound_to_another_attempt_stages_no_device() -> Bool { Cons { head: a, tail: _ } => match accepted_attempt(i: 6, id: "theirs") { Cons { head: b, tail: _ } => { - let plan = plan_for(pair: pair, account: pair.account, attempt: a, mint: live_grant(attempt: b), ground: GroundClear) + let plan = planned_with(pair: pair, account: pair.account, attempt: a, minted_for: b, encoded: doubled(s: "A", k: 10), ground: GroundClear) no_device_no_vmm(plan: plan) && match refusal_of(plan: plan) { Cons { head: JitCredentialBoundToDifferentAttempt { bound_to: other }, tail: _ } => other == MicroVmJitSlot { attempt: b } @@ -336,9 +364,9 @@ test fn an_unauthorized_grant_yields_zero_jailer_launches() -> Bool { Cons { head: pair, tail: _ } => match accepted_attempt(i: 2, id: "unauth") { Cons { head: a, tail: _ } => - match plan_for(pair: pair, account: exhausted_account, attempt: a, mint: live_grant(attempt: a), ground: GroundClear) { + match planned_with(pair: pair, account: exhausted_account, attempt: a, minted_for: a, encoded: doubled(s: "A", k: 10), ground: GroundClear) { LaunchRefusedUnauthorized { authorization: _ } => - no_device_no_vmm(plan: plan_for(pair: pair, account: exhausted_account, attempt: a, mint: live_grant(attempt: a), ground: GroundClear)) + no_device_no_vmm(plan: planned_with(pair: pair, account: exhausted_account, attempt: a, minted_for: a, encoded: doubled(s: "A", k: 10), ground: GroundClear)) _ => false } Empty {} => false @@ -352,9 +380,9 @@ test fn prior_resources_refuse_rather_than_reuse() -> Bool { Cons { head: pair, tail: _ } => match accepted_attempt(i: 3, id: "prior") { Cons { head: a, tail: _ } => - match plan_for(pair: pair, account: pair.account, attempt: a, mint: live_grant(attempt: a), ground: GroundOccupied) { + match planned_with(pair: pair, account: pair.account, attempt: a, minted_for: a, encoded: doubled(s: "A", k: 10), ground: GroundOccupied) { LaunchRefusedPriorResources => - no_device_no_vmm(plan: plan_for(pair: pair, account: pair.account, attempt: a, mint: live_grant(attempt: a), ground: GroundOccupied)) + no_device_no_vmm(plan: planned_with(pair: pair, account: pair.account, attempt: a, minted_for: a, encoded: doubled(s: "A", k: 10), ground: GroundOccupied)) _ => false } Empty {} => false @@ -378,7 +406,7 @@ test fn a_live_grant_stages_exactly_one_device_and_records_the_registration() -> Cons { head: pair, tail: _ } => match accepted_attempt(i: 4, id: "ok1") { Cons { head: a, tail: _ } => { - let plan = plan_for(pair: pair, account: pair.account, attempt: a, mint: live_grant(attempt: a), ground: GroundClear) + let plan = planned_with(pair: pair, account: pair.account, attempt: a, minted_for: a, encoded: doubled(s: "A", k: 10), ground: GroundClear) planned_jailer_launches(plan: plan) == 1 && match plan { LaunchAuthorized { @@ -550,7 +578,7 @@ fn staging_with(jit_of: Bool, obs: WorkspaceStagingObservation, ground: AttemptG Cons { head: pair, tail: _ } => match accepted_attempt(i: 2, id: "ws1") { Cons { head: a, tail: _ } => { - let plan = plan_for(pair: pair, account: pair.account, attempt: a, mint: live_grant(attempt: a), ground: ground) + let plan = planned_with(pair: pair, account: pair.account, attempt: a, minted_for: a, encoded: doubled(s: "A", k: 10), ground: ground) staging_label(v: attempt_staging_verdict( plan: plan, jail: staged_jail_material(), @@ -600,7 +628,7 @@ fn jail_label(m: JailMaterialStaging) -> String { Cons { head: pair, tail: _ } => match accepted_attempt(i: 2, id: "ws1") { Cons { head: a, tail: _ } => { - let plan = plan_for(pair: pair, account: pair.account, attempt: a, mint: live_grant(attempt: a), ground: GroundClear) + let plan = planned_with(pair: pair, account: pair.account, attempt: a, minted_for: a, encoded: doubled(s: "A", k: 10), ground: GroundClear) staging_label(v: attempt_staging_verdict( plan: plan, jail: m, @@ -652,7 +680,7 @@ fn admitted_receipt_names_this_attempts_paths() -> Bool { Cons { head: pair, tail: _ } => match accepted_attempt(i: 2, id: "ws1") { Cons { head: a, tail: _ } => { - let plan = plan_for(pair: pair, account: pair.account, attempt: a, mint: live_grant(attempt: a), ground: GroundClear) + let plan = planned_with(pair: pair, account: pair.account, attempt: a, minted_for: a, encoded: doubled(s: "A", k: 10), ground: GroundClear) match attempt_staging_verdict(plan: plan, jail: staged_jail_material(), jit: staged_device_of(plan: plan), workspace: good_workspace()) { StagingAdmitsJailer { receipt: r } => r.bootstrap_device_path == concat(attempt_jail_chroot_root(attempt: a, firecracker_binary: "/bin/firecracker"), jail_jit_path as String) diff --git a/dag/test/claim/runner/runner_microvm_slot_controller_witness_test.dag b/dag/test/claim/runner/runner_microvm_slot_controller_witness_test.dag index 58a8cd86699..46cc57310e9 100644 --- a/dag/test/claim/runner/runner_microvm_slot_controller_witness_test.dag +++ b/dag/test/claim/runner/runner_microvm_slot_controller_witness_test.dag @@ -1,5 +1,11 @@ module test.claim.runner.runner_microvm_slot_controller_witness_test +import gunbc.runner.runner_jit_perform { JitMintDispatchAuthorized, JitMintDispatchRefused, dispatch_jit_mint, receive_jit_mint } +import gunbc.runner_jit_mint { MicroVmSlotBinding } +import gunbc.runner_microvm_attempt { bind_owned_attempt } +import gunbc.runner.runner_jit_admission { jit_admission_axis_standing, AttemptBindingAxis } +import test.claim.github_app_registry { app_credential, observed_grant, runner_grant, gunbai_org_ref, restricted_group_1 } +import extdeps.github.actions_jit_runner { jit_config_mint_outcome } import v2.std.algebra { any } import std.algebra { list_append } import std.types { String, NonEmptyStr, Bool, Int, List } @@ -297,8 +303,22 @@ fn delivered_mint() -> Bool { Absent => false Present { value: a } => match jit_config_mint_outcome(status: 201, encoded: "ZmFrZS1qaXQtY29uZmlnLXRoYXQtaXMtbG9uZy1lbm91Z2gtdG8tcGFzcy10aGUtZmxvb3ItY2hlY2stZm9yLXRoZS13aXRuZXNz", runner_id: 4242, error_body: "") { - JitConfigMinted { config: c, runner_id: id } => - minted_registration(mint: JitMintReceived { delivery: JitCredentialBoundToAttempt { slot: MicroVmJitSlot { attempt: a }, credential: c, runner_id: id } }) == Present { value: 4242 } + JitConfigMinted { config: _, runner_id: _ } => + match dispatch_jit_mint( + binding: MicroVmSlotBinding { binding: bind_owned_attempt(attempt: a, owned: true) }, + authority: app_credential, + control_plane: observed_grant(perms: runner_grant), + organization: gunbai_org_ref, + runner_group: restricted_group_1(), + attempt_binding: jit_admission_axis_standing(axis: AttemptBindingAxis), + ) { + JitMintDispatchAuthorized { dispatch: d } => + minted_registration(mint: JitMintReceived { delivery: receive_jit_mint( + dispatch: JitMintDispatchAuthorized { dispatch: d }, + outcome: jit_config_mint_outcome(status: 201, encoded: "ZmFrZS1qaXQtY29uZmlnLXRoYXQtaXMtbG9uZy1lbm91Z2gtdG8tcGFzcy10aGUtZmxvb3ItY2hlY2stZm9yLXRoZS13aXRuZXNz", runner_id: 4242, error_body: ""), + ) }) == Present { value: 4242 } + JitMintDispatchRefused { refusal: _ } => false + } _ => false } } diff --git a/dag/test/claim/runner/runner_qualification_delivery_rewrap_witness_test.dag b/dag/test/claim/runner/runner_qualification_delivery_rewrap_witness_test.dag new file mode 100644 index 00000000000..a6994244df9 --- /dev/null +++ b/dag/test/claim/runner/runner_qualification_delivery_rewrap_witness_test.dag @@ -0,0 +1,77 @@ +module test.claim.runner_qualification_delivery_rewrap_witness + +import std.types { String, Bool, Int } +import extdeps.filesystem.filesystem_io +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, CompileDiagnosticCensusRow, CensusObserved, CensusNotRunnable, +} + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// THE REWRAP ROUTE, ENROLLED AS AN EXECUTED RED (DESIGN 4b: a state unrepresentable in the accepted +// corpus is still representable as source handed to the compiler). test.probe.qualification_delivery_ +// rewrap_probe relabels delivery B's credential and runner id as dispatch A's; it must refuse at +// BoundJitCredential, the sealed carrier receive_jit_mint alone constructs, so no +// QualificationDispatchSubject can ever be built over a rewrapped delivery. A control source that only +// NAMES the same types must refuse at none of them, so the refusal is attributable to the forgery. + +fn census_of(source: String) -> CompileDiagnosticCensus { + compile_dag_diagnostic_census(source) +} + +fn blocking(c: CompileDiagnosticCensus, wanted: String, subject: String) -> Int { + match c { + CensusNotRunnable { cause: _ } => -1 + CensusObserved { rows: rows } => + rows + |> filter(r => (r.diagnostic_class as String) == wanted && r.subject_name == subject && r.blocking) + |> fold(init: 0, f: (acc, r) => acc + r.count) + } +} + +data control_source: String = "module probe_qualification_delivery_control\nimport std.types { Bool }\nimport gunbc.runner.runner_jit_perform { BoundJitCredential, JitCredentialDelivery, JitCredentialBoundToAttempt, jit_credential_delivered, receive_jit_mint }\nimport gunbc.github_effect_perform { jit_mint_performance_of_generate }\nimport gunbc.runner.runner_qualification_dispatch { CollectedQualificationRun }\nfn delivered(d: JitCredentialDelivery) -> Bool { jit_credential_delivered(delivery: d) }\n" + +fn blocking_class(c: CompileDiagnosticCensus, wanted: String) -> Int { + match c { + CensusNotRunnable { cause: _ } => -1 + CensusObserved { rows: rows } => + rows + |> filter(r => (r.diagnostic_class as String) == wanted && r.blocking) + |> fold(init: 0, f: (acc, r) => acc + r.count) + } +} + +fn probe(name: String) -> CompileDiagnosticCensus { + census_of(source: filesystem_read(path: concat(concat("dag/test/probe/", name), ".dag")).content) +} + +// ONE CONTROL FOR EVERY RED BELOW: a source that IMPORTS each sealed name -- the carriers and the two +// admitted mints -- and calls none of them refuses at none of the walls, so each red is the call or +// the literal, never the import. +test fn a_source_that_only_names_the_carrier_forges_nothing() -> Bool { + let c = census_of(source: control_source) + blocking(c: c, wanted: "SoleConstructorViolation", subject: "BoundJitCredential") == 0 + && blocking_class(c: c, wanted: "SoleConstructorViolation") == 0 + && blocking_class(c: c, wanted: "ConstructorCallAdmissionRefused") == 0 +} + +// THE REWRAP WITH NO FORGED LITERAL (review 5408711178 item 1): delivery B's credential and runner id +// handed to receive_jit_mint under dispatch A. Each probe holds ONE route, so its refusal is that +// route's. +test fn a_rewrap_through_receive_jit_mint_refuses_at_its_admission() -> Bool { + blocking_class(c: probe(name: "qualification_receive_jit_mint_rewrap_probe"), wanted: "ConstructorCallAdmissionRefused") >= 1 +} + +test fn a_supplied_generate_answer_refuses_outside_the_perform_function() -> Bool { + blocking_class(c: probe(name: "qualification_generate_answer_rewrap_probe"), wanted: "ConstructorCallAdmissionRefused") >= 1 +} + +// item 2: collecting outside the token join is minting a collection the join never admitted. +test fn a_collection_minted_outside_the_token_join_refuses_at_the_sealed_carrier() -> Bool { + blocking(c: probe(name: "qualification_collection_relabel_probe"), wanted: "SoleConstructorViolation", subject: "CollectedQualificationRun") >= 1 +} + +test fn a_rewrapped_delivery_refuses_at_the_sealed_carrier() -> Bool { + blocking(c: census_of(source: filesystem_read(path: "dag/test/probe/qualification_delivery_rewrap_probe.dag").content), wanted: "SoleConstructorViolation", subject: "BoundJitCredential") >= 1 +} diff --git a/dag/test/claim/runner/runner_qualification_dispatch_witness_test.dag b/dag/test/claim/runner/runner_qualification_dispatch_witness_test.dag new file mode 100644 index 00000000000..6609ee81c9d --- /dev/null +++ b/dag/test/claim/runner/runner_qualification_dispatch_witness_test.dag @@ -0,0 +1,662 @@ +module test.claim.runner_qualification_dispatch_witness + +import std.types { Bool, CommitSha, Int, List, NonEmptyStr, String } +import std.algebra { Cons, Empty } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import product.placement_supply { HostIdentity } +import extdeps.transports.rest { + RestAnswered, RestRefused, RestRefusal, RestTransportRefused, RestStatusRefused, RestBodyUndecodable, +} +import extdeps.github.workflows { WorkflowDispatchReceipt } +import extdeps.github.git_database { GitRefWire, GitRefObjectWire } +import extdeps.github.actions { Workflow, Job, WorkflowDispatch, RunsOnExpression, SelfHosted, RunnerSpec, Step, RunStep, UsesStep } +import extdeps.github.effect { DispatchWorkflow, GitHubOrganizationRef } +import extdeps.github.workflow_runs { + WorkflowRun, WorkflowJobRun, WorkflowJobRunList, Completed, InProgress, Success, Failure, +} +import gunbc.managed_host { managed_hosts, managed_host_binding } +import gunbc.runner.runner_host_unit_slot { host_unit_slot_for } +import gunbc.runner_jit_mint { HostUnitSlotBinding } +import gunbc.runner.runner_jit_admission { jit_admission_axis_standing, AttemptBindingAxis } +import gunbc.runner.runner_jit_perform { JitMintDispatchAuthorized, JitMintDispatchRefused, dispatch_jit_mint, receive_jit_mint } +import gunbc.runner_throughput_qualification_route { ephemeral_slot_labels, ephemeral_slot_unit } +import test.claim.github_app_registry { + app_credential, other_app_credential, other_installation_credential, a_pull_request_job_credential, + bot_installation_id, other_installation_id, observed_grant, runner_grant, gunbai_org_ref, group_restricted_to, minted_outcome, +} +import gunbc.auth.github_apps { gunbai_bot_declared, gunbai_ci_declared } +import gunbc.runner_group_restriction_observation { MicrovmRunnerGroupStanding, observe_runner_group_restriction } +import gunbc.fleet.org_actions_inspection { runner_groups_of_rest_read } +import extdeps.github.org_actions { OrgRunnerGroupWire, OrgRunnerGroupListWire } +import gunbc.runner.runner_qualification_ref_pin { + qualification_selected_workflow, qualification_workflow_path, qualification_branch_name, QualificationBranchNamed, QualificationBranchNameRefused, + qualification_ref_pin_of, QualificationRefPinned, QualificationRefPinRefused, +} +import gunbc.runner.runner_qualification_production_subject { qualification_dispatch_subject } +import gunbc.runner.runner_qualification_dispatch { + qualification_attempt_dispatch_input, qualification_revision_dispatch_input, qualification_dispatch_inputs, qualification_dispatch_effect, + qualification_floor_revision_guard_step, SubjectFloorRevisionGuardNotFirst, SubjectFloorStepRunsPastTheGuard, + QualificationSubjectAdmitted, QualificationSubjectRefused, + SubjectSlotForAnotherWorkflow, SubjectAttemptInputUndeclared, SubjectFloorJobAbsent, SubjectFloorRunsOnNotTheAttemptInput, + SubjectFloorNameNotUnique, SubjectDeliveryForAnotherDispatch, + dispatch_authority_refusal, DispatchAuthorityForAnotherInstallation, DispatchAuthorityNotAnInstallation, + qualification_dispatch_subject_over, + qualification_slot_refusal, qualification_floor_admission, QualificationFloorAdmitted, QualificationFloorRefused, + qualification_run_expectation, QualificationRunExpectation, + qualification_dispatch_standing, QualificationDispatchStanding, + DispatchStandingSucceeded, DispatchStandingRefused, DispatchStandingCommitAmbiguous, + hold_covers_slot_host, token_names_registration, + plan_qualification_collection, planned_collection_reads, CollectionRefusedBeforeAnyRead, + ReadQualificationRun, ReadQualificationAttemptJobs, RunCollectedUnderAnotherInstallation, + decide_qualification_run, QualificationRunVerdict, RunVerdictCollected, RunVerdictRefused, + RunReadUnreadable, RunSubjectMismatch, RunAdvancedPastDispatchedAttempt, RunRevisionNotPinned, RunOnAnotherBranch, RunNotCompleted, + RunCompletedWithoutConclusion, RunJobsUnreadable, RunJobsTruncated, RunFloorJobNotUnique, + RunNeverReachedAttemptRunner, RunRunnerNameDisagrees, RunRegisteredRunnerRanAnotherJob, RunFloorJobNotStarted, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data attempt: NonEmptyStr = "q-1" +data pin_branch: NonEmptyStr = "qualification/q-1" +data revision: CommitSha = "1111111111111111111111111111111111111111" +data floor_job_id: NonEmptyStr = "qualification-floor" +data registered_runner: NonEmptyStr = "gunbc-qualification-fixture-q-1.service" +data registered_runner_id: Int = 4242 + +// DESIGN section 3, A WITNESS DISCRIMINATES AT ONE INTERFACE. Every claim but one supplies its +// inputs as values at the interface it judges: the pure scope checks (qualification_slot_refusal, +// qualification_floor_admission), the dispatch standing, the hold comparison, and the run decision +// over a supplied QualificationRunExpectation. The pairing obligation is discharged by ONE claim that +// runs the real path: the route's JIT mint over the real managed-host roster, the sealed subject +// mint over a supplied floor workflow, and the expectation derived from that subject. + +// A group standing for the dedicated name under another id, through the same sealed observer. +fn group_with_id(id: Int, workflow: NonEmptyStr) -> MicrovmRunnerGroupStanding { + observe_runner_group_restriction( + name: "runner-qualification", + selected_workflow: workflow, + listed: runner_groups_of_rest_read(outcome: RestAnswered { answer: OrgRunnerGroupListWire { + total_count: 1, + runner_groups: [OrgRunnerGroupWire { + id: id, + name: "runner-qualification", + visibility: "selected", + allows_public_repositories: false, + restricted_to_workflows: true, + selected_workflows: [workflow as String], + workflow_restrictions_read_only: false, + }], + } }), + ) +} + +fn floor_job(runs_on: RunnerSpec) -> Job { + floor_job_with_steps(runs_on: runs_on, steps: [qualification_floor_revision_guard_step(), floor_work_step(if_condition: none)]) +} + +fn floor_work_step(if_condition: String?) -> Step { + RunStep { + name: Present { value: "run the floor" }, id: none, run: "claim_executor --required-ci", + shell: none, env: none, working_directory: none, if_condition: if_condition, continue_on_error: none, timeout_minutes: none, + } +} + +fn floor_job_with_steps(runs_on: RunnerSpec, steps: List) -> Job { + Job { + id: floor_job_id as String, + name: Present { value: "qualification floor" }, + runner: runs_on, + environment: none, + steps: steps, + needs: [], + env: none, + outputs: none, + if_condition: none, + timeout_minutes: none, + continue_on_error: none, + concurrency: none, + permissions: none, + } +} + +data attempt_runs_on: RunnerSpec = RunsOnExpression { expression: "${{ inputs.runner_attempt_label }}" } + +fn workflow_with(declares_input: Bool, runs_on: RunnerSpec) -> Workflow { + Workflow { + name: "fleet-converge", + run_name: none, + on: [WorkflowDispatch { inputs: if declares_input { [qualification_attempt_dispatch_input, qualification_revision_dispatch_input] } else { [qualification_revision_dispatch_input] } }], + concurrency: none, + jobs: [floor_job(runs_on: runs_on)], + env: none, + permissions: none, + } +} + +// ── THE ONE REAL-PATH CLAIM ───────────────────────────────────────────────────────────────────── +// The route's own JIT mint over the first real managed host, delivered through upstream's 201 fold; +// the sealed subject over a floor workflow carries the slot's attempt and host, the registration's +// minted name (ephemeral_slot_unit), and the floor job's name; the dispatch sends exactly the declared +// input with a label the slot registered; the effect names fleet-converge.yml in gunbc_repository at +// the pinned revision; the expectation the collection judges against is derived from that subject. +test fn the_real_mint_admits_the_attempt_through_the_sealed_subject() -> Bool { + match first(managed_hosts()) { + Present { value: h } => + match dispatch_jit_mint( + binding: HostUnitSlotBinding { standing: host_unit_slot_for(host: managed_host_binding(host: h), attempt: attempt, workflow: qualification_selected_workflow(branch: pin_branch)) }, + authority: app_credential, + control_plane: observed_grant(perms: runner_grant), + organization: gunbai_org_ref, + runner_group: group_restricted_to(workflow: qualification_selected_workflow(branch: pin_branch)), + attempt_binding: jit_admission_axis_standing(axis: AttemptBindingAxis), + ) { + JitMintDispatchAuthorized { dispatch: d } => match qualification_branch_name(attempt: attempt) { + QualificationBranchNameRefused { attempt: _, cause: _ } => false + QualificationBranchNamed { name: nm } => + match qualification_ref_pin_of( + name: nm, revision: revision, readback: RestAnswered { answer: GitRefWire { ref: "refs/heads/qualification/q-1", object: GitRefObjectWire { type: "commit", sha: revision as String } } }, + group: group_restricted_to(workflow: qualification_selected_workflow(branch: pin_branch)), + ) { + QualificationRefPinRefused { attempt: _, refusal: _ } => false + QualificationRefPinned { pin: p } => + { + let delivered = receive_jit_mint(dispatch: JitMintDispatchAuthorized { dispatch: d }, outcome: minted_outcome) + (match qualification_dispatch_subject_over( + dispatch: d, delivery: delivered, + workflow: workflow_with(declares_input: true, runs_on: attempt_runs_on), floor_job_id: floor_job_id, pin: p, + ) { + QualificationSubjectAdmitted { subject: s } => { + let expected = qualification_run_expectation(subject: s) + s.attempt == attempt + && s.runner_id == registered_runner_id && expected.registered_runner_id == registered_runner_id + && token_names_registration(token_app: s.registration.app, token_installation: s.registration.installation, subject: s) + && !token_names_registration(token_app: gunbai_ci_declared, token_installation: s.registration.installation, subject: s) + && !token_names_registration(token_app: s.registration.app, token_installation: other_installation_id, subject: s) + && count(planned_collection_reads(plan: plan_qualification_collection(subject: s, run_id: 77, token_app: gunbai_ci_declared, token_installation: s.registration.installation))) == 0 + && count(planned_collection_reads(plan: plan_qualification_collection(subject: s, run_id: 77, token_app: s.registration.app, token_installation: other_installation_id))) == 0 + && (match plan_qualification_collection(subject: s, run_id: 77, token_app: gunbai_ci_declared, token_installation: s.registration.installation) { + CollectionRefusedBeforeAnyRead { refusal: RunCollectedUnderAnotherInstallation { token_app: a, token_installation: _ } } => a == gunbai_ci_declared + _ => false + }) + && (match planned_collection_reads(plan: plan_qualification_collection(subject: s, run_id: 77, token_app: s.registration.app, token_installation: s.registration.installation)) { + Cons { head: ReadQualificationRun { run_id: 77 }, tail: Cons { head: ReadQualificationAttemptJobs { run_id: 77, attempt: 1 }, tail: Empty {} } } => true + _ => false + }) + && (s.host as String) == (h.host as String) + && (expected.registered_runner as String) == (ephemeral_slot_unit(host: h.host, attempt: attempt) as String) + && (expected.floor_job_name as String) == "qualification floor" + && (expected.revision as String) == (revision as String) + && count(map_keys(qualification_dispatch_inputs(attempt: s.attempt, revision: s.pin.revision))) == 2 + && (match map_get(qualification_dispatch_inputs(attempt: s.attempt, revision: s.pin.revision), qualification_revision_dispatch_input.name) { + Present { value: v } => v == (revision as String) + Absent => false + }) + && (match map_get(qualification_dispatch_inputs(attempt: s.attempt, revision: s.pin.revision), qualification_attempt_dispatch_input.name) { + Present { value: v } => v == (attempt as String) && (ephemeral_slot_labels(host: h.host, attempt: attempt) |> any(l => l == v)) + Absent => false + }) + && (match qualification_dispatch_effect(subject: s) { + DispatchWorkflow { repository: r, workflow: w, subject: sha } => + r.full_name == "gunb-ai/gunbc" && (w.file_name as String) == "fleet-converge.yml" && (sha as String) == (revision as String) + _ => false + }) + } + QualificationSubjectRefused { refusal: _ } => false + }) + } + } + } + JitMintDispatchRefused { refusal: _ } => false + } + Absent => false + } +} + +// THE PRODUCTION MINT OVER TODAY'S GENERATED WORKFLOW REFUSES, AND THE CLAIM ASSERTS THE ROUTE: the +// real JIT mint, then qualification_dispatch_subject, which reads the real fleet-converge inputs +// declaration first and refuses SubjectAttemptInputUndeclared naming runner_attempt_label. When the +// boot leg lands the qualification mode, this turns red and is replaced by the admitted case. +test fn the_production_mint_over_todays_fleet_converge_workflow_refuses_at_the_attempt_input() -> Bool { + match first(managed_hosts()) { + Present { value: h } => + match dispatch_jit_mint( + binding: HostUnitSlotBinding { standing: host_unit_slot_for(host: managed_host_binding(host: h), attempt: attempt, workflow: qualification_selected_workflow(branch: pin_branch)) }, + authority: app_credential, + control_plane: observed_grant(perms: runner_grant), + organization: gunbai_org_ref, + runner_group: group_restricted_to(workflow: qualification_selected_workflow(branch: pin_branch)), + attempt_binding: jit_admission_axis_standing(axis: AttemptBindingAxis), + ) { + JitMintDispatchAuthorized { dispatch: d } => match qualification_branch_name(attempt: attempt) { + QualificationBranchNameRefused { attempt: _, cause: _ } => false + QualificationBranchNamed { name: nm } => + match qualification_ref_pin_of( + name: nm, revision: revision, readback: RestAnswered { answer: GitRefWire { ref: "refs/heads/qualification/q-1", object: GitRefObjectWire { type: "commit", sha: revision as String } } }, + group: group_restricted_to(workflow: qualification_selected_workflow(branch: pin_branch)), + ) { + QualificationRefPinRefused { attempt: _, refusal: _ } => false + QualificationRefPinned { pin: p } => + + match qualification_dispatch_subject( + dispatch: d, + delivery: receive_jit_mint(dispatch: JitMintDispatchAuthorized { dispatch: d }, outcome: minted_outcome), + floor_job_id: floor_job_id, + pin: p, + ) { + QualificationSubjectRefused { refusal: SubjectAttemptInputUndeclared { input: i } } => i == "runner_attempt_label" + _ => false + } + } + } + JitMintDispatchRefused { refusal: _ } => false + } + Absent => false + } +} + +// ── THE RULING'S SCOPE, AT ITS PURE INTERFACES ────────────────────────────────────────────────── +// The subject mint above composes exactly these two checks; these claims supply their inputs. + +fn slot_refused_as_another_workflow(slot_workflow: NonEmptyStr) -> Bool { + match qualification_slot_refusal(slot_workflow: slot_workflow, branch: pin_branch) { + Present { value: SubjectSlotForAnotherWorkflow { slot_workflow: sw, qualification_workflow: _ } } => (sw as String) == (slot_workflow as String) + _ => false + } +} + +// RED: a slot for another workflow file, or for the qualification path on another branch, cannot +// become a subject; the qualification slot at this branch passes (the positive control). +test fn a_slot_for_another_workflow_or_branch_cannot_become_a_subject() -> Bool { + slot_refused_as_another_workflow(slot_workflow: "gunb-ai/gunbc/.github/workflows/witnesses.yml@refs/heads/main") + && slot_refused_as_another_workflow(slot_workflow: qualification_selected_workflow(branch: "feature")) + && (match qualification_slot_refusal(slot_workflow: qualification_selected_workflow(branch: pin_branch), branch: pin_branch) { Absent => true Present { value: _ } => false }) +} + +fn runs_on_refused(runs_on: RunnerSpec) -> Bool { + match qualification_floor_admission(workflow: workflow_with(declares_input: true, runs_on: runs_on), floor_job_id: floor_job_id) { + QualificationFloorRefused { refusal: SubjectFloorRunsOnNotTheAttemptInput { job_id: _, runs_on: _ } } => true + _ => false + } +} + +// RED: a floor runs-on that is a literal label, another input, the attempt input composed with +// anything, or a bare string refuses; so does an undeclared input or a missing floor job. Positive +// control: exactly the attempt input admits the floor job by its name. +test fn a_floor_runs_on_other_than_exactly_the_attempt_input_refuses() -> Bool { + runs_on_refused(runs_on: SelfHosted { labels: [attempt as String] }) + && runs_on_refused(runs_on: RunsOnExpression { expression: "${{ inputs.runner }}" }) + && runs_on_refused(runs_on: RunsOnExpression { expression: "${{ inputs.runner_attempt_label }}-x" }) + && runs_on_refused(runs_on: RunsOnExpression { expression: "gunbc-qualification" }) + && (match qualification_floor_admission(workflow: workflow_with(declares_input: false, runs_on: attempt_runs_on), floor_job_id: floor_job_id) { + QualificationFloorRefused { refusal: SubjectAttemptInputUndeclared { input: _ } } => true + _ => false + }) + && (match qualification_floor_admission(workflow: workflow_with(declares_input: true, runs_on: attempt_runs_on), floor_job_id: "another-job") { + QualificationFloorRefused { refusal: SubjectFloorJobAbsent { job_id: _ } } => true + _ => false + }) + && (match qualification_floor_admission(workflow: workflow_with(declares_input: true, runs_on: attempt_runs_on), floor_job_id: floor_job_id) { + QualificationFloorAdmitted { floor_job_name: n } => (n as String) == "qualification floor" + QualificationFloorRefused { refusal: _ } => false + }) + && (match qualification_floor_admission(workflow: workflow_sharing_the_floor_name(), floor_job_id: floor_job_id) { + QualificationFloorRefused { refusal: SubjectFloorNameNotUnique { name: _, jobs_with_name: k } } => k == 2 + _ => false + }) +} + +// A HELPER JOB WITH THE FLOOR'S DISPLAY NAME. The readback identifies the floor by the name GitHub +// reports, so two authored jobs sharing it would let the helper stand in for the floor; the subject +// mint refuses such a workflow before any dispatch exists. +fn workflow_sharing_the_floor_name() -> Workflow { + let helper = Job { + id: "helper", + name: Present { value: "qualification floor" }, + runner: SelfHosted { labels: ["self-hosted"] }, + environment: none, + steps: [], + needs: [], + env: none, + outputs: none, + if_condition: none, + timeout_minutes: none, + continue_on_error: none, + concurrency: none, + permissions: none, + } + Workflow { + name: "fleet-converge", + run_name: none, + on: [WorkflowDispatch { inputs: [qualification_attempt_dispatch_input, qualification_revision_dispatch_input] }], + concurrency: none, + jobs: [floor_job(runs_on: attempt_runs_on), helper], + env: none, + permissions: none, + } +} + +// ── THE INSTALLATION THAT PERFORMS THE REQUEST IS THE ONE WHOSE PERMISSION IS ASKED ───────────── +// The registration and token are App gunbai-bot installation 999 (app_credential). RED: an authority +// for another App, or for another installation of the same App, refuses before any network; an +// Actions job credential names no installation and refuses. Positive control: the matching authority. +test fn the_dispatch_authority_must_name_the_tokens_installation() -> Bool { + (match dispatch_authority_refusal(authority: app_credential, app: gunbai_bot_declared, installation: bot_installation_id) { Absent => true Present { value: _ } => false }) + && (match dispatch_authority_refusal(authority: other_app_credential, app: gunbai_bot_declared, installation: bot_installation_id) { + Present { value: DispatchAuthorityForAnotherInstallation { authority_app: _, authority_installation: _ } } => true + _ => false + }) + && (match dispatch_authority_refusal(authority: other_installation_credential, app: gunbai_bot_declared, installation: bot_installation_id) { + Present { value: DispatchAuthorityForAnotherInstallation { authority_app: _, authority_installation: _ } } => true + _ => false + }) + && (match dispatch_authority_refusal(authority: a_pull_request_job_credential, app: gunbai_bot_declared, installation: bot_installation_id) { + Present { value: DispatchAuthorityNotAnInstallation } => true + _ => false + }) +} + +// A DELIVERY CARRIES THE AUTHORIZED DISPATCH THAT PRODUCED IT, SEALED, AND THE SUBJECT COMPARES THE +// COMPLETE REQUEST. Two authorized mints for the SAME host-unit slot -- under another organization, and +// under the same slot, App, installation, organization and runner name but another runner group -- +// produce deliveries that agree on slot, credential and runner id; the subject over dispatch A refuses +// each rather than claiming A's registration for a credential another mint produced. (Rewrapping one +// delivery's credential with A's dispatch is unconstructable: +// test.claim.runner_qualification_delivery_rewrap_witness.) +test fn a_delivery_from_another_dispatch_on_the_same_slot_refuses() -> Bool { + match first(managed_hosts()) { + Present { value: h } => { + let binding = HostUnitSlotBinding { standing: host_unit_slot_for(host: managed_host_binding(host: h), attempt: attempt, workflow: qualification_selected_workflow(branch: pin_branch)) } + let group = group_restricted_to(workflow: qualification_selected_workflow(branch: pin_branch)) + match dispatch_jit_mint(binding: binding, authority: app_credential, control_plane: observed_grant(perms: runner_grant), organization: gunbai_org_ref, runner_group: group, attempt_binding: jit_admission_axis_standing(axis: AttemptBindingAxis)) { + JitMintDispatchAuthorized { dispatch: a } => match qualification_branch_name(attempt: attempt) { + QualificationBranchNameRefused { attempt: _, cause: _ } => false + QualificationBranchNamed { name: nm } => + match qualification_ref_pin_of( + name: nm, revision: revision, readback: RestAnswered { answer: GitRefWire { ref: "refs/heads/qualification/q-1", object: GitRefObjectWire { type: "commit", sha: revision as String } } }, + group: group_restricted_to(workflow: qualification_selected_workflow(branch: pin_branch)), + ) { + QualificationRefPinRefused { attempt: _, refusal: _ } => false + QualificationRefPinned { pin: p } => + + match dispatch_jit_mint(binding: binding, authority: app_credential, control_plane: observed_grant(perms: runner_grant), organization: GitHubOrganizationRef { login: "another-org" }, runner_group: group, attempt_binding: jit_admission_axis_standing(axis: AttemptBindingAxis)) { + JitMintDispatchAuthorized { dispatch: b } => + a.slot == b.slot + && (match qualification_dispatch_subject_over( + dispatch: a, delivery: receive_jit_mint(dispatch: JitMintDispatchAuthorized { dispatch: b }, outcome: minted_outcome), + workflow: workflow_with(declares_input: true, runs_on: attempt_runs_on), floor_job_id: floor_job_id, pin: p, + ) { + QualificationSubjectRefused { refusal: SubjectDeliveryForAnotherDispatch } => true + _ => false + }) + && (match dispatch_jit_mint(binding: binding, authority: app_credential, control_plane: observed_grant(perms: runner_grant), organization: gunbai_org_ref, runner_group: group_with_id(id: 4, workflow: qualification_selected_workflow(branch: pin_branch)), attempt_binding: jit_admission_axis_standing(axis: AttemptBindingAxis)) { + JitMintDispatchAuthorized { dispatch: c } => + a.slot == c.slot && a.app == c.app && a.installation == c.installation && a.organization == c.organization && a.request.name == c.request.name + && a.request.runner_group_id != c.request.runner_group_id + && (match qualification_dispatch_subject_over( + dispatch: a, delivery: receive_jit_mint(dispatch: JitMintDispatchAuthorized { dispatch: c }, outcome: minted_outcome), + workflow: workflow_with(declares_input: true, runs_on: attempt_runs_on), floor_job_id: floor_job_id, pin: p, + ) { + QualificationSubjectRefused { refusal: SubjectDeliveryForAnotherDispatch } => true + _ => false + }) + JitMintDispatchRefused { refusal: _ } => false + }) + JitMintDispatchRefused { refusal: _ } => false + } + } + } + JitMintDispatchRefused { refusal: _ } => false + } + } + Absent => false + } +} + +// ── THE DISPATCH STANDING AND THE INTERLOCK ───────────────────────────────────────────────────── + +fn mutation_standing(refusal: RestRefusal) -> QualificationDispatchStanding { + qualification_dispatch_standing(dispatch: RestRefused { refusal: refusal }) +} + +data dispatch_receipt: WorkflowDispatchReceipt = WorkflowDispatchReceipt { + workflow_run_id: 77, + run_url: "https://api.github.com/repos/gunb-ai/gunbc/actions/runs/77" as NonEmptyStr, + html_url: "https://github.com/gunb-ai/gunbc/actions/runs/77" as NonEmptyStr, +} + +fn ambiguous(s: QualificationDispatchStanding) -> Bool { + match s { DispatchStandingCommitAmbiguous { detail: _ } => true _ => false } +} + +// THREE STANDINGS, FROM THE MUTATION CLASSIFIER: a decided 422 is refused; no response, a 503, and an +// undecodable 200 are commit-ambiguous; only a succeeded exchange dispatches. The interlock: a hold +// covers the slot's own host and no other. +test fn the_dispatch_has_three_standings_and_an_interlock() -> Bool { + (match mutation_standing(refusal: RestStatusRefused { status: 422, body: "Unexpected inputs provided" }) { DispatchStandingRefused { status: st, body: _ } => st == 422 _ => false }) + && ambiguous(s: mutation_standing(refusal: RestTransportRefused { cause: "fixture: connection reset after send" })) + && ambiguous(s: mutation_standing(refusal: RestStatusRefused { status: 503, body: "fixture" })) + && ambiguous(s: mutation_standing(refusal: RestBodyUndecodable { status: 200, cause: "fixture: truncated body" })) + && (match qualification_dispatch_standing(dispatch: RestAnswered { answer: dispatch_receipt }) { DispatchStandingSucceeded { receipt: r } => r.workflow_run_id == 77 _ => false }) + && hold_covers_slot_host(held: "mtcollins1" as HostIdentity, slot_host: "mtcollins1" as HostIdentity) + && !hold_covers_slot_host(held: "srv1" as HostIdentity, slot_host: "mtcollins1" as HostIdentity) +} + +// ── THE COLLECTION, OVER A SUPPLIED EXPECTATION ───────────────────────────────────────────────── + +data expect: QualificationRunExpectation = QualificationRunExpectation { + registered_runner_id: registered_runner_id, + registered_runner: registered_runner, + floor_job_name: "qualification floor", + revision: revision, + branch: pin_branch, +} + +fn run(id: Int, attempt_n: Int, event: String, path: String, sha: CommitSha, completed: Bool, concluded: Bool) -> WorkflowRun { + run_on(id: id, attempt_n: attempt_n, event: event, path: path, sha: sha, completed: completed, concluded: concluded, on_branch: pin_branch as String) +} + +fn run_on(id: Int, attempt_n: Int, event: String, path: String, sha: CommitSha, completed: Bool, concluded: Bool, on_branch: String) -> WorkflowRun { + WorkflowRun { + id: id, + name: none, + path: Present { value: path }, + head_sha: sha, + head_branch: Present { value: on_branch }, + event: event, + status: if completed { Completed } else { InProgress }, + conclusion: if concluded { Present { value: Failure } } else { none }, + workflow_id: 9, + run_number: 1, + run_attempt: attempt_n, + actor: none, + triggering_actor: none, + html_url: "https://github.com/gunb-ai/gunbc/actions/runs/77", + created_at: "2026-10-04T00:00:00Z", + updated_at: "2026-10-04T01:00:00Z", + pull_requests: [], + } +} + +fn dispatched_run(attempt_n: Int) -> WorkflowRun { + run(id: 77, attempt_n: attempt_n, event: "workflow_dispatch", path: qualification_workflow_path() as String, sha: revision, completed: true, concluded: true) +} + +fn job(id: Int, name: String, runner_id: Int, runner: String, started: Bool, attempt_n: Int) -> WorkflowJobRun { + WorkflowJobRun { + id: id, + run_id: 77, + run_attempt: attempt_n, + name: name, + status: Completed, + conclusion: Present { value: Success }, + labels: [attempt as String], + runner_id: Present { value: runner_id }, + runner_name: Present { value: runner }, + created_at: Present { value: "2026-10-04T00:00:10Z" }, + started_at: if started { Present { value: "2026-10-04T00:01:00Z" } } else { none }, + completed_at: Present { value: "2026-10-04T00:50:00Z" }, + } +} + +fn floor_on(runner_id: Int) -> WorkflowJobRun { + job(id: 1, name: "qualification floor", runner_id: runner_id, runner: registered_runner as String, started: true, attempt_n: 1) +} + +fn jobs(js: List) -> WorkflowJobRunList { + WorkflowJobRunList { total_count: count(js), jobs: js } +} + +fn decide_run(r: WorkflowRun, js: WorkflowJobRunList) -> QualificationRunVerdict { + decide_qualification_run(subject: expect, run_id: 77, run_read: RestAnswered { answer: r }, jobs_read: RestAnswered { answer: js }) +} + +fn decide_jobs(js: WorkflowJobRunList) -> QualificationRunVerdict { + decide_run(r: dispatched_run(attempt_n: 1), js: js) +} + +fn mismatch(v: QualificationRunVerdict) -> Bool { + match v { + RunVerdictRefused { refusal: RunSubjectMismatch { observed_run_id: _, observed_event: _, observed_path: _, foreign_jobs: _ } } => true + _ => false + } +} + +// THE RUNNER IS JOINED BY ITS MINTED ID, WITH THE NAME AS CORROBORATION. Positive control: the named +// floor job on the registered runner id is collected with the run's own conclusion (a Failure is +// still this host's run). REDs: the same runner name and labels under another runner id; the minted +// id reported under another name; a helper job on the registered runner while the floor ran +// elsewhere; a floor on the registered runner that never started; two jobs on the registered runner. +test fn the_collection_joins_the_floor_job_to_the_registered_runner() -> Bool { + let mine = registered_runner as String + (match decide_jobs(js: jobs(js: [floor_on(runner_id: registered_runner_id)])) { + RunVerdictCollected { run: r, floor_job: f, conclusion: c } => r.id == 77 && f.id == 1 && (match c { Failure => true _ => false }) + _ => false + }) + && (match decide_jobs(js: jobs(js: [job(id: 1, name: "qualification floor", runner_id: 99, runner: mine, started: true, attempt_n: 1)])) { + RunVerdictRefused { refusal: RunNeverReachedAttemptRunner { registered_runner_id: rid, runner_ids_seen: seen } } => rid == registered_runner_id && count(seen) == 1 + _ => false + }) + && (match decide_jobs(js: jobs(js: [job(id: 1, name: "qualification floor", runner_id: registered_runner_id, runner: "another-name", started: true, attempt_n: 1)])) { + RunVerdictRefused { refusal: RunRunnerNameDisagrees { registered_runner_id: _, registered_runner: _, observed_runner_name: _ } } => true + _ => false + }) + && (match decide_jobs(js: jobs(js: [job(id: 2, name: "helper", runner_id: registered_runner_id, runner: mine, started: true, attempt_n: 1), floor_on(runner_id: 99)])) { + RunVerdictRefused { refusal: RunRegisteredRunnerRanAnotherJob { registered_runner: _, job_name: n } } => n == "helper" + _ => false + }) + && (match decide_jobs(js: jobs(js: [job(id: 1, name: "qualification floor", runner_id: registered_runner_id, runner: mine, started: false, attempt_n: 1)])) { + RunVerdictRefused { refusal: RunFloorJobNotStarted { job_id: id } } => id == 1 + _ => false + }) + && (match decide_jobs(js: jobs(js: [floor_on(runner_id: registered_runner_id), job(id: 2, name: "qualification floor", runner_id: registered_runner_id, runner: mine, started: true, attempt_n: 1)])) { + RunVerdictRefused { refusal: RunFloorJobNotUnique { floor_job_name: _, matching: m } } => m == 2 + _ => false + }) +} + +// THE SUBJECT IS THE DISPATCHED RUN'S FIRST ATTEMPT ON THE PIN BRANCH. REDs: the run re-run to +// attempt 2 (whose floor job carries the same labels and runner); a job of attempt 2 in the listing; +// another run id; another event; another workflow path; a run on another branch (the default branch +// after a move, which the pinned group would also refuse to hand our runner). +test fn a_rerun_or_another_run_cannot_be_collected_as_the_dispatch() -> Bool { + let floor = jobs(js: [floor_on(runner_id: registered_runner_id)]) + let path = qualification_workflow_path() as String + (match decide_run(r: dispatched_run(attempt_n: 2), js: floor) { + RunVerdictRefused { refusal: RunAdvancedPastDispatchedAttempt { observed_attempt: a } } => a == 2 + _ => false + }) + && mismatch(v: decide_jobs(js: jobs(js: [job(id: 1, name: "qualification floor", runner_id: registered_runner_id, runner: registered_runner as String, started: true, attempt_n: 2)]))) + && mismatch(v: decide_run(r: run(id: 78, attempt_n: 1, event: "workflow_dispatch", path: path, sha: revision, completed: true, concluded: true), js: floor)) + && mismatch(v: decide_run(r: run(id: 77, attempt_n: 1, event: "push", path: path, sha: revision, completed: true, concluded: true), js: floor)) + && mismatch(v: decide_run(r: run(id: 77, attempt_n: 1, event: "workflow_dispatch", path: ".github/workflows/witnesses.yml", sha: revision, completed: true, concluded: true), js: floor)) + && (match decide_run(r: run_on(id: 77, attempt_n: 1, event: "workflow_dispatch", path: path, sha: revision, completed: true, concluded: true, on_branch: "main"), js: floor) { + RunVerdictRefused { refusal: RunOnAnotherBranch { pinned: _, observed: _ } } => true + _ => false + }) +} + +test fn an_unfinished_unpinned_or_unreadable_run_refuses() -> Bool { + let floor = jobs(js: [floor_on(runner_id: registered_runner_id)]) + let path = qualification_workflow_path() as String + (match decide_run(r: run(id: 77, attempt_n: 1, event: "workflow_dispatch", path: path, sha: revision, completed: false, concluded: false), js: floor) { + RunVerdictRefused { refusal: RunNotCompleted { status: InProgress } } => true + _ => false + }) + && (match decide_run(r: run(id: 77, attempt_n: 1, event: "workflow_dispatch", path: path, sha: revision, completed: true, concluded: false), js: floor) { + RunVerdictRefused { refusal: RunCompletedWithoutConclusion } => true + _ => false + }) + && (match decide_run(r: run(id: 77, attempt_n: 1, event: "workflow_dispatch", path: path, sha: "2222222222222222222222222222222222222222", completed: true, concluded: true), js: floor) { + RunVerdictRefused { refusal: RunRevisionNotPinned { pinned: _, observed: _ } } => true + _ => false + }) + && (match decide_run(r: dispatched_run(attempt_n: 1), js: WorkflowJobRunList { total_count: 2, jobs: floor.jobs }) { + RunVerdictRefused { refusal: RunJobsTruncated { returned: rt, total: t } } => rt == 1 && t == 2 + _ => false + }) + && (match decide_qualification_run(subject: expect, run_id: 77, run_read: RestRefused { refusal: RestTransportRefused { cause: "fixture" } }, jobs_read: RestAnswered { answer: floor }) { + RunVerdictRefused { refusal: RunReadUnreadable { refusal: _ } } => true + _ => false + }) + && (match decide_qualification_run(subject: expect, run_id: 77, run_read: RestAnswered { answer: dispatched_run(attempt_n: 1) }, jobs_read: RestRefused { refusal: RestStatusRefused { status: 404, body: "fixture" } }) { + RunVerdictRefused { refusal: RunJobsUnreadable { refusal: _ } } => true + _ => false + }) +} + +// THE FLOOR CONTRACT CHECKS OUT THE PINNED REVISION FIRST AND NOTHING RUNS PAST A REFUSAL +// (decision: eager-gull-22, 2026-10-04). The guard is the floor job's FIRST step; on a mismatch it exits +// nonzero, and GitHub skips every later step of a failed job unless the step opts back in -- so the +// contract also refuses any step with an if: condition or continue-on-error, and a job with +// continue-on-error. REDs: the revision input undeclared; no guard; the guard after another step; a +// later step with if: always(); a later step with continue-on-error. The guard itself compares HEAD with +// the revision input and exits 1 on a mismatch. The post-run head_sha refusal is +// RunRevisionNotPinned (an_unfinished_unpinned_or_unreadable_run_refuses). +fn floor_refused(workflow: Workflow) -> Bool { + match qualification_floor_admission(workflow: workflow, floor_job_id: floor_job_id) { + QualificationFloorRefused { refusal: SubjectFloorRevisionGuardNotFirst { job_id: _ } } => true + QualificationFloorRefused { refusal: SubjectFloorStepRunsPastTheGuard { job_id: _ } } => true + QualificationFloorRefused { refusal: SubjectAttemptInputUndeclared { input: i } } => i == "qualification_revision" + _ => false + } +} + +fn workflow_with_floor(job: Job, inputs_declare_revision: Bool) -> Workflow { + Workflow { + name: "fleet-converge", + run_name: none, + on: [WorkflowDispatch { inputs: if inputs_declare_revision { [qualification_attempt_dispatch_input, qualification_revision_dispatch_input] } else { [qualification_attempt_dispatch_input] } }], + concurrency: none, + jobs: [job], + env: none, + permissions: none, + } +} + +test fn the_floor_checks_out_the_pinned_revision_first_and_nothing_runs_past_a_refusal() -> Bool { + let guard = qualification_floor_revision_guard_step() + let work = floor_work_step(if_condition: none) + let tolerant = RunStep { + name: Present { value: "run the floor anyway" }, id: none, run: "claim_executor --required-ci", + shell: none, env: none, working_directory: none, if_condition: none, continue_on_error: Present { value: true }, timeout_minutes: none, + } + (match qualification_floor_admission(workflow: workflow_with_floor(job: floor_job_with_steps(runs_on: attempt_runs_on, steps: [guard, work]), inputs_declare_revision: true), floor_job_id: floor_job_id) { + QualificationFloorAdmitted { floor_job_name: _ } => true + QualificationFloorRefused { refusal: _ } => false + }) + && floor_refused(workflow: workflow_with_floor(job: floor_job_with_steps(runs_on: attempt_runs_on, steps: [guard, work]), inputs_declare_revision: false)) + && floor_refused(workflow: workflow_with_floor(job: floor_job_with_steps(runs_on: attempt_runs_on, steps: [work]), inputs_declare_revision: true)) + && floor_refused(workflow: workflow_with_floor(job: floor_job_with_steps(runs_on: attempt_runs_on, steps: [work, guard]), inputs_declare_revision: true)) + && floor_refused(workflow: workflow_with_floor(job: floor_job_with_steps(runs_on: attempt_runs_on, steps: [guard, floor_work_step(if_condition: Present { value: "always()" })]), inputs_declare_revision: true)) + && floor_refused(workflow: workflow_with_floor(job: floor_job_with_steps(runs_on: attempt_runs_on, steps: [guard, tolerant]), inputs_declare_revision: true)) + && (match guard { + RunStep { name: _, id: _, run: r, shell: _, env: e, working_directory: _, if_condition: c, continue_on_error: ce, timeout_minutes: _ } => + string_contains(s: r, pattern: "git rev-parse HEAD") + && string_contains(s: r, pattern: "!= \"$QUALIFICATION_REVISION\"") + && string_contains(s: r, pattern: "exit 1") + && (match c { Absent => true Present { value: _ } => false }) + && (match ce { Absent => true Present { value: _ } => false }) + && (match e { Present { value: kvs } => kvs |> any(x => x.key == "QUALIFICATION_REVISION") Absent => false }) + UsesStep { name: _, id: _, uses: _, with: _, env: _, if_condition: _, continue_on_error: _, timeout_minutes: _ } => false + }) +} diff --git a/dag/test/claim/runner/runner_qualification_ref_pin_witness_test.dag b/dag/test/claim/runner/runner_qualification_ref_pin_witness_test.dag new file mode 100644 index 00000000000..3f0fe4237ef --- /dev/null +++ b/dag/test/claim/runner/runner_qualification_ref_pin_witness_test.dag @@ -0,0 +1,172 @@ +module test.claim.runner_qualification_ref_pin_witness + +import std.types { Bool, CommitSha, Int, List, NonEmptyStr, String } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import extdeps.transports.rest { RestAnswered, RestRefused, RestStatusRefused, RestTransportRefused } +import extdeps.github.git_database { GitRefWire, GitRefObjectWire } +import extdeps.github.actions { + WorkflowTrigger, Push, PullRequest, Schedule, WorkflowDispatch, WorkflowCall, WorkflowRunCompleted, MergeGroup, +} +import gunbc.fleet.org_actions_inspection { RunnerGroupListDecoded, RunnerGroupIdentity } +import gunbc.runner_group_restriction_observation { RunnerGroupRestrictionRefused, RunnerGroupAbsent } +import gunbc.fleet_desired_admission_workflow { fleet_desired_admission_workflow } +import test.claim.github_app_registry { group_restricted_to } +import gunbc.runner.runner_qualification_ref_pin { + qualification_branch_name, QualificationBranchNamed, QualificationBranchNameRefused, branch_full_ref, + qualification_selected_workflow, qualification_runner_group_name, + qualification_group_target, QualificationGroupTargeted, QualificationGroupNotTargetable, + branch_create_refusal, PinBranchPreexisting, PinBranchCreateRefused, PinBranchCreateAmbiguous, + qualification_ref_pin_of, QualificationRefPinned, QualificationRefPinRefused, PinBranchReadbackMismatch, PinGroupReadbackRefused, + classify_branch_removal, QualificationBranchRemoved, QualificationBranchRemovalRefused, BranchStillPresent, BranchReadUnreadable, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// A REF AS GitHub's GET /git/ref RETURNS IT, at a supplied commit: the readback this module judges. +fn ref_at(sha: String) -> GitRefWire { + GitRefWire { ref: "refs/heads/qualification/q-1", object: GitRefObjectWire { type: "commit", sha: sha } } +} + +data revision: CommitSha = "1111111111111111111111111111111111111111" + +fn named_ok(attempt: NonEmptyStr) -> Bool { + match qualification_branch_name(attempt: attempt) { + QualificationBranchNamed { name: n } => (n.branch as String) == concat("qualification/", attempt as String) && (branch_full_ref(name: n) as String) == concat("refs/heads/qualification/", attempt as String) + QualificationBranchNameRefused { attempt: _, cause: _ } => false + } +} + +fn named_refused(attempt: NonEmptyStr) -> Bool { + match qualification_branch_name(attempt: attempt) { + QualificationBranchNamed { name: _ } => false + QualificationBranchNameRefused { attempt: _, cause: _ } => true + } +} + +// RED: OUT OF PREFIX. A label carrying a slash, a parent step, a ref metacharacter, a leading dot or +// a .lock suffix cannot name refs/heads/qualification/ and refuses rather than escaping. +// Positive control: an ordinary attempt label names exactly refs/heads/qualification/. +test fn a_ref_outside_refs_heads_qualification_cannot_be_named() -> Bool { + named_ok(attempt: "q-1") + && named_refused(attempt: "../main") + && named_refused(attempt: "q/1") + && named_refused(attempt: "main~1") + && named_refused(attempt: ".hidden") + && named_refused(attempt: "q-1.lock") + && named_refused(attempt: "q 1") +} + +// RED: CREATE-ONCE. GitHub's 422 on CreateRef (the ref exists) is the pre-existing refusal, never an +// adoption; a lost or undecodable answer is ambiguous (removal still owed); only a created ref +// proceeds to readback. +test fn a_preexisting_branch_refuses_and_a_lost_create_is_ambiguous() -> Bool { + (match branch_create_refusal(created: RestRefused { refusal: RestStatusRefused { status: 422, body: "Reference already exists" } }) { + Present { value: PinBranchPreexisting { observed_sha: _ } } => true + _ => false + }) + && (match branch_create_refusal(created: RestRefused { refusal: RestStatusRefused { status: 403, body: "fixture" } }) { + Present { value: PinBranchCreateRefused { status: s, body: _ } } => s == 403 + _ => false + }) + && (match branch_create_refusal(created: RestRefused { refusal: RestStatusRefused { status: 502, body: "fixture: 502 after the write" } }) { + Present { value: PinBranchCreateAmbiguous { detail: _ } } => true + _ => false + }) + && (match branch_create_refusal(created: RestRefused { refusal: RestTransportRefused { cause: "fixture: connection reset after send" } }) { + Present { value: PinBranchCreateAmbiguous { detail: _ } } => true + _ => false + }) + && (match branch_create_refusal(created: RestAnswered { answer: ref_at(sha: revision as String) }) { Absent => true Present { value: _ } => false }) +} + +fn group_row(id: Int, name: NonEmptyStr) -> RunnerGroupIdentity { + RunnerGroupIdentity { id: id, name: name, allows_public_repositories: false, restricted_to_workflows: true, selected_workflows: [] } +} + +// RED: A WRITE TO ANY OTHER GROUP. Only the dedicated qualification group can become a write target: +// the shakedown group refuses even when it is present, as do an absent or duplicated dedicated group. +// Positive control: the dedicated group found once. +test fn a_restriction_write_to_any_other_group_refuses() -> Bool { + let listed = RunnerGroupListDecoded { groups: [group_row(id: 1, name: "microvm-shakedown"), group_row(id: 3, name: qualification_runner_group_name)] } + (match qualification_group_target(requested: "microvm-shakedown", listed: listed) { QualificationGroupNotTargetable { cause: _ } => true _ => false }) + && (match qualification_group_target(requested: "Default", listed: listed) { QualificationGroupNotTargetable { cause: _ } => true _ => false }) + && (match qualification_group_target(requested: qualification_runner_group_name, listed: RunnerGroupListDecoded { groups: [group_row(id: 1, name: "microvm-shakedown")] }) { + QualificationGroupNotTargetable { cause: _ } => true + _ => false + }) + && (match qualification_group_target(requested: qualification_runner_group_name, listed: RunnerGroupListDecoded { groups: [group_row(id: 3, name: qualification_runner_group_name), group_row(id: 4, name: qualification_runner_group_name)] }) { + QualificationGroupNotTargetable { cause: _ } => true + _ => false + }) + && (match qualification_group_target(requested: qualification_runner_group_name, listed: listed) { + QualificationGroupTargeted { target: t } => t.group_id == 3 + QualificationGroupNotTargetable { cause: _ } => false + }) +} + +// THE PIN IS MINTED ONLY FROM A READBACK AT THE EXACT REVISION AND A GROUP OBSERVED PINNED TO THE +// BRANCH. REDs: the branch read back at another commit; the group not observed restricted to the +// qualification workflow at the branch. Positive control: both hold. +test fn the_pin_is_minted_only_from_the_exact_revision_and_the_pinned_group() -> Bool { + match qualification_branch_name(attempt: "q-1") { + QualificationBranchNameRefused { attempt: _, cause: _ } => false + QualificationBranchNamed { name: n } => { + let pinned_group = group_restricted_to(workflow: qualification_selected_workflow(branch: n.branch)) + (match qualification_ref_pin_of(name: n, revision: revision, readback: RestAnswered { answer: ref_at(sha: revision as String) }, group: pinned_group) { + QualificationRefPinned { pin: p } => (p.name.branch as String) == "qualification/q-1" && (p.revision as String) == (revision as String) && p.group.group.value == 3 + QualificationRefPinRefused { attempt: _, refusal: _ } => false + }) + && (match qualification_ref_pin_of(name: n, revision: revision, readback: RestAnswered { answer: ref_at(sha: "2222222222222222222222222222222222222222") }, group: pinned_group) { + QualificationRefPinRefused { attempt: _, refusal: PinBranchReadbackMismatch { pinned: _, observed: _ } } => true + _ => false + }) + && (match qualification_ref_pin_of(name: n, revision: revision, readback: RestAnswered { answer: ref_at(sha: revision as String) }, group: RunnerGroupRestrictionRefused { name: qualification_runner_group_name, cause: RunnerGroupAbsent }) { + QualificationRefPinRefused { attempt: _, refusal: PinGroupReadbackRefused { standing: _ } } => true + _ => false + }) + } + } +} + +// REMOVAL IS A READBACK. A read finding the branch absent (404) is removed; a branch still present +// after the delete refuses BranchStillPresent; an unreadable read refuses rather than reporting it gone. +test fn the_branch_is_removed_only_when_a_read_finds_it_absent() -> Bool { + match qualification_branch_name(attempt: "q-1") { + QualificationBranchNameRefused { attempt: _, cause: _ } => false + QualificationBranchNamed { name: n } => + (match classify_branch_removal(name: n, readback: RestRefused { refusal: RestStatusRefused { status: 404, body: "Not Found" } }, deleted: true, delete_refusal: none) { + QualificationBranchRemoved { name: _, deleted: d } => d + _ => false + }) + && (match classify_branch_removal(name: n, readback: RestAnswered { answer: ref_at(sha: revision as String) }, deleted: true, delete_refusal: none) { + QualificationBranchRemovalRefused { name: _, cause: BranchStillPresent { observed_sha: o, delete_refusal: _ } } => o == (revision as String) + _ => false + }) + && (match classify_branch_removal(name: n, readback: RestRefused { refusal: RestStatusRefused { status: 500, body: "fixture" } }, deleted: true, delete_refusal: none) { + QualificationBranchRemovalRefused { name: _, cause: BranchReadUnreadable { refusal: _ } } => true + _ => false + }) + } +} + +// CREATING A QUALIFICATION BRANCH FIRES NO WORKFLOW. WorkflowTrigger has no `create` variant, so no +// generated workflow can trigger on branch creation by construction; the one generated workflow with a +// push trigger is gunbc.fleet_desired_admission_workflow, whose branch filter must not admit +// qualification/. A filter containing any glob is read as possibly matching (refused here +// rather than evaluated), so a widened filter turns this red. +fn push_trigger_could_fire_on(trigger: WorkflowTrigger, branch: String) -> Bool { + match trigger { + Push { branches: bs, paths: _ } => count(bs) == 0 || (bs |> any(b => b == branch || string_contains(s: b, pattern: "*"))) + PullRequest { branches: _, types: _ } => false + Schedule { cron: _ } => false + WorkflowDispatch { inputs: _ } => false + WorkflowCall { inputs: _ } => false + WorkflowRunCompleted { workflows: _, branches: _ } => false + MergeGroup => false + } +} + +test fn creating_a_qualification_branch_fires_no_generated_push_workflow() -> Bool { + !(fleet_desired_admission_workflow.on |> any(t => push_trigger_could_fire_on(trigger: t, branch: "qualification/q-1"))) + && push_trigger_could_fire_on(trigger: Push { branches: ["qualification/**"], paths: [] }, branch: "qualification/q-1") +} diff --git a/dag/test/claim/runner/runner_throughput_qualification_witness_test.dag b/dag/test/claim/runner/runner_throughput_qualification_witness_test.dag index 21a65bf2872..5ecd1e0e98b 100644 --- a/dag/test/claim/runner/runner_throughput_qualification_witness_test.dag +++ b/dag/test/claim/runner/runner_throughput_qualification_witness_test.dag @@ -749,8 +749,8 @@ test fn the_route_classifies_every_mutation_at_its_grain() -> Bool { )) } -// THE ROUTE IS NOT EXECUTABLE TODAY, AND THE CLAIM SAYS SO: the boot and dispatch legs are still -// declared frontiers. This flips to the regression control that the bindings stay when they land. +// THE ROUTE IS NOT EXECUTABLE TODAY, AND THE CLAIM SAYS SO: the boot leg has no authority and the +// registration, dispatch and deregistration authorities are implemented but not wired. This flips to the regression control that the bindings stay when they land. test fn the_route_is_not_executable_while_any_effectful_leg_is_unbound() -> Bool { !route_is_executable(route: route()) && !leg_is_wired(leg: qualification_run_producer_frontier) } @@ -765,9 +765,9 @@ test fn the_image_leg_is_implemented_not_wired_and_the_boot_leg_awaits_a_runner_ && match mtcollins1_route_legs.boot { LegAwaitingAuthority { lands_with: _, sufficient_for: _ } => true _ => false } } -// REGISTRATION AND DEREGISTRATION HAVE IMPLEMENTED AUTHORITIES AND ARE NOT WIRED -- by declaration -// identity, so pointing either leg at some other declaration, or promoting either to LegWired while -// nothing on the route calls it, turns this red -- and the route stays unexecutable. +// REGISTRATION, DISPATCH AND DEREGISTRATION HAVE IMPLEMENTED AUTHORITIES AND ARE NOT WIRED -- by +// declaration identity, so pointing any leg at some other declaration, or promoting one to LegWired +// while nothing on the route calls it, turns this red -- and the route stays unexecutable. fn leg_names(leg: RouteLegStanding, module_path: String, decl_name: String) -> Bool { match leg { LegAuthorityImplemented { authority: a, wiring_owed: _ } => (a.module_path as String) == module_path && (a.decl_name as String) == decl_name @@ -775,8 +775,9 @@ fn leg_names(leg: RouteLegStanding, module_path: String, decl_name: String) -> B } } -test fn the_registration_and_deregistration_legs_are_implemented_not_wired_and_the_route_is_not_executable() -> Bool { +test fn the_registration_dispatch_and_deregistration_legs_are_implemented_not_wired_and_the_route_is_not_executable() -> Bool { leg_names(leg: mtcollins1_route_legs.registration, module_path: "gunbc.runner.runner_jit_perform", decl_name: "dispatch_jit_mint") + && leg_names(leg: mtcollins1_route_legs.dispatch, module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "dispatch_qualification_floor") && leg_names(leg: mtcollins1_route_legs.deregistration, module_path: "gunbc.runner.runner_jit_deregistration", decl_name: "ensure_jit_runner_deregistered") && !leg_is_wired(leg: mtcollins1_route_legs.registration) && !leg_is_wired(leg: mtcollins1_route_legs.deregistration) diff --git a/dag/test/claim/superseded_run_starvation_census_witness_test.dag b/dag/test/claim/superseded_run_starvation_census_witness_test.dag index e5da6157f55..96091a15fd6 100644 --- a/dag/test/claim/superseded_run_starvation_census_witness_test.dag +++ b/dag/test/claim/superseded_run_starvation_census_witness_test.dag @@ -213,6 +213,8 @@ data job_cancelled: WorkflowJobRun = WorkflowJobRun { status: Completed, conclusion: Present { value: Cancelled }, labels: [], + runner_id: none, + runner_name: none, created_at: Present { value: "2026-09-01T00:01:00Z" }, started_at: Present { value: "2026-09-01T00:10:00Z" }, completed_at: Present { value: "2026-09-01T00:20:00Z" }, @@ -226,6 +228,8 @@ data job_failed: WorkflowJobRun = WorkflowJobRun { status: Completed, conclusion: Present { value: Failure }, labels: [], + runner_id: none, + runner_name: none, created_at: Present { value: "2026-09-01T00:00:00Z" }, started_at: Present { value: "2026-09-01T00:00:00Z" }, completed_at: Present { value: "2026-09-01T00:15:00Z" }, @@ -239,6 +243,8 @@ data job_success: WorkflowJobRun = WorkflowJobRun { status: Completed, conclusion: Present { value: Success }, labels: [], + runner_id: none, + runner_name: none, created_at: Present { value: "2026-09-01T00:02:00Z" }, started_at: Present { value: "2026-09-01T00:05:00Z" }, completed_at: Present { value: "2026-09-01T00:10:00Z" }, @@ -252,6 +258,8 @@ data job_queued: WorkflowJobRun = WorkflowJobRun { status: Queued, conclusion: none, labels: [], + runner_id: none, + runner_name: none, created_at: Present { value: "2026-09-01T00:03:00Z" }, started_at: none, completed_at: none, @@ -265,6 +273,8 @@ data job_in_progress: WorkflowJobRun = WorkflowJobRun { status: InProgress, conclusion: none, labels: [], + runner_id: none, + runner_name: none, created_at: Present { value: "2026-09-01T00:04:00Z" }, started_at: Present { value: "2026-09-01T00:30:00Z" }, completed_at: none, @@ -339,6 +349,8 @@ test fn earliest_created_at_returns_none_when_no_created_at() -> Bool { status: InProgress, conclusion: none, labels: [], + runner_id: none, + runner_name: none, created_at: none, started_at: none, completed_at: none, diff --git a/dag/test/probe/qualification_collection_relabel_probe.dag b/dag/test/probe/qualification_collection_relabel_probe.dag new file mode 100644 index 00000000000..1df99eb5bdc --- /dev/null +++ b/dag/test/probe/qualification_collection_relabel_probe.dag @@ -0,0 +1,19 @@ +module test.probe.qualification_collection_relabel_probe + +// THIS MODULE MUST NOT RESOLVE. Collecting outside the token join is minting a collection the join +// never admitted: relabel another collection's run and floor job as dispatch d's. The carrier is +// sealed, so the one function that mints it -- gunbc.runner.runner_qualification_dispatch +// collect_qualification_run, whose reads sit in the arm the token join admits -- is the only route. +// Reached only through test.claim.runner_qualification_delivery_rewrap_witness. + +import gunbc.runner.runner_qualification_dispatch { DispatchedQualificationRun, CollectedQualificationRun } + +fn relabel(d: DispatchedQualificationRun, c: CollectedQualificationRun) -> CollectedQualificationRun { + CollectedQualificationRun { + dispatched: d, + run: c.run, + floor_job: c.floor_job, + conclusion: c.conclusion, + instruments_unextracted: c.instruments_unextracted, + } +} diff --git a/dag/test/probe/qualification_delivery_rewrap_probe.dag b/dag/test/probe/qualification_delivery_rewrap_probe.dag new file mode 100644 index 00000000000..4d81ba655b4 --- /dev/null +++ b/dag/test/probe/qualification_delivery_rewrap_probe.dag @@ -0,0 +1,19 @@ +module test.probe.qualification_delivery_rewrap_probe + +// THIS MODULE MUST NOT RESOLVE. Each function is a route by which a holder of two legitimate JIT +// deliveries would relabel one: keep delivery B's sealed credential and the runner id GitHub returned +// for B, and claim dispatch A produced them -- so a qualification subject over A would carry B's +// runner. The witness test.claim.runner_qualification_delivery_rewrap_witness hands this source to the +// compiler and requires the refusal at the sealed carrier by name. dag/test/probe/ sits under the +// whole-tree strict-resolve exclusion, so this source reaches the compiler only through that witness. + +import std.types { Int } +import gunbc.runner.runner_jit_perform { + AuthorizedJitMintDispatch, BoundJitCredential, JitCredentialDelivery, JitCredentialBoundToAttempt, +} + +fn rewrap(a: AuthorizedJitMintDispatch, b: BoundJitCredential) -> JitCredentialDelivery { + JitCredentialBoundToAttempt { + bound: BoundJitCredential { dispatch: a, credential: b.credential, runner_id: b.runner_id }, + } +} diff --git a/dag/test/probe/qualification_generate_answer_rewrap_probe.dag b/dag/test/probe/qualification_generate_answer_rewrap_probe.dag new file mode 100644 index 00000000000..d710d3e0c2f --- /dev/null +++ b/dag/test/probe/qualification_generate_answer_rewrap_probe.dag @@ -0,0 +1,15 @@ +module test.probe.qualification_generate_answer_rewrap_probe + +// THIS MODULE MUST NOT RESOLVE. The generate fold pairs a dispatch with a 201 body it is handed, so +// an outside caller would mint a delivery for dispatch A from any created body. Only the perform +// function, whose body is GitHub's answer to dispatch.request, is admitted. Reached only through +// test.claim.runner_qualification_delivery_rewrap_witness. + +import extdeps.transports.rest { RestAnswered } +import extdeps.github.actions_jit_runner { JitConfigCreatedBody } +import gunbc.runner.runner_jit_perform { JitMintDispatch } +import gunbc.github_effect_perform { JitMintPerformance, jit_mint_performance_of_generate } + +fn mint_from_a_supplied_body(a: JitMintDispatch, body: JitConfigCreatedBody) -> JitMintPerformance { + jit_mint_performance_of_generate(dispatch: a, outcome: RestAnswered { answer: body }) +} diff --git a/dag/test/probe/qualification_receive_jit_mint_rewrap_probe.dag b/dag/test/probe/qualification_receive_jit_mint_rewrap_probe.dag new file mode 100644 index 00000000000..ed6688ed778 --- /dev/null +++ b/dag/test/probe/qualification_receive_jit_mint_rewrap_probe.dag @@ -0,0 +1,21 @@ +module test.probe.qualification_receive_jit_mint_rewrap_probe + +// THIS MODULE MUST NOT RESOLVE. It is the rewrap that needs no forged literal: hold an authorized +// dispatch A and a legitimate delivery B, and hand B's credential and runner id to receive_jit_mint +// under A. Unsealed, the result carries bound.dispatch == A and every equality on the dispatch admits +// it. The witness test.claim.runner_qualification_delivery_rewrap_witness requires the refusal at +// receive_jit_mint's admission. dag/test/probe/ sits under the whole-tree strict-resolve exclusion, +// so this source reaches the compiler only through that witness. + +import gunbc.runner.runner_jit_perform { + AuthorizedJitMintDispatch, BoundJitCredential, JitCredentialDelivery, JitMintDispatchAuthorized, + receive_jit_mint, +} +import extdeps.github.actions_jit_runner { JitConfigMinted } + +fn rewrap_through_the_receiver(a: AuthorizedJitMintDispatch, b: BoundJitCredential) -> JitCredentialDelivery { + receive_jit_mint( + dispatch: JitMintDispatchAuthorized { dispatch: a }, + outcome: JitConfigMinted { config: b.credential, runner_id: b.runner_id }, + ) +}