Skip to content
Merged
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
4 changes: 2 additions & 2 deletions dag/gunbc/doc_graph_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -402,7 +402,7 @@ data hand_authored_doc_bind_incomings: List<HandAuthoredDocBind> = [
slug: "c-linkage-unit-realization-design",
primary_work: DeclarationRef { module_path: "v2.std.compilers.compilation_unit", decl_name: "CompilationUnit", field: WholeDeclaration },
additional_works: [
DeclarationRef { module_path: "v2.std.compilers.compilation_unit", decl_name: "partition_fold", field: WholeDeclaration },
DeclarationRef { module_path: "v2.std.compilers.compilation_unit", decl_name: "partition_fold_outcome", field: WholeDeclaration },
DeclarationRef { module_path: "v2.std.compilers.compilation_unit", decl_name: "CompilationUnitId", field: WholeDeclaration },
],
dissolution: PlanRetiresWhen { condition: unbound_dissolution(description: "the work this document plans lands and its subject CompilationUnit describes shipped behavior rather than a planned change; the row deletes with the document. Registered at subject grain: the systems bound here are the ones whose movement would make this document's purpose false, not every system its prose mentions.") },
Expand Down Expand Up @@ -556,7 +556,7 @@ data hand_authored_doc_bind_incomings: List<HandAuthoredDocBind> = [
slug: "emitted-crate-partition-design",
primary_work: DeclarationRef { module_path: "v2.std.compilers.compilation_unit", decl_name: "CompilationUnit", field: WholeDeclaration },
additional_works: [
DeclarationRef { module_path: "v2.std.compilers.compilation_unit", decl_name: "partition_fold", field: WholeDeclaration },
DeclarationRef { module_path: "v2.std.compilers.compilation_unit", decl_name: "partition_fold_outcome", field: WholeDeclaration },
DeclarationRef { module_path: "v2.workflow.rust_crate_partition", decl_name: "PartitionPolicy", field: WholeDeclaration },
],
dissolution: PlanRetiresWhen { condition: unbound_dissolution(description: "the work this document plans lands and its subject CompilationUnit describes shipped behavior rather than a planned change; the row deletes with the document. Registered at subject grain: the systems bound here are the ones whose movement would make this document's purpose false, not every system its prose mentions.") },
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/witness/witness_row_cost_basis.tsv
Original file line number Diff line number Diff line change
Expand Up @@ -650,7 +650,7 @@ src/v2/test/claim/bash_program_fold_test.dag bash_program_serialize_redir_matche
src/v2/test/claim/bash_program_fold_test.dag bash_program_varref_vs_lit_quoting_matches_golden_holds 17 30550328673 srv_fleet_arm64 wall
src/v2/test/claim/build_artifact_verification_witness_test.dag witness_existence_check_no_mtime 184 30550328673 srv_fleet_arm64 wall
src/v2/test/claim/build_transport_admission_witness_test.dag build_transport_admits_dotdot_substring 1 30550328673 srv_fleet_arm64 wall
src/v2/test/claim/c_compilation_unit_witness_test.dag witness_partition_fold_compat_wrapper_not_receipt_path 6 30550328673 srv_fleet_arm64 wall
src/v2/test/claim/c_compilation_unit_witness_test.dag witness_partition_fold_outcome_yields_both_units 6 30550328673 srv_fleet_arm64 wall
src/v2/test/claim/c_compilation_unit_witness_test.dag witness_r4_accepts_link_cyclic_unit_graph 4 30550328673 srv_fleet_arm64 wall
src/v2/test/claim/c_compilation_unit_witness_test.dag witness_r4_accepts_module_scc_split_across_units 1 30550328673 srv_fleet_arm64 wall
src/v2/test/claim/c_compilation_unit_witness_test.dag witness_r4_accepts_pointer_type_cycle_across_units 1 30550328673 srv_fleet_arm64 wall
Expand Down
107 changes: 71 additions & 36 deletions src/v2/extdeps/languages/c.dag
Original file line number Diff line number Diff line change
Expand Up @@ -122,16 +122,21 @@ import v2.std.compilers.compilation_unit {
ModuleDag,
ModuleId,
ModuleTypeDefinitionRow,
MembersResolve,
MembersResolveOk,
MembersResolveRefused,
PartitionFoldOk,
PartitionFoldOutcome,
PartitionFoldRefused,
PartitionInputRejected,
PartitionR4Refused,
PartitionR4Valid,
PartitionR4ValidityVerdict,
module_type_definition_rows,
ResolvedModuleInterface,
module_unit_id,
partition_fold_outcome,
partition_unit_by_id,
resolve_member_interfaces,
type_definition_row_identity
}
import v2.std.logic { Bool }
Expand All @@ -148,8 +153,9 @@ import v2.std.node {
}

// C R3: CompilationUnit.interface renders to the unit .h (declarations only);
// CompilationUnit.members renders to the unit .c (implementation). partition_fold is the sole
// producer of interface/deps; this module only spells linkage paths and cross-unit #include lines.
// CompilationUnit.members renders to the unit .c (implementation). partition_fold_outcome is the
// sole producer of interface/deps; this module only spells linkage paths and cross-unit #include
// lines.

// C R4: permissive on module-SCC split across TUs, UnitGraphCycle, and LinkageCycle —
// mutually-recursive modules may live in different units; each .c #includes peer headers and links
Expand All @@ -161,10 +167,10 @@ data c_by_value_type_cycle_detail: String = "incomplete by-value type containmen

data c_by_value_type_ambiguous_identity_detail: String = "ambiguous type identity across modules for by-value R4 lookup"

// C callers requiring receipt-bearing partition results MUST use c_partition_fold_outcome (routes
// partition_fold_outcome from home). Never treat partition_fold() -> [] as a refusal signal — that
// compat wrapper collapses PartitionFoldRefused to [] (§5 absorbing-fallback). Returns
// PartitionFoldOutcome directly — no parallel C-local coproduct.
// C partition results route through c_partition_fold_outcome (partition_fold_outcome from home),
// which returns PartitionFoldOutcome directly — no parallel C-local coproduct. The List-returning
// compat wrapper that collapsed PartitionFoldRefused to [] no longer exists at the home, so there
// is no non-receipt route left to reach for.

fn c_partition_fold_outcome(
module_dag: ModuleDag,
Expand Down Expand Up @@ -452,15 +458,25 @@ fn c_type_definition_body(row: ModuleTypeDefinitionRow) -> Node {
row.definition
}

fn c_all_type_owners(module_dag: ModuleDag) -> List<CTypeOwner> {
module_dag.modules
|> fold(init: [], f: fn(acc, member_module) {
module_type_definition_rows(module_dag: module_dag, module: member_module)
// The owner roster and the by-value definition lookup both used to re-ask
// module_dag.type_definitions through the home's module_type_definition_rows, whose Rejected arm
// answered [] -- a rejected lookup became "this module owns no types", so c_validate_partition_r4
// answered PartitionR4Valid over a map it had failed to read (DESIGN section 5). Both now read one
// resolved member list, which the home refuses to produce on a rejected lookup; the R4 refusal
// carries that cause rather than a C-local restatement of it.
fn c_resolved_modules(module_dag: ModuleDag) -> MembersResolve {
resolve_member_interfaces(module_dag: module_dag, members: module_dag.modules)
}

fn c_all_type_owners(resolved: List<ResolvedModuleInterface>) -> List<CTypeOwner> {
resolved
|> fold(init: [], f: fn(acc, member) {
member.type_definitions
|> fold(init: acc, f: fn(inner, row) {
inner
|> list_push(
CTypeOwner {
module: member_module,
module: member.module,
identity: type_definition_row_identity(row: row),
}
)
Expand Down Expand Up @@ -526,32 +542,46 @@ fn c_type_owner_for_symbol(
}

fn c_type_definition_for_owner(
module_dag: ModuleDag,
resolved: List<ResolvedModuleInterface>,
owner: CTypeOwner
) -> Optional<Node> {
fold_list(
xs: module_type_definition_rows(module_dag: module_dag, module: owner.module),
xs: resolved,
empty: Absent,
cons: fn(acc, row) {
cons: fn(acc, member) {
match acc {
Present { value: _ } => acc
Absent =>
match type_definition_row_identity(row: row) == owner.identity {
true => Present { value: c_type_definition_body(row: row) }
match member.module == owner.module {
false => Absent
true =>
fold_list(
xs: member.type_definitions,
empty: Absent,
cons: fn(inner, row) {
match inner {
Present { value: _ } => inner
Absent =>
match type_definition_row_identity(row: row) == owner.identity {
true => Present { value: c_type_definition_body(row: row) }
false => Absent
}
}
}
)
}
}
}
)
}

fn c_by_value_type_edges(
module_dag: ModuleDag,
resolved: List<ResolvedModuleInterface>,
owners: List<CTypeOwner>
) -> List<CByValueTypeEdge> {
owners
|> fold(init: [], f: fn(acc, owner) {
match c_type_definition_for_owner(module_dag: module_dag, owner: owner) {
match c_type_definition_for_owner(resolved: resolved, owner: owner) {
Present { value: defn } =>
c_type_atoms_by_value_in_node(node: defn)
|> fold(init: acc, f: fn(inner, sym) {
Expand All @@ -578,15 +608,15 @@ fn c_by_value_type_edges(
}

fn c_by_value_type_identity_resolution_refusal(
module_dag: ModuleDag,
resolved: List<ResolvedModuleInterface>,
owners: List<CTypeOwner>
) -> Optional<String> {
owners
|> fold(init: Absent, f: fn(acc, owner) {
match acc {
Present { value: _ } => acc
Absent =>
match c_type_definition_for_owner(module_dag: module_dag, owner: owner) {
match c_type_definition_for_owner(resolved: resolved, owner: owner) {
Present { value: defn } =>
c_type_atoms_by_value_in_node(node: defn)
|> fold(init: Absent, f: fn(inner_acc, sym) {
Expand Down Expand Up @@ -707,11 +737,11 @@ fn c_find_by_value_type_cycle_detail(
}

fn c_by_value_type_cycle_detail_after_resolution(
module_dag: ModuleDag,
resolved: List<ResolvedModuleInterface>,
assignment: Map<ModuleId, CompilationUnitId>,
owners: List<CTypeOwner>
) -> Optional<String> {
let edges = c_by_value_type_edges(module_dag: module_dag, owners: owners)
let edges = c_by_value_type_edges(resolved: resolved, owners: owners)
c_find_by_value_type_cycle_detail(
edges: edges,
assignment: assignment,
Expand All @@ -720,20 +750,20 @@ fn c_by_value_type_cycle_detail_after_resolution(
}

fn c_partition_by_value_type_cycle_cause(
module_dag: ModuleDag,
resolved: List<ResolvedModuleInterface>,
assignment: Map<ModuleId, CompilationUnitId>,
units: List<CompilationUnit>
) -> Optional<String> {
let _ = units
let owners = c_all_type_owners(module_dag: module_dag)
let owners = c_all_type_owners(resolved: resolved)
match c_by_value_type_identity_resolution_refusal(
module_dag: module_dag,
resolved: resolved,
owners: owners
) {
Present { value: detail } => Present { value: detail }
Absent =>
c_by_value_type_cycle_detail_after_resolution(
module_dag: module_dag,
resolved: resolved,
assignment: assignment,
owners: owners
)
Expand All @@ -745,15 +775,20 @@ fn c_validate_partition_r4(
assignment: Map<ModuleId, CompilationUnitId>,
units: List<CompilationUnit>
) -> PartitionR4ValidityVerdict {
match c_partition_by_value_type_cycle_cause(
module_dag: module_dag,
assignment: assignment,
units: units
) {
Absent => PartitionR4Valid
Present { value: detail } =>
PartitionR4Refused {
cause: ByValueTypeCycle { detail: detail },
match c_resolved_modules(module_dag: module_dag) {
MembersResolveRefused { cause: cause } =>
PartitionR4Refused { cause: PartitionInputRejected { cause: cause } }
MembersResolveOk { members: resolved } =>
match c_partition_by_value_type_cycle_cause(
resolved: resolved,
assignment: assignment,
units: units
) {
Absent => PartitionR4Valid
Present { value: detail } =>
PartitionR4Refused {
cause: ByValueTypeCycle { detail: detail },
}
}
}
}
Expand Down
Loading