Skip to content
Merged
65 changes: 64 additions & 1 deletion dag/extdeps/filesystem/filesystem_io.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@ module extdeps.filesystem.filesystem_io
import v2.std.algebra { filter }
import extdeps.external_authority { ExternalAuthority }
import extdeps.uri { Uri, Https }
import std.types { Bool, FilePath, Int, List, String }
import std.types { Bool, FilePath, Int, List, String, NonEmptyStr }
import std.dissolution { DissolutionCondition, unbound_dissolution }
data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
uri: Uri {
scheme: Https
Expand Down Expand Up @@ -52,6 +53,7 @@ type FilesystemFailureKind
| FilesystemAlreadyExists
| FilesystemPermissionDenied
| FilesystemNotDirectory
| FilesystemCrossDevice
| FilesystemOtherFailure

type FilesystemFailureKindAdmission
Expand All @@ -67,6 +69,8 @@ fn admit_filesystem_failure_kind(observed: String) -> FilesystemFailureKindAdmis
FilesystemFailureKindAdmitted { kind: FilesystemPermissionDenied }
} else if observed == "not_a_directory" {
FilesystemFailureKindAdmitted { kind: FilesystemNotDirectory }
} else if observed == "cross_device" {
FilesystemFailureKindAdmitted { kind: FilesystemCrossDevice }
} else if observed == "other" {
FilesystemFailureKindAdmitted { kind: FilesystemOtherFailure }
} else {
Expand All @@ -80,6 +84,7 @@ fn filesystem_failure_kind_name(kind: FilesystemFailureKind) -> String {
FilesystemAlreadyExists => "already_exists"
FilesystemPermissionDenied => "permission_denied"
FilesystemNotDirectory => "not_a_directory"
FilesystemCrossDevice => "cross_device"
FilesystemOtherFailure => "other"
}
}
Expand Down Expand Up @@ -117,6 +122,7 @@ fn filesystem_exact_read(
FilesystemAlreadyExists => FilesystemExactPathUnreadable { path: path, kind: k, error: error }
FilesystemPermissionDenied => FilesystemExactPathUnreadable { path: path, kind: k, error: error }
FilesystemNotDirectory => FilesystemExactPathUnreadable { path: path, kind: k, error: error }
FilesystemCrossDevice => FilesystemExactPathUnreadable { path: path, kind: k, error: error }
FilesystemOtherFailure => FilesystemExactPathUnreadable { path: path, kind: k, error: error }
}
}
Expand Down Expand Up @@ -151,12 +157,57 @@ fn filesystem_create_new(
FilesystemNotFound => FilesystemCreateRefused { path: path, kind: k, error: error }
FilesystemPermissionDenied => FilesystemCreateRefused { path: path, kind: k, error: error }
FilesystemNotDirectory => FilesystemCreateRefused { path: path, kind: k, error: error }
FilesystemCrossDevice => FilesystemCreateRefused { path: path, kind: k, error: error }
FilesystemOtherFailure => FilesystemCreateRefused { path: path, kind: k, error: error }
}
}
}
}

// A CREATE-ONLY LINK OF AN EXISTING FILE UNDER A NEW NAME. The name appears with the source's bytes
// complete or not at all, because it is one link(2) -- the same primitive WriteCreateNew publishes
// with -- and an existing target refuses (create-only), so a second linker of one name is told it
// lost and must read what is there. A source on a DIFFERENT filesystem refuses as cross-device: a
// link across filesystems is not a copy, and nothing here falls back to one, so a caller staging a
// file for a store must stage it on the store root's filesystem. The source is left in place; the
// caller owns its staging name.
type FilesystemLinkCreateNew
= FilesystemLinked { path: String }
| FilesystemLinkTargetOccupied { path: String }
| FilesystemLinkCrossDevice { source: String, path: String }
| FilesystemLinkRefused { path: String, kind: FilesystemFailureKind, error: String }
| FilesystemLinkKindUnrecognized { path: String, observed: String, error: String }

