Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -1,16 +1,20 @@
module gunbc.recurring_failure_mode.a_quoted_key_record_literal_refusal_left_body_lowering_unrostered

import std.types { NonEmptyStr }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data a_quoted_key_record_literal_refusal_left_body_lowering_unrostered: RecurringFailureMode = RecurringFailureMode {
identity: "a_quoted_key_record_literal_refusal_left_body_lowering_unrostered" as NonEmptyStr,

receipts: [
"**A headless brace with a quoted key, under a non-map annotation, is no longer refused at body lowering** (`data ar_k: Bool = { \"n\": true }`). `v2.test.claim.body_lowering.anonymous_record` `ar_a_quoted_key_is_not_a_record_field_holds` expects `normalize` to refuse at the item with `body_lowering_reason_field_init_unlowered`, so that the quoted key is never read as field `n`. On origin/main, 2026-10-05, `normalize` ACCEPTS the subject (claim_batch on BuildBuddy, clever-raven-680; a probe claim over the same `ar_key_quoted_subject().normalized` returned Accepted). The sibling `ar_a_quoted_key_takes_the_string_key_production_holds` passes, so the parse still takes the string-key production. The claim was red on main. It is listed in `v2.workflow.floor_grandfathered_roster`, but that roster only selects an eval budget, so why the required lane did not expose the red is NOT established.",
"NOT ESTABLISHED: whether a later stage refuses the subject. The map-literal arm of resolve (`v2.compiler.resolve` `resolve_elided_construct_walk`, docs/plans/map-literal-introduction-design.md) refuses a headless brace whose expected head is not a Map, so the refusal may have moved from body lowering to resolve. In that case the claim keys a stage the compiler no longer refuses at, which is a stale expectation and not a fail-open. If no later stage refuses, the source is accepted with a quoted key standing where a record field was expected: silent wrongness, below the floor.",
"RUNG: unknown until the above is measured. NEXT TRIGGER: one run of the subject through resolve and infer that records which stage refuses and with what reason. Then the claim either asserts that refusal at that stage, or the body-lowering refusal is restored. Not repaired here.",
"**A headless brace with a quoted key, under a non-map annotation, is no longer refused at body lowering** (`data ar_k: Bool = { \"n\": true }`). MEASURED 2026-10-09 (zesty-heron-486, claim_batch on BuildBuddy at d0f2067f8b): `normalize` ACCEPTS; `ar_a_quoted_key_takes_the_string_key_production_holds` PASSES; resolve REFUSES with `resolve_anonymous_map_expected_type_not_map`. The map-literal arm (gunbc#12758, `v2.compiler.resolve` `resolve_elided_construct_walk`) is the wall: a string-keyed brace whose expected head is not Map. The former claim that keyed `body_lowering_reason_field_init_unlowered` was a stale stage, not a fail-open. The claim now asserts the resolve reason and that lowering still accepts, so a reader that treats `\"n\"` as field `n` still reds (that path refuses as a record, not as a map).",
"RUNG: mechanically preventable on the resolve path (enrolled claim). NEXT TRIGGER: none for this class's original silent-wrongness question; the quoted-key-as-field reading is refused. A later climb would make a quoted key under a non-Map annotation unwritable at lowering without restoring a second authority beside the map arm.",
],

evidence: [],
evidence: [
DeclarationRef { module_path: "v2.test.claim.body_lowering.anonymous_record", decl_name: "ar_a_quoted_key_is_not_a_record_field_holds", field: WholeDeclaration },
DeclarationRef { module_path: "v2.test.claim.body_lowering.anonymous_record", decl_name: "ar_a_quoted_key_takes_the_string_key_production_holds", field: WholeDeclaration },
DeclarationRef { module_path: "v2.compiler.resolve", decl_name: "resolve_elided_construct_walk", field: WholeDeclaration },
],
}
25 changes: 18 additions & 7 deletions src/v2/test/claim/body_lowering/anonymous_record_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -95,6 +95,10 @@ data ar_partial_source: String = "module v2.test.ar_partial\n\nimport std.types

data ar_cycle_source: String = "module v2.test.ar_cycle\n\nimport std.types { Bool }\nimport v2.test.arseq { ArCycA }\n\ndata ar_y: ArCycA = { first: true }\n"

data ar_key_bare_source: String = "module v2.test.ar_key_bare\n\ndata ar_k: Bool = { n: true }\n"

data ar_key_quoted_source: String = "module v2.test.ar_key_quoted\n\ndata ar_k: Bool = { \"n\": true }\n"

data ar_list_headed_source: String = "module v2.test.ar_list_headed\n\nimport std.types { Bool }\nimport std.algebra { FreeMonoid }\nimport v2.test.arp { ArB }\n\nfn ar_list() -> FreeMonoid<ArB> { [ArB { n: true, m: false }, ArB { n: false, m: false }] }\n"

