Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
4e288de
Carry authored string literals on every DataItem decl_facts projection.
Sep 11, 2026
e013c7d
Merge remote-tracking branch 'origin/main' into session/stern-heron-554
Sep 11, 2026
e5e08c4
Refuse unattachable DataItem projections and keep authored strings of…
Sep 11, 2026
a011da6
Typecheck skeleton walks: fold Edge children, join authored lexemes v…
Sep 11, 2026
1cb4ec8
Fold authored-string lexemes into the existing fold_node census.
Sep 11, 2026
be60905
Record that the census LitStr discovery hole is closed.
Sep 11, 2026
1db1667
Merge origin/main into session/stern-heron-554.
Sep 11, 2026
ef61cbc
Record the LitStr climb on the RFM and dispose the EdgeLabel skip.
Sep 11, 2026
ccd5dc8
Keep RFM found-at distinct from rung-now, and type the EdgeLabel disp…
Sep 12, 2026
00834dd
Merge origin/main into session/stern-heron-554.
Sep 12, 2026
3951f9b
Admit the two List coincidence deltas and delete consumed #11071 wave…
Sep 12, 2026
e7abcbd
Call the value-projection rows regression controls, not expected-red.
Sep 12, 2026
50fd200
Route authored-string edge skip through labeled_named_is.
Sep 12, 2026
f90ab96
Import List as authority and keep the authored-string attach crate-in…
Sep 12, 2026
3d5ab73
Merge origin/main into session/stern-heron-554.
Sep 12, 2026
ad30be9
Keep main's wave-admission table after the merge.
Sep 12, 2026
6e6d9b3
Enroll the three authored-string host items on the seed-growth roster.
Sep 12, 2026
65673f5
Delete the stale #11137 wave-admission row this head does not produce.
Sep 12, 2026
61c2a61
Merge origin/main into session/stern-heron-554.
Sep 12, 2026
2515b4e
Pay the channel-separation witness with one census fold, not two.
Sep 12, 2026
e434dbc
Point the channel-separation witness at a one-file decl_facts pool.
Sep 12, 2026
c31790f
Merge origin/main into session/stern-heron-554.
Sep 12, 2026
f8626a3
Pay the concat authored-lexeme witness with one census fold on a one-…
Sep 13, 2026
a717959
Merge origin/main into session/stern-heron-554.
Sep 13, 2026
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
57 changes: 57 additions & 0 deletions dag/gunbc/decl_facts_authored_string_attach_seed_growth.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
module gunbc.decl_facts_authored_string_attach_seed_growth

import gunbc.roadmap_model { RoadmapNodeId }
import gunbc.seed_growth { SeedGrowthJustification }
import std.decl_ref { DeclarationRef, WholeDeclaration }

// FORWARD-FREEZE RECEIPT for the three hand items added in
// v1_compiler.data_initializer_identity (gunbc#11082). Authored because
// gunbc.seed_growth_admission seed_growth_forward_freeze_policy_note makes unenumerated
// hand growth in src/v1 a stop-line, a DissolutionCondition in
// v2.std.decl_facts_skeleton is not a substitute, and pub(crate) is not an exemption.
// One SeedGrowthJustification per added item. .dag authority is the decl-facts
// projection (v2.std.data_initializer_identity marshal_data_initializer_projection
// and v2.std.decl_facts_skeleton authored-string EdgeLabel skip). Seed-retained
// module: data_initializer_identity.

data collect_authored_string_literals_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef {
module_path: "v1_compiler.data_initializer_identity",
decl_name: "collect_authored_string_literals",
field: WholeDeclaration
}
],
reason: "Walks the DataItem parse tree (not the typechecked projection) and collects every LitStr so lexeme-keyed discovery can see initializer values. WHY RUST REMAINS NECESSARY: the parse-tree ExprData/LitStr walk is a host interp fact; marshal_data_initializer_projection still does not intern those atoms into the typechecked Node. The .dag authority that will retire it is that marshal, not a second walk.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete collect_authored_string_literals when marshal_data_initializer_projection itself interns every initializer LitStr into the typechecked Node, so atom_identities_in_node / v1_consumer_discovery read inhabitance rather than a host attach.",
current_boundary: "v1_compiler.data_initializer_identity collect_authored_string_literals; called only from with_authored_string_literals. crate-internal. No public surface."
}

data authored_string_literal_edge_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef {
module_path: "v1_compiler.data_initializer_identity",
decl_name: "AUTHORED_STRING_LITERAL_EDGE",
field: WholeDeclaration
}
],
reason: "Intern spelling of v2.std.decl_facts_skeleton authored_string_literal_edge_name, duplicated in the seed until that Symbol row emits this const. WHY RUST REMAINS NECESSARY: constructor-spelling walks skip by intern equality on the host EdgeLabel; the seed cannot yet consume the .dag Symbol as its intern table.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete AUTHORED_STRING_LITERAL_EDGE when that host const is emitted from authored_string_literal_edge_name so a rename cannot silently un-skip constructor-spelling walks.",
current_boundary: "v1_compiler.data_initializer_identity AUTHORED_STRING_LITERAL_EDGE; consumed only by with_authored_string_literals when attaching named edges. crate-internal."
}

