Skip to content
Closed
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
6 changes: 3 additions & 3 deletions dag/gunbc/design_ledgers.dag
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ import gunbc.plans.md_helpers { h2, h3, p, li, ul, hr }
import extdeps.languages.markdown { serialize_markdown_source }
import gunbc.recurring_failure_mode { authored }
import gunbc.recurring_failure_mode.roster { recurring_failure_mode_roster }
import gunbc.rung_drop { rung_drop_declaration_message, RungDropStanding, Standing, Retired }
import gunbc.rung_drop { rung_drop_declaration_message, rung_drop_amendment_message, RungDropStanding, Standing, Retired }
import gunbc.rung_drop.roster { rung_drop_roster }
import v2.workflow.floor_discovery { floor_discovery_tree_identity }
import gunbc.self_host_compile_phase_frontier {
Expand Down Expand Up @@ -125,9 +125,9 @@ fn rung_drop_blocks() -> List<MarkdownBlock> {
],
flat_map(rung_drop_roster, d => concat(concat([
h3(text: concat(concat(concat(d.subject, " — declared "), d.declared), rung_drop_standing_suffix(standing: d.standing))),
], rung_drop_standing_blocks(standing: d.standing)), concat([
], rung_drop_standing_blocks(standing: d.standing)), concat(concat([
p(text: rung_drop_declaration_message(d: d)),
], if (d.identity as String) == "measurement_bankruptcy" {
], map(d.amendments, a => p(text: rung_drop_amendment_message(a: a)))), if (d.identity as String) == "measurement_bankruptcy" {
compile_phase_frontier_blocks()
} else { [] }))),
],
Expand Down
41 changes: 41 additions & 0 deletions dag/gunbc/rung_drop.dag
Original file line number Diff line number Diff line change
Expand Up @@ -301,12 +301,53 @@ type RungDropDeclaration
}
| AuthoredProse { legacy: LegacyProseIdentity, authored: String }

// A LATER RULING MOVED THE WORLD UNDER A STANDING DROP, AND THE DECLARATION HAD NOWHERE TO SAY SO.
// DESIGN section 4b(3) names five fields, all of them about the MOMENT the rung fell: previous,
// temporary, reason, population, trigger. None of them can carry a fact established AFTERWARDS that
// changes how the declaration should be read -- and one such fact was written into
// docs/design-rung-drops.md by hand on 2026-09-20, in a file that module's own note says is
// generated from this roster. It survived one regeneration as unexplained drift on two lanes
// (gunbc#11732 reverted the deletion; gunbc#11786 was left holding nothing but it) and was then
// regenerated away on main by gunbc#11789, which is the silent loss DESIGN section 6 calls manual
// application committed as source: the prose dies and the diff that kills it looks like noise.
//
// THIS IS NOT A COMMENTARY FIELD AND IS DELIBERATELY NOT ONE. A free-text note on a drop would be
// the absorbing fallback with a nicer name -- every sentence nobody could place would land in it.
// An amendment is a specific thing with three parts and no fourth: WHEN the later fact was
// recorded, WHAT it was (cited, so a reader can reach it), and WHAT IT DOES to this declaration.
// The third part is the load-bearing one, because the whole reason to carry an amendment rather
// than edit the row is that the declaration itself did NOT change: the trigger a drop is retired by
// is the trigger it was declared with, and an amendment that silently rewrote it would retire a
// drop by something other than its trigger, which 4b(3) forbids.
//
// WHY NOT AN ANNOTATION. The reasoning below already exists as a source annotation on the row that
// needs it, and that is exactly why the paragraph went missing: DESIGN section 4c states that no
// Accepted program can read an annotation, so the projection could not and did not. A fact a
// generated document must carry is program data, not commentary.
type RungDropAmendment {
amended: String
occasion: NonEmptyStr
consequence: NonEmptyStr
}

// THE ONE RENDERING, for the reason rung_drop_declaration_message is the one rendering of a
// declaration: a second speller of an amendment would drift from the row it amends.
fn rung_drop_amendment_message(a: RungDropAmendment) -> String {
concat(
concat("AMENDED ", concat(a.amended, ": ")),
concat(a.occasion, concat(" -- ", concat(a.consequence, ".")))
)
}

// `amendments` IS ORDINARILY EMPTY AND IS A LIST RATHER THAN AN OPTION because the world can move
// under one declaration more than once, and a second amendment must not overwrite the first.
type RungDrop {
identity: NonEmptyStr
subject: String
declared: String
standing: RungDropStanding
declaration: RungDropDeclaration
amendments: List<RungDropAmendment>
}

// THE ONE RENDERING, so a refusal arm never restates the row beside it. A gate that spelled its
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -70,5 +70,7 @@ data accumulator_copy_positive_controls_off_every_lane: RungDrop = RungDrop {
"v2.test.long.accumulator_copy_fold_analysis an_inline_step_beside_a_decoy_lambda_is_still_caught",
],
restoration_trigger: "an executing lane with a declared ceiling plans an ingest-reaching hermetic witness: either the per-frame front end is paid once per run so these enroll as test fns on ordinary discovery inside the enrolment margin (the restoration trigger of long_module_changed_witness_cpu_observed_only), or a scheduled substrate-long executor is re-added under the operator agreement gunbc#8283 reserved. Observed at retirement, not asserted: the six population identities are test fns planned by a live cadence and reach PASS on a required or scheduled run, and this row retires in the same change. Passing under claim_batch is the declared state, not the trigger."
}
},

