From 35dfe4ba06267004d10e0af31718fc2c16ef08f4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 24 Aug 2026 18:34:34 +0000 Subject: [PATCH 1/2] The inert-carrier lens reports both populations by name, not one Bool inert_carrier_clean_holds computed the offending carrier NAMES twice -- once as the unrostered fold, once as the stale-roster fold -- reduced each to a count, compared both to zero, and returned a bare Bool. Everything a reader needs to act was discarded at the last step: which carrier, and which of the two things to do about it. The two populations have OPPOSITE remedies, which is why a single located list would have been the wrong repair: UnrosteredInertCarrier -- the carrier is inert in the live tree and the roster does not admit it. The repair is to give it a live consumer, or (if it is deliberately staged ahead of one) to AUTHOR a roster row with a reason and a dissolution condition. StaleInertCarrierRow -- the roster admits a carrier that is no longer inert; a consumer exists. The repair is to DELETE the row. Applying either remedy to the other population is wrong in both directions: rostering a live carrier re-opens the admission the row exists to close, and deleting a row for an unrostered carrier removes nothing. So the finding is a coproduct with one variant per remedy, each carrying the carrier name, and the verdict is InertCarrierRosterClean / InertCarrierRosterDiverged { findings } -- the same verdict-lattice shape v2.lens.dependency_fidelity already uses. No fact is computed twice: names_not_in_roster / stale_roster_names are the single authority, count_not_in_roster and count_stale_roster are now length() over them, inert_carrier_live_{unrostered,stale_roster}_count read the verdict's populations, and inert_carrier_clean_holds is inert_carrier_verdict_is_clean over the live verdict. The existing callers and the roster registry row are untouched. Green by execution (remote dispatch, release gunbc, --source-root dag --source-root src/v2): all eight arms of inert_carrier_test return true, including the four new ones -- clean, unrostered-only, stale-only, and both-at-once, each asserting the name lands in its own population and NOT in the other. Discriminating RED: mutating inert_carrier_finding_is_stale_row so an unrostered finding also counts as stale -- i.e. collapsing the two populations back into one list -- turns the_two_populations_are_reported_separately and unrostered_population_names_the_carrier_needing_a_row false. The old bare Bool could not have caught that mutation at all. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01NMvpakyTk5X3YBh1wRqyqU --- src/v2/lens/inert_carrier.dag | 145 ++++++++++++++++++++++++++--- src/v2/lens/inert_carrier_test.dag | 38 ++++++++ 2 files changed, 170 insertions(+), 13 deletions(-) diff --git a/src/v2/lens/inert_carrier.dag b/src/v2/lens/inert_carrier.dag index 3b3213a8b81..f86df0c9d54 100644 --- a/src/v2/lens/inert_carrier.dag +++ b/src/v2/lens/inert_carrier.dag @@ -37,6 +37,7 @@ fn inert_carrier_rostered_names() -> List { data empty_inert_carrier_names: List = [] + fn list_contains_str(xs: List, target: String) -> Bool { fold_list( xs: xs, @@ -45,30 +46,148 @@ fn list_contains_str(xs: List, target: String) -> Bool { ) } -fn count_not_in_roster(names: List, roster: List) -> Int { +type InertCarrierFinding + = UnrosteredInertCarrier { carrier: String } + | StaleInertCarrierRow { carrier: String } + +type InertCarrierRosterVerdict + = InertCarrierRosterClean + | InertCarrierRosterDiverged { findings: List } + +data empty_inert_carrier_findings: List = [] + +data inert_carrier_finding_remedy_note: String = "The two populations have OPPOSITE remedies, which is why they are two variants and not one located list. UnrosteredInertCarrier: the carrier is inert in the live tree and the roster does not admit it -- the repair is to give it a live consumer, or (if it is deliberately staged ahead of one) to author a roster row with a reason and a dissolution condition. StaleInertCarrierRow: the roster admits a carrier that is NO LONGER inert -- a consumer exists, so the repair is to DELETE the row. Applying either remedy to the other population is wrong in both directions: rostering a live carrier re-opens the admission the row exists to close, and deleting a row for an unrostered carrier removes nothing." + +fn names_not_in_roster(names: List, roster: List) -> List { fold_list( xs: names, - empty: 0, - cons: fn(count, name) { - if list_contains_str(xs: roster, target: name) { count } else { count + 1 } + empty: empty_inert_carrier_names, + cons: fn(acc, name) { + if list_contains_str(xs: roster, target: name) { + acc + } else { + list_snoc_item(xs: acc, item: name) + } } ) } -fn count_stale_roster(roster: List, inert_names: List) -> Int { +fn stale_roster_names(roster: List, inert_names: List) -> List { fold_list( xs: roster, - empty: 0, - cons: fn(count, entry) { - if list_contains_str(xs: inert_names, target: entry) { count } else { count + 1 } + empty: empty_inert_carrier_names, + cons: fn(acc, entry) { + if list_contains_str(xs: inert_names, target: entry) { + acc + } else { + list_snoc_item(xs: acc, item: entry) + } + } + ) +} + +fn count_not_in_roster(names: List, roster: List) -> Int { + length(xs: names_not_in_roster(names: names, roster: roster)) +} + +fn count_stale_roster(roster: List, inert_names: List) -> Int { + length(xs: stale_roster_names(roster: roster, inert_names: inert_names)) +} + +fn inert_carrier_findings(names: List, roster: List) -> List { + let unrostered = fold_list( + xs: names_not_in_roster(names: names, roster: roster), + empty: empty_inert_carrier_findings, + cons: fn(acc, name) { list_snoc_item(xs: acc, item: UnrosteredInertCarrier { carrier: name }) } + ) + fold_list( + xs: stale_roster_names(roster: roster, inert_names: names), + empty: unrostered, + cons: fn(acc, entry) { list_snoc_item(xs: acc, item: StaleInertCarrierRow { carrier: entry }) } + ) +} + +fn inert_carrier_verdict_from_findings(findings: List) -> InertCarrierRosterVerdict { + if is_empty(xs: findings) { + InertCarrierRosterClean + } else { + InertCarrierRosterDiverged { findings: findings } + } +} + +fn inert_carrier_roster_verdict(names: List, roster: List) -> InertCarrierRosterVerdict { + inert_carrier_verdict_from_findings(findings: inert_carrier_findings(names: names, roster: roster)) +} + +fn inert_carrier_live_roster_verdict() -> InertCarrierRosterVerdict { + inert_carrier_roster_verdict(names: inert_carrier_names_live(), roster: inert_carrier_rostered_names()) +} + +fn inert_carrier_verdict_is_clean(v: InertCarrierRosterVerdict) -> Bool { + match v { + InertCarrierRosterClean => true + InertCarrierRosterDiverged { findings: _ } => false + } +} + +fn inert_carrier_finding_carrier(f: InertCarrierFinding) -> String { + match f { + UnrosteredInertCarrier { carrier } => carrier + StaleInertCarrierRow { carrier } => carrier + } +} + +fn inert_carrier_finding_is_unrostered(f: InertCarrierFinding) -> Bool { + match f { + UnrosteredInertCarrier { carrier: _ } => true + StaleInertCarrierRow { carrier: _ } => false + } +} + +fn inert_carrier_finding_is_stale_row(f: InertCarrierFinding) -> Bool { + match f { + UnrosteredInertCarrier { carrier: _ } => false + StaleInertCarrierRow { carrier: _ } => true + } +} + +fn inert_carrier_verdict_findings(v: InertCarrierRosterVerdict) -> List { + match v { + InertCarrierRosterClean => empty_inert_carrier_findings + InertCarrierRosterDiverged { findings } => findings + } +} + +fn inert_carrier_unrostered_names(v: InertCarrierRosterVerdict) -> List { + fold_list( + xs: inert_carrier_verdict_findings(v: v), + empty: empty_inert_carrier_names, + cons: fn(acc, f) { + if inert_carrier_finding_is_unrostered(f: f) { + list_snoc_item(xs: acc, item: inert_carrier_finding_carrier(f: f)) + } else { + acc + } + } + ) +} + +fn inert_carrier_stale_row_names(v: InertCarrierRosterVerdict) -> List { + fold_list( + xs: inert_carrier_verdict_findings(v: v), + empty: empty_inert_carrier_names, + cons: fn(acc, f) { + if inert_carrier_finding_is_stale_row(f: f) { + list_snoc_item(xs: acc, item: inert_carrier_finding_carrier(f: f)) + } else { + acc + } } ) } fn inert_carrier_clean_holds() -> Bool { - let names = inert_carrier_names_live() - count_not_in_roster(names: names, roster: inert_carrier_rostered_names()) == 0 - && count_stale_roster(roster: inert_carrier_rostered_names(), inert_names: names) == 0 + inert_carrier_verdict_is_clean(v: inert_carrier_live_roster_verdict()) } fn inert_carrier_live_count() -> Int { @@ -76,11 +195,11 @@ fn inert_carrier_live_count() -> Int { } fn inert_carrier_live_unrostered_count() -> Int { - count_not_in_roster(names: inert_carrier_names_live(), roster: inert_carrier_rostered_names()) + length(xs: inert_carrier_unrostered_names(v: inert_carrier_live_roster_verdict())) } fn inert_carrier_live_stale_roster_count() -> Int { - count_stale_roster(roster: inert_carrier_rostered_names(), inert_names: inert_carrier_names_live()) + length(xs: inert_carrier_stale_row_names(v: inert_carrier_live_roster_verdict())) } fn inert_carrier_live_declared_count() -> Int { diff --git a/src/v2/lens/inert_carrier_test.dag b/src/v2/lens/inert_carrier_test.dag index 806e851bf1b..192a904cd53 100644 --- a/src/v2/lens/inert_carrier_test.dag +++ b/src/v2/lens/inert_carrier_test.dag @@ -6,6 +6,11 @@ import v2.std.text { String } import v2.lens.inert_carrier { inert_carrier_clean_holds, inert_carrier_live_declared_count, + inert_carrier_roster_verdict, + inert_carrier_verdict_is_clean, + inert_carrier_unrostered_names, + inert_carrier_stale_row_names, + list_contains_str, count_not_in_roster, count_stale_roster, empty_inert_carrier_names @@ -16,6 +21,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly data roster_one: List = ["KnownEntry"] data names_with_unknown: List = ["UnknownEntry"] +data names_known_only: List = ["KnownEntry"] test fn inert_carrier_no_unrostered_or_stale() -> Bool { return inert_carrier_clean_holds() @@ -32,3 +38,35 @@ test fn count_not_in_roster_detects_unrostered() -> Bool { test fn count_stale_roster_detects_stale_entry() -> Bool { return count_stale_roster(roster: roster_one, inert_names: empty_inert_carrier_names) == 1 } + +test fn verdict_clean_when_roster_matches_live_inert_names() -> Bool { + return inert_carrier_verdict_is_clean(v: inert_carrier_roster_verdict(names: names_known_only, roster: roster_one)) +} + +test fn unrostered_population_names_the_carrier_needing_a_row() -> Bool { + let v = inert_carrier_roster_verdict(names: names_with_unknown, roster: empty_inert_carrier_names) + let unrostered = inert_carrier_unrostered_names(v: v) + return inert_carrier_verdict_is_clean(v: v) == false + && length(xs: unrostered) == 1 + && list_contains_str(xs: unrostered, target: "UnknownEntry") + && length(xs: inert_carrier_stale_row_names(v: v)) == 0 +} + +test fn stale_population_names_the_row_needing_deletion() -> Bool { + let v = inert_carrier_roster_verdict(names: empty_inert_carrier_names, roster: roster_one) + let stale = inert_carrier_stale_row_names(v: v) + return inert_carrier_verdict_is_clean(v: v) == false + && length(xs: stale) == 1 + && list_contains_str(xs: stale, target: "KnownEntry") + && length(xs: inert_carrier_unrostered_names(v: v)) == 0 +} + +test fn the_two_populations_are_reported_separately() -> Bool { + let v = inert_carrier_roster_verdict(names: names_with_unknown, roster: roster_one) + let unrostered = inert_carrier_unrostered_names(v: v) + let stale = inert_carrier_stale_row_names(v: v) + return list_contains_str(xs: unrostered, target: "UnknownEntry") + && (list_contains_str(xs: unrostered, target: "KnownEntry") == false) + && list_contains_str(xs: stale, target: "KnownEntry") + && (list_contains_str(xs: stale, target: "UnknownEntry") == false) +} From a872d98ec359340ab36ec3c59f55c6bef5caf479 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 24 Aug 2026 19:12:04 +0000 Subject: [PATCH 2/2] One partition fold, one source annotation (codex/gpt-5.6-sol review 55512) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Both findings are real; neither is cosmetic. (1) The three coproduct-matching Bool predicates are gone, and so is the reason they existed. inert_carrier_finding_is_unrostered, inert_carrier_finding_is_stale_row and inert_carrier_finding_carrier were three separate matches over InertCarrierFinding, and the two name projections then filtered the SAME list twice -- so the question "which population is this finding in" was answered in four places, and adding a third variant would have compiled cleanly into all of them (each new carrier silently absent from both lists). Replaced by one InertCarrierPopulations { unrostered, stale_rows } record and one partition fold: inert_carrier_population_add matches each finding EXACTLY ONCE and routes it into its own field, and the two name accessors are plain field reads over that record. A new variant now fails to compile in one place, which is where the decision actually lives. inert_carrier_verdict_is_clean is no longer a match either -- it is is_empty over inert_carrier_verdict_findings, so cleanliness is derived from the payload rather than restated by a second walk of the coproduct. The module is left with exactly two matches, both payload projections (verdict -> findings, finding -> populations) and neither collapsing a variant to a Bool. (2) The remedy note was a `data ... : String` whose sole purpose was commentary -- DESIGN.md ยง4c misplaced/dead data. It is now a standalone leading `//` annotation on type InertCarrierFinding: module-scope, attached to a declaration, which is the form the initial .dag realization admits. Nothing machine-consumed moved into it; the remedies it describes are already the two variants. Re-verified by execution after the restructure (remote dispatch, release gunbc, --source-root dag --source-root src/v2): all eight arms of inert_carrier_test return true. New discriminating RED for the new construction -- pointing the StaleInertCarrierRow arm of the partition fold at the unrostered field turns stale_population_names_the_row_needing_deletion and the_two_populations_are_reported_separately false. The previous RED control mutated a predicate that no longer exists, so it is replaced rather than kept. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01NMvpakyTk5X3YBh1wRqyqU --- src/v2/lens/inert_carrier.dag | 84 +++++++++++++++++------------------ 1 file changed, 40 insertions(+), 44 deletions(-) diff --git a/src/v2/lens/inert_carrier.dag b/src/v2/lens/inert_carrier.dag index f86df0c9d54..f6ce9f27149 100644 --- a/src/v2/lens/inert_carrier.dag +++ b/src/v2/lens/inert_carrier.dag @@ -46,17 +46,31 @@ fn list_contains_str(xs: List, target: String) -> Bool { ) } +// The two populations have OPPOSITE remedies, which is why they are two +// variants and not one located list. UnrosteredInertCarrier: the carrier is +// inert in the live tree and the roster does not admit it -- the repair is to +// give it a live consumer, or (if it is deliberately staged ahead of one) to +// author a roster row with a reason and a dissolution condition. +// StaleInertCarrierRow: the roster admits a carrier that is NO LONGER inert -- +// a consumer exists, so the repair is to DELETE the row. Applying either +// remedy to the other population is wrong in both directions: rostering a live +// carrier re-opens the admission the row exists to close, and deleting a row +// for an unrostered carrier removes nothing. type InertCarrierFinding = UnrosteredInertCarrier { carrier: String } | StaleInertCarrierRow { carrier: String } +type InertCarrierPopulations { + unrostered: List + stale_rows: List +} + type InertCarrierRosterVerdict = InertCarrierRosterClean | InertCarrierRosterDiverged { findings: List } data empty_inert_carrier_findings: List = [] -data inert_carrier_finding_remedy_note: String = "The two populations have OPPOSITE remedies, which is why they are two variants and not one located list. UnrosteredInertCarrier: the carrier is inert in the live tree and the roster does not admit it -- the repair is to give it a live consumer, or (if it is deliberately staged ahead of one) to author a roster row with a reason and a dissolution condition. StaleInertCarrierRow: the roster admits a carrier that is NO LONGER inert -- a consumer exists, so the repair is to DELETE the row. Applying either remedy to the other population is wrong in both directions: rostering a live carrier re-opens the admission the row exists to close, and deleting a row for an unrostered carrier removes nothing." fn names_not_in_roster(names: List, roster: List) -> List { fold_list( @@ -123,67 +137,49 @@ fn inert_carrier_live_roster_verdict() -> InertCarrierRosterVerdict { inert_carrier_roster_verdict(names: inert_carrier_names_live(), roster: inert_carrier_rostered_names()) } -fn inert_carrier_verdict_is_clean(v: InertCarrierRosterVerdict) -> Bool { +fn inert_carrier_verdict_findings(v: InertCarrierRosterVerdict) -> List { match v { - InertCarrierRosterClean => true - InertCarrierRosterDiverged { findings: _ } => false + InertCarrierRosterClean => empty_inert_carrier_findings + InertCarrierRosterDiverged { findings } => findings } } -fn inert_carrier_finding_carrier(f: InertCarrierFinding) -> String { - match f { - UnrosteredInertCarrier { carrier } => carrier - StaleInertCarrierRow { carrier } => carrier - } +fn inert_carrier_verdict_is_clean(v: InertCarrierRosterVerdict) -> Bool { + is_empty(xs: inert_carrier_verdict_findings(v: v)) } -fn inert_carrier_finding_is_unrostered(f: InertCarrierFinding) -> Bool { - match f { - UnrosteredInertCarrier { carrier: _ } => true - StaleInertCarrierRow { carrier: _ } => false - } +data empty_inert_carrier_populations: InertCarrierPopulations = InertCarrierPopulations { + unrostered: empty_inert_carrier_names, + stale_rows: empty_inert_carrier_names } -fn inert_carrier_finding_is_stale_row(f: InertCarrierFinding) -> Bool { +fn inert_carrier_population_add(acc: InertCarrierPopulations, f: InertCarrierFinding) -> InertCarrierPopulations { match f { - UnrosteredInertCarrier { carrier: _ } => false - StaleInertCarrierRow { carrier: _ } => true - } -} - -fn inert_carrier_verdict_findings(v: InertCarrierRosterVerdict) -> List { - match v { - InertCarrierRosterClean => empty_inert_carrier_findings - InertCarrierRosterDiverged { findings } => findings + UnrosteredInertCarrier { carrier } => InertCarrierPopulations { + unrostered: list_snoc_item(xs: acc.unrostered, item: carrier), + stale_rows: acc.stale_rows + } + StaleInertCarrierRow { carrier } => InertCarrierPopulations { + unrostered: acc.unrostered, + stale_rows: list_snoc_item(xs: acc.stale_rows, item: carrier) + } } } -fn inert_carrier_unrostered_names(v: InertCarrierRosterVerdict) -> List { +fn inert_carrier_populations(v: InertCarrierRosterVerdict) -> InertCarrierPopulations { fold_list( xs: inert_carrier_verdict_findings(v: v), - empty: empty_inert_carrier_names, - cons: fn(acc, f) { - if inert_carrier_finding_is_unrostered(f: f) { - list_snoc_item(xs: acc, item: inert_carrier_finding_carrier(f: f)) - } else { - acc - } - } + empty: empty_inert_carrier_populations, + cons: fn(acc, f) { inert_carrier_population_add(acc: acc, f: f) } ) } +fn inert_carrier_unrostered_names(v: InertCarrierRosterVerdict) -> List { + inert_carrier_populations(v: v).unrostered +} + fn inert_carrier_stale_row_names(v: InertCarrierRosterVerdict) -> List { - fold_list( - xs: inert_carrier_verdict_findings(v: v), - empty: empty_inert_carrier_names, - cons: fn(acc, f) { - if inert_carrier_finding_is_stale_row(f: f) { - list_snoc_item(xs: acc, item: inert_carrier_finding_carrier(f: f)) - } else { - acc - } - } - ) + inert_carrier_populations(v: v).stale_rows } fn inert_carrier_clean_holds() -> Bool {