// THE CONSUMER IS A DECLARED FRONTIER (DESIGN section 3c), stated here beside the operation: the
// production caller lands in the change stacked directly on this one.
data filesystem_link_create_new_consumer_frontier: DissolutionCondition = unbound_dissolution(description: "TRIGGER: gunbc#13095 lands, in which extdeps.realization.materialization_store_local local_store_link_part publishes every staged byte part into the store root through Filesystem.LinkCreateNew and classifies the answer with filesystem_link_create_new (linked or occupied proceed; cross-device and every refusal refuse the commit). SUFFICIENT FOR: the operation has a production consumer on the store's commit path, not only its witnesses; until that change lands the operation is consumed by its witnesses alone, and this row is retired by that landing and nothing else." as NonEmptyStr)

fn filesystem_link_create_new(
source: String,
path: String,
success: Bool,
error: String,
error_kind: String,
) -> FilesystemLinkCreateNew {
if success {
FilesystemLinked { path: path }
} else {
match admit_filesystem_failure_kind(observed: error_kind) {
FilesystemFailureKindUnrecognized { observed: o } =>
FilesystemLinkKindUnrecognized { path: path, observed: o, error: error }
FilesystemFailureKindAdmitted { kind: k } =>
match k {
FilesystemAlreadyExists => FilesystemLinkTargetOccupied { path: path }
FilesystemCrossDevice => FilesystemLinkCrossDevice { source: source, path: path }
FilesystemNotFound => FilesystemLinkRefused { path: path, kind: k, error: error }
FilesystemPermissionDenied => FilesystemLinkRefused { path: path, kind: k, error: error }
FilesystemNotDirectory => FilesystemLinkRefused { path: path, kind: k, error: error }
FilesystemOtherFailure => FilesystemLinkRefused { path: path, kind: k, error: error }
}
}
}
}

data filesystem_read_outcome_adoption_standing: String ="RUNG: mitigatable. filesystem_read_outcome provides the single modeled fold from Filesystem.Read's scalar transport observation into FilesystemReadSucceeded | FilesystemReadRefused, but nothing forces callers through it. gunbc.ci_yaml_validate is the first converted consumer and preserves read refusal separately from YAML parse refusal. The raw operation remains directly consumed elsewhere, so content+success+error nonsense combinations remain writable at those sites. SUBJECT: an unconverted consumption site is a Filesystem Read call whose bound result has any success, error, or content projection outside the three arguments of filesystem_read_outcome. The call and those three projections remain after conversion because they supply the fold; adoption changes where they are consumed, not whether they exist. BASELINE measured on origin/main b21b710d5378387ae0c841f07323292c5d72faba: 92 unconverted consumption sites across 48 .dag files. REMAINDER after the first conversion: 91 unconverted consumption sites across 47 files. RE-DERIVATION: enumerate Filesystem Read assignment calls in tracked .dag source, excluding this adoption-standing data declaration so the instrument cannot count its own prose; for each bound result, classify it converted only when every success, error, and content projection is an argument of filesystem_read_outcome, otherwise classify it unconverted; count unconverted rows and distinct paths. NEXT-RUNG TRIGGER: the unconverted population reaches zero -- every Filesystem Read result projection occurs only as an argument to filesystem_read_outcome. The compiler-only filesystem_read intrinsic is a separate replacement migration and is not part of this population or this fold."

// ABSENCE IS ESTABLISHED BY A SUCCESSFUL LISTING, NEVER BY A FAILED READ. `Read` answers
Expand Down Expand Up @@ -721,6 +772,18 @@ service Filesystem {
transport file { path: "{path}", verb: "write_create_new" }
}

operation LinkCreateNew {
requires none
input { source: String, path: String }
output {
success: Bool from "write_success"
path: String from "path"
error: String from "error"
error_kind: String from "error_kind"
}
transport file { path: "{path}", verb: "link_create_new" }
}

