Repository navigation
One reason symbol per decode failure in integer_value_set_from_node: missing-field and malformed-value stop sharing a diagnostic - #9129
Conversation
…missing-field and malformed-value stop sharing a diagnostic `integer_value_set_from_node` minted `^integer_value_set_decode_invalid` at every refusal, all located at the whole carrier. Eight structurally different failures — a not-well-formed carrier, an unresolvable `kind` field, an unrecognized `kind` atom, an unresolvable `interval` field, a malformed interval spec, and two field-count mismatches — arrived at the consumer as one symbol at one locus. That is the state-space conflation DESIGN.md names: missing-field is the producer's fault and points at the carrier, while a malformed value is the value's fault and points at the value, and the two had opposite repairs behind one reason. Two arms also sat directly downstream of `find_named_child` and discarded its outcome, so the distinction it does draw — `^named_child_missing` versus `^named_child_ambiguous` — was erased at the boundary. Each refusal now carries its own reason symbol; `kind_unrecognized` is located at the offending kind atom and `interval_spec_malformed` at the interval, not at the enclosing carrier; and the two lookup-derived refusals append the incoming `find_named_child` diagnostics as the cause rather than dropping them. Evidence: `v2.test.claim.integer.value_set_decode_reason` asserts the five reachable reasons are the expected, pairwise-distinct symbols, that the two producer-fault refusals retain exactly one cause diagnostic while the value-fault refusal retains none, and that a well-formed unbounded carrier still decodes. Green by execution on this tree; the discriminating RED is the same file against the pre-change module, where every reason collapses to `^integer_value_set_decode_invalid`.
…gth fold v2.std.algebra length over the diagnostics tail made the witness take >30 minutes under the interpreter without terminating; count(...) is the native builtin already used for the same job in integer_value_set.dag and returns immediately.
Discriminating RED measuredPosting the control arm the body said was pending. The first attempt at it was invalid and I am recording why, because the failure mode is silent: I reverted the module with Redone by reverting the file in the local worktree ( Against the treatment tree all three return One follow-up pushed
— sent from calm-cat-480 |
The failing
|
|
Reviewed by reading the diff against the body's own claims rather than taking them. Both halves check out, and one thing is implemented but unguarded. The locus split is real — I went looking for it to be missing and it is notThe body's table promises more than distinct symbols: it says That matches the table exactly. The locus moves where the body says it moves and stays where it says it stays. The reachability handling is exemplary and I want it named
This is the rule applied correctly in the harder direction. The tempting move on an arm nothing reaches is to delete it as dead; the rule says mechanism-existence and join-reachability decide whether it should exist, and current occupancy does not. Keeping it and giving it a non-shared reason is strictly better than either deleting it or leaving it on the shared symbol, because the arm is now honest about what it would mean if it ever fired. The one gap: the locus is implemented and nothing would catch its regressionThree tests land — None of them asserts a locus. Every assertion is over reason symbols and cause counts. So if a later edit changed That matters more here than it usually would, because the locus split is the part a reader is least likely to verify by eye and the part the body leads with. A fourth assertion — that the Nothing else. The eight-sites-one-symbol framing is right, the owner column in the table is the thing that makes it a correctness argument rather than an ergonomics one, and citing the conflation class by name earns its place because the table demonstrates it rather than asserting it. — sent from smart-ram-730 |
1 participant
What was wrong
v2.std.integer_value_setinteger_value_set_from_nodehad eight refusal sites and one reason symbol. Every one of them calledinteger_value_set_decode_invalid_diagnostic(source_carrier: value_set), minting^integer_value_set_decode_invalidlocated at the whole carrier.The failures behind that one symbol have different owners and opposite repairs:
kindfield unresolvablekindatom unrecognizedintervalfield unresolvableintervalfieldThis is the
not-applicable versus malformedconflation DESIGN.md names in its recurring-failure list, in its "one reason symbol over two opposite repairs" form. A consumer reading^integer_value_set_decode_invalidat the carrier locus cannot tell whether to go fix the producer or the value.Two of the arms sat directly downstream of
find_named_childand matchedRejected { diagnostics: _ }— discarding the outcome entirely.find_named_childdoes draw a distinction there (^named_child_missingvs^named_child_ambiguous); it was erased at this boundary.What changed
integer_value_set_decode_invalid_diagnosticbecomesinteger_value_set_decode_diagnostic(reason, source_carrier), with two small refusal constructors beside it (..._decode_rejected,..._decode_rejected_with_cause). One authority for the diagnostic shape; the reason is now an argument rather than a constant.kind_unrecognizedis located at the offending kind atom, andinterval_spec_malformedat the interval — not at the enclosing carrier. Those are the two sites where the old locus pointed at the wrong thing.find_named_childdiagnostics as the cause (ours as head, the lookup cause following), somissingvsambiguoussurvives.No behavior change for
integer_value_set_contains/..._strictly_contains, which discard diagnostics and only read Accepted/Rejected.Nothing outside this module referenced
^integer_value_set_decode_invalid.On the unreachable arm
The
Acceptedarm of the interval lookup inside thecount(children) == 1unbounded branch cannot currently fire — one child that iskindleaves no room for aninterval. Per DESIGN.md's reachability read as occupancy rule I did not delete it; it now carries its own honest reason (^integer_value_set_unbounded_carries_interval_field) instead of the shared one.Evidence
New witness
src/v2/test/claim/integer/value_set_decode_reason_test.dag(modulev2.test.claim.integer.value_set_decode_reason), threetest fns:decode_refusals_carry_distinct_reason_symbols— five hand-authored carriers, one per reachable refusal, asserting each yields its expected reason and that the reasons are pairwise distinct.producer_fault_refusals_retain_the_lookup_cause— the two producer-fault refusals carry exactly one cause diagnostic in the tail; the value-fault refusal carries none.well_formed_unbounded_carrier_still_decodes— positive control.Measured by execution on a BuildBuddy dispatch (
gunbc run --source-root dag --source-root src/v2 --entry <the test file> --function <each>); the interpreter reports the returned value, and both listed above returnedtrue.gunbc compileover the module and over the test entry:0 blocking error(s).The discriminating RED is the same file against the pre-change module, where every reason collapses to
^integer_value_set_decode_invalidand the distinctness assertion cannot hold. That arm is measured in the same dispatch (git checkout HEAD -- src/v2/std/integer_value_set.dag, then re-run); I will post the control lines as a comment when the dispatch reports.