Close the SCM init TOCTOU with a modeled create-only write

[gunbai-bot]

Closes review 5085479276's finding 1 on #9864 — the one finding that could not be fixed inside that PR, because the fix needs a new file-transport verb in a load-bearing pipeline stage. The operator ruled it into its own PR so the emit-stage change is judged on its own merits.

The defect

initialize_repository established an absence from a directory listing and then called save_repository, which writes unconditionally. The decision was honest; the write was simply not conditioned on it. An actor creating the file between the two makes init truncate exactly the bytes it advertises that it refuses to touch.

Why a better check cannot fix it

Check-then-write is two acts with a gap, and re-observing only makes the gap smaller. The existence test and the creation have to be one act — which is a property of open(2) with O_CREAT|O_EXCL, not something a fold over two modeled operations can express. So the substrate gains the operation rather than the caller gaining a check. Construction over validation (§5) at a boundary where validation structurally cannot win.

• extdeps.filesystem.filesystem_io — WriteCreateNew
• src/v1/05_emit.dag / 05_emit_rust.dag — FileWriteCreateNew verb
• v1_interpreter — one hand-authored write_file_create_new
• gunbc.scm.repository_save — create_repository beside save_repository. Persisting a repository that exists and creating one that must not exist are different subjects; the unconditional write stays correct for the first.

Not WriteOwnerOnly, which already calls create_new

Its O_EXCL is incidental to setting a mode at creation — meaningless on a path that already exists — and is not a contract. Owner-only mode and create-only existence are independent facts. A caller taking create-only from it would silently also take 0600, and would break the day owner-only stopped needing O_EXCL. Reusing a realization detail in place of a modeled fact is the inversion §3 names; the review rejected it explicitly.

The refusal does not classify itself, on purpose

It carries the host's error verbatim and does not report whether the cause was "already existed" or "permission denied". The transport's channels cannot separate them, and deciding it by matching the error text would be a heuristic standing in for an observation (§5). The caller learns what it needs in order to refuse, and does not learn a classification nothing measured. That gap carries its own next-rung trigger rather than being papered over.

Evidence

The mutation is the original defect, not an invented one: replacing create_new with create+truncate — literally what the code did before — takes the refusal test red while the positive control stays green.

test	mutant	fixed
create_new_refuses_a_path_that_already_exists_and_leaves_its_bytes	FAIL	PASS
create_new_writes_when_nothing_is_there	PASS	PASS

The load-bearing assertion is that the existing bytes survive, not that an error is returned. A write that truncated and then reported failure would satisfy a weaker test and still have destroyed the file — that distinction is the whole finding.

Also re-lands, on top of the primitive, the work cut from #9864 because it had no other consumer: the FilesystemEntryName admission carrier and the four init-decision witnesses.

Seed growth is receipted in gunbc.filesystem_create_new_admission and rostered, with a trigger naming the capability (creation exclusivity declarable as a property of a write, with the realization deriving the flags) rather than an artifact.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9

[briansrls]

Exact-head native review — 3a1d1729c5251865002cf9cb7d360879690e1ea3

REQUEST_CHANGES

The central correction is real and accepted as far as it goes: WriteCreateNew is a distinct modeled fact from WriteOwnerOnly; the interpreted host path uses OpenOptions::create_new(true); and the existing-path test asserts the load-bearing consequence that pre-existing bytes survive. That closes the original check-then-unconditional-write truncation route.

It does not yet make the complete init model safe or truthful. Six bounded findings remain.

1. ScmInitialized can contain a failed creation

initialize_repository_at currently does this:

ScmInitMayCreate(_) =>
  ScmInitialized { save: create_repository(...) }

But create_repository returns RepositorySave, whose arms include codec refusal, file-unwritable, and unrepresentable byte count as well as RepositorySaved. Therefore the model can produce values such as:

ScmInitialized { save: RepositoryFileUnwritable { ... } }

The renderer notices the nested failure and exits nonzero, but that does not repair the carrier. Any other consumer matching the outer arm is told initialization happened when it did not. A false success state is representable and is produced on the ordinary write-refusal path.

Match the save result before constructing the init outcome. Only RepositorySaved may construct ScmInitialized; every other save arm needs a refusal/indeterminate init arm, or the outer arm must be renamed so it does not assert success. Execute the total fold over all four RepositorySave arms; a mutation that wraps a failed save as initialized must go red.

2. The established-absence authority is discarded before actuation

The comments claim that ScmInitMayCreate carries the same unforgeable FilesystemEstablishedAbsence that authorizes the write. The implementation instead matches it as _ and actuates with an independently computed raw path:

ScmInitMayCreate(_) => create_repository(path: path, ...)

