gunbc-private

dag/extdeps/github/org_actions.dag

@@ -0,0 +1,72 @@
+module extdeps.github.org_actions
+
+import std.types { NonEmptyStr, String, Bool, Int, List }
+
+// ORG-LEVEL GITHUB ACTIONS SETTINGS - the upstream surface, cited. These are the org
+// settings that decide whether a repository's workflows can reach the org's self-hosted
+// runners at all: the runner GROUP is the access-control object, not the runner
+// (docs.github.com/en/rest/actions/self-hosted-runner-groups, read 2026-08-30). This
+// module owns the SHAPE the API returns; which groups our org should have and which
+// repositories they must admit is a fleet policy fact and lives in gunbc.fleet, never
+// here.
+
+type RunnerGroupVisibility
+  = AllRepositories
+  | SelectedRepositories
+
+// The runner_groups[] element shape. selected_repositories_url is populated only when
+// visibility is selected; allows_public_repositories gates whether public-repo workflows
+// may use the group (public forks running on self-hosted hardware is the canonical
+// self-hosted security trap, which is why it defaults false upstream).
+type OrgRunnerGroup {
+  id: Int
+  name: NonEmptyStr
+  visibility: RunnerGroupVisibility
+  allows_public_repositories: Bool
+}
+
+// THE CLI TRANSPORT, one of N realizations and not a fact about the dependency -
+// consistent with extdeps.github.actions_runs github.CliActionsRuns. Both operations are
+// readonly observations; the repositories read exists because per-repo admission is only
+// decidable by joining a selected-visibility group to its repository list.
+service github.CliOrgRunnerGroups {
+  operation ListRunnerGroupsJson {
+    input {
+      org: NonEmptyStr
+    }
+    output {
+      success: Bool from "exit_success"
+      stdout: String from "stdout"
+      stderr: String from "stderr"
+    }
+    readonly
+    transport shell {
+      argv: ["gh", "api", "orgs/{org}/actions/runner-groups"]
+    }
+  }
+
+  operation ListRunnerGroupRepositoriesJson {
+    input {
+      org: NonEmptyStr
+      runner_group_id: Int
+    }
+    output {
+      success: Bool from "exit_success"
+      stdout: String from "stdout"
+      stderr: String from "stderr"
+    }
+    readonly
+    transport shell {
+      argv: ["gh", "api", "orgs/{org}/actions/runner-groups/{runner_group_id}/repositories"]
+    }
+  }
+}
+
+// TOKEN-SCOPE FACT, observed by execution 2026-08-30: these endpoints require org
+// administration scope. A repository-scoped integration token receives HTTP 403
+// {"message":"Resource not accessible by integration"} - observed against
+// /orgs/gunb-ai/actions/runners and /repos/gunb-ai/gunbc-private/actions/runners from
+// this session's gh credential. So a fleet convergence of org settings has a CREDENTIAL
+// precondition, not merely an API binding; the refusal string is the discriminator a
+// reader of a failed converge run should match against.
+data org_admin_scope_refusal_fragment: NonEmptyStr = "Resource not accessible by integration"

dag/gunbc/fleet/org_actions_standing.dag

