From 23f8c1b43ab150d4d36c0c22fac457c359fad739 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 23:04:30 +0000 Subject: [PATCH 1/4] Decompose the Set carrier: the predicate half names PointwisePower, and the fork's open half is declared `std.types` names one spelling for two carriers. A TYPE position takes the `container_template_alias_rows` hop on to the target inhabitant row and lowers `Set` to `im::OrdSet`; a RECORD-LITERAL position takes the `container_template_algebra` hop and stops at the modeled algebra struct, `Rc>`. Where one compiled closure holds both, the two meet as a rustc refusal -- 27 of the 331 blocks on the 03_ingest board, in two shapes: 17 E0560 (the algebra name leaking as a Rust type at a construction site) and 10 E0609 (the carrier's own field read off the realized type). Per the standing ruling "decompose, do not choose": `Set` names the finite collection, and the predicate keeps its own authority under its own name. Every corpus site in src/v2 that constructs by characteristic function or reads `.member` now names `std.algebra` `PointwisePower` directly -- 37 literals, 26 `.member` consumers, 128 occurrences across 20 files. All 37 literals were read individually and all 37 are characteristic functions; none was a finite enumeration mis-spelled. Nothing in the finite-`Set` population moved (`std.graph` `visited`, `std.authorization_profile` `EnumeratedAudience.members`, `std.syllogism`, `std.occurrence_binding_candidates`, `gunbc.package_delivery`, the `dag/`-rooted emit templates): every one of those is fed by `empty_set` / `set_insert` and read by `set_contains`, never by `member`. WHAT THIS DOES NOT DO, declared rather than left to be rediscovered. The alias row itself still reads `type Set = PointwisePower`, so `Set { member: .. }` is still writable and nothing refuses a new one -- the class sits at MITIGATABLE (DESIGN 4b), not at a wall. The retarget that would make it unwritable is a `std` authority change whose only verification is a whole-corpus compile, and it has to move together with the Map row, whose 145 literals are untouched here. The obligation and its next-rung trigger are recorded on the declaration itself, in the annotation above `type Set` in `dag/std/types.dag`. That leaves the 9 `Map { lookup: .. }` blocks of the 27 open; the 18 Set-shaped ones close. Measured: `gunbc compile --entry src/v2/compiler/03_ingest.dag --source-root dag --source-root src/v2` runs frontend, normalize, reconcile and analyses to completion and reports 52 hard diagnostics, none of which names `Set`, `PointwisePower` or `member` -- all 52 are the pre-existing source-annotation class in `dag/test/manual/command_runner_local_argv_receipt_test.dag`, which this change does not touch. The emitted-block count is NOT re-measured here: "18 of 27 close" is derived from the site-to-literal correspondence, and is a prediction about the next board rather than a measurement of one. Receipts: docs/probes/set_carrier_decomposition_2026-08-23.md Co-Authored-By: Claude Opus 5 (1M context) --- dag/std/types.dag | 18 ++++ .../set_carrier_decomposition_2026-08-23.md | 84 +++++++++++++++++++ src/v2/compiler/02_parse.dag | 60 ++++++------- src/v2/compiler/03_resolve.dag | 8 +- src/v2/extdeps/languages/cpp.dag | 6 +- src/v2/extdeps/languages/dag.dag | 16 ++-- src/v2/extdeps/languages/ecmascript.dag | 6 +- src/v2/extdeps/languages/go.dag | 6 +- src/v2/extdeps/languages/java.dag | 10 +-- src/v2/extdeps/languages/kotlin.dag | 6 +- src/v2/extdeps/languages/lean.dag | 6 +- src/v2/extdeps/languages/python.dag | 6 +- src/v2/extdeps/languages/rust.dag | 16 ++-- src/v2/extdeps/languages/swift.dag | 6 +- src/v2/extdeps/languages/typescript.dag | 14 ++-- src/v2/extdeps/languages/wasm.dag | 6 +- src/v2/lens/subsumption.dag | 14 ++-- src/v2/std/collection.dag | 2 +- src/v2/std/grammar.dag | 26 +++--- src/v2/std/language_model.dag | 10 +-- .../claim/grammar/validate_grammar_test.dag | 16 ++-- ...dissolution_subsumption_reverification.dag | 22 ++--- .../claim/parse/parse_table_claims_test.dag | 4 +- 23 files changed, 236 insertions(+), 132 deletions(-) create mode 100644 docs/probes/set_carrier_decomposition_2026-08-23.md diff --git a/dag/std/types.dag b/dag/std/types.dag index 4049749310d..5a3939b4689 100644 --- a/dag/std/types.dag +++ b/dag/std/types.dag @@ -104,6 +104,24 @@ type Bytes type Char = Int where unicode_scalar, brand("Char") type List = FreeMonoid +// ONE SPELLING, TWO CARRIERS -- the open half of the collection-realization fork, stated where the +// fusion is authored rather than where it surfaces. `Set` names a predicate here and a finite +// enumeration at every realization: `extdeps.languages.rust.types` gives `PointwisePower` the +// inhabitant `BTreeSet<{0}>`, so a declaration position lowers to `im::OrdSet` while a record +// literal `Set { member: .. }` lowers to the algebra struct, and the two meet as a rustc refusal +// wherever one compiled closure holds both. Measured at +// `docs/probes/t3_collection_realization_2026-08-22.md`. +// +// The PREDICATE half is closed: every corpus site that constructs by characteristic function or +// reads `.member` now names `std.algebra` `PointwisePower` directly, so no `Set { member: .. }` +// literal survives in `src/v2`. What is NOT closed is this alias -- `Set` still resolves to the +// predicate carrier, so the literal is still writable and nothing refuses a new one. Making it +// unwritable is a retarget of this row onto the finite carrier, and it is deliberately not taken +// here: it is a `std` authority change whose only verification is a whole-corpus compile, and the +// Map half of the same fork (`Map { lookup: .. }`, 145 literals) is untouched and would have to +// move with it. NEXT-RUNG TRIGGER: the Map-side decomposition landing, after which both rows +// retarget in one motion. Until then the class sits at MITIGATABLE (DESIGN 4b) -- the invalid +// state is writable and only review sees it. type Set = PointwisePower type Map = PartialFunction diff --git a/docs/probes/set_carrier_decomposition_2026-08-23.md b/docs/probes/set_carrier_decomposition_2026-08-23.md new file mode 100644 index 00000000000..7ce5b1949d9 --- /dev/null +++ b/docs/probes/set_carrier_decomposition_2026-08-23.md @@ -0,0 +1,84 @@ +# The predicate half of the Set/Map carrier fork, decomposed (2026-08-23) + +**Work item:** `node://adhoc-66adece2-31f`. **Session:** `silent-gull-867`. +Measurement this rests on and does not restate: +[`t3_collection_realization_2026-08-22.md`](t3_collection_realization_2026-08-22.md) (the E0308 half) +and [`board_2026-08-23/README.md`](board_2026-08-23/README.md) (the retained log this brief's 27 +blocks were partitioned from). + +## The 27 blocks, at `.dag` grain + +Subject `src/v2/compiler/03_ingest.dag`, ref `98b18cdc81e`, board `CARGO_ERROR_TOTAL=330`. The brief +names 27 blocks in two shapes; both are the same fork read from two positions. + +| shape | code | blocks | what rustc saw | +|---|---|---:|---| +| the algebra name leaks as a Rust type | `E0560` | 17 | `struct Rc> has no field named member` (8) · `struct Rc> has no field named lookup` (9) | +| the carrier's own field read off the realized type | `E0609` | 10 | `no field member on type Rc>` | + +Both come from `std.types` naming one spelling for two carriers. A **type** position takes the +`container_template_alias_rows` hop on to the target inhabitant row and lowers `Set` to +`im::OrdSet`; a **record-literal** position takes the `container_template_algebra` hop and stops +at the modeled algebra struct, `Rc>`. Where one compiled closure holds both, the +two meet as a refusal. + +## What this change does + +Every corpus site that **constructs by characteristic function** or **reads `.member`** now names +`std.algebra` `PointwisePower` directly, under its own authority, instead of borrowing `Set`. The +populations were read individually, not sampled: + +| | count | +|---|---:| +| `Set { member: … }` literals in `src/v2` before | 37 | +| — of them, characteristic functions | 37 | +| — of them, finite enumerations mis-spelled | 0 | +| `Set { … }` literals in `src/v2` after | 0 | +| `.member(` call sites re-pointed | 26 | +| `Set<…>` declarations re-typed to `PointwisePower<…>` | 128 occurrences across 20 files | + +Nothing in the finite-`Set` population moved: `std.graph` `visited`, `std.authorization_profile` +`EnumeratedAudience.members`, `std.occurrence_binding_candidates`, `std.syllogism`, +`gunbc.package_delivery`, and the `dag/`-rooted emit templates keep `Set` and keep the `OrdSet` +realization, because every one of them is fed by `empty_set` / `set_insert` and read by +`set_contains` — the finite surface, never `member`. + +This closes the 18 blocks of the 27 that are Set-shaped (8 `E0560` + all 10 `E0609`). The 9 +remaining are `Map { lookup: … }`, and they are **not** closed here — see below. + +## What is deliberately left open, and why + +1. **The Map half.** `Map` needs no retarget — `PartialFunction`'s template roster already *is* the + finite map surface — but its 145 corpus literals do need re-authoring onto the construction route + `std.primitives` already declares (`empty_map_contract`, `map_insert_contract`; the second is + bound in `v2.std.collection` `map_insert_host_binding` and then not used, the function writing a + closure chain instead). 97 of those 145 are `lookup: ` delegates whose key list has to + be read out of the delegate body one at a time. That is a lane, not a rider on this one. +2. **The alias itself.** `std.types` still reads `type Set = PointwisePower`, so + `Set { member: … }` is still *writable* — nothing refuses a new one. Making it unwritable is a + retarget of that row onto the finite carrier, which is a `std` authority change whose only + verification is a whole-corpus compile, and which has to move together with the Map row. The + obligation is recorded on the declaration itself (`dag/std/types.dag`, the annotation above + `type Set`), with the next-rung trigger named there: the Map-side decomposition landing. Until + then the class sits at **mitigatable** (DESIGN §4b) and only review sees a regression. + +So the honest statement of the rung: this change removes the fork's instances on the Set side and +does not yet make the Set side's invalid state unwritable. + +## Controls + +- **The re-typed population is exactly the predicate population.** Two independent instruments + agree: a grep for `Set {` literals (37, each read) and a grep for `.member(` consumers (26, each + read). No site was found that constructs a `Set` literal and then enumerates it, and no finite- + surface call (`set_contains` / `set_insert` / `empty_set`) appears in any re-typed declaration's + module against a re-typed value. +- **The rewrite could not touch string data or prose.** The edit was applied outside double-quoted + spans and outside `//` annotation lines; the two `"Set"` string literals in + `v2.extdeps.languages.rust` (`target_collection_set_carrier` rows) are unchanged, and the two + prose blocks that cite the grounding (`v2.std.grammar`'s sync-token note and + `v2.compiler.02_parse`'s convergence-measure note) were updated by hand, not by the rewrite. +- **Not verified here:** the emitted-Rust block count. Re-measuring the board requires the probe + dispatch, and this change is landed against the `.dag` acceptance path (`gunbc compile --entry + src/v2/compiler/03_ingest.dag`) rather than against a re-run of `curated_cargo_probe_one.sh`. The + claim "18 of 27 close" is derived from the site-to-literal correspondence above, and is a + prediction about the next board, not a measurement of one. diff --git a/src/v2/compiler/02_parse.dag b/src/v2/compiler/02_parse.dag index f2b78590cfe..28b0aa445a4 100644 --- a/src/v2/compiler/02_parse.dag +++ b/src/v2/compiler/02_parse.dag @@ -87,7 +87,7 @@ import v2.std.provenance { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, list_at_optional, map_get, @@ -277,7 +277,7 @@ type ParseTableRealization { memo_hits: Int memo_misses: Int memo_lookup_calls: Int - nullable_set: Set + nullable_set: PointwisePower first_rows: Map> productions_by_name: Map } @@ -634,7 +634,7 @@ fn parse_table_empty() -> ParseTable { memo_hits: 0, memo_misses: 0, memo_lookup_calls: 0, - nullable_set: Set { member: fn(_) { false } }, + nullable_set: PointwisePower { member: fn(_) { false } }, first_rows: empty_map(), productions_by_name: empty_map() } @@ -1166,13 +1166,13 @@ fn parse_nonterminal_memoized_core( } } -fn set_symbol_insert(s: Set, item: Symbol) -> Set { - Set { +fn set_symbol_insert(s: PointwisePower, item: Symbol) -> PointwisePower { + PointwisePower { member: fn(sym) { sym == item || s.member(sym) } } } -fn expr_is_nullable_given_set(expr: GrammarExpr, nullable_set: Set) -> Bool { +fn expr_is_nullable_given_set(expr: GrammarExpr, nullable_set: PointwisePower) -> Bool { fold_grammar_expr( expr: expr, algebra: GrammarExprFold { @@ -1186,7 +1186,7 @@ fn expr_is_nullable_given_set(expr: GrammarExpr, nullable_set: Set) -> B ) } -fn compute_nullable_step(ns: Set, p: GrammarProduction) -> Set { +fn compute_nullable_step(ns: PointwisePower, p: GrammarProduction) -> PointwisePower { if expr_is_nullable_given_set(expr: p.expression, nullable_set: ns) { set_symbol_insert(s: ns, item: p.name) } else { @@ -1196,7 +1196,7 @@ fn compute_nullable_step(ns: Set, p: GrammarProduction) -> Set { // ONE ROUND of the nullable fixpoint: every production gets a chance to join the set given what // the set already holds. -fn compute_nullable_round(root: GrammarRoot, ns: Set) -> Set { +fn compute_nullable_round(root: GrammarRoot, ns: PointwisePower) -> PointwisePower { fold_list( xs: root.productions, empty: ns, @@ -1206,13 +1206,13 @@ fn compute_nullable_round(root: GrammarRoot, ns: Set) -> Set { ) } -// THE CONVERGENCE MEASURE. `Set` is a `PointwisePower` — a characteristic function — so two sets -// cannot be compared directly, and the fixpoint cannot stop by testing `next == previous`. It can +// THE CONVERGENCE MEASURE. The carrier is a `PointwisePower` — a characteristic function — so two +// sets cannot be compared directly, and the fixpoint cannot stop by testing `next == previous`. It can // stop on a MONOTONE MEASURE instead: `compute_nullable_step` only ever inserts, so the number of // productions the set admits rises until the round adds nothing, and equal counts across a round // mean equal sets. Counting over `root.productions` is exact here because that is the only // population `compute_nullable_step` can insert from. -fn nullable_member_count(root: GrammarRoot, ns: Set) -> Int { +fn nullable_member_count(root: GrammarRoot, ns: PointwisePower) -> Int { fold_list( xs: root.productions, empty: 0, @@ -1232,10 +1232,10 @@ fn nullable_member_count(root: GrammarRoot, ns: Set) -> Int { // a round adds nothing, so the RESULT is identical and only the redundant rounds are gone. fn compute_nullable_fixpoint( root: GrammarRoot, - ns: Set, + ns: PointwisePower, seen_count: Int, fuel: Int -) -> Set { +) -> PointwisePower { if fuel == 0 { ns } else { @@ -1249,10 +1249,10 @@ fn compute_nullable_fixpoint( } } -fn compute_nullable_set(root: GrammarRoot) -> Set { +fn compute_nullable_set(root: GrammarRoot) -> PointwisePower { compute_nullable_fixpoint( root: root, - ns: Set { member: fn(_) { false } }, + ns: PointwisePower { member: fn(_) { false } }, seen_count: 0, fuel: length(xs: root.productions) ) @@ -1264,7 +1264,7 @@ type GrammarExprFirstFold { } type GrammarFirstAnalysis { - nullable_set: Set + nullable_set: PointwisePower first_rows: Map> } @@ -1314,7 +1314,7 @@ fn expr_first_fold_terminal(token_class: Symbol) -> GrammarExprFirstFold { fn expr_first_fold_nonterminal( name: Symbol, - nullable_set: Set, + nullable_set: PointwisePower, first_rows: Map> ) -> GrammarExprFirstFold { GrammarExprFirstFold { @@ -1350,7 +1350,7 @@ fn expr_first_fold_repeat(element: GrammarExprFirstFold) -> GrammarExprFirstFold fn expr_first_fold( expr: GrammarExpr, - nullable_set: Set, + nullable_set: PointwisePower, first_rows: Map> ) -> GrammarExprFirstFold { fold_grammar_expr( @@ -1371,7 +1371,7 @@ fn expr_first_fold( fn compute_production_first_row_terminals( rows: Map>, p: GrammarProduction, - nullable_set: Set + nullable_set: PointwisePower ) -> List { expr_first_fold( expr: p.expression, @@ -1382,7 +1382,7 @@ fn compute_production_first_row_terminals( fn compute_production_first_rows_round( root: GrammarRoot, - nullable_set: Set, + nullable_set: PointwisePower, rows: Map> ) -> Map> { fold_list( @@ -1419,7 +1419,7 @@ fn production_first_rows_total(root: GrammarRoot, rows: Map fn compute_production_first_rows_fixpoint( root: GrammarRoot, - nullable_set: Set, + nullable_set: PointwisePower, rows: Map>, seen_total: Int, fuel: Int @@ -1445,7 +1445,7 @@ fn compute_production_first_rows_fixpoint( fn compute_production_first_rows( root: GrammarRoot, - nullable_set: Set + nullable_set: PointwisePower ) -> Map> { compute_production_first_rows_fixpoint( root: root, @@ -1489,7 +1489,7 @@ fn append_choice_ambiguity_row( fn collect_choice_ambiguities_in_expr( expr: GrammarExpr, production: Symbol, - nullable_set: Set, + nullable_set: PointwisePower, first_rows: Map>, acc: List ) -> List { @@ -1554,7 +1554,7 @@ fn collect_choice_ambiguities_in_expr( fn compute_grammar_first_analysis_given( root: GrammarRoot, - nullable_set: Set + nullable_set: PointwisePower ) -> GrammarFirstAnalysis { GrammarFirstAnalysis { nullable_set: nullable_set, @@ -1656,7 +1656,7 @@ fn expr_corner_fold_terminal(_: Symbol) -> GrammarExprCornerFold { GrammarExprCornerFold { corners: std.algebra.Empty, nullable: false } } -fn expr_corner_fold_nonterminal(name: Symbol, nullable_set: Set) -> GrammarExprCornerFold { +fn expr_corner_fold_nonterminal(name: Symbol, nullable_set: PointwisePower) -> GrammarExprCornerFold { GrammarExprCornerFold { corners: Cons { head: name, tail: std.algebra.Empty }, nullable: nullable_set.member(name) @@ -1699,7 +1699,7 @@ fn expr_corner_fold_repeat(element_fold: GrammarExprCornerFold) -> GrammarExprCo GrammarExprCornerFold { corners: element_fold.corners, nullable: true } } -fn expr_corner_nullable_fold(expr: GrammarExpr, nullable_set: Set) -> GrammarExprCornerFold { +fn expr_corner_nullable_fold(expr: GrammarExpr, nullable_set: PointwisePower) -> GrammarExprCornerFold { fold_grammar_expr( expr: expr, algebra: GrammarExprFold { @@ -1713,7 +1713,7 @@ fn expr_corner_nullable_fold(expr: GrammarExpr, nullable_set: Set) -> Gr ) } -fn expr_direct_left_corner_list(expr: GrammarExpr, nullable_set: Set) -> List { +fn expr_direct_left_corner_list(expr: GrammarExpr, nullable_set: PointwisePower) -> List { expr_corner_nullable_fold(expr: expr, nullable_set: nullable_set).corners } @@ -1744,7 +1744,7 @@ fn left_corner_list_union(left: List, right: List) -> List) -> Map> { +fn left_corner_direct_rows(root: GrammarRoot, nullable_set: PointwisePower) -> Map> { fold_list( xs: root.productions, empty: empty_map(), @@ -1825,7 +1825,7 @@ fn left_corner_fixpoint( } } -fn left_corner_rows(root: GrammarRoot, nullable_set: Set) -> Map> { +fn left_corner_rows(root: GrammarRoot, nullable_set: PointwisePower) -> Map> { let seeded = left_corner_direct_rows(root: root, nullable_set: nullable_set) left_corner_fixpoint( root: root, @@ -1838,7 +1838,7 @@ fn left_corner_rows(root: GrammarRoot, nullable_set: Set) -> Map) -> Bool { +fn grammar_has_left_recursion_given(root: GrammarRoot, nullable_set: PointwisePower) -> Bool { let rows = left_corner_rows(root: root, nullable_set: nullable_set) any( xs: root.productions, diff --git a/src/v2/compiler/03_resolve.dag b/src/v2/compiler/03_resolve.dag index 5c162468d25..9ab1d59e60a 100644 --- a/src/v2/compiler/03_resolve.dag +++ b/src/v2/compiler/03_resolve.dag @@ -16,7 +16,7 @@ import std.algebra { Cons, Empty, FreeMonoid } import v2.std.algebra { length, list_snoc_item } import v2.std.collection { Map, - Set, + PointwisePower, empty_map, map_get, map_insert @@ -87,7 +87,7 @@ type ResolvedTree = Node type Namespace { bindings: Map - canonical_symbols: Set + canonical_symbols: PointwisePower symbol_index: SymbolIndex module_qn: QualifiedName } @@ -128,8 +128,8 @@ fn empty_namespace() -> Namespace { } } -fn empty_canonical_symbol_set() -> Set { - Set { +fn empty_canonical_symbol_set() -> PointwisePower { + PointwisePower { member: fn(_) { false } diff --git a/src/v2/extdeps/languages/cpp.dag b/src/v2/extdeps/languages/cpp.dag index 96cef0f9310..063147f0a58 100644 --- a/src/v2/extdeps/languages/cpp.dag +++ b/src/v2/extdeps/languages/cpp.dag @@ -39,7 +39,7 @@ import v2.std.compilers.target_model { TargetModel, target_model_emit_transforms import v2.std.logic { Bool, bool_boolean_algebra } import std.algebra { Empty } import v2.std.algebra { BooleanAlgebra, boolean_algebra_node, commutative_semiring_node, fold_list, list_append, list_snoc_item, ordered_ring_node } -import v2.std.collection { Absent, List, Map, Present, Set, empty_map, map_insert } +import v2.std.collection { Absent, List, Map, PointwisePower, Present, empty_map, map_insert } import v2.std.model_core { AlgebraInhabitanceDecl, EffectSemanticsDecl, @@ -584,8 +584,8 @@ fn cpp_catalog_surface_symbol(sym: Symbol, target_profile: Node) -> Bool { cpp_bool_catalog_surface_symbol(sym: sym) } -fn cpp_language_model_canonical_symbols(target_profile: Node) -> Set { - Set { +fn cpp_language_model_canonical_symbols(target_profile: Node) -> PointwisePower { + PointwisePower { member: fn(sym) { cpp_catalog_surface_symbol(sym: sym, target_profile: target_profile) } diff --git a/src/v2/extdeps/languages/dag.dag b/src/v2/extdeps/languages/dag.dag index f8f603e05bd..76e6cef94fb 100644 --- a/src/v2/extdeps/languages/dag.dag +++ b/src/v2/extdeps/languages/dag.dag @@ -5,7 +5,7 @@ import v2.std.language_model { LanguageModel } import v2.std.host_transport { target_emit_host_runtime_row_unconfigured, TargetEmitHostRuntimeRow } import v2.std.collection { List, - Set, + PointwisePower, Map, empty_map, list_at_optional, @@ -3371,8 +3371,8 @@ fn dag_grammar() -> ParseGrammar { ModeledGrammar { root: dag_grammar_root() } } -fn dag_language_model_surface_prelude_atoms() -> Set { - Set { +fn dag_language_model_surface_prelude_atoms() -> PointwisePower { + PointwisePower { member: fn(sym) { sym == ^dag_c3_surface_sugar_service || sym == ^dag_c3_surface_sugar_fn || @@ -3383,8 +3383,8 @@ fn dag_language_model_surface_prelude_atoms() -> Set { } } -fn dag_language_model_empty_canonical_symbol_set() -> Set { - Set { +fn dag_language_model_empty_canonical_symbol_set() -> PointwisePower { + PointwisePower { member: fn(_) { false } @@ -3406,8 +3406,8 @@ fn dag_language_model_binding_canonical(sym: Symbol) -> Bool { || sym == ^dag_loop_measure_sym } -fn dag_canonical_symbols() -> Set { - Set { +fn dag_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { dag_language_model_surface_prelude_atoms().member(sym) || grammar_carries_symbol(grammar: dag_grammar(), sym: sym) || @@ -3446,7 +3446,7 @@ fn dag_language_model_surface_empty_prelude() -> LanguageModel { } } -fn dag_language_model_canonical_symbols(lm: LanguageModel) -> Set { +fn dag_language_model_canonical_symbols(lm: LanguageModel) -> PointwisePower { lm.canonical_symbols } diff --git a/src/v2/extdeps/languages/ecmascript.dag b/src/v2/extdeps/languages/ecmascript.dag index 02e00e624c1..59710250f57 100644 --- a/src/v2/extdeps/languages/ecmascript.dag +++ b/src/v2/extdeps/languages/ecmascript.dag @@ -57,7 +57,7 @@ import v2.std.compilers.lexing { import v2.std.compilers.target_model { ProducedDeclUnwired, ConcreteSyntaxToken, FixedToken, BoundToken, concrete_syntax_token_class, concrete_syntax_token_to_node } import v2.std.compilers.target_model { TargetModel, target_model_emit_transforms_empty } -import v2.std.collection { List, Map, Set, empty_map, map_insert } +import v2.std.collection { List, Map, PointwisePower, empty_map, map_insert } import v2.std.model_core { AlgebraInhabitanceDecl, EffectSemanticsDecl, @@ -1315,8 +1315,8 @@ fn ecmascript_catalog_surface_symbol(sym: Symbol) -> Bool { ecmascript_singleton_catalog_surface_symbol(sym: sym) } -fn ecmascript_language_model_canonical_symbols() -> Set { - Set { +fn ecmascript_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { ecmascript_catalog_surface_symbol(sym: sym) || ecmascript_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/go.dag b/src/v2/extdeps/languages/go.dag index 660a5020c80..b5c9abb5c25 100644 --- a/src/v2/extdeps/languages/go.dag +++ b/src/v2/extdeps/languages/go.dag @@ -41,7 +41,7 @@ import v2.std.compilers.lexing { TriviaRule, lex_rule_set_token_class_member } -import v2.std.collection { Absent, List, Map, Present, Set, empty_map, map_insert, optional_absent } +import v2.std.collection { Absent, List, Map, PointwisePower, Present, empty_map, map_insert, optional_absent } import v2.std.model_core { AlgebraInhabitanceDecl, EffectSemanticsDecl, @@ -2137,8 +2137,8 @@ fn go_catalog_surface_symbol(sym: Symbol) -> Bool { go_string_catalog_surface_symbol(sym: sym) } -fn go_language_model_canonical_symbols() -> Set { - Set { +fn go_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { go_catalog_surface_symbol(sym: sym) || go_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/java.dag b/src/v2/extdeps/languages/java.dag index 855d820d050..5a33a634d3b 100644 --- a/src/v2/extdeps/languages/java.dag +++ b/src/v2/extdeps/languages/java.dag @@ -46,7 +46,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, map_insert } @@ -1490,8 +1490,8 @@ fn java_grammar() -> ParseGrammar { ModeledGrammar { root: java_grammar_root() } } -fn java_canonical_symbols() -> Set { - Set { +fn java_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { java_catalog_surface_symbol(sym: sym) || sym == ^java_surface_spelling_void || @@ -1588,8 +1588,8 @@ fn java_method_add_lex_token_symbol(sym: Symbol) -> Bool { sym == ^java_token_semicolon } -fn java_language_model_canonical_symbols() -> Set { - Set { +fn java_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { java_catalog_surface_symbol(sym: sym) || sym == ^java_surface_spelling_void || diff --git a/src/v2/extdeps/languages/kotlin.dag b/src/v2/extdeps/languages/kotlin.dag index cfa1a45cec9..9e1062c2979 100644 --- a/src/v2/extdeps/languages/kotlin.dag +++ b/src/v2/extdeps/languages/kotlin.dag @@ -55,7 +55,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, map_insert } @@ -2530,8 +2530,8 @@ fn kotlin_lex_token_symbol(sym: Symbol) -> Bool { ) } -fn kotlin_language_model_canonical_symbols() -> Set { - Set { +fn kotlin_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { kotlin_catalog_surface_symbol(sym: sym) || kotlin_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/lean.dag b/src/v2/extdeps/languages/lean.dag index 1955dcd139f..77d6423f950 100644 --- a/src/v2/extdeps/languages/lean.dag +++ b/src/v2/extdeps/languages/lean.dag @@ -35,7 +35,7 @@ import v2.std.compilers.lexing { TokenRule, lex_rule_set_token_class_member } -import v2.std.collection { Absent, List, Map, Optional, Present, Set } +import v2.std.collection { Absent, List, Map, Optional, PointwisePower, Present } import v2.std.logic { Bool, bool_boolean_algebra } import extdeps.languages.lean.overflow { lean_upstream_fixed_width_overflow_returns_rule } import std.algebra { Cons, Empty } @@ -872,8 +872,8 @@ fn lean_ingest_grammar_probe() -> GrammarSchemaProbeBinding { data lean_ingest_grammar_probe_authority: GrammarSchemaProbeBinding = lean_ingest_grammar_probe() -fn lean_language_model_canonical_symbols() -> Set { - Set { +fn lean_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { lean_catalog_surface_symbol(sym: sym) || lean_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/python.dag b/src/v2/extdeps/languages/python.dag index 39d278968c4..dd044a82c5a 100644 --- a/src/v2/extdeps/languages/python.dag +++ b/src/v2/extdeps/languages/python.dag @@ -54,7 +54,7 @@ import v2.std.compilers.lexing { import v2.std.compilers.target_model { ProducedDeclUnwired, ConcreteSyntaxToken, FixedToken, BoundToken, concrete_syntax_token_class, concrete_syntax_token_to_node } import v2.std.compilers.target_model { TargetModel, target_model_emit_transforms_empty } -import v2.std.collection { List, Map, Set, empty_map, map_insert } +import v2.std.collection { List, Map, PointwisePower, empty_map, map_insert } import v2.std.host_transport { EmitHostRuntimeRow, HostRuntimeRowPresent, @@ -1530,8 +1530,8 @@ fn python_catalog_surface_symbol(sym: Symbol) -> Bool { python_singleton_catalog_surface_symbol(sym: sym) } -fn python_language_model_canonical_symbols() -> Set { - Set { +fn python_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { python_catalog_surface_symbol(sym: sym) || python_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/rust.dag b/src/v2/extdeps/languages/rust.dag index 7c3249de27e..c5356d38c3f 100644 --- a/src/v2/extdeps/languages/rust.dag +++ b/src/v2/extdeps/languages/rust.dag @@ -88,7 +88,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, list_at_optional, map_insert, @@ -1765,15 +1765,15 @@ fn rust_hash_set_supplemental_generic_bound_contracts() -> Map + requirements: PointwisePower authority: ExternalAuthority coverage: RustSupplementalGenericBoundContractCoverageDisposition } fn rust_hash_set_eq_hash_supplemental_generic_bound_requirements( representation_parameter: Symbol -) -> Set { - Set { +) -> PointwisePower { + PointwisePower { member: fn(requirement) { fold_list( xs: [ @@ -3078,8 +3078,8 @@ fn rust_fn_add_lex_token_symbol(sym: Symbol) -> Bool { lex_rule_set_token_class_member(rules: rust_fn_add_lex_rules(), token_class: sym) } -fn rust_language_model_canonical_symbols() -> Set { - Set { +fn rust_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { rust_catalog_surface_symbol(sym: sym) || rust_fn_add_lex_token_symbol(sym: sym) || @@ -4365,8 +4365,8 @@ fn rust_grammar() -> ParseGrammar { ModeledGrammar { root: rust_grammar_root() } } -fn rust_canonical_symbols() -> Set { - Set { +fn rust_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { rust_catalog_surface_symbol(sym: sym) || lex_rule_set_token_class_member(rules: rust_lex_rules(), token_class: sym) || diff --git a/src/v2/extdeps/languages/swift.dag b/src/v2/extdeps/languages/swift.dag index 23e2afe780d..5af6f790f0b 100644 --- a/src/v2/extdeps/languages/swift.dag +++ b/src/v2/extdeps/languages/swift.dag @@ -56,7 +56,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, map_insert } @@ -1817,8 +1817,8 @@ fn swift_catalog_surface_symbol(sym: Symbol) -> Bool { swift_nonnumeric_catalog_surface_symbol(sym: sym) } -fn swift_language_model_canonical_symbols() -> Set { - Set { +fn swift_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { swift_catalog_surface_symbol(sym: sym) || swift_lex_token_symbol(sym: sym) || diff --git a/src/v2/extdeps/languages/typescript.dag b/src/v2/extdeps/languages/typescript.dag index fda08b6041c..5f3e3c17f57 100644 --- a/src/v2/extdeps/languages/typescript.dag +++ b/src/v2/extdeps/languages/typescript.dag @@ -54,7 +54,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, map_insert } @@ -2146,8 +2146,8 @@ fn ts_catalog_surface_symbol(sym: Symbol) -> Bool { ) } -fn ts_language_model_canonical_symbols() -> Set { - Set { +fn ts_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { ts_catalog_surface_symbol(sym: sym) || ts_fn_add_lex_token_symbol(sym: sym) || @@ -3099,8 +3099,8 @@ fn ts_grammar() -> ParseGrammar { ModeledGrammar { root: ts_grammar_root() } } -fn ts_grammar_canonical_symbols() -> Set { - Set { +fn ts_grammar_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { ts_catalog_surface_symbol(sym: sym) || ts_lex_token_symbol(sym: sym) || @@ -3645,8 +3645,8 @@ fn ts_model_core() -> ModelCore { } } -fn ts_canonical_symbols() -> Set { - Set { +fn ts_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { ts_grammar_canonical_symbols().member(sym: sym) || sym == ^ts_surface_spelling_string diff --git a/src/v2/extdeps/languages/wasm.dag b/src/v2/extdeps/languages/wasm.dag index b749c8471a0..0d35daa1239 100644 --- a/src/v2/extdeps/languages/wasm.dag +++ b/src/v2/extdeps/languages/wasm.dag @@ -52,7 +52,7 @@ import v2.std.compilers.lexing { import v2.std.collection { List, Map, - Set, + PointwisePower, empty_map, map_insert } @@ -1552,8 +1552,8 @@ fn wasm_catalog_surface_symbol(sym: Symbol) -> Bool { wasm_float_catalog_surface_symbol(sym: sym) } -fn wasm_language_model_canonical_symbols() -> Set { - Set { +fn wasm_language_model_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(sym) { wasm_catalog_surface_symbol(sym: sym) || wasm_lex_token_symbol(sym: sym) || diff --git a/src/v2/lens/subsumption.dag b/src/v2/lens/subsumption.dag index a15a327e3b2..2a02e0d1419 100644 --- a/src/v2/lens/subsumption.dag +++ b/src/v2/lens/subsumption.dag @@ -18,12 +18,12 @@ type SubsumptionVerification type DissolutionSubsumption { root_fix: DiffId - subsumed_fixes: Set + subsumed_fixes: PointwisePower verification: SubsumptionVerification } -fn affected_set_irt1_subsumed_fixes_value() -> Set { - Set { +fn affected_set_irt1_subsumed_fixes_value() -> PointwisePower { + PointwisePower { member: fn(d) { d.id == ^affected_set_boundary_receipt_leaf_fix || d.id == ^affected_set_dimension_receipt_leaf_fix || @@ -35,7 +35,7 @@ fn affected_set_irt1_subsumed_fixes_value() -> Set { } } -data affected_set_irt1_subsumed_fixes: Set = affected_set_irt1_subsumed_fixes_value() +data affected_set_irt1_subsumed_fixes: PointwisePower = affected_set_irt1_subsumed_fixes_value() data affected_set_irt1_subsumption: DissolutionSubsumption = { root_fix: DiffId { id: ^affected_set_irt1_frontier_root_fix }, @@ -45,8 +45,8 @@ data affected_set_irt1_subsumption: DissolutionSubsumption = { } } -fn rust_language_model_emit_subsumed_fixes_value() -> Set { - Set { +fn rust_language_model_emit_subsumed_fixes_value() -> PointwisePower { + PointwisePower { member: fn(d) { d.id == ^emit_rust_template_leaf_fix || d.id == ^emit_rust_name_dispatch_leaf_fix @@ -54,7 +54,7 @@ fn rust_language_model_emit_subsumed_fixes_value() -> Set { } } -data rust_language_model_emit_subsumed_fixes: Set = rust_language_model_emit_subsumed_fixes_value() +data rust_language_model_emit_subsumed_fixes: PointwisePower = rust_language_model_emit_subsumed_fixes_value() data rust_language_model_emit_subsumption: DissolutionSubsumption = { root_fix: DiffId { id: ^rust_language_model_emit_root_fix }, diff --git a/src/v2/std/collection.dag b/src/v2/std/collection.dag index edd6d90e62d..e7b48d72334 100644 --- a/src/v2/std/collection.dag +++ b/src/v2/std/collection.dag @@ -1,6 +1,6 @@ module v2.std.collection -import std.algebra { FreeMonoid } +import std.algebra { FreeMonoid, PointwisePower } import std.primitives { empty_map_contract, map_insert_contract, PrimitiveContract } import v2.std.algebra { fold_list, is_empty } import std.types { Set, Map } diff --git a/src/v2/std/grammar.dag b/src/v2/std/grammar.dag index f8a1fd550f4..5c372950cf8 100644 --- a/src/v2/std/grammar.dag +++ b/src/v2/std/grammar.dag @@ -4,7 +4,7 @@ import std.algebra { Cons, Empty } import v2.std.algebra { fold_list, fold_list_node, list_append, list_snoc_item, zip_eq } import v2.std.collection { List, - Set, + PointwisePower, list_nth } import v2.std.optional { @@ -73,8 +73,8 @@ type FormalProduction { } type FormalGrammar { - nonterminals: Set - terminals: Set + nonterminals: PointwisePower + terminals: PointwisePower productions: List start: FormalNonterminal } @@ -101,8 +101,8 @@ fn validate_grammar_diagnostic(reason: Symbol) -> Diagnostic { } fn formal_grammar_symbol_in_alphabet( - nonterminals: Set, - terminals: Set, + nonterminals: PointwisePower, + terminals: PointwisePower, symbol: FormalGrammarSymbol ) -> Bool { match symbol { @@ -114,8 +114,8 @@ fn formal_grammar_symbol_in_alphabet( } fn formal_production_rhs_in_alphabet( - nonterminals: Set, - terminals: Set, + nonterminals: PointwisePower, + terminals: PointwisePower, production: FormalProduction ) -> Bool { fold_list( @@ -294,9 +294,9 @@ type GrammarProduction { // A grammar's error-recovery sync tokens are finite and known at authoring time — every producer in // the corpus writes either an empty set or a literal list of keyword classes. Carrying them as // `Set` made them a POINTWISE-POWER characteristic function (`std.types` grounds -// `Set = PointwisePower`), which is the right grounding for a set in general and -// the wrong carrier for six literal keywords: a characteristic function cannot be enumerated, so -// the whole grammar value became unhashable through this one field. +// `Set = PointwisePower`), which is the right grounding for a predicate and the +// wrong carrier for six literal keywords: a characteristic function cannot be enumerated, so the +// whole grammar value became unhashable through this one field. // // That was not a theoretical loss. `prepare_grammar` is memoized cross-claim on // (declaration identity, content hash of the grammar), and the interpreter's content-hash walk @@ -304,8 +304,10 @@ type GrammarProduction { // language in the corpus and not only `.dag`. The measured consequence was a full ~12s grammar // preparation on every parse, including of an empty module. // -// The field is therefore the enumeration it always was. `Set` keeps its grounding untouched; what -// changed is that this field stopped borrowing a power-set to carry a list. +// The field is therefore the enumeration it always was; what changed is that this field stopped +// borrowing a power-set to carry a list. The sibling fields beside it went the other way: they are +// predicates and now say so, carrying `PointwisePower` and +// `PointwisePower` under their own name rather than under `Set`. type GrammarRoot { start: Symbol productions: List diff --git a/src/v2/std/language_model.dag b/src/v2/std/language_model.dag index c8d76d47a9b..494ef2ecece 100644 --- a/src/v2/std/language_model.dag +++ b/src/v2/std/language_model.dag @@ -1,6 +1,6 @@ module v2.std.language_model -import v2.std.collection { Set } +import v2.std.collection { PointwisePower } import v2.std.grammar { ParseGrammar, VoidGrammar, @@ -20,7 +20,7 @@ type LanguageModel { lex: LexRules grammar: ParseGrammar language_identity: Symbol - canonical_symbols: Set + canonical_symbols: PointwisePower core: ModelCore } @@ -31,8 +31,8 @@ fn language_model_named_edge(name: Symbol, target: Node) -> Edge { } } -fn language_model_empty_canonical_symbols() -> Set { - Set { +fn language_model_empty_canonical_symbols() -> PointwisePower { + PointwisePower { member: fn(_) { false } @@ -49,7 +49,7 @@ fn void_language_model(identity: Symbol) -> LanguageModel { } } -fn language_model_canonical_symbols_to_node(symbols: Set) -> Node { +fn language_model_canonical_symbols_to_node(symbols: PointwisePower) -> Node { grammar_empty_node() } diff --git a/src/v2/test/claim/grammar/validate_grammar_test.dag b/src/v2/test/claim/grammar/validate_grammar_test.dag index c93bbccdef6..fca88e197b1 100644 --- a/src/v2/test/claim/grammar/validate_grammar_test.dag +++ b/src/v2/test/claim/grammar/validate_grammar_test.dag @@ -12,8 +12,8 @@ fn validate_grammar_fixture_well_formed() -> FormalGrammar { let start = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_start) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: Set { member: fn(n) { n == start } }, - terminals: Set { member: fn(t) { t == terminal } }, + nonterminals: PointwisePower { member: fn(n) { n == start } }, + terminals: PointwisePower { member: fn(t) { t == terminal } }, productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_start, @@ -30,8 +30,8 @@ fn validate_grammar_fixture_start_not_in_nonterminals() -> FormalGrammar { let other_nt = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_other_nt) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: Set { member: fn(n) { n == other_nt } }, - terminals: Set { member: fn(t) { t == terminal } }, + nonterminals: PointwisePower { member: fn(n) { n == other_nt } }, + terminals: PointwisePower { member: fn(t) { t == terminal } }, productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_other_nt, @@ -47,8 +47,8 @@ fn validate_grammar_fixture_lhs_not_in_nonterminals() -> FormalGrammar { let start = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_start) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: Set { member: fn(n) { n == start } }, - terminals: Set { member: fn(t) { t == terminal } }, + nonterminals: PointwisePower { member: fn(n) { n == start } }, + terminals: PointwisePower { member: fn(t) { t == terminal } }, productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_bad_lhs, @@ -64,8 +64,8 @@ fn validate_grammar_fixture_rhs_symbol_not_in_alphabet() -> FormalGrammar { let start = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_start) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: Set { member: fn(n) { n == start } }, - terminals: Set { member: fn(t) { t == terminal } }, + nonterminals: PointwisePower { member: fn(n) { n == start } }, + terminals: PointwisePower { member: fn(t) { t == terminal } }, productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_start, diff --git a/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag b/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag index 2337ed54e06..aae5ef9177d 100644 --- a/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag +++ b/src/v2/test/claim/manual/dissolution_subsumption_reverification.dag @@ -25,7 +25,7 @@ import v2.lens.subsumption { import v2.std.cardinality { RankingDimension, TerminationProof } import v2.std.collection { Map, - Set + PointwisePower } import v2.std.optional { Optional, @@ -100,8 +100,8 @@ type MechanicalReverificationRun { test_claim: TestClaimId applied_root_fix: DiffId execution: MechanicalReverificationExecution - findings_before: Set - findings_after: Set + findings_before: PointwisePower + findings_after: PointwisePower } type MechanicalReverificationError @@ -216,7 +216,7 @@ fn mechanical_reverification_execution_for_run(run: TestClaimRun, observed: Set) -> OptionalDiffId { +fn missing_subsumed_fix_before(expected: PointwisePower, observed: PointwisePower) -> OptionalDiffId { let template = DiffId { id: ^emit_rust_template_leaf_fix } let name_dispatch = DiffId { id: ^emit_rust_name_dispatch_leaf_fix } if expected.member(template) && !observed.member(template) { @@ -228,7 +228,7 @@ fn missing_subsumed_fix_before(expected: Set, observed: Set) -> } } -fn surviving_subsumed_fix_after(observed: Set) -> OptionalDiffId { +fn surviving_subsumed_fix_after(observed: PointwisePower) -> OptionalDiffId { let template = DiffId { id: ^emit_rust_template_leaf_fix } let name_dispatch = DiffId { id: ^emit_rust_name_dispatch_leaf_fix } if observed.member(template) { @@ -443,8 +443,8 @@ data run_rust_language_model_emit_mechanical_reverification_claim: TestClaimRun< subject: subject_rust_language_model_emit_mechanical_reverification_claim ) -fn rust_language_model_emit_observed_before_value() -> Set { - Set { +fn rust_language_model_emit_observed_before_value() -> PointwisePower { + PointwisePower { member: fn(d) { d.id == ^emit_rust_template_leaf_fix || d.id == ^emit_rust_name_dispatch_leaf_fix @@ -452,17 +452,17 @@ fn rust_language_model_emit_observed_before_value() -> Set { } } -data rust_language_model_emit_observed_before: Set = rust_language_model_emit_observed_before_value() +data rust_language_model_emit_observed_before: PointwisePower = rust_language_model_emit_observed_before_value() -fn rust_language_model_emit_observed_after_value() -> Set { - Set { +fn rust_language_model_emit_observed_after_value() -> PointwisePower { + PointwisePower { member: fn(_) { false } } } -data rust_language_model_emit_observed_after: Set = rust_language_model_emit_observed_after_value() +data rust_language_model_emit_observed_after: PointwisePower = rust_language_model_emit_observed_after_value() data rust_language_model_emit_lens_ci_report: MechanicalReverificationRun = MechanicalReverificationRun { test_claim: TestClaimId { id: ^rust_language_model_emit_mechanical_reverification_claim }, diff --git a/src/v2/test/claim/parse/parse_table_claims_test.dag b/src/v2/test/claim/parse/parse_table_claims_test.dag index 003184cda7f..353540a2eaa 100644 --- a/src/v2/test/claim/parse/parse_table_claims_test.dag +++ b/src/v2/test/claim/parse/parse_table_claims_test.dag @@ -20,8 +20,8 @@ test fn parse_table_token_position_indices_no_extra_append_holds() -> Bool { && ((length(xs: token_position_indices(tokens: parse_table_two_tokens)) == 4) == false) } -fn nullable_set_singleton(name: Symbol) -> Set { - Set { member: fn(sym) { sym == name } } +fn nullable_set_singleton(name: Symbol) -> PointwisePower { + PointwisePower { member: fn(sym) { sym == name } } } test fn parse_table_nullable_morphism_holds() -> Bool { From ad41d9adaa702462355e4b41a75e1433a6ec51e4 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 23:09:00 +0000 Subject: [PATCH 2/4] Addendum: full read of the Map delegate population refutes the sampled if-chain classification decomposition_scope.md flagged its 97-delegate row as the one number a full read could move. It moves: 78 of 87 resolved delegate bodies never compare the key, within two levels -- they are total functions of the key, not tables. Only 6 branch on the key directly and 3 one level down; the sample that produced the if-chain reading landed on program_facts_lookup, one of the 6. Consequence for the Map lane: most of the population wants the same move this PR made on the Set side (name PartialFunction under its own authority), not 145 re-authorings into finite maps. Stated as a lower bound on openness, with the convergence evidence and the 5 unresolved names declared rather than absorbed. Co-Authored-By: Claude Opus 5 (1M context) --- .../set_carrier_decomposition_2026-08-23.md | 35 +++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/docs/probes/set_carrier_decomposition_2026-08-23.md b/docs/probes/set_carrier_decomposition_2026-08-23.md index 7ce5b1949d9..081bb1d1761 100644 --- a/docs/probes/set_carrier_decomposition_2026-08-23.md +++ b/docs/probes/set_carrier_decomposition_2026-08-23.md @@ -82,3 +82,38 @@ does not yet make the Set side's invalid state unwritable. src/v2/compiler/03_ingest.dag`) rather than against a re-run of `curated_cargo_probe_one.sh`. The claim "18 of 27 close" is derived from the site-to-literal correspondence above, and is a prediction about the next board, not a measurement of one. + +## Addendum — the Map lane is not the shape the scoping doc predicted (full read, 2026-08-23) + +`decomposition_scope.md` classified the 97 `lookup: ` delegates from a **sample** and +flagged that row as "the one number here that a full read could move." It moves. Read +mechanically over every delegate body in `src/v2` + `dag`: + +| classification | count | test | +|---|---:|---| +| finite — branches on the key | **6** | the delegate body contains ` ==` or `match ` | +| finite one level down | **3** | a callee receiving the key does | +| **open — no key comparison anywhere in two levels** | **78** | computes a fact from the key unconditionally | + +92 delegate names, 87 bodies resolved. The sample that produced the "if-chain over a fixed key list" +reading landed on `v2.program` `program_facts_lookup`, which is one of the 6. + +The overwhelming majority are shaped like + +``` +fn bind_facts_lookup(key: Node) -> Optional { + optional_present(value: claim_inferred_facts_from_nodes(resolved: key, ..)) +} +``` + +— a **total function of the key**, not a table. So most of the Map population is a genuine partial +function that should name `PartialFunction` under its own authority, exactly the move this change +made on the Set side, rather than 145 re-authorings into finite maps. That makes the Map lane far +cheaper than scoped and brings the joint alias retarget closer. + +**What this does and does not establish.** The classifier is a text predicate over the body and one +level of callees, so it is a *lower bound on openness*: a delegate could still be finite through a +deeper helper. The 9 finite ones are confirmed by reading them; the 78 are "no key comparison found +within two levels", and the classification converged rather than drifted (going from one level to +two moved 3 of 81), which is evidence it is near-stable but not a proof. The remaining 5 unresolved +names are declared here rather than absorbed into either column. From a2b1027c87f60d6babab89a36a61679f086c11d3 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 23:14:29 +0000 Subject: [PATCH 3/4] Correct the addendum: the Map lane is a decomposition, not the symmetric retype The addendum as first written said the 78 open delegates should name PartialFunction "exactly the move this change made on the Set side". That is wrong, and it is the premise a reader would plan the Map lane against, so it is corrected in place rather than left standing. PointwisePower is ONE template row, which is why an open characteristic function inhabits it completely. PartialFunction is THIRTEEN -- it bundles a partial function with a finite map, and an open delegate cannot answer map_keys, map_values or count at all. Measured: 0 of the 145 Map{..} literals in the corpus supply any field beyond lookup, so the other twelve rows are promises the whole existing population already fails to keep. The missing carrier is on the Map side, and it already has a peer: v2.std.collection TotalMap { lookup: fn(K) -> V }. The partial peer is lookup: fn(K) -> V?, so this is the totality axis on an existing pair rather than a minted name. Raised by smart-ram-730 against the first revision; verified here from the profile rosters and the literal population rather than accepted. Co-Authored-By: Claude Opus 5 (1M context) --- .../set_carrier_decomposition_2026-08-23.md | 30 +++++++++++++++++-- 1 file changed, 27 insertions(+), 3 deletions(-) diff --git a/docs/probes/set_carrier_decomposition_2026-08-23.md b/docs/probes/set_carrier_decomposition_2026-08-23.md index 081bb1d1761..2ee3c434346 100644 --- a/docs/probes/set_carrier_decomposition_2026-08-23.md +++ b/docs/probes/set_carrier_decomposition_2026-08-23.md @@ -107,9 +107,33 @@ fn bind_facts_lookup(key: Node) -> Optional { ``` — a **total function of the key**, not a table. So most of the Map population is a genuine partial -function that should name `PartialFunction` under its own authority, exactly the move this change -made on the Set side, rather than 145 re-authorings into finite maps. That makes the Map lane far -cheaper than scoped and brings the joint alias retarget closer. +function rather than a finite table, and 145 re-authorings into finite maps is the wrong lane. + +**But it is NOT the symmetric move, and an earlier revision of this addendum said it was.** That +revision read "they should name `PartialFunction` under its own authority, exactly the move this +change made on the Set side." Corrected here rather than left standing, because it is the premise a +reader would plan the Map lane against. `PointwisePower` is **one** template row (`member`), which is +why an open characteristic function inhabits it completely and the Set change is clean. +`PartialFunction` is **thirteen** (`get map_get lookup map_insert map_merge map_has map_contains_key +map_keys map_values with contains length count`) — it bundles a partial function with a finite map, +and an open delegate cannot answer `map_keys`, `map_values` or `count` at all. + +The asymmetry is visible in the model's own profile rosters, and it is the Map side that is missing a +carrier, not the Set side that has a spare: + +| concept | Set side | Map side | +|---|---|---| +| open / characteristic | `PointwisePower` — 1 template | **missing** | +| finite / enumerable | `BooleanAlgebra` collection — 13 templates | `PartialFunction` — 13 templates | + +Inhabitance measured, not argued: **0 of the 145** `Map { … }` literals in `src/v2` + `dag` supply any +field beyond `lookup`. The other twelve rows are promises the entire existing population already +fails to keep. So the Map lane's first move is a **decomposition** of `PartialFunction` — the partial +function keeps its real meaning (`lookup: fn(K) -> V?`, mirroring the single-slot +`v2.std.collection` `TotalMap { lookup: fn(K) -> V }` already in tree, so this is the totality +axis on an existing pair rather than a minted name) and the finite map takes its own name — not a +retype. That is a `std` authority change of the same class as the alias row deferred above, so it +moves in its own PR verified by whole-corpus compile, and **both** alias retargets can ride it. **What this does and does not establish.** The classifier is a text predicate over the body and one level of callees, so it is a *lower bound on openness*: a delegate could still be finite through a From f73f998a5165e8aeb728014102d19ea553756412 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sun, 23 Aug 2026 23:21:54 +0000 Subject: [PATCH 4/4] Put the grammar fixture's PointwisePower reference where the import derivation can see it quiet-pike-368 declared a residue in their use-line derivation: the producer walks SIGNATURE-level type positions (type_annotation, params, inferred return), so a name that reaches emitted text only through a value-position body construction is never proposed as a use-line. Checked my own 20 re-typed files against that boundary rather than assuming they clear it: 19 carry the name in a signature position, and exactly one did not -- v2.test.claim.grammar.validate_grammar had 8 PointwisePower literals and 0 signature positions. This is not a class my change introduced (the file's previous `Set` reference was literal-only in the same way, and neither name is on the 7-name hardcoded roster in emit_faithful_text_carrier_import_lines), and the file is not in the 03_ingest closure, so no board site is involved. Fixed anyway because it is cheap and it removes the one site of mine that falls in a declared gap. The two singleton predicates every fixture built inline are now named helpers with declared return types -- 8 literals become 2, and the reference moves into a position the derivation walks. Better modeling independent of the emitter: the same value was being constructed four times. Measured: gunbc compile on BOTH this entry and src/v2/compiler/03_ingest.dag reports 52 hard diagnostics each, zero of which name PointwisePower, PartialFunction, `Set<` or a missing `member` field. 52 is the unchanged pre-existing source-annotation count in dag/test/manual/command_runner_local_argv_receipt_test.dag. Co-Authored-By: Claude Opus 5 (1M context) --- .../claim/grammar/validate_grammar_test.dag | 30 ++++++++++++++----- 1 file changed, 22 insertions(+), 8 deletions(-) diff --git a/src/v2/test/claim/grammar/validate_grammar_test.dag b/src/v2/test/claim/grammar/validate_grammar_test.dag index fca88e197b1..31023863f59 100644 --- a/src/v2/test/claim/grammar/validate_grammar_test.dag +++ b/src/v2/test/claim/grammar/validate_grammar_test.dag @@ -8,12 +8,26 @@ data validate_grammar_fixture_other_nt: Symbol = ^validate_grammar_fixture_other data validate_grammar_fixture_bad_lhs: Symbol = ^validate_grammar_fixture_bad_lhs data validate_grammar_fixture_orphan_terminal: Symbol = ^validate_grammar_fixture_orphan_terminal +// The two singleton predicates every fixture below builds. Extracted for a reason beyond +// de-duplication: before this, `PointwisePower` reached this module's emitted text ONLY through a +// value-position record literal, and the import derivation in `v1.compiler.emit_rust` +// `reference_derived_use_lines` walks SIGNATURE-level type positions -- a name spelled only inside +// a body construction is never proposed as a use-line. A declared return type puts the reference +// where the derivation can see it. +fn validate_grammar_fixture_nonterminal_singleton(only: FormalNonterminal) -> PointwisePower { + PointwisePower { member: fn(n) { n == only } } +} + +fn validate_grammar_fixture_terminal_singleton(only: FormalTerminal) -> PointwisePower { + PointwisePower { member: fn(t) { t == only } } +} + fn validate_grammar_fixture_well_formed() -> FormalGrammar { let start = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_start) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: PointwisePower { member: fn(n) { n == start } }, - terminals: PointwisePower { member: fn(t) { t == terminal } }, + nonterminals: validate_grammar_fixture_nonterminal_singleton(only: start), + terminals: validate_grammar_fixture_terminal_singleton(only: terminal), productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_start, @@ -30,8 +44,8 @@ fn validate_grammar_fixture_start_not_in_nonterminals() -> FormalGrammar { let other_nt = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_other_nt) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: PointwisePower { member: fn(n) { n == other_nt } }, - terminals: PointwisePower { member: fn(t) { t == terminal } }, + nonterminals: validate_grammar_fixture_nonterminal_singleton(only: other_nt), + terminals: validate_grammar_fixture_terminal_singleton(only: terminal), productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_other_nt, @@ -47,8 +61,8 @@ fn validate_grammar_fixture_lhs_not_in_nonterminals() -> FormalGrammar { let start = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_start) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: PointwisePower { member: fn(n) { n == start } }, - terminals: PointwisePower { member: fn(t) { t == terminal } }, + nonterminals: validate_grammar_fixture_nonterminal_singleton(only: start), + terminals: validate_grammar_fixture_terminal_singleton(only: terminal), productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_bad_lhs, @@ -64,8 +78,8 @@ fn validate_grammar_fixture_rhs_symbol_not_in_alphabet() -> FormalGrammar { let start = grammar_formal_nonterminal(identity: ^validate_grammar_fixture_start) let terminal = FormalTerminal { identity: ^validate_grammar_fixture_terminal_a } FormalGrammar { - nonterminals: PointwisePower { member: fn(n) { n == start } }, - terminals: PointwisePower { member: fn(t) { t == terminal } }, + nonterminals: validate_grammar_fixture_nonterminal_singleton(only: start), + terminals: validate_grammar_fixture_terminal_singleton(only: terminal), productions: Cons { head: grammar_formal_production( lhs: ^validate_grammar_fixture_start,