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

[gunbai-bot]

Repairing the init model that #10026 landed with its findings open

#10026 merged while review 5089156132 stood at REQUEST_CHANGES with six findings. This is the
follow-up on the same branch. All six are addressed here.

Every finding was verified against the code before being accepted, and every fix carries a control
that goes red on the defect.

1. ScmInitialized could contain a FAILED creation

It carried the whole RepositorySave, so ScmInitialized { save: RepositoryFileUnwritable { .. } }
was a spellable value telling every consumer matching the outer arm that initialization happened.
The renderer noticed the nested failure and exited nonzero — which repaired the message, not the
carrier. A consumer reading the arm rather than re-folding its payload was simply lied to, on the
ordinary write-refusal path.

ScmInitialized now carries only { path, written } from a successful create. init_outcome_of_save
is a total fold over all four save arms; everything else reaches a new ScmInitWriteRefused.

2. The established-absence authority was discarded before actuation

The code matched ScmInitMayCreate(_) — throwing the token away — and wrote to an independently
supplied path. So an absence established for subject A could sit beside a create against subject
B, and no mutation to the write target went red.

FilesystemEstablishedAbsence carries { directory, name }, so create_repository_at_absence now
derives the target from the token. There is no second target to disagree with.

The claim was hollow and four reviews endorsed it anyway. They read the sole_constructor and
called it rung-4 "structurally impossible"; the designated reviewer read the match and found the
token was never consumed. A capability carried past its actuation authorizes nothing. The annotation
is corrected rather than softened, and now says plainly that no preflight closes a TOCTOU —
O_EXCL does; the observation decides what the operator is told and which subject may be written.

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

open-then-write leaves a created, zero-or-partial file if write_all fails, while the model
reports the create did not happen. That is worse than the race this operation was added to close:
the race could destroy someone else's bytes; this fabricates a repository nobody wrote.

Fixed by construction rather than by modeling two dispositions. Content is staged to an O_EXCL
sibling and the target name is claimed with hard_link, which fails if the target exists — so
exclusivity moves to the publish step and every earlier failure leaves the target absent. The
admission prose becomes true instead of being weakened.

My first control for this was a decoration, and the dead attempt is documented in the test module
so it is not rebuilt. It put a directory at the target and asserted the target survived; measured
against the old construction it passed, because create_new fails at the open when the name
exists, so nothing was ever created and the assertion was satisfied by the defect. The replacement
injects RLIMIT_FSIZE in a forked child so the create succeeds and the write fails — the one
ordering that separates the constructions. Proven both ways: green on the fix, red on the
pre-fix construction with a write that failed after creation must leave NO target behind.

4. The filename grammar admitted another host's separator

FilesystemEntryName rejected / but admitted backslash and NUL, while WriteCreateNew is
implemented on non-Unix rather than refusing there. ..\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 now refuse. The grammar is the union over
supported targets, not the one the author happens to run on.

5. Two of the three evidence gaps

• 5.2 — the valid-repository case asserted only != may_create, which stays green if every
  present file maps to ScmInitForeignFilePresent (telling an operator a foreign file blocks their
  own repository). Now pinned to repository_present, one fact apart from the foreign case.

  Tightening it exposed a second authority in my own fixture, and that is the later commit on this
  branch. The pinned claim went red in CI: the hand-authored payload
  {"format":"gunbc-scm-repository-v2"} does not decode as a v2 repository, so the classifier
  answered foreign_present. Reverting the pin would restore a claim that cannot tell a repository
  from a foreign file, so the fixture is what changed. A literal here is a second authority for
  the repository wire format (DESIGN §3): it agrees with the codec only while someone keeps retyping
  it, and the version it drifts to is silently classified foreign — the classifier reporting a
  repository this program just wrote as not one. The fixture is now serialize_json of
  encode_repository_checked(empty_repository()), the same two calls repository_save makes, so
  writer and classifier are held to agreeing by execution. The encode-refused arm yields "",
  which decodes as foreign, so a refusal fails the claim instead of vacuously satisfying it.
  Mutation-proven: substituting the old literal back turns the claim red.

• 5.3 — ScmInitNameNotAnEntry became a fourth refusal arm while both renderer claims still
  enumerated three. Both now cover four, and the claim is renamed so its name moves with its
  population.

5.1 — the emitted realization kept the defect the interpreter fix removed

Review 58797 reclassified this correctly, and I had it wrong: I filed it as a
testing gap, and it was the defect being live. One fact — how a create-only file write is
performed — had two authorities, and finding 3 repaired only the seed interpreter. Rung honesty is
the minimum across in-scope paths, so a repaired seed beside an unrepaired emitted program is
not a repaired class.

05_emit_rust.dag's file_write_create_new_expr now emits the same staging-plus-hard_link
construction, so the emitted program no longer fabricates a repository nobody wrote.

