Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
91821b0
Delete world_converge at the root: read-only policy was bound as an a…
Sep 8, 2026
faa28d6
Merge remote-tracking branch 'origin/main' into session/sleek-newt-698
Sep 8, 2026
5ec3876
Delete goal_is_satisfied: a one-bit summary of a four-arm coproduct, …
Sep 8, 2026
bb52ab4
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 8, 2026
eb5dd6c
Enroll the new witnesses as test fn, and attach the is_satisfied rati…
Sep 8, 2026
59576d5
Merge remote-tracking branch 'origin/session/sleek-newt-698' into ses…
Sep 8, 2026
4573a5a
Merge remote-tracking branch 'origin/main' into session/sleek-newt-698
Sep 8, 2026
18dfb42
Delete the dead binding fixture and every import that outlived its co…
Sep 8, 2026
8255cea
Remove the assessor's remaining short-circuit: a one-dimension goal d…
Sep 8, 2026
cc8670d
Merge remote-tracking branch 'origin/main' into session/sleek-newt-698
Sep 8, 2026
ce584c0
Merge remote-tracking branch 'origin/main' into session/sleek-newt-698
Sep 8, 2026
a14a66d
Fix forward the world_converge census that fired at merge time, not a…
Sep 8, 2026
c6a2626
State the trigger for GoalAssessmentRefused: a declared frontier, not…
Sep 8, 2026
756fb21
Move the unreachable-arm rationale to module-item grain: an in-body a…
Sep 8, 2026
4978326
Merge remote-tracking branch 'origin/main' into session/sleek-newt-698
Sep 8, 2026
b2a2e1e
Restore the rationale two surviving witnesses lost with their deleted…
Sep 8, 2026
22b47bd
chore: regenerate drifted generated artifacts (ci auto-heal)
Sep 8, 2026
f54790b
Restore the parameter seam that makes the merge-queue unknown reachable
Sep 8, 2026
1020adf
Merge remote-tracking branch 'origin/main' into session/sleek-newt-698
Sep 8, 2026
d8f366c
Reconstruct a derived source at the base revision instead of inheriti…
Sep 8, 2026
3af78c5
Merge remote-tracking branch 'origin/main' into session/sleek-newt-698
Sep 8, 2026
fd0098e
Check that base and head share one renderer, and pay the consumed row…
Sep 8, 2026
43b7856
Restore the record my deletion left headless, and re-tense seven dead…
Sep 8, 2026
26f123a
Delete the dissolution record my own edit duplicated, and the stale e…
Sep 8, 2026
d24dc45
Merge remote-tracking branch 'origin/main' into session/sleek-newt-698
Sep 8, 2026
99a213a
Record why the gunbc#10813 admission row went with this merge
Sep 8, 2026
fe50f1d
Merge remote-tracking branch 'origin/main' into session/sleek-newt-698
Sep 8, 2026
6f90b0d
Yield the baseline-reconstruction fix to main's, which landed the sam…
Sep 8, 2026
c5ea502
Migrate the four world_converge consumers main added while this branc…
Sep 8, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ The reviewer's question is therefore two-part and both halves are located: for e

## 3d. Selection precedes convergence

**Selection precedes convergence.** A convergence primitive (`gunbc.world_converge`, `ensure`) neither enumerates subjects nor chooses a realization: it decides Noop/Apply/Refuse over a caller-supplied requirement with independent readback. Generating candidates or choosing policy inside convergence is the conflation this section forbids. The missing authority sits *before* those folds, in `std.decision`.
**Selection precedes convergence.** A convergence primitive (`std.goal_assessment`, `ensure`) neither enumerates subjects nor chooses a realization: it assesses a caller-supplied goal against an independent observation, or decides Noop/Apply/Refuse over a caller-supplied requirement with independent readback. Generating candidates or choosing policy inside convergence is the conflation this section forbids. The missing authority sits *before* those folds, in `std.decision`.

**Pareto assessment is not realization selection.** `std.pareto` computes dominance and the frontier — axis identities rather than positional alignment, per-axis orientation, interval-valued readings, `Incomparable` separated from `DominanceUndecided`, and refusal on missing or duplicated funded-axis readings. A Pareto front of two is not a winner. Realization selection is the policy-bound operation that can produce one desired realization; it **consumes** `std.pareto` and must not redeclare dominance, axis orientation, intervals, or evidence-gap vocabulary. Growing a second decision algebra beside Pareto is the §3 fork this law exists to prevent.