scm_init_decision also receives path separately from the observation, and create_repository is publicly callable with any String. Consequently the sole-constructor token neither identifies nor is consumed by the write. An absence established for subject A can coexist with an actuation against subject B; changing only the write path remains writable.

Choose one honest model:

• make the absence a real subject-bearing capability consumed by the create actuation, with the path derived inside that authority and no independently supplied target; or
• state that the preflight is diagnostic only and that O_EXCL is the actual safety wall, renaming/removing the unforgeable-authorization claim.

In either case, add a discriminating control showing that evidence about one directory entry cannot authorize creation of another.

3. WriteCreateNew erases the post-create write-failure state

Both realizations perform two host steps after the modeled operation is admitted:

open(... create_new(true))
write_all(content)

If the open succeeds and write_all then fails, the target file has already been created and may contain zero or partial bytes. The helper returns an ordinary error; the transport reports success=false, bytes_written=0; and create_repository classifies it only as RepositoryFileUnwritable. The admission prose says the operation reports that the create did not happen, which is false in this branch.

The two current tests cover only (a) refusal before creation because the target already exists and (b) complete success. Neither observes a failure after exclusive creation.

Do not collapse “nothing was created” with “a new incomplete artifact now exists.” Model the two dispositions, or provide cleanup whose own failure is represented; alternatively use a construction that publishes the target only after complete content is ready. Add an injected or otherwise deterministic post-open write-failure control. This is separate from the original overwrite race: the existing bytes are safe, but the repository path can be poisoned by a failed initialization.

4. FilesystemEntryName does not yet guarantee one host entry on every target this operation supports

The original filename bar required no path separator and no NUL. The admission rejects /, but not \\, and it does not reject NUL.

WriteCreateNew is implemented on non-Unix hosts rather than refusing there. On Windows, a spelling such as ..\\victim is a parent traversal even though it passes this carrier, so the listing is asked about one child while the joined actuation path names another subject—the exact defect the carrier claims to make impossible.

Either reject every path separator for every supported target (including \\) and NUL, with controls, or explicitly scope/refuse the operation on targets whose path grammar the carrier does not model. The current Unix-only examples are not sufficient for a portable realization.

5. The evidence leaves three load-bearing surfaces mutable

1. The mutation receipt reaches v1_interpreter::write_file_create_new, but src/v1/05_emit_rust.dag independently spells another realization in file_write_create_new_expr. Replacing that emitted expression's create_new(true) with an ordinary create/truncate leaves the two Rust unit tests green. The new emitter verb needs an executing emitted-program probe, or a construction that prevents the two realizations from drifting.
2. present_bytes_do_not_authorize_a_write_and_are_classified proves invalid bytes become foreign_present, but for a valid repository it asserts only != may_create. Mapping every present file—including a valid repository—to ScmInitForeignFilePresent would leave it green. Pin RepositoryDecoded -> ScmInitRepositoryPresent one fact apart from the foreign-file case.
3. ScmInitNameNotAnEntry is now a fourth refusal arm, but an_init_refusal_never_exits_success and the_three_init_refusals_render_differently still enumerate only the prior three. The direct admission test proves early refusal, not that this new arm renders distinctly and exits failure. Execute it through scm_init_response and update the claimed population.

6. Compose the final #9864 authority and current main before the next candidate

This branch still carries an older copy of the #9864 CLI slice: gunbc.scm.cli again says “every gunbc scm answer,” retains an unused empty_repository import, and the plan again claims it is only a plan while containing landed receipts, presents the direct subcommand as the required host binding, names save_repository as init's actuation, and carries the obsolete pre-#9891 add/commit recipe.

Do not repair those independently into a second version. #9864 is the predecessor and must land first; then compose its final authority, preserve only #10026's init/create-only delta, regenerate every overlapping projection from the composed authority, and establish the fixed point.

This exact head contains main@a0f03e41c992c9c1f4d404bda099804494b2629b; current main is 533264517ca822002519b96cc670c7832dcbc87f, and workflow 33631978217 is still nonterminal. Fresh terminal exact-head CI is required after the model and composition repairs.

Re-review bar

1. Make success/refusal truthful at the ScmInitOutcome outer arm.
2. Either consume the established-absence subject in actuation or narrow the authority claim honestly.
3. Represent or eliminate the created-but-incomplete failure state.
4. Close the cross-target filename grammar, including backslash and NUL, or scope the target.
5. Add discriminating evidence for the emitted realization, valid-repository classification, and the fourth renderer refusal.
6. Compose final #9864 plus current main, regenerate to fixed point, and obtain terminal exact-head green CI.

No objection is raised to keeping ordinary save_repository for replacement writes, or to modeling create-only separately from owner-only. No approval carries on 3a1d172.