Repository navigation
FLOOR-ROUTE-GAP-SELF-HOST: publish the executing route family that discharges the self-host behavioral witnesses from route_gap_held (49 required / 112 full) - #10188
Conversation
…s before extracting The anti-collapse count the convergence receipt requires, taken BEFORE any extraction so the post-extraction cause count has something to be measured against. 18 distinct causes deduplicated by remedy, with the three binding mismatches kept apart as 7a/7b/7c. It found the collapse in the opposite place from the one assumed: seven of the eighteen remedies are typed causes in local_repo_wet_terminal and detail-string payloads in floor_wet_route, and five more exist only in the Rust reader with no .dag spelling. The extraction therefore widens the transported route to main's grain and must not narrow main's seven causes to meet it. It also records that the terminal vocabulary is neither module's to mint: floor_terminal_ledger already owns the terminal, observation, expectation and thirteen dispositions, is imported by the conflicted consumer, and already derives PassedOverBudget/KnownRedNowPassing by expectation -- the same rule both wet modules re-derived independently. Three arrivals at one distinction is the proven coincidence DESIGN asks for before unifying vocabulary. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…th a typed binding The shared interface both wet routes will consume, and the reason it mints no terminal type of its own. WHAT IT IS NOT. It does not introduce a third terminal vocabulary. Two parallel ones is the fork being closed, so a third would be the same failure wearing a new name. v2.workflow.floor_terminal_ledger already owns the raw attempt terminal, the observed-verdict versus unreadable-observation split, the expectation, and thirteen derived dispositions -- and floor_changed_witness, the fold both routes feed, already imports it. This module imports that vocabulary and asks claim_disposition whether a terminal meets its expectation rather than deriving it again. That reuse is grounded in a PROVEN COINCIDENCE, not in taste: four independent arrivals at one distinction. The ledger derives PassedOverBudget and KnownRedNowPassing from a completed-past-limit terminal by expectation; the floor's seed keeps completed_over_cost_requirement apart from interrupted_before_verdict; local_repo_wet_terminal un-collapsed LocalRepoWetCompletedOverBudget out of its nonterminal arm; and floor_wet_route separated cost debt from no-verdict the same week. None of the three read the others, and none imported the fourth. THE LOAD-BEARING PIECE IS THE BINDING. local_repo_wet_terminal compared a candidate: String with ==, which DID decide admission -- so it was a validity key, not provenance -- but a bare String cannot say WHICH relation produced it. The binding is now two arms, deliberately asymmetric: a co-resident execution binds to the prepared subject and nothing else (executor identity and freshness are meaningless for a run inside the floor), while a transported receipt binds to the semantic subject AND the executor contract, because a receipt produced by a different executor over the same tree is a different evidential fact. The executor contract is a required field, not an optional one: an absent one has no constructor and cannot be defaulted permissively. Twelve typed causes, none collapsed. The three binding mismatches stay three, and evidence of the WRONG KIND is its own cause rather than a digest that happens to differ -- the case a String comparison could only ever report as "not equal". EVIDENCE. Eight witnesses green by execution, each RED paired with a control differing by exactly the fact under test. Then a mutation to prove they discriminate rather than merely pass: short-circuiting wet_binding_causes to return no causes turns exactly the three binding witnesses RED and leaves the other three GREEN. Predicted before the run, three red three green observed. A suite that went fully red would be entangled; one that stayed green would be inert. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
A live defect in 3270fea, found in review and confirmed by count: `dry_source` occurred EXACTLY ONCE in wet_evidence.dag -- its own field declaration. Nothing read it, and wet_evidence_validate did not consume it. Two consequences, both of which DESIGN names: `route` and `dry_source` varied independently, so the type admitted two states with no referent -- a co-resident execution after a deliberate wet decline, and a transported receipt after an observed hermetic route gap. The dry-source distinction was therefore COMMENTARY the realization could contradict, which is validation standing where construction was available (section 5). And a data row whose only function is to say something is the misplaced prose section 4c forbids. The field asserted an antecedent no executing consumer read. THE REPAIR IS STRUCTURAL, NOT A CHECK. `WetRouteAntecedent` fuses the two facts into one coproduct -- LocalRepoAfterHermeticRouteGap | SelfHostAfterDirectWetDecline -- and the route becomes a total PROJECTION of it rather than a field beside it. The invalid combinations now have no constructor, so there is nothing left to validate: rung 4 rather than the rung 2 an exhaustive WetRouteDrySourceMismatch refusal would have bought, and it costs no witness because no invalid state survives to witness. ONE WITNESS IS ADDED, for the residue the type cannot close. A TERMINAL's route is an execution fact, not a schedule fact, so a terminal claiming a different route than its schedule derives must still refuse -- a cause that had no witness before this commit. Nine witnesses green by execution. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
Picks up #10000, which regenerated the stale gunbc.rust_source_type_bindings stage0 mirror. The regen phase was failing on this branch for that reason and not for anything this branch changed: main's own run 33589101464 (head 39b0eb8) fails the identical phase on the identical file, and that run contains none of this branch's code.
…ter independent of the antecedent The first repair fused `route` and `dry_source` because they were adjacent IN THE TYPE. The third fact entered through a different door -- as an ARGUMENT -- and fusing a coproduct does not close a parameter. `wet_evidence_validate` took `required: WetEvidenceBinding` with nothing joining it to the schedule's antecedent, so this batch was constructible and ADMITTED: a schedule whose antecedent is `LocalRepoAfterHermeticRouteGap`, a required binding of `TransportedReceiptSubject`, and terminals carrying that same transported binding. Every pairwise check passed -- the terminal's route matched the schedule's antecedent, and the observed binding matched the required binding -- so a co-resident schedule was satisfied by transported evidence. The inverse was equally writable. `WetBindingRelationMismatch` never fired because it compares OBSERVED against REQUIRED, and those two agreed; what disagreed was ROUTE against REQUIRED RELATION, and they never met. The repair is structural rather than a fourth validator: `WetEvidenceRequirement` is one authority per batch, and route, antecedent and required binding are ALL derived from it totally. There is no longer a way to say "local schedule, transported requirement" because the requirement IS the route. `WetScheduledClaim` loses its `antecedent` field; the batch supplies it. `WetTerminalRow` KEEPS `route` as an independent execution observation. Deriving that one away would make the foreign-route refusal unauthorable -- a check whose RED cannot be written, which DESIGN section 4b calls a decoration rather than a weak wall. The schedule's route is derived; the observation's route is carried; the join between them stays load-bearing. Two consumer rules land in the module rather than only in review prose: validate one batch PER REQUIREMENT and never concatenate the routes, because the two require different binding relations and a merged call would have to weaken the requirement to admit both -- widening instead of refusing. And `WetEvidenceRefused` is not read wholesale as "receipt invalid": the verdict-not-expected arm means the evidence is VALID and the outcome is known, so a valid FAILING attempt stays publishable, or latest-attempt degrades into latest-SUCCESS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…d the ledger vocabulary Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…s own cycle argument
…sion/snappy-koi-879-wet-evidence-extraction
…hten two witnesses that claimed more than they asserted Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…ually authorable Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…o longer describes the head Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…call shape Both defects were authored today and both were found by execution rather than review: the DESIGN 4c annotation-placement rule refuses a // block inside a declaration body, and fold_list is declared (xs, empty, cons) rather than the (xs, init, step) I invented. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…serving every wall The seed's local_repo_wet_schedule reads the .dag roster through the interpreter and decodes it by type and field NAME, so the migration broke it in four places. CI caught this on both heads; no .dag witness could, because they construct fixtures directly. Walls preserved rather than ported: the identity/function agreement check is now a direct comparison of the two spellings the row carries rather than a suffix-strip, and the expectation arm still refuses everything but the one arm this lane realizes -- ClaimExpectation has two arms where its predecessor had one, and a wider type is not a wider capability. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…d by identity
The wave-admission phase refused both attempts with 57 unadjudicated deltas -- every one
a TargetChanged binding reading base {v2.workflow.required_floor} -> head
{v2.workflow.floor_terminal_ledger}, verified as the only shape in the report. That is
this PR's own move, and the roster's documented closure is to author a row per delta.
Enumerated, not patterned: 57 deltas, 57 rows, each naming its module, declaration and
spelling. The rows go stale the moment this merges and MUST be deleted in the first PR
after it lands -- a stale row refuses every unrelated PR in the repository.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…9-safety-vocabulary-move # Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
…sion/snappy-koi-879-wet-evidence-extraction
Main's seventeenth dissolution swept this roster to empty. My conflict resolution kept main's receipt prose but re-opened the const with the whole of my side's row list, which still carried the four dissolved rows -- so it reinstated a permission nobody re-authored and the wave phase reported them CONSUMED and refused. That is precisely the failure a conflict invites: a resolution in my favour restoring what the other side deliberately removed. The 57 rows themselves adjudicated correctly in that same run: 0 unadjudicated deltas. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…sion/snappy-koi-879-wet-evidence-extraction
…9-wet-evidence-extraction
The trigger read '#10077 MERGING ... once that PR is in main'. That was accurate when authored and became ambiguous the moment #10077 landed (a4a6db1, 18:55:08Z): a future-tense trigger gives a later reader no way to tell whether it has fired, and the next toucher pays for the ambiguity rather than its author. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…red and this change is the roster-touch that owes it #10077 merged as a4a6db1, so main carries the relocation and no run after it can produce those deltas. Run 33694346070 (on the merge commit 2b3b841) reported all 57 CONSUMED while still ADMITTING, because that commit does not touch this roster; the SJT-1 cohort's refusal states the charging rule exactly -- consumed rows are "due for deletion on this roster-touching change". Re-tensing the trigger touched the roster, so the obligation landed on the change that went looking for it. The roster returns to empty, which is not permissive: a real delta still refuses as UNADJUDICATED. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
…o host-probe rows across the roster's shape migration main's #10055 added two rows in the OLD shape (`LocalRepoWetScheduled`, a qualified `identity` string, `expected: LocalRepoWetExpectPassed`) to the same roster this branch migrates to `WetScheduledClaim` / `WitnessIdentity` / `expectation`. The conflict is that shape change meeting new members, so the resolution ports both rows into the new shape rather than choosing a side: their authored module_path and function are preserved verbatim, since which witnesses that lane admits is #10055's authority and not this branch's. The membership prose auto-merged to THIRTEEN MEMBERS IN THREE GROUPS and the roster now holds thirteen rows, so the count and its prose agree. No consumer hardcodes the old count; the roster's identity/function agreement witness covers the new rows unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
|
Closing: this PR would change nothing, and its content is already on main. Auto-opened by the session dashboard on a branch whose work landed as #9975 (squashed as The instrument for "what would merging this do" is neither diff, but the merge result itself: The merge result is byte-identical to current main: merging this would add nothing and delete nothing. Closed because it is empty, not because it is unsafe — an inert PR carrying an open work item's title is a false signal on the board for whoever reads that title next. The branch is spent; the remaining work in the sequence (#9725) proceeds on its own head from — sent from snappy-koi-879 |
Auto-opened by session-dashboard for session
snappy-koi-879.Pushing to
session/snappy-koi-879-wet-evidence-extractionadvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan