scm: a typed read-command result that names no destination

[gunbai-bot]

Recut onto current main at 616cd8f9d83. The diff is now exactly four files and carries no parent commits:

dag/gunbc/scm/read_command.dag
dag/gunbc/scm/repository_load.dag
dag/test/claim/scm_read_command_witness_test.dag
dag/test/claim/scm_repository_load_witness_test.dag

Why it was recut

The previous composition reached main through the save branch's ancestry, so it carried repository_save.dag and its witness. Neither is on main; both belong to #9434, which is draft. Merging this PR would therefore have landed the parked save half as a consequence of branch topology rather than as a decision anyone made — nobody doing anything wrong, the ancestry simply outranking the park.

The park is respected rather than routed around. There is no convert_to_draft event on #9434 and draft is not this tooling's default (#9433 was never toggled and merged), so the hold is unexplained rather than accidental, and the correct response to an unexplained hold is to leave it standing.

The load refinement stays, and is not scope creep. Splitting RepositoryLoadRefusal out of RepositoryLoad is what lets ScmReadRepositoryUnavailable carry a refusal that cannot hold a success. Without it this module's unavailable arm would be constructible holding RepositoryLoaded, with nothing to refuse the pair. It is the enabling half of this change. The dependency was checked before cutting and runs one way: the save witness imports RepositoryLoadRefused; nothing read-side references save.

The verdict is the shape, not a field

ScmReadResult<T> = ScmReadAnswered { path: String, answer: T }
                 | ScmReadRepositoryUnavailable { cause: RepositoryLoadRefusal }

There is no answered: Bool anywhere. A stored verdict would be a second representation of what the arms already determine, so a value could be constructed whose flag says answered and whose payload is a refusal, with nothing to refuse it. Here that pair has no spelling.

The type argument carries the verb's answer — CommitLog for scm_read_log, RepositoryStatus for scm_read_status — so the three ways a load can refuse are composed once rather than restated per verb. What the generic does not buy is recorded in the module itself, measured rather than assumed: a CommitLog in a ScmReadResult<RepositoryStatus> compiles with 0 blocking, because the type argument is substituted into the formal before the inhabitance judgment runs. That is a mitigatable rung with its next-rung trigger named, not a guarantee being claimed.

An empty repository is an answer. CommitLog's NoCommitsYet sits inside ScmReadAnswered — a repository with no commits was read successfully and truthfully has nothing to report. Filing it beside "the document was unparseable" is the not-applicable-rendered-as-malformed conflation: opposite owners, opposite repairs.

Evidence

Mutating scm_read_log to render a load refusal as an empty log answer — the empty-observation narrow — reds three claims while leaving the fourth green:

                empty      absent   verdict   schema
BASELINE          0           0        0         0
MUTATION          0 <--       1        1         1     <-- empty is an EXPECTED GREEN (control)
RESTORED          0           0        0         0

p_empty staying green is the result, not a gap. It is a negative control firing correctly. An empty repository and an unavailable one are different states; the mutation corrupts only the second; so the claim about the first is supposed to survive, and its survival is what establishes that the other three are bound to the distinction rather than merely to the module. A mutation that reds everything only proves the claims are attached to the code, which is what breaking anything gets you.

All six claims in the read-command witness and all five in the load witness are test fn, so the floor's strip_prefix("test fn ") scan discovers them. Both keystones return true on this tree over current main.

One claim whose name came down rather than up

scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log previously asserted sameness of cause in its name while its body only checked that neither verb answered — and two verbs that both fail are not evidence they share a composition.

The repair was to weaken the name, not strengthen the body, and the reason is the rule: a stronger claim is reachable exactly when it can be pinned to something this repository controls. The arm and the path are ours. The error string inside RepositoryFileUnreadable is host prose — we neither author it nor pin it — so a claim comparing full causes would be asserting a property of someone else's text. The body compares the arm and the path and binds the error _; the name now says exactly that.

What is deliberately absent

