Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions dag/gunbc/rung_drop.dag
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,8 @@ data builtin_signature_arity_pairing_fabricates: RungDrop = RungDrop { identity:

data concat_binary_signature_exempt_from_arg_binding: RungDrop = RungDrop { identity: "concat_binary_signature_exempt_from_arg_binding" as NonEmptyStr, subject: "n-ary concat call sites judged against concat's binary declared signature", declared: "2026-09-01", standing: Standing, authored: "Builtin signature grounding -- **RUNG DROP, DECLARED (2026-09-01).** PREVIOUS RUNG: none to lower -- nothing binds builtin arguments today, so this declares a class that the arm flip would otherwise create. concat's declared signature is BINARY, and it is binary correctly: std.algebra declares param_types [ReceiverSelf, ReceiverSelf], and src/v1/runtime_rust.dag emits `pub fn concat<T: V2Concat>(a: T, b: T) -> T`. The algebra and the emitted runtime agree; only the CORPUS calls concat at other arities. TEMPORARY RUNG: mitigatable. concat is exempted from the direct-call argument-shape judgement when decide_callable_candidates begins answering FuncSigResolved for a BuiltinCallable; every other builtin is judged. REASON: concat(a, b, c) is a FOLD of the binary associative operation, and what licenses folding an n-ary application into nested binary applications is ASSOCIATIVITY, which is not modeled. std.algebra declares Magma<T> as { op: fn(T, T) -> T } and Semigroup<T> as { op: fn(T, T) -> T } -- structurally identical, differing by a blank line where the law would sit. The type whose entire content is the associativity law carries no law, so nothing in the tree can say an operation is associative, and the missing capability is one level below the signature rather than in it. Widening AlgebraTypeTemplate with a variadic arm was refused because variadicity is not a property of a parameter's TYPE -- that vocabulary answers what type a position has, not how many positions there are -- and DESIGN section 4 puts surface arity in the sugar layer that adds no power. Declaring concat's signature absent was refused because the signature is expressible and true; erasing a fact that holds is a different failure from asserting one that does not. POPULATION: measured over dag, src/v1 and src/v2 with a scanner that skips string literals -- 12 free-call sites at arity 1, 8297 at 2, 507 at 3, 200 at 4, 178 at 5, and a tail to 262, across 64 distinct arities, roughly 1200 sites above binary. Closes by re-measurement, not by opinion. RESTORATION TRIGGER: n-ary application of a binary operation DECLARED ASSOCIATIVE folds to nested binary application -- SUFFICIENT FOR accepting concat's 64 measured arities against its unchanged binary declared signature, with no exemption and no widened vocabulary. Its own prerequisite is that associativity be declarable at all, which today it is not; that grounding is a DESIGN section 5 wall-after-grounding rather than a ratchet, since associativity of a declared operation is a modeled fact and not an undecidable one." }

data dashboard_merge_ready_semantic_admissibility: RungDrop = RungDrop { identity: "dashboard_merge_ready_semantic_admissibility" as NonEmptyStr, subject: "Dashboard MergeReady omits repository-semantic admissibility", declared: "2026-09-01", standing: Standing, authored: "**THE DASHBOARD REPORTS `MergeReady` WITHOUT CONSUMING WHETHER THE CHANGE IS SEMANTICALLY ADMISSIBLE TO ITS REPOSITORY (2026-09-01).** The dashboard's `pr_merge_ready_digest.mjs` `meetsMergeCriteria` constructs the verdict from review-vote tallies, absence of unresolved or request-changes reviews, GitHub's conflict-free `mergeable` observation, and a non-failing check summary. Those are real mechanical facts, but they do not answer the separate repository-semantic question required by the working agreement: whether the diff actually satisfies its request and the repository's authority documents. An approval explicitly means only that its reviewer found no blocking defect; it is not evidence that the requested change was delivered. Calling their join `MergeReady` therefore turns an incomplete projection into an affirmative operational instruction and can page an operator to land a mechanically clean change that misses its request. EXECUTED SPECIMEN, observed 2026-09-01 with gunbc#9932 at `cc1f3ff60` against main at `6bdc9492c2`: `meetsMergeCriteria` emitted `ready=true` while the decision-time instrument `git merge-tree --write-tree origin/main cc1f3ff60` returned `rc=1`. Both are re-derivable at those two pinned subjects: the driver verdict deterministically, and the dashboard verdict by replaying its named predicate over the same head. The review tallies and check summary that fed that verdict are deliberately NOT recorded here — a vote count on a head is a mutable population with no producer that re-derives it, and copying one would be the transcription this document forbids. The generated-artifact driver refuses `GeneratedArtifactConcurrentDivergence` when both sides changed a generated projection since the merge base; GitHub's plain text-merge verdict never invokes that driver, so its merge can succeed with no conflict, marker or signal while yielding bytes that project neither side's authorities. The repository-semantic answer was Refused while every fact the dashboard consumes admitted the PR. Naming both immutable subjects and the producer makes this the gap firing in production, not a conclusion transcribed from a moving PR. PREVIOUS RUNG: mitigatable — the worker or manager had to reread the request and authority documents before declaring readiness, so the missing semantic fact was bounded only by human diligence and was never a mechanical guarantee. TEMPORARY RUNG: below the ladder on the dashboard-verdict path — no `RepositoryMergeAdmissibility` observation enters the constructor, no typed unknown or refusal is carried, and the affirmative verdict is indistinguishable from one whose semantic admission was actually decided. The review, CI and conflict paths retain their own mechanically preventable rungs; this row does not lower or relabel them. REASON: the dashboard automated the mechanical half of the decision and named the projection after the whole decision without first modeling the other half. BOUNDED POPULATION: every `merge_ready` digest entry constructed by `meetsMergeCriteria`, including its stale-entry revalidation through the same predicate; parent and manager notifications are projections of those entries and are not separate instances. OUTSIDE-THE-MODEL BOUNDARY: semantic admissibility may ultimately require judgment, but that does not license fabricating `Admissible`; an undecided judgment is a first-class standing and must block the affirmative verdict. RESTORATION TRIGGER: in `gunb-ai/ctrl`, a typed `RepositoryMergeAdmissibility` input with at least admitted, refused and undecided standings is consumed by the one canonical merge-readiness predicate, and both initial construction and stale revalidation refuse to emit `MergeReady` unless the exact repository-and-head subject is `Admitted`. A boolean inferred from approvals, CI, GitHub `mergeable`, session state, or the absence of a recorded objection does not satisfy the trigger, because each merely renames a mechanical fact already present. The discriminating RED is an otherwise mechanically ready PR whose semantic standing is undecided or refused; the positive control is the same mechanical packet with an exact-head admitted receipt. The repair belongs to `gunb-ai/ctrl`, which owns the dashboard constructor; this repository records the rung honestly and does not mint a second merge-admission authority." }

data namespace_admission_consumed_row_deletion: RungDrop = RungDrop { identity: "namespace_admission_consumed_row_deletion" as NonEmptyStr, subject: "Consumed-row deletion obligation on the namespace transition-admission roster", declared: "2026-09-02", standing: Retired { trigger_fired: "2026-09-02" as NonEmptyStr }, authored: "Namespace wave admission -- **RUNG DROP, DECLARED (2026-09-02).** gunbc#9824 split ConsumedByMerge from UnmatchedAdmission so that a row whose admitted relocation the base already satisfies stops refusing unrelated pull requests, and it carried its own deletion obligation in one arm: consumed rows are due, and refuse, on the first change whose diff touches the roster source file itself. PREVIOUS RUNG: 2, mechanically preventable. Before that split a row past its life reported stale and refused every run, so the obligation was enforced by a mechanism that executed -- at the cost of billing the enforcement to bystanders, which is the externalized degradation #9824 was authorized to remove. TEMPORARY RUNG: 1, mitigatable. A consumed row is now a typed receipt printed by every run and nothing else, and its removal depends on a human reading that receipt. THIS ROW CORRECTS #9824 RATHER THAN RESTATING IT, AND THE CORRECTION IS THE REASON THE DROP IS DECLARED AT ALL. That pull request states its window as wall-clock unbounded, roster-use bounded, bystander-invisible. The first and third conjuncts hold. The second is FALSE IN EXECUTION: v1_compiler.cli_run.namespace_wave_admission.run_required_wave_admission derives roster_touched from the head side produced by diff_sides, whose final act retains only paths satisfying in_sweep_scope, and that predicate opens by requiring a .dag suffix -- while ADMISSION_ROSTER_REL_PATH names a .rs file. A .rs path cannot survive a .dag filter, so roster_touched is false on every production run, consumed_due in claim_executor.report_wave_admission_outcome can never be true, and the roster-use bound does not exist. REASON, and it is not a bug in the filter: in_sweep_scope answers WHICH FILES THE PARSER RE-READS to reconstruct the baseline, a different question asked for a different purpose, and nothing joins it to the deletion obligation it silently decides. That is the mechanism gunbc.recurring_failure_mode carries as incidental_denominator_as_wall, cited here at the polarity where the accident KILLS a declared wall rather than accidentally holding one up. The discriminating fact is already executed in this repository: tests/namespace_wave_admission.rs a_rename_contributes_its_source_to_the_base_side_and_its_destination_to_the_head_side asserts that a src/v1/stage0/src path enters neither side of the diff. POPULATION, bounded and enumerable at every head: the rows of NAMESPACE_TRANSITION_ADMISSIONS for which admission_consumed_at_base holds against that run base. The population is closed by construction, since a row can enter it only by being authored into that const and the const is the single production construction site; at the head declaring this row it is exactly the two RLM-2b rows, consumed since the commit that authored them, which is also the merge of the relocation they admit. The lifetime the population sits in is measurable and is not the roster lifetime: an admission is TRUE of a diff only from its authoring until its own pull request merges, and RESIDENT on main only from that merge until a human deletes it, two disjoint intervals separated by that merge, of which the second can never match a delta and is therefore pure liability. The disjointness carries one honest caveat: a branch that MERGES main in moves its merge base past the relocation, so no delta reappears, while a branch that cherry-picks instead could reopen the first interval -- no cohort in the recorded history did this, and the caveat is stated rather than assumed away. Re-derive the record with git log over src/v1/stage0/src/namespace_wave_admission.rs, reading added and removed label lines per commit. RESTORATION TRIGGER: the consumed-row deletion obligation is observed by a mechanism that EXECUTES on the required path -- SUFFICIENT FOR a consumed row standing on a roster-touching change refusing that change, established by a discriminating RED authored on the acceptance path rather than over a hand-built outcome value. That restores rung 2 and waits on no carrier. It is deliberately not the larger climb: admissions bound to the delta content they admit, adjudicated per run and never resident on main -- SUFFICIENT FOR making a row that is not about this run diff unwritable -- is what retires the roster itself, and this row is not retired by it.RETIRED THE SAME DAY IT WAS DECLARED, BY ITS TRIGGER AND BY NOTHING ELSE (2026-09-02). gunbc#10014 landed at 962d9288ab2: diff_sides now reports what a change touched ONCE and unfiltered, each consumer applies the scope its own question needs at its own point of use, and the verdict moved off the executor onto the wall as wave_admission_refusal. roster_touched is therefore reachable on the required path and the consumed-row deletion obligation is observed by a mechanism that executes, which is the capability this row named. THE WINDOW WAS REAL AND THE ROW IS KEPT AS ITS RECORD rather than deleted: it ran from gunbc#9824 on 2026-08-31, when the obligation was declared over an arm that could not fire, to gunbc#10014 today. ONE EVIDENCE OBLIGATION REMAINS OPEN ON THE RESTORED CAPABILITY AND IS NAMED HERE RATHER THAN LEFT TO BE REDISCOVERED: the obligation is observed by a PAIR of executing probes -- one establishing that the roster path reaches the side roster_touched reads, one establishing that a consumed row on a roster-touching run refuses while a bystander stays admitted -- and not yet by a single probe that walks a real diff through to a refusal. That is evidence owed on a capability that exists, which is a different thing from a capability that does not, so it is recorded as an obligation and is neither a new drop nor a next-rung trigger." }

data spark_serving_local_artifact_not_reproducible: RungDrop = RungDrop { identity: "spark_serving_local_artifact_not_reproducible" as NonEmptyStr, subject: "Reproduction of the Spark serving cell's model artifact from desired state", declared: "2026-09-02", standing: Standing, authored: "Spark serving model materialization — **RUNG DROP, DECLARED (2026-09-02).** SUBJECT: the ability to reconstruct a serving cell's model artifact from desired state alone. WHAT WAS HELD: while `gunbc.spark.serving_desired` `spark_serving_desired_manifest` selected an upstream library tag, `gunbc.spark.serving_converge_realize` `spark_serving_materialize_model_artifact_steps` emitted a complete fetch-and-verify install plan — manifest fetched by reference, checked against the frozen resolved digest, every blob in the closure fetched by digest, staged, verified and only then published. A cell with an empty model store could be converged into a serving one. WHAT IS LOST: desired state now selects `deepseek-v4-gguf:no-h3-stop`, which was produced by `POST /api/create` ON THE CELLS THEMSELVES and has no registry anywhere. The materializer REFUSES for it, so convergence can verify and serve the artifact but cannot rebuild it: a cell that lost its model store cannot be restored by this plan. WHY THE REFUSAL IS NOT ITSELF THE DEFECT: the alternative was emitting `curl` against a registry path that never existed, which fails at apply time on a real host with a transport error that reads as a network fault rather than as the category error it is; and the OTHER alternative — silently degrading to a verify-only plan — is the absorbing fallback, actuating as 'nothing to do' against a host with nothing installed. The line stops, typed and located, naming the producer. WHAT REMAINS: the upstream arm is untouched and still executes its full sequence, and stays enrolled as executing evidence via `test.claim.spark_serving_model_materialization_witness`, which now names `gpt_oss_120b_manifest` explicitly rather than reading desired state — precisely so this arm does not become green-by-vacuity while unselected. PREVIOUS RUNG: mechanically preventable. TEMPORARY RUNG: mitigatable — the gap is refused rather than silent, but the artifact's existence on the cells is an external fact this repository observes and cannot reproduce. RESTORATION TRIGGER — THE CAPABILITY, NOT AN ARTIFACT: a locally materialized manifest can be CONSTRUCTED by the convergence plan from facts this repository owns — the parent artifact's identity and blob closure, and the transformation applied to it — such that a cell with an empty model store converges to the byte-identical resolved identity without a human running `ollama create`. Modeling the Modelfile alone does NOT discharge this row: the plan must construct the artifact and the resulting identity must be checkable against the frozen resolution, or the same unreproducible state persists behind a row that reads as covered." }
Expand All @@ -140,6 +142,7 @@ data rung_drop_roster: List<RungDrop> = [
spark_role_scoped_retirement_production_root,
builtin_signature_arity_pairing_fabricates,
concat_binary_signature_exempt_from_arg_binding,
dashboard_merge_ready_semantic_admissibility,
namespace_admission_consumed_row_deletion,
spark_serving_local_artifact_not_reproducible,
]
Expand Down
Loading
Loading