@@ -0,0 +1,161 @@
+module gunbc.fleet.org_actions_standing
+
+import std.types { NonEmptyStr, String, Bool, Int, List }
+import std.dissolution { DissolutionCondition, unbound_dissolution }
+import extdeps.github.org_actions { org_admin_scope_refusal_fragment }
+
+// ORG ACTIONS SETTINGS AS A CONVERGED SURFACE (operator direction 2026-08-30: "we need
+// to connect the org github settings via fleet converge - basically this is all
+// unmodeled right now"). The org's runner-group access policy decides which repositories
+// reach the fleet, and until now it lived only in the GitHub settings UI - actuated by
+// hand, observed by nobody. This module declares the DESIRED state, the OBSERVATIONS
+// typed by channel, and the derived standing; the convergence binding is a typed
+// dissolution row below, not prose.
+
+// ---------------------------------------------------------------------------------------------
+// Desired state - fleet policy.
+// ---------------------------------------------------------------------------------------------
+
+type RepoRunnerAccess {
+  repository: NonEmptyStr
+  must_reach_fleet: Bool
+  reason: NonEmptyStr
+}
+
+data access_gunbc: RepoRunnerAccess = RepoRunnerAccess {
+  repository: "gunb-ai/gunbc",
+  must_reach_fleet: true,
+  reason: "the public witness floor runs on [self-hosted, linux, arm64]",
+}
+
+data access_gunbc_private: RepoRunnerAccess = RepoRunnerAccess {
+  repository: "gunb-ai/gunbc-private",
+  must_reach_fleet: true,
+  reason: "the private witness roster moved to the fleet 2026-08-30 (hosted-minutes pool exhausted; the business dogfoods its own runners)",
+}
+
+data desired_repo_access: List<RepoRunnerAccess> = [access_gunbc, access_gunbc_private]
+
+// The public-fork trap stays closed as policy: whatever group serves these repositories
+// must NOT allow public repositories unless a hardened, isolated runner class exists for
+// them - the tenant-isolation program owns that question, not a settings toggle.
+data desired_allows_public_repositories: Bool = false
+
+// ---------------------------------------------------------------------------------------------
+// Observations - typed by HOW they were seen. A successful settings read carries the
+// JOINED admission data (groups x their repository lists, flattened to the admitted set,
+// plus the public-repositories flag) because that is exactly what per-repo standing
+// needs - a read that carried less could not answer without fabricating.
+// ---------------------------------------------------------------------------------------------
+
+// The read observation preserves the GROUP grain the upstream stores (review 57611: a
+// flattened admitted set plus one org-wide public flag loses WHICH group admits which
+// repository, so with multiple groups the public-fork answer could be fabricated from a
+// non-serving group's flag). One row per observed group, carrying its own public flag
+// and its own repository list - the joined group -> repository -> public-access
+// relationship, lossless.
+type ObservedGroupAccess {
+  group_name: NonEmptyStr
+  allows_public_repositories: Bool
+  repositories: List<NonEmptyStr>
+}
+
+type OrgSettingsObservation
+  = SettingsRead { groups: List<ObservedGroupAccess>, observed_on: NonEmptyStr }
+  | SettingsReadRefusedTokenScope { refusal_fragment: NonEmptyStr, observed_on: NonEmptyStr }
+
+// run_id carried as decimal digits verbatim per the standing ruling in
+// extdeps.github.workflow_run_event (identity join, never arithmetic - no decode).
+type BehavioralReceipt {
+  repository: NonEmptyStr
+  runner_name: NonEmptyStr
+  run_id: NonEmptyStr
+  observed_on: NonEmptyStr
+}
+
+data settings_observation_current: OrgSettingsObservation = SettingsReadRefusedTokenScope {
+  refusal_fragment: org_admin_scope_refusal_fragment,
+  observed_on: "2026-08-30",
+}
+
+// A fleet runner EXECUTED a gunbc-private job - behavior proves the access policy admits
+// the repository today, even while the settings surface is unreadable to this credential.
+data receipt_private_on_fleet: BehavioralReceipt = BehavioralReceipt {
+  repository: "gunb-ai/gunbc-private",
+  runner_name: "srv4-01-1788089189-1873877",
+  run_id: "33309109321",
+  observed_on: "2026-08-30",
+}
+
+data behavioral_receipts: List<BehavioralReceipt> = [receipt_private_on_fleet]
+
+// ---------------------------------------------------------------------------------------------
+// Standing - derived, honest about the observation channel. The SettingsRead arm CONSULTS
+// its payload: membership admits, absence REFUSES - never a green from the read's mere
+// success. The derivation is pure in its observation so the witness can exercise every
+// arm; the data rows below bind it to the current observation.
+// ---------------------------------------------------------------------------------------------
+
+type OrgAccessStanding
+  = HoldsBySettingsRead { observed_on: NonEmptyStr }
+  | DivergesBySettingsRead { observed_admitted: Bool, desired: Bool, observed_on: NonEmptyStr }
+  | HoldsByBehavior { run_id: NonEmptyStr, observed_on: NonEmptyStr }
+  | Unobserved
+
+fn observed_admits(groups: List<ObservedGroupAccess>, repository: NonEmptyStr) -> Bool {
+  fold(groups, init: false, f: fn(acc, g) {
+    acc || count(filter(g.repositories, x => x == repository)) >= 1
+  })
+}
+
+// The read arm compares OBSERVED membership against the DESIRED boolean (review 57611:
+// membership alone reported a must_reach_fleet:false row's forbidden state as holding).
+// Agreement in either direction holds - admitted-and-required, or absent-and-forbidden -
+// and any mismatch is a typed divergence carrying both sides.
+fn standing_from(obs: OrgSettingsObservation, r: RepoRunnerAccess) -> OrgAccessStanding {
+  match obs {
+    SettingsRead { groups, observed_on } =>
+      if observed_admits(groups: groups, repository: r.repository) == r.must_reach_fleet {
+        HoldsBySettingsRead { observed_on: observed_on }
+      } else {
+        DivergesBySettingsRead { observed_admitted: observed_admits(groups: groups, repository: r.repository), desired: r.must_reach_fleet, observed_on: observed_on }
+      },
+    SettingsReadRefusedTokenScope { refusal_fragment, observed_on } =>
+      fold(behavioral_receipts, init: Unobserved, f: fn(acc, b) {
+        if b.repository == r.repository { HoldsByBehavior { run_id: b.run_id, observed_on: b.observed_on } } else { acc }
+      }),
+  }
+}
+
+fn repo_access_standing(r: RepoRunnerAccess) -> OrgAccessStanding {
+  standing_from(obs: settings_observation_current, r: r)
+}
+
+// Public-fork exposure is PER REPOSITORY over the group join: the desired-false policy is
+// violated exactly when some group that ADMITS this repository allows public
+// repositories - a non-serving group's flag can neither convict nor acquit.
+type PublicForkPolicyStanding
+  = MatchesDesired { observed_on: NonEmptyStr }
+  | DivergesFromDesired { exposing_groups: List<NonEmptyStr>, observed_on: NonEmptyStr }
+  | UnobservableUntilSettingsRead
+
+fn public_exposure_standing(obs: OrgSettingsObservation, r: RepoRunnerAccess) -> PublicForkPolicyStanding {
+  match obs {
+    SettingsRead { groups, observed_on } =>
+      match filter(groups, g => g.allows_public_repositories && count(filter(g.repositories, x => x == r.repository)) >= 1) {
+        exposing =>
+          if count(exposing) == 0 || desired_allows_public_repositories {
+            MatchesDesired { observed_on: observed_on }
+          } else {
+            DivergesFromDesired { exposing_groups: map(exposing, g => g.group_name), observed_on: observed_on }
+          },
+      },
+    SettingsReadRefusedTokenScope { refusal_fragment, observed_on } => UnobservableUntilSettingsRead,
+  }
+}
+
+// The converge binding, as a typed dissolution row (not prose): HoldsByBehavior is weaker
+// than HoldsBySettingsRead - behavior proves admission today, not group shape - and the
+// diff is the deliverable while apply stays gated, because a settings surface converged
+// by silent overwrite would erase an operator's deliberate UI change.
+data org_converge_binding_trigger: DissolutionCondition = unbound_dissolution(description: "dissolve-on: fleet-converge converges this surface. CAPABILITY, both parts required: (1) an org-administration-scoped credential lands in the fleet secret set - the repo-scoped integration token observably receives the 403 cited by org_admin_scope_refusal_fragment; (2) a converge phase reads github.CliOrgRunnerGroups (groups joined to their repository lists), constructs a SettingsRead observation, diffs it against desired_repo_access and desired_allows_public_repositories, and REFUSES on divergence it is not authorized to apply. Until both hold, the standing here is honest about its channel and the UI remains the hand-actuated authority.")