No command enum — choosing a verb from argv is dispatch, dispatch is realization, and a Log|Status coproduct would pull the CLI's concern into the value layer. Two functions instead.

No strings that are phrasing — the only Strings are a filesystem path and a commit message, both facts authored outside this repository. No message: field, no pre-formatted line, no field whose only consumer would be a printer. Wording, layout, ordering, plurals and colour are the binding's business and appear nowhere.

No binding. How this value reaches a human is a separate ruling, still open.

🤖 Generated with Claude Code

[gunbai-bot]

Closing until verified — the refactor in this branch invalidates two witnesses that I am mid-way through updating, and a draft PR still runs the full floor. Reopening once it compiles green locally-remote, so the fleet spends one run on finished work rather than three on work in progress.

— sent from gentle-eagle-360

[gunbai-bot]

Fixed, and the fix landed on #9434 rather than here — dag/gunbc/scm/repository_save.dag is that PR's file, and this branch carries it only because it is stacked. Commit dee767f9c68, merged forward into this branch.

The finding is correct. RepositorySaved { bytes_written: Int } put the unit in the field name and left the type a bare Int. The raw scalar is legitimate at the extdeps.filesystem boundary under cited-spec fidelity — the host really does report an Int — and propagating it inward was exactly the step this type took.

Took the wrap, not the marker. ByteSize (std.measure, Measure<Memory, One, Nat>) already is the authority for a quantity of bytes, so a tracked feature:/dissolve-on: marker would have registered debt in a place where the construction already existed.

One thing the wrap forced that is worth flagging, because it is a change in shape rather than in type. ByteSize counts a Nat, the host reports an Int, and the only available crossing — std.checked_arithmetic nat_magnitude — takes an absolute value. Applying it unguarded would turn a negative host report into a plausible byte count: fabricated plausible output, in the one module whose stated point is that adjudication precedes the write. So the crossing is guarded and the negative gets its own arm carrying what the host actually said:

type RepositorySave
  = RepositorySaved { path: String, written: ByteSize }
  | RepositorySaveRefusedByCodec { path: String, cause: RepositoryEncodeRefusal }
  | RepositoryFileUnwritable { path: String, error: String }
  | RepositoryWriteByteCountUnrepresentable { path: String, reported: Int }

nat_magnitude now runs only on the non-negative domain, where it is the identity.

RepositoryWriteByteCountUnrepresentable is a boundary obligation (§4b) — external reality observed, typed, admitted or refused — not a class on the ladder, so it carries no next-rung trigger. It also has no witness, and the annotation says so as a limit rather than leaving it to read as a gap: reaching it needs a host write that succeeds and then reports a negative, which no SubstrateInputsOnly fixture can author, and a real write refuses at the hermetic boundary before any count exists. The arm is kept because the alternative is not "no arm" — it is nat_magnitude silently producing a byte count from nonsense. Deleting it would delete the refusal, not the case.

Thanks for the read on the rest; the T inference gap note you singled out has since been sharpened by measurement — three serialized probes established that the judgment is reached and declines because the formal is a type variable, so the trigger now names the capability (the type argument substituted into the formal before the judgment runs) rather than a position class.

— sent from gentle-eagle-360

[gunbai-bot]

CI is red and the failure is not from this PR — declining to push a fix, with the evidence.

The failing job is required-witnesses-floor (job 98608330854). Verbatim:

required-ci: parse OK 4200 file(s) parse-clean
required-ci: declarations FAIL IMPORT-MEMBER-ABSENT dag/product/fabric/contention.dag:23:19:
  `product.fabric.contention` imports `grant_duration_seconds` from
  `product.fabric.supply`, which declares no such name

dag/product/fabric/ is untouched by this PR — the diff is dag/gunbc/scm/* and dag/test/claim/scm_*. The cause is on main: #9395 added contention.dag calling grant_duration_seconds, #9397 renamed that accessor in supply.dag to grant_duration_bound_seconds returning Second? and did not update the caller. Each was green against a base lacking the other; they edit different files, so git merged them cleanly and together they break main. No textual merge could have caught it.

Compiling contention.dag as an entry locally gives five blocking diagnostics, and three are the missing name while two are exhaustiveness obligations — occupancy_basis_of is missing UnobservedGrantDuration, and the affordability match is missing QuoteNotPriceableWithoutDuration. So this is not a mechanical rename: the accessor returns Second? because the underlying fact became partial, and the annotation in supply.dag states that QuoteNotPriceableWithoutDuration is not a fifth way of being unaffordable. Picking a default or a wildcard arm to make it compile is the fabrication that rename exists to prevent, in a domain this PR does not own. It is assigned to the owning lane.

Every open PR against current main fails this way, including ones whose branch does not contain the offending commit — the pull_request event evaluates the merge with current main, so branch ancestry exempts nothing. I confirmed that on a sibling PR whose branch predates the break and which fails identically.

No fix will be pushed here. This PR carries an approval with no findings (review 56869); it becomes mergeable when main is repaired, without any change to this diff.

— sent from gentle-eagle-360

[gunbai-bot]

Fixed in f1ff2675123. Review 56995's finding is correct and I've applied it.

One correction to the citation, which does not affect the substance. The cited lines 579,592,607 do not exist — the file is 130 lines. The three claims are at 99, 112, 127. I mention it only so the next reader can find them.

The finding stands exactly as written, and the cause is worth recording because it is not visible in either diff on its own. This branch forked from session/scm-repository-save before that branch's enrollment fix, so it carries a pre-fix copy of the save witness. Left alone, landing both PRs would have reverted the fix — the defect would have been introduced by merge order rather than authored by either change. That is why the review's framing is right: the file's mutation-receipt annotation describes an order property, the floor's strip_prefix("test fn ") scan discovers no identity for any of the three claims, and the annotation ends up citing evidence that never runs.

Applied: fn → test fn for the three claims. The keystone returns true after the change.

One deliberate non-change. scm_sv_unrepresentable_repository at line 90 stays a plain fn. It returns RepositoryEnvelope, not Bool — it is a fixture helper, not a claim, and promoting it would enroll a non-claim into the floor.

On the review's parenthetical about the _test name suffix: the file is already scm_repository_save_witness_test.dag, matching the load witness. I read that clause as describing the claim-name prefix convention (scm_rl_ vs scm_sv_), which is intentionally different because the two files witness different subjects; if a rename was meant, say so and I'll take it.

The two write-arm claims the annotation discusses remain unauthored, unchanged by this commit and for the reason the annotation gives: a write has no hermetic input carve-out, so authoring them would produce a route gap that blocks rather than merely sitting inert. That route is a wet-route enrollment, not another claim in this file.

— sent from gentle-eagle-360

[gunbai-bot]

Recut at 616cd8f9d83. Prior approvals were given on a different diff and should be re-taken.

The change reviewers approved is intact; what changed is the PR's scope. The earlier composition reached main through the save branch's ancestry and so carried repository_save.dag and scm_repository_save_witness_test.dag. Neither is on main, and both belong to #9434 — which is draft. Merging this PR would have landed the parked save half as a side effect of branch topology rather than as a decision anyone made.

The diff is now four files: read_command.dag, repository_load.dag, and their two witnesses. Save is out.

Two of the review findings against the old body were correct and are fixed in the rewrite:

1. The body showed the type without its parameter. It is ScmReadResult<T>, and the body now says so, along with what the type argument does not buy — a CommitLog in a ScmReadResult<RepositoryStatus> compiles with 0 blocking, because the argument is substituted into the formal before the inhabitance judgment runs. That is recorded as a mitigatable rung with its trigger named, not papered over.

2. The body claimed the same-cause claim "compares the causes." It does not, and should not. The claim is scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log; it compares the arm and the path and binds the error string _. That string is host prose we neither author nor pin, so a claim comparing full causes would assert a property of someone else's text. The name came down to meet the body rather than the body being pushed up to meet the name — the stronger claim is reachable exactly when it can be pinned to something this repository controls, and here it cannot.

Both keystones return true on the recut tree over current main; all six read-command claims and all five load claims are test fn, so the floor discovers them.

No route-gap rows are pre-enrolled. Whether any identity here gaps is for the floor receipt to say — enrolling a speculative row would correctly fail as stale.

— sent from gentle-eagle-360

[gunbai-bot]

Fixed in 2a0d65a70e0. Review 57012 is correct, and it is a sharper finding than it states.

repository_load_refusal_path had exactly one occurrence in the tree — its own definition. No consumer, so §6 residue, as reported.

The part worth recording: read_command.dag's header in this same PR cites this exact helper shape being removed twice before — once as checkout_succeeded, once from gunbc.scm.ancestry under review 56207 — and gives the reason that survives. So this diff re-added the third instance of a shape it was simultaneously documenting as twice-removed. Neither a lens nor a green run can see that; it is only visible by reading the two files against each other, which is what the review did.

Deleted the helper. The rationale in its comment block was about the types — why no loaded: Bool exists anywhere in the module — not about the accessor, so it moves to type RepositoryLoad rather than being deleted along with the function. A prose row removed for one reason should not silently take its contents with it.

I extended it with the reason this shape keeps recurring, which was written down nowhere and is the stronger half:

with no consumer the accessor is §6 residue, and with one it is worse — a fourth refusal arm would be absorbed by the projection instead of failing to compile at each site that must decide about it.

That is why the removal keeps being the right call rather than a style preference, and it now sits where the next author meets it before adding a fourth instance.

Both keystones return true after the deletion.

— sent from gentle-eagle-360

[gunbai-bot]

Verified: this red is main's, not this PR's. The fix is #9535, already open and approved.

Both failures on run 33127582340 are the same two that fail on every PR based on current main:

required-ci: lane=witnesses phases_run=3 failed=2
  FAILED PHASE namespace-wave-admission (0 unadjudicated delta(s), 53 stale admission(s))
  FAILED PHASE floor refused: BarrenTestSidecar count=1
    -- dag/test/claim/resolved_call_emission_identity_witness_test.dag

resolved_call_emission_identity_witness_test.dag landed in #9436 with seven claims all declared plain fn, so the floor enrolls nothing from it and refuses the barren sidecar. I opened #9535 to promote those seven declarations; it is approved and its CI is running. When it lands, this red clears here and for every other open PR at the same time.

I predicted this red before it arrived and checked the log anyway rather than assuming — a predicted failure still has to be the failure you predicted.

One thing I am explicitly not concluding. No scm_ claim appears anywhere in the failure output, and that is not evidence that this PR's claims passed. The floor refused during preparation, so none of them ran. Reading an absent failure as a pass would be execution-provenance loss: a refused-before-execution run and a clean run render identically here, and only one of them is a measurement.

What this PR's claims are backed by: both keystones return true locally over this exact tree, all six read-command claims and all five load claims are test fn so the floor will discover them, and review 57018 approved the recut diff. The floor's own verdict on them is still owed and arrives once #9535 unblocks it.

No fix is pushed here. Pushing one would mean putting an unrelated file into a diff whose scope is the read-command result, and the repair belongs in main.

— sent from gentle-eagle-360

[gunbai-bot]

Verified: the build-lane failure is inherited from main, not from this PR. No fix is pushed, and none is available from this branch.

Run 33131098881, build lane — one phase of five fails, and it is regen:

required-regen: first_generation_equal=false planned=138 executed=138 declared_divergent=1 [main.rs]
required-ci: regen FAIL generated surface drift:
  v1_compiler_emit_core_support.rs, v1_compiler_emit_go.rs,
  v1_compiler_emit_python.rs, v1_compiler_emit_rust.rs
required-ci: lane=build phases_run=5 failed=1
FAILED PHASE regen (1 failure(s))

The four drifted files are stage0 emitter mirrors. This PR touches four .dag files under dag/gunbc/scm/ and dag/test/claim/ and no mirror, no emitter, and no Rust. The same failure reproduces on main across consecutive push runs, so it predates and is independent of this branch.

The other four build phases pass on this head, which is the discriminating part — a broken diff would not pass them:

required-ci: emit-compile ... baseline=[Completed status=0] mutation=[Discriminated ...]
required-ci: partition-crates rendered=14 matches=14 drifted=0 absent=0
required-ci: generated-artifact rostered=70 adjudicated=70 matches=70 drifted=0 unadjudicated=0

A correction to something I said on this PR earlier. I previously wrote that this PR was "blocked only by the main floor breakage." That was unsound on its face and I should have caught it: BarrenTestSidecar is a floor refusal and cannot fail a build lane. I read one failing lane and generalised to both. The barren refusal is now fixed on main (#9535), and this build-lane regen failure is a separate, still-open item that the floor fix was never going to clear.

The regen drift is unassigned, older than tonight, and with my parent session. I am deliberately not adopting it: finding the log line does not make it mine, and taking it here would put four emitter mirrors into a diff whose scope is a typed read-command result.

The floor lane on this head is still running. This PR's own evidence is unchanged: APPROVE on the recut (review 57018), no open REQUEST_CHANGES, both keystones return true locally over this exact tree, and all eleven claims are test fn so the floor discovers them.

— sent from gentle-eagle-360

[gunbai-bot]

Correction to this merged PR's body. Two statements in it are wrong; the landed source is correct in both cases. Recording it here because the body is the review record the next contributor reads, and one of the two would teach them a false mechanism.

1. The body invents a mechanism the module deliberately did not claim

The body says:

a CommitLog in a ScmReadResult<RepositoryStatus> compiles with 0 blocking, because the type argument is substituted into the formal before the inhabitance judgment runs.

That "because" is mine and it is unfounded — and it is very close to the inverse of what was measured. The module's own annotation records three serialized probes, and the middle one refutes the explanation:

kernel at a NON-GENERIC record field   REFUSES
UNDEFINED NAME at the generic field    REFUSES   <-- inference DOES reach this position
kernel at that same generic field      ADMITS

The undefined-name probe exists precisely to prove that inference reaches this exact position rather than skipping it. So the judgment is not bypassed and the position is not skipped; what does not happen is that the concrete type argument is enforced there. The source says only that, and says it carefully — it states the rung is mitigatable, that this is "NOT a claim that the payload type is enforced here," and that the mechanism was "measured rather than reasoned about."

The body then reasoned about it anyway and published a cause. That is this repository's diagnostic name accurate about the situation, silent about the mechanism class: the observation (0 blocking) was real, the explanation was invented, and an invented explanation in a merged review record is what the next contributor builds on.

The annotation in the landed source is the authority here, not this body.

2. "The only strings are a path and a commit message" is false transitively

The body claims:

the only Strings are a filesystem path and a commit message, both facts authored outside this repository

But the refusal arm carries host prose through composition:

ScmReadRepositoryUnavailable { cause: RepositoryLoadRefusal }
  -> RepositoryFileUnreadable { path: String, error: String }   <-- host error text

The intent of that section is sound and the code honours it: no message: field, no pre-formatted line, no field whose only consumer is a printer, and no phrasing authored by this module. That is why the same-cause claim binds error as _ and had its name weakened rather than its body strengthened — the error string is host prose this repository neither authors nor pins. But "the only Strings are" is a statement about the whole value, and the whole value does carry one more, inherited from the load refusal.

The accurate claim is the narrower one the source already implements: no string in this module is presentation prose authored here.

Not affected

The landed code, the eleven claims, and the three route-gap enrollments all stand. These are review-record defects, not code defects, and I am not proposing a follow-up change to the source — the source is what is right in both cases.

Found by the advisory review thread; verified against origin/main before posting rather than taken on report.

— sent from gentle-eagle-360