What this does not claim. Two realization spellings still exist and are held in step by review
rather than by construction, and the source says so at the site. That residue is a DESIGN §3
single-authority defect in its own right; the reviewer has ruled it should be lifted as its own
atomic PR immediately after this one — one file-transport realization authority from which both seed
and emitted behavior are derived, deleting the two-spelling subject rather than adding another
equality witness. Deliberately not folded into this PR: repairing the unsafe emitted path and
raising the whole mechanism to the next construction rung are different bars.

6 — compose #9864's final authority

#9864 has landed, and this branch composes it.

🤖 Generated with Claude Code

https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9

[briansrls]

Re-review on exact head bc3bbb9. The code-side 5.1 repair is present: the emitted create-only realization is exercised as emitted bytes, while the remaining two-spelling residue is explicitly classified as a next-rung single-authority problem. The 5.2 fixture correction is also directionally right: derive valid repository bytes through encode_repository_checked + serialize_json rather than hand-authoring a second wire-format authority, with encode refusal failing the claim instead of vacuously passing it. One blocker remains before approval: the PR body still says only five findings are fixed, says the sixth is deliberately not guessed, and lists 5.1 under 'Not done'. That disposition ledger is false for bc3bbb9. Update the PR body to describe the actual six-finding state and the separate remaining next-rung authority residue. This is metadata-only and need not restart the running exact-head CI. CI itself is still in progress, so merge admission is not yet adjudicable regardless. After the body is corrected and exact-head CI terminates, I will apply the forward-delta gate to the then-current main.

[gunbai-bot]

Thanks — taking the staging-path nit from review 58836 as correct, with one narrowing, and deferring it deliberately rather than silently.

Verified against the code. The staging name is format!("{path}.gunbc-create-{}", std::process::id()), so it is unique per target but not per thread. Two threads of one process creating the same target derive the same staging name; the loser's O_EXCL create of the temp fails EEXIST.

What it is not. I checked the failure arm on both realizations before agreeing, because the dangerous version of this bug would be the loser deleting the winner's staged bytes. It does not: the interpreter returns on the open error before reaching any remove_file, and the emitted expression's ? early-returns for the same reason. Only the creator of a temp ever removes it. So there is no data loss and no cross-deletion.

What it is. A diagnostic-quality defect, and refusing is itself correct — with two threads racing one target, one must lose. The defect is that the loser is told EEXIST on <path>.gunbc-create-<pid>, an internal staging name it never asked to write, instead of on <path>. That is a refusal that does not locate itself at the operator's subject. The fix is to make the staging name unique per attempt so the loser falls through to hard_link and fails on the real target, which is the located diagnostic.

Why not in this PR. The reviewer's ruling on this head was that the only outstanding item was the PR body, explicitly as metadata with no head move and no CI restart. Pushing a code change now would move bc3bbb9, discard its exact-head qualification and spend another full CI cycle on a diagnostic string. Against that, the next PR is already commissioned — a single file-transport realization authority that rewrites exactly this code on both sides and deletes the two-spelling subject — so the fix lands there, in the one place that will still exist afterwards, rather than being applied twice to two spellings that are about to become one.

Recorded in my pinned plan against that PR so it cannot be lost if this session is replaced.

— sent from deep-carp-676

[briansrls]

The substantive PR-body blocker from review 5093293350 is closed: the body now says all six findings are addressed, records 5.1 as a live emitted-path defect rather than a testing gap, separates the remaining two-spelling §3 residue, records the 5.2 fixture-authority correction, and says #9864 has landed/composed. Two metadata corrections still remain before I can clear the prior REQUEST_CHANGES: (1) the PR title still says “five of ... six findings”; (2) the 5.1 section says “Review 5093286191's predecessor”, but 5093286191 is my APPROVE on #10095, not the review that reclassified 5.1. Remove or correct that citation rather than leaving a false referent. Both are metadata-only; do not move bc3bbb9 or restart CI. Exact-head CI is also still running, so native APPROVE remains withheld until it terminates and the forward delta is adjudicated.

[briansrls]

Re-review update on exact head bc3bbb9. Exact-head workflow 33663448232 is now terminal SUCCESS, so CI qualification of this composition is closed. I am not lifting CHANGES_REQUESTED yet. Two metadata defects named in review 5093448662 remain live: the PR title still says “five ... six findings”, and the 5.1 body cites “Review 5093286191’s predecessor” even though 5093286191 is the #10095 approval, not the review that reclassified 5.1. Both are metadata-only; fix them without moving the head. Separately, merge admission against current main requires recomposition: the forward delta from composed base de531c3 to observed main cd3cf69 overlaps both qualification machinery (.github/workflows/witnesses.yml) and #10069’s own implementation/generated closure (src/v1/05_emit_rust.dag and src/v1/stage0/src/v1_compiler_emit_rust.rs). Therefore the green bc3bbb9 receipt cannot authorize the combined tree. After metadata correction, compose current main once, regenerate, obtain one exact-head run, then adjudicate only later forward movement.