operation WriteCreateNewWithMode {
requires none
input { path: String, content: String, mode: Int }
Expand Down
10 changes: 10 additions & 0 deletions dag/extdeps/filesystem/filesystem_rust_realization.dag
Original file line number Diff line number Diff line change
Expand Up @@ -165,5 +165,15 @@ fn rust_file_create_new_canonical_block() -> String {
"\n",
"pub ",
rust_file_write_create_new_fn_def,
"\n",
"pub ",
rust_file_link_create_new_fn_def,
)
}

// THE CREATE-ONLY LINK (extdeps.filesystem.filesystem_io LinkCreateNew): the same link(2) that
// gunbc_file_write_create_new publishes its staged file with, applied to a file the caller already
// staged. An occupied target answers AlreadyExists and a source on another filesystem answers
// CrossesDevices, both from the host; there is no copy fallback, because a link across filesystems
// is not a copy. The source is left in place for its owner to remove.
data rust_file_link_create_new_fn_def: String = "fn gunbc_file_link_create_new(source_path: &str, file_path: &str) -> std::io::Result<()> {\n std::fs::hard_link(source_path, file_path)\n}\n"
3 changes: 2 additions & 1 deletion dag/extdeps/realization/materialization_store_local.dag
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module extdeps.realization.materialization_store_local
import extdeps.filesystem.filesystem_io {
Filesystem,
FilesystemFailureKind, FilesystemNotFound, FilesystemAlreadyExists, FilesystemPermissionDenied,
FilesystemOtherFailure, FilesystemNotDirectory,
FilesystemOtherFailure, FilesystemNotDirectory, FilesystemCrossDevice,
FilesystemExactRead, FilesystemExactPathRead, FilesystemExactPathAbsent,
FilesystemExactPathUnreadable, FilesystemExactPathKindUnrecognized,
FilesystemCreateNew, FilesystemCreated, FilesystemCreateTargetOccupied, FilesystemCreateRefused,
Expand Down Expand Up @@ -137,6 +137,7 @@ fn filesystem_fault(kind: FilesystemFailureKind, error: String) -> StoreFault {
FilesystemNotFound => StoreFault { class: StoreFaultUnreachable, detail: detail }
FilesystemAlreadyExists => StoreFault { class: StoreFaultUnreachable, detail: detail }
FilesystemNotDirectory => StoreFault { class: StoreFaultUnreachable, detail: detail }
FilesystemCrossDevice => StoreFault { class: StoreFaultUnreachable, detail: detail }
FilesystemOtherFailure => StoreFault { class: StoreFaultUnreachable, detail: detail }
}
}
Expand Down
18 changes: 18 additions & 0 deletions dag/extdeps/tools/coreutils_stat.dag
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,9 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
// %a IS THE ACCESS BITS IN OCTAL WITH NO INTERPRETATION. extdeps.access.posix owns what those digits
// MEAN and reads them back through file_mode_of_octal_text; PathMode's whole job is to fetch the
// spelling.
// %d IS THE DEVICE NUMBER OF THE FILESYSTEM HOLDING THE PATH (st_dev), in decimal. Two paths with
// different numbers are on different filesystems, which is what decides whether link(2) between
// them can succeed (extdeps.filesystem.filesystem_io LinkCreateNew's cross-device refusal).
service coreutils.Stat {
operation PathOwnership {
requires none
Expand Down Expand Up @@ -78,6 +81,21 @@ service coreutils.Stat {
}
}

operation PathDevice {
requires none
input { path: NonEmptyStr }
output {
device_text: String from "stdout"
success: Bool from "exit_success"
}
readonly
transport shell { argv: ["stat", "-c", "%d", "--", "{path}"] }
exit {
0 => Unit
nonzero => String "stat could not read the path"
}
}

operation PathMode {
requires none
input { path: NonEmptyStr }
Expand Down
5 changes: 5 additions & 0 deletions dag/gunbc/ci/ci_layer_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -1064,6 +1064,11 @@ data witness_exclusion_frontier: List<WitnessExclusionRow> = [
classification: LocalRepoWetLane,
reason: excl_local_repo_wet_tempdir_write_reason,
dissolution: excl_local_repo_wet_dissolve},
WitnessExclusionRow {
pattern: "filesystem_link_create_new_wet_witness_test.dag",
classification: LocalRepoWetLane,
reason: excl_local_repo_wet_tempdir_write_reason,
dissolution: excl_local_repo_wet_dissolve},
WitnessExclusionRow {
pattern: "mtcollins1_kvm_observer_protocol_wet_witness_test.dag",
classification: LocalRepoWetLane,
Expand Down
17 changes: 17 additions & 0 deletions dag/gunbc/filesystem_link_create_new_seed_growth.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
module gunbc.filesystem_link_create_new_seed_growth

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

data filesystem_link_create_new_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "dispatch_file", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "io_error_kind_name", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_rt", decl_name: "gunbc_file_link_create_new", field: WholeDeclaration },
],
reason: "extdeps.filesystem.filesystem_io declares Filesystem.LinkCreateNew (link(2), create-only, typed already_exists and cross_device refusals). Its production consumer is a DECLARED FRONTIER, not present at this change: extdeps.realization.materialization_store_local publishing staged byte parts without a copy lands in gunbc#13095 (filesystem_io filesystem_link_create_new_consumer_frontier states the same trigger); until then the operation is consumed by its wet witnesses alone. Its one realization is authored in extdeps.filesystem.filesystem_rust_realization and generated into gunbc_file_transport_generated. The seed adds no second realization: dispatch_file gains one arm that calls that generated function, io_error_kind_name gains one ErrorKind row so a cross-device refusal is typed rather than falling to other, and v1_rt gains the emitted programs' runtime entry beside its existing gunbc_file_write_create_new sibling, which the emitter's FileLinkCreateNew lowering calls. No fallback to a copy exists on any path. Executed by test.claim.filesystem_link_create_new_wet_witness, enrolled on the wet schedule.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete the dispatch_file arm and the v1_rt entry when the interpreter and the emitted runtime both bind Filesystem operations through the modeled filesystem realization rows rather than hand-matched operation names, so LinkCreateNew reaches gunbc_file_link_create_new with no per-operation host code. The wet witness's cross-device and occupied-target reds must remain enrolled; removing them is not dissolution.",
current_boundary: "Filesystem.LinkCreateNew -> v1_interpreter dispatch_file link_create_new -> gunbc_file_transport_generated gunbc_file_link_create_new -> std::fs::hard_link"
}
2 changes: 2 additions & 0 deletions dag/gunbc/seed_growth_admission.dag
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,7 @@ import gunbc.derived_row_roster_seed_growth { derived_row_roster_seed_growth_jus
import gunbc.live_tree_stamp_detector_seed_growth { live_tree_stamp_detector_seed_growth_justification }
import gunbc.floor_cost_debt_standing_seed_growth { floor_cost_debt_standing_seed_growth_justification }
import gunbc.floor_population_projection_seed_growth { floor_population_projection_seed_growth_justification }
import gunbc.filesystem_link_create_new_seed_growth { filesystem_link_create_new_seed_growth_justification }
import gunbc.whole_corpus_compile_admission { whole_corpus_compile_seed_growth_justification }
import std.decl_ref { DeclarationRef, WholeDeclaration, NamedField, TypeParameter }
import std.disposition { Disposition }
Expand Down Expand Up @@ -310,6 +311,7 @@ fn seed_growth_justification_roster() -> List<SeedGrowthJustification> {
floor_memory_instrumentation_seed_growth_justification,
portable_value_canonical_order_seed_growth_justification,
namespace_structural_observation_bridge_seed_growth_justification,
filesystem_link_create_new_seed_growth_justification,
emit_rust_reference_derived_rows_bridge_seed_growth_justification,
namespace_baseline_seed_growth_justification,
parsed_import_statement_bridge_seed_growth_justification,
Expand Down
Loading