Repair the init model: all six of review 5089156132's findings

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

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

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<String> {
   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<String> {
 
 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)
   }
 }

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 } =>