Expand Down
4 changes: 2 additions & 2 deletions dag/gunbc/design_argument.dag
Original file line number Diff line number Diff line change
Expand Up @@ -289,12 +289,12 @@ data design_section_2_to_7_rows: List<DesignRow> = [
DesignRow {
proposition: Proposition {
id: "s3d.selection-precedes-convergence",
statement: "selection precedes convergence: Pareto assessment (std.pareto) computes the frontier and realization selection (std.decision) is the policy-bound choose-one, consuming Pareto without redeclarating its algebra; world_converge and ensure do not enumerate candidates or choose policy",
statement: "selection precedes convergence: Pareto assessment (std.pareto) computes the frontier and realization selection (std.decision) is the policy-bound choose-one, consuming Pareto without redeclarating its algebra; goal assessment and ensure do not enumerate candidates or choose policy",
premises: ["s3.single-authority", "s5.fail-closed", "s1.minimal-safe-efficient"]
},
review: ReviewableOnChange { parts: [yes_no_review(
part: "selection-precedes-convergence",
question: "Does the change choose or converge a realization while the candidate field, constraints, funded-axis evidence or policy are unresolved; redeclare Pareto dominance/orientation/interval/gap vocabulary; treat a Pareto front as a winner; mint SelectedWithin over an incomplete closure; or widen world_converge/ensure into candidate generation or policy choice?",
question: "Does the change choose or converge a realization while the candidate field, constraints, funded-axis evidence or policy are unresolved; redeclare Pareto dominance/orientation/interval/gap vocabulary; treat a Pareto front as a winner; mint SelectedWithin over an incomplete closure; or widen goal assessment (std.goal_assessment) / ensure into candidate generation or policy choice?",
tells: [
"a convergence or ensure path that enumerates candidates or selects a realization",
"a second dominance, orientation, interval or evidence-gap algebra beside std.pareto",
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/design_document.dag
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ fn section_3c_blocks() -> List<MarkdownBlock> {
fn section_3d_blocks() -> List<MarkdownBlock> {
[
h2(text: "3d. Selection precedes convergence"),
p(text: "**Selection precedes convergence.** A convergence primitive (`gunbc.world_converge`, `ensure`) neither enumerates subjects nor chooses a realization: it decides Noop/Apply/Refuse over a caller-supplied requirement with independent readback. Generating candidates or choosing policy inside convergence is the conflation this section forbids. The missing authority sits *before* those folds, in `std.decision`."),
p(text: "**Selection precedes convergence.** A convergence primitive (`std.goal_assessment`, `ensure`) neither enumerates subjects nor chooses a realization: it assesses a caller-supplied goal against an independent observation, or decides Noop/Apply/Refuse over a caller-supplied requirement with independent readback. Generating candidates or choosing policy inside convergence is the conflation this section forbids. The missing authority sits *before* those folds, in `std.decision`."),
p(text: "**Pareto assessment is not realization selection.** `std.pareto` computes dominance and the frontier — axis identities rather than positional alignment, per-axis orientation, interval-valued readings, `Incomparable` separated from `DominanceUndecided`, and refusal on missing or duplicated funded-axis readings. A Pareto front of two is not a winner. Realization selection is the policy-bound operation that can produce one desired realization; it **consumes** `std.pareto` and must not redeclare dominance, axis orientation, intervals, or evidence-gap vocabulary. Growing a second decision algebra beside Pareto is the §3 fork this law exists to prevent."),
p(text: "The result is scoped, never `Optimal`: `SelectedWithin` binds a `SelectionReceipt` (decision subject, candidate-field identity and standing, constraint authority, funded axes, evidence snapshot, Pareto survivors, policy authority, selected identity). A different field, constraint set, evidence snapshot, funded-axis set or policy is a **different decision**, so a stale choice is mechanically detectable. Unresolved evidence is `SelectionNeedsEvidence`; two non-dominated survivors without a policy is `SelectionNeedsPolicy`; an attractive candidate that violates a hard constraint is excluded *before* Pareto, never ranked. Completeness of the subject — required (objective-term × decision-variable) cells as an identity join, invariance as a three-place relation, term drops only with order-preservation — remains a closed-subject obligation of the same home: absence is not irrelevance, and `SelectedWithin` may not mint over an incomplete closure."),
p(text: "This is also why §6 does not independently carry \"prioritize holistically\": ranking work on a funded multi-axis field rather than a bottleneck KPI **is** this law applied to authorship. Home: `std.decision`. A conformance domain is admitted only once that home is the consumed authority — a domain without a home remains a modeling obligation (§6), not a conformance row (§3b)."),
Expand Down
102 changes: 49 additions & 53 deletions dag/gunbc/product/cable_plant_converge.dag
Original file line number Diff line number Diff line change
Expand Up @@ -12,14 +12,14 @@ import product.cable_leg_observation {
LegComplianceCodeNotUnderstood,
assess_cable_leg,
}
import gunbc.world_converge {
WorldObservation, WorldObserved, WorldUnobservable,
WorldDifference, WorldInAgreement, WorldDiverged,
WorldActuation, WorldApplied, WorldActuationRefused,
WorldConvergenceHandler,
WorldConvergenceResult, WorldConverged, WorldNotConverged,
world_converge,
import std.goal_assessment {
ObservationAttempt, ObservationEstablished, ObservationRefused,
GoalAssessment,
GoalInspection,
inspect_goal,
assess_by_deviations,
}
import v2.std.cardinality { Never }

// THE INSTALLED CABLE PLANT AS A CONVERGENCE SUBJECT.
//
Expand All @@ -29,19 +29,32 @@ import gunbc.world_converge {
// standing question "does the copper in the floor still attest what we need", asked of the same
// observation carrier and answered through the one global convergence shape.
//
// WHY IT IS BOUND TO gunbc.world_converge AND NOT GIVEN ITS OWN LOOP. Observe, difference, actuate,
// receipt is not a cabling idea; it is THE convergence idea, and that authority is subject-agnostic
// by construction. A second loop authored here would be a fork of it (DESIGN section 3) and would
// arrive with its own opinion about what "converged" means.
// WHY IT IS BOUND TO std.goal_assessment AND NOT GIVEN ITS OWN LOOP. Observe then assess is not a
// cabling idea; it is THE assessment idea, and that authority is subject-agnostic by construction.
// A second loop authored here would be a fork of it (DESIGN section 3) and would arrive with its
// own opinion about what "agreement" means.
//
// THE ACTUATION ARM IS A REFUSAL, AND THAT IS THE HONEST RUNG, NOT A GAP. A transceiver's coding
// IT NO LONGER CARRIES AN ACTUATION ARM, AND THAT IS WHY THIS READS BETTER THAN IT DID. The shape
// it used to bind DEMANDED an `apply`, so this module supplied one that could only refuse -- and
// that refusal then shared a coproduct with the two causes meaning the plant could not be OBSERVED
// at all. An unread leg and a miscoded leg both arrived as "not converged, here is a refusal",
// which is one verdict answering two different questions. The observation layer now refuses on its
// own and the assessment reports deviations on its own, so a reader tells "we could not look" from
// "we looked and it is wrong" without inspecting the cause.
//
// THE INABILITY TO REPAIR IS THE HONEST RUNG, NOT A GAP. A transceiver's coding
// lives in EEPROM on the leg itself; writing it needs the vendor's programmer and their part
// definition. This repository can observe the plant and can say exactly which legs diverge, and it
// cannot repair one. DESIGN section 4b calls that column "outside the modeled guarantee": observed,
// refused, or mitigated at a declared boundary, never fabricated. So divergence terminates at
// `PlantCodingCannotBeActuatedHere` CARRYING THE DIVERGENT LEGS -- a located, countable refusal,
// which is what the operator can act on -- rather than at a silent no-op that would let an
// unrepaired plant read as converged.
// `GoalDiverged` CARRYING THE DIVERGENT LEGS -- located and countable, which is what the operator
// can act on -- rather than at a silent no-op that would let an unrepaired plant read as agreeing.
//
// THAT TERMINUS USED TO BE A REFUSAL CAUSE, `PlantCodingCannotBeActuatedHere`, and it is deleted
// rather than kept: it existed only because the old shape had nowhere else to put a divergence once
// the actuator refused, so it restated as a REFUSAL what the difference list already carried as a
// VALUE. Two representations of one fact, and the weaker one was the arm the reader reached first.
// The divergent legs now arrive as deviations, which is the same information without the fork.
//
// DISSOLVE-ON, NAMED AS A CAPABILITY: an admitted realization that writes a leg's extended
// specification compliance bytes AND READS THEM BACK off the same leg afterwards. A programmer that
Expand Down Expand Up @@ -93,7 +106,6 @@ type CableLegOutcome sole_constructor {
type CablePlantRefusal
= PlantLegNeverRead { endpoint: NonEmptyStr }
| PlantHoldsNoLegs { plant: NonEmptyStr }
| PlantCodingCannotBeActuatedHere { divergences: List<CableLegOutcome> }

type CablePlantReceipt sole_constructor {
legs_read: Nat
Expand Down Expand Up @@ -180,49 +192,37 @@ fn plant_read_legs(subject: CablePlant) -> List<ObservedLeg> {
// where narrowing the population to what could be measured makes an unmeasured plant indistinguishable
// from a healthy one. An empty plant refuses for the same reason one rung further out -- zero legs
// trivially agree, and a subject that converges because nothing is in it carries no information.
fn world_observe_cable_plant(
fn observe_cable_plant_attempt(
subject: CablePlant,
context: Bool,
) -> WorldObservation<CablePlantObserved, CablePlantRefusal> {
_: Bool,
) -> ObservationAttempt<CablePlantObserved, CablePlantRefusal> {
match plant_unread_endpoints(subject: subject).first() {
Present { value: e } => WorldUnobservable { cause: PlantLegNeverRead { endpoint: e } }
Present { value: e } => ObservationRefused { cause: PlantLegNeverRead { endpoint: e } }
Absent => {
let legs = plant_read_legs(subject: subject)
match legs.first() {
Absent => WorldUnobservable { cause: PlantHoldsNoLegs { plant: subject.plant } }
Present { value: l } => WorldObserved { value: CablePlantObserved { legs: legs } }
Absent => ObservationRefused { cause: PlantHoldsNoLegs { plant: subject.plant } }
Present { value: l } => ObservationEstablished { observed: CablePlantObserved { legs: legs } }
}
}
}
}

fn world_cable_plant_differences(
subject: CablePlant,
context: Bool,
observed: CablePlantObserved,
) -> WorldDifference<CableLegOutcome> {
let divergences = plant_divergent_outcomes(subject: subject, observed: observed)
match divergences.first() {
Absent => WorldInAgreement
Present { value: d } => WorldDiverged { differences: divergences }
}
}

fn world_cable_plant_apply(
fn assess_cable_plant(
subject: CablePlant,
context: Bool,
observed: CablePlantObserved,
differences: List<CableLegOutcome>,
) -> WorldActuation<CablePlantReceipt, CablePlantRefusal> {
WorldActuationRefused { cause: PlantCodingCannotBeActuatedHere { divergences: differences } }
) -> GoalAssessment<CablePlantReceipt, CableLegOutcome, Never, Never> {
assess_by_deviations(
evidence: cable_plant_agreement_receipt(subject: subject, observed: observed),
deviations: plant_divergent_outcomes(subject: subject, observed: observed),
)
}

// A CONVERGED PLANT STILL CARRIES ITS CONDITIONS. A leg attesting the required mode only under
// Clause 91 FEC has agreed, and the condition is a fact the deployment must honour -- so it rides in
// the receipt rather than being discarded on the way to a green.
fn world_cable_plant_unchanged_receipt(
fn cable_plant_agreement_receipt(
subject: CablePlant,
context: Bool,
observed: CablePlantObserved,
) -> CablePlantReceipt {
CablePlantReceipt {
Expand All @@ -231,17 +231,13 @@ fn world_cable_plant_unchanged_receipt(
}
}

type CablePlantConvergenceHandler = WorldConvergenceHandler<CablePlant, Bool, CablePlantObserved, CableLegOutcome, CablePlantReceipt, CablePlantRefusal>

data cable_plant_convergence_handler: CablePlantConvergenceHandler = WorldConvergenceHandler {
observe: world_observe_cable_plant,
differences: world_cable_plant_differences,
apply: world_cable_plant_apply,
unchanged_receipt: world_cable_plant_unchanged_receipt,
}

type CablePlantConvergence = WorldConvergenceResult<CablePlant, CablePlantObserved, CablePlantReceipt, CablePlantRefusal>
type CablePlantInspection = GoalInspection<CablePlant, CablePlantObserved, CablePlantReceipt, CableLegOutcome, Never, CablePlantRefusal, Never>

fn converge_cable_plant(subject: CablePlant) -> CablePlantConvergence {
world_converge(subject: subject, context: true, handler: cable_plant_convergence_handler)
fn inspect_cable_plant(subject: CablePlant) -> CablePlantInspection {
inspect_goal(
subject: subject,
scope: true,
observe: observe_cable_plant_attempt,
assess: o => assess_cable_plant(subject: subject, observed: o),
)
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
module gunbc.recurring_failure_mode.read_only_policy_bound_as_an_actuator_that_only_refuses

import std.types { NonEmptyStr }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data read_only_policy_bound_as_an_actuator_that_only_refuses: RecurringFailureMode = RecurringFailureMode {
identity: "read_only_policy_bound_as_an_actuator_that_only_refuses" as NonEmptyStr,

receipts: [
"**a subject that can only be READ is bound to an interface with an actuation stage, so the binding supplies an actuator whose every arm is a refusal** (the shape compiles, every claim over it passes, and nothing is obviously wrong -- the actuator is doing the safe thing. The defect is that the refusal vocabulary then grows to describe A WRITE THAT DOES NOT EXIST, and those causes are indistinguishable, at the type, from causes about the world. ",

"SPECIMEN (2026-09-07, gunbc.repo_ruleset against the deleted gunbc.world_converge). The repository-ruleset subject is observable and, under this repository's credential, unwritable: a whole-ruleset PUT would delete bypass actors the read cannot even enumerate. It was nonetheless bound to a six-parameter convergence handler carrying `apply`, so three of its seven refusal causes described the missing writer rather than the live ruleset -- an unbound actuation realization, a live rule a PUT would delete, a bypass roster a PUT would overwrite. ONE OF THE THREE WAS A SECOND REPRESENTATION OF A FACT THE DIVERGENCE LIST ALREADY CARRIED: an undeclared live rule was reported as the divergence `RulesetRuleUnexpected` AND as the actuation cause `RepositoryRulesetUnexpectedLiveRule`, free to disagree, with only the second reachable once a hold fired. ",

"**THE HARM IS ORDERING, AND IT ARRIVES LATER THAN THE MODELLING ERROR.** Refusals about the absent writer are checked BEFORE the comparison, because an actuator that cannot run has nothing to say about drift -- so the hold wins and the comparison is discarded. In the specimen the bypass roster is unreadable on EVERY live read, so the binding reported `the roster could not be read` unconditionally and NEVER reported that the enforcement, the required contexts or the ruleset name had also drifted. The one thing the subject existed to detect was suppressed by a refusal about a capability nobody was exercising. ",

"**THE TELL IS AN ACTUATION STAGE WITH NO GREEN ARM ANYWHERE IN THE CORPUS.** It is mechanically visible: the generic's own fixture bound `apply` to a constant refusal named `FixtureApplyShouldNotRun`, so the successful application path had never executed in the tree at all. An interface stage that no test and no production path can drive is not a conservative default; it is a stage whose contract is unmeasured, and it will be inherited by the next binding as though it were proven. ",

"**RECOGNITION RULE: if every arm a binding supplies for a stage is a refusal, the binding does not inhabit that stage -- ask whether the interface should have been the smaller one.** The repair is not a better refusal. It is to bind the READ-ONLY interface, delete the causes that described the absent writer, and let the facts they carried redistribute onto what they always were: an unreadable subject is an observation-layer refusal, an unread field is an unknown, an undeclared live rule is a deviation. ",

"SEPARATION FROM ITS NEIGHBOURS, since three rows are close. [[detector_promoted_to_an_actuator_predicate]] is the opposite direction -- something that only observes is made to decide an action. [[non_verdict_disposition_surfaces_as_refusal]] is about a disposition that is not a verdict being rendered as one, within a stage that legitimately exists. [[parallel_representation_debt]] covers the duplicated fact this specimen also carried, but not the ordering harm, which is the part that actually cost a finding. ",

"AND THE PRICE OF LEAVING IT: because the stage is structural, the misfiling compounds. Each new fact about why the write is unsafe arrives as another refusal cause rather than as an observation, so the subject's vocabulary drifts further from the thing it observes -- and the further it drifts, the more plausible the next refusal-shaped cause looks.)",
],

evidence: [],
}
Loading
Loading