Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
module gunbc.recurring_failure_mode.a_termination_contract_is_met_by_a_trimming_transport

import std.types { NonEmptyStr }
import std.decl_ref { DeclarationRef, WholeDeclaration }
import gunbc.recurring_failure_mode { RecurringFailureMode }

data a_termination_contract_is_met_by_a_trimming_transport: RecurringFailureMode = RecurringFailureMode {
identity: "a_termination_contract_is_met_by_a_trimming_transport" as NonEmptyStr,

receipts: [
"**a reader whose contract is LINE TERMINATION is fed through a transport whose contract is TRIMMING** (each contract is sound in isolation and they compose to a false reading: the producer really finished, and the reader really reports unfinished.",

"THE SHAPE. A reader of a stream being written concurrently must decide what counts as evidence, and the sound answer is TERMINATED LINES ONLY -- a final fragment with no newline is half a statement, and reading it would let a partially written value be read as a whole one. Independently, a capture transport normalizes what it hands back, and trailing-whitespace trimming is the near-universal convention for captured process output, because a caller comparing a captured word against a literal does not want the shell's newline. Neither party is wrong about its own subject. But the trim REMOVES THE EXACT BYTE the reader's contract depends on, so the producer's last line -- which is where terminators live: an END marker, a total, a verdict -- is silently dropped, and the reader reports the state it reserves for a producer that has not finished.",

"WHY IT IS QUIET. Nothing refuses. The transport succeeded, the exit code is zero, the reader returned one of its ordinary declared arms. The stream is intact to every eye that looks at it as text, because the missing byte is invisible in a terminal and in a diff. And the reader's arm is PLAUSIBLE -- `still being written` is exactly what you would expect of a live capture -- so the reading is not merely wrong, it is wrong in the direction that explains itself.",

"THE DEEPER DEFECT IS THAT LIVENESS WAS INFERRED FROM THE BYTES, and this is the part that generalizes past any one transport. Whether a capture's last line is whole is a fact about THE WRITER -- has the process exited -- and the bytes cannot carry it: a live stream cut mid-line and a completed transcript whose final newline a transport removed are BYTE-INDISTINGUISHABLE. A reader that decides between them by looking at the text has taken a caller's fact and guessed it, so it is not merely wrong when a transport trims; it was never entitled to be right.",

"SPECIMEN, gunbc main, 2026-09-21/22. `gunbc.machine_intake_host_capture_envelope` `host_capture_bind` gained `host_capture_terminated_lines` in #11987 -- drop the final line unless the capture ends in a newline -- for a grounded reason: the mtcollins1 census capture is bound while the host is still writing it over serial, and boot 23 had a half-written `workload-write-rc=` fragment. Production (`gunbc.machine_intake_mtcollins1_boot_run` `mtcollins1_boot_await_capture_terminal`) reads that capture with `Filesystem.Read`, so the newline survives and every fixture and every file-fed claim kept passing.",

"ONE CONSUMER FED IT A PIPE: `test.claim.mtcollins1_census_image_local_wet` `the_rendered_program_runs_and_its_output_parses_by_real_execution` rendered the capture program to `/dev/stdout` and bound `obs.stdout`. `extdeps.shell.exec` `Exec.RunArgv` is realized by `retained_utf8_lossy_trimmed`, which is `trim_end`. The program's final `echo` of the envelope END marker really wrote its newline; the trim removed it; the binder correctly declined to read an unterminated final line; the envelope bound OPEN; the claim went false. RENDERER UNCHANGED, WORLD UNCHANGED, READER MOVED.",

"WHAT IT COST, AND IT IS THE PART WORTH CARRYING: the red landed on main in a lane that was FAIL-OPEN, so it was reported as a refusal only once the receipt adjudicator was bound (gunbc#11829), after which it blocked every landing. One dropped byte, six sibling claims over the same grammar still green, and the only discriminating signal was the ONE claim whose medium differed from the other six. TWO SESSIONS DIAGNOSED IT INDEPENDENTLY AND REACHED THE SAME CHAIN, which is worth recording as evidence that the chain is READABLE and that the cost was in noticing it existed, not in explaining it.",

"THE REPAIR THAT LANDED, gunbc#12020, AND WHY IT IS THE RIGHT LINK. `HostCaptureText = HostCaptureLiveStream { text } | HostCaptureCompletedTranscript { text }` is declared ON THE BINDER'S INPUT, with one scan (`host_capture_bind_text`) over `host_capture_lines`: the live reading drops an unterminated fragment, the transcript reading does not. `host_capture_bind` keeps the live reading for every existing consumer and `host_capture_bind_transcript` reads a finished process's stdout. The caller's fact is now SUPPLIED by the caller instead of guessed from the text, so the byte-indistinguishability above stops being a hazard: there is nothing left to infer.",

"A REPAIR AT THE CLAIM WAS AVAILABLE AND IS WORSE, recorded because it is the tempting one and it passes its own controls. `host_capture_program` takes `console_device`, so the claim can render to a real file and read it back with `Filesystem.Read` -- the production medium, which preserves the newline. That makes the claim green, keeps every red, and LEAVES THE READER STILL INFERRING A CALLER'S FACT FROM BYTES: the next consumer to hand it a normalized capture gets the same false reading, and nothing in the model refuses. It is DESIGN section 5's validation standing where construction was available, and the tell is exactly the one section 6b names -- it repairs the link where the symptom was observed rather than the earliest boundary that cannot be justified.",

"RECOGNITION RULE. Ask, at every hop between a producer and a reader with a framing contract, WHAT THE TRANSPORT IS ENTITLED TO REWRITE -- and then ask whether the reader is INFERRING a fact about the writer that only the caller holds. The tells are mechanical: a reader that treats an unterminated tail specially, anywhere downstream of captured process output; a claim that binds `obs.stdout` where production binds file bytes; a reader returning its `incomplete` / `pending` / `open` arm for a producer that has demonstrably exited; and a parser whose fixtures (authored strings, which keep their newline) all pass while its one real-execution claim does not.",

"IT IS NOT `printed_remedy_is_mangled_by_the_medium_that_prints_it`: there the medium SUBSTITUTES or EXECUTES a span, arbitrary characters are at risk, and the remedy is quoting at the send site. Here the medium removes exactly the framing byte, deterministically and as specified, and no quoting rule addresses it. It is not `empty_capture_read_as_clean_result`: the capture is not empty and the reader does not consume an emptiness; it reads a complete stream and correctly reports one line less than was written. It is not `transport_close_read_as_completion`: there the transport's end-of-stream is mistaken for the producer's completion; here the producer's completion MARKER is deleted by the transport and its absence is read as incompletion -- the opposite direction.",

"RUNG FOUND AT: SILENT WRONGNESS at the composition -- neither party reports anything and the reader's answer is a declared, self-explaining arm -- caught only because one claim over the affected route happened to be a wall, in a lane that was itself fail-open at the time.",

"RUNG NOW, FOR THIS READER: STRUCTURALLY GUARANTEED by #12020. The invalid state is still describable -- a caller may pass `HostCaptureLiveStream` for a transcript -- but it can no longer be reached by a transport quietly normalizing bytes, because the arm is chosen at the call site by the party that knows. NOT structurally impossible: both arms wrap a bare `String`, so the mislabelling has a constructor.",

"ATTAINABLE CEILING: STRUCTURALLY IMPOSSIBLE, and the residue is now narrow and named. A capture whose trailing terminator is guaranteed and a capture that has been normalized are still two things wearing one `String`; a CAPTURED-TEXT CARRIER THAT DECLARES WHAT ITS TRANSPORT NORMALIZED would let the arm be derived from the transport that produced the bytes rather than asserted beside them, at which point a live-stream label over a trimmed capture has no constructor either. Nothing about this is undecidable: the normalization is declared at the transport's own boundary.",

"NEXT-RUNG TRIGGER, AT CAPABILITY GRAIN: A CAPTURED-TEXT CARRIER THAT DECLARES WHAT ITS TRANSPORT NORMALIZED, sufficient for the liveness arm at every call site of a termination-contracted reader to be DERIVED from the producing transport rather than supplied by the caller. It must reach every such reader and not this one: #12020 closed the host-capture binder, and a trigger naming only that binder would be satisfied while the next termination-contracted reader in the corpus is still fed a normalized stream with nothing to refuse it. A trigger naming `stop trimming in extdeps.shell.exec` is the artifact-grained version and is the wrong repair besides -- trimming is correct for the consumers that have it, and a corpus-wide untrim would change every one of them while leaving the inference hazard untouched.)",
],

evidence: [
DeclarationRef { module_path: "gunbc.machine_intake_host_capture_envelope", decl_name: "host_capture_bind_transcript", field: WholeDeclaration },
DeclarationRef { module_path: "test.claim.mtcollins1_census_image_local_wet", decl_name: "the_rendered_program_runs_and_its_output_parses_by_real_execution", field: WholeDeclaration },
],
}