diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index 2304e05b1fe..7d29155e145 100644 --- a/dag/extdeps/filesystem/filesystem_io.dag +++ b/dag/extdeps/filesystem/filesystem_io.dag @@ -123,6 +123,27 @@ fn admit_filesystem_entry_name(name: String) -> FilesystemEntryNameAdmission { "than the one the joined path names", ], ""), } + } else if string_contains(s: name, pattern: "\\") { + FilesystemEntryNameRefused { + name: name, + cause: join([ + "the entry name ", name, " contains a backslash, which is a path separator on some hosts ", + "this operation is implemented for -- so `..\\victim` is a parent traversal there while ", + "passing a check that rejects only `/`, which is the exact defect this carrier exists to ", + "make impossible. The grammar is the UNION over supported targets, not the one the author ", + "happens to be running on: a carrier that admits on Linux what it must refuse on Windows ", + "answers about a different subject depending on where it runs", + ], ""), + } + } else if string_contains(s: name, pattern: "\0") { + FilesystemEntryNameRefused { + name: name, + cause: join([ + "the entry name ", name, " contains a NUL, which terminates a C string -- so the name the ", + "host syscall sees is a PREFIX of the name the listing was asked about, and the two ", + "describe different subjects with no diagnostic between them", + ], ""), + } } else if string_contains(s: name, pattern: "\n") { FilesystemEntryNameRefused { name: name, @@ -328,6 +349,18 @@ fn filesystem_established_absence_detail(absence: FilesystemEstablishedAbsence) join(["no ", absence.name, " is listed in ", absence.directory], "") } +// AND THE SUBJECT IT ESTABLISHED IS THE ONLY PATH IT CAN AUTHORIZE. A consumer that takes an +// established absence AND a separately supplied target has not been authorized by the token at all: +// the absence is about `directory + name`, the actuation is about whatever String arrived beside it, +// and nothing joins them. That is a real defect and it was found in review on gunbc#10026 -- +// `ScmInitMayCreate(_)` discarded the token and wrote to an independent `path`, so an absence +// established for one subject could coexist with a write to another. Deriving the path HERE, from +// the carrier's own fields, is what makes consuming the token mean something: there is no second +// target to disagree with. +fn filesystem_established_absence_path(absence: FilesystemEstablishedAbsence) -> String { + join([absence.directory, "/", absence.name], "") +} + data filesystem_absence_establishment_adoption_standing: String = "RUNG: structurally guaranteed for the consumers that route through filesystem_file_observation, on the source-to-.dag acceptance path only, and MITIGATABLE NOWHERE ELSE -- the raw Filesystem.Read and Filesystem.List operations stay callable, so a module that has not adopted the carrier can still write the conflation. This row states the unconverted population at identity grain rather than as a count, because a count is not a plan and a one-sided ratchet over a number measured on the current tree is the oracle section 5 rejects. SUBJECT: a site that concludes ABSENCE, NOT-PRESENT or a dropped element from a FAILED read or a FAILED boolean path test, rather than from a listing that succeeded. It is not every Filesystem.Read consumer -- most read a file they already know exists, and those are the separate filesystem_read_outcome adoption population above. ENUMERATED SITES, each one read rather than pattern-matched, on origin/main at the head this row lands against, with the two converted by the change that lands this row already removed (gunbc.roadmap_verification_receipt current_verification_selection_observe and exact_verification_receipt_source_read, and gunbc.devboot.build read_text_file): gunbc.host_effect_nbd_proxy_serve host_effect_nbd_proxy_serve_read_session_token (read refusal answers Absent, and an empty content does too); gunbc.fleet_converge_plan_cli observe_cap_members_wet (a cap member whose dropin could not be read is DROPPED from the observed list, so the converge plan is computed over a silently narrowed population); v2.workflow.product_receipt_stage run_product_receipt_stage (an unreadable manifest answers ArtifactIdentityAbsent { ProducerReportedNoArtifact }, attributing to the producer a report it never made); tools.merge_admission_walk read_tested_subject and read_floor_receipt (a read refusal answers the Optional's absent arm); gunbc.codex_supervised_turn codex_supervised_turn_generation_observation (GenerationAbsent is concluded from shell.Test.IsFile answering false. THIS ROW IS CLASSIFIED FROM THE PRODUCER RATHER THAN FROM THE CALL SITE, on a caution from the lane that shipped this defect today: a predicate whose job is to answer the presence question would not belong here. extdeps.shell Test.IsFile is `test -f` with its own declared exit table reading `1 => Path is missing or not a regular file`, so ONE exit code carries missing, wrong-kind, and -- since `test -f` is false when the parent directory cannot be searched -- could-not-look. It answers false on an unreadable-but-present path, so it is the same defect with a different producer, and it is the construction gunbc.fabric_cell_acquire retired for exactly this reason); tools.opaque_realization_census declaration_body_standing (a file that could not be read leaves the fold state unchanged, so it is indistinguishable from a file that did not hold the declaration). WHAT IS DELIBERATELY NOT ON THE LIST: gunbc.roadmap_belt_actuate belt_read_or_empty, whose collapse is scoped and argued in belt_read_or_empty_scope_note -- both branches take the same action at every remaining caller -- and gunbc.fabric_cell_acquire, which already establishes absence from the parent enumeration through its own four-state observation and would gain nothing but a second spelling. MONOTONE DIRECTION: the roster above may only shrink. A row leaves it when the site routes through filesystem_file_observation or filesystem_entry_presence, or when the site is deleted; a NEW site of this shape is a defect to repair rather than a row to add. NEXT-RUNG TRIGGER, and it names the capability rather than an artifact: the raw List and Read result projections cease to be reachable outside this module's folds, so a consumer cannot spell the conflation at all -- at which point the enumeration above has no subject and this row is deleted. That is the same trigger filesystem_read_outcome_adoption_standing carries, one question further in: it asks that every read projection be folded, this asks that every ABSENCE be established." // WriteCreateNew: CREATE-ONLY IS A DIFFERENT FACT FROM OWNER-ONLY, and this annotation sits here diff --git a/dag/gunbc/scm/init.dag b/dag/gunbc/scm/init.dag index 1c6fe3516df..f39d031d4bf 100644 --- a/dag/gunbc/scm/init.dag +++ b/dag/gunbc/scm/init.dag @@ -69,7 +69,15 @@ import gunbc.scm.repository_envelope { RepositoryDecoded, RepositoryDecodeRefused } -import gunbc.scm.repository_save { RepositorySave, create_repository } +import gunbc.scm.repository_save { + RepositorySave, + RepositorySaved, + RepositorySaveRefusedByCodec, + RepositoryFileUnwritable, + RepositoryWriteByteCountUnrepresentable, + create_repository_at_absence, +} +import std.measure { ByteSize } // THE ARMS ARE THE ANSWER. There is no `initialized: Bool` beside a save outcome: a value whose // flag disagreed with its shape would have a spelling, and the refusals are distinguished because @@ -93,8 +101,19 @@ type ScmInitRefusal // operator's next action differs -- one path already IS a repository, one holds something else that // would be destroyed, one could not be observed at all, and one was never a valid // entry name. +// AND `ScmInitialized` MAY NOT CONTAIN A FAILED CREATION. It used to carry the whole +// `RepositorySave`, whose arms include codec refusal, file-unwritable and unrepresentable byte +// count -- so `ScmInitialized { save: RepositoryFileUnwritable { .. } }` was a spellable value that +// told every consumer matching the outer arm that initialization HAPPENED when it did not. The +// renderer noticed the nested failure and exited nonzero, which repaired the message and not the +// carrier: a consumer reading the arm rather than re-folding its payload was simply lied to, on the +// ordinary write-refusal path. Found in review on gunbc#10026. +// +// The outer arm is now the answer by itself. `ScmInitialized` carries only what a SUCCESSFUL create +// produced, and every other save arm reaches `ScmInitWriteRefused`, which asserts nothing. type ScmInitOutcome - = ScmInitialized { save: RepositorySave } + = ScmInitialized { path: String, written: ByteSize } + | ScmInitWriteRefused { save: RepositorySave } | ScmInitRefused { cause: ScmInitRefusal } // WHAT THE OBSERVATION DECIDES, WITHOUT PERFORMING ANYTHING. `ScmInitMayCreate` carries the @@ -158,8 +177,23 @@ fn initialize_repository_at( path: path, ) { ScmInitDecided { cause: c } => ScmInitRefused { cause: c } - ScmInitMayCreate(_) => - ScmInitialized { save: create_repository(path: path, repo: empty_repository()) } + ScmInitMayCreate(absence) => init_outcome_of_save( + save: create_repository_at_absence(absence: absence, repo: empty_repository()) + ) + } +} + +// THE SAVE RESULT IS FOLDED, NOT WRAPPED. This is a total match over all four RepositorySave arms, +// and only RepositorySaved may construct ScmInitialized. A mutation that routes any other arm to +// ScmInitialized changes what the outer arm ASSERTS, which is exactly the edit the claims enrolled +// beside this function hold red. +fn init_outcome_of_save(save: RepositorySave) -> ScmInitOutcome { + match save { + RepositorySaved { path: p, written: w } => ScmInitialized { path: p, written: w } + RepositorySaveRefusedByCodec { path: _, cause: _ } => ScmInitWriteRefused { save: save } + RepositoryFileUnwritable { path: _, error: _ } => ScmInitWriteRefused { save: save } + RepositoryWriteByteCountUnrepresentable { path: _, reported: _ } => + ScmInitWriteRefused { save: save } } } @@ -169,10 +203,31 @@ fn initialize_repository_at( // only_an_established_absence_may_create each fail under exactly that edit). Routing the DISAGREEMENT // arm there is not authorable at all: ScmInitMayCreate carries a FilesystemEstablishedAbsence, which // is sole_constructor and minted only by the substrate fold from a listing that succeeded, so no arm -// can manufacture the permission to write. The rung is therefore split and stated rather than -// averaged: structurally impossible for fabricating a write permission (rung 4, no constructor), -// and mechanically preventable for routing a REAL absence to the wrong outcome (rung 2, held by the -// claims above). +// can manufacture the permission to write. +// +// THAT CLAIM WAS OVERSTATED UNTIL THIS CHANGE, AND THE CORRECTION IS THE POINT. The token being +// unforgeable bought nothing while the actuation ignored it: this function matched +// `ScmInitMayCreate(_)`, discarded the absence, and wrote to an independently supplied `path`. An +// absence established for one subject could therefore sit beside a write to a DIFFERENT one, and no +// mutation to the write target went red. Four external reviews read the sole_constructor and +// endorsed a rung-4 authorization claim; the designated reviewer read the MATCH and found the token +// was never consumed. A capability that is carried past its actuation authorizes nothing. +// +// The absence is now CONSUMED: create_repository_at_absence derives its target from the carrier's +// own directory and name, so there is no second target to disagree with. +// +// THE RUNG, SPLIT AND STATED RATHER THAN AVERAGED, AND SMALLER THAN IT WAS CLAIMED TO BE: +// - fabricating a write permission out of nothing: structurally impossible (rung 4, no +// constructor for FilesystemEstablishedAbsence outside the substrate fold); +// - authorizing a write to a subject the absence was NOT established for: structurally impossible +// for THIS caller (rung 4, the path has one derivation and no independent target), and NOT a +// property of create_repository, which still takes a bare String for its own callers; +// - routing a REAL absence to the wrong outcome: mechanically preventable (rung 2, held by the +// claims above). +// +// AND THE RACE ITSELF IS NOT ON THAT LADDER AT ALL. No preflight closes a TOCTOU; O_EXCL does. The +// observation decides WHAT TO TELL THE OPERATOR and which subject may be written; the exclusive +// create is the wall against an actor that arrives between the two. // // THE DECISION IS ITS OWN FUNCTION SO IT CAN BE WITNESSED WITHOUT A FILESYSTEM. Every arm below is a // choice about whether bytes may be written, and while it lived inside the effectful entry the only diff --git a/dag/gunbc/scm/render.dag b/dag/gunbc/scm/render.dag index 3b3ccc2c0b4..6687a264cda 100644 --- a/dag/gunbc/scm/render.dag +++ b/dag/gunbc/scm/render.dag @@ -52,6 +52,7 @@ import gunbc.scm.repository_load { repository_load_refusal_lines } import gunbc.scm.init { ScmInitOutcome, ScmInitialized, + ScmInitWriteRefused, ScmInitRefused, ScmInitRefusal, ScmInitRepositoryPresent, @@ -271,7 +272,9 @@ fn scm_save_cli_response( // foreign file at that path is a choice about someone else's bytes. fn scm_init_lines(outcome: ScmInitOutcome) -> List { match outcome { - ScmInitialized { save: save } => repository_save_lines(save: save) + ScmInitialized { path: p, written: _ } => + [concat("initialized repository at ", p)] + ScmInitWriteRefused { save: save } => repository_save_lines(save: save) ScmInitRefused { cause: cause } => scm_init_refusal_lines(cause: cause) } } @@ -303,7 +306,8 @@ fn scm_init_refusal_lines(cause: ScmInitRefusal) -> List { fn scm_init_exit(outcome: ScmInitOutcome) -> ProcessExit { match outcome { - ScmInitialized { save: save } => scm_save_exit(save: save) + ScmInitialized { path: _, written: _ } => ExitSuccess + ScmInitWriteRefused { save: save } => scm_save_exit(save: save) ScmInitRefused { cause: cause } => scm_init_refusal_exit(cause: cause) } } diff --git a/dag/gunbc/scm/repository_save.dag b/dag/gunbc/scm/repository_save.dag index cbf11d4f22e..212e0400010 100644 --- a/dag/gunbc/scm/repository_save.dag +++ b/dag/gunbc/scm/repository_save.dag @@ -43,6 +43,7 @@ module gunbc.scm.repository_save import std.types { String, Int } import extdeps.filesystem.filesystem_io +import extdeps.filesystem.filesystem_io { FilesystemEstablishedAbsence, filesystem_established_absence_path } import extdeps.languages.json.emit { serialize_json } import std.measure { ByteSize, byte_size } import std.checked_arithmetic { nat_magnitude } @@ -102,6 +103,24 @@ type RepositorySave // remedy is the same -- the bytes are not yours to write and the host says why -- and the error text // is the host's own. A second arm would be a second spelling of one outcome (section 3), and one that // classified the cause from the error TEXT would be a heuristic standing in for an observation. +// THE CREATE THAT AN ESTABLISHED ABSENCE AUTHORIZES, AND THE ONLY ONE IT CAN. +// +// create_repository below takes a bare String, which is right for its own subject -- a caller that +// has some other reason to create at a path may use it. It is the WRONG entry for a caller whose +// permission came from an absence, because taking the token and a separate path lets the two name +// different subjects and nothing detects it. Review on gunbc#10026 found exactly that: init matched +// ScmInitMayCreate(_), threw the token away, and wrote to an independently computed path. +// +// So the absence-authorized create derives its target from the token itself. There is no second +// target to disagree with, which is the difference between a capability that is CONSUMED and one +// that is merely carried past the actuation. +fn create_repository_at_absence( + absence: FilesystemEstablishedAbsence, + repo: RepositoryEnvelope, +) -> RepositorySave { + create_repository(path: filesystem_established_absence_path(absence: absence), repo: repo) +} + fn create_repository(path: String, repo: RepositoryEnvelope) -> RepositorySave { match encode_repository_checked(repo: repo) { RepositoryEncodeRefused { cause: cause } => diff --git a/dag/test/claim/scm/scm_cli_witness_test.dag b/dag/test/claim/scm/scm_cli_witness_test.dag index ebe49fe5074..c93a4341d96 100644 --- a/dag/test/claim/scm/scm_cli_witness_test.dag +++ b/dag/test/claim/scm/scm_cli_witness_test.dag @@ -33,9 +33,25 @@ import gunbc.scm.init { ScmInitMayCreate, ScmInitDecided, ScmInitialized, + ScmInitWriteRefused, scm_init_decision, + init_outcome_of_save, initialize_repository } +import gunbc.scm.repository_save { + RepositorySave, + RepositorySaved, + RepositoryFileUnwritable, + RepositoryWriteByteCountUnrepresentable, +} +import gunbc.scm.repository_envelope { + RepositoryEncodeOutcome, + RepositoryEncoded, + RepositoryEncodeRefused, + encode_repository_checked, +} +import extdeps.languages.json.emit { serialize_json } +import std.measure { byte_size } import extdeps.filesystem.filesystem_io { FilesystemDirectoryListed, FilesystemDirectoryListingRefused, @@ -50,7 +66,8 @@ import extdeps.filesystem.filesystem_io { filesystem_file_observation, admit_filesystem_entry_name, FilesystemEntryNameAdmitted, - FilesystemEntryNameRefused + FilesystemEntryNameRefused, + filesystem_established_absence_path } // THE BYTES PIN THE CAPABILITY. This is the same expected string the render-level witness pins for @@ -163,15 +180,28 @@ test fn an_init_refusal_never_exits_success() -> Bool { && wire_refuses(r: scm_init_response( outcome: ScmInitRefused { cause: ScmInitPathUnobserved { path: "repo.json", cause: "the directory could not be listed" } } )) + && wire_refuses(r: scm_init_response( + outcome: ScmInitRefused { cause: ScmInitNameNotAnEntry { name: "../victim", cause: "it is a path, not one child" } } + )) } -test fn the_three_init_refusals_render_differently() -> Bool { +// THE POPULATION IS FOUR, AND IT SAYS SO. ScmInitNameNotAnEntry became a fourth refusal arm and +// these claims still enumerated three, so the direct admission test proved the name refuses EARLY +// while nothing proved it reaches an operator as its own answer. A claim that names a population +// has to move when the population does, or it silently covers a shrinking fraction of its subject. +// Review 5089156132 finding 5.3 on gunbc#10026. +test fn the_four_init_refusals_render_differently() -> Bool { let present = wire_bytes(r: scm_init_response(outcome: ScmInitRefused { cause: ScmInitRepositoryPresent { path: "repo.json" } })) let foreign = wire_bytes(r: scm_init_response(outcome: ScmInitRefused { cause: ScmInitForeignFilePresent { path: "repo.json" } })) let unobserved = wire_bytes(r: scm_init_response( outcome: ScmInitRefused { cause: ScmInitPathUnobserved { path: "repo.json", cause: "the directory could not be listed" } } )) + let not_an_entry = wire_bytes(r: scm_init_response( + outcome: ScmInitRefused { cause: ScmInitNameNotAnEntry { name: "../victim", cause: "it is a path, not one child" } } + )) present != foreign && foreign != unobserved && present != unobserved && present != "" + && not_an_entry != present && not_an_entry != foreign && not_an_entry != unobserved + && not_an_entry != "" } // THE UNOBSERVED ARM CARRIES THE HOST'S CAUSE THROUGH. A refusal that dropped it would tell the @@ -257,6 +287,30 @@ test fn two_disagreeing_observations_do_not_authorize_a_write() -> Bool { == "unobserved" } +// AND THE VALID REPOSITORY IS PINNED TO ITS OWN ARM, NOT MERELY AWAY FROM THE WRITE ARM. This +// asserted `!= may_create` for a decodable repository, which is satisfied by mapping EVERY present +// file -- valid repository included -- to ScmInitForeignFilePresent. That would tell an operator a +// foreign file is in the way of their own repository, and the claim would have stayed green. The +// two present arms are one fact apart (the same listing and read, differing only in whether the +// content decodes), so pinning each to its own arm is what makes the classification evidence rather +// than a not-the-write-arm check. Review 5089156132 finding 5.2 on gunbc#10026. +// THE VALID-REPOSITORY FIXTURE IS THE WRITER'S OWN OUTPUT, not a hand-authored literal. A literal +// here is a second authority for the repository wire format (DESIGN section 3): it agrees with the +// codec only for as long as someone keeps retyping it, and the version it drifts to is silently +// classified `foreign_present` -- the classifier reporting a repository this program just wrote as +// a foreign file. Deriving the bytes from `encode_repository_checked` makes writer and classifier +// agree BY EXECUTION, so a codec change that breaks the round trip turns this claim red at the +// change rather than at the next hand edit. +// +// A refused encode yields "" here, which decodes as foreign rather than as a repository, so the +// refusal arm fails this claim instead of vacuously satisfying it. +fn saved_repository_bytes() -> String { + match encode_repository_checked(repo: empty_repository()) { + RepositoryEncodeRefused { cause: _ } => "" + RepositoryEncoded { value: v } => serialize_json(v: v) + } +} + test fn present_bytes_do_not_authorize_a_write_and_are_classified() -> Bool { decide(o: observe(listed: true, entries: "repo.json", read_ok: true, content: "not json at all")) == "foreign_present" @@ -264,8 +318,8 @@ test fn present_bytes_do_not_authorize_a_write_and_are_classified() -> Bool { listed: true, entries: "repo.json", read_ok: true, - content: "{\"format\":\"gunbc-scm-repository-v2\"}", - )) != "may_create" + content: saved_repository_bytes(), + )) == "repository_present" } // ------------------------------------------------------------------------------------------------ @@ -292,6 +346,18 @@ test fn a_name_that_is_not_one_child_of_the_directory_is_refused() -> Bool { && !name_admits(n: "../victim") } +// THE GRAMMAR IS THE UNION OVER SUPPORTED TARGETS, NOT THE AUTHOR'S HOST. Review on gunbc#10026 +// found this carrier rejecting `/` while admitting `\\` and NUL, with WriteCreateNew implemented on +// non-Unix rather than refusing there -- so `..\\victim` is a parent traversal on Windows that +// passes a check named for making traversal impossible, and a NUL makes the syscall see a PREFIX of +// the name the listing was asked about. Both are the one-name-two-subjects defect the carrier +// exists to close, reached by spellings the first cut did not model. +test fn a_name_carrying_another_hosts_separator_or_a_nul_is_refused() -> Bool { + !name_admits(n: "..\\victim") + && !name_admits(n: "subdir\\repo.json") + && !name_admits(n: "repo.json\0.bak") +} + // THE NEWLINE CASE IS THIS MODULE'S OWN, because the delimiter belongs to Filesystem.List's encoding: // a name carrying one can make the membership test answer about an entry that is not present. test fn a_name_carrying_the_listing_delimiter_is_refused() -> Bool { @@ -304,7 +370,8 @@ test fn a_name_carrying_the_listing_delimiter_is_refused() -> Bool { // that is exactly the property being claimed. test fn a_refused_name_refuses_before_any_filesystem_operation() -> Bool { match initialize_repository(directory: "d", name: "../victim") { - ScmInitialized { save: _ } => false + ScmInitialized { path: _, written: _ } => false + ScmInitWriteRefused { save: _ } => false ScmInitRefused { cause: c } => match c { ScmInitNameNotAnEntry { name: _, cause: _ } => true @@ -314,3 +381,57 @@ test fn a_refused_name_refuses_before_any_filesystem_operation() -> Bool { } } } + +// A FAILED SAVE MAY NOT WEAR THE SUCCESS ARM. This is the discriminating control for the defect +// review found on gunbc#10026: ScmInitialized used to carry the whole RepositorySave, so +// `ScmInitialized { save: RepositoryFileUnwritable { .. } }` was spellable and told every consumer +// matching the outer arm that initialization happened. init_outcome_of_save is a total fold and only +// RepositorySaved may reach ScmInitialized; routing ANY other arm there turns these red. +// +// It is driven over the save arms directly rather than through the effectful entry, because the +// property is about the FOLD and a SubstrateInputsOnly witness cannot make a real write fail. +fn init_outcome_claims_success(save: RepositorySave) -> Bool { + match init_outcome_of_save(save: save) { + ScmInitialized { path: _, written: _ } => true + ScmInitWriteRefused { save: _ } => false + ScmInitRefused { cause: _ } => false + } +} + +test fn a_saved_repository_is_the_only_initialized_outcome() -> Bool { + init_outcome_claims_success( + save: RepositorySaved { path: "/d/repo.json", written: byte_size(count: 12) } + ) +} + +test fn no_failed_save_arm_reaches_the_initialized_outcome() -> Bool { + !init_outcome_claims_success( + save: RepositoryFileUnwritable { path: "/d/repo.json", error: "Permission denied" } + ) + && !init_outcome_claims_success( + save: RepositoryWriteByteCountUnrepresentable { path: "/d/repo.json", reported: 0 - 1 } + ) +} + +// THE ABSENCE NAMES THE SUBJECT IT AUTHORIZES. The second review defect: the token was matched as +// `_` and the write actuated on an independently supplied path, so evidence about one directory +// entry could sit beside a create against another. The path now has ONE derivation, from the +// carrier's own fields, and this pins it -- an absence for directory d and name n authorizes +// exactly d/n and nothing else. +test fn an_established_absence_derives_the_only_path_it_authorizes() -> Bool { + let listed = filesystem_listing_observation( + directory: "/d", success: true, entries: "other.json", error: "" + ) + match filesystem_file_observation( + listing: listed, + name: "repo.json", + path: "/d/repo.json", + read: filesystem_read_outcome(content: "", success: false, error: "No such file") + ) { + FilesystemFileAbsent(absence) => + filesystem_established_absence_path(absence: absence) == "/d/repo.json" + FilesystemFileRead { path: _, content: _ } => false + FilesystemFileIndeterminate { cause: _ } => false + FilesystemFileObservationsDisagree { path: _, cause: _ } => false + } +} diff --git a/src/v1/05_emit_rust.dag b/src/v1/05_emit_rust.dag index 70c334b8041..d53e50c5d54 100644 --- a/src/v1/05_emit_rust.dag +++ b/src/v1/05_emit_rust.dag @@ -14458,7 +14458,23 @@ data file_list_match_expr: String = "match std::fs::read_dir(&file_path) {\n data file_write_expr: String = "{\n let payload_bytes = content.len() as i64;\n match std::fs::write(&file_path, content.as_bytes()) {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(write_err) => (false, String::new(), format!(\"{}\", write_err), 0i64),\n }\n};" -data file_write_create_new_expr: String = "{\n let payload_bytes = content.len() as i64;\n let create_new_result = (|| -> std::io::Result<()> {\n use std::io::Write;\n let mut create_new_file = std::fs::OpenOptions::new().write(true).create_new(true).open(&file_path)?;\n create_new_file.write_all(content.as_bytes())?;\n Ok(())\n })();\n match create_new_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(create_new_err) => (false, String::new(), format!(\"{}\", create_new_err), 0i64),\n }\n};" +// THE EMITTED REALIZATION PUBLISHES ONLY COMPLETE CONTENT, exactly as the interpreter helper does, +// and this row exists because review 5089156132 on gunbc#10069 found the two had DIVERGED. The +// interpreter's v1_interpreter::write_file_create_new was repaired to stage-then-link while THIS +// expression still spelled open-then-write against the target, so a failed emitted write could +// still leave a partial repository while reporting failure -- the same fabricated-repository defect, +// surviving in the realization the tests do not execute. +// +// That is the shape DESIGN section 2 and 3 forbid: one fact with two authorities, where repairing +// the reachable one leaves the other lying. It is also section 4b rung honesty -- the class's rung +// is the MINIMUM across its paths, and a fix on the interpreted path does not raise the emitted one. +// +// These two spellings are still two spellings, which is the residue this row does not close: the +// emitted program is standalone Rust and cannot call the seed's helper, so nothing but review holds +// them in step today. NEXT-RUNG TRIGGER, naming the capability rather than an artifact: an emitted +// file-transport realization derived from ONE authority that both the seed and the emitted program +// consume, at which point the divergence has no spelling and this note has no subject. +data file_write_create_new_expr: String = "{\n let payload_bytes = content.len() as i64;\n let create_new_result = (|| -> std::io::Result<()> {\n use std::io::Write;\n let staging_path = format!(\"{}.gunbc-create-{}\", file_path, std::process::id());\n let mut staged = std::fs::OpenOptions::new().write(true).create_new(true).open(&staging_path)?;\n if let Err(staging_err) = staged.write_all(content.as_bytes()) {\n let _ = std::fs::remove_file(&staging_path);\n return Err(staging_err);\n }\n if let Err(sync_err) = staged.sync_all() {\n let _ = std::fs::remove_file(&staging_path);\n return Err(sync_err);\n }\n drop(staged);\n let published = std::fs::hard_link(&staging_path, &file_path);\n let _ = std::fs::remove_file(&staging_path);\n published\n })();\n match create_new_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(create_new_err) => (false, String::new(), format!(\"{}\", create_new_err), 0i64),\n }\n};" data file_write_owner_only_expr: String = "{\n let payload_bytes = content.len() as i64;\n let owner_only_result = (|| -> std::io::Result<()> {\n #[cfg(unix)]\n {\n use std::io::Write;\n use std::os::unix::fs::OpenOptionsExt;\n let mut owner_only_file = std::fs::OpenOptions::new().write(true).create_new(true).mode(0o600).open(&file_path)?;\n owner_only_file.write_all(content.as_bytes())?;\n return Ok(());\n }\n #[cfg(not(unix))]\n {\n return Err(std::io::Error::new(std::io::ErrorKind::Unsupported, \"write_owner_only refused: owner-only mode-at-creation is unavailable on this platform\"));\n }\n })();\n match owner_only_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(owner_only_err) => (false, String::new(), format!(\"{}\", owner_only_err), 0i64),\n }\n};" diff --git a/src/v1/stage0/src/v1_compiler_emit_rust.rs b/src/v1/stage0/src/v1_compiler_emit_rust.rs index 9d1de48aa8f..0c5e2d23e03 100644 --- a/src/v1/stage0/src/v1_compiler_emit_rust.rs +++ b/src/v1/stage0/src/v1_compiler_emit_rust.rs @@ -35243,7 +35243,7 @@ pub fn file_write_expr() -> String { pub fn file_write_create_new_expr() -> String { thread_local! { static CACHED: String = { - "{\n let payload_bytes = content.len() as i64;\n let create_new_result = (|| -> std::io::Result<()> {\n use std::io::Write;\n let mut create_new_file = std::fs::OpenOptions::new().write(true).create_new(true).open(&file_path)?;\n create_new_file.write_all(content.as_bytes())?;\n Ok(())\n })();\n match create_new_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(create_new_err) => (false, String::new(), format!(\"{}\", create_new_err), 0i64),\n }\n};".to_string() + "{\n let payload_bytes = content.len() as i64;\n let create_new_result = (|| -> std::io::Result<()> {\n use std::io::Write;\n let staging_path = format!(\"{}.gunbc-create-{}\", file_path, std::process::id());\n let mut staged = std::fs::OpenOptions::new().write(true).create_new(true).open(&staging_path)?;\n if let Err(staging_err) = staged.write_all(content.as_bytes()) {\n let _ = std::fs::remove_file(&staging_path);\n return Err(staging_err);\n }\n if let Err(sync_err) = staged.sync_all() {\n let _ = std::fs::remove_file(&staging_path);\n return Err(sync_err);\n }\n drop(staged);\n let published = std::fs::hard_link(&staging_path, &file_path);\n let _ = std::fs::remove_file(&staging_path);\n published\n })();\n match create_new_result {\n Ok(()) => (true, String::new(), String::new(), payload_bytes),\n Err(create_new_err) => (false, String::new(), format!(\"{}\", create_new_err), 0i64),\n }\n};".to_string() }; } CACHED.with(|c: &String| c.clone()) diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index 7027b35425d..c5110eef8a5 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -12808,12 +12808,57 @@ fn write_file_owner_only(path: &str, content: &[u8]) -> std::io::Result<()> { /// EXISTENCE are independent facts; a caller that obtained create-only from it would silently also /// get 0600, and would break if owner-only ever stopped needing O_EXCL. This is portable and sets no /// mode, because setting one would be the same conflation in reverse. +/// THE TARGET IS PUBLISHED ONLY WHEN ITS CONTENT IS COMPLETE. +/// +/// The first cut of this was `create_new(true).open(path)` followed by `write_all`, and review on +/// gunbc#10026 found the state that construction cannot describe: if the open SUCCEEDS and the +/// write then fails, the target has already been created and holds zero or partial bytes. The +/// helper returned an ordinary error, the transport reported `success=false, bytes_written=0`, and +/// the caller classified it as merely unwritable -- so the model said the create did not happen +/// while a new, incomplete artifact sat at the path. That collapses "nothing was created" into "a +/// truncated repository now exists", which is a worse lie than the overwrite race this operation +/// was added to close: the original race could destroy someone else's bytes, and this one +/// FABRICATES a repository nobody wrote. +/// +/// Two dispositions are not modeled here, because a construction that cannot reach the bad state +/// is available (DESIGN section 4b: construction over proof, proof over validation). Content is +/// written to a sibling temporary that is itself created with O_EXCL, and the target name is +/// claimed by `hard_link`, which FAILS IF THE TARGET EXISTS -- so exclusivity is preserved by the +/// publish step rather than by the open. Every failure before the link leaves the target absent, +/// which is exactly what the operation reports. +/// +/// The temporary is removed on every path. Its removal failure is deliberately NOT propagated: it +/// leaves a stray sibling and does not affect what the target is, and reporting it as a write +/// failure would say the repository was not created when it was. fn write_file_create_new(path: &str, content: &[u8]) -> std::io::Result<()> { use std::fs::OpenOptions; use std::io::Write; - let mut file = OpenOptions::new().write(true).create_new(true).open(path)?; - file.write_all(content)?; - Ok(()) + + let temp = format!("{path}.gunbc-create-{}", std::process::id()); + + // The temporary is exclusive too, so two concurrent creators cannot share one staging file. + // `?` rather than a match: this arm creates nothing, so there is no staging file to clean up -- + // which is exactly why it is the one failure below that does NOT remove_file. The emitted + // realization already spells it `?`, so this also stops the two spellings differing over a + // difference that was never semantic. + let mut file = OpenOptions::new() + .write(true) + .create_new(true) + .open(&temp)?; + if let Err(e) = file.write_all(content) { + let _ = std::fs::remove_file(&temp); + return Err(e); + } + if let Err(e) = file.sync_all() { + let _ = std::fs::remove_file(&temp); + return Err(e); + } + drop(file); + + // hard_link refuses an existing target, which is where this operation's exclusivity now lives. + let published = std::fs::hard_link(&temp, path); + let _ = std::fs::remove_file(&temp); + published } // ------------------------------------------------------------------------------------------------ @@ -12845,6 +12890,70 @@ mod write_file_create_new_tests { std::fs::remove_dir_all(&dir).ok(); } + // THE POST-OPEN FAILURE CONTROL, and it took two attempts to make it real. + // + // Review on gunbc#10026 found that neither existing cell observes a failure AFTER the target + // name would have been claimed -- exactly where the old open-then-write construction left a + // created-but-incomplete file while reporting that nothing was created. + // + // THE FIRST ATTEMPT WAS A DECORATION AND IS RECORDED HERE SO IT IS NOT REBUILT. It put a + // DIRECTORY at the target and asserted the target was untouched. Measured against the old + // construction, it PASSED: `create_new` fails at the OPEN when the name exists, so nothing was + // ever created and the assertion was satisfied by the defect. A check that cannot go red on the + // fault it names is worse than absent (DESIGN section 4b) because it gets cited as coverage. + // + // THIS ONE REACHES THE FAULT. RLIMIT_FSIZE makes `write_all` fail with EFBIG on a path that is + // ABSENT, so the create genuinely succeeds and the write genuinely fails -- the one ordering + // that distinguishes the two constructions. It runs in a forked child because the limit and the + // SIGXFSZ disposition are process-wide and this binary runs tests concurrently; the parent only + // reads the filesystem afterwards. + #[test] + fn a_write_failure_after_creation_leaves_no_target_behind() { + let dir = + std::env::temp_dir().join(format!("gunbc-create-new-efbig-{}", std::process::id())); + std::fs::create_dir_all(&dir).expect("temp dir"); + let target = dir.join("repo.json"); + let target_s = target.to_str().unwrap().to_string(); + + // 64 bytes allowed, 4 KiB written: the create succeeds, the write cannot. + let content = vec![b'x'; 4096]; + + let pid = unsafe { libc::fork() }; + assert!(pid >= 0, "fork failed"); + if pid == 0 { + unsafe { + libc::signal(libc::SIGXFSZ, libc::SIG_IGN); + let lim = libc::rlimit { + rlim_cur: 64, + rlim_max: 64, + }; + libc::setrlimit(libc::RLIMIT_FSIZE, &lim); + } + let _ = super::write_file_create_new(&target_s, &content); + unsafe { libc::_exit(0) }; + } + let mut status: libc::c_int = 0; + unsafe { libc::waitpid(pid, &mut status, 0) }; + + // THE LOAD-BEARING ASSERTION. Under the old construction the target was created by the open + // and survived the failed write as a zero-or-partial file -- a repository nobody wrote. + // Publishing only when the content is complete means there is nothing at the target at all. + assert!( + !target.exists(), + "a write that failed after creation must leave NO target behind" + ); + let strays: Vec = std::fs::read_dir(&dir) + .expect("list") + .filter_map(|e| e.ok()) + .map(|e| e.file_name().to_string_lossy().to_string()) + .collect(); + assert!( + strays.is_empty(), + "no staging temporary may survive either: {strays:?}" + ); + std::fs::remove_dir_all(&dir).ok(); + } + #[test] fn create_new_writes_when_nothing_is_there() { let dir = std::env::temp_dir().join(format!("gunbc-create-new-ok-{}", std::process::id()));