Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
47 commits
Select commit Hold shift + click to select a range
63c9500
mtcollins1 runner: JIT register/deregister over a managed-host unit b…
Oct 4, 2026
6423206
mtcollins1 runner: bind the dispatch leg to CreateDispatch with the a…
Oct 4, 2026
f33d265
leg 3: seal the dispatched run and the collected arm; check the readb…
Oct 4, 2026
303651b
leg 3: admit only Bool-returning claims to the sealed conclude; delet…
Oct 4, 2026
b07b575
Address side-chat RC on #13206: causal readback, sealed subject/recei…
Oct 4, 2026
60b36c6
Merge leg-2 split (b07b575) into leg 3; dispatch leg is LegAuthorityI…
Oct 4, 2026
ccad694
Image leg is LegAuthorityImplemented: no production caller builds the…
Oct 4, 2026
f48396f
Merge remote-tracking branch 'origin/session/nimble-ram-151' into ses…
Oct 4, 2026
5063c33
Merge remote-tracking branch 'origin/main' into session/jolly-bat-898
Oct 4, 2026
f6e820a
leg 3: answer the operator review -- sealed dispatch subject, commit-…
Oct 4, 2026
417b619
leg 3: fix builtin names and witness fixtures (first/last, declaratio…
Oct 4, 2026
a20fb39
leg 3: share #13225's runner identity (job_ran_on over runner_name ==…
Oct 4, 2026
d7838a7
leg 3: exhaustive matches over RunnerSpec, WorkflowTrigger and the te…
Oct 4, 2026
d3514f3
Seal the authorized JIT dispatch and bind the runner listing to its q…
Oct 4, 2026
d66a36a
Merge remote-tracking branch 'origin/session/nimble-ram-151' into ses…
Oct 4, 2026
dbb305f
Merge #13206 d3514f3 (AuthorizedJitMintDispatch sealed); the dispatch…
Oct 4, 2026
8bc9069
leg 3: split the over-budget scope claim into one claim per independe…
Oct 4, 2026
ecb6720
leg 3 witness per DESIGN section 3: supply values at each interface (…
Oct 4, 2026
67bb240
leg 3: keep the real-path claim to the mint and the sealed subject; d…
Oct 4, 2026
29003c4
leg 3: the production mint over the real fleet_converge_workflow is i…
Oct 4, 2026
afd21c5
Merge origin/main into leg 3 (imports-only conflict in runner_microvm…
Oct 4, 2026
de5e586
Merge origin/main into leg 3 (github_app_registry witness imports: ke…
Oct 4, 2026
cf29159
leg 3: production mint reads the declared inputs before building flee…
Oct 4, 2026
c22c2b5
leg 3 RC items 1-3: delivery carries its authorized dispatch; dispatc…
Oct 4, 2026
82498c3
leg 3 RC item 4: per-attempt branch pin -- create-once refs/heads/qua…
Oct 4, 2026
6ce55dd
leg 3 item 1: the delivery carries its mint's plain JitMintIdentity (…
Oct 4, 2026
c0a4c9b
leg 3 witness: the slot positive control passes pin_branch (a bare 'b…
Oct 4, 2026
6d3ebff
Merge origin/main (leg 2 #13206 landed) into leg 3; every conflict wa…
Oct 4, 2026
392995f
leg 3: branch_absent matches every RestExchangePerformance arm (floor…
Oct 4, 2026
8bb3f19
leg 3 RC (392995f): sealed delivery carrier, collection token join, W…
Oct 4, 2026
5a610d3
leg 3: commit the rewrap probe the rewrap witness compiles (a local .…
Oct 4, 2026
ea89826
leg 3 RC item 2 by sha-checkout (decision eager-gull-22): the floor j…
Oct 4, 2026
b49e0e2
leg 3 RC (review 5408711178): receive_jit_mint and the generate fold …
Oct 5, 2026
3e99b76
leg 3: collection admission is a pure read plan (plan_qualification_c…
Oct 5, 2026
7ebc19e
leg 3: close the planned-reads arm (unterminated function body at 3e9…
Oct 5, 2026
ea199ce
Merge origin/main into leg 3; authorization_pattern_selection witness…
Oct 5, 2026
ac79028
leg 3 (review 76234): the ruling record says only what the ruling say…
Oct 5, 2026
08be556
leg 3 (review 76234): the operator's 2026-10-05 scope ruling (escalat…
Oct 5, 2026
38e5456
leg 3: the scope ruling bounds where the 10-03 discharge may apply (a…
Oct 5, 2026
b164681
leg 3: the dedicated group's selected-workflow pin is authorized by i…
Oct 5, 2026
15eb7f6
Merge origin/main into leg 3: port onto #13171's RestResult (no outco…
Oct 5, 2026
85b699a
runner qualification: split the production subject wiring out of the …
Oct 7, 2026
8c1f0cd
workflow_runs: record that the runner-field trigger landed; drop the …
Oct 7, 2026
048afa6
runner_qualification_dispatch: delete unconsumed qualification_run_co…
Oct 7, 2026
6f897f0
Merge remote-tracking branch 'origin/main' into fix13211
Oct 8, 2026
1f16f30
Merge-adapt: StandingRulingUnderInterlock coproduct (#13493) -- censu…
Oct 8, 2026
7fddcd2
Merge origin/main into session/jolly-bat-898; census keeps both sides…
Oct 9, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 67 additions & 0 deletions dag/extdeps/github/git_database.dag
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,8 @@ type GitRefObjectWire {
sha: String
}

type GitRefDeletedBody {}

type GitRefWire {
ref: String
object: GitRefObjectWire
Expand Down Expand Up @@ -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/<name>`) 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/<name>` 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" }
}

Expand Down Expand Up @@ -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
}
}
}
36 changes: 36 additions & 0 deletions dag/extdeps/github/org_actions.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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 `<owner>/<repo>/<workflow path>@<ref>`; 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
Expand Down Expand Up @@ -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<String>
}
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
}
}
}
41 changes: 26 additions & 15 deletions dag/extdeps/github/workflow_runs.dag
Original file line number Diff line number Diff line change
Expand Up @@ -168,24 +168,20 @@ fn workflow_job_attempt_filter_wire(f: WorkflowJobAttemptFilter) -> String {
}
}

// A THIRD FIELD WAS DELETED HERE AND STAYS DELETED, and this annotation is the second attempt to
// settle it. An earlier lane added runner_name because the vendor machine name is corroborating --
// the Biome baseline job reports "depot-1mw2k81zm2" -- found nothing read it, and deleted it on the
// ground that interesting is not a consumer. This change put it back claiming a consumer had
// arrived, in prose, while the diff carried no import and no call site; it is deleted again on the
// original ground, which was right both times. DESIGN section 4c is the rule: an annotation is
// never evidence that a machine claim holds.
// THE RUNNER FIELDS RETURNED WHEN THEIR NAMED TRIGGER LANDED. An earlier lane added runner_name,
// found nothing read it, and deleted it on the ground that interesting is not a consumer; a second
// attempt claimed a consumer in prose with no import or call site and was deleted again. The trigger
// that was named is a fold that IMPORTS this module and reads the field, landing in the same change
// as the field: gunbc.runner.runner_qualification_dispatch job_ran_on is that fold, so the fields are
// here with their consumer in the same change.
//
// The example survives the deletion because it is the part that was worth keeping.
// "depot-1mw2k81zm2" is neither GitHub-hosted nor self-hosted but a third party's fleet, so any
// provenance reading with two arms folds a paying provider customer in with a team running its own
// hardware. The trigger that brings the field back is a fold that IMPORTS this module and reads
// the field, landing in the same change as the field -- and that fold now has a further obligation
// this lane learned the hard way: a runs-on LABEL already has an authority in
// gunbc.runner.runner_label_resolution, backed by the per-provider catalogs
// The example that survived both deletions still governs the reading. "depot-1mw2k81zm2" is neither
// GitHub-hosted nor self-hosted but a third party's fleet, so any provenance reading with two arms
// folds a paying provider customer in with a team running its own hardware. A runs-on LABEL has an
// authority in gunbc.runner.runner_label_resolution, backed by the per-provider catalogs
// gunbc.runner.runner_provider_survey enrolls, so a consumer may not re-answer the label question
// with a fresh prefix roster. A runner NAME is a different vocabulary with no such authority, which
// is the one thing this field would genuinely add.
// is what these fields add.
//
// `name` is the only matrix-leg identifier this resource carries. The Jobs REST job object
// (docs.github.com/en/rest/actions/workflow-jobs, X-GitHub-Api-Version 2026-03-10) publishes
Expand All @@ -194,6 +190,12 @@ fn workflow_job_attempt_filter_wire(f: WorkflowJobAttemptFilter) -> String {
// rendered name. The parenthetical of combination VALUES in axis order is the rendering this
// tree observed on those names; it is not a REST field. Standing is TranscribedUncited until
// GitHub's Jobs docs state that encoding.
// runner_id AND runner_name ARE WHICH RUNNER TOOK THE JOB, a third fact beside the declared runs-on
// and the observed labels: two runners can carry identical labels. runner_id is the exact identity
// GitHub returned when the JIT registration was minted (gunbc.runner.runner_qualification_dispatch
// job_ran_on joins on it); runner_name is corroboration, since one name can resolve to several ids.
// Upstream publishes both as nullable -- null until a runner takes the job -- and every record in
// this tree written before the fields existed carries none rather than a guessed value.
type WorkflowJobRun {
id: Int
run_id: Int
Expand All @@ -202,6 +204,8 @@ type WorkflowJobRun {
status: WorkflowRunStatus
conclusion: WorkflowRunConclusion?
labels: List<String>
runner_id: Int?
runner_name: String?
created_at: Timestamp?
started_at: Timestamp?
completed_at: Timestamp?
Expand Down Expand Up @@ -293,10 +297,17 @@ data structural_coverage_gap_workflow_run_codec_hand_rolled: List<String> = [
// 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" }
}

Expand Down
43 changes: 18 additions & 25 deletions dag/extdeps/github/workflows.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,13 +3,9 @@ module extdeps.github.workflows
import extdeps.ietf.http_semantics { POST }
import extdeps.github.github { default_api_base }
import extdeps.github.errors { GitHubErrorShape }
import std.credentials { EnvVar }
import std.types { CommitSha, List, NonEmptyStr }
import std.types { NonEmptyStr, Secret, String }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import std.roster_frontier { FrontierRow, frontier_row_decl }
import std.dissolution { unbound_dissolution }
import std.decl_ref { decl_ref }
import std.resources { Network }
import extdeps.ietf.http_semantics { POST }
import extdeps.transports.rest { RestResult }
Expand Down Expand Up @@ -42,48 +38,45 @@ 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<FrontierRow> = [
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<String, String>
}
output {
workflow_run_id: Int
run_url: NonEmptyStr
html_url: NonEmptyStr
result: WorkflowDispatchReceipt
}
transport rest {
method: POST,
path: "/repos/\{owner\}/\{repo\}/actions/workflows/\{workflow_id\}/dispatches",
headers: { "X-GitHub-Api-Version": workflows_api_version },
body: {
ref: ref,
inputs: { expected_healed_sha: expected_healed_sha }
inputs: inputs
}
}
response {
Expand Down
Loading
Loading