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
2 changes: 1 addition & 1 deletion DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -137,7 +137,7 @@ The recursion's payoff is that **language design itself opens up.** It is normal

## Recurring failure modes (instances of §3–§5, kept for pattern-matching)

hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`None` meaning >2 things — split into named variants; its most-repeated form here is **not-applicable rendered as malformed** — one reason symbol over "the input is wrong" and "this strategy had nothing to say about it", which have opposite owners and opposite repairs. Found three times in three stages by one lane (#8801 and #8828 in body lowering, `parse_g0_tokens_remain` in parse), always by reading the producer and never from the message. Recognition rule: if the arm sits downstream of a search, lookup or alternative that returned `Absent`, it is not-applicable and needs its own reason. → [the conflation class](docs/probes/not_applicable_versus_malformed_conflation_class_2026-08-22.md)) · absorbing fallback (a failure arm that widens — rerun everything, scan all keys, always run — instead of refusing; ⊤-as-answer conflated with ⊤-as-ignorance; the deficit's frequency zeroed by construction, the corpus-denominated cost breaking the budget later) · **empty-observation narrow** (the absorbing fallback's mirror: ⊥-as-answer conflated with ⊥-as-ignorance — an observation that could not express what changed rendered as the verdict "nothing is affected", so the run narrows to nothing instead of widening. Strictly worse than the widen §5 already forbids: a widen is merely expensive, a narrow is silently uncovered. Live specimen: a push whose baseline ref *is* the pushed ref diffs the commit against itself, and the witness floor reported the resulting zero-path observation as "N unaffected (import-closure, skipped without resolve)" — receipt, two main pushes reporting an identical `4118 unaffected` on different commits, a skip count that cannot be a function of the diff. The tell that one observation is wrong rather than three local choices reasonable: its consumers disagree — compile-clean widened to whole-tree, regen gated on the event name, the witness floor skipped) · cache impurity (key on declared-input content; byte-identical cached-vs-cold is the purity oracle) · reflection evidence ≠ structural proof (prove a read axis by execution, with a no-host-enumeration control) · coercion proven by normalized round-trip, not a golden string · parallel-representation debt (an honestly-marked scaffold duplicating a canonical fact is still a violation) · internal review finds missing tests, external review finds missing checks · unmarked workaround (an author-side absorbing fallback — routing around an obstacle with no dissolution trigger; the line-stop signal, never a landing state) · **self-authorized dissolution** (temporary work treated as admissible because the author named its future deletion — a trigger is a lifecycle fact, not permission; without an operator verdict, marked debt is rejected exactly like unmarked debt) · positional citation (a `file:line` pointer where a symbol was available — see §3). · **authority substitution** (fact F lives in carrier A; operation O is governed by carrier B; A is cited as the evidence that O changed; no A→B relation is claimed by either carrier. Nothing asserted is false — the *entailment* is invented, which is why review reads past it: both halves check out and only the arrow between them is missing. It is §3's single-authority rule read in the direction authors actually violate it — not two authorities for one fact, but one authority borrowed to answer for another's. Receipt (gunbc#8865): an expecting-red probe was enrolled in `gunbc.explicit_witness_admission`, which DOCUMENTS a known red, and the PR asserted the required floor therefore held it; the floor gates on `v2.workflow.floor_expected_red` and nothing relates the two, so CI went red on a row its author had recorded as expected. The general tell is a sentence of the form *I registered it in A, so B now does X* where B is never named — and its structural fix is never a broader guard joining every A row to B, since that manufactures exactly the entailment being invented; the guard must carry the narrow predicate, with its exceptions declared.) · **reachability read as occupancy** (a guard's arm, disposition or check is deleted because nothing currently lands in it. Three questions are in play and only the first two decide whether it should exist: *mechanism existence* — can any governing authority produce this state; *join reachability* — can that mechanism classify an element of THIS operation's denominator; *current occupancy* — does anything receive it today. **Yes / yes / zero is a healthy guard being quiet, not a dead one**, and deleting it removes a live wall while looking principled. The distinction is load-bearing because it borders a true rule pointing the other way: a check whose RED IS UNREACHABLE — no authorable input can produce it — is a decoration, permanently green and worse than absent, because it is cited as coverage. Unreachable means the red cannot be produced at all; empty means it can and nothing does. Two corollaries, each from a lane that got it wrong first. Reachability is judged against what a FIXTURE MAY AUTHOR, never what the accepted corpus contains — a regression probe is an invalid program by definition, so a state no `Accepted` program holds is usually still authorable as source, and scoping reachability to corpus-expressible is this same conflation one layer out. And an arm is reachable relative to ONE operation: `gunbc.scm`'s path-exclusion disposition is unreachable from the floor's own fold, which drops excluded subjects before inventory, yet reachable from a join over admission ROWS, which exclusion never removes — so *the arm's reachability is a property of the denominator of the operation that returns it, not of what some lower mechanism observes internally*. Both halves were found the same day by separate lanes, from opposite directions.)
hollow alias (minimality ≠ grounding) · state-space conflation (an `Option`/`None` meaning >2 things — split into named variants; its most-repeated form here is **not-applicable rendered as malformed** — one reason symbol over "the input is wrong" and "this strategy had nothing to say about it", which have opposite owners and opposite repairs. Found three times in three stages by one lane (#8801 and #8828 in body lowering, `parse_g0_tokens_remain` in parse), always by reading the producer and never from the message. Recognition rule: if the arm sits downstream of a search, lookup or alternative that returned `Absent`, it is not-applicable and needs its own reason. → [the conflation class](docs/probes/not_applicable_versus_malformed_conflation_class_2026-08-22.md)) · absorbing fallback (a failure arm that widens — rerun everything, scan all keys, always run — instead of refusing; ⊤-as-answer conflated with ⊤-as-ignorance; the deficit's frequency zeroed by construction, the corpus-denominated cost breaking the budget later) · **empty-observation narrow** (the absorbing fallback's mirror: ⊥-as-answer conflated with ⊥-as-ignorance — an observation that could not express what changed rendered as the verdict "nothing is affected", so the run narrows to nothing instead of widening. Strictly worse than the widen §5 already forbids: a widen is merely expensive, a narrow is silently uncovered. Live specimen: a push whose baseline ref *is* the pushed ref diffs the commit against itself, and the witness floor reported the resulting zero-path observation as "N unaffected (import-closure, skipped without resolve)" — receipt, two main pushes reporting an identical `4118 unaffected` on different commits, a skip count that cannot be a function of the diff. The tell that one observation is wrong rather than three local choices reasonable: its consumers disagree — compile-clean widened to whole-tree, regen gated on the event name, the witness floor skipped) · cache impurity (key on declared-input content; byte-identical cached-vs-cold is the purity oracle) · reflection evidence ≠ structural proof (prove a read axis by execution, with a no-host-enumeration control) · coercion proven by normalized round-trip, not a golden string · parallel-representation debt (an honestly-marked scaffold duplicating a canonical fact is still a violation) · internal review finds missing tests, external review finds missing checks · unmarked workaround (an author-side absorbing fallback — routing around an obstacle with no dissolution trigger; the line-stop signal, never a landing state) · **self-authorized dissolution** (temporary work treated as admissible because the author named its future deletion — a trigger is a lifecycle fact, not permission; without an operator verdict, marked debt is rejected exactly like unmarked debt) · positional citation (a `file:line` pointer where a symbol was available — see §3). · **authority substitution** (fact F lives in carrier A; operation O is governed by carrier B; A is cited as the evidence that O changed; no A→B relation is claimed by either carrier. Nothing asserted is false — the *entailment* is invented, which is why review reads past it: both halves check out and only the arrow between them is missing. It is §3's single-authority rule read in the direction authors actually violate it — not two authorities for one fact, but one authority borrowed to answer for another's. Receipt (gunbc#8865): an expecting-red probe was enrolled in `gunbc.explicit_witness_admission`, which DOCUMENTS a known red, and the PR asserted the required floor therefore held it; the floor gates on `v2.workflow.floor_expected_red` and nothing relates the two, so CI went red on a row its author had recorded as expected. The general tell is a sentence of the form *I registered it in A, so B now does X* where B is never named — and its structural fix is never a broader guard joining every A row to B, since that manufactures exactly the entailment being invented; the guard must carry the narrow predicate, with its exceptions declared.) · **reachability read as occupancy** (a guard's arm, disposition or check is deleted because nothing currently lands in it. Three questions are in play and only the first two decide whether it should exist: *mechanism existence* — can any governing authority produce this state; *join reachability* — can that mechanism classify an element of THIS operation's denominator; *current occupancy* — does anything receive it today. **Yes / yes / zero is a healthy guard being quiet, not a dead one**, and deleting it removes a live wall while looking principled. The distinction is load-bearing because it borders a true rule pointing the other way: a check whose RED IS UNREACHABLE — no authorable input can produce it — is a decoration, permanently green and worse than absent, because it is cited as coverage. Unreachable means the red cannot be produced at all; empty means it can and nothing does. Two corollaries, each from a lane that got it wrong first. Reachability is judged against what a FIXTURE MAY AUTHOR, never what the accepted corpus contains — a regression probe is an invalid program by definition, so a state no `Accepted` program holds is usually still authorable as source, and scoping reachability to corpus-expressible is this same conflation one layer out. And an arm is reachable relative to ONE operation: `gunbc.scm`'s path-exclusion disposition is unreachable from the floor's own fold, which drops excluded subjects before inventory, yet reachable from a join over admission ROWS, which exclusion never removes — so *the arm's reachability is a property of the denominator of the operation that returns it, not of what some lower mechanism observes internally*. Both halves were found the same day by separate lanes, from opposite directions.) · **total at the level examined, blind one level down** (a judgment is exhaustive over the type it matches and says nothing about the distinction that actually decides the outcome, which lives inside one of its arms. **The pairing is the whole content: the match is exhaustive AND wrong**, and the exhaustiveness is what hides it — there is no missing arm to report, no warning, nothing incomplete, so neither a reviewer reading the match nor a wildcard-free lens can see it. Specimen with a mutation receipt (gunbc.scm, 2026-08-22): `repository_load_disposition` matching `RepositoryDecodeImageRefusal { cause: _ }` is total over `RepositoryDecodeRefusal`, but `ImageRefusal`'s thirteen arms carry three different publication remedies — a reader limitation, an absent-object problem over a well-formed document, and malformed bytes. Only the third may supersede a head slot, so the collapsed form lets an OLDER READER OVERWRITE A NEWER WRITER'S DOCUMENT: data loss produced by the reader's own limitation, from a match that compiles and looks complete. Executed both ways — descending, four witnesses pass; collapsed, the witness driving all three remedies through the single outer arm goes red; a temporary decode arm makes the fold non-exhaustive; restored control passes. Second, independent specimen the same day, in the compiler itself: a census of the fourteen declared-type positions the grammar admits found five accepting a plain kernel value where a coproduct is declared — the judgment is present and total at the level it examines, and never descends. **The tell is a `_` or a bare binding in the arm that carries the payload**, and the test is not whether the match is complete but whether every cause it collapses shares one remedy; the fix is to descend so a new inner arm fails to compile HERE, rather than silently inheriting whichever remedy the outer arm happened to name.)

## Building & checks

Expand Down
Loading
Loading