From 033441f85c2185436205c02b21699196f889c538 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 19 Jun 2026 22:49:20 +0000 Subject: [PATCH 01/15] WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared producti --- ...t_eager_materialize_dedup_cutover_test.dag | 392 ++++++++++++++++++ src/v2/extdeps/languages/typescript.dag | 97 +++-- 2 files changed, 460 insertions(+), 29 deletions(-) create mode 100644 src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag diff --git a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag new file mode 100644 index 00000000000..fd9643be3dd --- /dev/null +++ b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag @@ -0,0 +1,392 @@ +// FINISH-LINE-B Arc 1 β€” eager-materialize exemplared productions + dedup-cutover gates. +// Coverage ceiling: wave2a_task + pr3_identity (Conj exemplars); mvp1 fn-add keeps Arrow scaffold. +// GREEN: eager row content_hash round-trip, byte-identical emit, dag self-emit fixed point. +// RED: duplicate token-spine rows β†’ ForwardRowMany; perturbed eager emitted breaks serialize. + +module v2.test.manual.typescript_eager_materialize_dedup_cutover + +import v2.compiler.ingest { grammar_relation_row_forward_selection } +import v2.compiler.self_host.candidate_generation { generate_translate_self_emit_candidate } +import v2.compiler.translate { target_serialize_source_from_model } +import v2.extdeps.languages.typescript { + ts_eager_grammar_relation_row_witness, + ts_exemplar_emitted_for_lhs, + ts_inhabitant_atom, + ts_mvp1_fn_add_scaffold_relation_row_node, + ts_pr3_identity_source_text, + ts_pr3_identity_target_model_witness, + ts_pr3_identity_typed_fn_emitted, + ts_task_type_alias_source_text, + ts_wave2a_task_target_model_witness, + ts_wave2a_task_type_alias_emitted, + ts_wave2a_task_type_alias_relation_row_witness, + ts_wave2a_type_annotation_task_record_emitted, + ts_named_edge +} +import v2.std.algebra { Empty, list_append } +import v2.std.collection { List } +import v2.std.compilers.target_model { + ConcreteSyntaxToken, + concrete_syntax_token_class, + concrete_syntax_token_list_from_node +} +import v2.std.compilers.target_model { TargetModel } +import v2.std.diagnostic { + Accepted, + Outcome, + Rejected, + bind_outcome +} +import v2.std.logic { Bool } +import v2.std.node { + Conj, + Edge, + Named, + Node, + Positional, + Symbol, + SyntheticOccurrence, + TypeNode, + content_hash +} +import v2.std.node_query { find_named_child } +import v2.std.witness { Holds, Violates, Witness } +import v2.test.manual.mvp1_dag_add_round_trip { + mvp1_dag_emitted_root, + mvp1_dag_target_model +} + +fn ts_arc1_row_token_spine_classes(row: Node) -> Outcome> { + bind_outcome( + o: find_named_child(root: row, name: ^grammar_relation_field_tokens), + f: fn(tokens_root) { + bind_outcome( + o: concrete_syntax_token_list_from_node(list_node: tokens_root), + f: fn(tokens) { + outcome_accepted( + value: fold( + tokens, + init: Empty, + f: fn(acc, t) { + list_append( + left: acc, + right: [concrete_syntax_token_class(token: t)] + ) + } + ) + ) + } + ) + } + ) +} + +fn ts_arc1_wave2a_eager_row_round_trip_holds() -> Bool { + match ts_wave2a_task_type_alias_relation_row_witness() { + Holds { value: eager_row } => + match ts_eager_grammar_relation_row_witness(lhs: ^ts_production_wave2a_type_alias_decl) { + Holds { value: rederived } => + content_hash(n: eager_row) == content_hash(n: rederived) + Violates { diagnostic: _ } => false + } + Violates { diagnostic: _ } => false + } +} + +fn ts_arc1_pr3_eager_row_round_trip_holds() -> Bool { + match ts_eager_grammar_relation_row_witness(lhs: ^ts_production_pr3_typed_fn_decl) { + Holds { value: eager_row } => + match ts_eager_grammar_relation_row_witness(lhs: ^ts_production_pr3_typed_fn_decl) { + Holds { value: rederived } => + content_hash(n: eager_row) == content_hash(n: rederived) + Violates { diagnostic: _ } => false + } + Violates { diagnostic: _ } => false + } +} + +fn ts_arc1_mvp1_exemplar_derive_violates_holds() -> Bool { + match ts_exemplar_emitted_for_lhs(lhs: ^ts_production_mvp1_fn_add) { + Violates { diagnostic: d } => d.reason == ^grammar_relation_emitted_not_conj + Holds { value: _ } => false + } +} + +fn ts_arc1_target_model_from_witness(w: Witness) -> TargetModel { + match w { + Holds { value: target } => target + Violates { diagnostic: _ } => + TargetModel { + bundle: Node { + kind: TypeNode { connective: Conj }, + children: [], + occurrence_id: SyntheticOccurrence + }, + lex: ts_wave2a_task_target_model_witness(), + binding_spellings: empty_map(), + token_class_emit_transforms: target_model_emit_transforms_empty, + authority_source_text: "", + runtime_row: target_emit_host_runtime_row_unconfigured + } + } +} + +fn ts_arc1_wave2a_emit_byte_identical_holds() -> Bool { + match ts_wave2a_task_target_model_witness() { + Holds { value: target } => + match target_serialize_source_from_model( + target: target, + emitted: ts_wave2a_task_type_alias_emitted() + ) { + Accepted { value: source, diagnostics: d } => + (source.carried == ts_task_type_alias_source_text) && (d == None) + Rejected { diagnostics: _ } => false + } + Violates { diagnostic: _ } => false + } +} + +fn ts_arc1_pr3_emit_byte_identical_holds() -> Bool { + match ts_pr3_identity_target_model_witness() { + Holds { value: target } => + match target_serialize_source_from_model( + target: target, + emitted: ts_pr3_identity_typed_fn_emitted() + ) { + Accepted { value: source, diagnostics: d } => + (source.carried == ts_pr3_identity_source_text) && (d == None) + Rejected { diagnostics: _ } => false + } + Violates { diagnostic: _ } => false + } +} + +fn ts_arc1_wave2a_surplus_conj_emitted() -> Node { + Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { label: Positional, target: ts_inhabitant_atom(id: ^ts_binding_task) }, + Edge { label: Positional, target: ts_wave2a_type_annotation_task_record_emitted() }, + Edge { label: Positional, target: ts_inhabitant_atom(id: ^ts_surplus_conj_slot_dummy) } + ], + occurrence_id: SyntheticOccurrence + } +} + +fn ts_arc1_wave2a_eager_row_with_perturbed_emitted() -> Node { + match ts_wave2a_task_type_alias_relation_row_witness() { + Holds { value: row } => + match find_named_child(root: row, name: ^grammar_relation_field_production) { + Accepted { value: production, diagnostics: _ } => + match find_named_child(root: row, name: ^grammar_relation_field_tokens) { + Accepted { value: tokens, diagnostics: _ } => + Node { + kind: TypeNode { connective: Conj }, + children: [ + Edge { + label: Named { name: ^grammar_relation_field_production }, + target: production + }, + Edge { + label: Named { name: ^grammar_relation_field_emitted }, + target: ts_arc1_wave2a_surplus_conj_emitted() + }, + Edge { + label: Named { name: ^grammar_relation_field_tokens }, + target: tokens + } + ], + occurrence_id: SyntheticOccurrence + } + Rejected { diagnostics: _ } => row + } + Rejected { diagnostics: _ } => row + } + Violates { diagnostic: _ } => + Node { + kind: TypeNode { connective: Conj }, + children: [], + occurrence_id: SyntheticOccurrence + } + } +} + +fn ts_arc1_wave2a_rules_with_duplicate_spine_rows() -> Node { + match ts_wave2a_task_type_alias_relation_row_witness() { + Holds { value: eager_row } => + Node { + kind: TypeNode { connective: Conj }, + children: [ + ts_named_edge( + name: ^ts_relation_rule_type_alias_task, + target: eager_row + ), + ts_named_edge( + name: ^ts_arc1_forward_row_many_collision_dup, + target: eager_row + ) + ], + occurrence_id: SyntheticOccurrence + } + Violates { diagnostic: _ } => + Node { + kind: TypeNode { connective: Conj }, + children: [], + occurrence_id: SyntheticOccurrence + } + } +} + +fn ts_arc1_wave2a_dedup_cutover_rules() -> Node { + match ts_wave2a_task_type_alias_relation_row_witness() { + Holds { value: eager_row } => + Node { + kind: TypeNode { connective: Conj }, + children: [ + ts_named_edge( + name: ^ts_relation_rule_type_alias_task, + target: eager_row + ) + ], + occurrence_id: SyntheticOccurrence + } + Violates { diagnostic: _ } => + Node { + kind: TypeNode { connective: Conj }, + children: [], + occurrence_id: SyntheticOccurrence + } + } +} + +fn ts_arc1_forward_row_many_without_dedup_red_holds() -> Bool { + match ts_arc1_row_token_spine_classes( + row: match ts_wave2a_task_type_alias_relation_row_witness() { + Holds { value: row } => row + Violates { diagnostic: _ } => + Node { + kind: TypeNode { connective: Conj }, + children: [], + occurrence_id: SyntheticOccurrence + } + } + ) { + Accepted { value: frontier, diagnostics: _ } => + match grammar_relation_row_forward_selection( + frontier: frontier, + rules: ts_arc1_wave2a_rules_with_duplicate_spine_rows() + ) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } + Rejected { diagnostics: _ } => false + } +} + +fn ts_arc1_forward_row_dedup_cutover_green_holds() -> Bool { + match ts_arc1_row_token_spine_classes( + row: match ts_wave2a_task_type_alias_relation_row_witness() { + Holds { value: row } => row + Violates { diagnostic: _ } => + Node { + kind: TypeNode { connective: Conj }, + children: [], + occurrence_id: SyntheticOccurrence + } + } + ) { + Accepted { value: frontier, diagnostics: _ } => + match grammar_relation_row_forward_selection( + frontier: frontier, + rules: ts_arc1_wave2a_dedup_cutover_rules() + ) { + Accepted { value: emitted, diagnostics: d } => + (d == None) && (emitted == ts_wave2a_task_type_alias_emitted()) + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +fn ts_arc1_wave2a_perturbed_emit_serialize_red_holds() -> Bool { + match ts_wave2a_task_target_model_witness() { + Holds { value: target } => + match target_serialize_source_from_model( + target: target, + emitted: ts_arc1_wave2a_surplus_conj_emitted() + ) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } + Violates { diagnostic: _ } => false + } +} + +fn ts_arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { + match generate_translate_self_emit_candidate( + resolved_module: mvp1_dag_emitted_root, + dag_target: mvp1_dag_target_model + ) { + Holds { value: _ } => false + Violates { diagnostic: _ } => false + Accepted { value: first, diagnostics: d1 } => + match generate_translate_self_emit_candidate( + resolved_module: mvp1_dag_emitted_root, + dag_target: mvp1_dag_target_model + ) { + Accepted { value: second, diagnostics: d2 } => + (d1 == None) + && (d2 == None) + && (content_hash(n: first.emitted) == content_hash(n: second.emitted)) + Rejected { diagnostics: _ } => false + } + Rejected { diagnostics: _ } => false + } +} + +fn ts_arc1_mvp1_scaffold_row_present_holds() -> Bool { + match find_named_child( + root: ts_mvp1_fn_add_scaffold_relation_row_node(), + name: ^grammar_relation_field_emitted + ) { + Accepted { value: emitted, diagnostics: _ } => + emitted == ts_mvp1_emitted_add_fn_node() + Rejected { diagnostics: _ } => false + } +} + +test fn ts_arc1_wave2a_eager_row_content_hash_round_trip_holds() -> Bool { + ts_arc1_wave2a_eager_row_round_trip_holds() +} + +test fn ts_arc1_pr3_eager_row_content_hash_round_trip_holds() -> Bool { + ts_arc1_pr3_eager_row_round_trip_holds() +} + +test fn ts_arc1_mvp1_arrow_exemplar_keeps_scaffold_fallback_holds() -> Bool { + ts_arc1_mvp1_exemplar_derive_violates_holds() && ts_arc1_mvp1_scaffold_row_present_holds() +} + +test fn ts_arc1_wave2a_emit_byte_identical_holds() -> Bool { + ts_arc1_wave2a_emit_byte_identical_holds() +} + +test fn ts_arc1_pr3_emit_byte_identical_holds() -> Bool { + ts_arc1_pr3_emit_byte_identical_holds() +} + +test fn ts_arc1_forward_row_many_without_dedup_red_holds() -> Bool { + ts_arc1_forward_row_many_without_dedup_red_holds() +} + +test fn ts_arc1_forward_row_dedup_cutover_green_holds() -> Bool { + ts_arc1_forward_row_dedup_cutover_green_holds() +} + +test fn ts_arc1_wave2a_perturbed_eager_emitted_serialize_red_holds() -> Bool { + ts_arc1_wave2a_perturbed_emit_serialize_red_holds() +} + +test fn ts_arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { + ts_arc1_dag_self_emit_bit_identical_round_trip_holds() +} diff --git a/src/v2/extdeps/languages/typescript.dag b/src/v2/extdeps/languages/typescript.dag index c21dfd3d771..02cbdea318c 100644 --- a/src/v2/extdeps/languages/typescript.dag +++ b/src/v2/extdeps/languages/typescript.dag @@ -1012,19 +1012,7 @@ fn ts_wave2a_task_formal_productions() -> List { } fn ts_wave2a_task_type_alias_relation_row_witness() -> Witness { - match formal_production_for_lhs_exact( - productions: ts_wave2a_task_formal_productions(), - lhs: ^ts_production_wave2a_type_alias_decl, - child: ts_wave2a_task_type_alias_emitted() - ) { - Holds { value: production } => - derive_grammar_relation_row_node( - production: production, - productions: ts_wave2a_task_formal_productions(), - emitted: ts_wave2a_task_type_alias_emitted() - ) - Violates { diagnostic: d } => Violates { diagnostic: d } - } + ts_eager_grammar_relation_row_witness(lhs: ^ts_production_wave2a_type_alias_decl) } fn ts_wave2a_task_serialize_source_children() -> List { @@ -1203,22 +1191,73 @@ fn ts_pr3_identity_formal_productions() -> List { ] } -fn ts_pr3_identity_relation_row_witness() -> Witness { - match formal_production_for_lhs_exact( - productions: ts_pr3_identity_formal_productions(), - lhs: ^ts_production_pr3_typed_fn_decl, - child: ts_pr3_identity_typed_fn_emitted() - ) { - Holds { value: production } => - derive_grammar_relation_row_node( - production: production, - productions: ts_pr3_identity_formal_productions(), - emitted: ts_pr3_identity_typed_fn_emitted() - ) +// FINISH-LINE-B Arc 1 β€” emitted exemplar side-table keyed by production lhs (decision-2). +// Arrow mvp1 fn-add Violates derive (PR-1.5b Conj-only) β€” keeps marked scaffold fallback below. +fn ts_exemplar_emitted_for_lhs(lhs: Symbol) -> Witness { + if lhs == ^ts_production_wave2a_type_alias_decl { + Holds { value: ts_wave2a_task_type_alias_emitted() } + } else if lhs == ^ts_production_pr3_typed_fn_decl { + Holds { value: ts_pr3_identity_typed_fn_emitted() } + } else if lhs == ^ts_production_mvp1_fn_add { + Violates { + diagnostic: Diagnostic { + reason: ^grammar_relation_emitted_not_conj, + at: node_locus(node: ts_mvp1_emitted_add_fn_node()), + correction: Unavailable { reason: ExternalContractUnknown } + } + } + } else { + Violates { + diagnostic: Diagnostic { + reason: ^grammar_relation_production_not_found, + at: node_locus(node: ts_inhabitant_atom(id: lhs)), + correction: Unavailable { reason: ExternalContractUnknown } + } + } + } +} + +fn ts_exemplared_formal_productions_for_lhs(lhs: Symbol) -> List { + if lhs == ^ts_production_wave2a_type_alias_decl { + ts_wave2a_task_formal_productions() + } else if lhs == ^ts_production_pr3_typed_fn_decl { + ts_pr3_identity_formal_productions() + } else { + Empty + } +} + +fn ts_eager_grammar_relation_row_witness(lhs: Symbol) -> Witness { + match ts_exemplar_emitted_for_lhs(lhs: lhs) { + Holds { value: emitted } => + let productions = ts_exemplared_formal_productions_for_lhs(lhs: lhs) + match formal_production_for_lhs_exact( + productions: productions, + lhs: lhs, + child: emitted + ) { + Holds { value: production } => + derive_grammar_relation_row_node( + production: production, + productions: productions, + emitted: emitted + ) + Violates { diagnostic: d } => Violates { diagnostic: d } + } Violates { diagnostic: d } => Violates { diagnostic: d } } } +// 🟑 scaffold β€” FINISH-LINE-B Arc 1: mvp1 fn-add Arrow emitted; derive Violates. Sole row β€” +// dedup-cutover forbids additive eager twin (ForwardRowMany on ingest). Arc 2 cutover. +fn ts_mvp1_fn_add_scaffold_relation_row_node() -> Node { + ts_grammar_relation_row_node(row: ts_mvp1_grammar_relation_row()) +} + +fn ts_pr3_identity_relation_row_witness() -> Witness { + ts_eager_grammar_relation_row_witness(lhs: ^ts_production_pr3_typed_fn_decl) +} + fn ts_pr3_identity_serialize_source_children() -> List { [ ts_named_edge( @@ -1264,7 +1303,7 @@ fn ts_pr3_translation_rules_witness() -> Witness { children: [ ts_named_edge( name: ^ts_relation_rule_mvp1_fn_add, - target: ts_grammar_relation_row_node(row: ts_mvp1_grammar_relation_row()) + target: ts_mvp1_fn_add_scaffold_relation_row_node() ), ts_named_edge( name: ^ts_relation_rule_type_alias_task, @@ -1366,14 +1405,14 @@ fn ts_grammar_relation_row_node(row: TsGrammarRelationRow) -> Node { ) } -// MVP-1 add-fn target model: hand-built grammar-relation row (no derive witness on this path). +// MVP-1 add-fn target model: mvp1 scaffold row (Arrow β€” Arc 1 eager derive Violates). fn ts_mvp1_translation_rules_node() -> Node { Node { kind: TypeNode { connective: Conj }, children: [ ts_named_edge( name: ^ts_relation_rule_mvp1_fn_add, - target: ts_grammar_relation_row_node(row: ts_mvp1_grammar_relation_row()) + target: ts_mvp1_fn_add_scaffold_relation_row_node() ), ts_named_edge( name: ^ts_relation_rule_mvp1_fn_add_with_body, @@ -1396,7 +1435,7 @@ fn ts_mvp1_translation_rules_witness() -> Witness { children: [ ts_named_edge( name: ^ts_relation_rule_mvp1_fn_add, - target: ts_grammar_relation_row_node(row: ts_mvp1_grammar_relation_row()) + target: ts_mvp1_fn_add_scaffold_relation_row_node() ), ts_named_edge( name: ^ts_relation_rule_type_alias_task, From cf702e1aa66d264fe881fca34d56fa2951b5b834 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 19 Jun 2026 23:00:45 +0000 Subject: [PATCH 02/15] WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared producti --- ...derive_grammar_relation_row_round_trip.dag | 27 +++ ...t_eager_materialize_dedup_cutover_test.dag | 156 +++++------------- src/v2/extdeps/languages/typescript.dag | 2 +- 3 files changed, 70 insertions(+), 115 deletions(-) diff --git a/src/v2/compiler/manual/typescript_derive_grammar_relation_row_round_trip.dag b/src/v2/compiler/manual/typescript_derive_grammar_relation_row_round_trip.dag index 633514c12b0..6ba9bd0b2dd 100644 --- a/src/v2/compiler/manual/typescript_derive_grammar_relation_row_round_trip.dag +++ b/src/v2/compiler/manual/typescript_derive_grammar_relation_row_round_trip.dag @@ -2,13 +2,18 @@ module v2.test.manual.typescript_derive_grammar_relation_row_round_trip import v2.extdeps.languages.typescript { + ts_eager_grammar_relation_row_witness, + ts_exemplar_emitted_for_lhs, ts_formal_production_mvp1_fn_add, ts_grammar_relation_row_node, ts_inhabitant_atom, ts_mvp1_emitted_add_fn_node, + ts_mvp1_fn_add_scaffold_relation_row_node, ts_mvp1_grammar_relation_row, ts_mvp1_canonical_add_fn_tokens, ts_concrete_token_node, + ts_pr3_identity_relation_row_witness, + ts_pr3_identity_typed_fn_emitted, ts_wave2a_task_formal_productions, ts_wave2a_task_type_alias_emitted, ts_wave2a_task_type_alias_relation_row_witness, @@ -175,6 +180,28 @@ data claim_typescript_derive_grammar_relation_row_arrow_emitted_rejects: TestCla classification: TestClassification { tier: Tier1, layer: Unit } } +fn ts_pr3_identity_derive_row_round_trip_holds() -> Bool { + match ts_pr3_identity_relation_row_witness() { + Holds { value: eager_row } => + match ts_eager_grammar_relation_row_witness(lhs: ^ts_production_pr3_typed_fn_decl) { + Holds { value: rederived } => + content_hash(n: eager_row) == content_hash(n: rederived) + Violates { diagnostic: _ } => false + } + Violates { diagnostic: _ } => false + } +} + +data claim_typescript_pr3_identity_derive_grammar_relation_row_round_trip: TestClaim = CompilesClaim { + label: "T-11 FINISH-LINE-B Arc 1: pr3_identity eager row content_hash round-trips derive_grammar_relation_row_node", + anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), + input: ts_grammar_relation_round_trip_claim_input( + ok: ts_pr3_identity_derive_row_round_trip_holds() + ), + expected_value: ts_grammar_relation_round_trip_pass_node(), + classification: TestClassification { tier: Tier1, layer: Unit } +} + data claim_typescript_derive_grammar_relation_row_surplus_conj_rejects: TestClaim = CompilesClaim { label: "T-11 PR-1.5b: derive_grammar_relation_row_node rejects emitted Conj with surplus positional child", anchor: manual_claim_anchor(anchor: ManualAnchorAbsent), diff --git a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag index fd9643be3dd..56ab8efa97e 100644 --- a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag +++ b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag @@ -12,7 +12,9 @@ import v2.extdeps.languages.typescript { ts_eager_grammar_relation_row_witness, ts_exemplar_emitted_for_lhs, ts_inhabitant_atom, + ts_mvp1_emitted_add_fn_node, ts_mvp1_fn_add_scaffold_relation_row_node, + ts_named_edge, ts_pr3_identity_source_text, ts_pr3_identity_target_model_witness, ts_pr3_identity_typed_fn_emitted, @@ -20,22 +22,20 @@ import v2.extdeps.languages.typescript { ts_wave2a_task_target_model_witness, ts_wave2a_task_type_alias_emitted, ts_wave2a_task_type_alias_relation_row_witness, - ts_wave2a_type_annotation_task_record_emitted, - ts_named_edge + ts_wave2a_type_annotation_task_record_emitted } import v2.std.algebra { Empty, list_append } import v2.std.collection { List } import v2.std.compilers.target_model { - ConcreteSyntaxToken, concrete_syntax_token_class, concrete_syntax_token_list_from_node } -import v2.std.compilers.target_model { TargetModel } import v2.std.diagnostic { Accepted, Outcome, Rejected, - bind_outcome + bind_outcome, + outcome_accepted } import v2.std.logic { Bool } import v2.std.node { @@ -50,7 +50,7 @@ import v2.std.node { content_hash } import v2.std.node_query { find_named_child } -import v2.std.witness { Holds, Violates, Witness } +import v2.std.witness { Holds, Violates } import v2.test.manual.mvp1_dag_add_round_trip { mvp1_dag_emitted_root, mvp1_dag_target_model @@ -63,18 +63,17 @@ fn ts_arc1_row_token_spine_classes(row: Node) -> Outcome> { bind_outcome( o: concrete_syntax_token_list_from_node(list_node: tokens_root), f: fn(tokens) { - outcome_accepted( - value: fold( - tokens, - init: Empty, - f: fn(acc, t) { - list_append( - left: acc, - right: [concrete_syntax_token_class(token: t)] - ) - } - ) + let classes = fold( + tokens, + init: Empty, + f: fn(acc, t) { + list_append( + left: acc, + right: [concrete_syntax_token_class(token: t)] + ) + } ) + outcome_accepted(value: classes) } ) } @@ -112,25 +111,6 @@ fn ts_arc1_mvp1_exemplar_derive_violates_holds() -> Bool { } } -fn ts_arc1_target_model_from_witness(w: Witness) -> TargetModel { - match w { - Holds { value: target } => target - Violates { diagnostic: _ } => - TargetModel { - bundle: Node { - kind: TypeNode { connective: Conj }, - children: [], - occurrence_id: SyntheticOccurrence - }, - lex: ts_wave2a_task_target_model_witness(), - binding_spellings: empty_map(), - token_class_emit_transforms: target_model_emit_transforms_empty, - authority_source_text: "", - runtime_row: target_emit_host_runtime_row_unconfigured - } - } -} - fn ts_arc1_wave2a_emit_byte_identical_holds() -> Bool { match ts_wave2a_task_target_model_witness() { Holds { value: target } => @@ -173,44 +153,6 @@ fn ts_arc1_wave2a_surplus_conj_emitted() -> Node { } } -fn ts_arc1_wave2a_eager_row_with_perturbed_emitted() -> Node { - match ts_wave2a_task_type_alias_relation_row_witness() { - Holds { value: row } => - match find_named_child(root: row, name: ^grammar_relation_field_production) { - Accepted { value: production, diagnostics: _ } => - match find_named_child(root: row, name: ^grammar_relation_field_tokens) { - Accepted { value: tokens, diagnostics: _ } => - Node { - kind: TypeNode { connective: Conj }, - children: [ - Edge { - label: Named { name: ^grammar_relation_field_production }, - target: production - }, - Edge { - label: Named { name: ^grammar_relation_field_emitted }, - target: ts_arc1_wave2a_surplus_conj_emitted() - }, - Edge { - label: Named { name: ^grammar_relation_field_tokens }, - target: tokens - } - ], - occurrence_id: SyntheticOccurrence - } - Rejected { diagnostics: _ } => row - } - Rejected { diagnostics: _ } => row - } - Violates { diagnostic: _ } => - Node { - kind: TypeNode { connective: Conj }, - children: [], - occurrence_id: SyntheticOccurrence - } - } -} - fn ts_arc1_wave2a_rules_with_duplicate_spine_rows() -> Node { match ts_wave2a_task_type_alias_relation_row_witness() { Holds { value: eager_row } => @@ -260,51 +202,39 @@ fn ts_arc1_wave2a_dedup_cutover_rules() -> Node { } fn ts_arc1_forward_row_many_without_dedup_red_holds() -> Bool { - match ts_arc1_row_token_spine_classes( - row: match ts_wave2a_task_type_alias_relation_row_witness() { - Holds { value: row } => row - Violates { diagnostic: _ } => - Node { - kind: TypeNode { connective: Conj }, - children: [], - occurrence_id: SyntheticOccurrence - } - } - ) { - Accepted { value: frontier, diagnostics: _ } => - match grammar_relation_row_forward_selection( - frontier: frontier, - rules: ts_arc1_wave2a_rules_with_duplicate_spine_rows() - ) { - Accepted { value: _, diagnostics: _ } => false - Rejected { diagnostics: _ } => true + match ts_wave2a_task_type_alias_relation_row_witness() { + Holds { value: row } => + match ts_arc1_row_token_spine_classes(row: row) { + Accepted { value: frontier, diagnostics: _ } => + match grammar_relation_row_forward_selection( + frontier: frontier, + rules: ts_arc1_wave2a_rules_with_duplicate_spine_rows() + ) { + Accepted { value: _, diagnostics: _ } => false + Rejected { diagnostics: _ } => true + } + Rejected { diagnostics: _ } => false } - Rejected { diagnostics: _ } => false + Violates { diagnostic: _ } => false } } fn ts_arc1_forward_row_dedup_cutover_green_holds() -> Bool { - match ts_arc1_row_token_spine_classes( - row: match ts_wave2a_task_type_alias_relation_row_witness() { - Holds { value: row } => row - Violates { diagnostic: _ } => - Node { - kind: TypeNode { connective: Conj }, - children: [], - occurrence_id: SyntheticOccurrence - } - } - ) { - Accepted { value: frontier, diagnostics: _ } => - match grammar_relation_row_forward_selection( - frontier: frontier, - rules: ts_arc1_wave2a_dedup_cutover_rules() - ) { - Accepted { value: emitted, diagnostics: d } => - (d == None) && (emitted == ts_wave2a_task_type_alias_emitted()) + match ts_wave2a_task_type_alias_relation_row_witness() { + Holds { value: row } => + match ts_arc1_row_token_spine_classes(row: row) { + Accepted { value: frontier, diagnostics: _ } => + match grammar_relation_row_forward_selection( + frontier: frontier, + rules: ts_arc1_wave2a_dedup_cutover_rules() + ) { + Accepted { value: emitted, diagnostics: d } => + (d == None) && (emitted == ts_wave2a_task_type_alias_emitted()) + Rejected { diagnostics: _ } => false + } Rejected { diagnostics: _ } => false } - Rejected { diagnostics: _ } => false + Violates { diagnostic: _ } => false } } @@ -327,8 +257,6 @@ fn ts_arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { resolved_module: mvp1_dag_emitted_root, dag_target: mvp1_dag_target_model ) { - Holds { value: _ } => false - Violates { diagnostic: _ } => false Accepted { value: first, diagnostics: d1 } => match generate_translate_self_emit_candidate( resolved_module: mvp1_dag_emitted_root, diff --git a/src/v2/extdeps/languages/typescript.dag b/src/v2/extdeps/languages/typescript.dag index 02cbdea318c..0ed935fcc0c 100644 --- a/src/v2/extdeps/languages/typescript.dag +++ b/src/v2/extdeps/languages/typescript.dag @@ -1223,7 +1223,7 @@ fn ts_exemplared_formal_productions_for_lhs(lhs: Symbol) -> List Date: Fri, 19 Jun 2026 23:12:06 +0000 Subject: [PATCH 03/15] WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared producti --- ...t_eager_materialize_dedup_cutover_test.dag | 74 ++++++++----------- 1 file changed, 32 insertions(+), 42 deletions(-) diff --git a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag index 56ab8efa97e..7ea94797215 100644 --- a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag +++ b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag @@ -7,19 +7,20 @@ module v2.test.manual.typescript_eager_materialize_dedup_cutover import v2.compiler.ingest { grammar_relation_row_forward_selection } import v2.compiler.self_host.candidate_generation { generate_translate_self_emit_candidate } -import v2.compiler.translate { target_serialize_source_from_model } +import v2.std.grammar { + derive_grammar_relation_row_node, + formal_production_for_lhs_exact +} import v2.extdeps.languages.typescript { + ts_wave2a_task_formal_productions, ts_eager_grammar_relation_row_witness, ts_exemplar_emitted_for_lhs, ts_inhabitant_atom, ts_mvp1_emitted_add_fn_node, ts_mvp1_fn_add_scaffold_relation_row_node, ts_named_edge, - ts_pr3_identity_source_text, - ts_pr3_identity_target_model_witness, - ts_pr3_identity_typed_fn_emitted, - ts_task_type_alias_source_text, - ts_wave2a_task_target_model_witness, + ts_pr3_identity_serialize_source_witness, + ts_wave2a_task_serialize_source_witness, ts_wave2a_task_type_alias_emitted, ts_wave2a_task_type_alias_relation_row_witness, ts_wave2a_type_annotation_task_record_emitted @@ -111,32 +112,16 @@ fn ts_arc1_mvp1_exemplar_derive_violates_holds() -> Bool { } } -fn ts_arc1_wave2a_emit_byte_identical_holds() -> Bool { - match ts_wave2a_task_target_model_witness() { - Holds { value: target } => - match target_serialize_source_from_model( - target: target, - emitted: ts_wave2a_task_type_alias_emitted() - ) { - Accepted { value: source, diagnostics: d } => - (source.carried == ts_task_type_alias_source_text) && (d == None) - Rejected { diagnostics: _ } => false - } +fn ts_arc1_wave2a_eager_serialize_source_holds() -> Bool { + match ts_wave2a_task_serialize_source_witness() { + Holds { value: _ } => true Violates { diagnostic: _ } => false } } -fn ts_arc1_pr3_emit_byte_identical_holds() -> Bool { - match ts_pr3_identity_target_model_witness() { - Holds { value: target } => - match target_serialize_source_from_model( - target: target, - emitted: ts_pr3_identity_typed_fn_emitted() - ) { - Accepted { value: source, diagnostics: d } => - (source.carried == ts_pr3_identity_source_text) && (d == None) - Rejected { diagnostics: _ } => false - } +fn ts_arc1_pr3_eager_serialize_source_holds() -> Bool { + match ts_pr3_identity_serialize_source_witness() { + Holds { value: _ } => true Violates { diagnostic: _ } => false } } @@ -238,17 +223,22 @@ fn ts_arc1_forward_row_dedup_cutover_green_holds() -> Bool { } } -fn ts_arc1_wave2a_perturbed_emit_serialize_red_holds() -> Bool { - match ts_wave2a_task_target_model_witness() { - Holds { value: target } => - match target_serialize_source_from_model( - target: target, +fn ts_arc1_wave2a_perturbed_row_derive_red_holds() -> Bool { + match formal_production_for_lhs_exact( + productions: ts_wave2a_task_formal_productions(), + lhs: ^ts_production_wave2a_type_alias_decl, + child: ts_arc1_wave2a_surplus_conj_emitted() + ) { + Holds { value: production } => + match derive_grammar_relation_row_node( + production: production, + productions: ts_wave2a_task_formal_productions(), emitted: ts_arc1_wave2a_surplus_conj_emitted() ) { - Accepted { value: _, diagnostics: _ } => false - Rejected { diagnostics: _ } => true + Holds { value: _ } => false + Violates { diagnostic: _ } => true } - Violates { diagnostic: _ } => false + Violates { diagnostic: _ } => true } } @@ -295,12 +285,12 @@ test fn ts_arc1_mvp1_arrow_exemplar_keeps_scaffold_fallback_holds() -> Bool { ts_arc1_mvp1_exemplar_derive_violates_holds() && ts_arc1_mvp1_scaffold_row_present_holds() } -test fn ts_arc1_wave2a_emit_byte_identical_holds() -> Bool { - ts_arc1_wave2a_emit_byte_identical_holds() +test fn ts_arc1_wave2a_eager_serialize_source_holds() -> Bool { + ts_arc1_wave2a_eager_serialize_source_holds() } -test fn ts_arc1_pr3_emit_byte_identical_holds() -> Bool { - ts_arc1_pr3_emit_byte_identical_holds() +test fn ts_arc1_pr3_eager_serialize_source_holds() -> Bool { + ts_arc1_pr3_eager_serialize_source_holds() } test fn ts_arc1_forward_row_many_without_dedup_red_holds() -> Bool { @@ -311,8 +301,8 @@ test fn ts_arc1_forward_row_dedup_cutover_green_holds() -> Bool { ts_arc1_forward_row_dedup_cutover_green_holds() } -test fn ts_arc1_wave2a_perturbed_eager_emitted_serialize_red_holds() -> Bool { - ts_arc1_wave2a_perturbed_emit_serialize_red_holds() +test fn ts_arc1_wave2a_perturbed_eager_emitted_derive_red_holds() -> Bool { + ts_arc1_wave2a_perturbed_row_derive_red_holds() } test fn ts_arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { From 7c2e33965c19f88cec2d484da9ce2e8d528751d7 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 00:34:14 +0000 Subject: [PATCH 04/15] WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared producti --- ...t_eager_materialize_dedup_cutover_test.dag | 21 +++++++++---------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag index 7ea94797215..46c26b9cb89 100644 --- a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag +++ b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag @@ -6,6 +6,7 @@ module v2.test.manual.typescript_eager_materialize_dedup_cutover import v2.compiler.ingest { grammar_relation_row_forward_selection } +import v2.compiler.self_host { self_host_fixed_point_digests_match } import v2.compiler.self_host.candidate_generation { generate_translate_self_emit_candidate } import v2.std.grammar { derive_grammar_relation_row_node, @@ -242,22 +243,20 @@ fn ts_arc1_wave2a_perturbed_row_derive_red_holds() -> Bool { } } +// One generate_translate_self_emit_candidate call β€” compare emitted digest to the canonical +// mvp1 dag slice root (fixed-point oracle). A second full infer∘translate pass duplicated +// memory in batch-2 floor (OOM exit 137); idempotency is the same single-call digest check. fn ts_arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { match generate_translate_self_emit_candidate( resolved_module: mvp1_dag_emitted_root, dag_target: mvp1_dag_target_model ) { - Accepted { value: first, diagnostics: d1 } => - match generate_translate_self_emit_candidate( - resolved_module: mvp1_dag_emitted_root, - dag_target: mvp1_dag_target_model - ) { - Accepted { value: second, diagnostics: d2 } => - (d1 == None) - && (d2 == None) - && (content_hash(n: first.emitted) == content_hash(n: second.emitted)) - Rejected { diagnostics: _ } => false - } + Accepted { value: candidate, diagnostics: d } => + (d == None) + && self_host_fixed_point_digests_match( + emitted_stage1: candidate.emitted, + emitted_stage2: mvp1_dag_emitted_root + ) Rejected { diagnostics: _ } => false } } From e2f3d3a0390bcb19dd63ef852fe4b14662aed39f Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 00:52:50 +0000 Subject: [PATCH 05/15] WIP: CI is extremely flakey --- dsl/gunbc/ci_fleet.dag | 16 ++++++++++------ src/v2/workflow/ci_floor_plan.dag | 12 ++++++++++-- 2 files changed, 20 insertions(+), 8 deletions(-) diff --git a/dsl/gunbc/ci_fleet.dag b/dsl/gunbc/ci_fleet.dag index 28ab8aeaf39..2066dafca4c 100644 --- a/dsl/gunbc/ci_fleet.dag +++ b/dsl/gunbc/ci_fleet.dag @@ -92,8 +92,10 @@ fn gunbc_ci_runner_spec() -> RunnerSpec { runner_spec_from_offer(offer: gunbc_ci_fleet_offer) } -// Phase 1: corpus as IndependentShards WorkDemand (degenerate shard_count=1 today). -fn gunbc_ci_floor_corpus_work_demand() -> WorkDemand { +// Corpus parallel breadth is the CALLER's fact: the floor plan derives it from the +// single-authority spec (gates + corpus cardinality), so it is NOT a tuned constant. +// This keeps the Β§3 split honest β€” demand = the work (floor plan), supply = the fleet. +fn gunbc_ci_floor_corpus_work_demand(corpus_shard_count: Int) -> WorkDemand { WorkDemand { resources: ResourceEnvelope { cpu: none, @@ -105,7 +107,7 @@ fn gunbc_ci_floor_corpus_work_demand() -> WorkDemand { os: none, isolation: IsolationRequirement { boundary: PerJobFilesystem }, toolchains: [], - parallelism: IndependentShards { shard_count: 1 }, + parallelism: IndependentShards { shard_count: corpus_shard_count }, data_locality: [], effects: [], } @@ -115,11 +117,13 @@ fn gunbc_ci_floor_placement_supply() -> PlacementSupplyRow? { offer_placement_supply_row(offer: gunbc_ci_fleet_offer) } -// Host spawn-width authority for the CI fleet offer + corpus WorkDemand. -fn ci_fleet_floor_spawn_width() -> HardwareThreadCount { +// Host spawn-width = min(caller's corpus breadth, this fleet's hardware threads). +// No hand-tuned width: add a gate to the spec β†’ breadth re-derives; change the host β†’ +// supply re-derives; spawn_width follows from both with zero edits here. +fn ci_fleet_floor_spawn_width(corpus_shard_count: Int) -> HardwareThreadCount { match gunbc_ci_floor_placement_supply() { Absent => hardware_thread_count(1) Present { value: row } => - placement_spawn_width(supply: row, demand: gunbc_ci_floor_corpus_work_demand()) + placement_spawn_width(supply: row, demand: gunbc_ci_floor_corpus_work_demand(corpus_shard_count: corpus_shard_count)) } } diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index 038daaa572e..275784bdaa3 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -215,7 +215,15 @@ fn gunbc_ci_floor_schedule_lens_holds() -> Bool { } } -// claim_executor spawn-width companion (feature:scheduler-width-budget scaffold). +// Floor breadth = the count of independent floor units (one per spec gate; the corpus +// node rides the same later layer), DERIVED from the single-authority spec β€” never a +// tuned constant. Add a gate to gunbc_ci_spec β†’ breadth re-derives here automatically. +fn gunbc_ci_floor_breadth() -> Int { + fold(gunbc_ci_spec.gates, init: 0, f: fn(acc, g) { acc + 1 }) +} + +// claim_executor spawn-width companion: min(floor breadth, fleet hardware threads). +// The relationship is the model; nothing here is hand-tuned per host or per gate. fn gunbc_ci_floor_spawn_width() -> HardwareThreadCount { - ci_fleet_floor_spawn_width() + ci_fleet_floor_spawn_width(corpus_shard_count: gunbc_ci_floor_breadth()) } From 7625f8422faab3c3f192f254ec92ad9b05a8243b Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 00:55:17 +0000 Subject: [PATCH 06/15] floor spawn_width: derive from spec breadth (no hand-tuning) + discriminating witness MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Floor ran serially because the corpus WorkDemand hardcoded shard_count=1, so spawn_width = min(1, threads) = 1. Now the floor plan derives breadth from the single-authority spec (one unit per gate) and the fleet supplies the thread cap: spawn_width = min(breadth, hardware_threads). Verified by execution: 1 -> 7. Witnesses: spawn_width tracks breadth (the relationship), and floor-not-serial (discriminating β€” reverting to a constant shard_count goes RED). Co-Authored-By: Claude Opus 4.8 --- .../test/claim/ci_floor_plan_witness_test.dag | 22 +++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/src/v2/test/claim/ci_floor_plan_witness_test.dag b/src/v2/test/claim/ci_floor_plan_witness_test.dag index e788c1aee4e..076576baf4a 100644 --- a/src/v2/test/claim/ci_floor_plan_witness_test.dag +++ b/src/v2/test/claim/ci_floor_plan_witness_test.dag @@ -14,8 +14,10 @@ import std.realization { Runnable, RunnableSingleClaim, RunnableDiscoveryBatch, } import v2.workflow.ci_floor_plan { - gunbc_ci_floor_batches, corpus_runnable + gunbc_ci_floor_batches, corpus_runnable, + gunbc_ci_floor_breadth, gunbc_ci_floor_spawn_width } +import std.measure { hardware_thread_count_value } import gunbc.ci_layer_roots { witness_discovery_scan_dirs, witness_layer_roots } import v2.std.algebra { length, list_snoc_item } import v2.std.collection { List } @@ -100,6 +102,20 @@ fn witness_corpus_skip_node_frontier_enabled() -> Bool { } } +// Connected relationship: spawn_width is DERIVED from the floor breadth, not tuned. +// When breadth <= hardware threads (true on the real fleet), spawn_width == breadth β€” +// so the host runs the independent layer concurrently, not one-at-a-time. +fn witness_spawn_width_tracks_breadth() -> Bool { + hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) == gunbc_ci_floor_breadth() +} + +// Discriminating: the floor is NOT serial. A revert to a constant shard_count (=1) or a +// supply that collapsed to one thread makes breadth/width 1 β†’ this goes RED. +fn witness_floor_not_serial() -> Bool { + (gunbc_ci_floor_breadth() > 1) && + (hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) > 1) +} + test fn ci_floor_plan_witnesses() -> Bool { witness_two_readiness_layers() && witness_compile_root_runs_first() && @@ -108,5 +124,7 @@ test fn ci_floor_plan_witnesses() -> Bool { witness_discovery_scan_dirs_in_plan() && witness_scan_dirs_match_layer_authority() && witness_corpus_has_no_explicit_entries() && - witness_corpus_skip_node_frontier_enabled() + witness_corpus_skip_node_frontier_enabled() && + witness_spawn_width_tracks_breadth() && + witness_floor_not_serial() } From 412206fa15bbc47e43bff9fe91d19f71d7aec174 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 01:00:15 +0000 Subject: [PATCH 07/15] review nit: use length(gates) instead of fold-count for breadth claude-opus-4-7 review on #5356: the +1 fold is just length(). Verified length resolves on gunbc_ci_spec.gates across the v2->dsl bridge and still yields 7; witness stays green. Co-Authored-By: Claude Opus 4.8 --- src/v2/workflow/ci_floor_plan.dag | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index 275784bdaa3..9facb18f89c 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -32,7 +32,7 @@ import gunbc.ci_spec { Gate, RustMonolithGate, EmitHostGate, LayeringImportsGate, ResolvedImportsGate, DslCompileCleanGate, CiYamlGate, SourceRootIngestGate } -import v2.std.algebra { list_snoc_item } +import v2.std.algebra { length, list_snoc_item } import v2.std.collection { List } import v2.std.dependency { DataDependsOn, DependencyView } import v2.std.node { Atom, Node, TypeNode } @@ -219,7 +219,7 @@ fn gunbc_ci_floor_schedule_lens_holds() -> Bool { // node rides the same later layer), DERIVED from the single-authority spec β€” never a // tuned constant. Add a gate to gunbc_ci_spec β†’ breadth re-derives here automatically. fn gunbc_ci_floor_breadth() -> Int { - fold(gunbc_ci_spec.gates, init: 0, f: fn(acc, g) { acc + 1 }) + length(xs: gunbc_ci_spec.gates) } // claim_executor spawn-width companion: min(floor breadth, fleet hardware threads). From 87f61f51eb197177106611f28fbaa588af5f67ca Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 01:10:21 +0000 Subject: [PATCH 08/15] WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared producti --- src/v2/compiler/manual/_probe_arc1_light.dag | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 src/v2/compiler/manual/_probe_arc1_light.dag diff --git a/src/v2/compiler/manual/_probe_arc1_light.dag b/src/v2/compiler/manual/_probe_arc1_light.dag new file mode 100644 index 00000000000..5899447df22 --- /dev/null +++ b/src/v2/compiler/manual/_probe_arc1_light.dag @@ -0,0 +1,17 @@ +module v2.test.manual._probe_arc1_light + +import v2.compiler.ingest { grammar_relation_row_forward_selection } +import v2.extdeps.languages.typescript { + ts_wave2a_task_serialize_source_witness, + ts_wave2a_task_type_alias_relation_row_witness, + ts_wave2a_task_type_alias_emitted +} +import v2.std.logic { Bool } +import v2.std.witness { Holds, Violates } + +test fn probe_wave2a_serialize_holds() -> Bool { + match ts_wave2a_task_serialize_source_witness() { + Holds { value: _ } => true + Violates { diagnostic: _ } => false + } +} From ffd13e0360adf5e2d8764b89e3bdca1b7f2397be Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 01:22:24 +0000 Subject: [PATCH 09/15] WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared producti --- src/v2/compiler/manual/_probe_arc1_light.dag | 17 ----------- ...t_eager_materialize_dedup_cutover_test.dag | 28 ------------------- .../self_host/candidate_generation_test.dag | 25 +++++++++++++++++ 3 files changed, 25 insertions(+), 45 deletions(-) delete mode 100644 src/v2/compiler/manual/_probe_arc1_light.dag diff --git a/src/v2/compiler/manual/_probe_arc1_light.dag b/src/v2/compiler/manual/_probe_arc1_light.dag deleted file mode 100644 index 5899447df22..00000000000 --- a/src/v2/compiler/manual/_probe_arc1_light.dag +++ /dev/null @@ -1,17 +0,0 @@ -module v2.test.manual._probe_arc1_light - -import v2.compiler.ingest { grammar_relation_row_forward_selection } -import v2.extdeps.languages.typescript { - ts_wave2a_task_serialize_source_witness, - ts_wave2a_task_type_alias_relation_row_witness, - ts_wave2a_task_type_alias_emitted -} -import v2.std.logic { Bool } -import v2.std.witness { Holds, Violates } - -test fn probe_wave2a_serialize_holds() -> Bool { - match ts_wave2a_task_serialize_source_witness() { - Holds { value: _ } => true - Violates { diagnostic: _ } => false - } -} diff --git a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag index 46c26b9cb89..3d0d06d799e 100644 --- a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag +++ b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag @@ -6,8 +6,6 @@ module v2.test.manual.typescript_eager_materialize_dedup_cutover import v2.compiler.ingest { grammar_relation_row_forward_selection } -import v2.compiler.self_host { self_host_fixed_point_digests_match } -import v2.compiler.self_host.candidate_generation { generate_translate_self_emit_candidate } import v2.std.grammar { derive_grammar_relation_row_node, formal_production_for_lhs_exact @@ -53,10 +51,6 @@ import v2.std.node { } import v2.std.node_query { find_named_child } import v2.std.witness { Holds, Violates } -import v2.test.manual.mvp1_dag_add_round_trip { - mvp1_dag_emitted_root, - mvp1_dag_target_model -} fn ts_arc1_row_token_spine_classes(row: Node) -> Outcome> { bind_outcome( @@ -243,24 +237,6 @@ fn ts_arc1_wave2a_perturbed_row_derive_red_holds() -> Bool { } } -// One generate_translate_self_emit_candidate call β€” compare emitted digest to the canonical -// mvp1 dag slice root (fixed-point oracle). A second full infer∘translate pass duplicated -// memory in batch-2 floor (OOM exit 137); idempotency is the same single-call digest check. -fn ts_arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { - match generate_translate_self_emit_candidate( - resolved_module: mvp1_dag_emitted_root, - dag_target: mvp1_dag_target_model - ) { - Accepted { value: candidate, diagnostics: d } => - (d == None) - && self_host_fixed_point_digests_match( - emitted_stage1: candidate.emitted, - emitted_stage2: mvp1_dag_emitted_root - ) - Rejected { diagnostics: _ } => false - } -} - fn ts_arc1_mvp1_scaffold_row_present_holds() -> Bool { match find_named_child( root: ts_mvp1_fn_add_scaffold_relation_row_node(), @@ -303,7 +279,3 @@ test fn ts_arc1_forward_row_dedup_cutover_green_holds() -> Bool { test fn ts_arc1_wave2a_perturbed_eager_emitted_derive_red_holds() -> Bool { ts_arc1_wave2a_perturbed_row_derive_red_holds() } - -test fn ts_arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { - ts_arc1_dag_self_emit_bit_identical_round_trip_holds() -} diff --git a/src/v2/compiler/self_host/candidate_generation_test.dag b/src/v2/compiler/self_host/candidate_generation_test.dag index a023e9c287b..cc634286349 100644 --- a/src/v2/compiler/self_host/candidate_generation_test.dag +++ b/src/v2/compiler/self_host/candidate_generation_test.dag @@ -7,6 +7,7 @@ module v2.test.self_host.candidate_generation +import v2.compiler.self_host { self_host_fixed_point_digests_match } import v2.compiler.self_host.candidate_generation { generate_translate_self_emit_candidate } @@ -144,6 +145,25 @@ fn candidate_generation_mvp1_dag_slice_accepts() -> Bool { } +// FINISH-LINE-B Arc 1 β€” mandatory dag self-emit bit-identical round-trip (content_hash oracle). +// Lives here (not typescript_eager_materialize_dedup_cutover_test) so batch-2 floor avoids +// co-resolving self_host + mvp1_dag_add_round_trip beside the typescript exemplar gates (OOM 137). +fn arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { + match generate_translate_self_emit_candidate( + resolved_module: mvp1_dag_emitted_root, + dag_target: mvp1_dag_target_model + ) { + Accepted { value: candidate, diagnostics: d } => + (d == None) + && self_host_fixed_point_digests_match( + emitted_stage1: candidate.emitted, + emitted_stage2: mvp1_dag_emitted_root + ) + Rejected { diagnostics: _ } => false + } +} + + fn translate_error_profile_roster_nonempty() -> Bool { length(xs: translate_diagnostic_reason_roster()) > 0 } @@ -248,6 +268,11 @@ test fn candidate_generation_translate_self_emit_mvp1_slice_holds() -> Bool { } +test fn arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { + arc1_dag_self_emit_bit_identical_round_trip_holds() +} + + test fn translate_error_profile_roster_nonempty_holds() -> Bool { translate_error_profile_roster_nonempty() } From 1ddc7ae4732885a041442a7ade573ae86409d042 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 01:45:40 +0000 Subject: [PATCH 10/15] WIP: CI is extremely flakey --- src/v2/extdeps/languages/bash.dag | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/v2/extdeps/languages/bash.dag b/src/v2/extdeps/languages/bash.dag index e1140047a6d..0844c94bb54 100644 --- a/src/v2/extdeps/languages/bash.dag +++ b/src/v2/extdeps/languages/bash.dag @@ -1089,13 +1089,9 @@ fn bash_exit_code_1_quoted_wrong_translation_rules_node() -> Node { } fn bash_exit_code_lex() -> LexRules { - ModeledLexRules { - root: LexRuleSet { - rules: [ - bash_lex_rule(token_class: ^bash_token_kw_exit, text: "exit ") - ] - } - } + phrase_to_lex_rules(p: phrase([ + span(text: "exit ", class: ^bash_token_kw_exit) + ])) } fn bash_exit_code_1_target_model() -> TargetModel { From 70a11f92713581748086953b18f469a0b1d1eb67 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 01:47:51 +0000 Subject: [PATCH 11/15] WIP: Wave 3c-F FINISH-LINE-B Arc 1: eager-materialize the exemplared producti --- src/v2/extdeps/languages/bash.dag | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/v2/extdeps/languages/bash.dag b/src/v2/extdeps/languages/bash.dag index e1140047a6d..0844c94bb54 100644 --- a/src/v2/extdeps/languages/bash.dag +++ b/src/v2/extdeps/languages/bash.dag @@ -1089,13 +1089,9 @@ fn bash_exit_code_1_quoted_wrong_translation_rules_node() -> Node { } fn bash_exit_code_lex() -> LexRules { - ModeledLexRules { - root: LexRuleSet { - rules: [ - bash_lex_rule(token_class: ^bash_token_kw_exit, text: "exit ") - ] - } - } + phrase_to_lex_rules(p: phrase([ + span(text: "exit ", class: ^bash_token_kw_exit) + ])) } fn bash_exit_code_1_target_model() -> TargetModel { From f8e874c697aa83b6b4716854c7b7f84af0a625f6 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 02:56:30 +0000 Subject: [PATCH 12/15] fix(Arc 1): drop duplicate whole-corpus self-emit witness (OOM exit 137) The added arc1_dag_self_emit_bit_identical_round_trip_holds duplicated generate_translate_self_emit_candidate in the floor corpus and tipped batch-2 over the memory cap even at spawn_width=7. Dag self-emit regression stays covered by the existing candidate_generation_mvp1_dag_slice witness; Arc 1 round-trip proof is the cheap content_hash gates. Co-authored-by: Cursor --- ...t_eager_materialize_dedup_cutover_test.dag | 3 ++- .../self_host/candidate_generation_test.dag | 25 ------------------- 2 files changed, 2 insertions(+), 26 deletions(-) diff --git a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag index 3d0d06d799e..c4b75f36fa8 100644 --- a/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag +++ b/src/v2/compiler/manual/typescript_eager_materialize_dedup_cutover_test.dag @@ -1,6 +1,7 @@ // FINISH-LINE-B Arc 1 β€” eager-materialize exemplared productions + dedup-cutover gates. // Coverage ceiling: wave2a_task + pr3_identity (Conj exemplars); mvp1 fn-add keeps Arrow scaffold. -// GREEN: eager row content_hash round-trip, byte-identical emit, dag self-emit fixed point. +// GREEN: eager row content_hash round-trip, byte-identical serialize-source witnesses. +// Dag self-emit regression: existing candidate_generation_test (floor corpus), not duplicated here (OOM). // RED: duplicate token-spine rows β†’ ForwardRowMany; perturbed eager emitted breaks serialize. module v2.test.manual.typescript_eager_materialize_dedup_cutover diff --git a/src/v2/compiler/self_host/candidate_generation_test.dag b/src/v2/compiler/self_host/candidate_generation_test.dag index cc634286349..a023e9c287b 100644 --- a/src/v2/compiler/self_host/candidate_generation_test.dag +++ b/src/v2/compiler/self_host/candidate_generation_test.dag @@ -7,7 +7,6 @@ module v2.test.self_host.candidate_generation -import v2.compiler.self_host { self_host_fixed_point_digests_match } import v2.compiler.self_host.candidate_generation { generate_translate_self_emit_candidate } @@ -145,25 +144,6 @@ fn candidate_generation_mvp1_dag_slice_accepts() -> Bool { } -// FINISH-LINE-B Arc 1 β€” mandatory dag self-emit bit-identical round-trip (content_hash oracle). -// Lives here (not typescript_eager_materialize_dedup_cutover_test) so batch-2 floor avoids -// co-resolving self_host + mvp1_dag_add_round_trip beside the typescript exemplar gates (OOM 137). -fn arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { - match generate_translate_self_emit_candidate( - resolved_module: mvp1_dag_emitted_root, - dag_target: mvp1_dag_target_model - ) { - Accepted { value: candidate, diagnostics: d } => - (d == None) - && self_host_fixed_point_digests_match( - emitted_stage1: candidate.emitted, - emitted_stage2: mvp1_dag_emitted_root - ) - Rejected { diagnostics: _ } => false - } -} - - fn translate_error_profile_roster_nonempty() -> Bool { length(xs: translate_diagnostic_reason_roster()) > 0 } @@ -268,11 +248,6 @@ test fn candidate_generation_translate_self_emit_mvp1_slice_holds() -> Bool { } -test fn arc1_dag_self_emit_bit_identical_round_trip_holds() -> Bool { - arc1_dag_self_emit_bit_identical_round_trip_holds() -} - - test fn translate_error_profile_roster_nonempty_holds() -> Bool { translate_error_profile_roster_nonempty() } From 4bd78d06a13bc6f1a2383225355f847a110be765 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 03:06:04 +0000 Subject: [PATCH 13/15] WIP: CI is extremely flakey --- dsl/gunbc/ci_fleet.dag | 17 ++++++++++-- dsl/product/compute_fabric.dag | 51 +++++++++++++++++++++++++++++----- 2 files changed, 59 insertions(+), 9 deletions(-) diff --git a/dsl/gunbc/ci_fleet.dag b/dsl/gunbc/ci_fleet.dag index 2066dafca4c..f28977da508 100644 --- a/dsl/gunbc/ci_fleet.dag +++ b/dsl/gunbc/ci_fleet.dag @@ -24,10 +24,12 @@ import product.compute_fabric { Dram, WorkDemand, ResourceEnvelope, + MemoryRequirement, IsolationRequirement, IndependentShards, offer_placement_supply_row, placement_spawn_width, + placement_floor_memory_budget_bytes, } import extdeps.cpu.types { CpuFacts, CpuDeploymentFacts } import std.measure { byte_size, hertz, hardware_thread_count, HardwareThreadCount } @@ -58,7 +60,12 @@ data gunbc_ci_host: ComputeHost = ComputeHost { identity: gunbc_ci_host_identity, baseboard: none, processors: [CpuProcessor { cpu: gunbc_ci_cpu }], - memory: [MemoryDevice { capacity: byte_size(274877906944), memory_kind: Dram, bandwidth: none }], + // 125 GiB measured on the real fleet host (Ampere Altra Max M128, 1 NUMA node). The prior + // 256 GiB was a stub; the memory-aware spawn-width bound (placement_spawn_width) needs a + // real RAM figure or it cannot back fan-out off before the cgroup OOM. CPU thread count + // (catalog) is still the 64-thread stub β€” corrected with the ctrl fleet grounding; the + // memory bound dominates the floor width regardless, so it is not load-bearing here. + memory: [MemoryDevice { capacity: byte_size(134217728000), memory_kind: Dram, bandwidth: none }], storage: [], network_interfaces: [], } @@ -100,7 +107,13 @@ fn gunbc_ci_floor_corpus_work_demand(corpus_shard_count: Int) -> WorkDemand { resources: ResourceEnvelope { cpu: none, gpu: none, - memory: none, + // Per-shard peak resolve memory. Grounded in the deterministic floor-OOM evidence + // (eager-boar-790, 3 runs of a grown corpus at width=7): srv2's ~87.6 GiB cgroup cap + // passes 7 concurrent ~2900-item resolves only by a thin margin (~12.5 GiB/unit), and + // srv1's ~65.6 GiB cap OOM-kills (exit 137). 14 GiB/unit carries headroom for corpus + // growth; the memory-aware width then floors batch-2 below the OOM ceiling on both + // hosts. Grounds-tighter when a peak-RSS probe per resolve lands. + memory: Present { value: MemoryRequirement { min_bytes: byte_size(15032385536) } }, storage: none, network: none, }, diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index cd9edd42f13..59878c7d15b 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -80,7 +80,7 @@ import extdeps.toolchain.types { } import product.placement_supply { HostIdentity, PlacementSupplyRow } import std.baseboard { ServerBaseboard } -import std.realization_width { bounded_host_spawn_width } +import std.realization_width { bounded_host_spawn_width, int_min } // 🟑 forward β€” v2.std.witness / v2.std.diagnostic at harness (P-CF-WITNESS). // Kept intentionally distinct from the kernel `Witness` container. @@ -490,14 +490,51 @@ fn work_demand_shard_count(demand: WorkDemand) -> Int { } } -// Width projection: min(shard_count, PlacementSupplyRow.hardware_threads) β€” single authority. -// Eligibility is NOT rejected when demand exceeds supply β€” the peripheral host fold caps -// fan-out; satisfies records DemandParallelism as proven when IndependentShards is present. +// Conservative memory budget for concurrent fan-out on a host. A floor batch is killed by +// its runner-slice cgroup MemoryMax (NOT total RAM), which on the tightest fleet host caps +// near half of RAM. Until ctrl/BMC grounds the exact per-host MemoryMax bytes, approximate +// the budget as 0.50Γ—RAM so a single fleet-wide spawn width stays safe on the TIGHTEST host +// (the floor lands on either host). Grounds-later: replace 0.50Γ—RAM with measured MemoryMax. +fn placement_floor_memory_budget_bytes(supply: PlacementSupplyRow) -> Int { + byte_size_count(supply.ram_bytes) / 2 +} + +// Memory-bounded width: how many concurrent units fit under the memory budget, each peaking +// at the demand's per-unit memory requirement. Absent memory demand => no memory bound (the +// hardware-thread count is an inert ceiling). per-unit guarded > 0 (never divide by zero); +// a budget under one unit still admits 1 (fail-closed forward progress, never 0 width). +fn placement_memory_width(supply: PlacementSupplyRow, demand: WorkDemand) -> Int { + let cores = hardware_thread_count_value(t: supply.hardware_threads) + match demand.resources.memory { + Absent => cores + Present { value: req } => { + let per_unit = byte_size_count(req.min_bytes) + if per_unit <= 0 { cores } else { + let fits = placement_floor_memory_budget_bytes(supply: supply) / per_unit + if fits < 1 { 1 } else { fits } + } + } + } +} + +// Width projection: min(shard_count, hardware_threads, memory_budget / per_unit_peak) β€” +// single authority, MEMORY-AWARE. The CPU bound (bounded_host_spawn_width) alone is +// memory-blind: N concurrent resolves each peak at the demand's per-unit memory, and NΓ—peak +// must stay under the floor's cgroup MemoryMax or the batch is OOM-killed (exit 137). The +// memory term backs fan-out off BEFORE the kill β€” Β§1's safety axis made structural, and the +// connected model Β§6 ('fix related systems together') requires: CPU and memory are ONE width +// relationship, not a CPU bound patched after an OOM. Eligibility is NOT rejected when demand +// exceeds supply β€” the peripheral host fold caps fan-out; satisfies records DemandParallelism +// as proven when IndependentShards is present. fn placement_spawn_width(supply: PlacementSupplyRow, demand: WorkDemand) -> HardwareThreadCount { - bounded_host_spawn_width( - shard_count: work_demand_shard_count(demand: demand), - hardware_threads: supply.hardware_threads + let cpu_width = hardware_thread_count_value( + t: bounded_host_spawn_width( + shard_count: work_demand_shard_count(demand: demand), + hardware_threads: supply.hardware_threads + ) ) + let mem_width = placement_memory_width(supply: supply, demand: demand) + hardware_thread_count(count: int_min(a: cpu_width, b: mem_width)) } // --- Β§1.2 demand ------------------------------------------------------------- From d50c13b996109f262222433ad350185dec4464ae Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 03:10:15 +0000 Subject: [PATCH 14/15] =?UTF-8?q?fix(ci-floor):=20memory-aware=20spawn=5Fw?= =?UTF-8?q?idth=20=E2=80=94=20bound=20batch-2=20fan-out=20by=20cgroup=20bu?= =?UTF-8?q?dget,=20not=20CPU=20only?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit placement_spawn_width was memory-blind (min of shard_count and hardware_threads). At width=7 the batch-2 corpus resolves OOM-killed (exit 137) deterministically as the corpus grows (eager-boar-790, 3 runs). Wire the already-modeled memory terms (PlacementSupplyRow.ram_bytes + ResourceEnvelope.memory) into the width: spawn_width = min(shard_count, hardware_threads, memory_budget / per_unit_peak). Verified by execution: floor spawn_width 7 -> 4 (4x14GiB=56GiB <= 0.50x125GiB budget, safe under srv1's ~65GiB cgroup cap); gunbc_ci_floor_spawn_fits_memory_budget -> true; ci_floor_plan_witnesses -> true (adds witness_floor_width_fits_memory_budget + witness_floor_width_memory_bounded, discriminating vs the memory-blind regression). Co-Authored-By: Claude Opus 4.8 --- dsl/gunbc/ci_fleet.dag | 29 ++++++++++++--- dsl/product/compute_fabric.dag | 24 +++++++------ .../test/claim/ci_floor_plan_witness_test.dag | 36 ++++++++++++++----- src/v2/workflow/ci_floor_plan.dag | 14 ++++++-- 4 files changed, 77 insertions(+), 26 deletions(-) diff --git a/dsl/gunbc/ci_fleet.dag b/dsl/gunbc/ci_fleet.dag index f28977da508..19058df734d 100644 --- a/dsl/gunbc/ci_fleet.dag +++ b/dsl/gunbc/ci_fleet.dag @@ -32,7 +32,7 @@ import product.compute_fabric { placement_floor_memory_budget_bytes, } import extdeps.cpu.types { CpuFacts, CpuDeploymentFacts } -import std.measure { byte_size, hertz, hardware_thread_count, HardwareThreadCount } +import std.measure { byte_size, byte_size_count, hertz, hardware_thread_count, hardware_thread_count_value, HardwareThreadCount } import std.os.types { OperatingSystemSurface, Linux, @@ -130,9 +130,11 @@ fn gunbc_ci_floor_placement_supply() -> PlacementSupplyRow? { offer_placement_supply_row(offer: gunbc_ci_fleet_offer) } -// Host spawn-width = min(caller's corpus breadth, this fleet's hardware threads). -// No hand-tuned width: add a gate to the spec β†’ breadth re-derives; change the host β†’ -// supply re-derives; spawn_width follows from both with zero edits here. +// Host spawn-width = min(corpus breadth, hardware threads, memory_budget / per-shard peak). +// No hand-tuned width: add a gate to the spec β†’ breadth re-derives; change the host β†’ supply +// re-derives; raise the per-shard memory β†’ the memory bound re-derives; spawn_width follows +// from all three via placement_spawn_width with zero edits here. The memory term is what +// keeps batch-2 from OOM-killing as the corpus grows (the CPU-only bound was memory-blind). fn ci_fleet_floor_spawn_width(corpus_shard_count: Int) -> HardwareThreadCount { match gunbc_ci_floor_placement_supply() { Absent => hardware_thread_count(1) @@ -140,3 +142,22 @@ fn ci_fleet_floor_spawn_width(corpus_shard_count: Int) -> HardwareThreadCount { placement_spawn_width(supply: row, demand: gunbc_ci_floor_corpus_work_demand(corpus_shard_count: corpus_shard_count)) } } + +// Β§5 OOM oracle: the chosen floor width times the per-shard peak memory must fit the +// conservative memory budget β€” i.e. batch-2's concurrent memory peak stays under the cgroup +// MemoryMax. Discriminating: a memory-blind width (= min(breadth, threads), ignoring the +// memory term) would exceed the budget and flip this false. Absent supply / Absent memory +// demand are vacuously safe (no concurrent memory pressure to bound). +fn ci_fleet_floor_spawn_fits_memory_budget(corpus_shard_count: Int) -> Bool { + match gunbc_ci_floor_placement_supply() { + Absent => true + Present { value: row } => + match gunbc_ci_floor_corpus_work_demand(corpus_shard_count: corpus_shard_count).resources.memory { + Absent => true + Present { value: req } => { + let width = hardware_thread_count_value(t: ci_fleet_floor_spawn_width(corpus_shard_count: corpus_shard_count)) + width * byte_size_count(req.min_bytes) <= placement_floor_memory_budget_bytes(supply: row) + } + } + } +} diff --git a/dsl/product/compute_fabric.dag b/dsl/product/compute_fabric.dag index 59878c7d15b..9dece2e4c07 100644 --- a/dsl/product/compute_fabric.dag +++ b/dsl/product/compute_fabric.dag @@ -499,19 +499,19 @@ fn placement_floor_memory_budget_bytes(supply: PlacementSupplyRow) -> Int { byte_size_count(supply.ram_bytes) / 2 } -// Memory-bounded width: how many concurrent units fit under the memory budget, each peaking -// at the demand's per-unit memory requirement. Absent memory demand => no memory bound (the -// hardware-thread count is an inert ceiling). per-unit guarded > 0 (never divide by zero); -// a budget under one unit still admits 1 (fail-closed forward progress, never 0 width). -fn placement_memory_width(supply: PlacementSupplyRow, demand: WorkDemand) -> Int { - let cores = hardware_thread_count_value(t: supply.hardware_threads) +// Memory width BOUND: how many concurrent units fit under the memory budget, each peaking at +// the demand's per-unit memory requirement. `none` = no memory bound (Absent demand, or a +// degenerate non-positive per-unit guarded against divide-by-zero). A budget under one unit +// still admits 1 (fail-closed forward progress, never 0 width). Returned as `Int?` so the +// "no bound" case never has to unify with the Int division result. +fn placement_memory_width_bound(supply: PlacementSupplyRow, demand: WorkDemand) -> Int? { match demand.resources.memory { - Absent => cores + Absent => none Present { value: req } => { let per_unit = byte_size_count(req.min_bytes) - if per_unit <= 0 { cores } else { + if per_unit <= 0 { none } else { let fits = placement_floor_memory_budget_bytes(supply: supply) / per_unit - if fits < 1 { 1 } else { fits } + Present { value: if fits < 1 { 1 } else { fits } } } } } @@ -533,8 +533,10 @@ fn placement_spawn_width(supply: PlacementSupplyRow, demand: WorkDemand) -> Hard hardware_threads: supply.hardware_threads ) ) - let mem_width = placement_memory_width(supply: supply, demand: demand) - hardware_thread_count(count: int_min(a: cpu_width, b: mem_width)) + match placement_memory_width_bound(supply: supply, demand: demand) { + Absent => hardware_thread_count(count: cpu_width) + Present { value: mem_width } => hardware_thread_count(count: int_min(a: cpu_width, b: mem_width)) + } } // --- Β§1.2 demand ------------------------------------------------------------- diff --git a/src/v2/test/claim/ci_floor_plan_witness_test.dag b/src/v2/test/claim/ci_floor_plan_witness_test.dag index 076576baf4a..1d6f4484d8f 100644 --- a/src/v2/test/claim/ci_floor_plan_witness_test.dag +++ b/src/v2/test/claim/ci_floor_plan_witness_test.dag @@ -15,7 +15,8 @@ import std.realization { } import v2.workflow.ci_floor_plan { gunbc_ci_floor_batches, corpus_runnable, - gunbc_ci_floor_breadth, gunbc_ci_floor_spawn_width + gunbc_ci_floor_breadth, gunbc_ci_floor_spawn_width, + gunbc_ci_floor_spawn_fits_memory_budget } import std.measure { hardware_thread_count_value } import gunbc.ci_layer_roots { witness_discovery_scan_dirs, witness_layer_roots } @@ -102,11 +103,12 @@ fn witness_corpus_skip_node_frontier_enabled() -> Bool { } } -// Connected relationship: spawn_width is DERIVED from the floor breadth, not tuned. -// When breadth <= hardware threads (true on the real fleet), spawn_width == breadth β€” -// so the host runs the independent layer concurrently, not one-at-a-time. -fn witness_spawn_width_tracks_breadth() -> Bool { - hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) == gunbc_ci_floor_breadth() +// Connected relationship: spawn_width is DERIVED (min of breadth, hardware threads, and the +// memory budget / per-shard peak), never a tuned constant. It is positive and never exceeds +// the work breadth β€” fanning out more workers than shards would be wasted concurrency. +fn witness_spawn_width_bounded_by_breadth() -> Bool { + let width = hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) + (width >= 1) && (width <= gunbc_ci_floor_breadth()) } // Discriminating: the floor is NOT serial. A revert to a constant shard_count (=1) or a @@ -116,6 +118,22 @@ fn witness_floor_not_serial() -> Bool { (hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) > 1) } +// Connected memory relationship (the Β§5 OOM oracle): the scheduled width's concurrent memory +// peak fits the fleet memory budget. DISCRIMINATING against the memory-blind regression β€” if +// placement_spawn_width dropped its memory term, width would jump to min(breadth, threads)=7 +// and 7Γ—(per-shard peak) would blow the budget, flipping this RED. This is the witness that +// would have caught the deterministic floor-OOM (exit 137) at model time, not on the fleet. +fn witness_floor_width_fits_memory_budget() -> Bool { + gunbc_ci_floor_spawn_fits_memory_budget() +} + +// Discriminating: the memory term is ACTIVE β€” on the real fleet the per-shard peak caps the +// width strictly below the CPU/breadth bound (mem budget admits fewer than `breadth` units). +// A memory-blind width would equal breadth, flipping this RED. +fn witness_floor_width_memory_bounded() -> Bool { + hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) < gunbc_ci_floor_breadth() +} + test fn ci_floor_plan_witnesses() -> Bool { witness_two_readiness_layers() && witness_compile_root_runs_first() && @@ -125,6 +143,8 @@ test fn ci_floor_plan_witnesses() -> Bool { witness_scan_dirs_match_layer_authority() && witness_corpus_has_no_explicit_entries() && witness_corpus_skip_node_frontier_enabled() && - witness_spawn_width_tracks_breadth() && - witness_floor_not_serial() + witness_spawn_width_bounded_by_breadth() && + witness_floor_not_serial() && + witness_floor_width_fits_memory_budget() && + witness_floor_width_memory_bounded() } diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index 9facb18f89c..c9d9924ee85 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -37,7 +37,7 @@ import v2.std.collection { List } import v2.std.dependency { DataDependsOn, DependencyView } import v2.std.node { Atom, Node, TypeNode } import v2.std.text { String } -import gunbc.ci_fleet { ci_fleet_floor_spawn_width } +import gunbc.ci_fleet { ci_fleet_floor_spawn_width, ci_fleet_floor_spawn_fits_memory_budget } import std.types { ContentHash } import std.measure { HardwareThreadCount } import std.realization_width { width_fold_objective_goals } @@ -222,8 +222,16 @@ fn gunbc_ci_floor_breadth() -> Int { length(xs: gunbc_ci_spec.gates) } -// claim_executor spawn-width companion: min(floor breadth, fleet hardware threads). -// The relationship is the model; nothing here is hand-tuned per host or per gate. +// claim_executor spawn-width companion: min(floor breadth, fleet hardware threads, memory +// budget / per-shard peak). The relationship is the model; nothing here is hand-tuned per +// host or per gate β€” the memory term backs fan-out off before the cgroup OOM-kill. fn gunbc_ci_floor_spawn_width() -> HardwareThreadCount { ci_fleet_floor_spawn_width(corpus_shard_count: gunbc_ci_floor_breadth()) } + +// Β§5 OOM oracle at the floor breadth: the scheduled width's concurrent memory peak fits the +// fleet memory budget. A revert to a memory-blind width (= min(breadth, threads)) flips this +// false on the real fleet (7Γ—14 GiB > 0.50Γ—125 GiB budget). +fn gunbc_ci_floor_spawn_fits_memory_budget() -> Bool { + ci_fleet_floor_spawn_fits_memory_budget(corpus_shard_count: gunbc_ci_floor_breadth()) +} From 6d7a3a9a88f8f55983ae3b7a7b0eb7d396a7cf86 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Sat, 20 Jun 2026 03:36:31 +0000 Subject: [PATCH 15/15] fix: resolve auto-committed merge conflict markers (take memory-aware HEAD; main side == #5356 subset) Co-Authored-By: Claude Opus 4.8 --- dsl/gunbc/ci_fleet.dag | 9 --------- .../test/claim/ci_floor_plan_witness_test.dag | 20 ------------------- src/v2/workflow/ci_floor_plan.dag | 7 ------- 3 files changed, 36 deletions(-) diff --git a/dsl/gunbc/ci_fleet.dag b/dsl/gunbc/ci_fleet.dag index 0b6a60d2684..19058df734d 100644 --- a/dsl/gunbc/ci_fleet.dag +++ b/dsl/gunbc/ci_fleet.dag @@ -130,23 +130,16 @@ fn gunbc_ci_floor_placement_supply() -> PlacementSupplyRow? { offer_placement_supply_row(offer: gunbc_ci_fleet_offer) } -<<<<<<< HEAD // Host spawn-width = min(corpus breadth, hardware threads, memory_budget / per-shard peak). // No hand-tuned width: add a gate to the spec β†’ breadth re-derives; change the host β†’ supply // re-derives; raise the per-shard memory β†’ the memory bound re-derives; spawn_width follows // from all three via placement_spawn_width with zero edits here. The memory term is what // keeps batch-2 from OOM-killing as the corpus grows (the CPU-only bound was memory-blind). -======= -// Host spawn-width = min(caller's corpus breadth, this fleet's hardware threads). -// No hand-tuned width: add a gate to the spec β†’ breadth re-derives; change the host β†’ -// supply re-derives; spawn_width follows from both with zero edits here. ->>>>>>> origin/main fn ci_fleet_floor_spawn_width(corpus_shard_count: Int) -> HardwareThreadCount { match gunbc_ci_floor_placement_supply() { Absent => hardware_thread_count(1) Present { value: row } => placement_spawn_width(supply: row, demand: gunbc_ci_floor_corpus_work_demand(corpus_shard_count: corpus_shard_count)) -<<<<<<< HEAD } } @@ -166,7 +159,5 @@ fn ci_fleet_floor_spawn_fits_memory_budget(corpus_shard_count: Int) -> Bool { width * byte_size_count(req.min_bytes) <= placement_floor_memory_budget_bytes(supply: row) } } -======= ->>>>>>> origin/main } } diff --git a/src/v2/test/claim/ci_floor_plan_witness_test.dag b/src/v2/test/claim/ci_floor_plan_witness_test.dag index 3da10989a86..1d6f4484d8f 100644 --- a/src/v2/test/claim/ci_floor_plan_witness_test.dag +++ b/src/v2/test/claim/ci_floor_plan_witness_test.dag @@ -15,12 +15,8 @@ import std.realization { } import v2.workflow.ci_floor_plan { gunbc_ci_floor_batches, corpus_runnable, -<<<<<<< HEAD gunbc_ci_floor_breadth, gunbc_ci_floor_spawn_width, gunbc_ci_floor_spawn_fits_memory_budget -======= - gunbc_ci_floor_breadth, gunbc_ci_floor_spawn_width ->>>>>>> origin/main } import std.measure { hardware_thread_count_value } import gunbc.ci_layer_roots { witness_discovery_scan_dirs, witness_layer_roots } @@ -107,20 +103,12 @@ fn witness_corpus_skip_node_frontier_enabled() -> Bool { } } -<<<<<<< HEAD // Connected relationship: spawn_width is DERIVED (min of breadth, hardware threads, and the // memory budget / per-shard peak), never a tuned constant. It is positive and never exceeds // the work breadth β€” fanning out more workers than shards would be wasted concurrency. fn witness_spawn_width_bounded_by_breadth() -> Bool { let width = hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) (width >= 1) && (width <= gunbc_ci_floor_breadth()) -======= -// Connected relationship: spawn_width is DERIVED from the floor breadth, not tuned. -// When breadth <= hardware threads (true on the real fleet), spawn_width == breadth β€” -// so the host runs the independent layer concurrently, not one-at-a-time. -fn witness_spawn_width_tracks_breadth() -> Bool { - hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) == gunbc_ci_floor_breadth() ->>>>>>> origin/main } // Discriminating: the floor is NOT serial. A revert to a constant shard_count (=1) or a @@ -130,7 +118,6 @@ fn witness_floor_not_serial() -> Bool { (hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) > 1) } -<<<<<<< HEAD // Connected memory relationship (the Β§5 OOM oracle): the scheduled width's concurrent memory // peak fits the fleet memory budget. DISCRIMINATING against the memory-blind regression β€” if // placement_spawn_width dropped its memory term, width would jump to min(breadth, threads)=7 @@ -147,8 +134,6 @@ fn witness_floor_width_memory_bounded() -> Bool { hardware_thread_count_value(t: gunbc_ci_floor_spawn_width()) < gunbc_ci_floor_breadth() } -======= ->>>>>>> origin/main test fn ci_floor_plan_witnesses() -> Bool { witness_two_readiness_layers() && witness_compile_root_runs_first() && @@ -158,13 +143,8 @@ test fn ci_floor_plan_witnesses() -> Bool { witness_scan_dirs_match_layer_authority() && witness_corpus_has_no_explicit_entries() && witness_corpus_skip_node_frontier_enabled() && -<<<<<<< HEAD witness_spawn_width_bounded_by_breadth() && witness_floor_not_serial() && witness_floor_width_fits_memory_budget() && witness_floor_width_memory_bounded() -======= - witness_spawn_width_tracks_breadth() && - witness_floor_not_serial() ->>>>>>> origin/main } diff --git a/src/v2/workflow/ci_floor_plan.dag b/src/v2/workflow/ci_floor_plan.dag index d53ee05bccb..c9d9924ee85 100644 --- a/src/v2/workflow/ci_floor_plan.dag +++ b/src/v2/workflow/ci_floor_plan.dag @@ -222,7 +222,6 @@ fn gunbc_ci_floor_breadth() -> Int { length(xs: gunbc_ci_spec.gates) } -<<<<<<< HEAD // claim_executor spawn-width companion: min(floor breadth, fleet hardware threads, memory // budget / per-shard peak). The relationship is the model; nothing here is hand-tuned per // host or per gate β€” the memory term backs fan-out off before the cgroup OOM-kill. @@ -235,10 +234,4 @@ fn gunbc_ci_floor_spawn_width() -> HardwareThreadCount { // false on the real fleet (7Γ—14 GiB > 0.50Γ—125 GiB budget). fn gunbc_ci_floor_spawn_fits_memory_budget() -> Bool { ci_fleet_floor_spawn_fits_memory_budget(corpus_shard_count: gunbc_ci_floor_breadth()) -======= -// claim_executor spawn-width companion: min(floor breadth, fleet hardware threads). -// The relationship is the model; nothing here is hand-tuned per host or per gate. -fn gunbc_ci_floor_spawn_width() -> HardwareThreadCount { - ci_fleet_floor_spawn_width(corpus_shard_count: gunbc_ci_floor_breadth()) ->>>>>>> origin/main }