dag/test/claim/fleet/org_actions_standing_witness_test.dag

@@ -0,0 +1,148 @@
+module test.claim.org_actions_standing_witness
+
+import std.types { Bool, Int, NonEmptyStr, List }
+import gunbc.fleet.org_actions_standing {
+  RepoRunnerAccess, desired_repo_access, access_gunbc_private, access_gunbc,
+  OrgSettingsObservation, SettingsRead, SettingsReadRefusedTokenScope, ObservedGroupAccess,
+  OrgAccessStanding, HoldsBySettingsRead, DivergesBySettingsRead, HoldsByBehavior, Unobserved,
+  standing_from, repo_access_standing, observed_admits,
+  PublicForkPolicyStanding, MatchesDesired, DivergesFromDesired, UnobservableUntilSettingsRead,
+  public_exposure_standing, desired_allows_public_repositories,
+}
+
+// THE DISCRIMINATING CLAIMS, every observation arm exercised at group grain. (1) Channel
+// honesty under today's refused read: gunbc-private holds BY BEHAVIOR while unreceipted
+// gunbc derives Unobserved. (2) The read arm compares membership against the DESIRED
+// boolean, both directions (review 57611): required-and-admitted holds, required-but-
+// absent diverges, and a FORBIDDEN row that is nonetheless admitted derives divergence -
+// never a hold. (3) Public-fork exposure is decided by the SERVING group's flag: a
+// public-allowing group that admits the repo convicts and is NAMED; a public-allowing
+// group that does NOT admit it cannot convict; refused read is unobservable. (4) Every
+// desired row demands fleet reach.
+
+data grp_private_closed: ObservedGroupAccess = ObservedGroupAccess {
+  group_name: "default",
+  allows_public_repositories: false,
+  repositories: ["gunb-ai/gunbc-private"],
+}
+
+data grp_private_open: ObservedGroupAccess = ObservedGroupAccess {
+  group_name: "default",
+  allows_public_repositories: true,
+  repositories: ["gunb-ai/gunbc-private"],
+}
+
+data grp_other_open: ObservedGroupAccess = ObservedGroupAccess {
+  group_name: "sandbox",
+  allows_public_repositories: true,
+  repositories: ["gunb-ai/some-other-repo"],
+}
+
+data probe_read_private_only: OrgSettingsObservation = SettingsRead {
+  groups: [grp_private_closed],
+  observed_on: "2026-08-30",
+}
+
+data probe_read_exposing: OrgSettingsObservation = SettingsRead {
+  groups: [grp_private_open],
+  observed_on: "2026-08-30",
+}
+
+data probe_read_nonserving_open: OrgSettingsObservation = SettingsRead {
+  groups: [grp_private_closed, grp_other_open],
+  observed_on: "2026-08-30",
+}
+
+// The review-57611 case: a policy row FORBIDDING fleet reach, observed admitted anyway.
+data probe_forbidden_repo: RepoRunnerAccess = RepoRunnerAccess {
+  repository: "gunb-ai/gunbc-private",
+  must_reach_fleet: false,
+  reason: "probe: forbidden-access row",
+}
+
+// The variant-to-Bool helpers below are witness-local assertion instruments - the
+// corpus-standard shape for pinning one arm of a coproduct - not substrate query surfaces.
+fn holds_by_behavior(s: OrgAccessStanding) -> Bool {
+  match s {
+    HoldsByBehavior { run_id, observed_on } => true,
+    HoldsBySettingsRead { observed_on } => false,
+    DivergesBySettingsRead { observed_admitted, desired, observed_on } => false,
+    Unobserved => false,
+  }
+}
+
+fn holds_by_read(s: OrgAccessStanding) -> Bool {
+  match s {
+    HoldsBySettingsRead { observed_on } => true,
+    DivergesBySettingsRead { observed_admitted, desired, observed_on } => false,
+    HoldsByBehavior { run_id, observed_on } => false,
+    Unobserved => false,
+  }
+}
+
+fn diverges_by_read(s: OrgAccessStanding) -> Bool {
+  match s {
+    DivergesBySettingsRead { observed_admitted, desired, observed_on } => true,
+    HoldsBySettingsRead { observed_on } => false,
+    HoldsByBehavior { run_id, observed_on } => false,
+    Unobserved => false,
+  }
+}
+
+fn is_unobserved(s: OrgAccessStanding) -> Bool {
+  match s {
+    Unobserved => true,
+    HoldsBySettingsRead { observed_on } => false,
+    DivergesBySettingsRead { observed_admitted, desired, observed_on } => false,
+    HoldsByBehavior { run_id, observed_on } => false,
+  }
+}
+
+test fn witness_refused_read_is_channel_honest() -> Bool {
+  holds_by_behavior(s: repo_access_standing(r: access_gunbc_private))
+    && is_unobserved(s: repo_access_standing(r: access_gunbc))
+}
+
+test fn witness_read_arm_compares_desired_both_directions() -> Bool {
+  holds_by_read(s: standing_from(obs: probe_read_private_only, r: access_gunbc_private))
+    && diverges_by_read(s: standing_from(obs: probe_read_private_only, r: access_gunbc))
+    && diverges_by_read(s: standing_from(obs: probe_read_private_only, r: probe_forbidden_repo))
+}
+
+fn fork_matches(p: PublicForkPolicyStanding) -> Bool {
+  match p {
+    MatchesDesired { observed_on } => true,
+    DivergesFromDesired { exposing_groups, observed_on } => false,
+    UnobservableUntilSettingsRead => false,
+  }
+}
+
+fn fork_diverges_naming(p: PublicForkPolicyStanding, group: NonEmptyStr) -> Bool {
+  match p {
+    DivergesFromDesired { exposing_groups, observed_on } => count(filter(exposing_groups, g => g == group)) == 1,
+    MatchesDesired { observed_on } => false,
+    UnobservableUntilSettingsRead => false,
+  }
+}
+
+fn fork_unobservable(p: PublicForkPolicyStanding) -> Bool {
+  match p {
+    UnobservableUntilSettingsRead => true,
+    MatchesDesired { observed_on } => false,
+    DivergesFromDesired { exposing_groups, observed_on } => false,
+  }
+}
+
+test fn witness_public_exposure_convicts_only_the_serving_group() -> Bool {
+  desired_allows_public_repositories == false
+    && fork_matches(p: public_exposure_standing(obs: probe_read_private_only, r: access_gunbc_private))
+    && fork_diverges_naming(p: public_exposure_standing(obs: probe_read_exposing, r: access_gunbc_private), group: "default")
+    && fork_matches(p: public_exposure_standing(obs: probe_read_nonserving_open, r: access_gunbc_private))
+    && fork_unobservable(p: public_exposure_standing(obs: SettingsReadRefusedTokenScope { refusal_fragment: "probe", observed_on: "2026-08-30" }, r: access_gunbc_private))
+}
+
+test fn witness_desired_rows_demand_fleet_reach() -> Bool {
+  fold(desired_repo_access, init: true, f: fn(acc, r) { acc && r.must_reach_fleet })
+    && observed_admits(groups: [grp_private_closed], repository: "gunb-ai/gunbc-private")
+    && !observed_admits(groups: [grp_private_closed], repository: "gunb-ai/gunbc")
+}