diff --git a/dag/extdeps/github/actions_artifacts.dag b/dag/extdeps/github/actions_artifacts.dag new file mode 100644 index 00000000000..48daa030940 --- /dev/null +++ b/dag/extdeps/github/actions_artifacts.dag @@ -0,0 +1,128 @@ +module extdeps.github.actions_artifacts + +import extdeps.github.github { default_api_base, max_per_page } +import extdeps.github.errors { GitHubErrorShape } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } +import std.credentials { EnvVar } +import std.types { Bool, Bytes, Int, List, String } +import std.resources { Network } +import std.serialization { Text } +import extdeps.ietf.http_semantics { GET } + +// THE GITHUB ACTIONS ARTIFACTS REST API, as the upstream names it: "List workflow run artifacts" +// (operationId actions/list-workflow-run-artifacts) and "Download an artifact" +// (actions/download-artifact), docs.github.com/en/rest/actions/artifacts, read 2026-10-04. +// +// THE DOWNLOAD IS A REDIRECT TO A ZIP, AND BOTH HALVES ARE UPSTREAM FACTS. GitHub answers +// `GET /repos/{owner}/{repo}/actions/artifacts/{artifact_id}/{archive_format}` with `302 Found` and a +// `Location` header naming a short-lived storage URL (about one minute), and `410 Gone` once the +// artifact has expired; `archive_format` admits exactly `zip`, and the body at the Location is the +// artifact as a zip archive -- upload-artifact always archives, even a single file. Following the +// redirect is the bound REST realization's work, not this interface's: the seed handler +// (v1_interpreter observe_rest_exchange, over ureq's redirect policy) follows it and decides on the +// final response, so the response block below names the answer at the end of the redirect. +// +// THE ARCHIVE IS Bytes AND NO BOUND REALIZATION CAN YET CARRY IT. The REST handler reads every body +// as UTF-8 text (RestBodyObservation carries body: String), so a zip arrives as a body that could not +// be read and the call answers RestBodyUndecodable with the status it came under. That refusal is the +// honest answer today and it is typed; reading a member out of the archive needs a binary body +// carrier on the REST transport and an inflate reader, which is +// the trigger of gunbc.runner.runner_qualification_dispatch qualification_instrument_extraction_frontier_rows' +// parse_claim_cost_tsv row. Its production caller is that module's read_claim_cost_artifact. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "docs.github.com/en/rest/actions/artifacts" + } +} + +// THE FIELDS A READER OF A RUN'S ARTIFACTS ASKS OF ONE, AND NO OTHERS. The claim-cost read +// (gunbc.runner.runner_qualification_dispatch conclude_claim_cost_listing) finds the artifact by +// name, refuses it when upstream's `expired` flag is set -- a download would answer 410 -- and +// downloads it by id. Upstream's artifact object also carries size_in_bytes, archive_download_url, +// created_at and expires_at; nothing here reads them, so they are not modeled (DESIGN 3c), and a +// size that one day is read arrives as std.measure ByteSize, not a bare count. +type ActionsArtifact { + id: Int + name: String + expired: Bool +} + +type ActionsArtifactList { + total_count: Int + artifacts: List +} + +// `archive_format` IS A PATH SEGMENT WHOSE UPSTREAM VOCABULARY HAS ONE MEMBER, `zip`, so the path +// carries it as the literal upstream spelling rather than as an input. An input would make every +// other spelling representable, and a coproduct input interpolated into a path is rendered by the +// seed with its AUTHORED variant name (the regression extdeps.github.workflow_runs +// WorkflowJobAttemptFilter records), so neither would be more faithful than the literal. +// AUTHENTICATION IS THE CALLER'S TOKEN. Accepting an auth_token operation input does not by itself +// bind authentication; auth_input names that input as the credential, as extdeps.github.git_database +// and github.WorkflowRuns declare, so the controller installation token the qualification collector +// passes is the one the request carries rather than the ambient GITHUB_TOKEN. An empty token keeps +// the env fallback, the same dual declaration github.WorkflowRuns uses. +service github.Artifacts { + config { + endpoint: default_api_base + auth: Bearer + auth_input: auth_token + auth_source: EnvVar { name: "GITHUB_TOKEN" } + } + + operation ListWorkflowRunArtifacts { + requires Network + input { + auth_token: Secret + owner: String + repo: String + run_id: String + per_page: Int = max_per_page + } + output { + result: ActionsArtifactList + } + readonly + transport rest { + method: GET, + path: "/repos/\{owner\}/\{repo\}/actions/runs/\{run_id\}/artifacts", + query: { per_page: per_page } + } + response { + 200 => ActionsArtifactList + 401 => GitHubErrorShape + 403 => GitHubErrorShape + 404 => GitHubErrorShape + 5xx => GitHubErrorShape + } + } + + operation DownloadArtifact { + requires Network + input { + auth_token: Secret + owner: String + repo: String + artifact_id: String + } + output { + archive: Bytes + } + readonly + transport rest { + method: GET, + path: "/repos/\{owner\}/\{repo\}/actions/artifacts/\{artifact_id\}/zip", + response_format: Text + } + response { + 200 => Bytes + 401 => GitHubErrorShape + 403 => GitHubErrorShape + 404 => GitHubErrorShape + 410 => GitHubErrorShape + 5xx => GitHubErrorShape + } + } +} 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..748a013a95e 100644 --- a/dag/extdeps/github/workflow_runs.dag +++ b/dag/extdeps/github/workflow_runs.dag @@ -15,6 +15,7 @@ import std.dissolution { unbound_dissolution } import std.decl_ref { decl_ref } import std.algebra { Cons, Empty } import std.resources { Network } +import std.serialization { Text } import extdeps.transports.rest { RestResult } // WorkflowJobRun.labels are read by gunbc.public_workload_census (observed_job_labels) to @@ -194,6 +195,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 +209,8 @@ type WorkflowJobRun { status: WorkflowRunStatus conclusion: WorkflowRunConclusion? labels: List + runner_id: Int? + runner_name: String? created_at: Timestamp? started_at: Timestamp? completed_at: Timestamp? @@ -287,16 +296,32 @@ data structural_coverage_gap_workflow_run_codec_hand_rolled: List = [ // operation is not a module item, so per-operation rationale is not expressible; it belongs here // or nowhere. // +// DOWNLOADJOBLOGSFORWORKFLOWRUN IS UPSTREAM'S "Download job logs for a workflow run" +// (actions/download-job-logs-for-workflow-run, docs.github.com/en/rest/actions/workflow-jobs, read +// 2026-10-04): `GET /repos/{owner}/{repo}/actions/jobs/{job_id}/logs` answers `302 Found` with a +// `Location` naming a storage URL that expires after about a minute, and the body there is the job's +// log as plain text, one line per row behind an RFC 3339 timestamp. The redirect is followed by the +// bound REST realization (the seed's ureq handler), so the response block names the text at the end +// of it. A body the handler cannot read -- not UTF-8, or past its read cap -- is RestBodyUndecodable +// with its status, never a truncated log reported as the whole one. +// // THE FILTER IS A CALLER'S CHOICE AND WAS A LITERAL. "latest" returns only the most recent attempt // of each job, which is the right answer for "what is the current state" and the wrong one for any // census of consumed capacity: a re-run mutates a job's record in place, so the attempts "latest" // 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" } } @@ -415,6 +440,33 @@ service github.WorkflowRuns { 500 => GitHubErrorShape } } + operation DownloadJobLogsForWorkflowRun { + requires Network + input { + auth_token: Secret + owner: String + repo: String + job_id: String + } + output { + log: String + } + readonly + transport rest { + method: GET, + path: "/repos/\{owner\}/\{repo\}/actions/jobs/\{job_id\}/logs", + response_format: Text + } + response { + 200 => String + 401 => GitHubErrorShape + 403 => GitHubErrorShape + 404 => GitHubErrorShape + 410 => GitHubErrorShape + 5xx => GitHubErrorShape + } + } + operation ListJobs { requires Network input { diff --git a/dag/extdeps/github/workflows.dag b/dag/extdeps/github/workflows.dag index 858c6c753f3..5fcd64b4899 100644 --- a/dag/extdeps/github/workflows.dag +++ b/dag/extdeps/github/workflows.dag @@ -2,13 +2,9 @@ module extdeps.github.workflows 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 } @@ -41,40 +37,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, @@ -82,7 +75,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 f408c87efb6..16ec09ed3e6 100644 --- a/dag/gunbc/auth/privileged_effect_census.dag +++ b/dag/gunbc/auth/privileged_effect_census.dag @@ -386,6 +386,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: runner_lifecycle_operator_ruling.interlock, + 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: group_a_dev_standing_grant.ruling.interlock, @@ -541,6 +548,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: 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 + } +} + data privileged_effect_census: List = [ PrivilegedEffectSite { site: site(module_path: "gunbc.live_deploy.emit", decl_name: "approval_broker_helper_grant_steps"), @@ -593,6 +654,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 61d97a11cbb..97c9ee39cec 100644 --- a/dag/gunbc/github_effect_perform.dag +++ b/dag/gunbc/github_effect_perform.dag @@ -1,7 +1,8 @@ module gunbc.github_effect_perform -import std.types { String, NonEmptyStr, Int, List, Secret, EpochSecs } +import std.types { String, NonEmptyStr, Int, List, Secret, EpochSecs, Bytes } 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,16 @@ 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 extdeps.github.actions_artifacts +import extdeps.github.actions_artifacts { ActionsArtifactList } import gunbc.auth.github_apps { DeclaredGitHubApp, gunbai_ci_declared } import extdeps.github.app { GitHubAppInstallationId } import gunbc.runner.runner_jit_perform { @@ -138,10 +149,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 +335,157 @@ 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 RUN'S OUTPUTS, READ UNDER THE SAME CONTROLLER TOKEN AS THE RUN ITSELF. One job's +// log (actions/download-job-logs-for-workflow-run, followed through its redirect by the bound REST +// handler), the run's artifact listing, and one artifact's archive. Each answer is sealed beside its +// RestResult, like the run and job reads above, so a consumer cannot pair a body with a result it +// did not come with. The archive is Bytes and today's handler reads bodies as text, +// so a real download answers RestRefused with RestBodyUndecodable (extdeps.github.actions_artifacts). +type WorkflowJobLogRead sole_constructor { + job_id: Int + log: RestResult +} + +fn read_job_log_with(token: ControllerInstallationToken, owner: NonEmptyStr, repo: NonEmptyStr, job_id: Int) -> WorkflowJobLogRead uses net: Network { + let read = github.WorkflowRuns.DownloadJobLogsForWorkflowRun(auth_token: token.token, owner: owner as String, repo: repo as String, job_id: job_id as String) + WorkflowJobLogRead { + job_id: job_id, + log: match read { + RestAnswered { answer } => RestAnswered { answer: answer.log } + RestRefused { refusal } => RestRefused { refusal: refusal } + }, + } +} + +type WorkflowRunArtifactsRead sole_constructor { + listed: RestResult +} + +fn list_run_artifacts_with(token: ControllerInstallationToken, owner: NonEmptyStr, repo: NonEmptyStr, run_id: Int) -> WorkflowRunArtifactsRead uses net: Network { + let read = github.Artifacts.ListWorkflowRunArtifacts(auth_token: token.token, owner: owner as String, repo: repo as String, run_id: run_id as String) + WorkflowRunArtifactsRead { + listed: match read { + RestAnswered { answer } => RestAnswered { answer: answer.result } + RestRefused { refusal } => RestRefused { refusal: refusal } + }, + } +} + +type ArtifactArchiveRead sole_constructor { + artifact_id: Int + archive: RestResult +} + +fn download_artifact_with(token: ControllerInstallationToken, owner: NonEmptyStr, repo: NonEmptyStr, artifact_id: Int) -> ArtifactArchiveRead uses net: Network { + let read = github.Artifacts.DownloadArtifact(auth_token: token.token, owner: owner as String, repo: repo as String, artifact_id: artifact_id as String) + ArtifactArchiveRead { + artifact_id: artifact_id, + archive: match read { + RestAnswered { answer } => RestAnswered { answer: answer.archive } + 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/host/host_budget_source.dag b/dag/gunbc/host/host_budget_source.dag index 2cb18c62a96..83e78ac966a 100644 --- a/dag/gunbc/host/host_budget_source.dag +++ b/dag/gunbc/host/host_budget_source.dag @@ -4,6 +4,11 @@ import std.types { NonEmptyStr, String, Bool, List } import std.measure { ByteSize, byte_size_count } import std.os.types { KernelFamily, Linux, Darwin, WindowsNt, LinuxGuestOnWindows } import extdeps.linux.cgroup_v2 { kernel_provides_cgroup_v2 } +import extdeps.linux.cgroup_v2_memory { + CgroupMemoryLimitValue, CgroupMemoryLimited, CgroupMemoryUnlimited, CgroupMemoryLimitUnparseable, + CgroupMemoryCount, CgroupMemoryCountUnparseable, parse_cgroup_memory_limit, parse_cgroup_memory_count, +} +import gunbc.required_ci_phase_roster { floor_log_row_fields, floor_log_field_value } import std.disposition { Disposition, Terminal, Scaffold, SingleAuthority } import std.decl_ref { DeclarationRef, WholeDeclaration } import extdeps.linux.procfs { @@ -353,3 +358,69 @@ data host_budget_source_seed_mirror_disposition: Disposition = Scaffold { data host_budget_source_seed_mirror_note: String = "THIS MODEL IS THE AUTHORITY AND v1 STILL HAND-REALIZES IT, which is a mirror of exactly the kind that just went stale elsewhere in this change — so it is declared rather than left implicit. memory_governor::read_host_budget_bytes composes its own labels and cli_run::typed_module_cache_cap_derivation computes its own degraded flag, and neither reads these rows.\n\nWhy the mirror cannot simply be deleted today: one consumer runs strictly before any .dag value could exist. cli_run's enforce_typed_cache_entry_cap derives the typed-module-cache eviction bound from this same budget WHILE MODULES ARE BEING RESOLVED — it is the thing bounding the memory used to resolve the corpus, so it cannot be a value obtained by resolving the corpus. The governor's own arm in claim_executor is different and could in principle read a resolved value (it happens after the plan resolve), so that half is ordinary seed-shrink debt rather than a bootstrap constraint. The two must not be conflated when the emit lands: the first needs the value baked into the seed, the second only needs the seed to stop duplicating it.\n\nTHAT CHECK NOW EXISTS BUT IS NOT RUN BY CI, and the distinction is the whole point of this row: test.claim.seed_mirror_constant_lens_witness_test reads the seed's constants against their authority rows and covers the union of what this note and gunbc.typed_module_cache_capacity's seed_mirror_note each asked for separately — DECLARED_RUNNER_SLOT_MEMORY_HIGH_BYTES, DECLARED_FLOOR_MINIMUM_VIABLE_ARMED_BUDGET_BYTES, and the three typed-module-cache constants. Two notes naming different overlapping subsets, neither of which was the union, was itself two partial specifications of one mechanism. THIS NOTE'S OWN WARNING CAME TRUE AND IS WORTH KEEPING FOR IT. It cited DECLARED_RUNNER_SLOT_MEMORY_HIGH_BYTES as having drifted once already; it then drifted again and sat eleven days at 13958643712 against an authority of 16106127360 (gunbc.runner_slot_desired gunbc_runner_slot_desired, moved by #8388 on 2026-08-17). Knowing about a gap and naming its fix is not the same as closing it, and the interval is the receipt. Note also that the sibling witness could not have caught it: test.claim.host_budget_source_witness built its expectation from the mirror value retyped, so it greened whichever way the mirror went — a second inert-by-construction surface, since corrected to derive from the row." + +// ── THE FLOOR'S [floor-cgroup] LEVEL ROWS, READ BACK FROM A RUN'S LOG ────────────────────────── +// +// The floor prints, at entry and on every heartbeat, one `[floor-cgroup] when= level=` +// row per cgroup level from its own cgroup upward, carrying that level's memory.max, memory.high, +// memory.current and memory.peak as the kernel spelled them (plus events and pressure, which this +// reading does not take). The budget this module resolves IS the memory.high of the slot level, so +// the bound and the peak a qualification reads are denominated in this module's vocabulary -- which is +// why gunbc.runner_throughput_qualification_route names HostBudgetResolution as their producer. The +// values are decoded by extdeps.linux.cgroup_v2_memory, the kernel interface's own authority, never +// re-parsed here: `max` is CgroupMemoryUnlimited, never a large number. +// +// The `when= path=` row the floor prints beside them is a different row (the process's +// own cgroup path, no readings) and is not a level row: it reads as none, like any other line. +type FloorCgroupLevelRow { + when: NonEmptyStr + level: NonEmptyStr + high: CgroupMemoryLimitValue + peak: ByteSize +} + +type FloorCgroupRowReading + = FloorCgroupLevelRead { row: FloorCgroupLevelRow } + | FloorCgroupRowGarbled { line: String, cause: NonEmptyStr } + +data floor_cgroup_row_tag: String = "[floor-cgroup]" + +fn floor_cgroup_garbled(line: String, cause: String) -> FloorCgroupRowReading? { + Present { value: FloorCgroupRowGarbled { line: line, cause: cause as NonEmptyStr } } +} + +fn read_floor_cgroup_level_row(line: String) -> FloorCgroupRowReading? { + match floor_log_row_fields(line: line, tag: floor_cgroup_row_tag) { + Absent => none + Present { value: fields } => + match floor_log_field_value(fields: fields, key: "level") { + Absent => none + Present { value: level } => + match floor_log_field_value(fields: fields, key: "when") { + Absent => floor_cgroup_garbled(line: line, cause: "[floor-cgroup] level row carries no when= field") + Present { value: when } => + if when == "" || level == "" { + floor_cgroup_garbled(line: line, cause: "[floor-cgroup] level row carries an empty when= or level= field") + } else { + match floor_log_field_value(fields: fields, key: "high") { + Absent => floor_cgroup_garbled(line: line, cause: "[floor-cgroup] level row carries no high= field") + Present { value: raw_high } => + match parse_cgroup_memory_limit(body: raw_high) { + CgroupMemoryLimitUnparseable { body: _ } => floor_cgroup_garbled(line: line, cause: "[floor-cgroup] high= is neither a byte count nor max") + high => + match floor_log_field_value(fields: fields, key: "peak") { + Absent => floor_cgroup_garbled(line: line, cause: "[floor-cgroup] level row carries no peak= field") + Present { value: raw_peak } => + match parse_cgroup_memory_count(body: raw_peak) { + CgroupMemoryCountUnparseable { body: _ } => floor_cgroup_garbled(line: line, cause: "[floor-cgroup] peak= is not a byte count") + CgroupMemoryCount { bytes: peak } => + Present { value: FloorCgroupLevelRead { row: FloorCgroupLevelRow { when: when as NonEmptyStr, level: level as NonEmptyStr, high: high, peak: peak } } } + } + } + } + } + } + } + } + } +} 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/required_ci_phase_roster.dag b/dag/gunbc/required_ci_phase_roster.dag index e76f1dfbaf8..2c181a186a0 100644 --- a/dag/gunbc/required_ci_phase_roster.dag +++ b/dag/gunbc/required_ci_phase_roster.dag @@ -1,6 +1,9 @@ module gunbc.required_ci_phase_roster -import std.types { String, Bool, List } +import std.types { String, Bool, Int, List, NonEmptyStr } +import std.measure { Millisecond, millisecond } +import std.checked_arithmetic { nat_magnitude } +import v2.std.optional { Present, Absent } // THE SUBSTRATE AUTHORITY FOR WHICH PHASES REQUIRED CI RUNS, AND WHICH LANE OWNS EACH. // gunbc.required_ci_host_verdict_census recorded the gap this module closes: "Phase existence and @@ -196,3 +199,97 @@ fn required_ci_lane_phase_rows() -> List { phase: required_ci_phase_name(p: p) }) } + +// ── THE FLOOR PHASE'S OWN PROGRESS ROWS, READ BACK FROM A RUN'S LOG ───────────────────────────── +// +// FloorPhase is one RequiredCiPhase; inside it the host prints `[floor-phase] phase= ...` rows +// for its own preparation stages (claim_executor, cli_run). Those stage WORDS are not this roster's +// vocabulary -- they are an open host vocabulary with no substrate authority, so a reading carries +// the word as the host spelled it and never maps it onto RequiredCiPhase. What this module owns is +// the reading's denominator: these rows are the timings OF required_ci_phases' FloorPhase, which is +// why gunbc.runner_throughput_qualification_route names this module as their producer. +// +// THE LINE ENCODING IS `[tag] key=value key=value`, one row per line, possibly behind the timestamp +// GitHub prefixes to each job-log line. floor_log_row_fields is the one reader of that encoding; the +// [floor-cgroup] reader (gunbc.host_budget_source) uses it rather than tokenizing a second time. A +// value may itself contain `=` (the cgroup pressure field does), so only the FIRST `=` splits. +type FloorLogField { + key: String + value: String +} + +fn floor_log_field(token: String) -> FloorLogField? { + let parts = split(s: token, delimiter: "=") + match parts.first() { + Absent => none + Present { value: k } => + if count(parts) < 2 { + none + } else { + let v = substring(s: token, start: string_length(s: k) + 1, end: string_length(s: token)) + Present { value: FloorLogField { key: k, value: v } } + } + } +} + +// none: the line is not a row of this tag. A row of the tag yields its fields, possibly empty. +fn floor_log_row_fields(line: String, tag: String) -> List? { + let halves = split(s: line, delimiter: concat(tag, " ")) + match halves.skip(n: 1).first() { + Absent => none + Present { value: payload } => + if count(halves) != 2 { + none + } else { + let tokens = split(s: payload, delimiter: " ") + let fields = tokens |> flat_map(t => match floor_log_field(token: t) { Absent => [] Present { value: f } => [f] }) + Present { value: fields } + } + } +} + +fn floor_log_field_value(fields: List, key: String) -> String? { + match fields |> filter(f => f.key == key) |> first { + Absent => none + Present { value: f } => Present { value: f.value } + } +} + +data floor_phase_row_tag: String = "[floor-phase]" + +// A STAGE ROW EITHER CARRIES ITS WALL OR DOES NOT, and the two are not one row with a zero. The host +// prints `state=started` rows and classification rows with no wall_ms; reporting those as 0 ms would +// fabricate a timing. A row with no phase word, or a wall_ms that is not a count, is garbled and is +// carried with its line, never skipped. +type FloorPhaseRow + = FloorPhaseTimed { phase: NonEmptyStr, wall: Millisecond } + | FloorPhaseUntimed { phase: NonEmptyStr } + +type FloorPhaseRowReading + = FloorPhaseRowRead { row: FloorPhaseRow } + | FloorPhaseRowGarbled { line: String, cause: NonEmptyStr } + +fn read_floor_phase_row(line: String) -> FloorPhaseRowReading? { + match floor_log_row_fields(line: line, tag: floor_phase_row_tag) { + Absent => none + Present { value: fields } => + match floor_log_field_value(fields: fields, key: "phase") { + Absent => Present { value: FloorPhaseRowGarbled { line: line, cause: "[floor-phase] row carries no phase= field" as NonEmptyStr } } + Present { value: "" } => Present { value: FloorPhaseRowGarbled { line: line, cause: "[floor-phase] row carries an empty phase= field" as NonEmptyStr } } + Present { value: phase } => + match floor_log_field_value(fields: fields, key: "wall_ms") { + Absent => Present { value: FloorPhaseRowRead { row: FloorPhaseUntimed { phase: phase as NonEmptyStr } } } + Present { value: raw } => + match parse_int(s: raw) { + Absent => Present { value: FloorPhaseRowGarbled { line: line, cause: "[floor-phase] wall_ms is not a count" as NonEmptyStr } } + Present { value: ms } => + if ms < 0 { + Present { value: FloorPhaseRowGarbled { line: line, cause: "[floor-phase] wall_ms is negative" as NonEmptyStr } } + } else { + Present { value: FloorPhaseRowRead { row: FloorPhaseTimed { phase: phase as NonEmptyStr, wall: millisecond(count: nat_magnitude(a: ms)) } } } + } + } + } + } + } +} diff --git a/dag/gunbc/runner/runner_attempt_launch.dag b/dag/gunbc/runner/runner_attempt_launch.dag index 230408165af..325f26234e2 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 { @@ -207,7 +207,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 } { @@ -225,6 +228,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 194929ded32..a552e0e2319 100644 --- a/dag/gunbc/runner/runner_microvm_slot_controller.dag +++ b/dag/gunbc/runner/runner_microvm_slot_controller.dag @@ -530,7 +530,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..accbcb1e670 --- /dev/null +++ b/dag/gunbc/runner/runner_qualification_dispatch.dag @@ -0,0 +1,1219 @@ +module gunbc.runner.runner_qualification_dispatch + +import std.types { Bool, Bytes, 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, RestStatusRefused, RestTransportRefused, RestBodyUndecodable, + 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.fleet_converge_workflow { fleet_converge_workflow, fleet_converge_dispatch_inputs } +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, + WorkflowJobLogRead, read_job_log_with, list_run_artifacts_with, download_artifact_with, +} +import gunbc.runner_throughput_qualification_route { + QualificationInstrument, qualification_instruments, + FloorPhaseRows, FloorCgroupRows, ClaimCostArtifactEvalSteps, CalibrationSpecimenWitnessLine, + GuestIdleMeminfoAndNproc, ConcurrentCohortSeatWindows, +} +import gunbc.required_ci_phase_roster { + FloorPhaseRow, FloorPhaseTimed, FloorPhaseUntimed, FloorPhaseRowReading, FloorPhaseRowRead, FloorPhaseRowGarbled, + read_floor_phase_row, +} +import gunbc.host_budget_source { + FloorCgroupLevelRow, FloorCgroupRowReading, FloorCgroupLevelRead, FloorCgroupRowGarbled, + read_floor_cgroup_level_row, +} +import gunbc.witness_floor_workflow { required_floor_claim_cost_artifact_name } +import extdeps.github.actions_artifacts { ActionsArtifact, ActionsArtifactList } +import gunbc.runner.runner_host_unit_slot { HostUnitSlot } +import std.content_hash { Fnv1a64Structural, content_hash_atom } +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 +// 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_dispatch", 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 } } + } + } +} + +// 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, + ) + } +} + +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 } + +// A COLLECTED RUN SAYS WHICH JOB IS THE FLOOR AND NOTHING YET ABOUT WHAT IT MEASURED. The instruments +// are read from it afterwards by collect_qualification_instruments, from floor_job alone. +type CollectedQualificationRun sole_constructor { + dispatched: DispatchedQualificationRun + run: WorkflowRun + floor_job: WorkflowJobRun + conclusion: WorkflowRunConclusion +} + +type QualificationRunCollection + = QualificationRunCollected { collected: CollectedQualificationRun } + | QualificationRunRefused { run_id: Int, refusal: QualificationRunRefusal } + +fn qualification_run_collected(c: QualificationRunCollection) -> Bool { + match c { + QualificationRunCollected { collected: _ } => true + QualificationRunRefused { run_id: _, refusal: _ } => false + } +} + +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, + }, + } + } + } + } +} + +// ── EXTRACT: THE INSTRUMENTS READ FROM THE COLLECTED RUN ────────────────────────────────────── +// +// WHERE EACH INSTRUMENT IS READ FROM IS A TOTAL MATCH, so adding an instrument to +// gunbc.runner_throughput_qualification_route QualificationInstrument refuses to compile here until it +// says where its reading comes from. Two are the designated floor job's log; two are this run's +// required-floor-claim-cost artifact, whose read is attempted on every collection and today ends in a +// typed refusal (read_claim_cost_artifact); two are not outputs of this run at all. Each of the +// four is carried by a row below with the capability that would read it, and the two log +// instruments carry a row too until the route invokes collect_qualification_instruments. +type QualificationInstrumentSource + = ReadFromAttemptJobLog + | ReadFromClaimCostArtifact + | ReadFromBootLegReadback + | ReadFromCohortObservation + +fn qualification_instrument_source(i: QualificationInstrument) -> QualificationInstrumentSource { + match i { + FloorPhaseRows => ReadFromAttemptJobLog + FloorCgroupRows => ReadFromAttemptJobLog + ClaimCostArtifactEvalSteps => ReadFromClaimCostArtifact + CalibrationSpecimenWitnessLine => ReadFromClaimCostArtifact + GuestIdleMeminfoAndNproc => ReadFromBootLegReadback + ConcurrentCohortSeatWindows => ReadFromCohortObservation + } +} + +fn qualification_instrument_read_from_job_log(i: QualificationInstrument) -> Bool { + match qualification_instrument_source(i: i) { + ReadFromAttemptJobLog => true + ReadFromClaimCostArtifact => false + ReadFromBootLegReadback => false + ReadFromCohortObservation => false + } +} + +// ── THE PURE DECODER ────────────────────────────────────────────────────────────────────────── +// +// It decides what one log's text says and nothing about whose log it is; identity is the subject's +// and the receipt's. It is open so the row shapes are witnessable on supplied and recorded text. +// The phase rows are every [floor-phase] row the log printed, timed and untimed, in log order; the +// cgroup rows are only the [floor-cgroup] rows at the slot's own level, because the levels above it +// are other subjects' memory and a qualification of this slot must not take their peak for its own. +type QualificationLogReadings { + floor_phase_rows: List + slot_cgroup_rows: List +} + +type InstrumentReadRefusal + = FloorPhaseRowGarbledInLog { line: String, cause: NonEmptyStr } + | FloorCgroupRowGarbledInLog { line: String, cause: NonEmptyStr } + | FloorPhaseRowsAbsent + | SlotCgroupLevelAbsent { slot_unit: NonEmptyStr, levels_seen: List } + +type JobLogInstrumentDecode + = JobLogInstrumentsDecoded { readings: QualificationLogReadings } + | JobLogInstrumentsUndecodable { refusal: InstrumentReadRefusal } + +// A garbled row stops the read: a reading assembled around a row it skipped would report a phase +// or a level as absent that the run printed. +type JobLogRowsReading + = JobLogRowsRead { phases: List, levels: List } + | JobLogRowsRefused { refusal: InstrumentReadRefusal } + +fn read_job_log_line(acc: JobLogRowsReading, line: String) -> JobLogRowsReading { + match acc { + JobLogRowsRefused { refusal: _ } => acc + JobLogRowsRead { phases: ps, levels: ls } => + match read_floor_phase_row(line: line) { + Present { value: FloorPhaseRowGarbled { line: l, cause: c } } => + JobLogRowsRefused { refusal: FloorPhaseRowGarbledInLog { line: l, cause: c } } + Present { value: FloorPhaseRowRead { row: r } } => JobLogRowsRead { phases: list_push(ps, r), levels: ls } + Absent => + match read_floor_cgroup_level_row(line: line) { + Present { value: FloorCgroupRowGarbled { line: l, cause: c } } => + JobLogRowsRefused { refusal: FloorCgroupRowGarbledInLog { line: l, cause: c } } + Present { value: FloorCgroupLevelRead { row: r } } => JobLogRowsRead { phases: ps, levels: list_push(ls, r) } + Absent => acc + } + } + } +} + +fn level_is_slot(row: FloorCgroupLevelRow, slot_unit: NonEmptyStr) -> Bool { + ends_with(s: row.level as String, suffix: concat("/", slot_unit as String)) +} + +fn phase_row_is_timed(p: FloorPhaseRow) -> Bool { + match p { + FloorPhaseTimed { phase: _, wall: _ } => true + FloorPhaseUntimed { phase: _ } => false + } +} + +fn decode_job_log_instruments(log: String, slot_unit: NonEmptyStr) -> JobLogInstrumentDecode { + match fold(split(s: log, delimiter: "\n"), init: JobLogRowsRead { phases: [], levels: [] }, f: (acc, line) => read_job_log_line(acc: acc, line: line)) { + JobLogRowsRefused { refusal: r } => JobLogInstrumentsUndecodable { refusal: r } + JobLogRowsRead { phases: phases, levels: levels } => { + let slot_levels = levels |> filter(l => level_is_slot(row: l, slot_unit: slot_unit)) + if count(phases |> filter(p => phase_row_is_timed(p: p))) == 0 { + JobLogInstrumentsUndecodable { refusal: FloorPhaseRowsAbsent } + } else if count(slot_levels) == 0 { + JobLogInstrumentsUndecodable { refusal: SlotCgroupLevelAbsent { slot_unit: slot_unit, levels_seen: levels |> map(l => l.level as String) } } + } else { + JobLogInstrumentsDecoded { readings: QualificationLogReadings { floor_phase_rows: phases, slot_cgroup_rows: slot_levels } } + } + } + } +} + +// ── THE READ, AND THE RECEIPT ONLY THE READ CAN MINT ────────────────────────────────────────── +// +// A log is admitted only if it is the designated job's: the read is addressed by the subject's job +// id, and the join below is what a supplied log of any other job fails. +type AttemptJobLog + = AttemptJobLogRead { job_id: Int, log: String } + | AttemptJobLogUnreadable { job_id: Int, refusal: RestExchangeRefusal } + +type JobLogReadRefusal + = JobLogOfAnotherJob { designated_job_id: Int, read_job_id: Int } + | JobLogUnreadable { job_id: Int, refusal: RestExchangeRefusal } + | JobLogEmpty { job_id: Int } + | JobLogUndecodable { job_id: Int, refusal: InstrumentReadRefusal } + +type DesignatedJobLog + = DesignatedJobLogText { job_id: Int, log: NonEmptyStr } + | DesignatedJobLogRefused { refusal: JobLogReadRefusal } + +fn designated_job_log(designated_job_id: Int, log: AttemptJobLog) -> DesignatedJobLog { + match log { + AttemptJobLogUnreadable { job_id: j, refusal: o } => + if j != designated_job_id { + DesignatedJobLogRefused { refusal: JobLogOfAnotherJob { designated_job_id: designated_job_id, read_job_id: j } } + } else { + DesignatedJobLogRefused { refusal: JobLogUnreadable { job_id: j, refusal: o } } + } + AttemptJobLogRead { job_id: j, log: text } => + if j != designated_job_id { + DesignatedJobLogRefused { refusal: JobLogOfAnotherJob { designated_job_id: designated_job_id, read_job_id: j } } + } else if text == "" { + DesignatedJobLogRefused { refusal: JobLogEmpty { job_id: j } } + } else { + DesignatedJobLogText { job_id: j, log: text as NonEmptyStr } + } + } +} + +// THE SUCCESS RECEIPT IS SEALED AND CARRIES ITS EVIDENCE. Only collect_qualification_instruments +// writes it, and only after reading the designated job's log over the network: the subject it +// names (the collection, which carries the sealed dispatch and the joined floor job, and the slot whose +// unit the cgroup rows are filtered to), the length (in Unicode code points, as the transport hands the body over) and the content +// digest of the complete log body the rows came from, and the rows. A later assessment does not +// have to trust rows detached from the job and the bytes that produced them. The decoder above is +// open; this record is not. +// +// THE SEAL IS ENROLLED AS EXECUTED REDS. test.claim.qualification_job_log_receipt_forged_probe_witness +// compiles test.probe.qualification_job_log_receipt_forged_probe -- a receipt written from invented +// readings, and job_log_standing called from outside the collect stage -- and requires a +// SoleConstructorViolation at QualificationJobLogReceipt and a ConstructorCallAdmissionRefused at +// job_log_standing, beside a control that only names this module and refuses at neither. Removing +// sole_constructor from this record or the admit list from job_log_standing turns that witness red. +type QualificationJobLogReceipt sole_constructor { + collected: CollectedQualificationRun + slot: HostUnitSlot + log_code_points: Int + log_digest: Fnv1a64Structural + readings: QualificationLogReadings +} + +// A STANDING PER INSTRUMENT SOURCE, NOT ONE "INSTRUMENTS READ" ARM. The job-log instruments either +// carry the sealed receipt or the typed reason they do not; the claim-cost read carries its own +// typed standing beside it; the boot-leg and cohort instruments are not in this stage's payload at +// all and are rows below. Nothing in this value says the collect stage is complete. +type JobLogInstrumentStanding + = QualificationJobLogInstrumentsRead { receipt: QualificationJobLogReceipt } + | QualificationJobLogInstrumentsRefused { refusal: JobLogReadRefusal } + +type QualificationCollectStage { + job_log: JobLogInstrumentStanding + claim_cost: ClaimCostArtifactRead +} + +fn job_log_standing(collected: CollectedQualificationRun, slot: HostUnitSlot, log: AttemptJobLog) -> JobLogInstrumentStanding + admit_callers: [ + decl_ref(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "collect_qualification_instruments_under"), + ] +{ + match designated_job_log(designated_job_id: collected.floor_job.id, log: log) { + DesignatedJobLogRefused { refusal: r } => QualificationJobLogInstrumentsRefused { refusal: r } + DesignatedJobLogText { job_id: j, log: text } => + match decode_job_log_instruments(log: text as String, slot_unit: slot.unit) { + JobLogInstrumentsUndecodable { refusal: r } => QualificationJobLogInstrumentsRefused { refusal: JobLogUndecodable { job_id: j, refusal: r } } + JobLogInstrumentsDecoded { readings: rd } => + QualificationJobLogInstrumentsRead { + receipt: QualificationJobLogReceipt { + collected: collected, + slot: slot, + log_code_points: string_length(s: text as String), + log_digest: content_hash_atom(value: text), + readings: rd, + }, + } + } + } +} + +fn attempt_job_log_of(read: WorkflowJobLogRead) -> AttemptJobLog { + match read.log { + RestAnswered { answer: text } => AttemptJobLogRead { job_id: read.job_id, log: text } + RestRefused { refusal: r } => AttemptJobLogUnreadable { job_id: read.job_id, refusal: classify_rest_refusal(standing: RestReadExchange { refusal: r }) } + } +} + +// THE CLAIM-COST ARTIFACT, READ AS FAR AS ANY BOUND REALIZATION CAN READ IT. It is looked up by the +// name the floor workflow uploads it under (gunbc.witness_floor_workflow +// required_floor_claim_cost_artifact_name), downloaded through GitHub's redirect, and every way that +// can fail is its own arm. An archive that DID arrive is still not a reading: it is a zip, and no +// inflate reader exists to take the TSV out of it, so that arm says so instead of passing bytes on +// as if they were the TSV. There is deliberately no parsed arm yet; it lands with the capability the +// parse_claim_cost_tsv row of qualification_instrument_extraction_frontier_rows names, at which point +// this read hands the member to gunbc.floor_cost_distribution parse_claim_cost_tsv. +type ClaimCostArtifactRead + = ClaimCostArtifactListUnreadable { refusal: RestExchangeRefusal } + | ClaimCostArtifactListTruncated { returned: Int, total: Int } + | ClaimCostArtifactAbsent { names_seen: List } + | ClaimCostArtifactAmbiguous { artifact_ids: List } + | ClaimCostRunUnreadable { refusal: RestExchangeRefusal } + | ClaimCostRunAdvancedPastAttempt { observed_attempt: Int } + | ClaimCostArtifactExpired { artifact_id: Int } + | ClaimCostArchiveUnreadable { artifact_id: Int, refusal: RestExchangeRefusal } + | ClaimCostArchiveNotInflatable { artifact_id: Int } + +fn claim_cost_artifacts_named(listed: ActionsArtifactList) -> List { + listed.artifacts |> filter(a => a.name == required_floor_claim_cost_artifact_name) +} + +fn claim_cost_artifact_listed(listed: ActionsArtifactList) -> ActionsArtifact? { + let named = claim_cost_artifacts_named(listed: listed) + if count(named) == 1 { named |> first } else { none } +} + +// none: the listing names an unexpired claim-cost artifact and the download is owed. +fn listed_claim_cost_artifact(listed: RestResult) -> ActionsArtifact? { + match listed { + RestAnswered { answer: l } => claim_cost_artifact_listed(listed: l) + RestRefused { refusal: _ } => none + } +} + +fn conclude_claim_cost_listing(listed: RestResult) -> ClaimCostArtifactRead? { + match listed { + RestAnswered { answer: l } => + if count(l.artifacts) != l.total_count { + Present { value: ClaimCostArtifactListTruncated { returned: count(l.artifacts), total: l.total_count } } + } else { + match claim_cost_artifact_listed(listed: l) { + Absent => + if count(claim_cost_artifacts_named(listed: l)) > 1 { + Present { value: ClaimCostArtifactAmbiguous { artifact_ids: claim_cost_artifacts_named(listed: l) |> map(a => a.id) } } + } else { + Present { value: ClaimCostArtifactAbsent { names_seen: l.artifacts |> map(a => a.name) } } + } + Present { value: a } => + if a.expired { Present { value: ClaimCostArtifactExpired { artifact_id: a.id } } } else { none } + } + } + RestRefused { refusal: r } => Present { value: ClaimCostArtifactListUnreadable { refusal: classify_rest_refusal(standing: RestReadExchange { refusal: r }) } } + } +} + +// THE ARTIFACT IS BOUND TO ATTEMPT 1 BY READING THE RUN AFTER THE LISTING. Upstream's artifact object +// names its workflow run's id, head SHA and branch but no attempt, and a re-run reuses the run id, so a +// listing alone cannot tell attempt 1's artifact from a re-run's. A re-run that uploaded before the +// listing was taken had already advanced the run, so re-reading the run AFTER the listing and requiring +// run_attempt to still be the dispatched attempt excludes every artifact the listing could have seen +// from a later attempt. none: the run is still at the collected attempt. +fn conclude_claim_cost_attempt(run: RestResult) -> ClaimCostArtifactRead? { + match run { + RestAnswered { answer: r } => + if r.run_attempt != dispatched_run_attempt { + Present { value: ClaimCostRunAdvancedPastAttempt { observed_attempt: r.run_attempt } } + } else { + none + } + RestRefused { refusal: f } => Present { value: ClaimCostRunUnreadable { refusal: classify_rest_refusal(standing: RestReadExchange { refusal: f }) } } + } +} + +// A 410 ON THE DOWNLOAD IS UPSTREAM'S EXPIRY ANSWER (actions/download-artifact documents 410 Gone for +// an expired artifact), so it is ClaimCostArtifactExpired like the listing's own flag, not a generic +// unreadable archive. +fn conclude_claim_cost_download(artifact_id: Int, archive: RestResult) -> ClaimCostArtifactRead { + match archive { + RestAnswered { answer: _ } => ClaimCostArchiveNotInflatable { artifact_id: artifact_id } + RestRefused { refusal: r } => + match r { + RestStatusRefused { status: st, body: _ } => + if st == 410 { + ClaimCostArtifactExpired { artifact_id: artifact_id } + } else { + ClaimCostArchiveUnreadable { artifact_id: artifact_id, refusal: classify_rest_refusal(standing: RestReadExchange { refusal: r }) } + } + RestTransportRefused { cause: _ } => ClaimCostArchiveUnreadable { artifact_id: artifact_id, refusal: classify_rest_refusal(standing: RestReadExchange { refusal: r }) } + RestBodyUndecodable { status: _, cause: _ } => ClaimCostArchiveUnreadable { artifact_id: artifact_id, refusal: classify_rest_refusal(standing: RestReadExchange { refusal: r }) } + } + } +} + +fn read_claim_cost_artifact(token: ControllerInstallationToken, owner: NonEmptyStr, repo: NonEmptyStr, run_id: Int) -> ClaimCostArtifactRead + uses net: Network + admit_callers: [ + decl_ref(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "collect_qualification_instruments_under"), + ] +{ + let listed = list_run_artifacts_with(token: token, owner: owner, repo: repo, run_id: run_id) + let after = read_run_with(token: token, owner: owner, repo: repo, run_id: run_id) + match conclude_claim_cost_listing(listed: listed.listed) { + Present { value: refused } => refused + Absent => + match conclude_claim_cost_attempt(run: after.run) { + Present { value: refused } => refused + Absent => + match listed_claim_cost_artifact(listed: listed.listed) { + Absent => ClaimCostArtifactAbsent { names_seen: [] } + Present { value: a } => { + let archive = download_artifact_with(token: token, owner: owner, repo: repo, artifact_id: a.id) + conclude_claim_cost_download(artifact_id: a.id, archive: archive.archive) + } + } + } + } +} + +// THE PRODUCTION ENTRY. It takes the sealed collection and the controller token, and refuses before any +// read unless that token is the registration's App and installation (token_names_registration, the +// join collect_qualification_run makes), so it reads nothing under another installation. Nothing +// else a caller could cross-wire: the repository is gunbc_repository, the run, revision and attempt are the +// collection's, the floor job is the one collect_qualification_run joined to the minted runner, and +// the slot is that registration's own host-unit slot. It reads the floor job's log and the claim-cost +// artifact and returns a standing per instrument source. Its consumer is the route's collect stage +// (gunbc.runner_throughput_qualification_route CollectInstruments, standing mtcollins1_collect_leg), +// which does not invoke it yet: that edge is the row below. +// The microVM arm is refused by the dispatch subject already (SubjectSlotNotHostUnit), so no collected +// run carries one; the arm exists because the slot sum does, and it reads nothing. +type QualificationCollectOutcome + = QualificationCollected { stage: QualificationCollectStage } + | QualificationCollectSlotNotAHostUnit + | QualificationCollectUnderAnotherInstallation { token_app: DeclaredGitHubApp, token_installation: GitHubAppInstallationId } + +// THE READ PLAN, PURE: WHICH READS THE COLLECTOR MAY MAKE, DECIDED BEFORE ANY OF THEM. A token that +// does not name the registration's App and installation (token_names_registration, the same join +// collect_qualification_run makes) plans no reads at all; otherwise the plan is the designated floor +// job's log and this run's artifacts, by id. The collector below performs exactly the reads its plan +// names and takes the ids from the plan, so a claim on this function with supplied values is a claim +// on what the collector reads. +type CollectRead + = ReadFloorJobLog { job_id: Int } + | ReadRunArtifacts { run_id: Int } + +type CollectReadPlan + = CollectReadsRefused { token_app: DeclaredGitHubApp, token_installation: GitHubAppInstallationId } + | CollectReadsPlanned { job_id: Int, run_id: Int } + +fn collect_read_plan( + subject: QualificationDispatchSubject, + token_app: DeclaredGitHubApp, + token_installation: GitHubAppInstallationId, + floor_job_id: Int, + run_id: Int, +) -> CollectReadPlan { + if token_names_registration(token_app: token_app, token_installation: token_installation, subject: subject) { + CollectReadsPlanned { job_id: floor_job_id, run_id: run_id } + } else { + CollectReadsRefused { token_app: token_app, token_installation: token_installation } + } +} + +fn collect_read_plan_reads(plan: CollectReadPlan) -> List { + match plan { + CollectReadsRefused { token_app: _, token_installation: _ } => [] + CollectReadsPlanned { job_id: j, run_id: r } => [ReadFloorJobLog { job_id: j }, ReadRunArtifacts { run_id: r }] + } +} + +fn collect_qualification_instruments(collected: CollectedQualificationRun, token: ControllerInstallationToken) -> QualificationCollectOutcome uses net: Network { + match collect_read_plan( + subject: collected.dispatched.subject, + token_app: token.app, + token_installation: token.installation, + floor_job_id: collected.floor_job.id, + run_id: collected.dispatched.receipt.workflow_run_id, + ) { + CollectReadsRefused { token_app: a, token_installation: i } => QualificationCollectUnderAnotherInstallation { token_app: a, token_installation: i } + CollectReadsPlanned { job_id: _, run_id: _ } => collect_qualification_instruments_under(collected: collected, token: token) + } +} + +// THE READS, CONFINED TO THE CHECKED ENTRY. Only collect_qualification_instruments may call this, and +// only after its read plan admitted the token; the job id and run id are the sealed collection's own, +// never arguments, so no caller can pair a collection with another run's id or read under a token the +// plan did not admit. +fn collect_qualification_instruments_under(collected: CollectedQualificationRun, token: ControllerInstallationToken) -> QualificationCollectOutcome + uses net: Network + admit_callers: [ + decl_ref(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "collect_qualification_instruments"), + ] +{ + let job_id = collected.floor_job.id + let run_id = collected.dispatched.receipt.workflow_run_id + let owner = gunbc_repository.owner as NonEmptyStr + let repo = gunbc_repository.name as NonEmptyStr + match collected.dispatched.subject.registration.slot { + MicroVmJitSlot { attempt: _ } => QualificationCollectSlotNotAHostUnit + HostUnitJitSlot { slot: slot } => { + let log = attempt_job_log_of(read: read_job_log_with(token: token, owner: owner, repo: repo, job_id: job_id)) + let claim_cost = read_claim_cost_artifact(token: token, owner: owner, repo: repo, run_id: run_id) + QualificationCollected { stage: QualificationCollectStage { job_log: job_log_standing(collected: collected, slot: slot, log: log), claim_cost: claim_cost } } + } + } +} + +// ── THE INSTRUMENTS THIS RUN'S LOG DOES NOT CARRY, EACH WITH THE CAPABILITY THAT WOULD READ IT ── +// +// The extraction above reads every instrument qualification_instrument_source places on the job +// log. The remaining four are three facts, so three rows: one per missing capability, so that each +// row is retired by its own trigger and by nothing else. +data qualification_instrument_extraction_frontier_rows: List = [ + frontier_row_decl( + ref: decl_ref(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "collect_qualification_instruments"), + reason: "FloorPhaseRows and FloorCgroupRows have an implemented extraction authority and no production consumer. collect_qualification_instruments reads the designated floor job's log and mints the sealed QualificationJobLogReceipt, but nothing on the route calls it: the collect stage's standing is gunbc.runner_throughput_qualification_route mtcollins1_collect_leg, LegAuthorityImplemented, and only witnesses reach the decoder. Its input is the CollectedQualificationRun the dispatch leg's collect_qualification_run returns, whose floor job is already joined to the minted runner", + dissolution: unbound_dissolution(description: "the qualification route's collect stage invokes collect_qualification_instruments with the CollectedQualificationRun collect_qualification_run returned and the controller token, on an executed route, so mtcollins1_collect_leg is LegWired and FloorPhaseRows and FloorCgroupRows are read from a real run's designated job. NOT satisfied by a witness calling the decoder or the subject join, nor by the collector compiling"), + ), + frontier_row_decl( + ref: decl_ref(module_path: "gunbc.floor_cost_distribution", decl_name: "parse_claim_cost_tsv"), + reason: "ClaimCostArtifactEvalSteps and CalibrationSpecimenWitnessLine are both read from the required-floor-claim-cost TSV (gunbc.floor_cost_distribution parse_claim_cost_tsv; the calibration specimen's row is joined there by calibration_specimen_grounding). Neither is on the job log: on the recorded required-floor log of run 35048059968 / job 104642384772 (test.fixture recorded_required_floor_log_excerpt) there are zero [witness] lines and zero occurrences of the specimen identity, and eval_steps appear only on the [over-cost] preview, a 25-row truncated view that is not the instrument. The required floor job uploads the artifact (gunbc.witness_floor_workflow required_floor_claim_cost_upload_bound_step, bound by gunbc.compiler_gate_workflow), and read_claim_cost_artifact lists it under the registration's installation token, refuses zero or several same-name artifacts, binds the listing to the collected attempt by re-reading the run after it (ClaimCostRunAdvancedPastAttempt), and downloads the one artifact. What does not exist is the reading after the download: an uploaded artifact is always a zip, the REST handler reads every body as UTF-8 text (extdeps.transports.rest RestBodyObservation body: String), so DownloadArtifact answers RestBodyUndecodable today and a body that did arrive is ClaimCostArchiveNotInflatable", + dissolution: unbound_dissolution(description: "the REST transport carries a binary response body, AND an inflate reader takes the exact required_floor_claim_cost.tsv member out of one upload-artifact zip, AND that member is parsed by parse_claim_cost_tsv into a reading bound to this collected run -- the artifact downloaded is the one listed for the sealed run id at the collected attempt, carried with its artifact id beside the parsed rows in the sealed receipt -- SUFFICIENT FOR collect_qualification_instruments to read ClaimCostArtifactEvalSteps and CalibrationSpecimenWitnessLine from the same run as the job log, and for qualification_instrument_source to place both on that read. NOT satisfied by the binary transport or the inflate reader alone, by reading any other member, by the [over-cost] preview or any other truncated view, by a new print of eval_steps into the log, or by an artifact downloaded outside this route"), + ), + frontier_row_decl( + ref: decl_ref(module_path: "gunbc.runner_throughput_qualification_route", decl_name: "mtcollins1_boot_leg"), + reason: "GuestIdleMeminfoAndNproc is not a run output: the guest's idle MemTotal, MemAvailable (extdeps.linux.proc_meminfo), nproc and uname -m are read before the job starts, by the boot leg's runner-host-up readback, and that leg is gunbc.runner_throughput_qualification_route mtcollins1_boot_leg, still LegAwaitingAuthority", + dissolution: unbound_dissolution(description: "the boot leg's terminal is the runner host observed up and its readback carries the guest's idle meminfo, nproc and machine word, SUFFICIENT FOR this route to hand that readback to the qualification receipt beside this run's extraction. NOT satisfied by a meminfo read inside the floor job, which is a loaded guest rather than an idle one"), + ), + frontier_row_decl( + ref: decl_ref(module_path: "product.capacity.cohort_observation", decl_name: "seal_cohort"), + reason: "ConcurrentCohortSeatWindows is sealed by product.capacity.cohort_observation seal_cohort over a roster of seats released at one barrier, each with ready, start and end instants and a settlement. This route registers ONE ephemeral slot and dispatches one floor, so there is no cohort and no barrier to read; one job's started_at and completed_at are not a seat window", + dissolution: unbound_dissolution(description: "a qualification route that registers a roster of concurrent seats on the host, releases them at a barrier, and reads each seat's ready, start and end back, SUFFICIENT FOR seal_cohort to seal that reading for this host. NOT satisfied by a cohort of one, nor by job timestamps standing in for seat readiness"), + ), +] 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 e52fb479519..80d70610fae 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. @@ -45,13 +46,13 @@ import gunbc.runner_throughput_qualification { type StageEffect = BmcWrite { gate: DeclarationRef, boot: RouteLegStanding, image: RouteLegStanding } | GitHubControlPlaneWrite { authority: RouteLegStanding } - | ObservationOnly + | ObservationOnly { collection: RouteLegStanding } type QualificationStage = BootHostUnderApprovalGate { host: HostIdentity, boot: RouteLegStanding, image: RouteLegStanding } | RegisterEphemeralRunnerSlot { unit: NonEmptyStr, labels: List, workspace: WorkspaceBacking, registration: RouteLegStanding } | DispatchFloorToSlot { workload: FloorWorkloadPin, selector: List, dispatch: RouteLegStanding } - | CollectInstruments { instruments: List } + | CollectInstruments { instruments: List, collection: RouteLegStanding } | DeregisterRunnerSlot { unit: NonEmptyStr, deregistration: RouteLegStanding } fn stage_effect(stage: QualificationStage) -> StageEffect { @@ -64,7 +65,7 @@ fn stage_effect(stage: QualificationStage) -> StageEffect { } RegisterEphemeralRunnerSlot { unit: _, labels: _, workspace: _, registration: r } => GitHubControlPlaneWrite { authority: r } DispatchFloorToSlot { workload: _, selector: _, dispatch: d } => GitHubControlPlaneWrite { authority: d } - CollectInstruments { instruments: _ } => ObservationOnly + CollectInstruments { instruments: _, collection: c } => ObservationOnly { collection: c } DeregisterRunnerSlot { unit: _, deregistration: d } => GitHubControlPlaneWrite { authority: d } } } @@ -80,7 +81,7 @@ fn stage_egress(stage: QualificationStage) -> EgressPolicyShape? { BootHostUnderApprovalGate { host: _, boot: _, image: _ } => none RegisterEphemeralRunnerSlot { unit: _, labels: _, workspace: _, registration: _ } => Present { value: runner_host_egress_policy } DispatchFloorToSlot { workload: _, selector: _, dispatch: _ } => Present { value: runner_host_egress_policy } - CollectInstruments { instruments: _ } => none + CollectInstruments { instruments: _, collection: _ } => none DeregisterRunnerSlot { unit: _, deregistration: _ } => Present { value: runner_host_egress_policy } } } @@ -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 { @@ -245,6 +247,13 @@ data mtcollins1_deregistration_leg: RouteLegStanding = LegAuthorityImplemented { wiring_owed: "the same route fold calling ensure_jit_runner_deregistered on every slot exit with the registration jit_registration_of minted from the registration leg's dispatch, joined to a host-unit gunbc.runner.runner_teardown_receipt RunnerTeardownResult; SUFFICIENT FOR the route reporting a slot retired only when the runner is absent from the organization listing and the unit's resources are observed gone" as NonEmptyStr, } +// THE COLLECT STAGE'S STANDING. The authority reads the designated floor job's log and the +// claim-cost artifact into a sealed receipt; nothing on the route invokes it yet. +data mtcollins1_collect_leg: RouteLegStanding = LegAuthorityImplemented { + authority: decl_ref(module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "collect_qualification_instruments"), + wiring_owed: "the same route fold calling collect_qualification_instruments with the DispatchedQualificationRun the dispatch leg returned, the collection collect_qualification_run read back, and the JitRegistration the registration leg minted; SUFFICIENT FOR FloorPhaseRows and FloorCgroupRows being read on every executed attempt from the one job its registered runner ran, as a sealed QualificationJobLogReceipt or a typed refusal (gunbc.runner.runner_qualification_dispatch qualification_instrument_extraction_frontier_rows)" as NonEmptyStr, +} + // THE FLEET-CONVERGE MODE THIS ROUTE BECOMES IS NOT NAMED HERE. A mode row belongs to // `gunbc.fleet_converge_workflow` and lands there with the boot leg (section 3c: a declared frontier // with its trigger beside it); a mode whose boot leg has no authority on main would dispatch nothing @@ -257,6 +266,7 @@ type QualificationRouteLegs { image: RouteLegStanding registration: RouteLegStanding dispatch: RouteLegStanding + collect: RouteLegStanding deregistration: RouteLegStanding } @@ -265,6 +275,7 @@ data mtcollins1_route_legs: QualificationRouteLegs = QualificationRouteLegs { image: mtcollins1_image_leg, registration: mtcollins1_registration_leg, dispatch: mtcollins1_dispatch_leg, + collect: mtcollins1_collect_leg, deregistration: mtcollins1_deregistration_leg, } @@ -281,7 +292,7 @@ fn qualification_route( BootHostUnderApprovalGate { host: host, boot: legs.boot, image: legs.image }, RegisterEphemeralRunnerSlot { unit: unit, labels: labels, workspace: workspace, registration: legs.registration }, DispatchFloorToSlot { workload: workload, selector: labels, dispatch: legs.dispatch }, - CollectInstruments { instruments: qualification_instruments }, + CollectInstruments { instruments: qualification_instruments, collection: legs.collect }, DeregisterRunnerSlot { unit: unit, deregistration: legs.deregistration }, ] } @@ -300,17 +311,19 @@ fn mtcollins1_qualification_route(attempt: NonEmptyStr, workload: FloorWorkloadP fn stage_is_effectful(stage: QualificationStage) -> Bool { match stage_effect(stage: stage) { - ObservationOnly => false + ObservationOnly { collection: _ } => false BmcWrite { gate: _, boot: _, image: _ } => true GitHubControlPlaneWrite { authority: _ } => true } } -// THE LEGS AN EFFECTFUL STAGE STANDS ON. A BMC write stands on its boot and image legs; a -// control-plane write on its authority; observation on nothing. +// THE LEGS A STAGE STANDS ON. A BMC write stands on its boot and image legs; a control-plane write +// on its authority; the collect stage on its collection standing. Observation is not exempt: a +// route whose effectful legs were all wired while nothing invoked the collector would execute and +// read nothing, so the collect stage's standing counts toward route_is_executable like any leg. fn stage_legs(stage: QualificationStage) -> List { match stage_effect(stage: stage) { - ObservationOnly => [] + ObservationOnly { collection: c } => [c] BmcWrite { gate: _, boot: b, image: i } => [b, i] GitHubControlPlaneWrite { authority: a } => [a] } diff --git a/dag/test/claim/authorization_pattern_selection_witness_test.dag b/dag/test/claim/authorization_pattern_selection_witness_test.dag index 6697a259935..3da3815d443 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, 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,76 @@ 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" + && (runner_lifecycle_operator_ruling.interlock.decl_name as String) == "UnitHoldProof" + && (runner_lifecycle_operator_ruling.interlock.module_path as String) == "gunbc.managed_host_unit_hold" + && 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 6ce5a604869..030ef1b552e 100644 --- a/dag/test/claim/github_app_registry_witness_test.dag +++ b/dag/test/claim/github_app_registry_witness_test.dag @@ -1306,17 +1306,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 45efa581a32..b7488718758 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/qualification_job_log_receipt_forged_probe_witness_test.dag b/dag/test/claim/runner/qualification_job_log_receipt_forged_probe_witness_test.dag new file mode 100644 index 00000000000..f61a111ca19 --- /dev/null +++ b/dag/test/claim/runner/qualification_job_log_receipt_forged_probe_witness_test.dag @@ -0,0 +1,67 @@ +module test.claim.qualification_job_log_receipt_forged_probe_witness + +import std.types { String, Bool, Int, List } +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 FORGED JOB-LOG RECEIPT ROUTES, ENROLLED AS EXECUTED REDS (DESIGN 4b: a state unrepresentable +// in the accepted corpus is still representable as source handed to the compiler, and the refusal +// is the enrollable evidence). test.probe.qualification_job_log_receipt_forged_probe writes the +// sealed receipt from invented readings and calls its one minter from outside the collect stage; +// each must refuse at its own subject. Counts are scoped to class AND subject, and a control source +// that only NAMES the module and calls its open decoder must refuse at neither, so the refusals are +// attributable to the forgeries rather than to importing the module at all. The pattern is +// test.claim.jit_deregistration_forged_probe_witness's. + +fn census_of(source: String) -> CompileDiagnosticCensus { + compile_dag_diagnostic_census(source) +} + +fn probe() -> CompileDiagnosticCensus { + census_of(source: filesystem_read(path: "dag/test/probe/qualification_job_log_receipt_forged_probe.dag").content) +} + +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_receipt_harness_control\nimport std.types { String }\nimport gunbc.runner.runner_qualification_dispatch { JobLogInstrumentDecode, decode_job_log_instruments }\nfn decoded(t: String) -> JobLogInstrumentDecode { decode_job_log_instruments(log: t, slot_unit: \"x.service\") }\n" + +test fn a_source_that_only_names_the_module_forges_nothing() -> Bool { + let c = census_of(source: control_source) + blocking(c: c, wanted: "SoleConstructorViolation", subject: "QualificationJobLogReceipt") == 0 + && blocking(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "job_log_standing") == 0 + && blocking(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "collect_qualification_instruments_under") == 0 + && blocking(c: c, wanted: "ConstructorCallAdmissionRefused", subject: "read_claim_cost_artifact") == 0 +} + +test fn a_forged_job_log_receipt_refuses_at_its_own_name() -> Bool { + blocking(c: probe(), wanted: "SoleConstructorViolation", subject: "QualificationJobLogReceipt") >= 1 +} + +test fn the_receipt_minter_refuses_a_caller_other_than_the_collect_stage() -> Bool { + blocking(c: probe(), wanted: "ConstructorCallAdmissionRefused", subject: "job_log_standing") >= 1 +} + +// THE COLLECTOR'S READS ARE REACHABLE ONLY THROUGH ITS READ PLAN. collect_qualification_instruments_under +// takes no job or run id -- they are the sealed collection's -- and admits only the checked entry, so a +// caller holding a genuine collection cannot read it under another installation's token. +test fn the_reads_refuse_a_caller_other_than_the_checked_entry() -> Bool { + blocking(c: probe(), wanted: "ConstructorCallAdmissionRefused", subject: "collect_qualification_instruments_under") >= 1 +} + +// AND THE CLAIM-COST READ CANNOT BE AIMED AT ANOTHER RUN: it admits only the confined reads above. +test fn the_claim_cost_read_refuses_a_free_token_and_run_id() -> Bool { + blocking(c: probe(), wanted: "ConstructorCallAdmissionRefused", subject: "read_claim_cost_artifact") >= 1 +} 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 2b513f6758f..70e0de0b543 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 6d7fc92e04b..652d426ff89 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.types { String, NonEmptyStr, Bool, Int, List } import std.nat { Nat } @@ -293,8 +299,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..517532787b0 --- /dev/null +++ b/dag/test/claim/runner/runner_qualification_dispatch_witness_test.dag @@ -0,0 +1,892 @@ +module test.claim.runner_qualification_dispatch_witness + +import std.types { Bool, Bytes, CommitSha, Int, List, NonEmptyStr, String } +import std.bytes { utf8_encode_bytes } +import std.algebra { Cons, Empty } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import product.placement_supply { HostIdentity } +import extdeps.transports.rest { + RestResult, RestAnswered, RestRefused, RestRefusal, RestTransportRefused, RestStatusRefused, RestBodyUndecodable, + RestExchangeStatusRefused, RestExchangeUnreached, RestExchangeUndecodable, +} +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, qualification_instruments, FloorPhaseRows, FloorCgroupRows } +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_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, 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, + AttemptJobLog, AttemptJobLogRead, AttemptJobLogUnreadable, + DesignatedJobLog, DesignatedJobLogText, DesignatedJobLogRefused, designated_job_log, + JobLogReadRefusal, JobLogOfAnotherJob, JobLogUnreadable, JobLogEmpty, + JobLogInstrumentDecode, JobLogInstrumentsDecoded, JobLogInstrumentsUndecodable, decode_job_log_instruments, + QualificationLogReadings, InstrumentReadRefusal, FloorPhaseRowGarbledInLog, FloorCgroupRowGarbledInLog, + FloorPhaseRowsAbsent, SlotCgroupLevelAbsent, + qualification_instrument_read_from_job_log, qualification_instrument_extraction_frontier_rows, + ClaimCostArtifactRead, ClaimCostArtifactAbsent, ClaimCostArtifactExpired, ClaimCostArtifactListTruncated, + ClaimCostArchiveUnreadable, ClaimCostArchiveNotInflatable, + conclude_claim_cost_listing, conclude_claim_cost_download, conclude_claim_cost_attempt, + collect_read_plan, collect_read_plan_reads, CollectReadsRefused, CollectReadsPlanned, + ClaimCostArtifactAmbiguous, ClaimCostRunAdvancedPastAttempt, ClaimCostRunUnreadable, +} +import gunbc.required_ci_phase_roster { FloorPhaseTimed, FloorPhaseUntimed } +import extdeps.linux.cgroup_v2_memory { CgroupMemoryLimited } +import std.measure { byte_size_count, millisecond_count } +import extdeps.github.actions_artifacts { ActionsArtifact, ActionsArtifactList } +import test.fixture.recorded_required_floor_log_excerpt { + recorded_required_floor_log_excerpt, recorded_floor_log_slot_unit, +} + +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(collect_read_plan_reads(plan: collect_read_plan(subject: s, token_app: gunbai_ci_declared, token_installation: s.registration.installation, floor_job_id: 501, run_id: 77))) == 0 + && count(collect_read_plan_reads(plan: collect_read_plan(subject: s, token_app: s.registration.app, token_installation: other_installation_id, floor_job_id: 501, run_id: 77))) == 0 + && (match collect_read_plan(subject: s, token_app: gunbai_ci_declared, token_installation: s.registration.installation, floor_job_id: 501, run_id: 77) { + CollectReadsRefused { token_app: _, token_installation: _ } => true + CollectReadsPlanned { job_id: _, run_id: _ } => false + }) + && (match collect_read_plan(subject: s, token_app: s.registration.app, token_installation: s.registration.installation, floor_job_id: 501, run_id: 77) { + CollectReadsPlanned { job_id: 501, run_id: 77 } => true + _ => false + }) + && 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 + }) +} + +// ── THE DESIGNATED JOB'S LOG ────────────────────────────────────────────────────────────────── + +// RED: a log read for any job other than the designated one is refused, whatever it says. +test fn a_log_of_another_job_is_not_the_floor_jobs_log() -> Bool { + (match designated_job_log(designated_job_id: 502, log: AttemptJobLogRead { job_id: 501, log: "[floor-phase] phase=x wall_ms=1" }) { + DesignatedJobLogRefused { refusal: JobLogOfAnotherJob { designated_job_id: 502, read_job_id: 501 } } => true + _ => false + }) + && (match designated_job_log(designated_job_id: 502, log: AttemptJobLogUnreadable { job_id: 502, refusal: RestExchangeStatusRefused { status: 410, body: "Gone" } }) { + DesignatedJobLogRefused { refusal: JobLogUnreadable { job_id: 502, refusal: _ } } => true + _ => false + }) + && (match designated_job_log(designated_job_id: 502, log: AttemptJobLogRead { job_id: 502, log: "" }) { + DesignatedJobLogRefused { refusal: JobLogEmpty { job_id: 502 } } => true + _ => false + }) +} + +// ── THE PURE DECODER, OVER SUPPLIED TEXT ────────────────────────────────────────────────────── + +data slot: NonEmptyStr = "gunbc-qualification-mtcollins1-q-20261004-1.service" + +data phase_line: String = "2026-10-04T00:10:00.0000000Z [floor-phase] phase=gate-closure state=completed wall_ms=22194 prefixes=0" +data started_line: String = "2026-10-04T00:09:00.0000000Z [floor-phase] phase=strict-preparation state=started" +data slot_level_line: String = "2026-10-04T00:09:00.0000000Z [floor-cgroup] when=floor-entry level=/sys/fs/cgroup/system.slice/gunbc-qualification-mtcollins1-q-20261004-1.service max=17179869184 high=16106127360 current=8949473280 peak=10444185600 events=[low,0]" +data slice_level_line: String = "2026-10-04T00:09:00.0000000Z [floor-cgroup] when=floor-entry level=/sys/fs/cgroup/system.slice max=max high=max current=1 peak=364675248128" + +fn decode(lines: List) -> JobLogInstrumentDecode { + decode_job_log_instruments(log: join(lines, "\n"), slot_unit: slot) +} + +fn undecodable_with(d: JobLogInstrumentDecode, check: fn(InstrumentReadRefusal) -> Bool) -> Bool { + match d { + JobLogInstrumentsUndecodable { refusal: r } => check(r) + JobLogInstrumentsDecoded { readings: _ } => false + } +} + +test fn the_job_log_instruments_are_the_two_the_extraction_reads() -> Bool { + qualification_instrument_read_from_job_log(i: FloorPhaseRows) + && qualification_instrument_read_from_job_log(i: FloorCgroupRows) + && count(qualification_instruments |> filter(i => qualification_instrument_read_from_job_log(i: i))) == 2 + && count(qualification_instrument_extraction_frontier_rows) == 4 +} + +// THE POSITIVE CONTROL: timed and untimed phase rows are both carried, and only the slot's own +// level is taken -- the slice above it has a larger peak and must not be read as the slot's. +test fn a_log_with_phase_rows_and_the_slot_level_is_decoded() -> Bool { + match decode(lines: ["noise before the floor", started_line, slot_level_line, slice_level_line, phase_line]) { + JobLogInstrumentsDecoded { readings: rd } => + count(rd.floor_phase_rows) == 2 + && count(rd.slot_cgroup_rows) == 1 + && (rd.slot_cgroup_rows |> all(l => byte_size_count(b: l.peak) == 10444185600)) + && (rd.floor_phase_rows |> any(p => match p { FloorPhaseTimed { phase: _, wall: w } => millisecond_count(m: w) == 22194 _ => false })) + JobLogInstrumentsUndecodable { refusal: _ } => false + } +} + +test fn a_garbled_row_refuses_rather_than_being_skipped() -> Bool { + undecodable_with(d: decode(lines: [slot_level_line, phase_line, "[floor-phase] phase=gate-closure wall_ms=twelve"]), check: r => match r { + FloorPhaseRowGarbledInLog { line: _, cause: _ } => true + _ => false + }) + && undecodable_with(d: decode(lines: [phase_line, "[floor-cgroup] when=beat-10 level=/sys/fs/cgroup/x.service high=lots peak=1"]), check: r => match r { + FloorCgroupRowGarbledInLog { line: _, cause: _ } => true + _ => false + }) +} + +// RED, THE SPLIT-ACROSS-JOBS CASE: the phase rows of one job and the slot row of another never meet, +// because only the designated job's log is decoded -- read alone, the job carrying only phase rows +// refuses for want of the slot level, and the one carrying only the slot level refuses for want of a +// timed phase row. +test fn rows_split_across_two_jobs_are_not_one_measurement() -> Bool { + undecodable_with(d: decode(lines: [started_line, phase_line]), check: r => match r { + SlotCgroupLevelAbsent { slot_unit: u, levels_seen: seen } => u == slot && count(seen) == 0 + _ => false + }) + && undecodable_with(d: decode(lines: [slot_level_line, slice_level_line]), check: r => match r { + FloorPhaseRowsAbsent => true + _ => false + }) +} + +test fn a_log_without_the_slot_level_names_the_levels_it_saw() -> Bool { + undecodable_with(d: decode(lines: [phase_line, slice_level_line]), check: r => match r { + SlotCgroupLevelAbsent { slot_unit: u, levels_seen: seen } => u == slot && count(seen) == 1 + _ => false + }) +} + +// ── INHABITANCE: THE REAL PRODUCER'S BYTES ───────────────────────────────────────────────────── +// +// The supplied lines above are designed against the row shapes; this claim is what keeps them +// readings. It hands decode_job_log_instruments the verbatim [floor-phase] and [floor-cgroup] lines +// claim_executor printed on a recorded required-floor run (test.fixture +// recorded_required_floor_log_excerpt), under that run's real slot unit, and asserts the ROUTE as well +// as the answer: every one of the 79 phase rows is read (none garbled, none dropped), the timed rows +// carry the gate-closure wall the log printed, and of the 12 level rows only the 4 at the slot's own +// level -- floor entry and three heartbeats -- are taken, with the slot's memory.high read as a byte +// bound and floor entry's memory.peak as printed. If the host's row encoding moves, this goes red +// while the designed fixtures above stay green. +test fn the_decoder_reads_a_recorded_required_floor_log() -> Bool { + match decode_job_log_instruments(log: recorded_required_floor_log_excerpt, slot_unit: recorded_floor_log_slot_unit as NonEmptyStr) { + JobLogInstrumentsDecoded { readings: rd } => + count(rd.floor_phase_rows) == 79 + && (rd.floor_phase_rows |> any(p => match p { FloorPhaseTimed { phase: ph, wall: w } => (ph as String) == "gate-closure" && millisecond_count(m: w) == 22194 _ => false })) + && (rd.floor_phase_rows |> any(p => match p { FloorPhaseUntimed { phase: ph } => (ph as String) == "strict-preparation" _ => false })) + && count(rd.slot_cgroup_rows) == 4 + && (rd.slot_cgroup_rows |> all(l => match l.high { CgroupMemoryLimited { bytes: b } => byte_size_count(b: b) == 16106127360 _ => false })) + && (rd.slot_cgroup_rows |> any(l => (l.when as String) == "floor-entry" && byte_size_count(b: l.peak) == 10444185600)) + JobLogInstrumentsUndecodable { refusal: _ } => false + } +} + +// SUPPLIED RestResult VALUES FOR THE CLAIM-COST DECISIONS, built once so the claims below stay readable. +fn answered_listing(l: ActionsArtifactList) -> RestResult { + RestAnswered { answer: l } +} + +fn answered_run(r: WorkflowRun) -> RestResult { + RestAnswered { answer: r } +} + +data unreached_run: RestResult = RestRefused { refusal: RestTransportRefused { cause: "unreached" } } + +fn archive_refused(r: RestRefusal) -> RestResult { + RestRefused { refusal: r } +} + +data archive_arrived: RestResult = RestAnswered { answer: utf8_encode_bytes(s: "PK") } + +// ── THE CLAIM-COST READ'S REFUSALS ───────────────────────────────────────────────────────────── +// +// Every way the artifact read can end today is a typed arm, and none of them is a reading: the +// listing truncated, the artifact absent (with the names that were there), expired, the archive +// unreadable (the RestBodyUndecodable a zip body produces), or an archive that arrived with no +// inflate reader to open it. +fn artifact(name: String, expired: Bool) -> ActionsArtifact { + ActionsArtifact { id: 9001, name: name, expired: expired } +} + +test fn every_claim_cost_read_ends_in_a_typed_refusal() -> Bool { + let present = ActionsArtifactList { total_count: 1, artifacts: [artifact(name: "required-floor-claim-cost", expired: false)] } + let gone = archive_refused(r: RestStatusRefused { status: 410, body: "Gone" }) + let undecodable = archive_refused(r: RestBodyUndecodable { status: 200, cause: "stream did not contain valid UTF-8" }) + (match conclude_claim_cost_listing(listed: answered_listing(l: ActionsArtifactList { total_count: 1, artifacts: [artifact(name: "required-ci-measurement-receipt", expired: false)] })) { + Present { value: ClaimCostArtifactAbsent { names_seen: ns } } => count(ns) == 1 + _ => false + }) + && (match conclude_claim_cost_listing(listed: answered_listing(l: ActionsArtifactList { total_count: 1, artifacts: [artifact(name: "required-floor-claim-cost", expired: true)] })) { + Present { value: ClaimCostArtifactExpired { artifact_id: 9001 } } => true + _ => false + }) + && (match conclude_claim_cost_listing(listed: answered_listing(l: ActionsArtifactList { total_count: 3, artifacts: [] })) { + Present { value: ClaimCostArtifactListTruncated { returned: 0, total: 3 } } => true + _ => false + }) + && (match conclude_claim_cost_listing(listed: answered_listing(l: present)) { Absent => true _ => false }) + && (match conclude_claim_cost_download(artifact_id: 9001, archive: undecodable) { + ClaimCostArchiveUnreadable { artifact_id: 9001, refusal: _ } => true + _ => false + }) + && (match conclude_claim_cost_download(artifact_id: 9001, archive: gone) { + ClaimCostArtifactExpired { artifact_id: 9001 } => true + _ => false + }) + && (match conclude_claim_cost_download(artifact_id: 9001, archive: archive_arrived) { + ClaimCostArchiveNotInflatable { artifact_id: 9001 } => true + _ => false + }) +} + +// TWO SAME-NAME ARTIFACTS ARE A REFUSAL, NEVER FIRST-ONE-WINS. +fn claim_cost_artifact_with(id: Int) -> ActionsArtifact { + ActionsArtifact { id: id, name: "required-floor-claim-cost", expired: false } +} + +test fn two_same_name_claim_cost_artifacts_refuse_as_ambiguous() -> Bool { + match conclude_claim_cost_listing(listed: answered_listing(l: ActionsArtifactList { total_count: 2, artifacts: [claim_cost_artifact_with(id: 1), claim_cost_artifact_with(id: 2)] })) { + Present { value: ClaimCostArtifactAmbiguous { artifact_ids: ids } } => count(ids) == 2 + _ => false + } +} + +// THE LISTING IS BOUND TO THE COLLECTED ATTEMPT: a run re-read after the listing at attempt 2 means the +// listing may hold attempt 2's artifact, so no claim-cost read proceeds for attempt 1; at attempt 1 it +// proceeds; an unreadable re-read refuses rather than assuming attempt 1. +test fn a_rerun_seen_after_the_listing_refuses_the_claim_cost_read() -> Bool { + (match conclude_claim_cost_attempt(run: answered_run(r: dispatched_run(attempt_n: 2))) { + Present { value: ClaimCostRunAdvancedPastAttempt { observed_attempt: 2 } } => true + _ => false + }) + && (match conclude_claim_cost_attempt(run: answered_run(r: dispatched_run(attempt_n: 1))) { Absent => true _ => false }) + && (match conclude_claim_cost_attempt(run: unreached_run) { + Present { value: ClaimCostRunUnreadable { refusal: _ } } => true + _ => 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 9465908b8aa..6d0e379bcc6 100644 --- a/dag/test/claim/runner/runner_throughput_qualification_witness_test.dag +++ b/dag/test/claim/runner/runner_throughput_qualification_witness_test.dag @@ -739,16 +739,16 @@ test fn the_route_classifies_every_mutation_at_its_grain() -> Bool { match stage_effect(stage: s) { GitHubControlPlaneWrite { authority: _ } => true _ => false } DeregisterRunnerSlot { unit: _, deregistration: _ } => match stage_effect(stage: s) { GitHubControlPlaneWrite { authority: _ } => true _ => false } - CollectInstruments { instruments: _ } => - match stage_effect(stage: s) { ObservationOnly => true _ => false } + CollectInstruments { instruments: _, collection: _ } => + match stage_effect(stage: s) { ObservationOnly { collection: _ } => true _ => false } BootHostUnderApprovalGate { host: _, boot: _, image: _ } => match stage_effect(stage: s) { BmcWrite { gate: _, boot: _, image: _ } => true _ => false } } )) } -// 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) } @@ -763,9 +763,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 @@ -773,13 +773,16 @@ 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) && !leg_is_wired(leg: mtcollins1_route_legs.boot) && !leg_is_wired(leg: mtcollins1_route_legs.dispatch) + && leg_names(leg: mtcollins1_route_legs.collect, module_path: "gunbc.runner.runner_qualification_dispatch", decl_name: "collect_qualification_instruments") + && !leg_is_wired(leg: mtcollins1_route_legs.collect) && !route_is_executable(route: route()) } @@ -795,7 +798,7 @@ test fn only_the_runner_stages_open_the_network_and_only_default_drop() -> Bool Absent => match s { BootHostUnderApprovalGate { host: _, boot: _, image: _ } => true - CollectInstruments { instruments: _ } => true + CollectInstruments { instruments: _, collection: _ } => true _ => false } Present { value: policy } => @@ -817,7 +820,7 @@ test fn the_collect_stage_owes_a_sealed_concurrent_cohort() -> Bool { !leg_is_wired(leg: qualification_run_producer_frontier) && (route() |> any(s => match s { - CollectInstruments { instruments: is } => + CollectInstruments { instruments: is, collection: _ } => is |> any(i => match i { ConcurrentCohortSeatWindows => { @@ -835,7 +838,7 @@ test fn the_collect_stage_owes_a_sealed_concurrent_cohort() -> Bool { test fn the_collect_stage_owes_the_rate_specimen_and_the_cgroup_rows() -> Bool { route() |> any(s => match s { - CollectInstruments { instruments: is } => + CollectInstruments { instruments: is, collection: _ } => (is |> any(i => match i { CalibrationSpecimenWitnessLine => { 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/fixture/recorded_required_floor_log_excerpt.dag b/dag/test/fixture/recorded_required_floor_log_excerpt.dag new file mode 100644 index 00000000000..6c738127189 --- /dev/null +++ b/dag/test/fixture/recorded_required_floor_log_excerpt.dag @@ -0,0 +1,22 @@ +module test.fixture.recorded_required_floor_log_excerpt + +import std.types { Int, String } + +// REAL BYTES FROM ONE RECORDED REQUIRED-FLOOR JOB LOG, NOT A DESIGNED FIXTURE. The source is GitHub +// Actions run 35048059968, job 104642384772 (required-witnesses-floor, conclusion success, runner slot +// actions-runner@srv4-18.service), read through GitHub's "Download job logs for a workflow run" on +// 2026-10-04. The excerpt is every `[floor-phase]` and `[floor-cgroup]` line of that log, verbatim and +// in log order with GitHub's timestamp prefix kept, plus a handful of the log's untagged and +// differently tagged lines (an `[over-cost]` preview row among them) that a reader of the two tags +// must pass over. Nothing is edited inside a line; the .dag string escapes are the only change. +// +// IT IS AN EXCERPT BECAUSE THE WHOLE LOG IS 1.5 MB, and that size is itself a recorded fact the +// extraction relies on: it sits well under the seed REST handler's whole-body read, so the network +// read of a log like this one is not refused for size. +data recorded_floor_log_run_id: Int = 35048059968 + +data recorded_floor_log_job_id: Int = 104642384772 + +data recorded_floor_log_slot_unit: String = "actions-runner@srv4-18.service" + +data recorded_required_floor_log_excerpt: String = "2026-09-16T02:36:29.9676382Z [floor-cgroup] when=floor-entry path=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice/actions-runner@srv4-18.service\n2026-09-16T02:36:29.9692531Z [floor-cgroup] when=floor-entry level=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice/actions-runner@srv4-18.service max=17179869184 high=16106127360 current=8949473280 peak=10444185600 events=[low,0,high,0,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,0,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=0.00,avg60=0.00,avg300=0.00,total=2,full,avg10=0.00,avg60=0.00,avg300=0.00,total=2]\n2026-09-16T02:36:29.9698651Z [floor-cgroup] when=floor-entry level=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice max=max high=max current=196170059776 peak=364675248128 events=[low,0,high,53814358,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,0,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=0.00,avg60=0.00,avg300=0.02,total=13867330781,full,avg10=0.00,avg60=0.00,avg300=0.02,total=13729467014]\n2026-09-16T02:36:29.9703909Z [floor-cgroup] when=floor-entry level=/sys/fs/cgroup/system.slice max=max high=max current=212249088000 peak=380169330688 events=[low,0,high,53814358,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,0,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=0.00,avg60=0.00,avg300=0.02,total=13841256370,full,avg10=0.00,avg60=0.00,avg300=0.02,total=13703013143]\n2026-09-16T02:36:29.9709147Z [floor-phase] phase=strict-preparation state=started\n2026-09-16T02:40:20.9989392Z [floor-phase] phase=gate-closure state=completed wall_ms=22194 prefixes=0 seeds=1 closure=168 bare_pulled=36 outside_closure=5688 corpus=5856\n2026-09-16T02:40:32.0494666Z [floor-phase] phase=expr-var-classification expr_var_occurrences=13930 free_reference_edges=3081 bound_occurrences_suppressed=10836 qualified_chain_heads=13 classification_refusals=0\n2026-09-16T02:40:32.0501531Z [floor-phase] phase=expr-var-classification BoundByParameter=7869 BoundByLet=1153 BoundByMatchPattern=1814 DeclaredInThisModule=1964 DeclaredElsewhere=1117 QualifiedChainHead=13\n2026-09-16T02:40:32.0506107Z [floor-phase] phase=reference-closure-index state=completed wall_ms=63 modules=168 names=6680 subject=93ea90191edaf50d\n2026-09-16T02:40:32.7858463Z [floor-phase] phase=touched-entry-compile-subject seeds=5 modules=[\"extdeps.tmux\", \"gunbc.roadmap_dashboard_instance\", \"gunbc.roadmap_dashboard_instance_apply\", \"test.claim.roadmap_dashboard_instance_apply_witness\", \"test.claim.tmux_session_list_outcome_witness\"]\n2026-09-16T02:40:32.7866444Z [floor-phase] phase=arm-set-changed-consumers state=completed changed_declarations=0 consumers_added=0 flat_channel_consumers=0 outside_floor_roots=0 base=db2257679fb454fcf80ddb4b901d422e8afa5d51 head=84085164947f2c2116ecd8060368c2cf35d22c8c\n2026-09-16T02:41:38.2496524Z [floor-phase] phase=gate-closure state=completed wall_ms=65296 prefixes=32 seeds=1027 closure=3021 bare_pulled=71 outside_closure=2835 corpus=5856\n2026-09-16T02:46:29.9985719Z [floor-cgroup] when=beat-10 path=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice/actions-runner@srv4-18.service\n2026-09-16T02:46:29.9992653Z [floor-cgroup] when=beat-10 level=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice/actions-runner@srv4-18.service max=17179869184 high=16106127360 current=16104755200 peak=16106577920 events=[low,0,high,3848,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,3848,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=5.62,avg60=3.64,avg300=1.66,total=8053481,full,avg10=5.62,avg60=3.64,avg300=1.66,total=8053205]\n2026-09-16T02:46:30.0042734Z [floor-cgroup] when=beat-10 level=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice max=max high=max current=227828391936 peak=364675248128 events=[low,0,high,53837371,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,0,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=1.16,avg60=1.36,avg300=0.72,total=13872120203,full,avg10=1.16,avg60=1.36,avg300=0.72,total=13734253335]\n2026-09-16T02:46:30.0074968Z [floor-cgroup] when=beat-10 level=/sys/fs/cgroup/system.slice max=max high=max current=243909996544 peak=380169330688 events=[low,0,high,53837371,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,0,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=1.15,avg60=1.39,avg300=0.72,total=13846043407,full,avg10=1.15,avg60=1.39,avg300=0.72,total=13707796653]\n2026-09-16T02:48:21.6671401Z [floor-phase] phase=module-path-index-warm state=completed cpu_ms=0 wall_ms=0 rss_growth_bytes=8192 modules=5856 provenance=built-by-preparation\n2026-09-16T02:48:21.6828893Z [floor-phase] phase=shared-index-warm state=completed cpu_ms=0 wall_ms=0 rss_growth_bytes=61440 modules=5856 provenance=built-by-preparation\n2026-09-16T02:48:22.6822520Z [floor-phase] phase=expr-var-classification expr_var_occurrences=178167 free_reference_edges=47772 bound_occurrences_suppressed=129176 qualified_chain_heads=1210 classification_refusals=0\n2026-09-16T02:48:22.6831385Z [floor-phase] phase=expr-var-classification BoundByParameter=84278 BoundByLet=17473 BoundByMatchPattern=27425 DeclaredInThisModule=21920 DeclaredElsewhere=25852 QualifiedChainHead=1210 NamesNothingKnown=9\n2026-09-16T02:48:22.7377365Z [floor-phase] phase=expr-var-classification unclassified=9 distinct=7 specimens=[\"extdeps.cloud.gcp.iam::access_token\", \"extdeps.cloud.gcp.secret_manager::access_token\", \"extdeps.cloudflare.account_api_tokens::auth_token\", \"extdeps.github.pulls::List_PullRequest\", \"extdeps.github.pulls::List_PullReview\", \"extdeps.github.pulls::List_ReviewComment\", \"std.resources::ReadWrite\"]\n2026-09-16T02:48:22.7385985Z [floor-phase] phase=reference-closure-index state=completed wall_ms=926 modules=3019 names=68559 subject=eb8fa8db5887fb3b\n2026-09-16T02:48:24.2494508Z [floor-phase] phase=pool-root-index-warm state=completed cpu_ms=524 wall_ms=777 rss_growth_bytes=7786496 producer=v2.lens.registry.completeness.lens_registry_completeness_live_facts provenance=built-by-preparation\n2026-09-16T02:48:25.1817029Z [floor-phase] phase=languages-consumer-census-warm state=completed cpu_ms=729 wall_ms=785 rss_growth_bytes=0 decl_rows=72 provenance=built-by-preparation\n2026-09-16T02:48:27.8950074Z [floor-phase] phase=prepared-effect-input-acquire state=completed acquisition=gunbc.roadmap_authority.roadmap_acceptance_event_history_load checkout_input=dag/gunbc/roadmap/roadmap_acceptance_event_history.jsonl content_digest=ac7a97b227a758c0 disposition=RoadmapAcceptanceEventHistoryLoaded cpu_ms=13 wall_ms=23 rss_growth_bytes=0\n2026-09-16T02:48:28.1831332Z [floor-phase] phase=prepared-effect-input-warm state=completed producer=gunbc.roadmap_authority.roadmap_authority_projection input=gunbc.roadmap_authority.roadmap_acceptance_event_history_load disposition=Stored cpu_ms=250 wall_ms=287 rss_growth_bytes=1867776\n2026-09-16T02:48:30.3776259Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.native_decl_selection.collision_resolved disposition=Stored cpu_ms=2150 wall_ms=2194 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:30.3818798Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.extdeps.languages.bash_command_fold.bash_fold_formal_productions disposition=Stored cpu_ms=4 wall_ms=4 rss_growth_bytes=20480 provenance=built-by-preparation\n2026-09-16T02:48:30.3826228Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.extdeps.languages.bash_command_fold.bash_fold_lex disposition=Stored cpu_ms=0 wall_ms=0 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:30.4161518Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.compiler.program_assembly.dag_prepared_grammar disposition=Stored cpu_ms=32 wall_ms=32 rss_growth_bytes=4096 provenance=built-by-preparation\n2026-09-16T02:48:31.1141726Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.long.emit_host_produced_module_equals_eval.produced_add_module_source disposition=Stored cpu_ms=694 wall_ms=697 rss_growth_bytes=237568 provenance=built-by-preparation\n2026-09-16T02:48:31.6563401Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.long.emit_host_classical_not_ingested_equals_eval.ingested_classical_not_arrow_with_body disposition=Stored cpu_ms=529 wall_ms=531 rss_growth_bytes=20480 provenance=built-by-preparation\n2026-09-16T02:48:31.8729253Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.long.emit_host_classical_not_ingested_equals_eval.ingested_classical_not_swapped_arrow_with_body disposition=Stored cpu_ms=224 wall_ms=225 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:32.2808714Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.compiler.self_host.direct_rust_door_fixture.direct_rust_door_specimen_resolved disposition=Stored cpu_ms=405 wall_ms=408 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:32.6503107Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.execution.emit_on_demand_match_loop_fold_family_witness.mlf_family_primary_emitted disposition=Stored cpu_ms=358 wall_ms=369 rss_growth_bytes=487424 provenance=built-by-preparation\n2026-09-16T02:48:33.0043494Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.execution.emit_on_demand_family_crate_witness.logic_family_primary_emitted disposition=Stored cpu_ms=341 wall_ms=353 rss_growth_bytes=221184 provenance=built-by-preparation\n2026-09-16T02:48:33.3686481Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.self_host.stage0_production_target.stage0_boundary_profile_emitted_source disposition=Stored cpu_ms=358 wall_ms=364 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:33.5046083Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.self_host.stage0_production_target.stage0_boundary_base_emitted_source disposition=Stored cpu_ms=11 wall_ms=11 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:34.1446122Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.claim.self_host.rust_module_emission_population.population_emission_add disposition=Stored cpu_ms=744 wall_ms=764 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:34.3435250Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.claim.self_host.rust_module_emission_population.population_emission_add2 disposition=Stored cpu_ms=180 wall_ms=198 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:34.6980018Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.claim.self_host.rust_module_emission_population.population_emission_add_then_add2 disposition=Stored cpu_ms=342 wall_ms=354 rss_growth_bytes=114688 provenance=built-by-preparation\n2026-09-16T02:48:34.7349575Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.claim.self_host.rust_module_emission_population.population_declarationless_refuses disposition=Stored cpu_ms=35 wall_ms=36 rss_growth_bytes=20480 provenance=built-by-preparation\n2026-09-16T02:48:34.7437180Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.claim.self_host.rust_module_emission_population.population_unwired_two_declaration_refuses disposition=Stored cpu_ms=9 wall_ms=9 rss_growth_bytes=4096 provenance=built-by-preparation\n2026-09-16T02:48:34.7516227Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.claim.self_host.rust_module_emission_population.population_declaration_count_add disposition=Stored cpu_ms=6 wall_ms=6 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:34.7582621Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.claim.self_host.rust_module_emission_population.population_declaration_count_add_then_add2 disposition=Stored cpu_ms=8 wall_ms=8 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:34.9354974Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.parse.d1_declaration_grammar_parse.d1_where_reproducer_parsed disposition=Stored cpu_ms=166 wall_ms=173 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:35.0535117Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.parse.d1_declaration_grammar_parse.d1_where_bare_parsed disposition=Stored cpu_ms=116 wall_ms=121 rss_growth_bytes=90112 provenance=built-by-preparation\n2026-09-16T02:48:35.1540672Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.parse.d1_declaration_grammar_parse.d1_where_control_parsed disposition=Stored cpu_ms=97 wall_ms=100 rss_growth_bytes=49152 provenance=built-by-preparation\n2026-09-16T02:48:35.3384595Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.parse.d1_declaration_grammar_parse.d1_cache_identity_where_parsed disposition=Stored cpu_ms=183 wall_ms=184 rss_growth_bytes=4096 provenance=built-by-preparation\n2026-09-16T02:48:35.5009300Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.parse.where_refinement_clause_parse.where_refinement_bare_parsed disposition=Stored cpu_ms=161 wall_ms=162 rss_growth_bytes=16384 provenance=built-by-preparation\n2026-09-16T02:48:35.6112723Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.parse.expression_bodied_fn_decl_parse.expression_bodied_fn_parsed disposition=Stored cpu_ms=109 wall_ms=110 rss_growth_bytes=16384 provenance=built-by-preparation\n2026-09-16T02:48:35.6769819Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.parse.expression_bodied_fn_decl_parse.expression_bodied_literal_fn_parsed disposition=Stored cpu_ms=65 wall_ms=65 rss_growth_bytes=20480 provenance=built-by-preparation\n2026-09-16T02:48:35.7771869Z [floor-phase] phase=pure-producer-share-warm state=completed producer=v2.test.parse.expression_bodied_fn_decl_parse.braced_fn_control_parsed disposition=Stored cpu_ms=99 wall_ms=100 rss_growth_bytes=0 provenance=built-by-preparation\n2026-09-16T02:48:35.7781034Z [floor-phase] phase=pure-producer-share-scope state=completed rostered_modules_outside_subject=1 modules=[test.claim.live_deploy.emit]\n2026-09-16T02:48:55.2023750Z [floor-phase] phase=bare-reference-edge-index-warm state=completed roots=BareReferenceEdgeIndexBuild/source-roots cpu_ms=10124 wall_ms=17621 rss_growth_bytes=0 source_files=5856 bare_eligible=637 provenance=built-by-preparation\n2026-09-16T02:48:55.2034410Z [floor-phase] phase=bare-reference-edge-index-warm state=completed roots=BareReferenceEdgeIndexBuild/witness-layer-roots cpu_ms=6 wall_ms=6 rss_growth_bytes=0 source_files=5856 bare_eligible=637 provenance=already-warm-on-entry triggered_by=a-site-ahead-of-floor-preparation\n2026-09-16T02:48:55.2046185Z [floor-phase] phase=strict-preparation state=completed wall_ms=745230 modules_resolved=3019 modules_excluded=2 digest=eb8fa8db5887fb3b\n2026-09-16T02:48:55.4049682Z [floor-phase] phase=module-index state=completed wall_ms=202 modules=4460\n2026-09-16T02:48:55.7569513Z [floor-phase] phase=declarer-discovery state=completed wall_ms=350 declarers=18\n2026-09-16T02:48:56.1087890Z [floor-phase] phase=whole-tree-graph-facts state=completed wall_ms=353\n2026-09-16T02:48:56.1231903Z [floor-phase] phase=declarer-closure state=completed wall_ms=14 sources=19\n2026-09-16T02:48:56.2786170Z [floor-phase] phase=closure-strict-resolve state=completed wall_ms=155 sources=19\n2026-09-16T02:48:56.3076153Z [floor-phase] phase=published-mock-projection state=completed wall_ms=1105 keys=91\n2026-09-16T02:50:27.9817767Z [floor-phase] phase=discovery-authority state=completed wall_ms=90265 authority=v2.workflow.floor_discovery_source_authority sources=5856 rows=19891 entries=2194 full_inventory_release_rss_kb_before=15307380 full_inventory_release_trim_reclaimed_kb=731228 full_inventory_release_rss_kb_after=14577200\n2026-09-16T02:50:28.9533919Z [floor-claim-ceiling] grandfathered_identities=3779 grandfathered_budget_steps=361500 new_witness_budget_steps=72300\n2026-09-16T02:50:29.0124493Z [floor-phase] phase=site-projection state=completed wall_ms=91735 declared=19891 sites=4879 files=2194 claims=3971 declined_long=401 declined_fixture=0 declined_outside_gate=177 declined_gate_closure=15007 declined_discovery_excluded=5 declined_cost_debt=330\n2026-09-16T02:50:31.9575417Z [floor-phase] phase=expr-var-classification expr_var_occurrences=0 free_reference_edges=0 bound_occurrences_suppressed=0 qualified_chain_heads=0 classification_refusals=0\n2026-09-16T02:50:31.9580122Z [floor-phase] phase=expr-var-classification \n2026-09-16T02:50:31.9626843Z [floor-phase] phase=reference-closure-index state=completed wall_ms=0 modules=3 names=5 subject=c01458db5a196a34\n2026-09-16T02:50:31.9645327Z [floor-phase] phase=expr-var-classification expr_var_occurrences=1 free_reference_edges=0 bound_occurrences_suppressed=1 qualified_chain_heads=0 classification_refusals=0\n2026-09-16T02:50:31.9649696Z [floor-phase] phase=expr-var-classification BoundByParameter=1\n2026-09-16T02:50:31.9653062Z [floor-phase] phase=reference-closure-index state=completed wall_ms=0 modules=3 names=4 subject=92107e64fdc80bbc\n2026-09-16T02:50:31.9704793Z [floor-phase] phase=expr-var-classification expr_var_occurrences=1 free_reference_edges=1 bound_occurrences_suppressed=0 qualified_chain_heads=0 classification_refusals=0\n2026-09-16T02:50:31.9707855Z [floor-phase] phase=expr-var-classification DeclaredElsewhere=1\n2026-09-16T02:50:31.9712213Z [floor-phase] phase=reference-closure-index state=completed wall_ms=0 modules=4 names=7 subject=9b51427d706ae1d9\n2026-09-16T02:50:31.9898466Z [floor-phase] phase=expr-var-classification expr_var_occurrences=1 free_reference_edges=1 bound_occurrences_suppressed=0 qualified_chain_heads=0 classification_refusals=0\n2026-09-16T02:50:31.9903147Z [floor-phase] phase=expr-var-classification DeclaredInThisModule=1\n2026-09-16T02:50:31.9905070Z [floor-phase] phase=reference-closure-index state=completed wall_ms=0 modules=4 names=7 subject=3bd800efac0c7530\n2026-09-16T02:50:31.9923594Z [floor-phase] phase=expr-var-classification expr_var_occurrences=0 free_reference_edges=0 bound_occurrences_suppressed=0 qualified_chain_heads=0 classification_refusals=0\n2026-09-16T02:50:31.9926724Z [floor-phase] phase=expr-var-classification \n2026-09-16T02:50:31.9930122Z [floor-phase] phase=reference-closure-index state=completed wall_ms=0 modules=3 names=4 subject=fd4346f64dfada17\n2026-09-16T02:50:31.9993760Z [floor-phase] phase=expr-var-classification expr_var_occurrences=0 free_reference_edges=0 bound_occurrences_suppressed=0 qualified_chain_heads=0 classification_refusals=0\n2026-09-16T02:50:31.9995823Z [floor-phase] phase=expr-var-classification \n2026-09-16T02:50:31.9999837Z [floor-phase] phase=reference-closure-index state=completed wall_ms=0 modules=3 names=4 subject=fd4346f64dfada17\n2026-09-16T02:50:32.0033070Z [floor-phase] phase=expr-var-classification expr_var_occurrences=0 free_reference_edges=0 bound_occurrences_suppressed=0 qualified_chain_heads=0 classification_refusals=0\n2026-09-16T02:50:32.0037327Z [floor-phase] phase=expr-var-classification \n2026-09-16T02:50:32.0039559Z [floor-phase] phase=reference-closure-index state=completed wall_ms=0 modules=3 names=4 subject=fd4346f64dfada17\n2026-09-16T02:56:30.0047177Z [floor-cgroup] when=beat-20 path=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice/actions-runner@srv4-18.service\n2026-09-16T02:56:30.0056010Z [floor-cgroup] when=beat-20 level=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice/actions-runner@srv4-18.service max=17179869184 high=16106127360 current=16078217216 peak=16106631168 events=[low,0,high,7254,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,7254,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=2.17,avg60=1.80,avg300=1.62,total=26620107,full,avg10=2.17,avg60=1.80,avg300=1.62,total=26619735]\n2026-09-16T02:56:30.0068529Z [floor-cgroup] when=beat-20 level=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice max=max high=max current=159988195328 peak=364675248128 events=[low,0,high,53855074,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,0,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=0.24,avg60=0.28,avg300=0.47,total=13878228854,full,avg10=0.24,avg60=0.28,avg300=0.47,total=13740334938]\n2026-09-16T02:56:30.0079198Z [floor-cgroup] when=beat-20 level=/sys/fs/cgroup/system.slice max=max high=max current=176071000064 peak=380169330688 events=[low,0,high,53855074,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,0,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=0.21,avg60=0.26,avg300=0.45,total=13852086330,full,avg10=0.21,avg60=0.26,avg300=0.45,total=13713813769]\n2026-09-16T02:59:58.3859791Z [floor-fold-time] scope_build=143.5s over 695 construction(s) (mean=206ms) frame_build=2.2s over 3971 construction(s) (mean=0.5ms)\n2026-09-16T02:59:58.3860774Z [floor-scope-cost] max=0.13GB at=v2.test.claim.staging (1596 modules) total_built=1.29GB over 695 construction(s)\n2026-09-16T03:00:30.6968920Z [floor-phase] phase=terminal-ledger-publish state=completed resolve_ms=31249 total_ms=32635 rows=3971\n2026-09-16T03:00:30.8700701Z [over-cost] v2.test.claim.enforcement.determinism_transitive_witness.determinism_live_intra_holds observed_wall_ms=325 observed_cpu_ms=317 eval_steps=165094 line_ms=100 outcome=pass\n2026-09-16T03:00:30.8705737Z [over-cost] v2.test.lens_test_migration_debt.test_migration_debt_test.retained_rust_kernel_wall_holds_against_live_tree observed_wall_ms=295 observed_cpu_ms=292 eval_steps=3128 line_ms=100 outcome=fail\n2026-09-16T03:00:30.8711745Z [over-cost] v2.test.claim.body_lowering.arrow_body_form_witness.arrow_body_form_eval_value_vertical_holds observed_wall_ms=287 observed_cpu_ms=232 eval_steps=90747 line_ms=100 outcome=pass\n2026-09-16T03:00:30.8717111Z [over-cost] v2.test.claim.enforcement.lens_module_gate_witness.question_zero_verdict_live_holds observed_wall_ms=274 observed_cpu_ms=212 eval_steps=63825 line_ms=100 outcome=pass\n2026-09-16T03:00:30.8723183Z [over-cost] v2.test.emit.emit_module_contribution.emc_all_three_arms_are_constructed_by_the_emitter_holds observed_wall_ms=211 observed_cpu_ms=203 eval_steps=110579 line_ms=100 outcome=pass\n2026-09-16T03:00:30.8724944Z [over-cost] v2.test.parse.d5_expression_grammar_parse.cause_i_match_infix_parses_holds observed_wall_ms=204 observed_cpu_ms=203 eval_steps=76436 line_ms=100 outcome=pass\n2026-09-16T03:00:30.8726657Z [over-cost] v2.test.emit.emit_module_contribution.emc_origins_locate_the_unobserved_producer_holds observed_wall_ms=208 observed_cpu_ms=201 eval_steps=110307 line_ms=100 outcome=pass\n2026-09-16T03:06:30.0271620Z [floor-cgroup] when=beat-30 path=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice/actions-runner@srv4-18.service\n2026-09-16T03:06:30.0274812Z [floor-cgroup] when=beat-30 level=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice/actions-runner@srv4-18.service max=17179869184 high=16106127360 current=16106008576 peak=16112607232 events=[low,0,high,10824,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,10824,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=9.69,avg60=6.15,avg300=2.73,total=39674404,full,avg10=9.69,avg60=6.15,avg300=2.73,total=39670316]\n2026-09-16T03:06:30.0279569Z [floor-cgroup] when=beat-30 level=/sys/fs/cgroup/system.slice/system-actions\\x2drunner.slice max=max high=max current=172097458176 peak=364675248128 events=[low,0,high,53882643,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,0,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=0.61,avg60=1.03,avg300=1.39,total=13890030741,full,avg10=0.51,avg60=0.99,avg300=1.38,total=13752007203]\n2026-09-16T03:06:30.0283751Z [floor-cgroup] when=beat-30 level=/sys/fs/cgroup/system.slice max=max high=max current=188181905408 peak=380169330688 events=[low,0,high,53882645,max,0,oom,0,oom_kill,0,oom_group_kill,0] events_local=[low,0,high,0,max,0,oom,0,oom_kill,0,oom_group_kill,0] pressure=[some,avg10=0.61,avg60=1.00,avg300=1.35,total=13863806856,full,avg10=0.51,avg60=0.97,avg300=1.34,total=13725404851]" 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_job_log_receipt_forged_probe.dag b/dag/test/probe/qualification_job_log_receipt_forged_probe.dag new file mode 100644 index 00000000000..5e0c7f066a8 --- /dev/null +++ b/dag/test/probe/qualification_job_log_receipt_forged_probe.dag @@ -0,0 +1,45 @@ +module test.probe.qualification_job_log_receipt_forged_probe + +// THIS MODULE MUST NOT RESOLVE. Each function below is a route by which a caller outside +// gunbc.runner.runner_qualification_dispatch would otherwise hold a job-log receipt for rows it never +// read from a run, or read a run's outputs under a token or run id the collector never admitted: (a) +// writing the sealed receipt from invented readings, (b) calling the one function that mints it from +// outside the collect stage, (c) calling the reads past the read plan, (d) reading the claim-cost +// artifact for a free token and run id. The witness +// test.claim.qualification_job_log_receipt_forged_probe_witness hands this source to the compiler and +// requires each refusal at its subject 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.content_hash { content_hash_atom } +import std.types { Int, NonEmptyStr } +import std.resources { Network } +import gunbc.github_effect_perform { ControllerInstallationToken } +import gunbc.runner.runner_host_unit_slot { HostUnitSlot } +import gunbc.runner.runner_qualification_dispatch { + CollectedQualificationRun, QualificationJobLogReceipt, QualificationLogReadings, + JobLogInstrumentStanding, AttemptJobLog, job_log_standing, + QualificationCollectOutcome, collect_qualification_instruments_under, + ClaimCostArtifactRead, read_claim_cost_artifact, +} + +// (a) AN OUTSIDE-AUTHORED RECEIPT. Refuses at QualificationJobLogReceipt. +fn forged_receipt(c: CollectedQualificationRun, h: HostUnitSlot, rd: QualificationLogReadings) -> QualificationJobLogReceipt { + QualificationJobLogReceipt { collected: c, slot: h, log_code_points: 1, log_digest: content_hash_atom(value: "invented"), readings: rd } +} + +// (b) THE MINTER CALLED FROM OUTSIDE THE COLLECT STAGE, over a log this caller supplies. Refuses at +// job_log_standing. +fn sneaked_receipt(c: CollectedQualificationRun, h: HostUnitSlot, l: AttemptJobLog) -> JobLogInstrumentStanding { + job_log_standing(collected: c, slot: h, log: l) +} + +// (c) THE READS CALLED PAST THE READ PLAN: a genuine collection under a token the plan never admitted. +// Refuses at collect_qualification_instruments_under. +fn reads_past_the_plan(c: CollectedQualificationRun, t: ControllerInstallationToken) -> QualificationCollectOutcome uses net: Network { + collect_qualification_instruments_under(collected: c, token: t) +} + +// (d) THE CLAIM-COST READ UNDER A FREE TOKEN AND ANOTHER RUN'S ID. Refuses at read_claim_cost_artifact. +fn claim_cost_for_another_run(t: ControllerInstallationToken, owner: NonEmptyStr, repo: NonEmptyStr, other_run_id: Int) -> ClaimCostArtifactRead uses net: Network { + read_claim_cost_artifact(token: t, owner: owner, repo: repo, run_id: other_run_id) +} 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 }, + ) +}