Repository navigation
C0(b2) declaration-to-capability totality + UTF-8 repair in the witness-admission row scan - #7986
Closed
gunbai-bot[bot] wants to merge 10 commits into
Closed
gunbai-bot[bot] wants to merge 10 commits into
gunbai-bot[bot] wants to merge 10 commits into
Conversation
classification_matches_fact joins a roster row to a DeclFact on BARE NAME, while DeclFact carries qualified_name and kind and could key exactly. That is sound only while every top-level declaration of v1.compiler.complexity has a distinct name, and nothing in the carrier makes that true -- it is a property of the subject module, not a wall this carrier erects. Measured over src/v1/complexity.dag: 201 top-level declarations (171 fn, 26 type, 4 data, 0 let), zero duplicate names. So the join is correct today. But a measurement of the current tree is not an oracle (DESIGN section 5), so the precondition is now EXECUTED rather than assumed. The gap this closes is real and none of the four existing totality witnesses covers it: a duplicate name in the DERIVED population still classifies, still matches a roster row, and leaves no stale row, so one roster row can silently answer for two declarations while every count agrees. roster_names_distinct does not cover it either -- it constrains the AUTHORED side only, and the duplicate here would be on the derived side. Added population_names_distinct beside the existing roster_names_distinct, reusing name_already_seen rather than minting a second distinctness fold. Green by execution, all three run through claim_batch against the real tree: PASS w_population_decl_names_are_distinct (live population) PASS w_distinctness_fold_reds_on_a_planted_duplicate (discriminating RED) PASS w_distinctness_fold_accepts_a_distinct_control (positive control) The RED matters: a distinctness fold that cannot fail proves nothing, so a planted same-name pair must come back false or the live green is empty. Dissolve-on is named on the carrier: the roster carrying exact DeclFact identity (qualified_name, or name plus kind) makes the join exact by construction and retires the precondition. That is a 201-row re-authoring and is deliberately not bundled here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…I fixed (review 49289)
Review 49289 caught three more instances of exactly the defect this PR exists
to remove, and it was right: I corrected one occurrence and did not sweep for
the class -- the same shortcut I would send back on someone else's diff.
Fixed, all verified against main rather than recalled:
section 7 C0(c) bullet still called the split "the next implementation
slice" while the C0 summary said DELIVERED
section 9 operator ruling same, so a reader of section 9 could still treat
C0(c) as open
section 2 table still listed a single lens_contract_complexity row
carrying RatchetForever. That row does not exist on
main. Replaced with the two rows that do --
derived_kernel (WallAfterGrounding) and optimality
(RatchetForever, the genuinely undecidable residue)
Two the review did not name, found by sweeping for the class instead of the
reported lines:
section 4 asserted in the present tense that lens_contract_complexity
carries RatchetForever. Marked RESOLVED by #7841 and kept as the
argument the split rests on, rather than deleted -- the reasoning
is why the split has the shape it has
section 8 a discriminating control named the deleted contract. Re-pointed
at both split rows, where the mode/consumer disagreement is
actually checkable
status blockquote said one carrier "currently" declares it permanent
Remaining bare mentions at lines 119, 143 and 147 are deliberate historical
references ("the mixed row", "as written then") describing the pre-split state
in explicitly past tense, not live claims about the tree.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…sfiable condition (review 49307) Third catch of the same class, and this one was more than a stale name -- the retirement criteria were unsatisfiable as written. Clause 1 required that "lens_contract_complexity's boundary class distinguishes the genuinely undecidable residue from the decidable capability". That is precisely what #7841 delivered, so the clause is SATISFIED and now says so, naming the two rows that replaced the mixed one. Clause 2 required that "lens_contract_complexity has a live consumer witness and has flipped off AuditOnly". Read onto the split, that can never be true. lens_contract_complexity_optimality is RatchetForever and stays permanently AuditOnly by the plan's own section 7 C0(c) ruling -- so a retirement condition demanding it flip would make this doc unretirable BY CONSTRUCTION. Re-scoped to lens_contract_complexity_derived_kernel, which is the half that can legitimately flip, and the clause now states explicitly why optimality is excluded so nobody re-adds it later. That second half is the part worth noticing: a dissolution trigger that cannot fire is a scaffold with no exit, which is the failure DESIGN section 6 asks a named trigger to prevent. The stale name would have been cosmetic; the unsatisfiable condition was not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…nstead Reviews caught this plan stale in four separate places, each claim true when written and false a day later. The common shape was a merge-event assertion -- "DELIVERED ON MERGE of #7841", "both rows are on main" -- which rots without anyone touching it, because nothing in the tree can decide it. Replace the class, not the four lines. Every delivery claim now names the carrier SYMBOL a reader can resolve (DESIGN section 3, cite-the-symbol), so it is decidable by grep rather than by remembering which PR merged when. Verified: all seven cited symbols resolve; zero PR numbers and zero merge-event phrases remain in the carrier. Also fixes a real dangling reference the C0(c) split created: the census note in gunbc.v1_complexity_capability_census cited lens_contract_complexity, a row that no longer exists. Re-pointed at lens_contract_complexity_derived_kernel, which is the one a consumer surface would actually move -- optimality is AuditOnly permanently.
The floor worker died exit 101 with no terminal receipt on
witness_admission_entry_function_keys_from_source: WINDOW is a 400-BYTE budget
applied to UTF-8 prose via after.len().min(WINDOW), so whenever byte 400 lands
inside a multi-byte char the slice panics and takes the whole run down. The row
that exposed it simply happened to put an em dash across that offset.
Every other slice in that function takes its offset from find/split_once, which
return char boundaries; this fixed offset was the only unguarded one. It now
walks down to the nearest boundary, so an over-long row is truncated rather than
fatal. Note the comment directly above already recorded an earlier panic in this
same function, so the failure mode has form.
Fixing the string instead of the scanner was the tempting move and it is the
unmarked workaround DESIGN section 5 forbids: it would leave the defect armed for
the next author who writes prose with an em dash in it. So the em dash stays in
the row, and the scanner is what changed.
PROVEN DISCRIMINATING BY EXECUTION, both directions:
- unfixed: panics "byte index 400 is not a char boundary; it is inside em dash
(bytes 398..401)" -- the production failure reproduced exactly
- fixed: passes
The fixture puts entry: and function: FIRST, mirroring real rows, because the
scanner deliberately panics when entry: falls outside the window and that refusal
is correct behaviour rather than the bug under test -- an earlier draft of this
fixture tripped that arm and would have tested the wrong thing. The prose is a
run of em dashes shifted by 0/1/2 ASCII bytes, covering every residue class mod
3, so at least one iteration is GUARANTEED to put the window edge strictly inside
a character. The test deliberately does not model where the scanner sets
search_from; pinning that offset would make the fixture fail for the wrong reason
the moment the scanner moves.
gunbai-bot
Bot
changed the title
Contributor
Author
|
Closing as superseded — this content is already in
Including the UTF-8 row-scan fix this PR was titled for. The per-path check was run with a positive control — the same command shape reports non-empty for a file that genuinely differs — so the empty result is a real negative, not a blind read. Consequence worth recording: this PR carried two approvals guarding content that had already landed. An approval tally says a reviewer read the diff; it does not say the diff still contributes anything. Ancestry and content grain answer different questions, and here they disagree — ancestry says "unmerged", content says "already present". Lane consolidation for the tree wind-down is #8027; this PR is not folded into it because there is nothing to fold. Branch kept. — sent from proud-bear-834 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Two independent things that happened to be in flight on the same branch. Both are complete; neither depends on the other.
1. A UTF-8 correctness repair in the witness-admission row scan (
src/v1/stage0/src/cli_run.rs).WINDOWis a byte budget, but the buffer it clamps is UTF-8 prose.&after[..after.len().min(WINDOW)]slices mid-character whenever byteWINDOWlands inside a multi-byte char — and the admission rows this reads are prose that routinely contains one (em dash, arrow). That panicked the whole floor worker — exit 101, no terminal receipt — on a row whosereasonstring simply happened to put an em dash across byte 400.Every other slice in that function takes its offset from
find/split_once, which return char boundaries. This fixed offset was the only unguarded one. The fix walks down to the nearest boundary, so an over-long row is truncated rather than fatal.The regression test computes the pad rather than eyeballing it, so the straddle is a property of the fixture instead of anyone's byte counting: the em dash starts one byte before the edge, so bytes 399..402 span it and 400 is not a boundary.
entry:/function:are placed first, mirroring real rows — the scanner deliberately panics when it cannot findentry:in the window, and that refusal is correct behaviour, not the bug under test, so keeping them early isolates the test to the slice.2. C0(b2) — the declaration-to-capability totality slice (
gunbc.v1_complexity_decl_classificationand its witnesses).Derives the top-level declaration population of
v1.compiler.complexityfromDeclFactand classifies each declaration as authority-of / helper-of / legacy-hazard-of a capability, or deliberately out of scope.Test plan
Fast lane, per-PR (
v1_complexity_decl_classification_witness_test) — the discriminating mechanism:w_distinctness_fold_reds_on_a_planted_duplicate— a planted duplicate over a synthetic two-element fixture, RED by constructionw_distinctness_fold_accepts_a_distinct_control— the positive control beside itA broken fold therefore reds on every PR. Only the live-population reading waits for the cadence.
Scheduled long lane (
long/v1_complexity_decl_classification_totality_test) — sixtest fns over the real derived population: counts match, every population declaration is classified, every classification row matches the population, no stale rows, population non-empty, andw_population_decl_names_are_distinct.That last one is explicitly enrolled in
gunbc.ci_layer_rootsas aSubstrateLongLaneRowwith a stated reason and adissolve_ontrigger (the roster carrying exactDeclFactidentity, so the join is exact by construction and the precondition becomes unnecessary). It is not admitted by living underlong/.Notes
classification_matches_factkeys onDeclFact.name. That join assumes bare names are unique in the population — so this PR executes that precondition (w_population_decl_names_are_distinct) instead of leaving it implicit.The 201-declaration figure is not used as an oracle anywhere. A measurement taken from the current tree is not an independent referent; the distinctness property is checked at identity grain by an executing witness, and the fast-lane mechanism tests use controlled fixtures that author their own input and expected population.
Not proven: discovery of a capability omitted from C0(b1). Classification is authored against the closed
ComplexityCapabilityIdvocabulary and inherits that limitation.Also carries plan-carrier corrections from review: a dissolution trigger that named a deleted row and set an unsatisfiable condition (
review 49307), and a sweep of the same stale-status class across the whole plan rather than the single line first reported (review 49289).