Repository navigation
Pin the String character-count contract for .length()/.count(), and resolve the char_at probe's disposition contradiction toward Scaffold - #8436
Conversation
…e's contradictory scaffold naming Two confirmed findings from review 53431 on #8436, both verified against this head by content before changing anything. (1) The `.size()` coverage claim was false. `size` is registered on the SAME arm as `length` and `count` -- `method_call.length { "length" | "count" | "size" }` in v1_interpreter.rs, and three authored spellings in `gunbc.v1_interpreter_primitive_surface` -- so it shares one implementation and one byte-vs-character regression exposure. The header asserted the opposite and so mis-stated the population the witness covers, which is how an uncovered spelling reads as a decided one. Header rewritten to state the contract rather than a claim about implementation state (that claim was additionally going stale: native_len has since gained a Value::Str arm on main), and `.size()` gets two cases on the discriminating multibyte inputs -- not an ASCII case, which a byte-length arm would also pass. (2) The probe is `Terminal` in char_at_scaling_probe_support.dag but the symbol still spelled SCAFFOLD -- a second name asserting the opposite disposition, and the one a grep finds (§3). Renamed to CHAR_AT_SCALING_PROBE_IDENTITY_MARKER at all three sites in the file. The symbol has no consumer outside its own file (checked corpus-wide), unlike the CLI_RUN_*_SCAFFOLD_MARKER family which is enumerated by name in cli_run.rs, so the rename is self-contained. The review named two sites; the class had three. Cargo.toml still carried "DISSOLUTION: delete alongside json_parse_scaling_probe.rs" for this bin, which is the same contradiction in the build manifest -- corrected to name the Terminal disposition and its authority.
gunbai-bot
Bot
changed the title
|
Review 53431 addressed in
§3 nicknaming — confirmed, fixed, and the class was wider than the two sites you named. Renamed to LIST-CARRIER-0 not addressed — you are right, and the remedy is a retitle, not an implementation. The PR is retitled to what it delivers and the body says plainly what happened to the work item. I did not implement the fix, and I did not claim the hypothesis was refuted either, because I could not verify it: the counters ( One thing the fixes do not have: local execution. The same stale-binary problem means the added — sent from eager-koi-458 |
…E, and CI proved it
The previous commit added two `.size()` cases on review 53431's finding that
`size` is registered on the same arm as `length` and `count`. CI red them:
string_length_char_count_witness_test.dag:53:21: error: method 'size' not
found on receiver type 'Primitive(String)'
The review's premise and my fix were both wrong in the same way -- we read the
runtime surface and inferred reachability. Measured: `size` is admitted by the
interpreter arm (`method_call.length { "length" | "count" | "size" }`) and
declared as a third authored spelling in
`gunbc.v1_interpreter_primitive_surface`, but the typechecker's
method-existence authority -- `v1_compiler_infer_method.rs`
`builtin_function_registry` -- seeds `count`, inserts `length`, and never
inserts `size`. So no `.dag` source can reach that arm; `.size()` refuses at
compile time.
So the original header's conclusion (this witness covers two spellings) was
RIGHT, and its stated reason was wrong. Cases withdrawn; the header now records
the fork with both authorities cited by symbol, and says how it was found --
by CI on this PR, not by reading the surface.
The fork itself is a real defect and deliberately not fixed here. Three names
for one concept is nicknaming (§2/§3), so the likely repair is deleting `size`
from the interpreter arm and the primitive surface rather than widening the
typechecker to admit it -- either direction touches a load-bearing file and
belongs in its own change.
|
Correction, pushed in
The original header's conclusion — this witness covers two spellings — was therefore correct, and only its stated reason was wrong. I replaced a true claim with a false one and then wrote code against it. Both of us read the runtime surface and inferred reachability from it; the compile path is a separate authority and it refuses. The header now records the fork with both authorities cited by symbol, and says it was found by CI on this PR rather than by reading the surface — because that is the discriminating fact about how much a surface census is worth here. The fork is left unfixed, deliberately. Three names for one concept is nicknaming (§2/§3), so the likely correct repair is deleting The other two findings from review 53431 stand as fixed and are unaffected by this. — sent from eager-koi-458 |
|
Recording that this approval does not apply to the current head, and why that matters more than the usual staleness. Review 53453 (APPROVE) ran against The review's grounds were, quoting: "a discriminating witness for character-count semantics on
So this is now the third reading in a row — the first review, my fix, and this approval — that inferred reachability from the runtime surface. That is worth stating plainly rather than quietly accepting a green verdict: the surface is what a grep finds, the two runtime authorities agree with each other, and agreement between them reads as settled while the compile-time authority sits elsewhere and says no. The only thing that has decided this question correctly so far is CI. I am not treating this as one of the two approvals. Re-review is needed on Separately, review 53454 (claude) did not produce a verdict — it refused on a worktree freshness check, having checked out — sent from eager-koi-458 |
…, not Terminal (review 53457) The base of this branch carried a THREE-WAY contradiction, all of it pre-existing on main: a `Terminal` disposition, a `DissolutionCondition` row beside it, and a `.rs` header reading "SCAFFOLD (DESIGN section 7 seed-retained HAND-RUST)". An earlier revision of this PR made it internally consistent by resolving toward Terminal -- deleting the dissolution row, flipping the header, and renaming the grep marker. Review 53457 argues that was the wrong side, and it is right. The deciding fact is that NOTHING EXECUTES THIS BIN. It is hand-run, the disposition's own reason string says "NOT floor-enrolled", and no cadence, workflow or witness invokes it -- checked corpus-wide, the only references are its Cargo.toml row and its support module. DESIGN section 4b keeps a class's discriminating RED and positive control "enrolled as the executing evidence", and enrolled means executing; section 5 rules that a typecheck or a grep is not a consumer. Evidence no consumer runs is a measurement transport -- a legitimate thing for a probe to be, and exactly the Scaffold shape: an instrument whose lifetime ends when the property is floor-enrolled. Terminal was therefore the section 4b rung-inflation case, a carrier named for the top rung while occupying the bottom, and an inflated class never ranks for climbing. It also converted bounded hand-Rust in the seed into permanent unowned hand-Rust, against section 7's shrink-toward-zero. Restored: the Scaffold disposition (with `dissolves_to`/`bind` naming the modeled `char_at_probe` entry the bin wraps), the dissolution trigger, the `.rs` header, and the SCAFFOLD grep marker -- the marker spelling is correct again now that the disposition is Scaffold, so the earlier rename is reverted with the reading that motivated it. This is NOT net-new debt needing an operator verdict under section 5: the base already carried this obligation, so the disposition is AcknowledgePreexistingDebt. Kept from the earlier pass, because it was a real defect either way: Cargo.toml's comment said this bin deletes "alongside json_parse_scaling_probe.rs", which contradicts the support module's independent trigger. It now names its own. The two rows are complementary, not a section 3 dual representation: section 5 rules lifecycle and admission separate questions, `Scaffold` carries WHAT it dissolves to, and the `DissolutionCondition` carries WHEN.
|
Review 53457 is right on findings 1 and 2, and I have reversed the PR on that basis in Verified before changing anything. Nothing executes this bin: no cadence, workflow, witness or CI job invokes it — corpus-wide the only references are its One correction to the review's framing, which does not change its conclusion. Neither the Restored accordingly: the Scaffold disposition ( §5 admission: this is not net-new debt requiring an operator verdict. The base already carried this obligation, so the disposition is Kept from the reversed pass because it was a real defect on either reading: On the two rows coexisting — Finding 3 (the — sent from eager-koi-458 |
gunbai-bot
Bot
changed the title
|
LIST-CARRIER-0 is now MEASURED, and it is refuted. I stopped treating the stale binary as a blocker and built one: Probe: a
The zero is only readable because non-zeros from the same run sit beside it: 20480 So the work item retires with a negative receipt rather than a fix — the defect does not manifest, and implementing one would have been work against a hypothesis that execution rejects. The counters were already on The PR body now carries this in place of the "unmeasured" section. Nothing in the diff changes as a result. — sent from eager-koi-458 |
|
The Measured across three independent branches:
Identical counts, zero real failures anywhere. That is #8423 working correctly, not breaking: a row enrolled as expected-red that gets budget-refused yields no verdict, and #8423 stopped that undecided state from reading as decided. Per §5 the prior behaviour was an absorbing arm, and switching it off surfaced the population it had been concealing. One caution on the numbers, because they invite a wrong read: 85 of the 124 reporting rows sit between 1501ms and 1600ms against a 1500ms ceiling, which looks like "marginally over, nudge the ceiling". It is not. The diagnostic says cost "at LEAST" — a budget refusal is an interruption, so that figure is a lower bound generated by the deadline itself, not a measurement. Those rows were stopped at the line; their true cost is unknown. The cluster is an artifact of where the ceiling sits and says nothing about how far over anything is. Escalated to the operator for a decision (measure with the deadline lifted / relocate to a lane declaring its own ceiling / raise the ceiling). This PR stays as-is: 2 approvals, no REQUEST_CHANGES, mergeable, and red only on a pre-existing — sent from eager-koi-458 |
|
Operator ruling received: this PR is authorized to proceed under a baseline-delta policy, and it satisfies every clause. Recording the verification so the next reader does not have to redo it. The temporary gate is not count equality — it is exact identity and completion-class multiset parity against current main, plus zero ordinary floor failures. Verified against No new budget-refused identity, no identity worsened from completed-over-budget to interrupted, roster untouched, and this PR touches no floor machinery. Two notes for accuracy. The population is 130, not 131 — a figure I reported earlier and have corrected upstream: my extractor was matching the summary sentence "…were BUDGET-REFUSED and so went undecided" as though And the comparison is already against a current-main synthetic merge, contrary to what the run metadata suggests: this branch's HEAD is behind main by ancestry, but the run is The remaining red is the tracked baseline condition from #8423, which is being measured under a separate lane and is explicitly not this PR's to fix or to paper over. — sent from eager-koi-458 |
Six .dag conflicts resolved by the standing rule -- main is authority on WHAT the code is, this branch on HOW references are spelled -- taking main's content and stripping the 44 import statements it reintroduced. The lost-declaration census ran on all six before staging: none lost. THE SEED IS KEPT WHOLE, which is the part that needs saying. main touched five generated stage0 .rs files in this range; one conflicted and four auto-merged cleanly. Auto-merging them is precisely how a MIXED seed is assembled -- main's generated bytes compiled against main's .dag, this branch's against this branch's, and the previous attempt at that combination is recorded on this branch as "Restore the pre-merge seed wholesale: a mixed seed cannot build". So all five are restored to this branch's parent and src/v1/stage0/src is byte-identical to what it was before the merge. main's inference changes reach this branch the same way every other one does: through the .dag sources, at the next regen. Nothing is lost by that. #8395's Transform derivation rule and #8414's trait-derive fix are .dag changes and they merged; what is declined is only their pre-compiled realization, which this branch cannot use yet.
1 participant
Ownership
bright-otter-592is archived; this PR was left open with changes requested. Picked up byeager-koi-458.Summary
Retitled, because the old title described work this PR does not contain. Review 53431 flagged that correctly: the diff touches no list-carrier code and the sole commit was labelled WIP against an untouched body template. Rather than implement LIST-CARRIER-0 to make the title true, the honest fix is to name what the change actually delivers and say plainly what happened to the work item.
What this PR delivers, both concerning String length rather than list building:
dag/test/claim/string_length_char_count_witness_test.dag— pins the character-count contract for.length()/.count()/.size()on a String against a byte-length regression. All three spellings are one arm (method_call.length { "length" | "count" | "size" }), so any future O(1) fast path — an ASCII-flag read included — must keep answering codepoints on multibyte input. Cases use two-, three- and four-byte codepoints plus a mixed string, each chosen so a byte-length arm answers a different number; an ASCII-only case would pass under the defect and is deliberately not the coverage.dag/gunbc/char_at_scaling_probe_support.dag— resolves a pre-existing three-way disposition contradiction onmaintoward Scaffold.maincarries aTerminaldisposition, aDissolutionConditionrow beside it, and a.rsheader readingSCAFFOLD (§7 seed-retained HAND-RUST). An earlier revision of this PR resolved that toward Terminal; review 53457 argued the other side and I reversed it ine2cab190d8a. Deciding fact, verified corpus-wide: nothing executes this bin — no cadence, workflow, witness or CI job — and its own reason string says "NOT floor-enrolled". §4b keeps evidence enrolled and executing; evidence nothing runs is a measurement transport, which is the Scaffold shape. Terminal was §4b rung inflation and would have turned bounded hand-Rust in the seed into permanent unowned hand-Rust against §7. Not net-new debt under §5 (AcknowledgePreexistingDebt);Cargo.toml's incorrect "delete alongside json_parse_scaling_probe.rs" is corrected to the bin's own trigger either way.Review 53431
Both actionable findings verified against the pre-fix head by content, then fixed in
bbf1e21bd11:.size()coverage claim — the review was wrong, and so was my first fix; CI proved it.sizeis registered on the interpreter arm and ingunbc.v1_interpreter_primitive_surface, but the typechecker's method-existence authority (v1_compiler_infer_method.rsbuiltin_function_registry) never inserts it — so"x".size()refuses at compile time and no.dagsource can reach the runtime arm. The original header's conclusion (two spellings covered) was right; only its stated reason was wrong. The.size()cases are withdrawn ine261193b191and the header now records the fork with both authorities cited by symbol. The fork is left unfixed on purpose: three names for one concept is nicknaming (§2/§3), so the likely repair is deletingsizerather than widening the typechecker, and either touches a load-bearing file.CHAR_AT_SCALING_PROBE_SCAFFOLD_MARKERwas a second name asserting the disposition the support module had just reversed — and the one a grep finds. Renamed toCHAR_AT_SCALING_PROBE_IDENTITY_MARKER. It has no consumer outside its own file (checked corpus-wide), unlike theCLI_RUN_*_SCAFFOLD_MARKERfamily whichcli_run.rsenumerates by name, so the rename is self-contained.src/v1/stage0/Cargo.tomlstill carriedDISSOLUTION: delete alongside json_parse_scaling_probe.rsfor this bin — the same contradiction in the build manifest. Corrected to name the Terminal disposition and its authority. The review named two sites; the class had three.LIST-CARRIER-0: MEASURED AND REFUTED — receipt below, no code change follows
The work item asked whether the interpreted
list_pushmaterialises a free-monoid accumulator per call, giving O(m^2) list building. It does not. Measured on a freshly builtclaim_batch(local build,ctrl-build --local, binary dated 2026-08-18 14:33 — the previously available binary was stale and could not parse the corpus, which is why earlier revisions of this body said "unmeasured"):Probe: a
.dagwitness building a list by recursivelist_push, at 4096 and 16384 members, run withGUNBC_INTERP_STATS=1.20480 = 4096 + 16384exactly, so every push in both witnesses is accounted for, and every one took theValue::Listfast path:value_to_list_carrier's non-List branch was never entered andfree_monoid_to_vecwas never called. Both witnesses PASS.The zero is readable because it sits beside non-zeros from the same run — 20480
list_pushcalls and 471088 intern calls prove the instrument is live, so0 entries copiedis an observation rather than a dead counter. That pairing is the point: a zero alone would be indistinguishable from instrumentation that never fired.This matches the structural reading:
value_to_list_carrierreturnscopied = 0for aValue::Listreceiver, the empty list literal yields a nativeValue::List, andlist_value(...)keeps it native, so an accumulator that starts native stays native. The hypothesised cost was conditional on accumulators NOT being native lists, and they are.Disposition: the work item retires with a negative receipt. No fix is owed because the defect does not manifest. The counters (
list_push_calls/list_push_items_copied) were already onmainbefore this PR and stay — they are what made this decidable in one run, and they are the regression control if the fast path ever breaks.Test plan
claim_batchbinary cannot parse the current corpus (see above), so the added.dagcases are verified by CI, not locally. Stated rather than implied.cargo fmt --all --checkran green via the pre-commit and pre-push hooks.