From 01597ca55c00c9a5778876e3a899e9ad9a483fba Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 30 Aug 2026 12:10:46 +0000 Subject: [PATCH 1/4] Org Actions settings enter the modeled surface: extdeps.github.org_actions cites the runner-group shape, endpoints and the observed org-admin token-scope refusal; gunbc.fleet.org_actions_standing declares desired repo->fleet access and derives channel-honest standing (gunbc-private HoldsByBehavior via the srv4 run receipt, settings surface unread, public-fork toggle unobservable until the read lands); converge binding named as the next trigger with its credential precondition --- dag/extdeps/github/org_actions.dag | 39 +++++++ dag/gunbc/fleet/org_actions_standing.dag | 106 ++++++++++++++++++ .../org_actions_standing_witness_test.dag | 40 +++++++ 3 files changed, 185 insertions(+) create mode 100644 dag/extdeps/github/org_actions.dag create mode 100644 dag/gunbc/fleet/org_actions_standing.dag create mode 100644 dag/test/claim/fleet/org_actions_standing_witness_test.dag diff --git a/dag/extdeps/github/org_actions.dag b/dag/extdeps/github/org_actions.dag new file mode 100644 index 00000000000..bfd60b97c05 --- /dev/null +++ b/dag/extdeps/github/org_actions.dag @@ -0,0 +1,39 @@ +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 + +// GET /orgs/:org/actions/runner-groups -> runner_groups[]. 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 +} + +data org_runner_groups_endpoint: NonEmptyStr = "GET /orgs/:org/actions/runner-groups" +data org_runner_group_repos_endpoint: NonEmptyStr = "GET /orgs/:org/actions/runner-groups/:runner_group_id/repositories" +data org_actions_permissions_endpoint: NonEmptyStr = "GET /orgs/:org/actions/permissions" + +// 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" diff --git a/dag/gunbc/fleet/org_actions_standing.dag b/dag/gunbc/fleet/org_actions_standing.dag new file mode 100644 index 00000000000..b996331a64f --- /dev/null +++ b/dag/gunbc/fleet/org_actions_standing.dag @@ -0,0 +1,106 @@ +module gunbc.fleet.org_actions_standing + +import std.types { NonEmptyStr, String, Bool, Int, List } +import extdeps.github.org_actions { + OrgRunnerGroup, RunnerGroupVisibility, AllRepositories, SelectedRepositories, + org_runner_groups_endpoint, 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, exactly the unmodeled-authority shape fleet converge exists +// to eliminate. This module declares the DESIRED state and the OBSERVATIONS; the +// convergence loop (read settings -> diff -> refuse-or-apply) binds to fleet-converge +// once its credential precondition is met, and that binding is this module's declared +// next trigger, not something a hand edit in the UI satisfies. + +// --------------------------------------------------------------------------------------------- +// 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 = [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 - what we can actually see today, typed by HOW it was seen. +// --------------------------------------------------------------------------------------------- + +type OrgSettingsObservation + = SettingsRead { groups: List, observed_on: NonEmptyStr } + | SettingsReadRefusedTokenScope { refusal_fragment: NonEmptyStr, observed_on: NonEmptyStr } + +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 = [receipt_private_on_fleet] + +// --------------------------------------------------------------------------------------------- +// Standing - derived, honest about the observation channel. +// --------------------------------------------------------------------------------------------- + +type OrgAccessStanding + = HoldsBySettingsRead { observed_on: NonEmptyStr } + | HoldsByBehavior { run_id: NonEmptyStr, observed_on: NonEmptyStr } + | Unobserved + +fn repo_access_standing(r: RepoRunnerAccess) -> OrgAccessStanding { + match settings_observation_current { + SettingsRead { groups, observed_on } => HoldsBySettingsRead { 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 standing_is_observed(s: OrgAccessStanding) -> Bool { + match s { + HoldsBySettingsRead { observed_on } => true, + HoldsByBehavior { run_id, observed_on } => true, + Unobserved => false, + } +} + +data org_converge_binding_note: String = "NEXT TRIGGER, named as the capability: fleet-converge can converge this surface when (1) an org-administration-scoped credential is modeled in the fleet secret set - the repo-scoped integration token observably receives the 403 this module cites - and (2) the converge phase reads org_runner_groups_endpoint, diffs against desired_repo_access and desired_allows_public_repositories, and REFUSES on divergence it is not authorized to apply (a settings surface converged by silent overwrite would erase an operator's deliberate UI change; the diff is the deliverable, apply is gated). Until then the standing here is honest about its channel: HoldsByBehavior is weaker than HoldsBySettingsRead - behavior proves admission TODAY, not that the group's visibility row matches the desired shape - and a behavioral receipt cannot observe desired_allows_public_repositories at all, which is why that row has no standing fn: it is UNOBSERVABLE until the settings read lands, and deriving a green from its absence would be the reachability-read-as-occupancy failure." diff --git a/dag/test/claim/fleet/org_actions_standing_witness_test.dag b/dag/test/claim/fleet/org_actions_standing_witness_test.dag new file mode 100644 index 00000000000..d9f2741ff30 --- /dev/null +++ b/dag/test/claim/fleet/org_actions_standing_witness_test.dag @@ -0,0 +1,40 @@ +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, + OrgAccessStanding, HoldsBySettingsRead, HoldsByBehavior, Unobserved, + repo_access_standing, standing_is_observed, behavioral_receipts, + desired_allows_public_repositories, +} + +// THE DISCRIMINATING CLAIMS. (1) The standing derivation is channel-honest: with the +// settings read refused (today's observation), gunbc-private holds BY BEHAVIOR - the +// receipt names the run - while a repository with no behavioral receipt derives +// Unobserved rather than borrowing its neighbour's green. gunbc itself currently has no +// receipt row, so it IS the discriminating negative: if the derivation ever widens to +// answer for unreceipted repositories, this witness reds. (2) The public-fork policy row +// is false. (3) Every desired row demands fleet reach (a row that does not is dead). + +fn holds_by_behavior(s: OrgAccessStanding) -> Bool { + match s { + HoldsByBehavior { run_id, observed_on } => true, + HoldsBySettingsRead { observed_on } => false, + Unobserved => false, + } +} + +test fn witness_private_holds_by_behavior_only() -> Bool { + holds_by_behavior(s: repo_access_standing(r: access_gunbc_private)) + && !standing_is_observed(s: repo_access_standing(r: access_gunbc)) +} + +test fn witness_public_fork_trap_stays_closed() -> Bool { + desired_allows_public_repositories == false +} + +test fn witness_desired_rows_live() -> Bool { + count(desired_repo_access) == 2 + && fold(desired_repo_access, init: true, f: fn(acc, r) { acc && r.must_reach_fleet }) + && count(behavioral_receipts) == 1 +} From 4e08e6b31cbda60709ff78a2b650a5317d6f5f66 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 30 Aug 2026 12:37:38 +0000 Subject: [PATCH 2/4] Review 57587: SettingsRead arm consults its payload (membership admits, absence refuses - the fabricated-green control now executes and flips); observation carries the joined admitted set + public flag; converge binding moves from a String blob to a typed DissolutionCondition with rationale in annotations; count change-detectors dropped from the witness; endpoints re-modeled as github.CliOrgRunnerGroups operations in house transport style; run_id verbatim-digits ruling cited --- dag/extdeps/github/org_actions.dag | 47 +++++++-- dag/gunbc/fleet/org_actions_standing.dag | 75 +++++++++++---- .../org_actions_standing_witness_test.dag | 96 +++++++++++++++---- 3 files changed, 179 insertions(+), 39 deletions(-) diff --git a/dag/extdeps/github/org_actions.dag b/dag/extdeps/github/org_actions.dag index bfd60b97c05..b7d1d57d6f5 100644 --- a/dag/extdeps/github/org_actions.dag +++ b/dag/extdeps/github/org_actions.dag @@ -14,10 +14,10 @@ type RunnerGroupVisibility = AllRepositories | SelectedRepositories -// GET /orgs/:org/actions/runner-groups -> runner_groups[]. 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). +// 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 @@ -25,9 +25,42 @@ type OrgRunnerGroup { allows_public_repositories: Bool } -data org_runner_groups_endpoint: NonEmptyStr = "GET /orgs/:org/actions/runner-groups" -data org_runner_group_repos_endpoint: NonEmptyStr = "GET /orgs/:org/actions/runner-groups/:runner_group_id/repositories" -data org_actions_permissions_endpoint: NonEmptyStr = "GET /orgs/:org/actions/permissions" +// 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 diff --git a/dag/gunbc/fleet/org_actions_standing.dag b/dag/gunbc/fleet/org_actions_standing.dag index b996331a64f..8878b11455e 100644 --- a/dag/gunbc/fleet/org_actions_standing.dag +++ b/dag/gunbc/fleet/org_actions_standing.dag @@ -1,20 +1,16 @@ module gunbc.fleet.org_actions_standing import std.types { NonEmptyStr, String, Bool, Int, List } -import extdeps.github.org_actions { - OrgRunnerGroup, RunnerGroupVisibility, AllRepositories, SelectedRepositories, - org_runner_groups_endpoint, org_admin_scope_refusal_fragment, -} +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, exactly the unmodeled-authority shape fleet converge exists -// to eliminate. This module declares the DESIRED state and the OBSERVATIONS; the -// convergence loop (read settings -> diff -> refuse-or-apply) binds to fleet-converge -// once its credential precondition is met, and that binding is this module's declared -// next trigger, not something a hand edit in the UI satisfies. +// 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. @@ -46,13 +42,22 @@ data desired_repo_access: List = [access_gunbc, access_gunbc_p data desired_allows_public_repositories: Bool = false // --------------------------------------------------------------------------------------------- -// Observations - what we can actually see today, typed by HOW it was seen. +// 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. // --------------------------------------------------------------------------------------------- type OrgSettingsObservation - = SettingsRead { groups: List, observed_on: NonEmptyStr } + = SettingsRead { + admitted_repositories: List, + allows_public_repositories: Bool, + 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 @@ -77,17 +82,26 @@ data receipt_private_on_fleet: BehavioralReceipt = BehavioralReceipt { data behavioral_receipts: List = [receipt_private_on_fleet] // --------------------------------------------------------------------------------------------- -// Standing - derived, honest about the observation channel. +// 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 } + | RefusedBySettingsRead { observed_on: NonEmptyStr } | HoldsByBehavior { run_id: NonEmptyStr, observed_on: NonEmptyStr } | Unobserved -fn repo_access_standing(r: RepoRunnerAccess) -> OrgAccessStanding { - match settings_observation_current { - SettingsRead { groups, observed_on } => HoldsBySettingsRead { observed_on: observed_on }, +fn standing_from(obs: OrgSettingsObservation, r: RepoRunnerAccess) -> OrgAccessStanding { + match obs { + SettingsRead { admitted_repositories, allows_public_repositories, observed_on } => + if count(filter(admitted_repositories, x => x == r.repository)) >= 1 { + HoldsBySettingsRead { observed_on: observed_on } + } else { + RefusedBySettingsRead { 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 } @@ -95,12 +109,41 @@ fn repo_access_standing(r: RepoRunnerAccess) -> OrgAccessStanding { } } +fn repo_access_standing(r: RepoRunnerAccess) -> OrgAccessStanding { + standing_from(obs: settings_observation_current, r: r) +} + fn standing_is_observed(s: OrgAccessStanding) -> Bool { match s { HoldsBySettingsRead { observed_on } => true, + RefusedBySettingsRead { observed_on } => true, HoldsByBehavior { run_id, observed_on } => true, Unobserved => false, } } -data org_converge_binding_note: String = "NEXT TRIGGER, named as the capability: fleet-converge can converge this surface when (1) an org-administration-scoped credential is modeled in the fleet secret set - the repo-scoped integration token observably receives the 403 this module cites - and (2) the converge phase reads org_runner_groups_endpoint, diffs against desired_repo_access and desired_allows_public_repositories, and REFUSES on divergence it is not authorized to apply (a settings surface converged by silent overwrite would erase an operator's deliberate UI change; the diff is the deliverable, apply is gated). Until then the standing here is honest about its channel: HoldsByBehavior is weaker than HoldsBySettingsRead - behavior proves admission TODAY, not that the group's visibility row matches the desired shape - and a behavioral receipt cannot observe desired_allows_public_repositories at all, which is why that row has no standing fn: it is UNOBSERVABLE until the settings read lands, and deriving a green from its absence would be the reachability-read-as-occupancy failure." +// The public-fork policy row has its own standing because a behavioral receipt cannot +// observe it at all - only a settings read can, and deriving a green from its absence +// would be the reachability-read-as-occupancy failure. +type PublicForkPolicyStanding + = MatchesDesired { observed_on: NonEmptyStr } + | DivergesFromDesired { observed: Bool, observed_on: NonEmptyStr } + | UnobservableUntilSettingsRead + +fn public_fork_policy_standing(obs: OrgSettingsObservation) -> PublicForkPolicyStanding { + match obs { + SettingsRead { admitted_repositories, allows_public_repositories, observed_on } => + if allows_public_repositories == desired_allows_public_repositories { + MatchesDesired { observed_on: observed_on } + } else { + DivergesFromDesired { observed: allows_public_repositories, 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.") diff --git a/dag/test/claim/fleet/org_actions_standing_witness_test.dag b/dag/test/claim/fleet/org_actions_standing_witness_test.dag index d9f2741ff30..486a16eb1a6 100644 --- a/dag/test/claim/fleet/org_actions_standing_witness_test.dag +++ b/dag/test/claim/fleet/org_actions_standing_witness_test.dag @@ -3,38 +3,102 @@ 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, - OrgAccessStanding, HoldsBySettingsRead, HoldsByBehavior, Unobserved, - repo_access_standing, standing_is_observed, behavioral_receipts, - desired_allows_public_repositories, + OrgSettingsObservation, SettingsRead, SettingsReadRefusedTokenScope, + OrgAccessStanding, HoldsBySettingsRead, RefusedBySettingsRead, HoldsByBehavior, Unobserved, + standing_from, repo_access_standing, standing_is_observed, + PublicForkPolicyStanding, MatchesDesired, DivergesFromDesired, UnobservableUntilSettingsRead, + public_fork_policy_standing, desired_allows_public_repositories, } -// THE DISCRIMINATING CLAIMS. (1) The standing derivation is channel-honest: with the -// settings read refused (today's observation), gunbc-private holds BY BEHAVIOR - the -// receipt names the run - while a repository with no behavioral receipt derives -// Unobserved rather than borrowing its neighbour's green. gunbc itself currently has no -// receipt row, so it IS the discriminating negative: if the derivation ever widens to -// answer for unreceipted repositories, this witness reds. (2) The public-fork policy row -// is false. (3) Every desired row demands fleet reach (a row that does not is dead). +// THE DISCRIMINATING CLAIMS, every observation arm exercised. (1) Channel honesty under +// today's refused read: gunbc-private holds BY BEHAVIOR (the receipt names the run) while +// gunbc, with no receipt, derives Unobserved rather than borrowing its neighbour's green. +// (2) THE SETTINGS-READ ARM CONSULTS ITS PAYLOAD (the review-57587 defect): a read whose +// admitted set contains only gunbc-private admits it and REFUSES gunbc - a read arm that +// greens on mere read-success reds here. (3) The public-fork policy is decidable only by +// a settings read: matches on false, diverges on true, unobservable under the refusal. +// (4) Every desired row demands fleet reach. + +data probe_read_private_only: OrgSettingsObservation = SettingsRead { + admitted_repositories: ["gunb-ai/gunbc-private"], + allows_public_repositories: false, + observed_on: "2026-08-30", +} + +data probe_read_public_forks_open: OrgSettingsObservation = SettingsRead { + admitted_repositories: ["gunb-ai/gunbc", "gunb-ai/gunbc-private"], + allows_public_repositories: true, + observed_on: "2026-08-30", +} fn holds_by_behavior(s: OrgAccessStanding) -> Bool { match s { HoldsByBehavior { run_id, observed_on } => true, HoldsBySettingsRead { observed_on } => false, + RefusedBySettingsRead { observed_on } => false, + Unobserved => false, + } +} + +fn holds_by_read(s: OrgAccessStanding) -> Bool { + match s { + HoldsBySettingsRead { observed_on } => true, + RefusedBySettingsRead { observed_on } => false, + HoldsByBehavior { run_id, observed_on } => false, + Unobserved => false, + } +} + +fn refused_by_read(s: OrgAccessStanding) -> Bool { + match s { + RefusedBySettingsRead { observed_on } => true, + HoldsBySettingsRead { observed_on } => false, + HoldsByBehavior { run_id, observed_on } => false, Unobserved => false, } } -test fn witness_private_holds_by_behavior_only() -> Bool { +test fn witness_refused_read_is_channel_honest() -> Bool { holds_by_behavior(s: repo_access_standing(r: access_gunbc_private)) && !standing_is_observed(s: repo_access_standing(r: access_gunbc)) } -test fn witness_public_fork_trap_stays_closed() -> Bool { +test fn witness_settings_read_arm_consults_membership() -> Bool { + holds_by_read(s: standing_from(obs: probe_read_private_only, r: access_gunbc_private)) + && refused_by_read(s: standing_from(obs: probe_read_private_only, r: access_gunbc)) +} + +fn fork_matches(p: PublicForkPolicyStanding) -> Bool { + match p { + MatchesDesired { observed_on } => true, + DivergesFromDesired { observed, observed_on } => false, + UnobservableUntilSettingsRead => false, + } +} + +fn fork_diverges(p: PublicForkPolicyStanding) -> Bool { + match p { + DivergesFromDesired { observed, observed_on } => observed, + MatchesDesired { observed_on } => false, + UnobservableUntilSettingsRead => false, + } +} + +fn fork_unobservable(p: PublicForkPolicyStanding) -> Bool { + match p { + UnobservableUntilSettingsRead => true, + MatchesDesired { observed_on } => false, + DivergesFromDesired { observed, observed_on } => false, + } +} + +test fn witness_public_fork_policy_decidable_only_by_read() -> Bool { desired_allows_public_repositories == false + && fork_matches(p: public_fork_policy_standing(obs: probe_read_private_only)) + && fork_diverges(p: public_fork_policy_standing(obs: probe_read_public_forks_open)) + && fork_unobservable(p: public_fork_policy_standing(obs: SettingsReadRefusedTokenScope { refusal_fragment: "probe", observed_on: "2026-08-30" })) } -test fn witness_desired_rows_live() -> Bool { - count(desired_repo_access) == 2 - && fold(desired_repo_access, init: true, f: fn(acc, r) { acc && r.must_reach_fleet }) - && count(behavioral_receipts) == 1 +test fn witness_desired_rows_demand_fleet_reach() -> Bool { + fold(desired_repo_access, init: true, f: fn(acc, r) { acc && r.must_reach_fleet }) } From eb85e08866cd84f4c4790287fb8e30bd7ebfb78b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 30 Aug 2026 13:20:27 +0000 Subject: [PATCH 3/4] Review 57595: standing_is_observed moves into its only consumer (the witness) - a test-only predicate had no business in the model surface; the remaining variant-to-Bool helpers stay as witness-local assertion instruments, the corpus-standard shape --- dag/gunbc/fleet/org_actions_standing.dag | 9 --------- .../fleet/org_actions_standing_witness_test.dag | 14 +++++++++++++- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/dag/gunbc/fleet/org_actions_standing.dag b/dag/gunbc/fleet/org_actions_standing.dag index 8878b11455e..b9371d16f6d 100644 --- a/dag/gunbc/fleet/org_actions_standing.dag +++ b/dag/gunbc/fleet/org_actions_standing.dag @@ -113,15 +113,6 @@ fn repo_access_standing(r: RepoRunnerAccess) -> OrgAccessStanding { standing_from(obs: settings_observation_current, r: r) } -fn standing_is_observed(s: OrgAccessStanding) -> Bool { - match s { - HoldsBySettingsRead { observed_on } => true, - RefusedBySettingsRead { observed_on } => true, - HoldsByBehavior { run_id, observed_on } => true, - Unobserved => false, - } -} - // The public-fork policy row has its own standing because a behavioral receipt cannot // observe it at all - only a settings read can, and deriving a green from its absence // would be the reachability-read-as-occupancy failure. diff --git a/dag/test/claim/fleet/org_actions_standing_witness_test.dag b/dag/test/claim/fleet/org_actions_standing_witness_test.dag index 486a16eb1a6..c8efc0aa5d3 100644 --- a/dag/test/claim/fleet/org_actions_standing_witness_test.dag +++ b/dag/test/claim/fleet/org_actions_standing_witness_test.dag @@ -5,7 +5,7 @@ import gunbc.fleet.org_actions_standing { RepoRunnerAccess, desired_repo_access, access_gunbc_private, access_gunbc, OrgSettingsObservation, SettingsRead, SettingsReadRefusedTokenScope, OrgAccessStanding, HoldsBySettingsRead, RefusedBySettingsRead, HoldsByBehavior, Unobserved, - standing_from, repo_access_standing, standing_is_observed, + standing_from, repo_access_standing, PublicForkPolicyStanding, MatchesDesired, DivergesFromDesired, UnobservableUntilSettingsRead, public_fork_policy_standing, desired_allows_public_repositories, } @@ -31,6 +31,18 @@ data probe_read_public_forks_open: OrgSettingsObservation = SettingsRead { observed_on: "2026-08-30", } +// The variant-to-Bool helpers below are witness-local assertion instruments - the +// corpus-standard shape for pinning one arm of a coproduct (pareto_selection_witness, +// model_artifact_identity_witness use it the same way) - not substrate query surfaces. +fn standing_is_observed(s: OrgAccessStanding) -> Bool { + match s { + HoldsBySettingsRead { observed_on } => true, + RefusedBySettingsRead { observed_on } => true, + HoldsByBehavior { run_id, observed_on } => true, + Unobserved => false, + } +} + fn holds_by_behavior(s: OrgAccessStanding) -> Bool { match s { HoldsByBehavior { run_id, observed_on } => true, From fc5fb48864c2104e61673fe745cce1664c342bd4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sun, 30 Aug 2026 14:51:06 +0000 Subject: [PATCH 4/4] Review 57611: the read observation keeps the upstream GROUP grain (per-group public flag + repository list, lossless join) and public-fork exposure convicts only a group that ADMITS the repository, naming it; the read arm compares observed membership against must_reach_fleet in both directions, so a forbidden-but-admitted row derives typed divergence, never a hold - all arms witness-exercised including the forbidden-row probe and the non-serving-open-group probe --- dag/gunbc/fleet/org_actions_standing.dag | 59 ++++++--- .../org_actions_standing_witness_test.dag | 116 +++++++++++------- 2 files changed, 114 insertions(+), 61 deletions(-) diff --git a/dag/gunbc/fleet/org_actions_standing.dag b/dag/gunbc/fleet/org_actions_standing.dag index b9371d16f6d..159d64c0bca 100644 --- a/dag/gunbc/fleet/org_actions_standing.dag +++ b/dag/gunbc/fleet/org_actions_standing.dag @@ -48,12 +48,20 @@ data desired_allows_public_repositories: Bool = false // 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 +} + type OrgSettingsObservation - = SettingsRead { - admitted_repositories: List, - allows_public_repositories: Bool, - observed_on: NonEmptyStr - } + = SettingsRead { groups: List, observed_on: NonEmptyStr } | SettingsReadRefusedTokenScope { refusal_fragment: NonEmptyStr, observed_on: NonEmptyStr } // run_id carried as decimal digits verbatim per the standing ruling in @@ -90,17 +98,27 @@ data behavioral_receipts: List = [receipt_private_on_fleet] type OrgAccessStanding = HoldsBySettingsRead { observed_on: NonEmptyStr } - | RefusedBySettingsRead { 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, 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 { admitted_repositories, allows_public_repositories, observed_on } => - if count(filter(admitted_repositories, x => x == r.repository)) >= 1 { + SettingsRead { groups, observed_on } => + if observed_admits(groups: groups, repository: r.repository) == r.must_reach_fleet { HoldsBySettingsRead { observed_on: observed_on } } else { - RefusedBySettingsRead { observed_on: observed_on } + 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) { @@ -113,21 +131,24 @@ fn repo_access_standing(r: RepoRunnerAccess) -> OrgAccessStanding { standing_from(obs: settings_observation_current, r: r) } -// The public-fork policy row has its own standing because a behavioral receipt cannot -// observe it at all - only a settings read can, and deriving a green from its absence -// would be the reachability-read-as-occupancy failure. +// 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 { observed: Bool, observed_on: NonEmptyStr } + | DivergesFromDesired { exposing_groups: List, observed_on: NonEmptyStr } | UnobservableUntilSettingsRead -fn public_fork_policy_standing(obs: OrgSettingsObservation) -> PublicForkPolicyStanding { +fn public_exposure_standing(obs: OrgSettingsObservation, r: RepoRunnerAccess) -> PublicForkPolicyStanding { match obs { - SettingsRead { admitted_repositories, allows_public_repositories, observed_on } => - if allows_public_repositories == desired_allows_public_repositories { - MatchesDesired { observed_on: observed_on } - } else { - DivergesFromDesired { observed: allows_public_repositories, observed_on: observed_on } + 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, } diff --git a/dag/test/claim/fleet/org_actions_standing_witness_test.dag b/dag/test/claim/fleet/org_actions_standing_witness_test.dag index c8efc0aa5d3..e880bae58af 100644 --- a/dag/test/claim/fleet/org_actions_standing_witness_test.dag +++ b/dag/test/claim/fleet/org_actions_standing_witness_test.dag @@ -3,51 +3,70 @@ 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, - OrgAccessStanding, HoldsBySettingsRead, RefusedBySettingsRead, HoldsByBehavior, Unobserved, - standing_from, repo_access_standing, + OrgSettingsObservation, SettingsRead, SettingsReadRefusedTokenScope, ObservedGroupAccess, + OrgAccessStanding, HoldsBySettingsRead, DivergesBySettingsRead, HoldsByBehavior, Unobserved, + standing_from, repo_access_standing, observed_admits, PublicForkPolicyStanding, MatchesDesired, DivergesFromDesired, UnobservableUntilSettingsRead, - public_fork_policy_standing, desired_allows_public_repositories, + public_exposure_standing, desired_allows_public_repositories, } -// THE DISCRIMINATING CLAIMS, every observation arm exercised. (1) Channel honesty under -// today's refused read: gunbc-private holds BY BEHAVIOR (the receipt names the run) while -// gunbc, with no receipt, derives Unobserved rather than borrowing its neighbour's green. -// (2) THE SETTINGS-READ ARM CONSULTS ITS PAYLOAD (the review-57587 defect): a read whose -// admitted set contains only gunbc-private admits it and REFUSES gunbc - a read arm that -// greens on mere read-success reds here. (3) The public-fork policy is decidable only by -// a settings read: matches on false, diverges on true, unobservable under the refusal. -// (4) Every desired row demands fleet reach. +// 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 probe_read_private_only: OrgSettingsObservation = SettingsRead { - admitted_repositories: ["gunb-ai/gunbc-private"], +data grp_private_closed: ObservedGroupAccess = ObservedGroupAccess { + group_name: "default", allows_public_repositories: false, - observed_on: "2026-08-30", + repositories: ["gunb-ai/gunbc-private"], } -data probe_read_public_forks_open: OrgSettingsObservation = SettingsRead { - admitted_repositories: ["gunb-ai/gunbc", "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", } -// The variant-to-Bool helpers below are witness-local assertion instruments - the -// corpus-standard shape for pinning one arm of a coproduct (pareto_selection_witness, -// model_artifact_identity_witness use it the same way) - not substrate query surfaces. -fn standing_is_observed(s: OrgAccessStanding) -> Bool { - match s { - HoldsBySettingsRead { observed_on } => true, - RefusedBySettingsRead { observed_on } => true, - HoldsByBehavior { run_id, observed_on } => true, - Unobserved => false, - } +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, - RefusedBySettingsRead { observed_on } => false, + DivergesBySettingsRead { observed_admitted, desired, observed_on } => false, Unobserved => false, } } @@ -55,42 +74,52 @@ fn holds_by_behavior(s: OrgAccessStanding) -> Bool { fn holds_by_read(s: OrgAccessStanding) -> Bool { match s { HoldsBySettingsRead { observed_on } => true, - RefusedBySettingsRead { observed_on } => false, + DivergesBySettingsRead { observed_admitted, desired, observed_on } => false, HoldsByBehavior { run_id, observed_on } => false, Unobserved => false, } } -fn refused_by_read(s: OrgAccessStanding) -> Bool { +fn diverges_by_read(s: OrgAccessStanding) -> Bool { match s { - RefusedBySettingsRead { observed_on } => true, + 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)) - && !standing_is_observed(s: repo_access_standing(r: access_gunbc)) + && is_unobserved(s: repo_access_standing(r: access_gunbc)) } -test fn witness_settings_read_arm_consults_membership() -> Bool { +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)) - && refused_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: 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 { observed, observed_on } => false, + DivergesFromDesired { exposing_groups, observed_on } => false, UnobservableUntilSettingsRead => false, } } -fn fork_diverges(p: PublicForkPolicyStanding) -> Bool { +fn fork_diverges_naming(p: PublicForkPolicyStanding, group: NonEmptyStr) -> Bool { match p { - DivergesFromDesired { observed, observed_on } => observed, + DivergesFromDesired { exposing_groups, observed_on } => count(filter(exposing_groups, g => g == group)) == 1, MatchesDesired { observed_on } => false, UnobservableUntilSettingsRead => false, } @@ -100,17 +129,20 @@ fn fork_unobservable(p: PublicForkPolicyStanding) -> Bool { match p { UnobservableUntilSettingsRead => true, MatchesDesired { observed_on } => false, - DivergesFromDesired { observed, observed_on } => false, + DivergesFromDesired { exposing_groups, observed_on } => false, } } -test fn witness_public_fork_policy_decidable_only_by_read() -> Bool { +test fn witness_public_exposure_convicts_only_the_serving_group() -> Bool { desired_allows_public_repositories == false - && fork_matches(p: public_fork_policy_standing(obs: probe_read_private_only)) - && fork_diverges(p: public_fork_policy_standing(obs: probe_read_public_forks_open)) - && fork_unobservable(p: public_fork_policy_standing(obs: SettingsReadRefusedTokenScope { refusal_fragment: "probe", observed_on: "2026-08-30" })) + && 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") }