From 149737814dbb5ded8331b4041133211b95a92e02 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 6 Aug 2026 20:49:24 +0000 Subject: [PATCH 1/2] MemberChanged{from,to}: declaration-owned occurrence identity and typed replacement classification Split MemberAction's collapsed upsert into four arms per operator ruling: MemberAdded{to} | MemberChanged{from,to} | MemberRemoved{from} | MemberRemovalRefused{from, cause}. The discarded `from` was the load-bearing loss. Every safe realization of a change consumes the prior value: an SCM ref update is a compare-and-swap that names the expected prior (git update-ref ), and a host resource whose address moved needs the prior endpoint to retire. With only `to` in hand the sole reachable realization is the unconditional write. MemberEffect splits the same way (EffectAdd/EffectReplace{from,to}/EffectRemove) so the apply grain can retire a prior realization instead of overwriting it blind. gunbc.host_resource: identity is allocator-minted at declaration, never derived from unit/path/content. HostResourceIdentity{host, occurrence} + HostResource{identity, role, value}, role a type parameter so a new role is an instantiation rather than a widened central enum. This is the closed-system answer to renames: git does not track them, it INFERS them from content similarity, and DESIGN 4 rules a heuristic never necessary in a closed system -- a content-derived key_of is that inference wearing a bundle. Distinct carrier from std.occurrence_identity (source-occurrence specific; one shared Int space would let occurrence_id_eq answer true on a numeric coincidence -- the cross-family comparison the ContentHash grounding closed). The subject- parameterized extraction is registered as a trigger, not built under a load-bearing module with stage0 work in flight. gunbc.change_realization: the classification table. SCM ref -> atomic CAS; source declaration move -> atomic SCM tree transformation; same runtime address -> in-place update; changed host address -> staged replacement with declared intermediates. Kills a live conflation: a .dag module re-home is an SCM tree transformation, NOT a host migration. StagedIntermediates is head+tail so an empty intermediate plan has no constructor, and an undeclared one refuses (typed, located) rather than degrading to an overwrite -- the srv4 lesson (its build-cache server died with its cgroup, never unlinked its socket, ran uncached for weeks) made unwritable rather than warned about in prose. A change-refusal arm was built during this work and WITHDRAWN: gunbc.ownership defines Ensured as "requires present but does NOT own (never torn down)", a constraint on removal, not update. It broke tool_readiness and repo_local_git_config (whose job is re-installing drifted pins/bindings) and was unreachable elsewhere. Per DESIGN 4c a carrier note is not evidence, so the withdrawal is enrolled as w_ensured_member_converges_but_refuses_removal. All three new guards verified DISCRIMINATING by planting their exact regressions: reintroducing the change-refusal arm reds the Ensured control alone; reintroducing the collapse reds the both-sides rows; turning the staged-replacement refusal into an InPlaceUpdate fallback reds the srv4 row. Caught during migration: repo_local_git_config's apply fold has a `_ => acc` wildcard for its construction-unreachable removal arms, and MemberChanged would have fallen into it -- silently dropping the drift that module exists to converge. Both write arms are now explicit. live_deploy's EffectReplace is structurally unreachable at both degenerate poles and emits a loud typed poison per that module's discipline; its 44 byte-identity goldens pass unchanged. Witnesses green by execution: membership_reconcile 10/10, change_realization 8/8, live_deploy 44/44, plus tool_readiness, repo_local_git_config, workflow_reconcile, srv3, host_phase_status, roadmap_belt, host_axis_caps. Corpus compile carries the same 10 pre-existing diagnostics as main, none mine. Co-Authored-By: Claude Opus 5 (1M context) --- DESIGN.md | 2 +- dag/gunbc/change_realization.dag | 81 ++++++++ dag/gunbc/design_document.dag | 2 +- dag/gunbc/host_axis_caps.dag | 10 +- dag/gunbc/host_phase_status.dag | 13 +- dag/gunbc/host_resource.dag | 67 +++++++ dag/gunbc/live_deploy/emit.dag | 17 +- dag/gunbc/membership_reconcile.dag | 103 ++++++---- dag/gunbc/non_fold_residue.dag | 2 +- .../host_convergence_circuit_residue.dag | 2 +- dag/gunbc/repo_local_git_config.dag | 54 +++--- dag/gunbc/roadmap_belt.dag | 32 +-- dag/gunbc/tool_readiness.dag | 2 +- dag/gunbc/workflow_reconcile.dag | 25 ++- .../claim/change_realization_witness_test.dag | 183 ++++++++++++++++++ .../claim/host_phase_status_witness_test.dag | 4 +- .../membership_reconcile_witness_test.dag | 105 +++++++--- .../repo_local_git_config_witness_test.dag | 8 +- .../claim/srv3_subsumption_witness_test.dag | 34 ++-- .../claim/tool_readiness_witness_test.dag | 12 +- .../claim/workflow_reconcile_witness_test.dag | 45 +++-- .../hermetic-tool-provisioning-design.md | 2 +- .../membership-diff-reconcile-spine-design.md | 63 ++++++ .../recursive-workflow-advancement-design.md | 2 +- docs/plans/seamless-deploys-design.md | 2 +- 25 files changed, 701 insertions(+), 171 deletions(-) create mode 100644 dag/gunbc/change_realization.dag create mode 100644 dag/gunbc/host_resource.dag create mode 100644 dag/test/claim/change_realization_witness_test.dag diff --git a/DESIGN.md b/DESIGN.md index fba457e816b..71d96e59021 100644 --- a/DESIGN.md +++ b/DESIGN.md @@ -145,7 +145,7 @@ hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/` - **witness realization — the v2 execution path.** Emit witnesses to native code (Rust now; C a row-policy option, §7) and use realization/materialization to schedule the runs; the dependency-ordered work that discharges the v2 memory-control findings, none of it gated on self-hosting. → [witness realization plan](docs/plans/witness-realization-plan.md) (findings it discharges: [v2 memory-control audit](docs/plans/v2-memory-control-audit.md)) - **machine-shape orthogonal scheduling — one realization kernel over faithfully modeled machine facts, with locality (§2).** DRAFT for review; model-before-implement, each phase names its trigger. Its authority transfers to the std/extdeps carriers it names when Phase 1 lands, at which point this md dissolves into a registered `gunbc.plan.Plan` row (§6). → [machine-shape scheduling design](docs/plans/machine-shape-orthogonal-scheduling.md) - **namespace-only name resolution — the containment tree is the single naming authority (operator-signed 2026-07-06).** Supersedes resolver-graph-major §1c's *import-name-universe* ("own declarations ∪ direct import lists" visibility), carrying forward its mechanics unchanged (binding-edge owner, unbound/double-bound = error, patterns-via-scrutinee, no expected-type picker). One structure — **syntactic containment** — induces everything at once: qualified name = nesting position (`T{a}` → `a` *is* `T.a`; `T{a{a}}` → inner *is* `T.a.a`, so Rule-2 no-ambiguity holds by construction), reference = lexical lookup up the ancestor chain (a sibling module is visible, its members projected `node.Symbol`), `.` = projection one level down (field / module-member / variant — one op), and `.` *is* the `std.induction` sub-value relation (descent evidence). So one content-addressed tree grounds THREE consumers — resolution *walks* it, content-addressing *hashes* it, termination reads its *sub-value* edges (§2 Realization: one structure, N consumers). Frontend BUILDS the tree from nesting (pure structure, zero resolution logic); backend WALKS it (lexical up, project down) — no heuristics to tune (the tuning risk = resolving against a flat index instead of the tree). Two governing rules (operator, 2026-07-06): **no dual representation / minimal at every layer; no ambiguity at any layer.** Rides on `SymbolIndex` = "the containment tree materialized" (`type-env-single-authority`, lively-raven lane) — the loyal-heron scaling gate that formerly blocked resolver surgery was **discharged at #6809** (per §7.5 of the design doc: "the lane is no longer blocked on it"); `import-scoped` (§1c, today) and `namespace-only-Y` (position-info uniqueness: expected type filters a variant to one, never picks) are two walk-rules over one *fill-agnostic* index (fill = whole tree; policy gates lookup, never fill). Census: 98% of names globally unique → always bare; the residue is v1-seed forks (resolve by subtree, free) + github-style variants ((Y) context-resolves); no consolidate-now forks (the census's 2 same-name flags proved to be a homonym + whole-file v1-seed duplication, not genuine cross-tree §3 forks). Terminal step: delete the `import` grammar + supporting code → `import` becomes a *parse error*, deps derived from `container.member` references (Rule-1 end-state). → [namespace-only resolution design](docs/plans/namespace-resolution-design.md) -- **fleet-reconcile spine — one grain-agnostic membership diff (deploy · fleet · session).** ONE `membership_reconcile` reuses `std.change.keyed_two_way_diff` verbatim (no fork): desired set vs observed set keyed by member IDENTITY — Added/Modified → upsert, Removed → teardown-or-refuse, Unchanged → noop (absence of a hunk). A member may be a service/unit/host OR a Session (operator: 'it should all be the same'), so a new member type is a new instantiation of the same fn with its own `(key_of, key_eq, value_eq, ownership_of)` bundle — zero spine change (a Realization, §2; a forked reconcile means the genericity bought nothing). R5 teardown-owned-only is a CONSTRUCTION WALL: a Removed non-owned member yields `MemberTeardownRefused`, which has no effect arm in any apply dispatch, so the bad state is unwritable — never a post-check, never 'assume owned' (the absorbing fallback §5 forbids); ownership-unknown REFUSES too, typed/located/counted. Ownership is extracted as its own single authority (`gunbc.ownership.Ownership`) and `live_deploy`'s `DeploymentStep` re-grounds onto it (pass 2, a declared dissolution trigger — never a second `Owned|Ensured`). Pass 1 (spine + R5 + a synthetic discriminating witness the degenerate apply/retract poles cannot exercise) landed. → [membership-diff reconcile spine design](docs/plans/membership-diff-reconcile-spine-design.md) +- **fleet-reconcile spine — one grain-agnostic membership diff (deploy · fleet · session).** ONE `membership_reconcile` reuses `std.change.keyed_two_way_diff` verbatim (no fork): desired set vs observed set keyed by member IDENTITY — Added → `MemberAdded{to}`, Modified → `MemberChanged{from,to}`, Removed → `MemberRemoved`-or-`MemberRemovalRefused`, Unchanged → noop (absence of a hunk). **Add and change are separate arms, not one `upsert`** (operator ruling): the collapse discarded `from`, which is precisely the fact a safe realization of a change needs — an SCM ref update is a compare-and-swap naming the expected prior (`git update-ref `), and a host resource whose address moved needs the prior endpoint to retire, so with only `to` in hand the sole reachable realization is the unconditional write. `gunbc.change_realization` `classify_change` is the table that consumes both sides: SCM ref → atomic CAS; source declaration move → atomic SCM tree transformation; same runtime address → in-place update; changed host address → staged replacement with **declared** intermediates. That last row is the srv4 lesson made unwritable rather than warned about — `StagedIntermediates` is head+tail so an empty intermediate plan has no constructor, and an undeclared one REFUSES (typed, located) instead of degrading to an overwrite. It also kills a live conflation: a `.dag` module re-home is an SCM tree transformation, **not** a host migration. **Only removal consults ownership**, and that asymmetry is deliberate: `gunbc.ownership` defines `Ensured` as 'requires present but does NOT own (never torn down)', a constraint on removal, so converging a drifted member the model does not own is the intended behavior of an `Ensured` member rather than a violation of it (`tool_readiness` exists to re-install a drifted pin). A change-refusal arm was built during this work and WITHDRAWN for over-firing on exactly that; the regression control `w_ensured_member_converges_but_refuses_removal` keeps it withdrawn by execution rather than by prose. A member may be a service/unit/host OR a Session (operator: 'it should all be the same'), so a new member type is a new instantiation of the same fn with its own `(key_of, key_eq, value_eq, ownership_of)` bundle — zero spine change (a Realization, §2; a forked reconcile means the genericity bought nothing). R5 removal-owned-only is a CONSTRUCTION WALL: a Removed non-owned member yields `MemberRemovalRefused`, which has no effect arm in any apply dispatch, so the bad state is unwritable — never a post-check, never 'assume owned' (the absorbing fallback §5 forbids); ownership-unknown REFUSES too, typed/located/counted. Ownership is extracted as its own single authority (`gunbc.ownership.Ownership`) and `live_deploy`'s `DeploymentStep` re-grounds onto it (pass 2, a declared dissolution trigger — never a second `Owned|Ensured`). Pass 1 (spine + R5 + a synthetic discriminating witness the degenerate apply/retract poles cannot exercise) landed. Identity is **declaration-owned and allocator-minted**, never derived from unit/path/content (operator ruling): `gunbc.host_resource` carries `HostResourceIdentity{host, occurrence}` and `HostResource{identity, role, value}`, where the occurrence is minted by an allocator, `role` is a **type parameter** (so a new role is an instantiation, never a widened central enum), and unit name / FIFO / storage path / configuration are mutable *value* fields. That is what makes a rename ONE `MemberChanged` rather than a delete-plus-create some key function must be clever enough to re-pair — git does not track renames, it INFERS them from content similarity, and §4 rules a heuristic never necessary in a closed system; a content-or-path-derived `key_of` is that same inference wearing a bundle. It is a carrier distinct from `std.occurrence_identity` deliberately: that module is specifically about SOURCE occurrences (its `OccurrenceCategory` enumerates callable/type/field/method, its allocator is coupled to `AuthoredTokenOrdinalSpace`), and sharing one `Int` space across two subjects would let `occurrence_id_eq` answer `true` on a numeric coincidence — the cross-family comparison the `ContentHash` family grounding closed. Extracting one subject-parameterized minted-identity carrier (the `Vendor` shape) is registered as a trigger, not built under a load-bearing module with stage0 work in flight. → [membership-diff reconcile spine design](docs/plans/membership-diff-reconcile-spine-design.md) - **one authorization kernel, several typed request profiles (operator directive 2026-08-01).** `std.access.AccessRequest` carries subject, action, object, typed context, and typed evidence; `AccessPolicy` is the sole policy-to-decision seam, `decision_meet` the sole conjunction, and every denial carries a typed cause at structured request coordinates. Effect, reference, publication admission, disclosure, and sealed execution are exact request products projected into that kernel, never independent allow/deny folds. Principals project external evidence — OIDC issuer/subject and observed POSIX effective principal — rather than being invented internal identities. The provisional gunbc#7541 `Verb::Reference` / `Verb::Publish` / `AudienceScopeTree` carriers dissolved: audiences are sets with join and partial-order subset, because real audiences can overlap without either containing the other. `PublicationAdmissionRequest` is only the generic request shape here: the operator-deleted Stage-0 placement wall, publisher policy, and pathname census are deliberately absent. - **publication and reference-admission capabilities — carrier retirement, replacement ontology unresolved.** **Removal record (operator ruling 2026-08-01):** the Stage-0 `Publish`/`Reference` effect-grant experiment retired after its sole live publication consumer, the placement gate, was deleted. `Reference` and `Publish` were removed from `std.effect_grant.Verb`, `AudienceScopeTree` was removed, and `std.visibility_grant` plus its carrier-only witnesses were deleted; generic authorization admission re-homed onto the `std.access` kernel. This retires those carriers, not the underlying capabilities. Publication remains required, but no replacement ontology has been selected and any redesign requires operator review before implementation. Reference-edge admission — whether an edge may form within one compiled program — is a separate deferred capability awaiting a concrete consumer; the publication rollback decides nothing about it. **Stage 0 per-file placement gate DELETED:** its constant `Publish World` rows duplicated Git's post-cutover path population, four same-day repair rounds raced identical reconstructions and repeatedly redded fleet CI, ordinary modifications were invisible, and a CI check after a public push could protect merge integrity but not confidentiality because the objects had already reached public storage. New public files require no stamp. Any future confidentiality boundary must act before unauthorized bytes enter public storage — for example by withholding public-write capability from ordinary sessions — but that constraint selects no replacement architecture. The locked extension remains a **publication capability product, not a ladder**: source/interface disclosure, artifact delivery, local/remote execution, integrity, reproducibility, existence/churn disclosure, revocation/erase, and placement/trust are independent policy axes. An emitted artifact is not source disclosure but remains inspectable; client-held key means plaintext access, distinct from remote/attested key custody. Locked blobs use AEAD with subject/interface/version/audience/policy context bound as associated data plus confidentiality-and-integrity-preserving per-audience key wraps; wrong key/context/authentication is typed refusal. Per-statement holes remain refused; interface/realization is the cut; size padding and `Secret`/`Pii`→`SecretRef` construction constraints remain. Commitments never promise zero leakage: length, timing, interface shape, wrap count, access pattern, low-entropy guessing, and churn stay in a named threat model. Remote execution and SCM diagnostics obey information-flow/noninterference + explicit declassification; metering prices an oracle but does not secure it, and unauthorized audiences receive only a non-leaking diagnostic projection. Cryptographic erase is conditional on every key/wrap/backup/cache/derivative/recovery path being sanitized and the result validated, never “delete one key.” → [retired node/subtree carrier experiment](docs/plans/node-subtree-visibility-grants.md) - **effect grants over namespaces — dissolve `Hermetic | Wet` into (frame × verb × subtree).** The 2-valued `Hermetic | Wet` enum conflates four axes (input closure / replayability, output reach / interference, handler binding, selection eligibility) — a §3 state-space conflation with proto-envelopes already forked (the hand-rolled `workspace_root` containment gate, `std.resources.ResourceHandle`, `AuthScope`, `LiveTreeDisposition`). End shape (§3, cited not minted): an effect target is a position in a containment tree that already exists — filesystem paths, URIs, `/proc`, service-operation paths, and the unifying case **code names themselves** (the containment tree the namespace-resolution lane makes the single naming authority); permission is a grant of (verb × subtree) attached to a `Frame`; admissibility is the namespace prefix relation — the same `⊑` the resolver walks, content-addressing hashes, and termination reads, so effects become the **fourth consumer** of the one containment structure. Dispatch projects an `EffectRequest` through `std.access.AccessPolicy` fail-closed (`Deny` carries the typed/located/counted refusal, never a silent widen — §5); *replayable* / *isolated* / `LiveTreeDisposition` become **derived** projections, and `Hermetic | Wet | Record` survive only as named envelope presets, deleted at the end. Frame-containment is graded on the §5 construction/validation axis (`LifecycleByConstruction` vs `LifecycleByConvention`). No code lands from the design doc; the FLAG-A interim is the only near-term consumer. → [effect-namespace-grants design](docs/plans/effect-namespace-grants.md) diff --git a/dag/gunbc/change_realization.dag b/dag/gunbc/change_realization.dag new file mode 100644 index 00000000000..d1e17c198fa --- /dev/null +++ b/dag/gunbc/change_realization.dag @@ -0,0 +1,81 @@ +module gunbc.change_realization + +import std.types { String, List, Bool, Int, NonEmptyStr } + +data change_realization_authority_note: String = "THE classification a MemberChanged\{from,to} carries into apply: given that an occurrence survived and only its value moved, HOW is that move realized? This is the table that makes MemberChanged useful rather than merely more faithful — without it, every change is an undifferentiated overwrite and the only available realization is the most dangerous one. The four rows are not four conveniences: they are four DIFFERENT atomicity guarantees, and picking the wrong row is how a safe transformation acquires an unsafe realization." + +data scm_versus_host_conflation_note: String = "THE conflation this table exists to kill: a .dag module re-home is an SCM TREE TRANSFORMATION, not a host migration. Moving a declaration between modules changes no runtime address, unlinks no socket, and restarts no unit — it is atomic in the SCM and needs no intermediates at all. Treating it as a host migration is what made an ordinary source cleanup look like it required an operational migration plan. The converse error is the dangerous one: renaming a systemd unit or moving a FIFO IS a host replacement, its intermediate states are real and observable, and calling it a mere update is how a live endpoint gets stranded." + +type ChangeSubject + = ScmRefSubject + | SourceDeclarationSubject + | HostResourceSubject + +data address_continuity_note: String = "For a host resource the deciding fact is whether the RUNTIME ADDRESS survived the change — the unit name, socket path, FIFO, endpoint. Same address means the running thing can absorb a new value in place; a changed address means two addresses exist during the transition and the old one must be retired, which is a staged operation with observable intermediate states. Continuity is DERIVED by comparing the address projection of from and to (address_continuity), never asserted by a caller-supplied Bool: an address that is claimed preserved while actually moving is exactly the silent wrong answer DESIGN §5 forbids." + +type AddressContinuity = AddressPreserved | AddressChanged + +fn address_continuity(from: A, to: A, address_eq: fn(A, A) -> Bool) -> AddressContinuity { + if address_eq(from, to) { AddressPreserved } else { AddressChanged } +} + +data staged_intermediate_srv4_specimen_note: String = "The LIVE specimen that makes declared intermediates a requirement rather than a nicety: srv4's build-cache server died with its cgroup, never unlinked its socket, and ran uncached for weeks because nobody modeled the intermediate state. gunbc.build_cache_instance already says IN PROSE that a managed unit must clear a stale endpoint on start — and a sentence in prose is the one place no machine can read it (DESIGN §4c: any machine-consumed fact belongs in a typed carrier). StagedIntermediates is that sentence given a carrier. Emptiness is unrepresentable by construction (head + tail, not a List that could be []), because a staged replacement whose intermediate list is empty is precisely the srv4 state: a transition that believed it had nothing to retire." + +type StagedIntermediate + = RetirePriorEndpoint { endpoint: NonEmptyStr } + | UnlinkStalePath { path: NonEmptyStr } + | StopPriorUnit { unit: NonEmptyStr } + | DrainPriorConsumers { description: NonEmptyStr } + +type StagedIntermediates { + first: StagedIntermediate + rest: List +} + +fn staged_intermediates_all(steps: StagedIntermediates) -> List { + concat([steps.first], steps.rest) +} + +fn staged_intermediates_count(steps: StagedIntermediates) -> Int { + 1 + count(steps.rest) +} + +type ChangeRealization + = AtomicCompareAndSwap + | AtomicTreeTransformation + | InPlaceUpdate + | StagedReplacement { intermediates: StagedIntermediates } + +data change_classification_refusal_note: String = "A staged replacement whose intermediates were never declared REFUSES; it does not fall back to an in-place update and it does not proceed with an empty plan. Both fallbacks are the absorbing fallback DESIGN §5 forbids, and the second is the srv4 outcome exactly. The refusal is typed and LOCATED — it carries subject_label, the identity of the resource whose intermediates are missing, so a refusal points at a thing rather than merely reporting that something somewhere is undeclared so the deficit is countable and ranks for fixing, rather than having its frequency zeroed by a silent widen." + +type ChangeRefusalCause + = StagedReplacementIntermediatesUndeclared { subject_label: NonEmptyStr } + +type ChangeClassification + = ChangeRealized { realization: ChangeRealization } + | ChangeRefused { cause: ChangeRefusalCause } + +fn classify_change( + subject: ChangeSubject, + subject_label: NonEmptyStr, + continuity: AddressContinuity, + declared_intermediates: StagedIntermediates?, +) -> ChangeClassification { + match subject { + ScmRefSubject => ChangeRealized { realization: AtomicCompareAndSwap } + SourceDeclarationSubject => ChangeRealized { realization: AtomicTreeTransformation } + HostResourceSubject => + match continuity { + AddressPreserved => ChangeRealized { realization: InPlaceUpdate } + AddressChanged => + match declared_intermediates { + Present { value: steps } => + ChangeRealized { realization: StagedReplacement { intermediates: steps } } + Absent => + ChangeRefused { cause: StagedReplacementIntermediatesUndeclared { subject_label: subject_label } } + } + } + } +} + +data scm_ref_compare_and_swap_note: String = "An SCM ref update is a COMPARE-AND-SWAP, not a write: git update-ref names the expected prior value, so a concurrent update loses rather than silently overwriting. That expected-prior is the from side of MemberChanged — which is another reason the pre-MemberChanged collapse was lossy in a load-bearing way, not merely untidy: with only the to side in hand, the sole available realization is the unconditional write, and the atomicity the underlying capability already offers cannot be reached. AtomicCompareAndSwap is therefore a realization the from side UNLOCKS, not merely one it documents." diff --git a/dag/gunbc/design_document.dag b/dag/gunbc/design_document.dag index 19ee9d952b6..063706d1843 100644 --- a/dag/gunbc/design_document.dag +++ b/dag/gunbc/design_document.dag @@ -182,7 +182,7 @@ fn open_threads_blocks() -> List { li(text: "**witness realization — the v2 execution path.** Emit witnesses to native code (Rust now; C a row-policy option, §7) and use realization/materialization to schedule the runs; the dependency-ordered work that discharges the v2 memory-control findings, none of it gated on self-hosting. → [witness realization plan](docs/plans/witness-realization-plan.md) (findings it discharges: [v2 memory-control audit](docs/plans/v2-memory-control-audit.md))"), li(text: "**machine-shape orthogonal scheduling — one realization kernel over faithfully modeled machine facts, with locality (§2).** DRAFT for review; model-before-implement, each phase names its trigger. Its authority transfers to the std/extdeps carriers it names when Phase 1 lands, at which point this md dissolves into a registered `gunbc.plan.Plan` row (§6). → [machine-shape scheduling design](docs/plans/machine-shape-orthogonal-scheduling.md)"), li(text: "**namespace-only name resolution — the containment tree is the single naming authority (operator-signed 2026-07-06).** Supersedes resolver-graph-major §1c's *import-name-universe* (\"own declarations ∪ direct import lists\" visibility), carrying forward its mechanics unchanged (binding-edge owner, unbound/double-bound = error, patterns-via-scrutinee, no expected-type picker). One structure — **syntactic containment** — induces everything at once: qualified name = nesting position (`T\{a\}` → `a` *is* `T.a`; `T\{a\{a\}\}` → inner *is* `T.a.a`, so Rule-2 no-ambiguity holds by construction), reference = lexical lookup up the ancestor chain (a sibling module is visible, its members projected `node.Symbol`), `.` = projection one level down (field / module-member / variant — one op), and `.` *is* the `std.induction` sub-value relation (descent evidence). So one content-addressed tree grounds THREE consumers — resolution *walks* it, content-addressing *hashes* it, termination reads its *sub-value* edges (§2 Realization: one structure, N consumers). Frontend BUILDS the tree from nesting (pure structure, zero resolution logic); backend WALKS it (lexical up, project down) — no heuristics to tune (the tuning risk = resolving against a flat index instead of the tree). Two governing rules (operator, 2026-07-06): **no dual representation / minimal at every layer; no ambiguity at any layer.** Rides on `SymbolIndex` = \"the containment tree materialized\" (`type-env-single-authority`, lively-raven lane) — the loyal-heron scaling gate that formerly blocked resolver surgery was **discharged at #6809** (per §7.5 of the design doc: \"the lane is no longer blocked on it\"); `import-scoped` (§1c, today) and `namespace-only-Y` (position-info uniqueness: expected type filters a variant to one, never picks) are two walk-rules over one *fill-agnostic* index (fill = whole tree; policy gates lookup, never fill). Census: 98% of names globally unique → always bare; the residue is v1-seed forks (resolve by subtree, free) + github-style variants ((Y) context-resolves); no consolidate-now forks (the census's 2 same-name flags proved to be a homonym + whole-file v1-seed duplication, not genuine cross-tree §3 forks). Terminal step: delete the `import` grammar + supporting code → `import` becomes a *parse error*, deps derived from `container.member` references (Rule-1 end-state). → [namespace-only resolution design](docs/plans/namespace-resolution-design.md)"), - li(text: "**fleet-reconcile spine — one grain-agnostic membership diff (deploy · fleet · session).** ONE `membership_reconcile` reuses `std.change.keyed_two_way_diff` verbatim (no fork): desired set vs observed set keyed by member IDENTITY — Added/Modified → upsert, Removed → teardown-or-refuse, Unchanged → noop (absence of a hunk). A member may be a service/unit/host OR a Session (operator: 'it should all be the same'), so a new member type is a new instantiation of the same fn with its own `(key_of, key_eq, value_eq, ownership_of)` bundle — zero spine change (a Realization, §2; a forked reconcile means the genericity bought nothing). R5 teardown-owned-only is a CONSTRUCTION WALL: a Removed non-owned member yields `MemberTeardownRefused`, which has no effect arm in any apply dispatch, so the bad state is unwritable — never a post-check, never 'assume owned' (the absorbing fallback §5 forbids); ownership-unknown REFUSES too, typed/located/counted. Ownership is extracted as its own single authority (`gunbc.ownership.Ownership`) and `live_deploy`'s `DeploymentStep` re-grounds onto it (pass 2, a declared dissolution trigger — never a second `Owned|Ensured`). Pass 1 (spine + R5 + a synthetic discriminating witness the degenerate apply/retract poles cannot exercise) landed. → [membership-diff reconcile spine design](docs/plans/membership-diff-reconcile-spine-design.md)"), + li(text: "**fleet-reconcile spine — one grain-agnostic membership diff (deploy · fleet · session).** ONE `membership_reconcile` reuses `std.change.keyed_two_way_diff` verbatim (no fork): desired set vs observed set keyed by member IDENTITY — Added → `MemberAdded\{to}`, Modified → `MemberChanged\{from,to}`, Removed → `MemberRemoved`-or-`MemberRemovalRefused`, Unchanged → noop (absence of a hunk). **Add and change are separate arms, not one `upsert`** (operator ruling): the collapse discarded `from`, which is precisely the fact a safe realization of a change needs — an SCM ref update is a compare-and-swap naming the expected prior (`git update-ref `), and a host resource whose address moved needs the prior endpoint to retire, so with only `to` in hand the sole reachable realization is the unconditional write. `gunbc.change_realization` `classify_change` is the table that consumes both sides: SCM ref → atomic CAS; source declaration move → atomic SCM tree transformation; same runtime address → in-place update; changed host address → staged replacement with **declared** intermediates. That last row is the srv4 lesson made unwritable rather than warned about — `StagedIntermediates` is head+tail so an empty intermediate plan has no constructor, and an undeclared one REFUSES (typed, located) instead of degrading to an overwrite. It also kills a live conflation: a `.dag` module re-home is an SCM tree transformation, **not** a host migration. **Only removal consults ownership**, and that asymmetry is deliberate: `gunbc.ownership` defines `Ensured` as 'requires present but does NOT own (never torn down)', a constraint on removal, so converging a drifted member the model does not own is the intended behavior of an `Ensured` member rather than a violation of it (`tool_readiness` exists to re-install a drifted pin). A change-refusal arm was built during this work and WITHDRAWN for over-firing on exactly that; the regression control `w_ensured_member_converges_but_refuses_removal` keeps it withdrawn by execution rather than by prose. A member may be a service/unit/host OR a Session (operator: 'it should all be the same'), so a new member type is a new instantiation of the same fn with its own `(key_of, key_eq, value_eq, ownership_of)` bundle — zero spine change (a Realization, §2; a forked reconcile means the genericity bought nothing). R5 removal-owned-only is a CONSTRUCTION WALL: a Removed non-owned member yields `MemberRemovalRefused`, which has no effect arm in any apply dispatch, so the bad state is unwritable — never a post-check, never 'assume owned' (the absorbing fallback §5 forbids); ownership-unknown REFUSES too, typed/located/counted. Ownership is extracted as its own single authority (`gunbc.ownership.Ownership`) and `live_deploy`'s `DeploymentStep` re-grounds onto it (pass 2, a declared dissolution trigger — never a second `Owned|Ensured`). Pass 1 (spine + R5 + a synthetic discriminating witness the degenerate apply/retract poles cannot exercise) landed. Identity is **declaration-owned and allocator-minted**, never derived from unit/path/content (operator ruling): `gunbc.host_resource` carries `HostResourceIdentity\{host, occurrence}` and `HostResource\{identity, role, value}`, where the occurrence is minted by an allocator, `role` is a **type parameter** (so a new role is an instantiation, never a widened central enum), and unit name / FIFO / storage path / configuration are mutable *value* fields. That is what makes a rename ONE `MemberChanged` rather than a delete-plus-create some key function must be clever enough to re-pair — git does not track renames, it INFERS them from content similarity, and §4 rules a heuristic never necessary in a closed system; a content-or-path-derived `key_of` is that same inference wearing a bundle. It is a carrier distinct from `std.occurrence_identity` deliberately: that module is specifically about SOURCE occurrences (its `OccurrenceCategory` enumerates callable/type/field/method, its allocator is coupled to `AuthoredTokenOrdinalSpace`), and sharing one `Int` space across two subjects would let `occurrence_id_eq` answer `true` on a numeric coincidence — the cross-family comparison the `ContentHash` family grounding closed. Extracting one subject-parameterized minted-identity carrier (the `Vendor` shape) is registered as a trigger, not built under a load-bearing module with stage0 work in flight. → [membership-diff reconcile spine design](docs/plans/membership-diff-reconcile-spine-design.md)"), li(text: "**one authorization kernel, several typed request profiles (operator directive 2026-08-01).** `std.access.AccessRequest` carries subject, action, object, typed context, and typed evidence; `AccessPolicy` is the sole policy-to-decision seam, `decision_meet` the sole conjunction, and every denial carries a typed cause at structured request coordinates. Effect, reference, publication admission, disclosure, and sealed execution are exact request products projected into that kernel, never independent allow/deny folds. Principals project external evidence — OIDC issuer/subject and observed POSIX effective principal — rather than being invented internal identities. The provisional gunbc#7541 `Verb::Reference` / `Verb::Publish` / `AudienceScopeTree` carriers dissolved: audiences are sets with join and partial-order subset, because real audiences can overlap without either containing the other. `PublicationAdmissionRequest` is only the generic request shape here: the operator-deleted Stage-0 placement wall, publisher policy, and pathname census are deliberately absent."), li(text: "**publication and reference-admission capabilities — carrier retirement, replacement ontology unresolved.** **Removal record (operator ruling 2026-08-01):** the Stage-0 `Publish`/`Reference` effect-grant experiment retired after its sole live publication consumer, the placement gate, was deleted. `Reference` and `Publish` were removed from `std.effect_grant.Verb`, `AudienceScopeTree` was removed, and `std.visibility_grant` plus its carrier-only witnesses were deleted; generic authorization admission re-homed onto the `std.access` kernel. This retires those carriers, not the underlying capabilities. Publication remains required, but no replacement ontology has been selected and any redesign requires operator review before implementation. Reference-edge admission — whether an edge may form within one compiled program — is a separate deferred capability awaiting a concrete consumer; the publication rollback decides nothing about it. **Stage 0 per-file placement gate DELETED:** its constant `Publish World` rows duplicated Git's post-cutover path population, four same-day repair rounds raced identical reconstructions and repeatedly redded fleet CI, ordinary modifications were invisible, and a CI check after a public push could protect merge integrity but not confidentiality because the objects had already reached public storage. New public files require no stamp. Any future confidentiality boundary must act before unauthorized bytes enter public storage — for example by withholding public-write capability from ordinary sessions — but that constraint selects no replacement architecture. The locked extension remains a **publication capability product, not a ladder**: source/interface disclosure, artifact delivery, local/remote execution, integrity, reproducibility, existence/churn disclosure, revocation/erase, and placement/trust are independent policy axes. An emitted artifact is not source disclosure but remains inspectable; client-held key means plaintext access, distinct from remote/attested key custody. Locked blobs use AEAD with subject/interface/version/audience/policy context bound as associated data plus confidentiality-and-integrity-preserving per-audience key wraps; wrong key/context/authentication is typed refusal. Per-statement holes remain refused; interface/realization is the cut; size padding and `Secret`/`Pii`→`SecretRef` construction constraints remain. Commitments never promise zero leakage: length, timing, interface shape, wrap count, access pattern, low-entropy guessing, and churn stay in a named threat model. Remote execution and SCM diagnostics obey information-flow/noninterference + explicit declassification; metering prices an oracle but does not secure it, and unauthorized audiences receive only a non-leaking diagnostic projection. Cryptographic erase is conditional on every key/wrap/backup/cache/derivative/recovery path being sanitized and the result validated, never “delete one key.” → [retired node/subtree carrier experiment](docs/plans/node-subtree-visibility-grants.md)"), li(text: "**effect grants over namespaces — dissolve `Hermetic | Wet` into (frame × verb × subtree).** The 2-valued `Hermetic | Wet` enum conflates four axes (input closure / replayability, output reach / interference, handler binding, selection eligibility) — a §3 state-space conflation with proto-envelopes already forked (the hand-rolled `workspace_root` containment gate, `std.resources.ResourceHandle`, `AuthScope`, `LiveTreeDisposition`). End shape (§3, cited not minted): an effect target is a position in a containment tree that already exists — filesystem paths, URIs, `/proc`, service-operation paths, and the unifying case **code names themselves** (the containment tree the namespace-resolution lane makes the single naming authority); permission is a grant of (verb × subtree) attached to a `Frame`; admissibility is the namespace prefix relation — the same `⊑` the resolver walks, content-addressing hashes, and termination reads, so effects become the **fourth consumer** of the one containment structure. Dispatch projects an `EffectRequest` through `std.access.AccessPolicy` fail-closed (`Deny` carries the typed/located/counted refusal, never a silent widen — §5); *replayable* / *isolated* / `LiveTreeDisposition` become **derived** projections, and `Hermetic | Wet | Record` survive only as named envelope presets, deleted at the end. Frame-containment is graded on the §5 construction/validation axis (`LifecycleByConstruction` vs `LifecycleByConvention`). No code lands from the design doc; the FLAG-A interim is the only near-term consumer. → [effect-namespace-grants design](docs/plans/effect-namespace-grants.md)"), diff --git a/dag/gunbc/host_axis_caps.dag b/dag/gunbc/host_axis_caps.dag index 6629e438481..05a5165b5e9 100644 --- a/dag/gunbc/host_axis_caps.dag +++ b/dag/gunbc/host_axis_caps.dag @@ -9,8 +9,8 @@ import gunbc.membership_reconcile { EffectsOrRefusal, EffectsReady, ApplyRefused, - membership_upsert_count, - membership_teardown_count, + membership_write_count, + membership_removal_count, membership_refusal_count, } import gunbc.host_converge { @@ -19,7 +19,7 @@ import gunbc.host_converge { gunbc_runner_per_slot_high_dropin_path, } -data host_axis_caps_note: String = "PerSlotMemoryCap axis, closed vertically on the membership_reconcile spine — the first non-degenerate reconcile in the repo (desired vs a real OBSERVED set, not observed=[]). A CapMember is a per-slot systemd drop-in keyed by its file path (stable IDENTITY, so a content drift is Modified->Upsert, never Remove+Add). The interference domain is the drop-in directory itself: ownership is DERIVED from the path (managed set -> Owned; anything else -> a foreign occupant, Ensured), never stored, so a Removed foreign file yields MemberTeardownRefused (R5, no effect arm, never deleted). Idempotence = zero hunks (Unchanged); perturb = Modified->Upsert of exactly the drifted row; foreign occupant = ApplyRefused wholesale. Live apply/observe are host_effect_apply typed transports (operator one-liners for the go-live receipts); this module is the pure, hermetically-witnessed fold." +data host_axis_caps_note: String = "PerSlotMemoryCap axis, closed vertically on the membership_reconcile spine — the first non-degenerate reconcile in the repo (desired vs a real OBSERVED set, not observed=[]). A CapMember is a per-slot systemd drop-in keyed by its file path (stable IDENTITY, so a content drift is Modified->MemberChanged, never Remove+Add). The interference domain is the drop-in directory itself: ownership is DERIVED from the path (managed set -> Owned; anything else -> a foreign occupant, Ensured), never stored, so a Removed foreign file yields MemberRemovalRefused (R5, no effect arm, never deleted). Idempotence = zero hunks (Unchanged); perturb = Modified->MemberChanged of exactly the drifted row; foreign occupant = ApplyRefused wholesale. Live apply/observe are host_effect_apply typed transports (operator one-liners for the go-live receipts); this module is the pure, hermetically-witnessed fold." type CapMember { dropin_path: NonEmptyStr @@ -90,11 +90,11 @@ fn caps_effects(desired: List, observed: List) -> EffectsO } fn caps_upsert_count(desired: List, observed: List) -> Int { - membership_upsert_count(plan: caps_reconcile(desired: desired, observed: observed)) + membership_write_count(plan: caps_reconcile(desired: desired, observed: observed)) } fn caps_teardown_count(desired: List, observed: List) -> Int { - membership_teardown_count(plan: caps_reconcile(desired: desired, observed: observed)) + membership_removal_count(plan: caps_reconcile(desired: desired, observed: observed)) } fn caps_refusal_count(desired: List, observed: List) -> Int { diff --git a/dag/gunbc/host_phase_status.dag b/dag/gunbc/host_phase_status.dag index 508e1cbd048..0853b86a885 100644 --- a/dag/gunbc/host_phase_status.dag +++ b/dag/gunbc/host_phase_status.dag @@ -21,11 +21,12 @@ import gunbc.host_standup_assimilation_deduction { srv3_post_install_actuation_v import gunbc.membership_reconcile { MembershipPlan, MemberAction, - MemberUpsert, - MemberTeardown, - MemberTeardownRefused, + MemberAdded, + MemberChanged, + MemberRemoved, + MemberRemovalRefused, membership_reconcile, - membership_upsert_count, + membership_write_count, } import gunbc.ownership { Ownership, Owned } import gunbc.fleet_intent_network { operator_host_srv1, operator_host_srv2, operator_host_srv3, operator_host_srv4 } @@ -193,7 +194,7 @@ fn host_phase_cell_ownership(c: HostPhaseCellStatus) -> Ownership? { Present { value: Owned } } -data host_phase_reconcile_instantiation_note: String = "The status matrix reconciled as a MEMBERSHIP DIFF — one more (key_of, key_eq, value_eq, ownership_of) bundle handed to the single generic gunbc.membership_reconcile.membership_reconcile, never a forked diff (a forked reconcile means the genericity bought nothing). Desired is every cell modeled AND observed Converged: that is the end state of the whole subsumption lane — every phase modeled AND every enrolled host converged on it — so a Modified hunk is precisely one unit of remaining work, and membership_upsert_count is the answer to 'how much is left' as a NUMBER rather than a prose reconstruction. Removed is a real arm, not a degenerate pole: a cell observed for a host no longer in fleet_intent is a host that left the fleet, and cells are Owned, so it tears down rather than refusing. The witness exercises that arm synthetically because the live fleet has no departed host today — an instantiation whose interesting hunks are all unreachable in practice is an instantiation nobody has actually tested." +data host_phase_reconcile_instantiation_note: String = "The status matrix reconciled as a MEMBERSHIP DIFF — one more (key_of, key_eq, value_eq, ownership_of) bundle handed to the single generic gunbc.membership_reconcile.membership_reconcile, never a forked diff (a forked reconcile means the genericity bought nothing). Desired is every cell modeled AND observed Converged: that is the end state of the whole subsumption lane — every phase modeled AND every enrolled host converged on it — so a Modified hunk is precisely one unit of remaining work, and membership_write_count is the answer to 'how much is left' as a NUMBER rather than a prose reconstruction. Removed is a real arm, not a degenerate pole: a cell observed for a host no longer in fleet_intent is a host that left the fleet, and cells are Owned, so it tears down rather than refusing. The witness exercises that arm synthetically because the live fleet has no departed host today — an instantiation whose interesting hunks are all unreachable in practice is an instantiation nobody has actually tested." fn host_phase_desired(enrollments: List) -> List { map( @@ -242,7 +243,7 @@ fn host_phase_fleet_reconcile(enrollments: List) -> Member } fn host_phase_remaining_work_count(enrollments: List) -> Int { - membership_upsert_count(plan: host_phase_fleet_reconcile(enrollments: enrollments)) + membership_write_count(plan: host_phase_fleet_reconcile(enrollments: enrollments)) } fn host_phase_observation_coverage_count(enrollments: List) -> Int { diff --git a/dag/gunbc/host_resource.dag b/dag/gunbc/host_resource.dag new file mode 100644 index 00000000000..da71b0699ca --- /dev/null +++ b/dag/gunbc/host_resource.dag @@ -0,0 +1,67 @@ +module gunbc.host_resource + +import std.types { String, Int, Bool } +import product.placement_supply { HostIdentity } + +data resource_occurrence_subject_decision_note: String = "WHY THIS IS A DISTINCT CARRIER AND NOT std.occurrence_identity (DESIGN §3, decided by reading rather than by assumption). std.occurrence_identity is specifically about SOURCE occurrences: its OccurrenceCategory enumerates CallableOccurrence/TypeOccurrence/ConstructorOccurrence/FieldOccurrence/MethodOccurrence/NamespaceSegmentOccurrence/LexicalValueOccurrence, its carriers are DeclarationOccurrence/ReferenceOccurrence over OccurrenceContainmentPath, and its allocator is coupled through occurrence_id_allocator_advance_to to AuthoredTokenOrdinalSpace — the authored-source token ordering that gates ModuleExposure. A host resource has no authored token ordinal and no containment path, so a fleet allocator sharing that surface would inherit a watermark constraint that means nothing for it. The subject-agnostic residue in that module is only a monotone Int counter, and sharing ONE Int space across two unrelated subjects is not single authority — it is the cross-family comparison DESIGN closed for ContentHash: occurrence_id_eq would answer true on a numeric coincidence between a host resource and a source occurrence, which is exactly the state-space conflation the family grounding row forbids. So a distinct carrier is correct here. The genuinely shared concept — an opaque, allocator-minted identity in a NAMED subject space, never derived from content — is real but not yet extracted; see resource_occurrence_generalization_trigger." + +data minted_not_derived_note: String = "Identity is MINTED BY THE DECLARATION, never derived from content, path, or unit name (operator ruling). This is the whole point: a derived key makes a rename indistinguishable from a delete-plus-create unless some key function is clever enough to notice the two are the same thing — which is inference, and DESIGN §4 rules a heuristic never necessary in a closed system. Git does not track renames; it INFERS them from content similarity after the fact, and that inference is precisely what a content-or-path-derived key_of reproduces. Minting the occurrence at declaration time closes it: the occurrence is stable across every value change, so a rename is ONE MemberChanged whose from and to share an identity, and nothing has to be guessed. A consequence worth stating because it is easy to lose: the identity is NOT the role and NOT the address — role is a separate typed field, and unit name, FIFO path, storage path and configuration are all mutable VALUE fields that may change under a fixed identity." + +type ResourceOccurrenceId { + value: Int +} + +type ResourceOccurrenceAllocator { + next_id: Int +} + +type ResourceOccurrenceAllocResult { + id: ResourceOccurrenceId + alloc: ResourceOccurrenceAllocator +} + +fn resource_occurrence_allocator_initial() -> ResourceOccurrenceAllocator { + ResourceOccurrenceAllocator { next_id: 0 } +} + +fn alloc_resource_occurrence(alloc: ResourceOccurrenceAllocator) -> ResourceOccurrenceAllocResult { + ResourceOccurrenceAllocResult { + id: ResourceOccurrenceId { value: alloc.next_id }, + alloc: ResourceOccurrenceAllocator { next_id: alloc.next_id + 1 }, + } +} + +fn resource_occurrence_eq(left: ResourceOccurrenceId, right: ResourceOccurrenceId) -> Bool { + left.value == right.value +} + +type HostResourceIdentity { + host: HostIdentity + occurrence: ResourceOccurrenceId +} + +fn host_resource_identity_eq(left: HostResourceIdentity, right: HostResourceIdentity) -> Bool { + (left.host as String) == (right.host as String) + && resource_occurrence_eq(left: left.occurrence, right: right.occurrence) +} + +data host_resource_role_parameter_note: String = "role is a TYPE PARAMETER R, not a closed HostRole enum (operator ruling: 'not a closed operator-maintained HostRole enum'). Jobserver, BuildCache and RunnerSlot are typed roles supplied by whichever module owns them, so a new role is a new instantiation rather than an edit to a central coproduct — the same rule DESIGN §3 states for browser products ('adding Opera must not widen a generic browser-product enum'). A central enum would also make the role list an operator maintenance duty, which is the governance redundancy §2 prices." + +type HostResource { + identity: HostResourceIdentity + role: R + value: V +} + +fn host_resource_identity_of(resource: HostResource) -> HostResourceIdentity { + resource.identity +} + +fn host_resource_same_occurrence( + left: HostResource, + right: HostResource, +) -> Bool { + host_resource_identity_eq(left: left.identity, right: right.identity) +} + +data resource_occurrence_generalization_trigger: String = "OPEN, deliberately not built here: the shared concept behind ResourceOccurrenceId and std.occurrence_identity's OccurrenceId is 'an opaque allocator-minted identity in a named subject space'. Extracting it as one subject-parameterized carrier (the Vendor move — one concept, the subject as a type argument) is the §2-horizontal answer and would make cross-subject comparison unwritable rather than merely unlikely. It is NOT done in this change because std.occurrence_identity is load-bearing compiler substrate with staged work in flight (the stage0 roster and ContainmentPath projection), so migrating it under a fleet-membership brief would be exactly the improvising past doubt the working agreement forbids. DISSOLVE-ON: a THIRD minted-identity subject appears, or the std.occurrence_identity stage0 projection settles — whichever comes first; at that point extract the parameterized carrier and re-ground both subjects on it." diff --git a/dag/gunbc/live_deploy/emit.dag b/dag/gunbc/live_deploy/emit.dag index c01228cfddd..953a63d1379 100644 --- a/dag/gunbc/live_deploy/emit.dag +++ b/dag/gunbc/live_deploy/emit.dag @@ -50,7 +50,7 @@ import gunbc.ownership { Ownership } import v2.std.algebra { list_tail, TailFound, TailAbsent } import gunbc.membership_reconcile { MembershipPlan, - MemberEffect, EffectUpsert, EffectTeardown, + MemberEffect, EffectAdd, EffectReplace, EffectRemove, MemberRefusal, EffectsOrRefusal, EffectsReady, ApplyRefused, membership_reconcile, membership_effects, @@ -535,9 +535,15 @@ fn emit_artifact_teardown(art: DeploymentArtifactStep, spec: DeploymentSpec) -> } } -data emit_deploy_member_effect_note: String = "The per-member realization HANDLER: share the DIFF (membership_reconcile), dispatch the APPLY (this). One handler for both fold directions — EffectUpsert dispatches on member kind to the artifact/dependency install fragments; EffectTeardown to the removal fragments. Orchestration is DERIVED from the effect kind, not an always-on envelope: a SystemdUnit upsert carries its own daemon-reload/enable/restart (once, part of the unit's realization); ServerScript carries the /opt/gunbc install -d it writes into. MemberEffect is a bidirectional sum, so each POLE has one structurally-unreachable direction (apply never Teardown, retract never Upsert) — those ARE reached across the two poles combined. The ONE arm unreachable across BOTH poles is EffectTeardown of a Dependency: a dependency is Ensured, so a Removed dependency is MemberTeardownRefused, never an EffectTeardown. That arm REFUSES loudly (emit_deploy_teardown_dependency_refusal — a typed/located poison step), it does NOT fabricate a no-op (DESIGN §5: an unreachable arm refuses, never a silent pass)." +data emit_deploy_member_effect_note: String = "The per-member realization HANDLER: share the DIFF (membership_reconcile), dispatch the APPLY (this). One handler for both fold directions — EffectAdd dispatches on member kind to the artifact/dependency install fragments; EffectRemove to the removal fragments. Orchestration is DERIVED from the effect kind, not an always-on envelope: a SystemdUnit upsert carries its own daemon-reload/enable/restart (once, part of the unit's realization); ServerScript carries the /opt/gunbc install -d it writes into. MemberEffect is a bidirectional sum, so each POLE has one structurally-unreachable direction (apply never Remove, retract never Add) — those ARE reached across the two poles combined. TWO arms are unreachable across BOTH poles. EffectRemove of a Dependency: a dependency is Ensured, so a Removed dependency is MemberRemovalRefused, never an EffectRemove. And EffectReplace in either direction: both poles are DEGENERATE (apply observes nothing, retract desires nothing), so neither can produce a Modified hunk at all — a replace here would mean a pole stopped being degenerate, which is a real observed-provider arriving and needs its staged-replacement intermediates declared (gunbc.change_realization) before it may emit anything. That arm REFUSES loudly (emit_deploy_teardown_dependency_refusal — a typed/located poison step), it does NOT fabricate a no-op (DESIGN §5: an unreachable arm refuses, never a silent pass)." -data live_deploy_teardown_dependency_unreachable_poison: String = "__GUNBC_DEPLOY_UNREACHABLE__ R5 wall breach — EffectTeardown of an Ensured dependency reached the emit dispatch. A dependency is Ensured, so a Removed dependency is MemberTeardownRefused (never an EffectTeardown); reaching this arm means deployment_step_ownership or membership_effects is broken. This marker is not valid deploy shell, so the golden drift gate reds — DESIGN §5: an unreachable arm REFUSES loudly (typed/located/counted), never fabricates a no-op. dependency=" +data live_deploy_replace_unreachable_poison: String = "__GUNBC_DEPLOY_UNREACHABLE__ EffectReplace reached the deploy emit dispatch. Both deploy poles are degenerate — apply observes the empty set, retract desires the empty set — so no Modified hunk can arise and no replace can be emitted. Reaching this arm means a NON-degenerate observed provider landed without its realization being modeled: a replace on a host resource is an in-place update only if the address survived, and a STAGED replacement with declared intermediates otherwise (gunbc.change_realization). Emitting an unconditional overwrite here would be the srv4 failure exactly — a transition that believed it had nothing to retire. This marker is not valid deploy shell, so the golden drift gate reds. member=" + +fn emit_deploy_replace_unreachable_refusal(step: DeploymentStep) -> List { + [deploy_raw(command: concat(live_deploy_replace_unreachable_poison, deployment_step_key(step: step) as String))] +} + +data live_deploy_teardown_dependency_unreachable_poison: String = "__GUNBC_DEPLOY_UNREACHABLE__ R5 wall breach — EffectRemove of an Ensured dependency reached the emit dispatch. A dependency is Ensured, so a Removed dependency is MemberRemovalRefused (never an EffectRemove); reaching this arm means deployment_step_ownership or membership_effects is broken. This marker is not valid deploy shell, so the golden drift gate reds — DESIGN §5: an unreachable arm REFUSES loudly (typed/located/counted), never fabricates a no-op. dependency=" fn emit_deploy_teardown_dependency_refusal(dep: DeploymentDependencyStep) -> List { [deploy_raw(command: concat(live_deploy_teardown_dependency_unreachable_poison, dep.package))] @@ -545,14 +551,15 @@ fn emit_deploy_teardown_dependency_refusal(dep: DeploymentDependencyStep) -> Lis fn emit_deploy_member_effect(effect: MemberEffect, spec: DeploymentSpec) -> List { match effect { - EffectUpsert { member: step } => + EffectAdd { to: step } => match step { Dependency { step: dep } => [ ensure_apt_package_step(pkg: dep.package, privileged: true), ] ArtifactStep { step: art } => emit_artifact_upsert(art: art, spec: spec) } - EffectTeardown { member: step } => + EffectReplace { from: _, to: step } => emit_deploy_replace_unreachable_refusal(step: step) + EffectRemove { from: step } => match step { ArtifactStep { step: art } => emit_artifact_teardown(art: art, spec: spec) Dependency { step: dep } => emit_deploy_teardown_dependency_refusal(dep: dep) diff --git a/dag/gunbc/membership_reconcile.dag b/dag/gunbc/membership_reconcile.dag index d7e73ecffb8..dbcd8975592 100644 --- a/dag/gunbc/membership_reconcile.dag +++ b/dag/gunbc/membership_reconcile.dag @@ -14,17 +14,19 @@ import std.decl_ref { DeclarationRef, WholeDeclaration } type TeardownRefusalCause = MemberNotOwned | OwnershipUnknown type MemberAction - = MemberUpsert { member: M } - | MemberTeardown { member: M } - | MemberTeardownRefused { member: M, cause: TeardownRefusalCause } + = MemberAdded { to: M } + | MemberChanged { from: M, to: M } + | MemberRemoved { from: M } + | MemberRemovalRefused { from: M, cause: TeardownRefusalCause } type MembershipPlan { actions: List> } type MemberEffect - = EffectUpsert { member: M } - | EffectTeardown { member: M } + = EffectAdd { to: M } + | EffectReplace { from: M, to: M } + | EffectRemove { from: M } type MemberRefusal { member: M @@ -35,24 +37,37 @@ type EffectsOrRefusal = EffectsReady { effects: List> } | ApplyRefused { refusals: List> } -data membership_reconcile_authority_note: String = "THE grain-agnostic membership-diff reconcile (R2/R3/R5/R9). Desired set vs observed set keyed by member identity: Added/Modified -> upsert, Removed -> teardown (owned-only) or refuse, Unchanged -> noop (absence of a hunk). Generic over member type M and key K: a member may be a service/unit/host OR a Session — consumers CALL this with their (key_of, key_eq, value_eq, ownership_of) bundle, they NEVER copy-adapt it (one fn, N bundles — a Realization; a forked reconcile means the genericity bought nothing). Reuses std.change.keyed_two_way_diff (the single already-generic diff engine) — no fork. R5 teardown-owned-only is a CONSTRUCTION WALL: a Removed non-owned member yields MemberTeardownRefused, which has NO effect arm in any apply dispatch, so the bad state is unwritable — never a post-check, never 'assume owned' (the absorbing fallback DESIGN §5 forbids). key_of MUST return stable IDENTITY (not content) so a content drift is Modified (re-upsert), not Remove+Add (teardown+reinstall); value_eq is presence+content so a same-key content drift re-upserts." +data membership_reconcile_authority_note: String = "THE grain-agnostic membership-diff reconcile (R2/R3/R5/R9). Desired set vs observed set keyed by member identity: Added -> add, Modified -> change, Removed -> remove (owned-only) or refuse, Unchanged -> noop (absence of a hunk). Add and change are DISTINCT arms and are NOT collapsed into one 'upsert': an add creates where nothing was, a change carries BOTH sides of a surviving occurrence. Only REMOVAL consults ownership, and that asymmetry is deliberate rather than an oversight — gunbc.ownership defines Ensured as 'requires present but does NOT own (never torn down)', a constraint on removal specifically. Converging a drifted member the model does not own is the intended behavior of an Ensured member, not a violation of it: tool_readiness exists precisely to re-install a pin whose observed version drifted from desired, and refusing that would break the module rather than protect anything. Generic over member type M and key K: a member may be a service/unit/host OR a Session — consumers CALL this with their (key_of, key_eq, value_eq, ownership_of) bundle, they NEVER copy-adapt it (one fn, N bundles — a Realization; a forked reconcile means the genericity bought nothing). Reuses std.change.keyed_two_way_diff (the single already-generic diff engine) — no fork. R5 removal-owned-only is a CONSTRUCTION WALL: a Removed non-owned member yields MemberRemovalRefused, which has NO effect arm in any apply dispatch, so the bad state is unwritable — never a post-check, never 'assume owned' (the absorbing fallback DESIGN §5 forbids). key_of MUST return stable IDENTITY (not content) so a content drift is Modified (one change), not Remove+Add (teardown+reinstall)." fn member_rows(members: List, key_of: fn(M) -> K) -> List> { map(members, m => KeyedRow { row_key: key_of(m), value: m }) } +data member_changed_both_sides_note: String = "WHY MemberChanged carries `from` as well as `to`. The prior shape collapsed a Modified hunk into an upsert of the `to` side and DISCARDED `from`, which is lossy in a load-bearing way rather than merely untidy: the prior value is what every safe realization of a change needs. An SCM ref update is a compare-and-swap that names the expected prior (git update-ref ), so without `from` the only reachable realization is the unconditional write and the atomicity the capability already offers cannot be used. A host resource whose address moved must retire the prior endpoint, and `from` is the only place that endpoint survives. gunbc.change_realization is the table that consumes both sides. A NOTE ON WHAT THIS IS NOT: an earlier draft of this change also refused a Modified hunk whose `from` was not Owned, on the reading that replacement is destruction. That was withdrawn — it over-fires on every Ensured consumer and contradicts gunbc.ownership, where Ensured constrains teardown only. Ownership gates removal; it does not gate convergence." + +type RemovalAdmission + = RemovalAdmitted + | RemovalRefused { cause: TeardownRefusalCause } + +fn removal_admission(existing: M, ownership_of: fn(M) -> Ownership?) -> RemovalAdmission { + match ownership_of(existing) { + Present { value: own } => + match own { + Owned => RemovalAdmitted + Ensured => RemovalRefused { cause: MemberNotOwned } + } + Absent => RemovalRefused { cause: OwnershipUnknown } + } +} + fn hunk_to_action(hunk: KeyedDiffHunk, ownership_of: fn(M) -> Ownership?) -> MemberAction { match hunk { - KeyedDiffAddedHunk { hunk_key: _, to: m } => MemberUpsert { member: m } - KeyedDiffModifiedHunk { hunk_key: _, from: _, to: m } => MemberUpsert { member: m } + KeyedDiffAddedHunk { hunk_key: _, to: m } => MemberAdded { to: m } + KeyedDiffModifiedHunk { hunk_key: _, from: f, to: t } => MemberChanged { from: f, to: t } KeyedDiffRemovedHunk { hunk_key: _, from: m } => - match ownership_of(m) { - Present { value: own } => - match own { - Owned => MemberTeardown { member: m } - Ensured => MemberTeardownRefused { member: m, cause: MemberNotOwned } - } - Absent => MemberTeardownRefused { member: m, cause: OwnershipUnknown } + match removal_admission(existing: m, ownership_of: ownership_of) { + RemovalAdmitted => MemberRemoved { from: m } + RemovalRefused { cause: c } => MemberRemovalRefused { from: m, cause: c } } } } @@ -76,14 +91,15 @@ fn membership_reconcile( } } -data membership_effects_note: String = "The APPLY-grain projection of a plan: partitions a MembershipPlan into effects (upsert/teardown) OR a wholesale refusal. EffectsOrRefusal is a SUM, not a product: the ApplyRefused arm carries NO effects, so a plan with any refusal is UN-EMITTABLE — a consumer can obtain a List only from the EffectsReady arm, making drop-and-proceed (emit the effects, ignore the refusals) unrepresentable, not merely discouraged (DESIGN §5 construction-over-validation). Refused is PRESERVED and surfaced as MemberRefusal (member+cause: typed+located+counted), never dropped — the spine keeps producing it (plan grain), the apply grain refuses wholesale on it. flat_map (not a concat-in-fold) builds each list in one pass — no accumulator-copy. See membership_effects_wholesale_refuse_policy_trigger for the deliberate scope-dependent policy." +data membership_effects_note: String = "The APPLY-grain projection of a plan: partitions a MembershipPlan into effects (add/replace/remove) OR a wholesale refusal. EffectReplace carries BOTH sides because an apply handler that replaces a member must be able to retire the prior realization, not merely write the new one over it; an EffectAdd carries one side because there is nothing there to retire. EffectsOrRefusal is a SUM, not a product: the ApplyRefused arm carries NO effects, so a plan with any refusal is UN-EMITTABLE — a consumer can obtain a List only from the EffectsReady arm, making drop-and-proceed (emit the effects, ignore the refusals) unrepresentable, not merely discouraged (DESIGN §5 construction-over-validation). Refused is PRESERVED and surfaced as MemberRefusal (member+cause: typed+located+counted), never dropped — the spine keeps producing it (plan grain), the apply grain refuses wholesale on it. flat_map (not a concat-in-fold) builds each list in one pass — no accumulator-copy. See membership_effects_wholesale_refuse_policy_trigger for the deliberate scope-dependent policy." fn membership_effects(plan: MembershipPlan) -> EffectsOrRefusal { let refusals = flat_map(plan.actions, a => match a { - MemberTeardownRefused { member: m, cause: c } => [MemberRefusal { member: m, cause: c }] - MemberUpsert { member: _ } => [] - MemberTeardown { member: _ } => [] + MemberRemovalRefused { from: m, cause: c } => [MemberRefusal { member: m, cause: c }] + MemberAdded { to: _ } => [] + MemberChanged { from: _, to: _ } => [] + MemberRemoved { from: _ } => [] } ) if count(refusals) > 0 { @@ -92,9 +108,10 @@ fn membership_effects(plan: MembershipPlan) -> EffectsOrRefusal { EffectsReady { effects: flat_map(plan.actions, a => match a { - MemberUpsert { member: m } => [EffectUpsert { member: m }] - MemberTeardown { member: m } => [EffectTeardown { member: m }] - MemberTeardownRefused { member: _, cause: _ } => [] + MemberAdded { to: m } => [EffectAdd { to: m }] + MemberChanged { from: f, to: t } => [EffectReplace { from: f, to: t }] + MemberRemoved { from: m } => [EffectRemove { from: m }] + MemberRemovalRefused { from: _, cause: _ } => [] } ) } @@ -102,32 +119,46 @@ fn membership_effects(plan: MembershipPlan) -> EffectsOrRefusal { } type MembershipTally { - upserts: Int - teardowns: Int + adds: Int + changes: Int + removals: Int refusals: Int } -data membership_tally_note: String = "The counts-monoid of a plan (zero = all-zero, combine = componentwise +). ONE catamorphism over the actions computes all three counts in a single pass; the membership_upsert/teardown/refusal_count fns are its projections (was three separate folds — DESIGN §2 one-concept, the elegant fold the diff is). The accumulator is a fixed-size record (O(1)/step), not a growing list, so no copy cost." +data membership_tally_note: String = "The counts-monoid of a plan (zero = all-zero, combine = componentwise +). ONE catamorphism over the actions computes all four counts in a single pass; the membership_added/change/removal/refusal_count fns are its projections (was three separate folds — DESIGN §2 one-concept, the elegant fold the diff is). The accumulator is a fixed-size record (O(1)/step), not a growing list, so no copy cost." fn membership_tally(plan: MembershipPlan) -> MembershipTally { - fold(plan.actions, init: MembershipTally { upserts: 0, teardowns: 0, refusals: 0 }, f: (acc, a) => + fold(plan.actions, init: MembershipTally { adds: 0, changes: 0, removals: 0, refusals: 0 }, f: (acc, a) => match a { - MemberUpsert { member: _ } => - MembershipTally { upserts: acc.upserts + 1, teardowns: acc.teardowns, refusals: acc.refusals } - MemberTeardown { member: _ } => - MembershipTally { upserts: acc.upserts, teardowns: acc.teardowns + 1, refusals: acc.refusals } - MemberTeardownRefused { member: _, cause: _ } => - MembershipTally { upserts: acc.upserts, teardowns: acc.teardowns, refusals: acc.refusals + 1 } + MemberAdded { to: _ } => + MembershipTally { adds: acc.adds + 1, changes: acc.changes, removals: acc.removals, refusals: acc.refusals } + MemberChanged { from: _, to: _ } => + MembershipTally { adds: acc.adds, changes: acc.changes + 1, removals: acc.removals, refusals: acc.refusals } + MemberRemoved { from: _ } => + MembershipTally { adds: acc.adds, changes: acc.changes, removals: acc.removals + 1, refusals: acc.refusals } + MemberRemovalRefused { from: _, cause: _ } => + MembershipTally { adds: acc.adds, changes: acc.changes, removals: acc.removals, refusals: acc.refusals + 1 } } ) } -fn membership_upsert_count(plan: MembershipPlan) -> Int { - membership_tally(plan: plan).upserts +fn membership_added_count(plan: MembershipPlan) -> Int { + membership_tally(plan: plan).adds +} + +fn membership_change_count(plan: MembershipPlan) -> Int { + membership_tally(plan: plan).changes +} + +data membership_write_count_note: String = "adds + changes — the count of members this plan will WRITE, which is what the former membership_upsert_count actually answered for its consumers ('how much work is left'). It is kept as a DERIVED projection over the two separate tally fields, never as a stored merged counter: an add and a change have different realizations (gunbc.change_realization), so a single stored 'upserts' number is the conflation this change removed and re-storing it would reinstate it. A consumer that genuinely cares which kind of write it is reads adds and changes directly." + +fn membership_write_count(plan: MembershipPlan) -> Int { + let t = membership_tally(plan: plan) + t.adds + t.changes } -fn membership_teardown_count(plan: MembershipPlan) -> Int { - membership_tally(plan: plan).teardowns +fn membership_removal_count(plan: MembershipPlan) -> Int { + membership_tally(plan: plan).removals } fn membership_refusal_count(plan: MembershipPlan) -> Int { diff --git a/dag/gunbc/non_fold_residue.dag b/dag/gunbc/non_fold_residue.dag index 0ed96a81918..47b747fc4d6 100644 --- a/dag/gunbc/non_fold_residue.dag +++ b/dag/gunbc/non_fold_residue.dag @@ -798,7 +798,7 @@ data non_fold_residue_frontier: List = [ FrontierRow { subject: PathSubject { path: "dag/gunbc/repo_local_git_config.dag::apply_repo_local_git_config_action_at_repo" }, reason: nfr_reason_legacy_slice1_bridge, - trigger: TriggerProse { text: "DISSOLVE-ON: membership apply dispatch derives off-variant noop from MemberAction inhabitance (MemberTeardown/MemberTeardownRefused are construction-unreachable for Ensured bindings) and the wildcard arm deletes with the row" }, + trigger: TriggerProse { text: "DISSOLVE-ON: membership apply dispatch derives off-variant noop from MemberAction inhabitance (MemberRemoved/MemberRemovalRefused are construction-unreachable for Ensured bindings) and the wildcard arm deletes with the row" }, }, FrontierRow { subject: PathSubject { path: "dag/gunbc/ci_materialization.dag::warm_without_provider_receipt" }, diff --git a/dag/gunbc/plans/host_convergence_circuit_residue.dag b/dag/gunbc/plans/host_convergence_circuit_residue.dag index 2ebb9b9f931..34127192925 100644 --- a/dag/gunbc/plans/host_convergence_circuit_residue.dag +++ b/dag/gunbc/plans/host_convergence_circuit_residue.dag @@ -24,7 +24,7 @@ fn hccr_done() -> List { h3(text: "P1 core — PerSlotMemoryCap axis on the membership_reconcile spine (4 receipts, GREEN)"), ul(items: [ li(text: "dag/gunbc/host_axis_caps.dag: the first NON-DEGENERATE membership_reconcile in the repo (desired vs a real observed set, not observed=[]). One spine instantiation with a (key_of, key_eq, value_eq, ownership_of) bundle; ownership DERIVED from the drop-in path (managed -> Owned, foreign -> Ensured), never stored."), - li(text: "Interference domain = the drop-in directory, realized through the SAME spine: a foreign occupant is Removed + not-owned -> MemberTeardownRefused (R5, no effect arm, never deleted) -> ApplyRefused wholesale."), + li(text: "Interference domain = the drop-in directory, realized through the SAME spine: a foreign occupant is Removed + not-owned -> MemberRemovalRefused (R5, no effect arm, never deleted) -> ApplyRefused wholesale."), li(text: "Four hermetic receipts, each with a RED control, all GREEN, auto-discovered as a CI corpus consumer (not inert): idempotence (zero effects), perturb-and-heal (exactly the drifted row Upsert), foreign occupant (ApplyRefused + zero teardowns; RED = an owned removed file DOES teardown), derived content ([Service]/property/bytes derived, no hand strings)."), ]), h3(text: "P1a — interpreter closed + realize executes for real (loop closed at the live entry)"), diff --git a/dag/gunbc/repo_local_git_config.dag b/dag/gunbc/repo_local_git_config.dag index 451ddcc143d..2fbd54bdbb9 100644 --- a/dag/gunbc/repo_local_git_config.dag +++ b/dag/gunbc/repo_local_git_config.dag @@ -5,10 +5,11 @@ import std.types { FilePath } import gunbc.membership_reconcile { MembershipPlan, MemberAction, - MemberUpsert, + MemberAdded, + MemberChanged, membership_reconcile, - membership_upsert_count, - membership_teardown_count, + membership_write_count, + membership_removal_count, membership_refusal_count, } import gunbc.ownership { Ownership, Ensured } @@ -112,11 +113,11 @@ fn observed_binding(key: String, value: String) -> RepoLocalGitConfigBinding { } fn repo_local_git_config_converged(observed: List) -> Bool { - membership_upsert_count(plan: repo_local_git_config_reconcile( + membership_write_count(plan: repo_local_git_config_reconcile( desired: desired_repo_local_git_config_bindings(), observed: observed, )) == 0 - && membership_teardown_count(plan: repo_local_git_config_reconcile( + && membership_removal_count(plan: repo_local_git_config_reconcile( desired: desired_repo_local_git_config_bindings(), observed: observed, )) == 0 @@ -161,25 +162,34 @@ fn apply_repo_local_git_config_action_at_repo( acc } else { match action { - MemberUpsert { member: binding } => { - let result = git.Core.ConfigLocalSetInRepo(repo: repo, key: binding.key, value: binding.value) - if result.success { - acc - } else { - RepoLocalGitConfigApplyReceipt { - all_success: false, - first_failure: concat( - concat("git config --local set failed for ", binding.key), - concat(": ", result.stderr), - ), - } - } - } + MemberAdded { to: binding } => apply_repo_local_git_config_binding(repo: repo, binding: binding, acc: acc) + MemberChanged { from: _, to: binding } => apply_repo_local_git_config_binding(repo: repo, binding: binding, acc: acc) _ => acc } } } +data repo_local_git_config_write_arm_note: String = "MemberAdded and MemberChanged BOTH write, through this one fn. The arms are listed separately rather than left to the wildcard on purpose: the wildcard exists for the construction-unreachable removal arms (bindings are Ensured, so MemberRemoved/MemberRemovalRefused cannot arise — see gunbc.non_fold_residue), and a MemberChanged silently falling into it would drop exactly the drift this module exists to converge. A binding whose observed value drifted from desired is a Modified hunk, and re-setting it IS the module's job." + +fn apply_repo_local_git_config_binding( + repo: FilePath, + binding: RepoLocalGitConfigBinding, + acc: RepoLocalGitConfigApplyReceipt, +) -> RepoLocalGitConfigApplyReceipt { + let result = git.Core.ConfigLocalSetInRepo(repo: repo, key: binding.key, value: binding.value) + if result.success { + acc + } else { + RepoLocalGitConfigApplyReceipt { + all_success: false, + first_failure: concat( + concat("git config --local set failed for ", binding.key), + concat(": ", result.stderr), + ), + } + } +} + fn apply_repo_local_git_config_plan_at_repo( repo: FilePath, plan: MembershipPlan, @@ -206,8 +216,8 @@ fn repo_local_git_config_converge_actuate_at( applied: desired, } } else { - let upserts = membership_upsert_count(plan: plan) - let applied = if upserts > 0 { + let writes = membership_write_count(plan: plan) + let applied = if writes > 0 { apply_repo_local_git_config_plan_at_repo(repo: repo, plan: plan) } else { RepoLocalGitConfigApplyReceipt { all_success: true, first_failure: "" } @@ -219,7 +229,7 @@ fn repo_local_git_config_converge_actuate_at( if repo_local_git_config_converged(observed: observed_after) { Converged { evidence: RepoLocalGitConfigConvergedEvidence { - upserts_applied: upserts, + upserts_applied: writes, observed_bindings: observed_after, }, applied: observed_after, diff --git a/dag/gunbc/roadmap_belt.dag b/dag/gunbc/roadmap_belt.dag index 0a179181977..8778f031a81 100644 --- a/dag/gunbc/roadmap_belt.dag +++ b/dag/gunbc/roadmap_belt.dag @@ -11,7 +11,7 @@ import gunbc.roadmap_authority { } import gunbc.membership_reconcile { MembershipPlan, MemberAction, - MemberUpsert, MemberTeardown, MemberTeardownRefused, + MemberAdded, MemberChanged, MemberRemoved, MemberRemovalRefused, membership_reconcile, } import gunbc.ownership { Ownership, Owned } @@ -191,7 +191,7 @@ fn roadmap_belt_status_json() -> String { } } -data belt_reconcile_authority_note: String = "R9 session-grain binding: the belt IS gunbc.membership_reconcile at member-type = dispatch Session. Desired = frontier.ready roadmap nodes; observed = dispatch_live_sessions (belt-owned by construction — the gunbc-dispatch- prefix filter + node-id keying, so a foreign tmux session has no node-id key, is not a member, and never enters Removed). Added -> spawn, Removed(owned) -> reap, Unchanged -> noop, Paused -> no actions, capacity caps upserts. This SUBSUMES belt_step (spawn-only, observed hardcoded empty): belt_step is the degenerate slice-1 precursor and retires when the host-effect driver (slice 2b: MemberUpsert -> dispatch_spawn_commands, MemberTeardown -> tmux_kill_session_argv) consumes belt_reconcile as the sole belt decision. The belt is a CONTINUOUS reconciler => SIBLINGS-CONTINUE (product/plan grain: emit doable spawns+reaps, count+surface refusals), NOT the deploy's atomic wholesale-refuse. It reuses the spine UNCHANGED (zero spine edit) — the grain-agnosticism proof (DESIGN §2 Realization / R9)." +data belt_reconcile_authority_note: String = "R9 session-grain binding: the belt IS gunbc.membership_reconcile at member-type = dispatch Session. Desired = frontier.ready roadmap nodes; observed = dispatch_live_sessions (belt-owned by construction — the gunbc-dispatch- prefix filter + node-id keying, so a foreign tmux session has no node-id key, is not a member, and never enters Removed). Added -> spawn, Removed(owned) -> reap, Unchanged -> noop, Paused -> no actions, capacity caps upserts. This SUBSUMES belt_step (spawn-only, observed hardcoded empty): belt_step is the degenerate slice-1 precursor and retires when the host-effect driver (slice 2b: MemberAdded/MemberChanged -> dispatch_spawn_commands, MemberRemoved -> tmux_kill_session_argv) consumes belt_reconcile as the sole belt decision. The belt is a CONTINUOUS reconciler => SIBLINGS-CONTINUE (product/plan grain: emit doable spawns+reaps, count+surface refusals), NOT the deploy's atomic wholesale-refuse. It reuses the spine UNCHANGED (zero spine edit) — the grain-agnosticism proof (DESIGN §2 Realization / R9)." type DispatchMember = DesiredMember { node_id: String, node: RoadmapNode } @@ -255,9 +255,10 @@ fn belt_membership_plan( fn belt_plan_upserts(plan: MembershipPlan) -> List { fold(plan.actions, init: [], f: fn(acc, a) { match a { - MemberUpsert { member } => concat(acc, [member]) - MemberTeardown { member: _ } => acc - MemberTeardownRefused { member: _, cause: _ } => acc + MemberAdded { to: member } => concat(acc, [member]) + MemberChanged { from: _, to: member } => concat(acc, [member]) + MemberRemoved { from: _ } => acc + MemberRemovalRefused { from: _, cause: _ } => acc } }) } @@ -265,18 +266,20 @@ fn belt_plan_upserts(plan: MembershipPlan) -> List) -> List { fold(plan.actions, init: [], f: fn(acc, a) { match a { - MemberTeardown { member } => concat(acc, [member]) - MemberUpsert { member: _ } => acc - MemberTeardownRefused { member: _, cause: _ } => acc + MemberRemoved { from: member } => concat(acc, [member]) + MemberAdded { to: _ } => acc + MemberChanged { from: _, to: _ } => acc + MemberRemovalRefused { from: _, cause: _ } => acc } }) } fn belt_plan_refusals(plan: MembershipPlan) -> List> { plan.actions |> filter(a => match a { - MemberTeardownRefused { member: _, cause: _ } => true - MemberUpsert { member: _ } => false - MemberTeardown { member: _ } => false + MemberRemovalRefused { from: _, cause: _ } => true + MemberAdded { to: _ } => false + MemberChanged { from: _, to: _ } => false + MemberRemoved { from: _ } => false }) } @@ -339,9 +342,10 @@ fn belt_member_ids(ms: List) -> List { fn belt_refusal_member_id(a: MemberAction) -> String { match a { - MemberTeardownRefused { member, cause: _ } => dispatch_member_id(m: member) - MemberUpsert { member } => dispatch_member_id(m: member) - MemberTeardown { member } => dispatch_member_id(m: member) + MemberRemovalRefused { from: member, cause: _ } => dispatch_member_id(m: member) + MemberAdded { to: member } => dispatch_member_id(m: member) + MemberChanged { from: _, to: member } => dispatch_member_id(m: member) + MemberRemoved { from: member } => dispatch_member_id(m: member) } } diff --git a/dag/gunbc/tool_readiness.dag b/dag/gunbc/tool_readiness.dag index 4e4686ad8f4..0d1be202c0d 100644 --- a/dag/gunbc/tool_readiness.dag +++ b/dag/gunbc/tool_readiness.dag @@ -137,7 +137,7 @@ fn pinned_tool_readiness( observed_identity: observation.observed_identity, ) let tally = membership_tally(plan: plan) - if tally.upserts > 0 || tally.teardowns > 0 || tally.refusals > 0 { + if (tally.adds + tally.changes) > 0 || tally.removals > 0 || tally.refusals > 0 { tool_refused( tool: pin.subject, cause: ToolMembershipNotConverged { diff --git a/dag/gunbc/workflow_reconcile.dag b/dag/gunbc/workflow_reconcile.dag index 3a4b7ea89cc..e45c18e2edb 100644 --- a/dag/gunbc/workflow_reconcile.dag +++ b/dag/gunbc/workflow_reconcile.dag @@ -11,9 +11,10 @@ import std.workflow_recursive { import gunbc.membership_reconcile { MembershipPlan, MemberAction, - MemberUpsert, - MemberTeardown, - MemberTeardownRefused, + MemberAdded, + MemberChanged, + MemberRemoved, + MemberRemovalRefused, membership_reconcile, } import gunbc.ownership { Ownership, Ensured } @@ -86,7 +87,7 @@ type WorkflowReconcileReport { verdict: ReduceVerdict } -data workflow_recursive_reconcile_note: String = "A workflow is desired facts reconciled against observed facts, not a stored stage enum. WorkflowFactTree is recursive at every grain: a fact may be a leaf or may be decomposed into child workflow facts while retaining its own verdict. fold_workflow_fact_tree is THE catamorphism over that shape; membership, verdict, and observation tallies are algebras over the same traversal rather than independent recursive walkers. Its membership algebra DERIVES each WorkflowFactMember parent_key from the tree edge, so moving an unchanged child between parents is one Modified upsert rather than an invisible no-op or hand-authored remove/add pair. Desired and observed members feed the existing generic membership_reconcile; Added/Modified members become one generic upsert obligation, unchanged members disappear by monoid identity, and an observed member removed from desired REFUSES because workflow facts are Ensured rather than Owned. Goal shrink therefore cannot compile into evidence deletion: an intentional removal must remain as an explicit WorkflowFactWaived desired fact. intent_revision is per-obligation semantic identity, so an approved refinement produces a Modified hunk while unchanged sibling facts remain noops. The verdict projection reuses std.workflow_recursive: a decomposed parent participates beside its descendants, so green children cannot silently complete a pending parent and one deep refusal latches the whole tree. Observed failure/refusal and plan refusal are separate typed counts: a provider refusal cannot degrade into generic not-converged, and an unsafe goal removal cannot masquerade as provider failure. Realizations consume the generic MemberUpsert as either a direct effect or another planned workflow; they do not each reimplement desired-vs-observed mutation logic." +data workflow_recursive_reconcile_note: String = "A workflow is desired facts reconciled against observed facts, not a stored stage enum. WorkflowFactTree is recursive at every grain: a fact may be a leaf or may be decomposed into child workflow facts while retaining its own verdict. fold_workflow_fact_tree is THE catamorphism over that shape; membership, verdict, and observation tallies are algebras over the same traversal rather than independent recursive walkers. Its membership algebra DERIVES each WorkflowFactMember parent_key from the tree edge, so moving an unchanged child between parents is one MemberChanged rather than an invisible no-op or hand-authored remove/add pair. Desired and observed members feed the existing generic membership_reconcile; Added members become a MemberAdded obligation and Modified members a MemberChanged obligation (both are work remaining; they differ in how they realize — gunbc.change_realization), unchanged members disappear by monoid identity, and an observed member removed from desired REFUSES because workflow facts are Ensured rather than Owned. Goal shrink therefore cannot compile into evidence deletion: an intentional removal must remain as an explicit WorkflowFactWaived desired fact. intent_revision is per-obligation semantic identity, so an approved refinement produces a Modified hunk while unchanged sibling facts remain noops. The verdict projection reuses std.workflow_recursive: a decomposed parent participates beside its descendants, so green children cannot silently complete a pending parent and one deep refusal latches the whole tree. Observed failure/refusal and plan refusal are separate typed counts: a provider refusal cannot degrade into generic not-converged, and an unsafe goal removal cannot masquerade as provider failure. Realizations consume the generic MemberAdded/MemberChanged as either a direct effect or another planned workflow; they do not each reimplement desired-vs-observed mutation logic." fn workflow_fact_state_key(state: WorkflowFactState) -> String { match state { @@ -396,7 +397,7 @@ fn workflow_reconcile_fold_action( action: MemberAction, ) -> WorkflowReconcileFold { match action { - MemberUpsert { member } => + MemberAdded { to: member } => WorkflowReconcileFold { remaining: acc.remaining + 1, plan_refusals: acc.plan_refusals, @@ -406,7 +407,17 @@ fn workflow_reconcile_fold_action( acc.first_missing }, } - MemberTeardown { member } => + MemberChanged { from: _, to: member } => + WorkflowReconcileFold { + remaining: acc.remaining + 1, + plan_refusals: acc.plan_refusals, + first_missing: if acc.first_missing == "" { + workflow_fact_locus(fact: member.fact) + } else { + acc.first_missing + }, + } + MemberRemoved { from: member } => WorkflowReconcileFold { remaining: acc.remaining + 1, plan_refusals: acc.plan_refusals + 1, @@ -416,7 +427,7 @@ fn workflow_reconcile_fold_action( acc.first_missing }, } - MemberTeardownRefused { member, cause: _ } => + MemberRemovalRefused { from: member, cause: _ } => WorkflowReconcileFold { remaining: acc.remaining + 1, plan_refusals: acc.plan_refusals + 1, diff --git a/dag/test/claim/change_realization_witness_test.dag b/dag/test/claim/change_realization_witness_test.dag new file mode 100644 index 00000000000..80c54aefd91 --- /dev/null +++ b/dag/test/claim/change_realization_witness_test.dag @@ -0,0 +1,183 @@ +module test.claim.change_realization_witness + +import std.types { String, List, Bool, Int, NonEmptyStr } +import gunbc.change_realization { + ChangeSubject, ScmRefSubject, SourceDeclarationSubject, HostResourceSubject, + AddressContinuity, AddressPreserved, AddressChanged, address_continuity, + StagedIntermediate, RetirePriorEndpoint, UnlinkStalePath, StopPriorUnit, DrainPriorConsumers, + StagedIntermediates, staged_intermediates_all, staged_intermediates_count, + ChangeRealization, AtomicCompareAndSwap, AtomicTreeTransformation, InPlaceUpdate, StagedReplacement, + ChangeClassification, ChangeRealized, ChangeRefused, + ChangeRefusalCause, StagedReplacementIntermediatesUndeclared, + classify_change, +} +import gunbc.host_resource { + ResourceOccurrenceId, ResourceOccurrenceAllocator, ResourceOccurrenceAllocResult, + resource_occurrence_allocator_initial, alloc_resource_occurrence, resource_occurrence_eq, + HostResourceIdentity, host_resource_identity_eq, + HostResource, host_resource_same_occurrence, +} +import product.placement_supply { HostIdentity } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +fn str_eq(a: String, b: String) -> Bool { a == b } + +fn one_intermediate(step: StagedIntermediate) -> StagedIntermediates { + StagedIntermediates { first: step, rest: [] } +} + +fn is_realized_staged(c: ChangeClassification) -> Bool { + match c { + ChangeRealized { realization: r } => + match r { + StagedReplacement { intermediates: _ } => true + AtomicCompareAndSwap => false + AtomicTreeTransformation => false + InPlaceUpdate => false + } + ChangeRefused { cause: _ } => false + } +} + +fn is_realized(c: ChangeClassification, expected_in_place: Bool) -> Bool { + match c { + ChangeRealized { realization: r } => + match r { + InPlaceUpdate => expected_in_place + AtomicCompareAndSwap => !expected_in_place + AtomicTreeTransformation => false + StagedReplacement { intermediates: _ } => false + } + ChangeRefused { cause: _ } => false + } +} + +data w_scm_ref_is_cas_note: String = "An SCM ref update classifies as a compare-and-swap because git update-ref NAMES the expected prior — the from side of MemberChanged. This is the row that shows the from side UNLOCKS a realization rather than merely documenting one: with only `to` in hand the sole reachable realization is the unconditional write, and a concurrent update would be silently overwritten instead of losing." + +test fn w_scm_ref_update_is_compare_and_swap() -> Bool { + match classify_change(subject: ScmRefSubject, subject_label: "refs/heads/main" as NonEmptyStr, continuity: AddressPreserved, declared_intermediates: none) { + ChangeRealized { realization: r } => + match r { + AtomicCompareAndSwap => true + AtomicTreeTransformation => false + InPlaceUpdate => false + StagedReplacement { intermediates: _ } => false + } + ChangeRefused { cause: _ } => false + } +} + +data w_source_move_is_not_host_migration_note: String = "THE CONFLATION THIS TABLE KILLS. A .dag module re-home is an atomic SCM TREE TRANSFORMATION: it changes no runtime address, unlinks no socket, restarts no unit, and needs no intermediates. Treating it as a host migration is what made an ordinary source cleanup look like it required an operational migration plan. Discriminating against the host row below: the SAME AddressChanged input yields a tree transformation for a source declaration and a staged replacement for a host resource — so the subject, not the address delta alone, decides." + +test fn w_source_declaration_move_is_tree_transformation_not_migration() -> Bool { + let moved = classify_change( + subject: SourceDeclarationSubject, + subject_label: "gunbc.membership_reconcile.MemberChanged" as NonEmptyStr, + continuity: AddressChanged, + declared_intermediates: none, + ) + match moved { + ChangeRealized { realization: r } => + match r { + AtomicTreeTransformation => true + AtomicCompareAndSwap => false + InPlaceUpdate => false + StagedReplacement { intermediates: _ } => false + } + ChangeRefused { cause: _ } => false + } +} + +data w_host_address_decides_note: String = "For a host resource the deciding fact is whether the RUNTIME ADDRESS survived. Same unit name / socket / FIFO means the running thing absorbs a new value in place. A changed address means two addresses exist during the transition and the old one must be retired — a staged operation with observable intermediate states. Both directions asserted from the same subject, so the address axis is proven to decide rather than being incidentally true." + +test fn w_host_resource_address_preserved_is_in_place() -> Bool { + is_realized( + c: classify_change( + subject: HostResourceSubject, + subject_label: "srv4/build-cache" as NonEmptyStr, + continuity: address_continuity(from: "gunbc-cache.service", to: "gunbc-cache.service", address_eq: str_eq), + declared_intermediates: none, + ), + expected_in_place: true, + ) +} + +test fn w_host_resource_address_changed_is_staged_replacement() -> Bool { + is_realized_staged( + c: classify_change( + subject: HostResourceSubject, + subject_label: "srv4/build-cache" as NonEmptyStr, + continuity: address_continuity(from: "gunbc-cache.service", to: "gunbc-buildcache.service", address_eq: str_eq), + declared_intermediates: Present { + value: one_intermediate(step: RetirePriorEndpoint { endpoint: "/run/sccache.sock" as NonEmptyStr }) + }, + ) + ) +} + +data w_srv4_undeclared_intermediates_refuses_note: String = "THE srv4 SPECIMEN, made executable. srv4's build-cache server died with its cgroup, never unlinked its socket, and ran uncached for weeks because nobody modeled the intermediate state. gunbc.build_cache_instance says in PROSE that a managed unit must clear a stale endpoint on start, and a sentence in prose is the one place no machine can read it (DESIGN §4c). This row is the machine reading it: a staged replacement whose intermediates were never declared REFUSES, typed and located. It does NOT silently degrade to an in-place update and it does NOT proceed with an empty plan — the first is the absorbing fallback DESIGN §5 forbids, and the second IS the srv4 outcome. The discriminating half is that the ONLY difference from the accepted row above is the missing declaration." + +test fn w_staged_replacement_without_declared_intermediates_refuses() -> Bool { + match classify_change( + subject: HostResourceSubject, + subject_label: "srv4/build-cache" as NonEmptyStr, + continuity: AddressChanged, + declared_intermediates: none, + ) { + ChangeRefused { cause: c } => + match c { + StagedReplacementIntermediatesUndeclared { subject_label: label } => + (label as String) == "srv4/build-cache" + } + ChangeRealized { realization: _ } => false + } +} + +data w_intermediates_nonempty_by_construction_note: String = "StagedIntermediates is head + tail, not a List that could be []. So the srv4 state — a staged replacement that believed it had nothing to retire — is UNREPRESENTABLE rather than validated against (DESIGN §5 construction-over-validation, §4b: the invalid state has no constructor). This row asserts the floor that construction guarantees: every StagedIntermediates yields at least one step, so a count of zero cannot be built to be tested for." + +test fn w_staged_intermediates_are_never_empty() -> Bool { + let single = one_intermediate(step: StopPriorUnit { unit: "sccache.service" as NonEmptyStr }) + let many = StagedIntermediates { + first: StopPriorUnit { unit: "sccache.service" as NonEmptyStr }, + rest: [ + UnlinkStalePath { path: "/run/sccache.sock" as NonEmptyStr }, + DrainPriorConsumers { description: "in-flight compiles" as NonEmptyStr }, + ], + } + staged_intermediates_count(steps: single) == 1 + && count(staged_intermediates_all(steps: single)) == 1 + && staged_intermediates_count(steps: many) == 3 + && count(staged_intermediates_all(steps: many)) == 3 +} + +data w_identity_minted_not_derived_note: String = "Identity is MINTED BY THE ALLOCATOR, never derived from content, path, or unit name. This is what makes a rename ONE change rather than a delete-plus-create that some key function has to be clever enough to re-pair: git does not track renames, it INFERS them from content similarity after the fact, and DESIGN §4 rules a heuristic never necessary in a closed system. The row asserts the property that inference cannot give you — a resource whose unit name AND storage path both changed still compares as the SAME occurrence, because the occurrence was allocated, not computed." + +test fn w_occurrence_survives_total_value_change() -> Bool { + let a0 = resource_occurrence_allocator_initial() + let first = alloc_resource_occurrence(alloc: a0) + let second = alloc_resource_occurrence(alloc: first.alloc) + let id = HostResourceIdentity { host: "srv4" as HostIdentity, occurrence: first.id } + let before = HostResource { identity: id, role: "BuildCache", value: "gunbc-cache.service@/run/sccache.sock" } + let after = HostResource { identity: id, role: "BuildCache", value: "gunbc-buildcache.service@/run/buildcache.sock" } + let unrelated = HostResource { + identity: HostResourceIdentity { host: "srv4" as HostIdentity, occurrence: second.id }, + role: "BuildCache", + value: "gunbc-cache.service@/run/sccache.sock", + } + host_resource_same_occurrence(left: before, right: after) + && !host_resource_same_occurrence(left: before, right: unrelated) + && !resource_occurrence_eq(left: first.id, right: second.id) +} + +data w_identity_is_host_scoped_note: String = "The occurrence is scoped BY HOST: HostResourceIdentity pairs a HostIdentity with the occurrence, so the same occurrence ordinal on two different hosts is two different resources. Without the host component a per-host allocator's ordinals would collide across the fleet and two unrelated resources would compare equal — the same numeric-coincidence failure that keeps this carrier separate from std.occurrence_identity in the first place." + +test fn w_same_occurrence_different_host_is_different_identity() -> Bool { + let a0 = resource_occurrence_allocator_initial() + let first = alloc_resource_occurrence(alloc: a0) + let on_srv3 = HostResourceIdentity { host: "srv3" as HostIdentity, occurrence: first.id } + let on_srv4 = HostResourceIdentity { host: "srv4" as HostIdentity, occurrence: first.id } + !host_resource_identity_eq(left: on_srv3, right: on_srv4) + && host_resource_identity_eq(left: on_srv3, right: on_srv3) +} diff --git a/dag/test/claim/host_phase_status_witness_test.dag b/dag/test/claim/host_phase_status_witness_test.dag index 1dfbc01aaf3..bb84a605fdc 100644 --- a/dag/test/claim/host_phase_status_witness_test.dag +++ b/dag/test/claim/host_phase_status_witness_test.dag @@ -133,8 +133,8 @@ test fn witness_reconcile_covers_upsert_teardown_and_noop() -> Bool { observed: [at_desired, unconverged, departed], ) plan.actions.length() == 2 - && membership_upsert_count(plan: plan) == 1 - && membership_teardown_count(plan: plan) == 1 + && membership_write_count(plan: plan) == 1 + && membership_removal_count(plan: plan) == 1 && membership_refusal_count(plan: plan) == 0 } diff --git a/dag/test/claim/membership_reconcile_witness_test.dag b/dag/test/claim/membership_reconcile_witness_test.dag index 6f559825437..f38c50ab275 100644 --- a/dag/test/claim/membership_reconcile_witness_test.dag +++ b/dag/test/claim/membership_reconcile_witness_test.dag @@ -4,11 +4,12 @@ import std.types { String, List, Bool, Int } import gunbc.ownership { Ownership, Owned, Ensured } import gunbc.membership_reconcile { MembershipPlan, MemberAction, - MemberUpsert, MemberTeardown, MemberTeardownRefused, + MemberAdded, MemberChanged, MemberRemoved, MemberRemovalRefused, TeardownRefusalCause, MemberNotOwned, OwnershipUnknown, membership_reconcile, - membership_upsert_count, membership_teardown_count, membership_refusal_count, - MemberEffect, EffectUpsert, EffectTeardown, + membership_write_count, membership_removal_count, membership_refusal_count, + MemberEffect, EffectAdd, EffectReplace, EffectRemove, + membership_added_count, membership_change_count, MemberRefusal, EffectsOrRefusal, EffectsReady, ApplyRefused, membership_effects, @@ -48,18 +49,28 @@ fn t_reconcile(desired: List, observed: List) -> MembershipPla ) } -fn plan_has_upsert(plan: MembershipPlan, mid: String) -> Bool { - any(plan.actions, a => match a { MemberUpsert { member: m } => m.mid == mid _ => false }) +fn plan_has_add(plan: MembershipPlan, mid: String) -> Bool { + any(plan.actions, a => match a { MemberAdded { to: m } => m.mid == mid _ => false }) +} + +fn plan_has_change_from_to(plan: MembershipPlan, mid: String, from_ver: String, to_ver: String) -> Bool { + any(plan.actions, a => + match a { + MemberChanged { from: f, to: t } => + f.mid == mid && t.mid == mid && f.ver == from_ver && t.ver == to_ver + _ => false + } + ) } fn plan_has_teardown(plan: MembershipPlan, mid: String) -> Bool { - any(plan.actions, a => match a { MemberTeardown { member: m } => m.mid == mid _ => false }) + any(plan.actions, a => match a { MemberRemoved { from: m } => m.mid == mid _ => false }) } fn plan_has_refused_not_owned(plan: MembershipPlan, mid: String) -> Bool { any(plan.actions, a => match a { - MemberTeardownRefused { member: m, cause: c } => + MemberRemovalRefused { from: m, cause: c } => m.mid == mid && (match c { MemberNotOwned => true OwnershipUnknown => false }) _ => false } @@ -69,7 +80,7 @@ fn plan_has_refused_not_owned(plan: MembershipPlan, mid: String) -> Boo fn plan_has_refused_unknown(plan: MembershipPlan, mid: String) -> Bool { any(plan.actions, a => match a { - MemberTeardownRefused { member: m, cause: c } => + MemberRemovalRefused { from: m, cause: c } => m.mid == mid && (match c { OwnershipUnknown => true MemberNotOwned => false }) _ => false } @@ -78,34 +89,54 @@ fn plan_has_refused_unknown(plan: MembershipPlan, mid: String) -> Bool test fn w_added_upserts() -> Bool { let plan = t_reconcile(desired: [tm_owned(mid: "a", ver: "1")], observed: []) - plan_has_upsert(plan: plan, mid: "a") - && membership_upsert_count(plan: plan) == 1 - && membership_teardown_count(plan: plan) == 0 + plan_has_add(plan: plan, mid: "a") + && membership_write_count(plan: plan) == 1 + && membership_removal_count(plan: plan) == 0 } test fn w_removed_owned_tears_down() -> Bool { let plan = t_reconcile(desired: [], observed: [tm_owned(mid: "a", ver: "1")]) plan_has_teardown(plan: plan, mid: "a") - && membership_teardown_count(plan: plan) == 1 + && membership_removal_count(plan: plan) == 1 && membership_refusal_count(plan: plan) == 0 } test fn w_unchanged_noop() -> Bool { let m = tm_owned(mid: "a", ver: "1") let plan = t_reconcile(desired: [m], observed: [m]) - membership_upsert_count(plan: plan) == 0 - && membership_teardown_count(plan: plan) == 0 + membership_write_count(plan: plan) == 0 + && membership_removal_count(plan: plan) == 0 && membership_refusal_count(plan: plan) == 0 } -test fn w_modified_reupserts() -> Bool { +data w_modified_changes_note: String = "A Modified hunk is a MemberChanged carrying BOTH sides, NOT an add of the `to` side. The from-side assertion is the discriminating half: it reds if anyone reintroduces the collapse that discarded `from`, which is the fact every safe realization of a change needs (an SCM compare-and-swap names the expected prior; a moved host address needs the prior endpoint to retire). Asserted at the ACTION grain — a tally alone cannot tell a change from an add." + +test fn w_modified_is_change_carrying_both_sides() -> Bool { let plan = t_reconcile( desired: [tm_owned(mid: "a", ver: "2")], observed: [tm_owned(mid: "a", ver: "1")], ) - plan_has_upsert(plan: plan, mid: "a") - && membership_upsert_count(plan: plan) == 1 - && membership_teardown_count(plan: plan) == 0 + plan_has_change_from_to(plan: plan, mid: "a", from_ver: "1", to_ver: "2") + && !plan_has_add(plan: plan, mid: "a") + && membership_change_count(plan: plan) == 1 + && membership_added_count(plan: plan) == 0 + && membership_write_count(plan: plan) == 1 + && membership_removal_count(plan: plan) == 0 + && membership_refusal_count(plan: plan) == 0 +} + +data w_ensured_converges_note: String = "REGRESSION CONTROL for a wall that was BUILT AND WITHDRAWN during this change (DESIGN §4b(4): the evidence stays enrolled after the reasoning settles; §4c: prose is never evidence a machine claim holds). An earlier draft refused a Modified hunk whose `from` was not Owned, reading replacement as destruction. That is wrong, and this row is what makes it stay wrong out loud. WHAT IT PROVES, precisely: gunbc.ownership defines Ensured as 'requires present but does NOT own (never torn down)' — a constraint on REMOVAL. Ensured says NOTHING about update, and treating it as if it did breaks the module whose entire job is re-installing drifted pins (tool_readiness classifies every pin Ensured; repo_local_git_config every binding). So the SAME Ensured member must CONVERGE when its value drifts and REFUSE when it is removed — one member, both arms, in one plan, so the asymmetry is asserted rather than assumed. Reintroducing the change-refusal arm turns the first conjunct red." + +test fn w_ensured_member_converges_but_refuses_removal() -> Bool { + let plan = t_reconcile( + desired: [tm_ensured(mid: "drifted", ver: "2")], + observed: [tm_ensured(mid: "drifted", ver: "1"), tm_ensured(mid: "gone", ver: "1")], + ) + plan_has_change_from_to(plan: plan, mid: "drifted", from_ver: "1", to_ver: "2") + && membership_change_count(plan: plan) == 1 + && plan_has_refused_not_owned(plan: plan, mid: "gone") + && membership_refusal_count(plan: plan) == 1 + && membership_removal_count(plan: plan) == 0 } test fn w_r5_owned_only_teardown_synthetic() -> Bool { @@ -122,12 +153,38 @@ test fn w_r5_owned_only_teardown_synthetic() -> Bool { && !plan_has_teardown(plan: plan, mid: "e") && plan_has_refused_unknown(plan: plan, mid: "u") && !plan_has_teardown(plan: plan, mid: "u") - && membership_teardown_count(plan: plan) == 1 + && membership_removal_count(plan: plan) == 1 && membership_refusal_count(plan: plan) == 2 } fn effects_has_teardown(es: List>, mid: String) -> Bool { - any(es, e => match e { EffectTeardown { member: m } => m.mid == mid EffectUpsert { member: _ } => false }) + any(es, e => + match e { + EffectRemove { from: m } => m.mid == mid + EffectAdd { to: _ } => false + EffectReplace { from: _, to: _ } => false + } + ) +} + +data w_effect_replace_note: String = "EffectReplace carries BOTH sides into apply, which is the point of the split: a handler that replaces a member must be able to retire the prior realization, and `from` is the only place the prior endpoint survives. An EffectAdd carries one side because there is nothing there to retire." + +test fn w_change_projects_to_effect_replace_with_both_sides() -> Bool { + let plan = t_reconcile( + desired: [tm_owned(mid: "a", ver: "2")], + observed: [tm_owned(mid: "a", ver: "1")], + ) + match membership_effects(plan: plan) { + EffectsReady { effects: es } => + count(es) == 1 + && any(es, e => + match e { + EffectReplace { from: f, to: t } => f.ver == "1" && t.ver == "2" && f.mid == "a" + EffectAdd { to: _ } => false + EffectRemove { from: _ } => false + }) + ApplyRefused { refusals: _ } => false + } } data w_effects_wholesale_refuse_note: String = "DISCRIMINATING (§5): a plan carrying any Refused MUST refuse WHOLESALE — membership_effects returns ApplyRefused (o's owned teardown NOT surfaced as an effect), never EffectsReady with the refused sibling silently filtered out. If membership_effects is ever broken to drop-the-refused and return the effects, this hits the EffectsReady arm and returns false = RED. The degenerate apply/retract poles never produce a Refused, so only this synthetic mixed observed set exercises the wall." @@ -162,9 +219,11 @@ test fn w_tally_matches_counts() -> Bool { observed: [tm_owned(mid: "b", ver: "1"), tm_ensured(mid: "c", ver: "1")], ) let t = membership_tally(plan: plan) - t.upserts == 1 && t.teardowns == 1 && t.refusals == 1 - && t.upserts == membership_upsert_count(plan: plan) - && t.teardowns == membership_teardown_count(plan: plan) + t.adds == 1 && t.removals == 1 && t.refusals == 1 && t.changes == 0 + && t.adds == membership_added_count(plan: plan) + && t.changes == membership_change_count(plan: plan) + && (t.adds + t.changes) == membership_write_count(plan: plan) + && t.removals == membership_removal_count(plan: plan) && t.refusals == membership_refusal_count(plan: plan) } diff --git a/dag/test/claim/repo_local_git_config_witness_test.dag b/dag/test/claim/repo_local_git_config_witness_test.dag index 8751641dc2b..070d17f25aa 100644 --- a/dag/test/claim/repo_local_git_config_witness_test.dag +++ b/dag/test/claim/repo_local_git_config_witness_test.dag @@ -17,8 +17,8 @@ import gunbc.repo_local_git_config { repo_local_git_config_converge_function, } import gunbc.membership_reconcile { - membership_upsert_count, - membership_teardown_count, + membership_write_count, + membership_removal_count, membership_refusal_count, } import extdeps.git { @@ -46,8 +46,8 @@ test fn witness_converge_entry_is_declared() -> Bool { test fn witness_empty_observed_reconcile_upserts_holds() -> Bool { let plan = repo_local_git_config_reconcile(desired: desired_repo_local_git_config_bindings(), observed: []) - membership_upsert_count(plan: plan) == 2 - && membership_teardown_count(plan: plan) == 0 + membership_write_count(plan: plan) == 2 + && membership_removal_count(plan: plan) == 0 && membership_refusal_count(plan: plan) == 0 } diff --git a/dag/test/claim/srv3_subsumption_witness_test.dag b/dag/test/claim/srv3_subsumption_witness_test.dag index 7369e2532a9..4d35d3ea2f9 100644 --- a/dag/test/claim/srv3_subsumption_witness_test.dag +++ b/dag/test/claim/srv3_subsumption_witness_test.dag @@ -61,9 +61,10 @@ test fn srv3_reconcile_adds_exactly_the_missing_fleet_key() -> Bool { let plan = srv3_plan() let upsert_materials = flat_map(plan.actions, a => match a { - MemberUpsert { member: m } => [m.material as String] - MemberTeardown { member: _ } => [] - MemberTeardownRefused { member: _, cause: _ } => [] + MemberAdded { to: m } => [m.material as String] + MemberChanged { from: _, to: m } => [m.material as String] + MemberRemoved { from: _ } => [] + MemberRemovalRefused { from: _, cause: _ } => [] } ) count(upsert_materials) == 1 @@ -75,14 +76,15 @@ test fn srv3_reconcile_refuses_both_unowned_keys_never_teardown() -> Bool { let tally = membership_tally(plan: plan) let refused_materials = flat_map(plan.actions, a => match a { - MemberTeardownRefused { member: m, cause: OwnershipUnknown } => [m.material as String] - MemberTeardownRefused { member: _, cause: MemberNotOwned } => [] - MemberUpsert { member: _ } => [] - MemberTeardown { member: _ } => [] + MemberRemovalRefused { from: m, cause: OwnershipUnknown } => [m.material as String] + MemberRemovalRefused { from: _, cause: MemberNotOwned } => [] + MemberAdded { to: _ } => [] + MemberChanged { from: _, to: _ } => [] + MemberRemoved { from: _ } => [] } ) - tally.upserts == 1 - && tally.teardowns == 0 + tally.adds == 1 + && tally.removals == 0 && tally.refusals == 2 && any(refused_materials, m => m == srv3_observed_node_orch_srv2_key.material as String) && any(refused_materials, m => m == srv3_observed_briansrls_srv1_key.material as String) @@ -90,14 +92,14 @@ test fn srv3_reconcile_refuses_both_unowned_keys_never_teardown() -> Bool { test fn srv4_reconcile_is_converged_empty_plan() -> Bool { let tally = membership_tally(plan: srv4_plan()) - tally.upserts == 0 && tally.teardowns == 0 && tally.refusals == 0 + tally.adds == 0 && tally.removals == 0 && tally.refusals == 0 } test fn srv3_and_srv4_disagree_on_convergence() -> Bool { let srv3 = membership_tally(plan: srv3_plan()) let srv4 = membership_tally(plan: srv4_plan()) - (srv3.upserts + srv3.refusals) > 0 - && (srv4.upserts + srv4.teardowns + srv4.refusals) == 0 + (srv3.adds + srv3.refusals) > 0 + && (srv4.adds + srv4.removals + srv4.refusals) == 0 } fn ownership_lies_owned(k: SshPublicKey) -> Ownership? { @@ -115,12 +117,12 @@ test fn reconcile_would_teardown_only_if_ownership_claimed_it() -> Bool { ownership_of: ownership_lies_owned, )) honest.refusals == 2 - && honest.teardowns == 0 + && honest.removals == 0 && lying.refusals == 0 - && lying.teardowns == 2 + && lying.removals == 2 } -test fn comment_only_drift_is_reupsert_not_remove_add() -> Bool { +test fn comment_only_drift_is_one_change_not_remove_add() -> Bool { let renamed_macbook = SshPublicKey { algorithm: operator_macbook_ssh_key.algorithm, material: operator_macbook_ssh_key.material, @@ -128,7 +130,7 @@ test fn comment_only_drift_is_reupsert_not_remove_add() -> Bool { } let observed = [renamed_macbook, fleet_automation_ssh_key] let tally = membership_tally(plan: host_authorized_keys_reconcile(observed: observed)) - tally.upserts == 1 && tally.teardowns == 0 && tally.refusals == 0 + tally.changes == 1 && tally.adds == 0 && tally.removals == 0 && tally.refusals == 0 } data host_toolchain_reach_pairing_witness_note: String = "Discriminating witnesses for the 2026-07-24 target/access pairing in gunbc.host_toolchain_ensure. The defect being walled: access used to be looked up from the REQUESTED host while the target was resolved kind-aware, so a BuildCache request for srv3 targeted srv3 and authenticated to srv1 — the effect lands on the wrong machine and reports success. A test that merely asserts the reach resolves would pass under the old code too, so the load-bearing row here is reach_access_host_is_the_target_host, which compares the two sides of the pair and is red exactly when they disagree. Its negative control is reach_wrong_machine_pairing_is_unwritable: the old behaviour is reconstructed by hand and shown to violate the same predicate, so the predicate is proven to discriminate rather than assumed to." diff --git a/dag/test/claim/tool_readiness_witness_test.dag b/dag/test/claim/tool_readiness_witness_test.dag index 25491c04368..319f9295ba7 100644 --- a/dag/test/claim/tool_readiness_witness_test.dag +++ b/dag/test/claim/tool_readiness_witness_test.dag @@ -20,7 +20,7 @@ import extdeps.realization.emit_on_demand_host { ResolvedBuildContext, } import gunbc.membership_reconcile { - membership_upsert_count, + membership_write_count, membership_refusal_count, } import gunbc.tool_readiness { @@ -97,7 +97,7 @@ test fn matching_pinned_tool_is_admitted_with_zero_hunks() -> Bool { ) { PinnedAdmitted { pin: admitted, plan: plan } => ((admitted.subject.name as String) == "rustfmt") - && membership_upsert_count(plan: plan) == 0 + && membership_write_count(plan: plan) == 0 && membership_refusal_count(plan: plan) == 0 PinnedRefused { refusals: _ } => false UnpinnedFrontier { row: _, observed: _ } => false @@ -120,7 +120,7 @@ test fn digest_mismatch_refuses_and_frontier_cannot_bypass_it() -> Bool { ((refusal.tool.name as String) == "rustfmt") && match refusal.cause { ToolMembershipNotConverged { plan: plan, admission: admission } => - membership_upsert_count(plan: plan) == 1 + membership_write_count(plan: plan) == 1 && match admission { PinRefused { subject: _, cause: cause } => match cause { @@ -152,7 +152,7 @@ test fn unchanged_tracked_pin_still_refuses_integrity() -> Bool { Present { value: refusal } => match refusal.cause { ToolPinIntegrityRefused { cause: cause, plan: plan } => - membership_upsert_count(plan: plan) == 0 + membership_write_count(plan: plan) == 0 && match cause { TrackedResolutionUnrecorded { channel: channel } => (channel as String) == "stable" @@ -186,10 +186,10 @@ test fn unrelated_tool_identity_does_not_change_rustfmt_readiness() -> Bool { ) match before { PinnedAdmitted { pin: _, plan: before_plan } => - membership_upsert_count(plan: before_plan) == 0 + membership_write_count(plan: before_plan) == 0 && match after { PinnedAdmitted { pin: _, plan: after_plan } => - membership_upsert_count(plan: after_plan) == 0 + membership_write_count(plan: after_plan) == 0 _ => false } _ => false diff --git a/dag/test/claim/workflow_reconcile_witness_test.dag b/dag/test/claim/workflow_reconcile_witness_test.dag index dc26a21b3c2..448361b2ef2 100644 --- a/dag/test/claim/workflow_reconcile_witness_test.dag +++ b/dag/test/claim/workflow_reconcile_witness_test.dag @@ -21,9 +21,9 @@ import gunbc.workflow_reconcile { workflow_reconcile_status_key, } import gunbc.membership_reconcile { - MemberUpsert, - MemberTeardown, - MemberTeardownRefused, + MemberAdded, MemberChanged, + MemberRemoved, + MemberRemovalRefused, } fn workflow_fact_fixture( @@ -149,10 +149,11 @@ test fn missing_nested_child_derives_one_reconcile_action() -> Bool { && report.plan_refusal_count == 0 && count(report.plan.actions) == 1 && all(report.plan.actions, action => match action { - MemberUpsert { member } => + MemberAdded { to: member } => member.fact.key.obligation_id == "database" - MemberTeardown { member: _ } => false - MemberTeardownRefused { member: _, cause: _ } => false + MemberChanged { from: _, to: _ } => false + MemberRemoved { from: _ } => false + MemberRemovalRefused { from: _, cause: _ } => false }) && match report.verdict { Unknown { missing } => @@ -184,15 +185,18 @@ test fn goal_revision_change_is_modified_not_delete_add() -> Bool { && report.plan_refusal_count == 0 && count(report.plan.actions) == 1 && all(report.plan.actions, action => match action { - MemberUpsert { member } => + MemberChanged { from: prior, to: member } => member.fact.key.obligation_id == "frontend" && member.fact.intent_revision == "frontend-v2" - MemberTeardown { member: _ } => false - MemberTeardownRefused { member: _, cause: _ } => false + && prior.fact.key.obligation_id == "frontend" + && prior.fact.intent_revision == "frontend-v1" + MemberAdded { to: _ } => false + MemberRemoved { from: _ } => false + MemberRemovalRefused { from: _, cause: _ } => false }) } -test fn reparented_child_is_one_modified_upsert() -> Bool { +test fn reparented_child_is_one_member_changed() -> Bool { let observed = [ workflow_decomposed_fixture( obligation_id: "deliver-feature", @@ -227,15 +231,21 @@ test fn reparented_child_is_one_modified_upsert() -> Bool { && report.plan_refusal_count == 0 && count(report.plan.actions) == 1 && all(report.plan.actions, action => match action { - MemberUpsert { member } => + MemberChanged { from: prior, to: member } => member.fact.key.obligation_id == "database" && match member.parent { WorkflowFactChild { parent_key: parent } => parent.obligation_id == "backend" WorkflowFactRoot => false } - MemberTeardown { member: _ } => false - MemberTeardownRefused { member: _, cause: _ } => false + && match prior.parent { + WorkflowFactChild { parent_key: parent } => + parent.obligation_id == "frontend" + WorkflowFactRoot => false + } + MemberAdded { to: _ } => false + MemberRemoved { from: _ } => false + MemberRemovalRefused { from: _, cause: _ } => false }) } @@ -268,10 +278,11 @@ test fn silent_goal_shrink_refuses_evidence_deletion() -> Bool { && report.plan_refusal_count == 1 && count(report.plan.actions) == 1 && all(report.plan.actions, action => match action { - MemberTeardownRefused { member, cause: _ } => + MemberRemovalRefused { from: member, cause: _ } => member.fact.key.obligation_id == "backend" - MemberUpsert { member: _ } => false - MemberTeardown { member: _ } => false + MemberAdded { to: _ } => false + MemberChanged { from: _, to: _ } => false + MemberRemoved { from: _ } => false }) && workflow_reconcile_status_key(report: report) == "refused" } @@ -405,7 +416,7 @@ test fn workflow_reconcile_keystone_holds() -> Bool { recursive_reconcile_all_satisfied_is_noop() && missing_nested_child_derives_one_reconcile_action() && goal_revision_change_is_modified_not_delete_add() - && reparented_child_is_one_modified_upsert() + && reparented_child_is_one_member_changed() && silent_goal_shrink_refuses_evidence_deletion() && explicit_waiver_is_a_fact_not_deletion() && deep_failure_blocks_green_parent_and_siblings() diff --git a/docs/plans/hermetic-tool-provisioning-design.md b/docs/plans/hermetic-tool-provisioning-design.md index 217e11fac55..b9d2394d4e5 100644 --- a/docs/plans/hermetic-tool-provisioning-design.md +++ b/docs/plans/hermetic-tool-provisioning-design.md @@ -313,7 +313,7 @@ Realization; a forked reconcile means the genericity bought nothing"): re-upserts, which is exactly the ensure semantics wanted. - `ownership_of` = `Owned` for tools provisioned into the repo-local root (removable), `Ensured` for system-required tools — so the R5 construction - wall already refuses teardown of a system tool (`MemberTeardownRefused`, + wall already refuses teardown of a system tool (`MemberRemovalRefused`, which has no effect arm in any apply dispatch), and ownership-unknown refuses rather than assuming. diff --git a/docs/plans/membership-diff-reconcile-spine-design.md b/docs/plans/membership-diff-reconcile-spine-design.md index f61cd5d2ee4..97fe7d4fc74 100644 --- a/docs/plans/membership-diff-reconcile-spine-design.md +++ b/docs/plans/membership-diff-reconcile-spine-design.md @@ -140,3 +140,66 @@ Pass 2 wired live_deploy onto the spine and refined the pre-commit design in thr 2. **Verdict→decision DRY** (calm-ferret flagged it forked 4×): my partition works off diff HUNKS, not `ObservationVerdict`, so I do NOT need that map for pass 1. Consolidating the 4× fork is a related but separate §3 cleanup — fold in later, not here. Agree? 3. **`Refuse: NonEmptyStr` upgrade**: R5 wants typed+located+counted refusals. I model `MemberTeardownRefused{member, cause}` (typed+located+counted) at the membership layer rather than upgrading `UpsertDecision.Refuse`. OK, or do you want the `UpsertDecision.Refuse` authority upgraded to carry a typed diagnostic? 4. **royal-carp — grain-agnosticism check**: does the "diff takes Session without surgery" test pass on this shape (only a new instantiation + dispatch arms, no spine-type edit)? And is the R5 owned-only boundary (Removed∩¬Owned + Unknown both REFUSE, construction-walled) what you locked? + +## Pass 3 — LANDED (occurrence identity + typed replacement classification) + +Operator ruling: *"Identity should be declaration-owned and allocator-minted — not derived from unit/path, and not a closed operator-maintained `HostRole` enum."* + +### The arms + +`MemberAction` is four arms, not three: + +``` += MemberAdded { to: M } +| MemberChanged { from: M, to: M } +| MemberRemoved { from: M } +| MemberRemovalRefused { from: M, cause: TeardownRefusalCause } +``` + +Add and change were previously collapsed into one `MemberUpsert{member}` carrying only the `to` side. **The discarded `from` is the load-bearing loss**, and it is not a tidiness point: the prior value is what every safe realization of a change consumes. An SCM ref update is a compare-and-swap that *names the expected prior* (`git update-ref `); a host resource whose address moved must retire the prior endpoint. With only `to` in hand the sole reachable realization is the unconditional write — the atomicity the underlying capability already offers cannot be reached. `MemberEffect` splits the same way (`EffectAdd{to}` / `EffectReplace{from,to}` / `EffectRemove{from}`) so the apply grain can retire a prior realization rather than overwrite it blind. + +`MemberRemovalRefused` is a first-class **action**, not an absence — that is what keeps a refusal countable rather than a hunk that silently did not appear. + +### What is NOT here, and why (a withdrawn wall) + +An earlier draft of this pass also refused a Modified hunk whose `from` was not `Owned`, reading replacement as destruction and claiming a live fail-open in five of seven consumers. **That was built, refuted by execution, and withdrawn.** `gunbc.ownership` defines `Ensured` as *"requires present but does NOT own (never torn down)"* — a constraint on **removal**, not on update. `tool_readiness` classifies every pin `Ensured` and exists precisely to re-install a pin whose observed version drifted; `repo_local_git_config` likewise. The wall broke those modules where it fired, and was unreachable where it did not (`host_axis_caps` derives ownership from the path, so a Modified hunk cannot pair a managed desired row with a foreign observed one; foreign `authorized_keys` are absent from desired, so they are Removed, never Modified). The original asymmetry was correct. + +Per DESIGN §4c a carrier note is *not* evidence a machine claim holds, so the withdrawal is enrolled rather than written down: `w_ensured_member_converges_but_refuses_removal` puts one `Ensured` member through **both** arms in one plan — it converges when its value drifts and refuses when it is removed. Reintroducing the change-refusal arm turns it red (verified by planting exactly that perturbation; the unrelated rows stayed green). + +### Identity: minted, not derived + +`gunbc.host_resource`: + +``` +type HostResourceIdentity { host: HostIdentity, occurrence: ResourceOccurrenceId } +type HostResource { identity: HostResourceIdentity, role: R, value: V } +``` + +The occurrence is **allocator-minted at declaration**, never computed from content, path, or unit name. This is the closed-system answer to renames: git does not track renames, it *infers* them from content similarity after the fact, and DESIGN §4 rules a heuristic never necessary in a closed system — a content- or path-derived `key_of` is that same inference wearing a bundle. Because the occurrence is allocated, a rename is ONE `MemberChanged` whose `from` and `to` share an identity and nothing has to be guessed. `role` is a **type parameter**, so `Jobserver` / `BuildCache` / `RunnerSlot` arrive as instantiations rather than edits to a central enum (the DESIGN §3 rule that adding Opera must not widen a browser-product enum). Unit name, FIFO, storage path and configuration are mutable **value** fields. `HostIdentity` is reused from `product.placement_supply`, not re-minted. + +**Why a distinct carrier from `std.occurrence_identity`** (decided by reading, recorded in-carrier): that module is specifically about *source* occurrences — `OccurrenceCategory` enumerates callable/type/constructor/field/method/namespace-segment, its carriers are `DeclarationOccurrence`/`ReferenceOccurrence` over containment paths, and its allocator is coupled through `occurrence_id_allocator_advance_to` to `AuthoredTokenOrdinalSpace`, a source-token watermark meaningless for a host resource. The subject-agnostic residue is only a monotone `Int` counter, and sharing one `Int` space across two subjects would let `occurrence_id_eq` answer `true` on a **numeric coincidence** between a host resource and a source occurrence — the exact cross-family comparison the `ContentHash` family grounding closed. The real §3 move (one subject-parameterized minted-identity carrier, the `Vendor` shape) is registered as `resource_occurrence_generalization_trigger` rather than built, because `std.occurrence_identity` is load-bearing compiler substrate with stage0 work in flight. + +### The classification table + +`gunbc.change_realization.classify_change` is what makes `MemberChanged` useful rather than merely more faithful — four **different atomicity guarantees**, where picking the wrong row is how a safe transformation acquires an unsafe realization: + +| subject / condition | realization | +| --- | --- | +| SCM ref update | atomic compare-and-swap (`git update-ref `) | +| source declaration move | atomic SCM tree transformation | +| host resource, same runtime address | in-place update | +| host resource, changed host address | staged replacement with **declared** intermediates | + +**The conflation this kills:** a `.dag` module re-home is an SCM tree transformation, **not** a host migration — it changes no runtime address, unlinks no socket, restarts no unit. Treating it as a migration is what made an ordinary source cleanup look like it needed an operational migration plan. The converse error is the dangerous one: renaming a systemd unit or moving a FIFO *is* a host replacement. + +**The srv4 specimen, made executable.** srv4's build-cache server died with its cgroup, never unlinked its socket, and ran uncached for weeks because nobody modeled the intermediate state. `gunbc.build_cache_instance` says in *prose* that a managed unit must clear a stale endpoint on start — the one place no machine can read it. `StagedIntermediates` is head + tail, so an empty intermediate plan **has no constructor** (§5 construction-over-validation; §4b: the invalid state is unrepresentable, not validated against). A staged replacement whose intermediates were never declared **refuses**, typed and located by `subject_label` — it does not degrade to an in-place update and does not proceed with an empty plan, both of which are the absorbing fallback §5 forbids and the second of which *is* the srv4 outcome. Verified discriminating: perturbing the refusal into an `InPlaceUpdate` fallback reds that row alone. + +### Consumer migration + +All seven consumers plus witnesses migrated; the compiler located every site by exhaustiveness. One real regression was caught in the process: `repo_local_git_config`'s apply fold has a `_ => acc` wildcard for its construction-unreachable removal arms, and a `MemberChanged` would have fallen into it — silently dropping exactly the drift that module exists to converge. Both write arms are now listed explicitly and routed through one `apply_repo_local_git_config_binding`. `live_deploy`'s `EffectReplace` arm is structurally unreachable at both degenerate poles, so per that module's established discipline it emits a loud typed poison rather than a fabricated no-op — and the poison names the staged-replacement requirement a real observed provider will have to satisfy. + +`membership_write_count` (adds + changes) is a **derived** projection replacing `membership_upsert_count` for consumers that used it as "how much work is left"; the split is never re-stored as one counter. + +### Open + +The `(key_of, key_eq, value_eq, ownership_of)` bundle still parameterizes the spine, so existing consumers are unchanged. Migrating them onto identity-carrying members is a separate lane — deliberately not bundled here, so the srv3 capacity work depending only on the `Added` arm is not blocked. diff --git a/docs/plans/recursive-workflow-advancement-design.md b/docs/plans/recursive-workflow-advancement-design.md index cffc2ee41f5..1f8c9cc128d 100644 --- a/docs/plans/recursive-workflow-advancement-design.md +++ b/docs/plans/recursive-workflow-advancement-design.md @@ -267,7 +267,7 @@ related but not interchangeable. ### 6.4 Every realizer may recurse -A `MemberUpsert` can be discharged by a direct modeled effect or by a child planned workflow. +A `MemberAdded` or `MemberChanged` can be discharged by a direct modeled effect or by a child planned workflow. Examples: - “ensure Codex authenticated” may spawn a provider-provisioning workflow; diff --git a/docs/plans/seamless-deploys-design.md b/docs/plans/seamless-deploys-design.md index 052b342d788..826cec93c75 100644 --- a/docs/plans/seamless-deploys-design.md +++ b/docs/plans/seamless-deploys-design.md @@ -360,7 +360,7 @@ nicety. This **resolves §7 q3 and re-prioritises the ticket**: item 3 is not optional work to be dropped if it proves expensive — it is the deployment ask, and "minimal possible items to update to intent" is exactly the spine's `Unchanged → noop`. The vocabulary already lines up one-to-one: **apply** = -`MemberUpsert`, **delete** = `MemberTeardown` (owned-only, else a typed refusal), **reconcile** = +`MemberAdded`/`MemberChanged`, **delete** = `MemberRemoved` (owned-only, else a typed refusal), **reconcile** = the diff itself, with unchanged members producing no hunk and therefore no effect. The good news is that this is **instantiation, not invention**. `live_deploy` is the *only* From 92ca80a2776c7d04908b52be36938ba5170338e3 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 6 Aug 2026 21:11:08 +0000 Subject: [PATCH 2/2] Trigger CI synchronize: #7938 opened with zero check runs (GitHub Actions webhook incident) The PR opened during the Actions backend incident and no workflow runs were created at all -- absent, not queued. ci.yml triggers on pull_request [opened, synchronize, reopened, ready_for_review], so this empty commit fires a synchronize to get the affected-set run executed against the branch. Co-Authored-By: Claude Opus 5 (1M context)