amendments: [],
}
Original file line number Diff line number Diff line change
Expand Up @@ -12,5 +12,7 @@ data builtin_signature_arity_pairing_fabricates: RungDrop = RungDrop {

standing: Standing,

declaration: AuthoredProse { legacy: BuiltinSignatureArityPairingFabricates, authored: "Builtin signature grounding -- **RUNG DROP, DECLARED (2026-09-01).** PREVIOUS RUNG: none to lower -- this declares that a class created by this change lands below its attainable ceiling rather than at it. v1.compiler.infer_method pairs each row's DECLARED parameter names with the parameter TYPES derived from std.algebra. When the two lists disagree in length, pair_declared_names yields AlgebraTypeVariable { id: \"unpaired_declared_parameter\" } for the unpaired position instead of refusing. That is a value standing where a refusal belongs -- DESIGN section 5's fabricated-plausible-output arm -- and it is declared here rather than left as a marker that reads like a wall. TEMPORARY RUNG: mitigatable. The marker is distinctive, greppable, and reaches src/v1/stage0/src/v1_compiler_infer_method.rs, so a mismatch is DISCOVERABLE by inspection of a generated artifact. It is not mechanically preventable, because NO CONSUMER ASSERTS ITS ABSENCE: an unchecked marker is an inert lens, and DESIGN is explicit that the tier where the machinery exists and nothing gates on it is itself a lie. REASON: builtin_function_registry is a `data` initializer and a .dag data initializer has no refusal channel -- there is nowhere at construction for a typed, located diagnostic to go, so the only arms available were a fabricated value or a silently shorter list, and a marked fabrication is the more honest of the two. POPULATION: bounded and closed at 20 rows -- exactly the registry names that std.algebra also declares and that therefore pair at all (count, to_int, substring, to_string, concat, map_insert, map_merge, with, map_contains_key, map_has, lookup, map_get, map_keys, map_values, get, reverse, list_push, length, starts_with, replace). The other 112 rows author their types directly and cannot reach this arm. Zero occurrences of the marker in the tree today, which is the state this row exists to keep observable. RESTORATION TRIGGER: construction-time refusal available inside a `data` initializer -- SUFFICIENT FOR a declared/derived arity disagreement to stop the line with a typed, located diagnostic at the row that causes it, rather than to produce a marked value that construction accepts. The trigger names that capability and not any artifact that would contribute to one; a witness asserting the marker's absence would raise this to mechanically preventable but would NOT retire the row, because the invalid state would still be writable." }
declaration: AuthoredProse { legacy: BuiltinSignatureArityPairingFabricates, authored: "Builtin signature grounding -- **RUNG DROP, DECLARED (2026-09-01).** PREVIOUS RUNG: none to lower -- this declares that a class created by this change lands below its attainable ceiling rather than at it. v1.compiler.infer_method pairs each row's DECLARED parameter names with the parameter TYPES derived from std.algebra. When the two lists disagree in length, pair_declared_names yields AlgebraTypeVariable { id: \"unpaired_declared_parameter\" } for the unpaired position instead of refusing. That is a value standing where a refusal belongs -- DESIGN section 5's fabricated-plausible-output arm -- and it is declared here rather than left as a marker that reads like a wall. TEMPORARY RUNG: mitigatable. The marker is distinctive, greppable, and reaches src/v1/stage0/src/v1_compiler_infer_method.rs, so a mismatch is DISCOVERABLE by inspection of a generated artifact. It is not mechanically preventable, because NO CONSUMER ASSERTS ITS ABSENCE: an unchecked marker is an inert lens, and DESIGN is explicit that the tier where the machinery exists and nothing gates on it is itself a lie. REASON: builtin_function_registry is a `data` initializer and a .dag data initializer has no refusal channel -- there is nowhere at construction for a typed, located diagnostic to go, so the only arms available were a fabricated value or a silently shorter list, and a marked fabrication is the more honest of the two. POPULATION: bounded and closed at 20 rows -- exactly the registry names that std.algebra also declares and that therefore pair at all (count, to_int, substring, to_string, concat, map_insert, map_merge, with, map_contains_key, map_has, lookup, map_get, map_keys, map_values, get, reverse, list_push, length, starts_with, replace). The other 112 rows author their types directly and cannot reach this arm. Zero occurrences of the marker in the tree today, which is the state this row exists to keep observable. RESTORATION TRIGGER: construction-time refusal available inside a `data` initializer -- SUFFICIENT FOR a declared/derived arity disagreement to stop the line with a typed, located diagnostic at the row that causes it, rather than to produce a marked value that construction accepts. The trigger names that capability and not any artifact that would contribute to one; a witness asserting the marker's absence would raise this to mechanically preventable but would NOT retire the row, because the invalid state would still be writable." },

amendments: [],
}
Loading