data ar_list_headless_source: String = "module v2.test.ar_list_headless\n\nimport std.types { Bool }\nimport std.algebra { FreeMonoid }\nimport v2.test.arp { ArB }\n\nfn ar_list() -> FreeMonoid<ArB> { [{ n: true, m: false }, { n: false, m: false }] }\n"
Expand Down Expand Up @@ -126,7 +130,8 @@ data ar_ingest: SourceRootIngest = [
ar_read(source: ar_reorder_source, id: ^ar_reorder_read, unit: ^ar_reorder_cu, path: "src/v2/test/fixture/anonymous_record/reorder.dag"),
ar_read(source: ar_constant_source, id: ^ar_constant_read, unit: ^ar_constant_cu, path: "src/v2/test/fixture/anonymous_record/constant.dag"),
ar_read(source: ar_partial_source, id: ^ar_partial_read, unit: ^ar_partial_cu, path: "src/v2/test/fixture/anonymous_record/partial.dag"),
ar_read(source: ar_cycle_source, id: ^ar_cycle_read, unit: ^ar_cycle_cu, path: "src/v2/test/fixture/anonymous_record/cycle.dag")
ar_read(source: ar_cycle_source, id: ^ar_cycle_read, unit: ^ar_cycle_cu, path: "src/v2/test/fixture/anonymous_record/cycle.dag"),
ar_read(source: ar_key_quoted_source, id: ^ar_key_quoted_read, unit: ^ar_key_quoted_cu, path: "src/v2/test/fixture/anonymous_record/key_quoted.dag")
]

fn ar_fixture_normalized() -> Outcome<FreeMonoid<NormalizedTree>> {
Expand Down Expand Up @@ -162,6 +167,7 @@ fn ar_resolved_reorder() -> Outcome<ResolvedTree> { ar_resolve_subject(subject:
fn ar_resolved_constant() -> Outcome<ResolvedTree> { ar_resolve_subject(subject: "v2.test.ar_constant") }
fn ar_resolved_partial() -> Outcome<ResolvedTree> { ar_resolve_subject(subject: "v2.test.ar_partial") }
fn ar_resolved_cycle() -> Outcome<ResolvedTree> { ar_resolve_subject(subject: "v2.test.ar_cycle") }
fn ar_resolved_key_quoted() -> Outcome<ResolvedTree> { ar_resolve_subject(subject: "v2.test.ar_key_quoted") }

// Every construct under the root, authored or elided, in tree order.
fn ar_constructs(root: Node) -> List<Node> {
Expand Down Expand Up @@ -312,9 +318,6 @@ test fn ar_an_alias_cycle_refuses_holds() -> Bool {
// and a bare key with the same spelling parse through DIFFERENT productions: only the quoted one
// carries ^dag_surface_field_init_string_key. A grammar that merged the two alternatives back into
// one production -- or classified the key by its text -- makes both counts equal and reds this.
data ar_key_bare_source: String = "module v2.test.ar_key_bare\n\ndata ar_k: Bool = { n: true }\n"

data ar_key_quoted_source: String = "module v2.test.ar_key_quoted\n\ndata ar_k: Bool = { \"n\": true }\n"

// Each fixture's parse and normalize is a shared producer (enrolled warm), run once on the real route.
fn ar_key_bare_subject() -> ReferenceConservationSubject { conservation_subject(id_tail: "ar_key_bare", source: ar_key_bare_source) }
Expand All @@ -338,10 +341,18 @@ test fn ar_a_quoted_key_takes_the_string_key_production_holds() -> Bool {
&& (ar_string_key_production_count(subject: ar_key_quoted_subject()) == 1)
}

// And the record arm refuses the quoted key at the item, never reading it as field `n`.
// A quoted key is a map-literal entry, never a record field named `n`. After the map arm
// (gunbc#12758) lowering keeps the string-key production as MapLiteralEntryEdge rather than
// refusing at the item; resolve then refuses a brace whose expected head is not Map
// (`data ar_k: Bool = { "n": true }`) as resolve_anonymous_map_expected_type_not_map, which is
// the reason only a STRING-KEYED brace takes. A reader that still treated `"n"` as field `n`
// would refuse as a record (resolve_anonymous_record_expected_type_not_record) or accept a
// Bool-headed construct. Lowering of this specimen stays Accepted (the sibling production
// claim already pins the grammar); the wall is at resolve.
test fn ar_a_quoted_key_is_not_a_record_field_holds() -> Bool {
match ar_key_quoted_subject().normalized {
Accepted { value: _, diagnostics: _ } => false
Rejected { diagnostics: d } => diagnostics_fatal_reason(d: d) == ^body_lowering_reason_field_init_unlowered
Rejected { diagnostics: _ } => false
Accepted { value: _, diagnostics: _ } =>
ar_refuses_with(o: ar_resolved_key_quoted(), reason: ^resolve_anonymous_map_expected_type_not_map)
}
}
Loading