MQ PR2: map literals elaborate from the declared Map type (map arm of the one elaboration writer)

dag/gunbc/explicit_witness_admission.dag

@@ -193,6 +193,62 @@ fn known_red_pre_verdict_probe(
 data known_red_class_note: String = "WHAT A KNOWN-RED ADMISSION IS: a witness red on main for a feature gap owned by a named lane. It is a RED CONTROL for that lane, not a broken test — deleting it would discard the discriminating input, while leaving it in per-PR discovery would red every wide PR on a debt that PR did not create. Greening is the counted un-quarantine event of std.witness_admission: the row deletes in the SAME change that lands the fix, which promotes the unchanged witness to ordinary DiscoverySelection as a permanent regression control (DESIGN 4b(4) — the climb deletes the quarantine machinery, never the evidence). A DISSOLVE_ON MUST NAME A FACT THAT IS FALSE TODAY AND BECOMES TRUE EXACTLY WHEN THE FIX LANDS, and this requirement is here because two rows failed it in one night. A trigger keyed on a condition already satisfied is not a trigger, it is a deletion licence with a date on it: whoever next reads it dissolves a quarantine standing in for a defect that is still live, and the row reads as dissolved-per-its-own-terms while the wall it substituted for does not exist. RECEIPT 1, another lane's: the #8592 row's trigger read 'the mirrors are regenerated so the compiled harness CONTAINS declared_arg_types_for_method' — that symbol has been present in v1_compiler_infer_lookup.rs all along, so the trigger was satisfiable from the moment it was written, while the defect it quarantines is live (on main the function still takes no TypeEnv, which is precisely the bug). RECEIPT 2, MY OWN, AND IT IS THE MORE INSTRUCTIVE ONE BECAUSE THE DELETION WAS STILL CORRECT: the min-length row's trigger read 'the compiled harness contains the wall'. Measured, where_refinement_predicates_covered has 2 occurrences in that mirror on main and always did, so a reader checking 'the wall' would have dissolved the row at any point in the preceding weeks. It dissolved correctly only because the author happened to grep where_predicate_guaranteed_min_length, which was 0 on main and 2 after the regen. THE TRIGGER DID NOT ENCODE WHICH FACT DECIDED IT; the right answer came from the reader, not the row. So: name the symbol, signature or behaviour whose ABSENCE is the gap — a new parameter, a specific new function, a named repro passing — never a category word like 'the wall' or 'the fix', and never a symbol that predates the change. The test a reviewer applies: run the trigger's check against main TODAY, and if it passes, the trigger is defective and the row is unprotected. The roster must not grow silently: a new admission carries a reason naming the diagnosis and owner plus a dissolve_on, both refused empty by NonEmptyStr, and a row whose witness runs green locally is stale and deletes. Local recipe per row: claim_batch --source-root dag --source-root src/v2 --entry <entry> --functions <function> -- AND FOR AN ExecutionWitnessKind ROW, --wet AS WELL, WITHOUT WHICH THE RECIPE CANNOT DO WHAT THE ROW ASKS OF IT. claim_batch is hermetic by default, so a wet row invoked by the recipe as written above never reaches its subject: measured 2026-08-26 on self_host_logic_behavioral_receipt_holds, it returns FAIL in 87 seconds with 'hermetic route has no arm for Dir: the claim never reached its subject, so this is a route gap and not a verdict', naming three undeclared dispatches (Filesystem.Read, git.Inspect.Toplevel, shell.Mktemp.Dir). The refusal is well-modeled and says plainly that it is not a verdict; the defect was in the recipe, which every wet dissolution condition below cites as the way its row greens. A row whose only recorded closing move cannot close it is the shape DESIGN records for a gate whose sole green is the forbidden action -- here arrived at from the other side, with no green reachable at all. CorpusWitnessKind rows run on the hermetic falsifier probe batch; ExecutionWitnessKind rows run on the falsifier wet quarantine batch."
 
 data explicit_witness_admissions: List<ExplicitWitnessAdmission> = [
+  known_red_probe(
+    entry: "src/v2/test/claim/body_lowering/map_literal_test.dag",
+    f: "ml_headless_literal_equals_the_headed_introduction_holds",
+    kind: CorpusWitnessKind,
+    budget: FastLaneEvalBudget,
+    reason: "map arm control under Map<String, V> (the headless map literal elaborates to exactly the headed introduction), RED because an unimported String does not bind on the v2 route (resolve_reason_unbound_symbol before the map arm runs; owner neat-ibex-696, gunbc#12760), and once it does, a string key still carries no text to compare (resolve_anonymous_map_key_text_unavailable; owner sleek-owl-120, gunbc#12759). On this branch only the arm's REFUSAL paths execute (key kind, name key, no expectation, mixed keys); no acceptance path executes here. The acceptance paths were measured GREEN on a throwaway merge of this branch with gunbc#12760's head, which is the evidence this row stands on.",
+    dissolution: unbound_dissolution(description: "BOTH hold: String bound by v2.extdeps.languages.dag dag_kernel_type_binding_optional with an infer text-literal arm (gunbc#12760), AND a string literal lowers to a lexeme-stamped terminal carrying its text rather than the one payload-less dag_token_string_literal atom (gunbc#12759). Measured against #12760 alone, the duplicate and escaped-key rows went green only through that collapse. The row deletes in the change that makes both true, promoting the witness to ordinary DiscoverySelection")
+  ),
+  known_red_probe(
+    entry: "src/v2/test/claim/body_lowering/map_literal_test.dag",
+    f: "ml_a_duplicate_key_refuses_holds",
+    kind: CorpusWitnessKind,
+    budget: FastLaneEvalBudget,
+    reason: "map arm control under Map<String, V> (a repeated key refuses resolve_anonymous_map_duplicate_key at its second occurrence), RED because an unimported String does not bind on the v2 route (resolve_reason_unbound_symbol before the map arm runs; owner neat-ibex-696, gunbc#12760), and once it does, a string key still carries no text to compare (resolve_anonymous_map_key_text_unavailable; owner sleek-owl-120, gunbc#12759). On this branch only the arm's REFUSAL paths execute (key kind, name key, no expectation, mixed keys); no acceptance path executes here. The acceptance paths were measured GREEN on a throwaway merge of this branch with gunbc#12760's head, which is the evidence this row stands on.",
+    dissolution: unbound_dissolution(description: "BOTH hold: String bound by v2.extdeps.languages.dag dag_kernel_type_binding_optional with an infer text-literal arm (gunbc#12760), AND a string literal lowers to a lexeme-stamped terminal carrying its text rather than the one payload-less dag_token_string_literal atom (gunbc#12759). Measured against #12760 alone, the duplicate and escaped-key rows went green only through that collapse. The row deletes in the change that makes both true, promoting the witness to ordinary DiscoverySelection")
+  ),
+  known_red_probe(
+    entry: "src/v2/test/claim/body_lowering/map_literal_test.dag",
+    f: "ml_an_escaped_and_a_raw_key_are_one_key_holds",
+    kind: CorpusWitnessKind,
+    budget: FastLaneEvalBudget,
+    reason: "map arm control under Map<String, V> (an escaped key and its raw scalar collide under the decoded-text key law), RED because an unimported String does not bind on the v2 route (resolve_reason_unbound_symbol before the map arm runs; owner neat-ibex-696, gunbc#12760), and once it does, a string key still carries no text to compare (resolve_anonymous_map_key_text_unavailable; owner sleek-owl-120, gunbc#12759). On this branch only the arm's REFUSAL paths execute (key kind, name key, no expectation, mixed keys); no acceptance path executes here. The acceptance paths were measured GREEN on a throwaway merge of this branch with gunbc#12760's head, which is the evidence this row stands on.",
+    dissolution: unbound_dissolution(description: "BOTH hold: String bound by v2.extdeps.languages.dag dag_kernel_type_binding_optional with an infer text-literal arm (gunbc#12760), AND a string literal lowers to a lexeme-stamped terminal carrying its text rather than the one payload-less dag_token_string_literal atom (gunbc#12759). Measured against #12760 alone, the duplicate and escaped-key rows went green only through that collapse. The row deletes in the change that makes both true, promoting the witness to ordinary DiscoverySelection")
+  ),
+  known_red_probe(
+    entry: "src/v2/test/claim/body_lowering/map_literal_test.dag",
+    f: "ml_distinct_keys_are_accepted_holds",
+    kind: CorpusWitnessKind,
+    budget: FastLaneEvalBudget,
+    reason: "map arm control under Map<String, V> (distinct keys elaborate), RED because an unimported String does not bind on the v2 route (resolve_reason_unbound_symbol before the map arm runs; owner neat-ibex-696, gunbc#12760), and once it does, a string key still carries no text to compare (resolve_anonymous_map_key_text_unavailable; owner sleek-owl-120, gunbc#12759). On this branch only the arm's REFUSAL paths execute (key kind, name key, no expectation, mixed keys); no acceptance path executes here. The acceptance paths were measured GREEN on a throwaway merge of this branch with gunbc#12760's head, which is the evidence this row stands on.",
+    dissolution: unbound_dissolution(description: "BOTH hold: String bound by v2.extdeps.languages.dag dag_kernel_type_binding_optional with an infer text-literal arm (gunbc#12760), AND a string literal lowers to a lexeme-stamped terminal carrying its text rather than the one payload-less dag_token_string_literal atom (gunbc#12759). Measured against #12760 alone, the duplicate and escaped-key rows went green only through that collapse. The row deletes in the change that makes both true, promoting the witness to ordinary DiscoverySelection")
+  ),
+  known_red_probe(
+    entry: "src/v2/test/claim/body_lowering/map_literal_test.dag",
+    f: "ml_infer_refuses_an_elaborated_value_mismatch_holds",
+    kind: CorpusWitnessKind,
+    budget: FastLaneEvalBudget,
+    reason: "map arm control under Map<String, V> (infer refuses an elaborated map whose value does not inhabit V), RED because an unimported String does not bind on the v2 route (resolve_reason_unbound_symbol before the map arm runs; owner neat-ibex-696, gunbc#12760), and once it does, a string key still carries no text to compare (resolve_anonymous_map_key_text_unavailable; owner sleek-owl-120, gunbc#12759). On this branch only the arm's REFUSAL paths execute (key kind, name key, no expectation, mixed keys); no acceptance path executes here. The acceptance paths were measured GREEN on a throwaway merge of this branch with gunbc#12760's head, which is the evidence this row stands on.",
+    dissolution: unbound_dissolution(description: "BOTH hold: String bound by v2.extdeps.languages.dag dag_kernel_type_binding_optional with an infer text-literal arm (gunbc#12760), AND a string literal lowers to a lexeme-stamped terminal carrying its text rather than the one payload-less dag_token_string_literal atom (gunbc#12759). Measured against #12760 alone, the duplicate and escaped-key rows went green only through that collapse. The row deletes in the change that makes both true, promoting the witness to ordinary DiscoverySelection")
+  ),
+  known_red_probe(
+    entry: "src/v2/test/claim/body_lowering/map_literal_test.dag",
+    f: "ml_an_elaborated_map_infers_holds",
+    kind: CorpusWitnessKind,
+    budget: FastLaneEvalBudget,
+    reason: "map arm control: a well-typed elaborated map infers. RED beyond the map arm: measured with gunbc#12760 merged, infer refuses infer_grounding_not_derived located (NodeLocus) at the MapIntroductionEntry { .. } construct, identically for the HEADED spelling and under Map<String, Int>. The discriminating specimen ml_a_same_module_generic_entry_construct_infers_holds (generic record declared in the same module) refuses the same way, so this is neither cross-module declaration reading (#12726 PR2) nor the v2 Bool fork. Owner: smart-newt-725 (record construct typing, #12763 lineage), per quiet-gull-780.",
+    dissolution: unbound_dissolution(description: "infer grounds a construct of a generic record whose type arguments come only from its expected type (callee parameter or list element): this witness greens and the row deletes in that change")
+  ),
+  known_red_probe(
+    entry: "src/v2/test/claim/body_lowering/map_literal_test.dag",
+    f: "ml_a_same_module_generic_entry_construct_infers_holds",
+    kind: CorpusWitnessKind,
+    budget: FastLaneEvalBudget,
+    reason: "the discriminating specimen for ml_an_elaborated_map_infers_holds: LocalEntry<K, V> and local_from_entries declared beside the data decl, so no cross-module declaration is read; infer refuses infer_grounding_not_derived at the LocalEntry { .. } construct (measured with gunbc#12760 merged; without it, unbound String refuses first). Owner: smart-newt-725.",
+    dissolution: unbound_dissolution(description: "infer grounds a construct of a generic record whose type arguments come only from its expected type (callee parameter or list element): this witness greens and the row deletes in that change")
+  ),
   known_red_probe(
     entry: "dag/test/claim/declared_type_inhabitance_direct_call_witness_test.dag",
     f: "w_a_branded_product_refinement_at_an_unrelated_product_formal_still_refuses",

dag/gunbc/recurring_failure_mode/expression_enclosing_a_block_headed_operand_lowers_to_that_block_at_v2_body_lowering.dag

@@ -14,6 +14,7 @@ data expression_enclosing_a_block_headed_operand_lowers_to_that_block_at_v2_body
     "DISTINGUISHING FACTS. Not `lowering_accessor_collapses_a_sequence_operand`, which keeps the LEFT element of an operand; here the block is kept and the enclosing expression is lost. Not gunbc#11911, a parse-order defect; here the parse accepts. Not `match_arms_after_the_second_are_dropped_at_v2_body_lowering`, which loses arms INSIDE a match; this loses what is AROUND it.",
     "RUNG FOUND AT: below the floor (silent wrongness). CEILING: structurally guaranteed. An expression lowers to its own operator, construct or application over every constituent, or refuses at the constituent it could not read. A control form is lowered as the whole value only where it IS the value. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: v2 body lowering has no reader that answers a value by searching its subtree for a control form, so an enclosing expression the fold left unlowered refuses instead of being replaced. Owner: bright-boar-848's fold queue (quiet-seal-543, 2026-09-25). The fall-back reader is that lane's subject. Pinned drops, each holding while the drop happens and redding when the repair lands, in `v2.test.claim.namespace_xl0.reference_conservation_accepted_drops`: `a_binary_operand_beside_a_match_is_reported_dropped_holds`, `a_binary_operand_beside_an_if_is_reported_dropped_holds`, `a_record_field_beside_a_match_valued_field_is_reported_dropped_holds`, `a_call_argument_beside_a_match_valued_argument_is_reported_dropped_holds`. The census's clean control, `v2.test.claim.namespace_xl0.reference_conservation` `the_clean_control_conserves_every_authored_atom_holds`, is the neighbour that conserves.",
     "CLIMBED, THE TRIGGER CAPABILITY MET (bright-boar-848, XL-2). Two links, both in `v2.compiler.body_lowering_fold`. (1) `body_lower_find_control_form_optional` no longer searches a value's subtree: it descends only through what does not change the expression -- a production to its captured child, a sequence whose right side is an empty tail, a lone opening or closing delimiter -- so a control form is lowered as the whole value only where it IS the value, and an enclosing operator, call or record goes whole to the binary/postfix route. (2) That route then exposed the second link: `body_lower_primary_expr` ran its raw-syntax strategy readers over a capture the bottom-up fold had ALREADY lowered (a Match or Branch) and one answered it with its first child, so `t && match w {..}` became `t && w`. Measured by calling `body_lower_value_read` at each production level of the operand: correct at the match_expr node, collapsed from its primary parent up. A primary whose capture is core substrate is now that node, the rule `body_lower_postfix_lowered_primary_optional` already states one level up. The four pinned drops flip to conservation controls (accepted AND the enclosing constituent not dropped), red against the base fold and green after. The label and let-binder atoms that stay absent in the same fixtures are the separately declared NamedArgumentLabel and StatementLetBinder drops. RUNG NOW: structurally guaranteed for the enclosing expression.",
+    "THE LEFT-OPERAND HALF IS STILL OPEN, and it is valid dag the corpus writes: a block-headed expression as the LEFT operand of a binary operator (`match w {..} && t`, `match w {..} || t`) at expression start. Measured occurrence count 179 (a scan of dag/ and src/v2 for a statement-initial `match .. {` whose closing brace is followed by a `&&`/`||` line); all sit under dag/test, which the native route does not admit into its population, so the native census shows none of them. The seed parser accepts the form and v2 refuses it, so the two parsers disagree on the same source. LOCATED SPECIMEN (gunbc#12758): v2.test.claim.body_lowering.map_literal `ml_the_key_law_names_both_occurrences_holds` is `match map_introduction_duplicate_key(..) { .. } && match .. { .. }`; claim_batch (seed) runs it PASS, and the v2 native route file-refuses src/v2/test/claim/body_lowering/map_literal_test.dag with parse_g0_tokens_remain (WholeFile). Bisected by feeding each top-level declaration to the v2 parser alone: only that declaration refuses. The specimen keeps its spelling as the witness; it is not rewritten around the gap. NEXT-RUNG TRIGGER: the v2 grammar admits a block-headed primary as the left operand of a binary operator, and this specimen's file clears parse on the native route.",
   ],
 
   evidence: [

dag/std/algebra.dag

@@ -237,6 +237,30 @@ type FinitelySupportedFunction<K, V> {
   size: fn() -> Int
 }
 
+// THE MAP-LITERAL INTRODUCTION: the declaration a map literal `{ "k": v, .. }` elaborates to, as
+// `FreeMonoid` is the one a list literal elaborates to (v2.std.map_introduction carries its head
+// path and constructor; docs/plans/map-literal-introduction-design.md). It is NOT a second
+// constructor of the carrier: it is the carrier's own insert (the `map_insert` row of
+// `finitely_supported_function_templates`) folded over its own empty (the `empty_map` row), in
+// authored order. It lives HERE, below `std.types`, because `std.types`' own map literals elaborate
+// to it; a home that imports `std.types` (v2.std.collection) would close an import cycle.
+//
+// The fold's last-write-wins is unobservable on every accepted program: the one writer that builds
+// this call (v2.compiler.resolve, the map arm) refuses a repeated key BEFORE it builds it
+// (v2.std.map_introduction map_introduction_duplicate_key). A caller that bypasses that writer and
+// calls this directly with a repeated key gets insert's semantics, which is what it asked for.
+// The result is spelled `Map<K, V>`, the kernel container spelling this module already uses bare
+// (kernel_algebra_profile_value), because the seed types `empty_map()` only under a keyed-collection
+// expectation; it names this carrier (std.types Map = FinitelySupportedFunction).
+type MapIntroductionEntry<K, V> {
+  key: K
+  value: V
+}
+
+fn map_from_entries<K, V>(entries: FreeMonoid<MapIntroductionEntry<K, V>>) -> Map<K, V> {
+  entries |> fold(init: empty_map(), f: (acc, entry) => map_insert(acc, entry.key, entry.value))
+}
+
 // MOVED HERE from `v2.std.collection` by the change that split `PartialFunction`. They are the
 // total corner of the family above, and leaving them in a different module from their own axis is
 // where a fork starts. `TotalPolicy` travels with `TotalMap` rather than staying behind: it is the