[gunbai-bot]

Review 58882 raises filesystem_established_absence_path inserting / unconditionally. I checked it rather than waving it through, and it is a real modeling gap — narrower than it first reads, but in a function whose entire purpose is subject identity, so worth stating precisely.

What it is. filesystem_established_absence_path is join([directory, "/", name], ""). Two inputs make that wrong:

• directory: "" yields /name — an absolute path at the filesystem root, a different subject entirely from name. This is the bad one: the function exists to guarantee there is no second target to disagree with, and here it would authorize a target the absence was never established for.
• directory: "d/" yields d//name, which POSIX collapses to d/name. Benign, but only by accident of the host.

The asymmetry that allowed it. name is admitted by a grammar — admit_filesystem_entry_name refuses /, backslash and NUL, which is finding 4 of this PR. directory has no grammar at all: it enters through filesystem_listing_observation(directory: String, ...) as an unadmitted caller-supplied String and is carried into FilesystemEstablishedAbsence verbatim. Half the path is constructed, half is trusted.

Reachability, measured rather than assumed. I traced both realizations. Filesystem.List is std::fs::read_dir(&path) in the interpreter (v1_interpreter.rs) and in file_list_match_expr; read_dir("") fails with ENOENT, so success: false, so filesystem_listing_observation produces FilesystemDirectoryListingRefused and no absence is established. So the empty-directory case is not reachable on the wet path today. It is representable in the model and constructible by a fixture, which is exactly the population §4b(2) says a check must be authorable against.

So the honest rung: this is not a live defect, and it is not structurally impossible either — it is prevented by a host accident rather than by construction, which is precisely the shape this PR spent six findings removing elsewhere.

Not fixing it here, deliberately. This head (b0de23b) is the composition the SCM reviewer required after ruling bc3bbb9 inadmissible onto cd3cf69, and it is mid-CI. A code change now discards that qualification and buys another full compose-and-rerun cycle for a case that cannot currently occur. It is also not in the transport PR's subject — that one owns write realization, this is path derivation — so I am not smuggling it in there either.

Filing it as its own follow-up: give directory a grammar so FilesystemEstablishedAbsence cannot hold one that does not name a directory, rather than normalizing the separator at the join. Normalizing would be validation standing where construction is available — it would leave the empty directory writable and merely paper over its rendering.

The PID-only staging temp from review 58836 remains folded into the transport PR, as the SCM reviewer directed, with a discriminating same-process concurrent control.

— sent from deep-carp-676

The requested content and metadata changes are closed: the title now says all six findings, the 5.1 citation names review 58797, and exact head 5d0d8b8 is terminal green. Dismissing this stale content blocker does not authorize merge: the forward delta from composed main cd3cf69 to observed main 8e025f8 overlaps the PR's emitter authority, generated mirror, interpreter, and qualification machinery, so a frozen or queued composed-candidate qualification is still required.

[briansrls]

Content and metadata are accepted on exact head 5d0d8b8. Workflow 33678358909 is terminal green across required build, floor, Rust unit/clippy, fabric evidence, and aggregate witnesses. I dismissed stale REQUEST_CHANGES review 5093293350 because every change it requested is closed.

Merge is not authorized on this head. Its composed-main checkpoint is cd3cf69; observed main is 8e025f8. That nine-commit forward delta overlaps src/v1/05_emit_rust.dag, src/v1/stage0/src/v1_compiler_emit_rust.rs, src/v1/stage0/src/v1_interpreter.rs, and required-floor machinery. #10073 may leave the create-new hunk text untouched, but it changes the authority/generated/host compilation surfaces and the clippy judge that already found a branch defect, so hunk disjointness cannot waive combined-tree execution.

RULING: use the quiet/queued-slot arm, not another unprotected treadmill cycle. This does not waive one final composition and run. It bounds them. Obtain either (1) a real merge queue that tests the exact synthetic merge result and holds it for native approval, or (2) an operator-enforced exclusive main freeze with #10069 as the next merge. When the slot opens: name main checkpoint T0; compose T0 once; resolve generated artifacts through the driver; regenerate to first-generation and referenced fixed point; run the full required suite on exact head H1; verify main is still exactly T0 and the slot remains held. Bring H1, T0, run ID, fixed-point receipts, and the live freeze/queue confirmation. I will then issue native APPROVE on H1, and it should merge immediately with expected-head protection. If main advances during the slot, the slot failed; do not call the stale candidate admitted.

Do not start another blind compose/run before the operator grants the slot. Current 5d0d8b8 remains useful qualification evidence, but not merge authority.