data with_authored_string_literals_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef {
module_path: "v1_compiler.data_initializer_identity",
decl_name: "with_authored_string_literals",
field: WholeDeclaration
}
],
reason: "Attaches collected LitStrs as named authored_string_literal children on the marshaled Node record. WHY RUST REMAINS NECESSARY: coproduct_reflection marshals DataItem through host marshal_data_initializer_projection; the attach is a host seam beside that projection until the projection carries LitStr atoms. PURPOSE-serving for v2 lexeme-keyed discovery; not a new language behavior.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete with_authored_string_literals together with collect_authored_string_literals when marshal_data_initializer_projection interns every initializer LitStr; the coproduct_reflection DataItem arm then returns the projection unattached.",
current_boundary: "v1_compiler.data_initializer_identity with_authored_string_literals; one call site in v1_compiler.coproduct_reflection marshal_decl_fact_node DataItem arm. pub(crate)."
}
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ data projection_drops_the_value_its_consumer_keys_on: RecurringFailureMode = Rec

"IT ALSO CORRECTED THE BRIEF THAT SENT SOMEONE TO FIX IT. The work item stated that a bare String initializer projects no atom identity WHILE A LIST-LITERAL INITIALIZER DOES, and scoped the repair to making the bare position behave like the list position. There is no such discriminator: both shapes are value-blind. Building the briefed repair would have copied a projection that also drops the value, and the discovery gate would have stayed blind while the change reported the blind spot closed — a false green on the exact axis the work existed to fix. The reading consistent with every measurement is that what surfaced for the list specimen was ExprRecordLit CONSTRUCTOR SPELLING, which v2.std.decl_facts_skeleton decl_facts_outer_record_constructor_lexeme_authority_note already records as spelling and explicitly not identity — spelling surfaces, authored values never do. A brief that names a discriminator is a measurement claim and is owed a reproduction before it is owed an implementation.",

"RUNG FOUND AT: mitigation by review — nothing refuses, and the gap was found only because a consumer's green was distrusted and re-measured. ATTAINABLE CEILING: structurally guaranteed. The question 'does this declaration fact carry the authored value' is decidable and fully modelled, so once the projection carries values a lexeme-keyed reader cannot be blind to a value that is present, and the class stops depending on anyone remembering to check. NEXT-RUNG TRIGGER, named as the CAPABILITY and not as an artifact that would contribute to one: DataItem declaration facts carrying authored string values through decl_facts_at, sufficient for a lexeme-keyed consumer to distinguish two rows by what they author. A projection change that carries values for one initializer shape does NOT satisfy it, because a per-shape answer has the same blind spot as none — which is the error the originating brief made.",
"RUNG FOUND AT: mitigation by review — nothing refuses, and the gap was found only because a consumer's green was distrusted and re-measured. RUNG NOW: mechanically preventable — executed evidence is test.claim.decl_fact_value_projection_witness (three value-only pairs must project different atoms) and test.claim.self_host_v1_consumer_census_witness_test discovery_fold_sees_a_bare_string_initializer; those rows stay enrolled as regression controls. The invalid state remains writable because authored LitStrs ride a host attach beside the typechecked projection, not inhabitance of that projection. ATTAINABLE CEILING: structurally guaranteed. NEXT-RUNG TRIGGER: marshal_data_initializer_projection itself interns every initializer LitStr into the typechecked Node so collect_authored_string_literals / with_authored_string_literals is deleted (v2.std.decl_facts_skeleton collect_authored_string_literals_dissolve_on). A per-shape attach does not satisfy the ceiling.",
],

evidence: [],
Expand Down
8 changes: 8 additions & 0 deletions dag/gunbc/seed_growth_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,11 @@ import gunbc.reference_closure_binder_seed_growth { reference_closure_binder_see
import gunbc.bare_reference_scanner_admission { bare_reference_scanner_seed_growth_justification }
import gunbc.ambiguity_ban_admission { ambiguity_ban_seed_growth_justification }
import gunbc.decl_facts_shared_memo_seed_growth { decl_facts_shared_memo_seed_growth_justification }
import gunbc.decl_facts_authored_string_attach_seed_growth {
collect_authored_string_literals_seed_growth_justification,
authored_string_literal_edge_seed_growth_justification,
with_authored_string_literals_seed_growth_justification
}
import gunbc.keyed_declaration_read_seed_growth { keyed_declaration_read_seed_growth_justification }
import gunbc.census_memo_seed_growth { census_memo_seed_growth_justification }
import gunbc.claim_unwind_seed_growth { claim_unwind_seed_growth_justification }
Expand Down Expand Up @@ -253,6 +258,9 @@ fn seed_growth_justification_roster() -> List<SeedGrowthJustification> {
regen_convergence_seed_growth_justification,
dag_artifact_identity_seed_growth_justification,
decl_facts_shared_memo_seed_growth_justification,
collect_authored_string_literals_seed_growth_justification,
authored_string_literal_edge_seed_growth_justification,
with_authored_string_literals_seed_growth_justification,
keyed_declaration_read_seed_growth_justification,
cli_wire_host_seed_growth_justification,
filesystem_create_new_seed_growth_justification,
Expand Down
Loading
Loading