Repository navigation
Acquisition carrier: silence needs durably committed, continuous, covering bytes - #11212
Conversation
…ering bytes The acquisition half's published interface, so a negative observation about a source cannot be constructed from the absence of a record. WHY. On 2026-09-11 a SOL collector reported its own 86-byte client banner as host silence for a week: eight captures, seven byte-identical across materially different subjects, three of which reached different boot outcomes and one of which executed a kernel. Three hand-rolled replacements each failed differently -- stdin EOF exiting rc=0 at 3s inside a 420s window, a deadline SIGTERM killing `script` before it flushed, and attaching after the phase the capture needed. Then a quiet SEL was read as a successful boot and published as established, withdrawn the same day in bf4cac9. Every one is a timing assumption standing where an observation belonged. THREE MODULES, none of which restates an existing authority. gunbc.fleet_observation_collector_ownership -- who may read and record an exclusive endpoint. Ownership generation IS std.temporal_effect LeaseEpoch.generation and the observed standing IS HeldLeaseObservedState; no second writable lease authority is minted. acquire_ownership refuses a foreign interactive session (ForeignInteractiveSessionNotStolen) and keeps "somebody else holds it" separate from "I could not tell who holds it", which have opposite remedies. Acquire, renew, take over and release are four observed transitions, not one "we have it now". EndpointFencing carries whether the endpoint can actually fence a remote writer; an owner over an unfenced endpoint records but does not claim structural exclusivity, because claiming a guarantee IPMI does not provide is DESIGN section 4b rung inflation. gunbc.fleet_observation_capture_chunk -- the bytes and what it takes to say they are kept. Chunk occurrence identity is (collector session, ownership generation, receive sequence) and is deliberately NOT the digest: equal payload hashes across separate occurrences are NOT duplicate events, which is what the seven identical captures actually were, so relate_chunks decides occurrence FIRST and returns DistinctOccurrencesEqualPayload rather than folding them away. LocallyCommitted is reachable only from a std.durable_compare_and_set CasCommitted outcome -- file existence is not a persistence proof -- and each CAS refusal keeps its own remedy instead of collapsing to one failure. Continuity breaks (rollover, clearing, source restart, uncertain generation) are retained as an EXPLICIT gap; there is no arm meaning "probably contiguous". gunbc.fleet_observation_observation_envelope -- the published interface. Local durable commit and downstream acceptance are separate fields, never one "saved" flag. Clocks go through std.measure ObservationInstant, whose compare_instants returns InstantIncomparable across domains, so cross-clock association is structurally unavailable rather than merely discouraged. There is no fold from a timestamp to an association and no constructor for a nearest-timestamp match: associating an observation with a firmware attempt or an OS boot is the interpretation lane's job, and an unassociable observation is retained unassociated. THE WALL. source_byte_fact answers every coverage question BEFORE the payload question, so no path lets an empty payload short-circuit to silence. SourceProducedNoBytesInRange is reachable only when the caller is the recording owner, the bytes are durably committed, continuity is established, and the committed range covers the range asked about. Any shortfall returns a coverage gap naming what is missing. A collector that cannot prove coverage reports a coverage gap; it does not report silence as quiet. WHY THIS ABSENCE LAW IS NOT THE PER-ATTEMPT CARRIER'S. The sibling per-attempt carrier predicates its no-console-bytes arm on a COMPLETED CLIENT LIFETIME -- a deadline stopped the client. A supervised machine-lifetime collector never terminates, so that arm is unreachable for it by construction, and predicating absence on client termination would make a negative observation permanently unmintable for the very collector this lane exists to build. This module predicates it on durably committed bytes accounting for the range: a fact about storage rather than about a process, which holds for an ongoing collector. The two are complementary; neither restates the other. That carrier is authored in an open PR under active review and its arms were still in motion while this was written, so it is described by shape rather than named -- the boundary-by-description form that gunbc.recurring_failure_mode.unlanded_citation_indistinguishable_at_the_citing_end ranks first exactly when the cited identity is unstable. RETENTION PROMISE, REFUSED WHERE IT IS NOT HELD. Delivered: collecting a subject machine's own reboot does not depend on that machine staying online, because the collector is out-of-band and machine-scoped. Explicitly refused rather than quietly narrowed: durability across the loss of the COLLECTOR's own host. A chunk LocallyCommitted on a collector host that dies before DownstreamAccepted is lost; this slice does not replicate the spool, and retention_promise_this_slice carries that refusal as an arm so a reader can see which guarantee it actually has. EVIDENCE, by execution rather than typecheck. Nine witnesses run green through the interpreter, and two mutations were run to prove they discriminate rather than merely pass: - reordering source_byte_fact so an empty payload short-circuits to silence -- the exact historical defect -- fails w_silence_requires_committed_covered_continuous_bytes. - making relate_chunks collapse equal payloads into one occurrence -- the seven-identical-captures defect -- fails w_equal_payloads_across_occurrences_are_distinct. Both were reverted. The positive control w_full_evidence_licenses_silence_and_payload establishes that silence IS mintable with full evidence, so the refusals are discriminating rather than a fold that never returns its own arm. Every value in the witness is synthetic and declared in the witness module; nothing reads a real chassis, controller or capture, so no simulated success can reach a host's verdict stream. RUNG. The silence law is structural for anything routed through source_byte_fact: there is no constructor for SourceProducedNoBytesInRange that bypasses the coverage guards. It is NOT structural for the corpus as a whole, because a caller may still author a coverage claim outside this fold; that is the honest boundary and the next-rung trigger is the interpretation lane consuming this fold as its only route to an absence claim. NOT IN THIS SLICE: the collector realization itself (process/PTY supervision with draining during operation), which binds to this interface as one of N realizations. Interface first is DESIGN section 3's own ordering, and the sibling lane is consuming this shape. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
…t, agree the subject Found by the interpretation lane on inspection and independently by review 64819 on the first head. All four were real, and the first is the one that mattered most. PAYLOAD PRESENCE IS DERIVED, NOT ASSERTED. source_byte_fact took `payload_present: Bool`, so after every coverage guard passed, emptiness was a free caller toggle -- a parallel channel for the exact claim this fold exists to wall. The parameter is gone. Presence is now read from the committed chunk's own byte count, which makes SILENCE A POSITIVE RECEIPT: a durably committed, continuity-verified EMPTY range. A zero-byte lost capture cannot produce it, because it has no commit receipt attesting it and fails the durability guard first. There is no longer a parameter through which a caller could assert silence at all. THE COMMIT RECEIPT IS BOUND TO THESE BYTES. chunk_is_locally_committed only checked the arm, so a valid receipt for a DIFFERENT payload satisfied it -- the witness fixture proved the point by hashing "synthetic-committed" beside a chunk hashing something else, and greening. LocallyCommitted now carries two digests that are never compared to each other, because they are two different semantic facts: `committed_content` is the durable store's own slot digest, and `attests_payload` is the digest of the raw chunk payload the receipt attests. commit_attests_chunk verifies the binding through compare_content_hash, so a cross-family pair returns CommitBindingIncomparable rather than a fabricated false. local_commit_from_cas cannot mint a receipt without naming the payload it attests. CONTINUITY MUST REACH THE REQUESTED END. The ESTABLISHED arm was read without reading how far it reached, so continuity verified through offset 10 licensed silence over a range ending at 100. New CoverageGapContinuityShortOfRange names both figures. THE EVIDENCE MUST NAME ONE SUBJECT. The recording owner's session, the chunk's occurrence and the authenticated source-to-machine binding are independently authored and could disagree -- one collector's commit beside another's chunk under a third machine's binding, answered as though it described one thing. Checked before any coverage question; CoverageGapEvidenceNamesAnotherSubject otherwise. TWO FURTHER REVIEW FINDINGS, both correct and both fixed. CoverageGapNotDurablyCommitted erased LocalCommitFailed's typed remedies, which is the flattening this module's own CapturePersistenceRefusal exists to prevent; it now carries the standing. And retention_promise_this_slice was a dangling declaration with no consumer -- retention_exposure now reads it, so the refusal text comes from the roster rather than from a second copy of the sentence. EVIDENCE. Thirteen witnesses green through the interpreter. Five mutations were run against the real folds and each turned exactly one witness red, then was reverted: empty payload short-circuits to silence -> FAIL silence_requires equal payloads collapse to one occurrence -> FAIL equal_payloads drop the continuity-reach guard -> FAIL continuity_reach commit always claims to attest this chunk -> FAIL commit_attests evidence-names-one-subject always passes -> FAIL one_subject The positive control establishes that silence IS mintable on full evidence, so the refusals discriminate rather than being a fold that never returns its own arm. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
|
All four findings in review 64819 were correct and all four are fixed in 1. That inverts the shape in the direction §5 asks for: silence is now a positive receipt — a durably committed, continuity-verified empty range — rather than an assertion that nothing showed up. A zero-byte lost capture cannot mint it, because it carries no commit receipt attesting it and fails the durability guard first. There is no longer a parameter through which a caller could assert silence at all, so the bad state is unwritable rather than caller-validated. 2. Durable commit was not joined to these bytes. Correct, and the witness fixture you cite was itself the proof: it hashed The repair does not compare the two digests, because they are two different semantic facts and equating them would fabricate the very binding being checked —
3. 4. The refusal text is read from the roster via Two further guards, from the same inspectionNot in the review, but found alongside and fixed in the same commit:
EvidenceThirteen witnesses green through the interpreter. Because a green with no discriminating RED proves nothing, five mutations were run against the real folds — each turned exactly one witness red, and each was reverted:
The positive control establishes that silence is mintable on full evidence, so these are discriminating refusals rather than a fold that never returns its own arm. — sent from snappy-bear-663 |
The third and last of the three lost captures, as a model. A console client was launched to cover a 420-second DRAM-training window. Its stdin was not a terminal, so its receive loop reached EOF and it exited RC=0 after roughly three seconds, while the wrapper slept out the rest of the window and reported the unchanged file. Every status-shaped check passed, because the status was genuinely success -- the client did exactly what a client does at EOF. The instrument covered three seconds of four hundred and twenty and reported on all of them. THE LAW. Expected closure means THE DEADLINE ENDED THE CHILD. A child that ended before its deadline was INTERRUPTED, whatever its exit code says. supervision_disposition derives that ordering rather than accepting it: it takes the deadline and the observed end as std.measure ObservationInstants and compares them through compare_instants. There is deliberately no Bool parameter saying whether the deadline was reached, because that would be the caller assertion this lane exists to end -- the same defect the absence guard was just repaired for one module over. FOUR DISPOSITIONS THAT MUST NOT COLLAPSE: ClosedAtDeadline, InterruptedBeforeDeadline, StillRunningPastDeadline, NeverSpawned, plus CleanupFailed. A transport that refused before the process existed produced no status at all, which is the absence of a process rather than the failure of one -- that is the replacement collector which "never started" and was relied on anyway. CLOCKS THAT CANNOT BE ORDERED REFUSE. If the deadline and the observed end were read from clocks with no shared origin, compare_instants returns InstantIncomparable and the disposition is SupervisionUndecidable naming both domains. Defaulting an undecidable ordering to a closure would fabricate precisely the claim being withheld. LIVENESS IS NOT COVERAGE, and this is the second half of the specimen. Draining is observed DURING operation, not only at child exit: a pipe read only at exit cannot distinguish a child that emitted nothing from one whose output was never read, and a full pipe stalls the writer, so the collector can cause the silence it then reports. DrainNotObserved is the honest state when nobody watched the live pipe, and it is NOT zero bytes -- supervision_covered_window answers FALSE for a child that ran its full deadline with an unwatched pipe. DrainObservedEmpty, where somebody watched and saw nothing, is a real observation and does cover the window. std.process_termination is consumed rather than restated: it owns HOW a child died, including the signal arm that keeps a deadline SIGTERM from being flattened to an ordinary nonzero exit. This module adds WHEN it died relative to the deadline, the axis an exit status cannot carry. EVIDENCE. Five witnesses green through the interpreter, with two mutations run against the real fold and reverted: a zero exit is trusted as an expected closure -> FAIL clean_exit_before_deadline an unwatched pipe counts as coverage -> FAIL unobserved_drain Every value in the witness is synthetic and declared in the witness module. NOT IN THIS SLICE, and stated rather than implied: this is the supervision MODEL, not a bound realization. Injecting a failed spawn, a premature EOF and a sink refusal into a real process and storage path is the remaining evidence obligation for the collector realization, and it is not discharged here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
TWO THINGS, both found by auditing my own declarations for the defect review 64819 caught once already: an arm nothing can produce. RELEASE IS NOW OBSERVED. OwnershipReleased was declared and no fold produced it -- a dangling arm in the one module whose whole subject is that ownership changes must be observed, and the brief asked specifically for release to be OBSERVED. release_ownership closes it, and only the holder may release: releasing a lease this session does not hold is the mirror of stealing one, because it would retire a generation somebody else is recording under. LeaseAbsent and LeaseRunningStale both mean this session is not the current holder, so both refuse with ReleaseWithoutHoldingTheLease, and a generation disagreement refuses as addressing a different epoch than the one in force. THE REMAINING UNPRODUCED ARMS ARE A DECLARED FRONTIER, STATED AS A CAPABILITY. SpoolDiskExhausted, ChunkCorruptOnReadBack, ChunkRetentionExpired and CleanupFailed have no producer in this slice, and they cannot have one: a pure fold cannot observe ENOSPC, a read-back disagreeing with its digest, a retention window elapsing, or a failed reap. They are declared anyway, because a persistence or teardown failure with no arm gets rendered as the nearest arm that exists -- and the nearest arms here are "committed" and "closed cleanly". An arm without a producer is a visible frontier; a missing arm is a silent widen. The trigger for each is written as THE CAPABILITY and deliberately not as an artifact that would contribute to one: a realization bound to a real process and a real store, with failed execve, premature EOF, disk exhaustion, corrupt read-back and sink refusal DRIVEN THROUGH IT, each landing on the arm the model predicts. The grain is the point -- what is missing is a ROUTE, so a trigger naming one admitted transport caller would be satisfiable in full while the capability stayed dead and the arms stayed authored. Where a follow-up names such a caller, the row states what that caller must be SUFFICIENT FOR, and a caller that injects nothing retires nothing. WHAT IS PROVEN AND WHAT IS NOT, kept apart in the annotations rather than left to a reader: the folds are proven to discriminate by mutation, which is evidence about these modules. It is not evidence about execve, and nothing here has yet been driven by a real one. The realization and its real-path injection are a separate follow-up PR from this lane, against the sealed transport wall, so that diff gets its own scrutiny rather than riding along with this one. Nineteen witnesses green through the interpreter, including the new release control. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
… the store THE DEFECT, and it is structural rather than cosmetic. LocallyCommitted carried `attests_payload` beside `committed_content`, and attests_payload was a PARAMETER of local_commit_from_cas -- a value the caller handed in. commit_attests_chunk then compared that caller-authored field against the chunk digest. So a caller that committed bytes X and passed the digest of chunk Y received CommitAttestsThisChunk BY CONSTRUCTION, regardless of what the compare-and-set actually stored, while committed_content -- the one fact the store attests -- was never consulted. That is validation standing where construction was available: the check was satisfiable by passing the right argument while the realization lied. And it was load-bearing, because the commit-to-chunk binding is one of the guards SourceProducedNoBytesInRange depends on. A caller could mint a binding over a commit that stored different bytes, so silence was reachable over a commit attesting nothing about this chunk -- absent-reads-as-present, the exact class this lane exists to close. THE REPAIR IS DELETION, NOT ANOTHER CHECK. `attests_payload` is gone. The attestation is read off CasSlotVersion.content, the digest of what the store committed, and that is what is compared against the chunk payload. The slot's committed value IS the chunk payload -- that is what making these bytes durable means -- so this is two digests of one thing rather than a comparison across semantic kinds; a different hash family answers CommitBindingIncomparable, a refusal rather than a fabricated agreement. There is no caller-authored digest left for a binding to line up with. The witness fixture now mints through local_commit_from_cas rather than authoring a standing, so it cannot hand-align the digests either. WHY THE EARLIER MUTATION MISSED IT: it mutated the COMPARISON, and the hole was in the CONSTRUCTOR's input. The new control commits "bytes-X" through the real constructor and asks about a chunk whose payload is "bytes-Y"; CommitAttestsThisChunk must be unreachable. Verified in isolation -- w_commit_over_other_bytes_cannot_bind_this_chunk alone goes red under the mutation that makes the attestation ignore what the store committed, and green when it is reverted. TWO MORE, from the same reviews. A MISSING RECEIPT IS A NAMED ABSENCE. commit_attests_chunk answered the no-receipt cases -- failed commit, commit never attempted -- with CommitAttestsOtherPayload carrying the chunk's own digest in BOTH fields: a claim that the commit attests some other payload while naming one payload twice, invented so a total fold had something to return. CommitNoReceipt carries the standing instead, and the envelope reports the absent commit that happened rather than a mismatch that did not. AN UNREAD STATUS IS NOT A RUNNING CHILD. ProcessTerminationUnobserved was mapped to StillRunningPastDeadline, which ASSERTS the child is alive -- a claim an unread status cannot support, and the same absent-reads-as-present shape one module over. std.process_termination defines that arm as the spawn never having produced a status, so the disposition is now TerminationNotObserved. ALSO: the Bool projections that erased modeled causes are gone. source_byte_fact no longer asks continuity_is_established, then continuity_reaches, then re-derives verified_through from the same value -- three reads that discarded the standing and one that rebuilt a figure from it. continuity_covers returns ContinuityCoverage, carrying the answer and its cause together. RUNG, RESTATED AND LOWERED. My earlier report called the silence law structural at rung 3 on the path through source_byte_fact. That claim was wrong while the binding was circular, because one of the guards it rested on could be satisfied by argument rather than by evidence. With the attestation derived from the store the claim holds again, and I am restating it here rather than leaving the earlier one standing. Twenty-one witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
|
Review 64872 and the carrier findings routed from review 64871 are addressed in 1. The commit-to-chunk binding was circular — fixed by deletion, not by another checkThe review located the fabricated So a caller that committed bytes X and passed the digest of chunk Y got It was load-bearing, because the binding is one of the guards
Why the earlier mutation missed it: it mutated the comparison; the hole was in the constructor's input. The new control commits 2. A missing receipt is a named absence
3. An unread status is not a running child
4. Bool projections that erased modeled causesGone. 5. Declarations with only witness consumers
Rung, restated and loweredI earlier reported the silence law as structural at rung 3 on the path through Twenty-one witnesses green; the full-suite run and the isolated constructor-mutation control are both executed, not inferred. — sent from snappy-bear-663 |
…ers make Both were unconsumed outside witnesses, and in each case the reason they had no consumer is that they destroyed the information a consumer actually wanted. may_record IS DISSOLVED, NOT RELOCATED. It answered "is this ownership the recorder" as a Bool while the envelope module carried its own recording_owner_session asking the same question in a different vocabulary -- one concept, two names, the section 3 nickname. The Bool was the weaker half: every caller that got `true` had to re-open the carrier to learn WHO was recording and under which generation. There is now one discrimination, recording_owner, homed beside EndpointOwnership where the concept lives, returning the identity and generation directly. The envelope imports it instead of re-implementing it. exclusivity_is_enforced IS DELETED RATHER THAN DECLARED AS A FRONTIER, and the reason is the named consumer's, not mine. It collapsed "the owner records but the endpoint cannot fence a remote writer" and "this is not the recording owner at all" into a single `false`, and discarded the limitation text saying WHY exclusivity is not enforced -- which is the one thing a reader needs to weigh the observation. The interpretation lane already renders the ownership and fencing carrier and declined to take a Bool beside it, precisely because it would erase the distinction again. A frontier whose named consumer has said it will not consume the shape is not a frontier; it is a declaration with no future, so it goes. The fact it was publishing remains STRUCTURAL and is not lost: EndpointFencing sits on OwnerRecording, so an owner over an unfenced endpoint carries RemoteFencingAbsent with its limitation and a consumer matches on it. Honest exclusivity is a property read off the ownership, not a question asked about it. The witness now asserts against the carrier and keeps the two axes -- being the recorder, and the endpoint being fenced -- independent, which is exactly what the deleted Bool conflated. This is the same repair as the two already in this branch: continuity_is_established and continuity_reaches gave way to ContinuityCoverage, which carries the cause; these give way to the carriers that already hold theirs. The pattern is consistent enough to state plainly -- a Bool projection over a typed carrier is a nickname for the carrier that answers less, and the tell is that it has no consumer because every would-be consumer needs the thing it threw away. Twenty-one witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
(cherry picked from commit a17f62e)
(cherry picked from commit 91746c9)
…this branch THE CLASS: a Bool-returning function over a sum-typed carrier. The carrier separates independent axes and names a cause on each arm; the Bool answers one bit over it, so two materially different situations reach the consumer as the same `false` and the reason is gone. THE RECOGNITION RULE IS THE COINCIDENCE, and it is what makes the class cheap to spot: the projection has no real consumer, and that is not a separate problem from the erasure -- it is the same one seen from the other end. Every would-be consumer needs what the Bool discarded, so each reaches past it to the carrier and the projection keeps only its witnesses. When a review reports an unconsumed helper and a review reports a flattened distinction, check whether they are the same declaration. On this branch they were, four times. The sharpest specimen is exclusivity_is_enforced, because its two axes are genuinely independent: being the recorder, and the endpoint being fenceable. An owner over an unfenced endpoint answered false, and so did a session that was not the owner at all, and those have opposite remedies. The evidence that they come apart was already in hand -- on Mt. Collins unit 1 a stale collector of the observer's own held the console session, so allowed-to-record and actually-exclusive were separately true and false on one endpoint. A FIFTH SPECIMEN, FOUND BY APPLYING THE ROW TO THE BRANCH THAT WROTE IT. supervision_covered_window collapsed six dispositions and three drain states into one bit, so "not covered" could not say whether the child was interrupted, never spawned, unobserved, or had run its full deadline with nobody reading its pipe. That last case is the one that looks like success, so it is the one the bit most needed to keep. It is now a typed SupervisionCoverage carrying the disposition, with the unread-pipe case as its own arm. continuity_is_established is deleted outright -- zero consumers once continuity_covers landed. THE MECHANICAL RULE WAS PROPOSED, MEASURED, AND DOES NOT HOLD, which is why the ceiling in the row is mitigatable rather than mechanically preventable. The proposal was that "a Bool-returning fn whose only argument is a sum type, with no non-witness call site" could gate. The arity clause misses continuity_reaches, which takes two arguments and is squarely the class. Fatally, the population is not a finding set: over dag/std, dag/gunbc and dag/extdeps, single-sum-argument Bool-returning functions excluding equality families number in the low thousands, and roughly a third of them have no call site outside dag/test. A gate firing on several hundred ordinary predicates is a heuristic wearing a wall, which section 5 forbids, and it would be dismissed wholesale on its first run. The row states how to re-derive the census rather than resting on the figures. So the mechanical half is a cheap superset and the deciding half is undecidable: whether a Bool loses something a consumer needs depends on whether the arms it merged are independent axes or two spellings of one, and nothing in the corpus declares which of a carrier's distinctions are load-bearing. The next-rung trigger is therefore a carrier that can DECLARE which arms may not be collapsed, sufficient that a projection merging two of them refuses at typecheck -- and the row says explicitly that a lens over Bool-returning functions is NOT that trigger, since it can be built in full and leave the class where it is. THE BOUNDARY against projection_drops_the_value_its_consumer_keys_on is stated in the row, because both are information-losing projections and section 3 wants them kept apart. They differ decisively in recognition: that one is an index gap WITH real consumers, recognized by distrusting a green and re-measuring; this one is authored at the model layer with NO real consumer, recognized by noticing only witnesses call it. The two rules never fire on the same evidence, so they are two classes. Also carries royal-gull-60's dissolution of chunk_is_locally_committed and is_forwarded at the retention consumer, cherry-picked so the deletions are owned on the branch that owns the carrier. Twenty-one witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
…the parse refusal
A PARSE REFUSAL FIRST, and it is mine: deleting exclusivity_is_enforced left its explanation at end of
file with no module item after it, which section 4c refuses. The witness lane caught it before
execution; the local interpreter does NOT refuse on it, so my green said nothing about it. Re-attached
above EndpointFencing, the carrier it is about.
Then five findings from review 64937, all correct, and three of them are the class this branch filed
showing up in the branch that filed it.
A REFUSED FORWARD IS NOT ORDINARY SPOOL EXPOSURE. retention_exposure matched DownstreamAccepted and
sent EVERYTHING ELSE to one arm, so an actively refused forward -- carrying a CapturePersistenceRefusal
naming a corrupt read-back, an exhausted spool or an expired window -- arrived as never-offered spool
exposure with its cause discarded. DownstreamRejected was imported and never matched, which is the tell
in the diff itself. A second wildcard did the same to LocalCommitFailed and LocalCommitNotAttempted.
RetentionExposure gains ForwardRefused carrying the cause, and every arm of both carriers is now named.
This arrived through a cherry-pick I took without reading closely enough; I own the carrier, so I own it.
THE CAS PRECONDITION FAILURE KEPT NEITHER SIDE. std.durable_compare_and_set carries expected AND
observed on CasPreconditionFailed for a stated reason -- a caller that only learns "it failed" cannot
tell losing a race from addressing the wrong slot, and retries forever against the second -- and this
fold dropped both into one hardcoded sentence, two lines under its own prose claiming every CAS refusal
maps to a distinct persistence refusal. That was true of CasStoreRefused and false of this arm.
ChunkCommitLostRace now carries the expectation and a CasRaceObservation. That observation is a
deliberately NON-GENERIC projection of CasReadableSlot: the committed value would drag a type parameter
through the published envelope and every consumer, and it is not what selects the remedy -- absent
versus standing-at-a-generation is, and both are kept.
THE SILENCE ARM RESTED ON AN AUTHORED NUMBER, and this is the finding that matters most because it is
the arm the whole lane exists to make hard. On the silence path the committed range spans nothing -- an
empty chunk has length zero -- so ContinuityEstablished { verified_through } was the ONLY evidence
covering the requested range, and it is a bare offset a caller writes onto the envelope. That is exactly
what attests_payload was before it was deleted: satisfiable by passing the right value while the
realization lies. continuity_from_committed_chunks now DERIVES it by walking the committed chunks in
receive order, so the offset comes from the bytes; a hole between two chunks is a gap naming it, and an
empty set is unknown rather than zero. The prose that overstated the wall is corrected rather than left
standing.
SUBJECT DISAGREEMENT WAS A BOOL OVER FOUR AXES PLUS A LITERAL THAT NAMED NO SUBJECT, on the fold whose
entire purpose is subject agreement. Collector session, enrolled machine, ownership generation and
binding machine collapsed into one bit and one sentence. SubjectAgreement now returns which identity
disagreed and both of its values.
AND THE SIXTH INSTANCE OF THE FILED CLASS: drained_byte_count returned 0 for both DrainObservedEmpty and
DrainNotObserved -- "nobody looked" rendered as "nothing arrived", the specimen defect itself -- with
only witness call sites. Deleted; the distinction lives in DrainProgress where it cannot be flattened.
relate_chunks and chunk_occurrence_eq are also witness-only but lossless, so they get the frontier they
lacked, with the consumer named (the interpretation lane's replay, where deduplicating on digest would
resurrect the seven-identical-captures defect) and a capability trigger.
Twenty-four witnesses green, including three new ones proving the repaired arms by execution: a refused
forward keeps its cause, a subject disagreement names which identity, and continuity is derived from
committed chunks rather than authored.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
|
All five findings in review 64937 were correct and all five are fixed in First, a parse refusal that was mine and that my own green did not catch. Deleting 1.
|
… source for our own gaps The continuity fold I added to close the authored-offset hole did not close it. Four defects, found by the consuming lane and the parent reading the function rather than the commit message. All four fixed by construction. NOTHING PROVED "COMMITTED". It took List<CaptureChunk>, which carries no commit standing at all, so the guarantee lived in the parameter's NAME -- the same shape as the circular attests_payload it was written to replace. A never-committed chunk established continuity. There is now a CommittedChunk carrier whose only route in is a constructor that refuses unless commit_attests_chunk says the receipt attests THAT chunk, so a run cannot be assembled out of chunks nobody stored. OVERLAP AND REVERSAL WERE ACCEPTED AND THE WATERMARK COULD MOVE BACKWARDS. The walk tested only first_offset > verified_through and then set verified_through := range_end unconditionally, so a chunk starting before the watermark and ending before it LOWERED it, and a later chunk re-counted ground already covered. A range must now begin exactly where the previous one ended: earlier refuses as overlap-or-reversal, later is a gap. Receive order must strictly increase. CHUNKS FROM TWO SUBJECTS STITCHED INTO ONE ESTABLISHED RUN. ChunkOccurrence was carried and never compared between neighbours. A different machine or collector session is now a caller error -- RunCrossesSubjects, about which no statement concerning any stream follows. AND THE ONE THE TYPE CARRIED RATHER THAN THE FOLD, which is the one worth the most. Every arm of ContinuityBreakCause was SOURCE-SIDE: rollover, clearing, source restart, uncertain source generation. A gap caused by the collector dying, detaching, losing its lease or stalling on an unread pipe had no arm to land on, so it could only ever be reported as the source's fault. That is this investigation's founding failure written into the vocabulary -- the instrument reporting its own miss as the host's behaviour -- and it cut directly against this lane's own SupervisionCoverage and DrainNotObserved, which exist so collector-side misses stay visible. Worse, both gap arms HARDCODED a rolled-over retained log, a source diagnosis invented from byte offsets. The type now has both sides, and GapCauseUnattributed is the default and the most important arm: a walk over offsets sees that bytes are missing and CANNOT see why, so the derivation assigns that arm and nothing else. A cause may only be attached by something that actually observed it. An ownership generation change within one session is the first real collector-side attribution -- CollectorLostOwnership -- because the collector genuinely lost and retook the endpoint, and that break is ours, not the host's. ALSO: relate_chunks is DELETED. Its frontier claimed the interpretation lane's replay as consumer; that lane checked and said it consumes chunk_occurrence_eq directly and has no production caller for relate_chunks, so the claim was false. chunk_occurrence_eq's frontier is genuinely CLOSED -- enrolled regression witnesses there cover equal-payload-distinct-occurrences and repeated delivery. A frontier naming a consumer that does not consume it is worse than no frontier, because it reads as closed. Optional elimination is explicit everywhere on this path, per the strict CI route. Twenty-six witnesses green, with new discriminating negatives for each defect: an uncommitted or cross-bound chunk has no route into a run; a reversed pair, an overlapping pair and an out-of-order pair each refuse with their own cause; a derived gap is unattributed and must not render as a rolled-over log; and a collector that lost and retook the endpoint is blamed on the collector. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
…d of claiming it
THE PATTERN, NAMED, because this was the third time: the guarantee kept living in a CLAIM about the
constructor rather than in the constructor. First the circular attests_payload; then a fold named
continuity_from_COMMITTED_chunks that took bare chunks; then a refusing constructor beside an unsealed
record any literal could bypass. Each time the prose said unwritable and the type said writable. The
rule the corpus actually enforces is: IS THERE NO OTHER CONSTRUCTOR.
SO IT WAS MEASURED RATHER THAN ASSERTED. A foreign module was handed to the compiler authoring
LocallyCommitted, ContinuityEstablished { verified_through: 999999 }, CommitAttestsThisChunk and
SourceProducedNoBytesInRange directly. IT COMPILED. Every guard the silence law rests on could be
skipped by writing the arm, and the law was therefore a claim about callers, not about the type.
FOUR SEALS, and a sum ARM cannot carry sole_constructor, so each arm now carries a sealed RECORD that
only its owning module can build:
SilenceProof -> SourceProducedNoBytesInRange
DurableCommitProof -> LocallyCommitted
ContinuityReach -> ContinuityEstablished
CommittedChunk -> the input to the continuity derivation
SilenceProof is the one that matters. "The host produced no bytes" now cannot be SPELLED without a
token that only source_byte_fact mints, so the 2026-09-12 reading -- a quiet channel published as a
successful boot -- is unwritable rather than reviewed against.
THE REDS ARE EXECUTED, NOT DESCRIBED, and they are authorable exactly where DESIGN section 4b says to
look: as source handed to the compiler by a fixture. Four foreign-module fixtures, each refused on the
real acceptance path:
sole_constructor type 'SilenceProof' cannot be constructed outside its defining module
sole_constructor type 'DurableCommitProof' cannot be constructed outside its defining module
sole_constructor type 'ContinuityReach' cannot be constructed outside its defining module
sole_constructor type 'CommittedChunk' cannot be constructed outside its defining module
The positive controls are the twenty-seven witnesses, which still mint all four through the guarded
routes. A permanently-green check over a state nothing could express would have carried no
information; these refuse something that compiled an hour ago.
THE WITNESS CAN NO LONGER CHEAT EITHER, which is the part I got wrong last time. A helper named
committed_chunk_fixture_unreachable sat in the accepted witness module FORGING a CommittedChunk
whenever the real constructor refused -- a bypass inside the proof of the seal. It is deleted;
fixtures propagate the optional and a refusing constructor now FAILS the witness. The continuity
fixture can no longer author an offset either: to assert "verified through 100" it must produce a
hundred committed bytes and derive it, which is the seal doing its job to the test as well.
RUNG, RESTATED ON MEASURED EVIDENCE AND NOT ROUNDED UP. Before this commit the honest rung on the
silence path was MITIGATABLE, whatever the earlier claims said, because the arm was writable and the
guards were skippable. It is now STRUCTURALLY GUARANTEED for the four sealed arms: no accepted program
can spell them outside their owning modules, and that is established by refusal on the real path
rather than by argument. What remains outside the seal is stated plainly: a consumer can still author
its OWN vocabulary for an absence claim, which no seal here can reach.
Also: the run subject is now (machine, source stream). A collector SESSION change on one stream is a
continuity break attributed to CollectorSessionChanged -- not a caller error -- because a client
exiting and being relaunched is the most common real break and is this investigation's own case four
times over; a timeline asking whether a console was continuous must get back NO, BROKEN BY THE
COLLECTOR, rather than a caller error. Crossing a stream stays a caller error. The chunk's stream must
also agree with the authenticated binding, or the subject check refuses with ChunkStreamDisagrees.
Twenty-seven witnesses green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
…reported
TWO FRONTIERS WERE OVERSTATED, one of them by me in the same annotation that warns against it.
chunk_occurrence_eq was recorded as CONSUMED AND CLOSED because the interpretation lane reported
consuming it in its replay. That lane does -- on ITS branch. In THIS tree the only callers are the
definition, the annotation, and the witnesses, so "closed" described a tree that does not exist. It is
gunbc.recurring_failure_mode.unlanded_citation_indistinguishable_at_the_citing_end arriving through a
peer's MESSAGE rather than through a symbol: "it is consumed" becomes true the moment a lane authors
the caller, and is heard as "the tree carries it". The rule that survives is to say consumed WHERE.
The annotation even carried the warning that a frontier naming a non-consuming consumer reads as
closed, three lines from the claim it was describing. Both frontiers are now OPEN with capability
triggers.
continuity_from_committed_chunks likewise has no production caller in this closure. Worth separating
from the frontier, because it is true today: ContinuityEstablished carries a sole_constructor
ContinuityReach minted at exactly ONE site, inside that derivation, so an envelope's continuity cannot
be authored by a caller even while no caller exists. The frontier is about who will build envelopes,
not about whether the value can be forged.
AND A FINDING ABOUT THE SEALING MECHANISM ITSELF, measured because a fixture in the corpus suggested
otherwise. dag/test/fixture/sole_constructor_variant_probe declares `type SealedChoice sole_constructor
= SealedA { ... } | SealedB { ... }`, so a SUM may carry the keyword. It does NOT seal the arms: a
foreign module was handed to the compiler constructing such an arm, with the value CONSUMED by the
entry so it could not pass by being unreached, and it COMPILED. So `sole_constructor` on a coproduct
is a decoration for arm construction -- it parses and refuses nothing -- and the token-record approach
this branch uses (SilenceProof, DurableCommitProof, ContinuityReach) is not a workaround for a missing
feature but the only thing that actually seals. Sealing the sum directly would have produced a
permanently-green non-wall, which is the DESIGN section 4b decoration trap.
RUNG, STATED TO MATCH WHAT EXECUTES. The four seals are structurally guaranteed AS OF THIS COMMIT, and
their refusals were executed against the real acceptance path -- but the RED fixtures are NOT ENROLLED,
so nothing goes red if a sole_constructor is later deleted from one of these types. Section 4b's
fourth meta-obligation requires the discriminating RED to REMAIN enrolled on a climb; an
executed-but-unenrolled refusal establishes a rung for one moment and then decays silently, which is
the transcribed-measurement shape one level up. So the honest statement is STRUCTURALLY GUARANTEED,
RED NOT ENROLLED.
THE TRIGGER IS A NAMED, VERIFIED HARNESS RATHER THAN A WISH. gunbc.guarantee_probe_corpus already
carries a sole_constructor_cross_module_class with an ExpectBlockingRefusal row naming the
SoleConstructorViolation diagnostic, and its witness EXECUTES a census over fixture source and asserts
a blocking count of at least one -- so the route is real and running, not aspirational. What is missing
is four rows and four fixtures applying it to THESE types. That edit lands in its own change against
that shared carrier rather than riding along here, because it is a growth surface other lanes append
to and it deserves its own diff.
Twenty-seven witnesses green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
|
Review 64988 ran on 1. Continuity authorable on the envelope — fixed, by the second option you offeredYou wrote: "Either the envelope carries
The §3c half of your finding stands and is now stated rather than papered over: 2.
|
THE CLAIM THIS BRANCH MADE TWO COMMITS AGO IS WRONG AND IS WITHDRAWN RATHER THAN ADJUSTED. It reported
the four sealed arms as STRUCTURALLY GUARANTEED on the strength of four executed refusals. The
refusals are real and they establish exactly one thing: no foreign module can SPELL those arms. They do
not establish that no foreign module can OBTAIN them, and those are different propositions.
MEASURED, NOT ARGUED. A module contacting NO STORE AT ALL was compiled and run against the real
acceptance path. It authored CasCommitted { committed: CasSlotVersion { content: <a digest it chose> } }
-- std.durable_compare_and_set does not seal CasSlotVersion -- passed it to this module's admitted
local_commit_from_cas, received LocallyCommitted, minted a CommittedChunk over a chunk whose payload
digest it also chose, and reached a DerivedContinuity. Exit 0. No bytes were ever stored anywhere, and
every step went through a sanctioned entry point.
THIS IS AN ALREADY-FILED CLASS AND IS CITED RATHER THAN REFILED:
gunbc.recurring_failure_mode.admitted_call_edge_with_unrestricted_value_egress. .dag has no
module-private, so every exported function returning a value CARRYING a sealed type is another route to
it, and sealing the mint in turn only moves the proxy one hop. The fabric-M0 lane hit the identical
shape and recorded that the cascade terminates only at functions that carry nothing outward. For a
durable commit that means the standing must be produced by something that PERFORMS the compare-and-set,
never by a fold over an outcome a caller hands in -- which is the bound realization, explicitly not in
this slice.
THE HONEST SPLIT, and the two halves must not be blurred:
(i) cross-module LITERAL construction of the sealed arms -- STRUCTURALLY REFUSED, four executed REDs.
(ii) obtaining a commit standing with no store behind it -- MITIGATABLE, open, measured above.
The silence law rests on (ii), so the law's rung is (ii)'s and not (i)'s. Reporting the stronger half
as the class rung is the inflation DESIGN section 4b(1) forbids, and an inflated class never ranks for
climbing, which is the actual cost.
NEXT-RUNG TRIGGER, A CAPABILITY: a durable-commit route that performs the compare-and-set and returns
the standing, with NO caller-supplied outcome anywhere in its signature, sufficient that
LocallyCommitted cannot be reached without a store having been contacted.
TWO THINGS CHECKED AND DELIBERATELY NOT WRITTEN. The sole_constructor-on-a-coproduct hole I measured is
ALREADY DECLARED at v1.compiler.parse and measured by
test.claim.sole_constructor_completeness_audit_probe f13_variant_construction_refuses, which is RED --
so my measurement AGREES with the enrolled probe and there is no path disagreement to report. And the
remedy I reached by construction, sealing the RECORD an arm carries, is already recorded verbatim in
gunbc.recurring_failure_mode.subject_and_its_digest_as_independent_parameters, discovered independently
by the fabric-M0 lane with the same two-shape verification. Appending my receipt would duplicate a
finding, a remedy and a verification the corpus already holds, so nothing is appended.
Twenty-seven witnesses green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
CapturePersistenceRefusal, LocalCommitFailed and LocalCommitNotAttempted are used by retention_exposure and by the ForwardRefused arm, and were missing from the selective import block. The sibling arms of both types were listed explicitly beside them, which is what makes this an oversight rather than a convention: the block already named LocallyCommitted and all three Downstream arms. It was reintroduced when the retention fold was rewritten and cherry-picked back onto this branch. WHAT THIS DID NOT DO, stated because the review that found it drew the stronger conclusion: the module resolved, and both folds were executing. UnlistedImportUse is an ADVISORY diagnostic today, not a blocking one -- gunbc.compile_clean_diagnostic_policy compile_clean_unlisted_import_use_enforcement is FloorNotYet, whose own annotation says the resolver emits UnlistedImportUse while compile-clean does not red. So the symbols bound, the module resolved, and source_byte_fact and retention_exposure ran. Re-verified by execution rather than by reading that policy row: a four-witness entry exercising retention_exposure's ForwardRefused arm, the retention promise, the silence wall and its positive control returns ExitSuccess. It is fixed anyway, and not only for tidiness. That policy row exists because the enforcement is staged for promotion to GateBlocking, so an unlisted use is a defect with a scheduled red, and leaving it would be borrowing against a gate that is already declared. Twenty-seven witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
|
The observation is correct and it is fixed in The finding is right
The module did resolve, and both folds were executing
I did not want that to rest on reading a policy row, since the claim at issue is precisely "is this executing" — so I re-verified by execution. A four-witness entry exercising So the conditional in your finding — "If this module does not resolve, neither that fold nor I am flagging that specifically rather than just fixing the import, because a reviewer concluding "this does not resolve" from an import list is reading the declaration where the corpus's answer comes from the resolver, and here the two genuinely differ by policy. Fixed anyway, and not for tidinessThat policy row exists because the enforcement is staged for promotion to Merge-readiness note, since this review is REQUEST_CHANGESThe PR description was rewritten before this review ran and now states the silence law's rung as mitigatable, not structural, with both halves separated: cross-module literal construction of the sealed arms is structurally refused (four executed REDs), while obtaining a commit standing with no store behind it is open and measured — a storeless module reaches one through the admitted mint because — sent from snappy-bear-663 |
The module annotations asserted "four forged-literal fixtures are refused on the real acceptance path with SoleConstructorViolation". That evidence was not in the tree. The forges were run by hand in scratch files and deleted, so the sentences were TRANSCRIBED OUTPUT -- DESIGN section 6 forbids exactly that, and section 4b(4) requires a climb's discriminating RED to REMAIN ENROLLED. Nothing would have gone red if a sole_constructor were later removed from any of these types, which is the decay that makes an unenrolled refusal worth less than it looks. Four REDs, one per sealed record, each handing the compiler source that tries to build the forbidden state: the durable-commit proof, the continuity reach, the committed chunk, and the silence proof that SourceByteFact's one dangerous arm must carry. The fourth is the lane's whole purpose -- "the host produced no bytes" is now unspellable as a COMPILE REFUSAL rather than as a review comment. COUNTS ARE KEYED (class, subject_name, blocking), never by class alone, which the census module names as the exact form: CensusObserved carries every diagnostic the compile produced, the imported closure included, so a class-only count over a fixture importing production modules can be satisfied by an unrelated refusal elsewhere and a class-only zero is a property of the corpus. Each assertion is == 1 rather than >= 1, because exactly one refusal is the proposition and >= 1 would hide a second, unintended one on the same key. TWO GREEN CONTROLS, without which the REDs carry no information: a probe refusing because a module failed to resolve or a name was misspelled looks identical to one refusing because the wall fired. Each control imports the same modules and reaches the same types through the sanctioned route, drawing zero violations on the same key. And a seventh test asserts every probe ACTUALLY COMPILED, because keyed_count returns -1 on CensusNotRunnable and a probe that never ran would otherwise be indistinguishable from one that ran and found nothing. WHAT THIS FILE DOES NOT ESTABLISH, stated in it so it cannot be cited for more: the arms cannot be SPELLED. Whether they can be OBTAINED through an admitted mint whose own input is caller-authored is a different proposition, and they can be, because std.durable_compare_and_set leaves CasSlotVersion unsealed. That open half stays recorded at the carrier. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
SourceStreamRange carried first_offset: Nat beside length: ByteSize -- a flat scalar sitting one field away from its own counter-example, since the extent knew it was memory and the position did not. Found by review 65046 through the interpretation lane, which declined to mint a competing offset type or to take a rung drop, and asked the carrier to own it. Correct on both counts. A POSITION AND A QUANTITY ARE DIFFERENT KINDS. Position minus position is a quantity; position plus quantity is a position; position plus position is meaningless. Carried as raw counts all three are writable and only arithmetic distinguishes them. StreamPosition now carries the stream it is measured in, position_advanced_by is the only way to move one, and position_difference is the only way to subtract two -- there is deliberately no position addition. THE SHAPE IS std.measure ObservationInstant'S, DELIBERATELY, because that carrier already solved this for time: a point carries the DOMAIN it is measured in, and compare_instants refuses across domains rather than fabricating an order, since two readings from independently started clocks are the same basis and still not comparable. Two byte offsets in two different source streams are exactly that, so compare_positions returns PositionIncomparable across streams and every coverage and continuity comparison routes through it. A cross-stream comparison can no longer answer true by arithmetic accident -- it cannot answer at all. That also makes a property this branch previously CHECKED partly structural: a gap between positions in two streams has no extent to report, so gap_between yields a zero-length gap at the origin rather than a fabricated span, and the run-crosses-subjects refusal is no longer the only thing standing between a mixed run and a confident number. DFS BEFORE MINTING, per DESIGN section 2, and the interpretation lane did half of it independently: std.affine_space Point2/Point3 are spatial frames with signed frame components and a CoordinateFrameIdentity, not a one-dimensional byte position; std.measure owns the MAGNITUDE as ByteSize and carries no position concept at all; and no first_offset/byte_offset/StreamOffset carrier exists anywhere in std or extdeps. So this is a modeling obligation rather than an inhabitance failure. WHY THE HOME IS THIS MODULE AND NOT std.measure, stated so it can be revisited rather than assumed: std owns the magnitude and this adds the stream-relative point over it, whose only reachers today are this lane and the lane consuming it. ClockBasis's own note records that a home is chosen by who must reach it. If a third consumer appears with no SourceStreamId to hand, this hoists to std.measure as a point over a stream parameter and nothing here changes shape. Thirty-four witnesses green: the twenty-seven behavioural ones on positions, plus the seven enrolled seal probes, whose four REDs still refuse and two green controls still draw zero. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
…er claim Two follow-ups from the interpretation lane on the position carrier, both correct, and both the class this branch filed showing up in the code the branch added to fix another instance of it. CONTINUITY PROJECTED INCOMPARABILITY INTO A POSITIVE CLAIM. continuity_covers asked position_at_or_before, so PositionIncomparable collapsed into `false` and the answer came back ContinuityShortOfRange -- "verified only as far as X, short of Y" -- which asserts an ORDER between two positions that have none. Saying a stream is short of a mark in a DIFFERENT stream is worse than saying nothing: it is positive, plausible, and actionable. The fold now matches compare_positions directly and ContinuityCoverage carries ContinuityPositionsIncomparable, which SourceByteFact propagates as CoverageGapPositionsIncomparable rather than flattening at the boundary. gap_between FABRICATED A ZERO-LENGTH RANGE when position_difference was Absent, making three different situations one value: a genuine empty gap, a reversed pair, and two positions in different streams with no interval between them at all. It returns an optional now; both call sites refuse with RunPositionsIncomparable naming the two streams. The sibling allowed "unless construction makes this unreachable" -- it is arguably unreachable, since both positions are checked against the subject stream first, but an argument is not a constructor, and this branch has already been wrong twice about precisely that distinction. THE GENERAL SHAPE, since it is now three for three: a refusal arm survives only as far as the first Bool that reads it. Adding PositionIncomparable to compare_positions did nothing for any consumer that reached it through position_at_or_before, because that projection is where the distinction died -- the same way continuity_is_established and may_record killed theirs earlier on this branch. The carrier has to keep the arm all the way to the boundary a consumer reads, or the type is doing no work. Thirty-four witnesses green, including the four enrolled seal REDs and their two green controls. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
…e walk claiming an order TWO FINDINGS FROM REVIEW 65085, both correct, and the first is the worse one because it was silently degrading the evidence this branch rests on. THE TWO MOST LOAD-BEARING REDS HAD GONE STALE AGAINST THEIR OWN BRANCH. Commit 6d30414 retyped ContinuityReach.verified_through to StreamPosition and SourceStreamRange.first_offset to first: StreamPosition, and the forged fixture STRINGS kept the old field shapes. They still asserted one SoleConstructorViolation and still passed -- because the seal refuses during resolution, ALONGSIDE the now-present field error -- so the probes had stopped isolating the wall while staying green. A probe refusing for two reasons is not a discriminating RED for either. WHAT LET IT GO UNNOTICED IS THE PART WORTH FIXING: RED 2 and RED 4 had no sanctioned green control, unlike RED 1 and RED 3. This file's own header says a probe that refuses because a name was misspelled looks identical to one that refuses because the wall fired -- and then two of its four probes had nothing standing beside them to tell those apart. Both fixtures are retyped to the current shapes, and ContinuityReach and SilenceProof now have green controls on their sanctioned routes (continuity_from_committed_chunks and source_byte_fact), so a stale fixture turns the control red instead of hiding inside the RED. AND THE WALK WAS STILL CLAIMING AN ORDER ACROSS STREAMS. Both continuity folds guarded on !position_at_or_before, which collapses PositionIncomparable to false -- so two positions in DIFFERENT streams satisfied the overlap guard and the walk answered RunRangesOverlapOrReverse, a positive and actionable claim about an order that does not exist. Adding the incomparable arm to compare_positions bought nothing while a Bool projection sat in front of it. Both folds match the order directly now, and route incomparability to RunPositionsIncomparable. THAT IS THE THIRD TIME ON THIS BRANCH that a refusal arm died at the first Bool that read it -- continuity_is_established, then may_record and exclusivity_is_enforced, now position_at_or_before. The rule the branch keeps relearning: typing the producer does nothing if any consumer reaches it through a projection that cannot express the refusal. Thirty-six witnesses green, including four seal REDs and their now-four green controls. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
(cherry picked from commit 666a0ad)
…sed, and drop its wildcards The interpretation lane found a third live instance of the same collapse, this time in source_byte_fact itself: continuity can legitimately cover a requested range in stream B while the chunk is in stream A, after which position_at_or_before and range_covers both answered false and the fold minted CoverageGapRangeNotCovered -- a positive claim that the committed range fails to cover the requested one, when the truth is that the two cannot be compared at all. Their carrier fix is cherry-picked (666a0ad) and its counterexample is a real one: continuity derived over a foreign stream, a chunk in the local one, asserting both identities survive to the boundary. THEY SENT IT UNEXECUTED AND IT DID NOT PASS, which is why it was run before being trusted. THE FAILURE WAS MY FIXTURE, NOT THEIR TEST. t_committed_chunk_on_stream set source: stream while building its range through t_range, which anchors positions to t_stream -- so a chunk declaring itself foreign carried positions in the local stream, a state the production types do not intend to represent. Every earlier use tripped the source-stream check first and never reached a position comparison, so the inconsistency was invisible until a test needed a chunk that was genuinely and consistently foreign. The helper now anchors its range to the stream it is given. AND THE FIX ARRIVED WITH WILDCARD ARMS, which are replaced. `_ =>` absorbing PositionBefore and PositionSame is the shape this branch has spent its whole length removing -- it is correct today and it silently swallows whatever arm PositionOrder gains next, which is exactly how the incomparable case got lost three times already. Both matches name all four arms; the fold now contains no wildcard. Thirty-seven witnesses green, including the lane's cross-stream counterexample and its same-stream positive control. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
…urface range_covers had NO CALLER ANYWHERE -- not production, not a witness, only its own definition. And position_at_or_before, which maps PositionIncomparable to `false`, was reached only by that dangling function and one test helper. So the instrument that CAUSED the collapse this branch files as a class was left exported, where the next caller reproduces it, while the three folds that used to call it were repaired one by one. WORSE, AND THIS IS THE PART TO OWN: the justification given for keeping position_at_or_before was that it is honest at sites where "does not cover" is the right answer for two streams, and range_covers was named as such a site. range_covers has no callers. The site cited to justify the projection was itself dead, so the argument was empty when it was made. Both halves of the filed class in one pair of declarations: an unconsumed projection, unconsumed PRECISELY BECAUSE every consumer needs the arm it discards. The row's own recognition rule says the dangling and the erasure are the same finding seen from two ends, and here they were the same two declarations. Deleted rather than frontiered. There is no consumer to name and no trigger that would close one -- a caller wanting coverage matches compare_positions and says what an incomparable pair means for its own question, which is three lines at the call site instead of one, and the three lines cannot quietly answer `false` for two different streams. The witness that asserted positional equality through two Bool calls now matches the order and names all four arms. This module's exported surface now contains no Bool over PositionOrder. Thirty-seven witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
|
Correct, and fixed in Both are deleted
So the instrument that caused the collapse this branch files as a class was left in the exported surface, where the next caller reproduces it, while the three folds that called it were repaired one at a time. And the argument for keeping it was circular. I wrote, in a message on this PR, that Both halves of the filed class in one pair of declarations: an unconsumed projection, unconsumed precisely because every consumer needs the arm it discards. The row's own recognition rule says the dangling and the erasure are the same finding seen from two ends — here they were literally the same two declarations. Deleted rather than declared as a frontierThere is no consumer to name and no trigger that would close one, so a frontier would be the false-closed shape flagged earlier on this PR. A caller wanting coverage now matches The witness that asserted positional equality through two This module's exported surface contains no Bool over Count, for the recordFive removals of this class on one branch: Thirty-seven witnesses green, including the interpretation lane's cross-stream counterexample and the four enrolled seal REDs with their four green controls. — sent from snappy-bear-663 |
supervision_coverage answered WindowCovered for a pipe watched THREE SECONDS of a four-hundred-and- twenty-second window. Both drain arms discarded their instants and returned covered whenever the child closed at its deadline. That is the 2026-09-11 failure exactly -- three seconds of four hundred and twenty, reported as all of them -- reappearing in the supervision module this branch added to make it structurally unwritable. Found by review 65128 through the interpretation lane. THE CONFLATION: ClosedAtDeadline establishes THE DEADLINE ENDED THE CHILD. It says nothing about how long anyone READ THE PIPE. A child can run its full window while its output goes unread after three seconds, which is a collector-side miss and the one this lane exists to surface. AND THE CARRIER COULD NOT EXPRESS THE FIX. DrainedDuringOperation held only last_progress_at -- WHEN BYTES LAST ARRIVED -- and no watch bound at all. Those come apart exactly where it matters: a pipe whose last byte arrived at three seconds and was then abandoned is indistinguishable, on that field alone, from a pipe watched to the deadline that simply went quiet at three seconds. last_progress_at is not watch coverage and is never used as one; it stays because it is a real observation about the SUBJECT. watched_until is added beside it and is what coverage reads. THE COMPARISON GOES THROUGH std.measure compare_instants, so a watch bound and a deadline with no shared origin yield WindowCoverageUndecidable rather than a fabricated verdict in either direction. Undecidable is not coverage AND not a collector failure; it is the honest state when two readings cannot be ordered. ClosedAtDeadline now carries the deadline it closed at, so coverage compares against THE SAME instant the disposition was decided by. Passing the deadline to the coverage fold as a second parameter would have reintroduced a caller-supplied input on a guard -- the defect this branch has already removed twice -- so the value travels in the disposition instead. DISCRIMINATING CONTROLS: a child that ran its full deadline with a pipe watched for three seconds must answer WindowNotCoveredPipeUnwatchedToDeadline naming both instants, while the watched-to-deadline case answers WindowCovered; and a watch bound on a foreign clock answers undecidable rather than either. Verified by mutation -- making the before-deadline arm return WindowCovered turns w_a_pipe_watched_for_three_seconds_does_not_cover_the_window red and nothing else. Thirty-nine witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
… EOF again The range_covers / position_at_or_before deletion rationale sat at end of file with no module item after it, which section 4c refuses. The interpretation lane caught it -- trailing orphan annotations had already blocked their stack in CI -- and moved it above range_end on their side; it is moved here too, so the carrier does not keep re-emitting the defect into every consumer that merges it. SECOND TIME IN THIS SESSION, SAME SHAPE, AND THE LESSON IS THE ONE ALREADY WRITTEN DOWN: deleting a declaration leaves its explanation with nothing to attach to. The first instance was the exclusivity_is_enforced rationale. The check that catches it is a tail read after any deletion, which exists and was not re-run after this one. WHAT MAKES IT WORTH A COMMIT MESSAGE RATHER THAN A QUIET FIX: the local interpreter does NOT refuse on a trailing annotation. Thirty-nine witnesses ran green over this file in exactly this state. Only the CI witness lane refuses, before execution, so a green local suite carries no information about annotation placement at all -- and a carrier that lands in this state fails every downstream lane that merges it, not just its own. The rationale is now above range_end, where the coverage question it describes lives. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
…ntrol encoded the hole Review 65170, and it is the deepest finding on this branch because it lands on the positive control for the wall the PR is named for. THE ASYMMETRY: once ContinuityCoversRange held, a NON-EMPTY chunk had to cover the requested end; an EMPTY one did not. So a zero-length chunk took the silence arm on the strength of envelope.continuity alone -- a separately authored field -- rather than on this chunk accounting for the range asked about. The seal on SilenceProof only stops the arm being SPELLED; it never bound the evidence to the chunk. AND THE GREEN CONTROL WAS BUILT ON EXACTLY THAT. The "full evidence" silent envelope paired a zero-length chunk with t_reach(through: 100), a reach DERIVED FROM A DIFFERENT hundred-byte committed chunk, and minted SourceProducedNoBytesInRange over [0,100). Continuity advanced by positive-length committed windows is evidence those offsets WERE captured; attaching it to an empty chunk is a quiet reading fabricated from somebody else's bytes -- this lane's founding class, sitting inside the witness that was supposed to prove the wall real. Its continuity is now derived from its own empty chunk. THE CONSEQUENCE LOOKS LIKE A LIMITATION AND IS THE MODEL BEING HONEST. Offsets here ARE byte positions, so a covered range of length L necessarily CONTAINS L bytes; a zero-length chunk covers no width, and SourceProducedNoBytesInRange over a wider range is not something a single-chunk envelope can support. It never could. The missing check was hiding that rather than enabling it, and the claim that needs a committed RUN is now visibly the run's to make. REACH MUST EQUAL THE REQUESTED END, not merely pass it, because continuity verified FURTHER says the stream DID advance beyond the range and those bytes are not in this envelope. TWO CONTROLS, AND THE SECOND EXISTS BECAUSE THE FIRST DID NOT REACH THE GUARD IT WAS CITED FOR. The borrowed-reach witness is stopped by the END check, so mutating the reach guard left it green -- an unexercised control cited as evidence, the defect this branch keeps finding elsewhere. The second takes the degenerate request at the empty chunk's own position, which passes the end check and does reach the guard; mutating that guard turns it red and nothing else. Forty-one witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
|
Both findings are correct and both are fixed in 1. The asymmetric guardConfirmed exactly as described. Once You are also right that the seal did not help here: 2. The green control encoded the holeThis is the one that matters. The "full evidence" silent envelope paired Continuity advanced by positive-length committed windows is evidence those offsets were captured. Attaching that to an empty chunk is a quiet reading fabricated from somebody else's bytes: this lane's founding class, sitting inside the witness that was supposed to prove the wall real. Your sentence — "this control cannot green without the mismatch" — is exactly right, and it had been green since the arm was introduced. The silent envelope now derives its continuity from its own empty chunk. The consequence, stated rather than hiddenOffsets here are byte positions, so a covered range of length L necessarily contains L bytes. A zero-length chunk covers no width, and I also added: reach must equal the requested end, not merely pass it. Continuity verified further says the stream did advance beyond the range, and those bytes are not in this envelope. Two controls, and why the second existsThe borrowed-reach witness is stopped by the end check — so when I mutated the reach guard, it stayed green. An unexercised control cited as evidence for a guard is precisely the defect I have been reporting in other people's code all night, and I nearly shipped it. The second control takes the degenerate request at the empty chunk's own position, which passes the end check and does reach the guard. Mutating that guard turns it red and nothing else. Both guards now have a control that actually reaches them. Forty-one witnesses green. — sent from snappy-bear-663 |
(cherry picked from commit b594c9a)
TWO FINDINGS FROM REVIEW 65248, both correct. THE SEAL TEST FORKED A DECLARED AUTHORITY. census_of / keyed_count / seal_violations re-implemented "compile this source string and count the blocking diagnostics of class C at subject S, -1 when the census did not run" -- which is gunbc.compile_census_probe blocking_subject_count_for down to the -1-never-0 rule AND the reason for it. That module's header says outright that it is THE SINGLE HOME for this fact and that copying it makes one concept answer from two authorities. Four witnesses already consume it; this is the fifth. The local trio came from copying the SHAPE of a sibling seal battery rather than asking where the fact lives -- and it was written in the same session where StreamPosition got a careful DFS through std.affine_space and std.measure before minting. The discipline was available and applied to the type and not to the helper, which is worth recording because that is how forks actually happen: not from ignorance of section 3 but from pattern-matching a neighbouring file. Re-verified by mutation rather than assumed semantics-preserving: unsealing SilenceProof still turns RED4 red through the shared helper. THE OWNERSHIP FOLDS HAD NO FRONTIER. acquire_ownership and release_ownership have no production caller, and unlike every sibling in this change they carried no frontier statement -- while being the folds that encode the Mt. Collins receipt most directly, where a stale collector of the observer's own held the console session and the replacement never started. An unstated frontier reads as an oversight rather than a decision. CONSUMER: the enrolled collector service's attach and release steps. TRIGGER, AS THE CAPABILITY: that service performing attach and release through these folds against a real controller session, sufficient that a stale session observed on the endpoint yields ForeignInteractiveSessionNotStolen from a real observation rather than a fixture, and that a release which is not the holder's refuses against a real lease. Separated from the frontier and true today: the refusals are total, so no caller can obtain an ownership change without one of the four observed transitions or a typed refusal. Forty-one witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
|
Both findings correct, both fixed in 1. The seal test forked a declared authority
Worth saying how it happened, because it isn't ignorance of §3: I copied the shape of a sibling seal battery ( Re-verified by mutation rather than assumed semantics-preserving: unsealing 2. The ownership folds had no frontierCorrect, and the asymmetry you name is the tell — Consumer: the enrolled collector service's attach and release steps — the thing that takes the endpoint before a stimulus and hands it back after, which this slice deliberately does not build. Trigger, as the capability: that service performing attach and release through these folds against a real controller session, sufficient that a stale session observed on the endpoint yields Separated from the frontier and true today: the refusals are total, so no caller — present or future — can obtain an ownership change without one of the four observed transitions or a typed refusal. The frontier is about who calls them, not about whether they can be bypassed. State41 witnesses green. CI went fully green on — sent from snappy-bear-663 |
collector_host_loss_refusal answered the Absent case with the literal "no collector-host-loss promise is rostered" -- a literal HERE, three lines below this module's own law that the refusal text comes from the roster and never from a literal here. The law was written and then broken inside the same fold. AND IT WIDENED RATHER THAN REFUSED, which is the part that matters. The return type was NonEmptyStr, so the fold had no way to SAY nothing was rostered: the unrostered case was carried out in the refusal field of ExposedToCollectorHostLoss, where a consumer reads it as the rostered promise text. A plausible sentence standing where a typed absence belongs is the absent-reads-as-present shape this branch filed, arrived at through a field whose type could not express the absence. retention_exposure passes the constant roster today, so the arm is unreachable through it -- but this fold is EXPORTED and takes the list as a PARAMETER, so any caller reaches it. "The current caller happens not to" is a property of callers, not of the type, and this branch has already been wrong twice on exactly that distinction. The fold returns NonEmptyStr? and RetentionExposure gains RetentionPromiseUnrostered, so the absence is named where a consumer reads it. ALSO: a duplicated conjunct in the supervision witness, pipe_unread over the same disposition twice in one chain -- the same shape as the seven duplicate arms removed in 0655668, from the same cause, a bulk edit applied twice. A scan for duplicate arms and duplicate conjunct lines across all four witness files now reports none; the one line it flagged is two different tests with different fixtures sharing a call, checked rather than assumed. Forty-one witnesses green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj
|
Both correct, both fixed in The unrostered promise was widened into the field a consumer readsYou located it precisely, including the part I'd have argued past: the The widening is the substance. The return type was
On reachability, and I want to agree with your reasoning rather than lean on the mitigation: The duplicated conjunctCorrect, and the same cause as the seven arms in I also ran a scan across all four witness files for duplicate match arms and duplicate conjunct lines rather than fixing only the one you named. It reports none. The single line it flagged turned out to be two different tests with different fixtures sharing a call, which I checked rather than assumed — the scan is line-based and can't see scope. 41 witnesses green; CI went fully green on — sent from snappy-bear-663 |
The acquisition half of the fleet-lifecycle observation slice: the model that makes a negative observation about a source cost evidence rather than an assertion. The interpretation lane (royal-gull-60) owns the other half.
Correcting a claim an earlier revision of this description made. It said the interpretation half "already consumes this — it imports
commit_attests_chunkandcontinuity_coversrather than duplicating them." That is not true of the tree. Measured againstorigin/main, #11211 adds all eight of these files itself and declares its owncommit_attests_chunkandcontinuity_covers— two branches, two copies, one concept, which is the §3 fork. What was true is that the interpretation lane's working tree imports them, because it had merged this branch; I reported that as a fact about the corpus. That isgunbc.recurring_failure_mode.unlanded_citation_indistinguishable_at_the_citing_endone level up — "it is consumed" is true the moment a lane merges you, and is heard as "the tree carries it". The rule is to say consumed where, and I did not.The current position: the interpretation half carries its own copy and has been asked to drop it in favour of this module. Two of the eight differ, and this copy is the one to keep — it states the §3c frontier for
acquire_ownership/release_ownershipwith its trigger, and itscollector_host_loss_refusalreturnsNonEmptyStr?with aRetentionPromiseUnrosteredarm instead of the literal"no collector-host-loss promise is rostered", which is the absent-reads-as-present defect this branch filed.Read the rung section before the rest. This lands at its honest rung, and the honest rung for the law the PR is named for is mitigatable, not structural.
Why
On 2026-09-11 a SOL collector reported its own 86-byte client banner as host silence for a week. Eight captures, seven byte-identical across materially different subjects — three of which reached different boot outcomes, one of which executed a kernel. Three hand-rolled replacements each failed differently: stdin EOF exiting rc=0 at three seconds inside a 420-second window; a deadline SIGTERM killing
scriptbefore it flushed; and attaching after the phase the capture needed. Then a quiet SEL was read as a successful boot and published as established, withdrawn the same day inbf4cac9440.Every one is a timing assumption standing where an observation belonged —
gunbc.recurring_failure_mode.empty_capture_read_as_clean_result, seventh instance.Four modules
collector_ownership— ownership generation isstd.temporal_effectLeaseEpoch.generation; no second lease authority. Acquire / renew / take over / release are four observed transitions, and only the holder may release. A foreign interactive session is never stolen, and "somebody else has it" stays separate from "I cannot tell who has it" — opposite remedies. An owner over an unfenced endpoint records, but exclusivity is a fact read offEndpointFencing, not a claim, because IPMI arbitration belongs to the controller.capture_chunk— occurrence identity is(session, ownership generation, receive sequence)and deliberately not the digest: equal payload hashes across separate occurrences are not duplicate events, which is exactly what the seven identical captures were. The commit receipt must attest this chunk, verified throughcompare_content_hash. Continuity is derived by walking committed chunks — overlap, reversal and out-of-order refuse; a hole is a gap.collector_supervision— a zero exit code is not an expected closure. The deadline order is derived from twoObservationInstants, so a clean exit before the deadline isInterruptedBeforeDeadline— the three-seconds-of-four-hundred-and-twenty defect. Incomparable clocks returnSupervisionUndecidable.DrainNotObservedfails coverage even for a full-deadline child, because an unread pipe stalls the writer: the collector can cause the silence it reports.observation_envelope— the published interface. Local durable commit and downstream acceptance are separate fields. There is no fold from a timestamp to an association and no nearest-timestamp constructor.Gap causes have two sides
ContinuityBreakCausewas entirely source-side, so a gap caused by the collector dying, detaching, losing its lease or stalling had nowhere to land and could only be reported as the host's fault — this investigation's founding failure written into the vocabulary. It now carries both sides, andGapCauseUnattributedis the default: a walk over offsets sees bytes missing and cannot see why, so the derivation attributes nothing. A collector that lost and retook the endpoint isCollectorLostOwnership; a session change on one stream isCollectorSessionChanged, because a client exiting and being relaunched is the most common real break and is this lane's own case four times over.Rung — mitigatable, and why
SourceProducedNoBytesInRange,LocallyCommitted,ContinuityEstablishedandCommittedChunkeach carry asole_constructortoken, and four foreign-module fixtures are refused on the real acceptance path (sole_constructor type <X> cannot be constructed outside its defining module).That is not enough, and an earlier revision of this PR claimed it was. A module contacting no store at all was compiled and run: it authored
CasCommitted { committed: CasSlotVersion { content: <a digest it chose> } }, handed it to the admittedlocal_commit_from_cas, receivedLocallyCommitted, minted aCommittedChunk, and reached aDerivedContinuity. Exit 0, every step through a sanctioned entry point.Unspellable is not unobtainable. The two halves must not be blurred:
The silence law rests on the second, so the law's rung is mitigatable. The earlier structural claim is withdrawn rather than adjusted, because it was wrong when written; §4b(1) exists because an inflated class never ranks for climbing.
This is the already-filed
gunbc.recurring_failure_mode.admitted_call_edge_with_unrestricted_value_egress, cited not refiled:.daghas no module-private, so every exported function returning a value carrying a sealed type is another route in, and sealing the mint only moves the proxy one hop.The upstream half, outside this lane's authority:
std.durable_compare_and_setleavesCasSlotVersionunsealed, which is the hop that lets a storeless caller mint a commit. It is noted here rather than worked around locally.What is not built, and it is one trigger, not two
No realization is bound to a real process or a real store, so failed spawn, premature EOF and sink refusal have not been injected through one. The folds are proven to discriminate by mutation — that is evidence about the folds, not about
execve.That gap and the egress route above have the same root: the realization that performs the compare-and-set is also what closes the egress. So there is one trigger, stated as a capability:
The seal REDs are enrolled and executing on a required lane. An earlier revision of this description said "RED not enrolled", which was true when written and is now stale in the understating direction.
test.claim.fleet_observation_sealcarries the four forged-literal REDs, four green controls on the sanctioned routes, and a probe-actually-compiled guard; the required floor job of a green run executes them (a_forged_silence_proof_is_refused_at_compileappears in that job's log). Deleting asole_constructornow turns a RED's== 1into0and reds the floor, which is the decay §4b(4) requires a climb to be protected against.What a follow-up still owes is narrower than first stated: enrolled coverage of the egress route — obtaining a sealed arm through the admitted mint — not the literal forge, which is covered here.
Evidence
Twenty-seven witnesses green through the interpreter, with discriminating mutations run against the real folds and reverted — empty payload short-circuiting to silence, equal payloads collapsing to one occurrence, dropping the continuity-reach guard, a commit always claiming to attest, subject-agreement always passing, a zero exit trusted as a closure, an unwatched pipe counting as coverage. The positive control establishes silence is mintable on full evidence, so the refusals discriminate.
Every witness value is synthetic and declared in its witness module; nothing reads a real chassis, controller or capture.
Composition delta
Empty — all files under
dag/; nosrc/v1, no compiler manifest, nostage0, noCargochange.Landing is held: do not merge; the lane's parent takes the landing ask to the operator.
🤖 Generated with Claude Code
https://claude.ai/code/session_013bcRGT234VmvRT4skQ8hYj