Repository navigation
F1 REST transport replay seam - #7610
Merged
briansrls merged 2 commits intoAug 1, 2026
Merged
Conversation
gunbai-bot
Bot
changed the base branch from
main
to
session/proud-swift-104-restoutcome
August 1, 2026 18:27
gunbai-bot
Bot
changed the base branch from
session/proud-swift-104-restoutcome
to
main
August 1, 2026 18:27
gunbai-bot
Bot
changed the base branch from
main
to
session/proud-swift-104-restoutcome
August 1, 2026 18:31
gunbai-bot
Bot
force-pushed
the
session/quiet-hawk-556
branch
from
August 1, 2026 18:32
a88cef7 to
601870b
Compare
briansrls
pushed a commit
that referenced
this pull request
Aug 2, 2026
… replay seam (#7600) * Model a REST response that is not 2xx as an answer, not an absence Service operations already declare what each status yields — github.Pulls.List declares 200/401/404/422/5xx, and twenty-two other extdeps modules declare 204 such arms between them. The v1 seed parses every one of those declarations onto the operation node as a response_<status> property and then never reads it: dispatch_rest raises InterpError::TypeError with a rendered "HTTP {status}: {body}" string for anything at or above 400. So a caller cannot reach the status, cannot reach the body, and cannot persist either without parsing a diagnostic written for a human. This lands the type the realization will project into. Four states rather than three: a transported request that was answered with a non-success status keeps both the status and the body it arrived with, because the body is usually the only place the remote says why; a request that never transported has no status at all, so none is invented; and a status that arrived over an unreadable payload is its own arm, so an unreadable body is never reported as an empty one. status is std.types HttpStatus rather than a fresh Int — the range already has one authority — and RestTransportRefused deliberately carries no status, since a sentinel zero would be a plausible-looking value standing where the honest answer is that the question does not apply. No realization consumes this yet, and the scope is stated on the carrier so it cannot be misread as complete: the outcome is opt-in per operation, and a refusal body stays a String rather than being decoded into the shape the response block already names. Both dissolve when the response block becomes the single authority for a result and output derives from its 2xx arm. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Roadmap * roster: import list_map * Move the ANSI roster work to its own branch An auto-commit captured an in-progress edit to extdeps.render.ansi on this branch. That work is the terminal control roster decomposition — a separate repair with its own reviewable argument — and it now lives on session/proud-swift-104-ansiroster. This branch carries only the REST outcome model, restoring ansi.dag to main. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Escape the braces in the note that .dag reads as interpolation The carrier note quoted the diagnostic the realization used to raise, 'HTTP {status}: {body}'. In .dag a brace followed by an identifier opens string interpolation, so those were parsed as references to variables named status and body, and the compile-clean gate refused with two undefined-variable errors. The escape is \{ and \}. Verified through a CONSUMER entry rather than the module itself: gunbc compile --entry on a module skips body analyses, so the clean result I took as verification earlier could not have caught this. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Surface opted-in REST failures as data (#7602) * WIP: REST non-2xx as data in dispatch_rest * Witness REST outcomes through .dag callers * Name REST witness scaffold dissolution --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> * F1 REST transport replay seam (#7610) * WIP: F1 REST transport replay seam * Bind REST replay fixtures to realized query targets --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> * Mark the new seed Rust with the repo's hand-Rust gate (review 46616) DESIGN 7 requires a seed-retained region to be a declared row with a reason and a migration trigger - countable and prioritizable, never a silent escape hatch. A comment explaining intent is not that, and both new regions had only the former. Two HAND-RUST GATE explicit deferrals, matching the existing pattern at native_cache_rebase_workspace_dir and resolve_host_tool_program. Each states what is actually deferred, which is much narrower than the line count suggests: witness frame - the policy is modeled (v2.std.witness_evaluation owns the carrier; rest_exchange_resolution owns lookup, equality and handler selection, and the interpreter calls back into .dag for the decision). Seed-side is the dynamic-extent push/pop, which no modeled construct can express while the seed is the evaluator. Lane: ROADMAP v1-materialization-kernel. REST bridge - every decision is modeled (RestOutcome, RestExchangeObservation, rest_bound_invocation_eq, rest_exchange_fixture_lookup). Seed-side is projecting them onto the declared output record, which needs the interpreter's Value/Node. Lane: ROADMAP v1-interpreter-quarantine -> v1-interpreter-delete. Both deletion conditions are checkable by execution rather than by assertion, and the REST one is EARLIER than its v1-exit lane: when the response block becomes the single authority and output derives from its 2xx arm, the opt-in disappears, so rest_outcome_output_field has no field to detect and deletes outright, taking the status >= 400 raise with it. Its control is that rest_operation_without_outcome_still_refuses must be REPLACED rather than kept green, since a Legacy operation with no outcome field can no longer exist. evaluate_in_witness_frame_seed_note gains the same receipt, and splits out what the original note blurred: the two stubs (witness_diagnostic_rendered_reason returning "" and evaluate_in_witness_frame always answering WitnessReturned) are fail-open in the direction that matters - under a pure evaluator a refusal is indistinguishable from a success carrying an empty reason. Nothing is wrong today because every consumer runs the realized path, but that debt gets its own nearer trigger rather than sheltering under a lane whose trigger is "witnesses emit to native code". NOT copied forward: the deletion row this pattern points at, dag/gunbc/v1_deletion_plan.dag ^witness_realization_kernel, no longer exists - that file's own v1_exit_model_doc records the brick ledger being retired 2026-07-28. Two live comments in the tree still cite it. These deferrals name verified-live roadmap node ids instead and record why; repointing the stale siblings belongs to the lane that owns them. cargo check -p v1-compiler clean, run locally with CTRL_BUILD_BYPASS_SHIMS=1 (ctrl-build executes remotely and leaves the local tree untouched, so a green from it would prove nothing here). The first cut of the frame deferral was a /// block before a thread_local! invocation and drew "unused doc comment" - it attaches to no item, so the marker would have been dropped; converted to //. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete rest_outcome_transported, which had no consumers (review 46657) One occurrence in the tree: its own definition. A predicate nobody calls is specification-without-execution, in the PR whose whole purpose is removing that from the REST surface - so the review's either/or resolves to delete rather than tag. A disposition tag would have made an unused predicate declared rather than used, and DESIGN 5 treats a dead scaffold as a wall-now class rather than something to annotate. The distinction it drew is real and the type still carries it: RestTransportRefused is the only arm where no status exists, which is the difference between "the remote said nothing" and "we never reached the remote". RestOutcome expresses that structurally, so a consumer matches the arm it cares about instead of folding four states to a Bool and losing which of the three transported ones occurred. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Make an active replay frame outrank the hermetic mock layer The replay seam worked only in Wet. In hermetic mode a non-governed service op with no fixture store fell straight to `eval_mock_response`, so the dispatcher was never reached and the fixture never consulted. That is the fail-open the seam exists to close, one layer up: the mock replays the operation RESULT off the declaration, while a replay frame supplies the transport OBSERVATION and requires the real dispatcher fold to run on top of it. Because CI runs the floor hermetically, the nine replay witnesses were exercising the mock layer rather than the seam -- they passed under `gunbc run --claim-run` (Wet) and failed under `claim_batch` (Hermetic) on one binary and one tree. An active frame now takes precedence, fail-closed on both arms. A REST transport routes to the ordinary wet dispatch so `rest_exchange_selection` decides, and that selection already refuses Absent/Ambiguous before any socket opens -- an active frame with no matching fixture is a typed refusal, not a live request escaping hermetic mode. Every other transport refuses rather than degrading to the mock or to a real shell/file effect. Measured on the merged tree: all nine witnesses FAIL->PASS under `claim_batch`, with the pre-fix binary as the direction control. Also merges main (20 commits), which carries the fix for the `\'` escape in live_deploy/emit.dag that made the local corpus run panic at parse. The new arm carries a HAND-RUST GATE marker naming the same lane as the `WITNESS_EVALUATION_FRAMES` deferral it sits under, with `rest_transport_failure_is_persistable` as its execution-checkable regression control. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Dissolve five hand-rolled equality predicates; pop the frame by construction Review 46769 (codex, REQUEST_CHANGES): `rest_http_method_eq`, `rest_uri_scheme_eq`, `rest_uri_eq`, `rest_operation_ref_eq` and `rest_auth_identity_eq` each matched every variant of a closed coproduct to decide whether two of them were the same -- a second representation of equality standing beside the one the substrate already provides. Worse than redundant: adding a variant to HttpMethod or UriScheme would leave the predicate silently answering false for it, so the duplicate decayed differently from the type it claimed to compare. All five are deleted and `rest_bound_invocation_eq` now consumes canonical `==`. Deliberately NOT collapsed to a whole-record `a == b`: which facts constitute an exact invocation identity is a modeled decision, so the field list stays spelled out. Equality of each named fact is canonical; the choice of which facts to compare is not equality, it is business. Review 46767 (claude, non-blocking): the frame pop was an ordinary statement after `apply_closure`, which held only because nothing between them returned early -- a property of the current body, not of the code, so the block comment's "removed on both paths" was a promise the shape did not keep. `WitnessFramePop`'s Drop now pops on every exit path including an unwind. That one is worth closing by construction rather than by care because this PR raised its severity: `dispatch_service` now consults `current_witness_evaluation_frame()` to decide whether a hermetic op reaches the real dispatcher, so a leaked frame would silently route SUBSEQUENT ops out of the mock layer -- a hermeticity hazard, not just a stale binding. All nine replay witnesses PASS under `claim_batch` after both changes. The sibling-operation and duplicate-fixture witnesses discriminate on identity, so canonical `==` deciding coproducts and records is proven by execution rather than assumed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Make the unrealized witness frame refuse instead of fabricating success Review 46769's second finding. `evaluate_in_witness_frame` returned `WitnessReturned` unconditionally, so an evaluator without the frame realization reported every refusal as a success -- the fabricated-plausible- output failure DESIGN §5 forbids, sitting in the one function whose entire job is to report whether a subject returned or refused. It had been defended as scaffolding with a declared dissolve-on. That defence does not hold: a trigger does not make a fail-open arm fail closed, it only schedules the arm's removal. Codex was right and the two APPROVEs that called this "worth watching" were reading the same code more kindly than it deserved. The pure body now answers `WitnessRefused` with a located reason naming the missing realization. Refusing costs nothing that was real: the interpreter dispatches this boundary by module and name and never evaluates this body, so the realized path is unchanged -- proven by the nine replay witnesses, which still PASS. What changes is the unrealized path, where a consumer now learns that no frame was installed instead of being told its subject succeeded. `witness_diagnostic_rendered_reason` returning "" remains open and is now strictly weaker: it can no longer disguise a refusal as a success, only render a real refusal's reason as empty. Same dissolve-on. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 2, 2026
…#7552) * Type the remote-read failure, name the offending refs, and get the argv out of the refusal Three defects from #7498 that merged to main, fixed together because they are one defect seen three ways. RemoteBranchesUnreadable carried `detail: String`, and three genuinely different failures were flattened into it at construction: the advertisement was refused by the transport, an advertised line did not parse, or an advertised ref projected to an empty branch name. Different remedies -- the first says nothing about the repository, the second means the remote spoke a format this parser rejects, the third means a ref survived advertisement but not projection. A caller holding a sentence could only recover which by matching substrings, which is the classify-by-prose move the transport-anemia plan exists to remove. The argv went with it. Each sentence concatenated the literal `git ls-remote --heads` onto the remote, so the command spelling was load-bearing in a domain refusal three times. The stable identity is the operation, git.Core.LsRemoteHeads, and the spelling is one realization of it that changes when the invocation is derived. render_remote_branch_read_failure is now the only function producing a sentence and it names the operation; a claim asserts the argv spelling is absent. advertised_refs_projecting_empty_branch returned an Int, so the identity of the offending ref was in hand at the moment of the test and discarded before the refusal was built. It now returns the refs. That is also strictly less work: the filter already built the set and count() collapsed it. It returns every offender rather than the first, per this module's own no_silent_pick_note. Evidence strengthened rather than merely kept. The witnesses asserted substrings of the flattened String, so they could not distinguish a renderer that lost a field from a model that never had it. They now assert typed fields, with the renderer claimed separately -- a rendering regression and a modeling regression now fail different claims. 24 claims green by execution across both files. NOT fixed, and the seam is named in-code: RefAdvertisementRefused still carries exit_code and stderr as Int and String, because the typed process observation that replaces them is Lane C and in flight separately. The other two arms have no such dependency. The `as NonEmptyStr` cast keeps its pre-cast guard: refinement brands are not construction-enforced, the compiler says so out loud at that site, and checking before the cast is the attainable ceiling until they are. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Roadmap * Fix the stale note this PR itself made false ls_remote_carries_no_exit_block_note said a caller learns whether the read succeeded from success/exit_code/stderr. This PR removed the success output, so that sentence became false inside the same diff that falsified it -- the stale citation class, committed by the change that created it. Corrected to name exit_code/stderr and to point at the note directly above it, which is the authority for why the Bool went. Caught in the portfolio review. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Carry the operation identity as an OperationRef, not a free string review 45876: this PR deleted the argv spelling from three domain refusals and then re-minted the operation NAME as a free String in the renderer. That is a smaller nickname in the same place, not the removal of one. The identity is now the corpus's modeled carrier, and the renderer projects it through operation_ref_label, added beside OperationRef in v2.std.operation_argv so the next module naming an operation has one place to reach for. Why this reduces drift instead of relocating it: shell_transport_operation_rows enumerates every declared shell-transport operation carrying its own OperationRef, and ArgvRefusalCause already has OperationNotFound for a ref resolving to nothing. A stale ref is reachable from an enumeration that exists. A sentence fragment inside a join([..]) is not reachable from it at all. Why the ref is WRITTEN here rather than derived, which is the sharper question and is refused deliberately: deriving it means selecting the row out of shell_transport_operation_rows, and that builtin reads the live source tree. This module's whole property, stated in belt_observes_note, is that it adjudicates over values a caller already holds, so every arm including the refusals is reachable with no network, no token, and no tree. Trading that for a staleness check would move the module to ReadsLiveTree. Written down as ls_remote_operation_ref_note rather than left implied; the check belongs outside, over the corpus's refs at once. Evidence, by execution: 10/10 roadmap_publish_observe witnesses PASS, including the two that assert the rendered text contains git.Core.LsRemoteHeads -- so the bytes are unchanged and those assertions are the discriminating check on the refactor. Compile 0 blocking on roadmap_publish, its witness, the operation-argv corpus witness, and effect_plan_bash_materialize. Only change to v2.std.operation_argv is an added pure function and its note. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Repository-bound publication observation: one identity, both reads Phase 1 slice, part 1 of the vertical. extdeps.github.github gains github_https_clone_url, projecting GitHub's documented HTTPS clone URL from a Repository's owner and name rather than storing it -- a stored URL would be a second representation of a fact those two fields already fix, free to disagree with them. WHY THE PROJECTION EXISTS when git accepts the local alias origin equally well: an alias is a fact about one checkout's configuration, not about a repository. Two checkouts can point origin at different repositories. A caller reading refs from origin and pull requests from an owner/name pair has performed two reads that are only COINCIDENTALLY about the same repository, and nothing in either result would reveal it if they were not. observe_publication_for_repository derives the remote from the SAME Repository that supplies owner and name to the pull-request read, so there is no arrangement of arguments in which the two observations describe different repositories. That is the construction answer rather than a convention to remember, and it needs no signature change to adjudicate_publication -- the caller simply stops passing an alias. STATED, NOT PAPERED OVER: github.Pulls.List declares its outputs for the 200 case so a successful read builds PullRequestsRead here, but a non-2xx does NOT arrive as a value -- the REST dispatch raises, so PullRequestsUnreadable is not constructible from a failed call. Deliberately NOT dressed up by wrapping the call in a fabricated refusal no real failure would produce. The arm stays in the type because a caller can hold a refusal from elsewhere, and deleting it would push the ignorance-as-answer conflation into every other producer. Compile 0 blocking on both modules. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Publication receipt: emit and decode, subject carried on both sides Phase 1 slice, part 2. The persisted-receipt half of the vertical. THE KEY IS THE VARIANT, NOT A GRADE. Eight outcomes, eight keys. publication_offers_the_expected_head folds seven of them to false, and a receipt storing only that fold could not distinguish a branch nobody pushed from a pull request whose head moved under a review - the two states with the most different remedies. The boolean would have been cheaper and would have destroyed exactly the information the arms exist to carry. THE RECEIPT NAMES ITS SUBJECT, which is what makes it a receipt rather than a status: repository, branch and expected head beside the outcome. A reader finding only an outcome key would have to trust that whoever wrote it was looking at the same head the reader cares about - and PublicationHeadDiverged, the arm this module exists for, is precisely the case where a stale receipt and a fresh one differ while both say something plausible. The expected head is recorded because it is the QUESTION ASKED, not the answer given. The decode returns the subject with the outcome for the same reason, in the other direction: a consumer holding only outcome_key can tell WHAT was judged and not WHAT ABOUT, so it could not detect a receipt answering a question about a head that has since moved. Dropping it on the read side would reintroduce the defect one layer down, in the artifact instead of the judgment. An unrecognized outcome key REFUSES rather than passing through as an opaque string. The keys are exactly what publication_outcome_key writes, so one outside that set means the document came from another emitter or a future version; carrying it would let a consumer match a value no arm corresponds to and fall into its default branch - a silent wrong answer at a boundary whose whole job is deciding whether a commit is published. Shape follows the validation receipt precedent exactly (schema constant, _json emitter, string-member reader, _decode over parse_json). Compile 0 blocking; execution receipt lands with the witnesses. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Prove the receipt round trip by execution, subject and all 22/22 roadmap_publish claims PASS, seven of them new. The three that carry weight are discriminating rather than confirming: a_receipt_records_the_head_that_was_asked_about - two receipts differing ONLY in expected_head must decode to different subjects. A receipt format that dropped the subject passes every other positive claim in this file and fails exactly this one, which is why it is a witness and not an inspection. a_receipt_missing_its_subject_refuses - a document carrying schema, outcome and detail but no repository is rejected, not decoded with blanks. an_outcome_key_this_emitter_never_writes_refuses - "published-ok" is the shape of key a reasonable OTHER emitter would produce, so it probes the boundary rather than a nonsense string. the_clone_url_names_the_repository_not_a_local_alias asserts both halves: the URL is what GitHub documents AND is not "origin". That file's existing fixture_remote is literally "origin", harmless where the adjudicator treats the remote as a label, and exactly the value the new binding must never produce - so the claim names it. Why this run matters beyond the compiles already reported on this branch: --entry compiles do not run body analyses, so those proved the modules typecheck, not that the receipt round-trips. This is the evidence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Roadmap * Publication reads a receipt: delete the constant, prove the replacement Phase 1 slice, part 3. The hardcoded arm is gone. It returned WorkflowSegmentPending with a fixed sentence whatever had happened, so a row published at exactly the head under judgment looked identical to one nobody had pushed. A constant cannot be wrong about a particular attempt because it is not about any attempt - which also means it can never become right. Two distinctions it was hiding: PENDING WAS TWO STATES. No receipt means publication has not been adjudicated - an ABSENT OBSERVATION. A receipt decoding to branch-not-published is a JUDGMENT that nobody pushed. Same lamp before, different remedies; the details now say which. AN UNDECODABLE RECEIPT REFUSES, it does not fall back to pending. That arm was the tempting one and it is the absorbing fallback in miniature - the failure would be indistinguishable from ordinary progress, its frequency zero by construction, and nothing would ever count it. Wiring: publication-receipt.json paths at attempt and current-attempt grain (mirroring the validation receipt), two WorkflowAttemptEvidence fields, the belt Filesystem.Read, and every one of the 14 construction sites corpus-wide. 23/23 progress claims PASS. TWO DEFECTS THIS RUN CAUGHT THAT THE COMPILES COULD NOT: 1. The segment key is "publish", not "publication". All five new claims compared "" against their expectations and failed. --entry compiles do not run body analyses and never reach the test corpus, so 0-blocking said nothing here. I also first checked field coverage with a within-30-lines proximity grep, which missed four construction sites; replaced with brace-depth matching from each site to its actual closing brace. 2. forged_admission_receipt_cannot_complete_environment was VACUOUS, and it is not mine. It asserted !(segment_state(.., "env") == "complete") - but "env" is not a key either, so segment_state returned "" and the negation was true unconditionally. It would have passed if the forged receipt DID complete Environment, which is the one thing it exists to forbid. Now asserts the segment is found AND not complete; the != "" clause is what stops a future key rename from silently re-vacuuming it. Same green before and after for that one, entirely different meaning. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Roadmap * wip: publication producer + subject-checked projection * wip: publish route + serve wiring * wip: located decoder refusals, full repository round trip * WIP: Roadmap * Remove the throwaway live probe; keep the explicit Open state at the pulls call site * Delete the second head a bound receipt could carry (review 46116) ReceiptBound carried its own pr_head, and the decoder read it independently of the receipt's subject. A document naming this subject while binding a different pull-request head therefore decoded cleanly, matched the subject on all six subject fields, and completed Publication for a head no pull request offered -- the exact class this lane exists to catch, walked in through the carrier meant to record it. Fixed by construction rather than by a check (DESIGN section 5). The variant means "a pull request is open at the subject's expected_head", so the head it offers IS subject.expected_head -- already in the same document and already the receipt's filename. The field is deleted, so the contradictory document is unrepresentable rather than rejected. ReceiptHeadDiverged keeps its pr_head: there the head is genuinely new information that appears nowhere else. The projection reads the same single copy: publication_outcome_segment_ detail now takes expected_head and renders it, so the completed sentence cannot disagree with the judgment it describes. Evidence, green by execution: - a_bound_receipt_binds_the_subject_head_and_no_other and a_stray_head_cannot_make_a_receipt_evidence_for_the_head_it_names feed the decoder the doctored document the old encoder would have produced (a stray pr_head naming the other fixture) and assert it answers with the subject's head, never the stray one. Both go red if any reading of an outcome-side head is restored. - the_completed_sentence_names_the_head_that_was_judged asserts both directions: the judged head appears, the other fixture sha does not. - publish 37/37, progress 26/26, belt 56 PASS (9 pre-existing no-mock_response failures, unrelated). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Roadmap * Establish receipt absence by listing, never by a failed read (review 46148) Filesystem.Read answers success=false both for a receipt that does not exist and for one that exists and cannot be read. The producer inferred absence from that bit, EvidenceAbsent mapped to PublishProceed, and an I/O fault on an existing receipt would therefore have overwritten evidence the belt could not read -- a fail-open in the one place this lane promises not to be. The repository had already paid for this lesson at the Verify seam: roadmap_validation_oracle's validation_not_run_note records the same defect (empty text arriving from three worlds, then the validation re-run and the evidence overwritten) and the same resolution -- make absence a state somebody ESTABLISHED, not a value inferred from failure. Pure half: publication_evidence_for now takes PublicationReceiptSource (Absent | Present{text} | Unreadable{detail}) instead of (Bool, String), so there is no longer a spelling for "I could not read it, treat it as gone". A present-but-empty file reads as unreadable, not absent -- a truncated write is a fault, and concluding "nothing published" from it is the same fabrication one step down. Effect half: belt_publication_receipt_source walks a ladder whose every absence conclusion is positive. It starts at the attempt state directory, which dispatch creates and which this producer only reaches for an attempt whose worktree head it already read, so a failed listing there is unambiguously a fault. Then: publication dir absent from a successful listing, or the head's file absent from a successful listing. Only a listed file is read, so a failed read is unambiguously a fault. Every failure arm refuses with the path and the host error; none widens. Line-exact listing membership, so a head sha is not found inside a longer one nor a receipt inside its own .tmp sibling. Evidence, green by execution: - an_unreadable_receipt_halts_rather_than_being_overwritten and an_absent_receipt_lets_the_publish_producer_proceed are the discriminating PAIR -- the old code proceeded on both, so either alone would pass under the defect. - a_present_but_empty_receipt_is_a_fault_not_an_absence. - an_absent_receipt_is_absent_and_present_but_unusable_ones_refuse separates all four sources at the pure layer. - an_unreadable_receipt_refuses_rather_than_reading_as_not_yet_published asserts the lamp differs from pending. - listing_membership_is_line_exact_not_substring covers prefix, suffix and empty-listing cases. - publish 37/37, progress 27/27, oracle 36/36, serve 15/15, belt 59 PASS (9 pre-existing no-mock_response failures, byte-identical set). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Make the repository identity one authority the five nicknames consume review 46301 rejected the added gunbc_repository as a fourth spelling carrying a promise to consolidate later, and it is right to: DESIGN's recurring-failure list says an honestly-marked scaffold duplicating a canonical fact is still a violation. A sixth nickname with a note is not an answer to five nicknames. It was also worse than the note claimed. There were FIVE existing spellings, not three: ci_heal_dispatch's owner/repo String pair, runner_host_deploy's org, review's parameter defaults, review_codex's own owner/repo pair, and bmc_token_federation's gunb-ai/gunbc slug -- three different shapes for one entity, none of them a Repository. So the value moves to gunbc.repository as the single typed authority and every one of the five now projects from it. No bare gunb-ai literal remains anywhere outside that row. Repository rather than a String pair because extdeps.github.github models what the API returns, so owner, name, full_name, private and default_branch travel as one fact: a consumer needing the default branch stops guessing main, and one needing the slug stops building it by concatenation. The instance lives in gunbc rather than extdeps because WHICH repository this project is, is a fact about the project; putting it in extdeps would make the dependency model know its dependent. One hazard is recorded at review's parameter defaults rather than left implicit: a default argument is evaluated in the CALLER's scope, so a future caller in a module without the import would die naming a symbol it never wrote. Safe today only because review_cycle has no in-corpus caller -- unreachable rather than proven, which is what the note says. Verified: 0 blocking errors on roadmap_belt_actuate, bmc_token_federation and runner_host_deploy; ci_heal_dispatch typechecks. review and review_codex fail on a pre-existing unresolved upsert_tagged_cron_tab that reproduces identically on the unmodified parent, so it is inherited rather than introduced -- baselined before attributing it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * List the belt's publication symbols in its import blocks review 46342 is right that seven symbols the new receipt reader uses are absent from roadmap_belt_actuate's selective import lists: PublicationReceiptSource with its three constructors, plus dispatch_attempt_state_path_for_instance, publication_receipt_directory_segment and dispatch_attempt_publication_dir_for_instance. The review's stated consequence does not hold -- the module compiled with zero diagnostics on any of those names, before and after, so they were resolving. But resolving is not the same as being declared, and HOW they resolved is the problem: by pool membership, because some other module in the closure already dragged the definer in. That is the failure class DESIGN records under the import-strip cascade, where a bare cross-module reference works only while an unrelated import elsewhere happens to keep its target in the pool, and stops working when that unrelated file changes. Coverage by coincidence. So the imports are listed. Nothing about the behaviour changes; what changes is that the dependency is now stated where a reader and the graph can both see it, and roadmap_belt_actuate stops disagreeing with roadmap_workflow_progress, which imports the same symbols explicitly. Verified with a freshly built binary, because a stale one had already produced one false green today: 0 diagnostics on every symbol named in the review; publish 37/37, progress 27/27, belt 60 PASS with the 9 standing no-mock_response failures unchanged. The only remaining diagnostics are the four inherited filter call-shape errors in roadmap_presentation, which PR #7592 fixes on its own branch. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Roadmap * Model a REST response that is not 2xx as an answer, not an absence Service operations already declare what each status yields — github.Pulls.List declares 200/401/404/422/5xx, and twenty-two other extdeps modules declare 204 such arms between them. The v1 seed parses every one of those declarations onto the operation node as a response_<status> property and then never reads it: dispatch_rest raises InterpError::TypeError with a rendered "HTTP {status}: {body}" string for anything at or above 400. So a caller cannot reach the status, cannot reach the body, and cannot persist either without parsing a diagnostic written for a human. This lands the type the realization will project into. Four states rather than three: a transported request that was answered with a non-success status keeps both the status and the body it arrived with, because the body is usually the only place the remote says why; a request that never transported has no status at all, so none is invented; and a status that arrived over an unreadable payload is its own arm, so an unreadable body is never reported as an empty one. status is std.types HttpStatus rather than a fresh Int — the range already has one authority — and RestTransportRefused deliberately carries no status, since a sentinel zero would be a plausible-looking value standing where the honest answer is that the question does not apply. No realization consumes this yet, and the scope is stated on the carrier so it cannot be misread as complete: the outcome is opt-in per operation, and a refusal body stays a String rather than being decoded into the shape the response block already names. Both dissolve when the response block becomes the single authority for a result and output derives from its 2xx arm. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Roadmap * roster: import list_map * Move the ANSI roster work to its own branch An auto-commit captured an in-progress edit to extdeps.render.ansi on this branch. That work is the terminal control roster decomposition — a separate repair with its own reviewable argument — and it now lives on session/proud-swift-104-ansiroster. This branch carries only the REST outcome model, restoring ansi.dag to main. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Escape the braces in the note that .dag reads as interpolation The carrier note quoted the diagnostic the realization used to raise, 'HTTP {status}: {body}'. In .dag a brace followed by an identifier opens string interpolation, so those were parsed as references to variables named status and body, and the compile-clean gate refused with two undefined-variable errors. The escape is \{ and \}. Verified through a CONSUMER entry rather than the module itself: gunbc compile --entry on a module skips body analyses, so the clean result I took as verification earlier could not have caught this. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Roadmap * Surface opted-in REST failures as data (#7602) * WIP: REST non-2xx as data in dispatch_rest * Witness REST outcomes through .dag callers * Name REST witness scaffold dissolution --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> * WIP: Roadmap * Revert the auto-commit belt-timer fragment off the Publication branch An auto-commit (49d377b, "WIP: Roadmap") captured a two-line mid-edit fragment of unrelated belt-timer work onto this branch: BeltTimerUnit added to OwnedArtifactKind and its teardown arm. The fragment is self-consistent and compiles -- a variant with a teardown answer and no construction site is inert -- so it was not the cause of this branch's CI red, which is inherited from main (two witnesses in v1_interpreter_primitive_surface_witness_test.dag, keen-swift-704 lane). It is reverted anyway because it does not belong here. This branch is the Publication producer; the belt tick driver is separate work and lands as its own PR against main. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Roadmap * F1 REST transport replay seam (#7610) * WIP: F1 REST transport replay seam * Bind REST replay fixtures to realized query targets --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> * Read back which repository the attempt worktree is actually a checkout of The publication path read a head SHA off a worktree on disk and then reported it as evidence about a repository, without ever establishing that the worktree was a checkout of that repository. Both REMOTE reads were already bound by construction - publication_subject_remote derives its URL from github_https_clone_url(subject.repository), so they cannot disagree about which repository they concern - but the LOCAL side had no such binding, and it is the local side the head comes from. WorktreeRepositoryBinding has three arms because the failure has three shapes and only one of them is a mismatch. WorktreeBoundElsewhere carries BOTH urls, since a mismatch whose message names only one of them cannot be acted on. WorktreeRemoteUnreadable carries the exit code and stderr, because "we could not ask" is a different fact from "we asked and the answer was wrong". An empty stdout resolves to unreadable rather than to a mismatch against the empty string, following the module's existing empty-stdout-is-unobserved precedent. The outcome is PublishEvidenceUnreadable, not PublishDeferred. Deferral means the belt should look again on the next tick, and neither a wrong checkout nor an unreadable remote fixes itself by waiting - a deferral would spend a tick per attempt forever while reporting nothing. git.Core.RemoteUrlIn existed on this branch with zero consumers, which is the specification-without-execution shape this lane keeps producing. It now has one. Also fixes the parse error the auto-committed mid-edit snapshot (0b5ce9c) pushed: the nested match arm was short two closing braces, so the parser ran past the function into the next declaration and reported the Colon it found there. Witnesses, green by execution (claim_batch, not compile): worktree_bound_to_the_subject_repository_is_recognized worktree_pointing_at_another_repository_refuses_and_names_both worktree_remote_read_failure_is_not_a_mismatch empty_remote_url_is_unreadable_not_bound_elsewhere Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Make observe_pull_requests total over the REST outcome Stacks on the REST replay seam (#7600), which is merged into this branch so the work can proceed; when #7600 lands on main this diff collapses to the Publication half. github.Pulls.List declares outcome: RestOutcome, so a non-2xx now arrives as a value instead of escaping as a raise. Three consequences, and the third is the one that mattered: result.pulls is read ONLY under RestOk. The realization leaves the ordinary body-derived fields uninhabited on a non-success outcome, so reading .pulls on any other arm would report the absence as an empty list of open pull requests - and an empty list is a perfectly ordinary answer meaning "not published yet". A 401 would have been indistinguishable from a genuine unpublished state, and the belt would have written a receipt saying so. The previous unconditional read was correct only because dispatch_rest raised and the arm was unreachable; making the outcome data is what makes that line newly wrong. PullRequestsUnreadable carries a typed cause instead of detail: String. Four failures reach it and they are not four phrasings of one event: no usable credential is a local decision taken before a request exists; a status refusal means a remote authority answered and the body is usually the only place it says why; a transport refusal means no status exists at all; an undecodable body is a decoder fault, not an access one. This is the repair remote_branch_read_failure_note already describes, applied to the peer observation that did not get it - same shape, same renderer discipline, and the renderer names github.Pulls.List through its OperationRef rather than the path and query. The 401 witness stops asserting a hand-written sentence. It constructed PullRequestsUnreadable { detail: "401 from the forge" } and grepped its own string back out; it now constructs the real status refusal and asserts the status, the body, and the repository each survive into the refusal detail. Compiles clean through both consumer entries (belt actuate, publish witness test). Witnesses for the four new arms are NOT yet written or executed - that is the next commit, and the live four-case receipt still waits on #7600 merging so the interpreter half is on main. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Mark the new seed Rust with the repo's hand-Rust gate (review 46616) DESIGN 7 requires a seed-retained region to be a declared row with a reason and a migration trigger - countable and prioritizable, never a silent escape hatch. A comment explaining intent is not that, and both new regions had only the former. Two HAND-RUST GATE explicit deferrals, matching the existing pattern at native_cache_rebase_workspace_dir and resolve_host_tool_program. Each states what is actually deferred, which is much narrower than the line count suggests: witness frame - the policy is modeled (v2.std.witness_evaluation owns the carrier; rest_exchange_resolution owns lookup, equality and handler selection, and the interpreter calls back into .dag for the decision). Seed-side is the dynamic-extent push/pop, which no modeled construct can express while the seed is the evaluator. Lane: ROADMAP v1-materialization-kernel. REST bridge - every decision is modeled (RestOutcome, RestExchangeObservation, rest_bound_invocation_eq, rest_exchange_fixture_lookup). Seed-side is projecting them onto the declared output record, which needs the interpreter's Value/Node. Lane: ROADMAP v1-interpreter-quarantine -> v1-interpreter-delete. Both deletion conditions are checkable by execution rather than by assertion, and the REST one is EARLIER than its v1-exit lane: when the response block becomes the single authority and output derives from its 2xx arm, the opt-in disappears, so rest_outcome_output_field has no field to detect and deletes outright, taking the status >= 400 raise with it. Its control is that rest_operation_without_outcome_still_refuses must be REPLACED rather than kept green, since a Legacy operation with no outcome field can no longer exist. evaluate_in_witness_frame_seed_note gains the same receipt, and splits out what the original note blurred: the two stubs (witness_diagnostic_rendered_reason returning "" and evaluate_in_witness_frame always answering WitnessReturned) are fail-open in the direction that matters - under a pure evaluator a refusal is indistinguishable from a success carrying an empty reason. Nothing is wrong today because every consumer runs the realized path, but that debt gets its own nearer trigger rather than sheltering under a lane whose trigger is "witnesses emit to native code". NOT copied forward: the deletion row this pattern points at, dag/gunbc/v1_deletion_plan.dag ^witness_realization_kernel, no longer exists - that file's own v1_exit_model_doc records the brick ledger being retired 2026-07-28. Two live comments in the tree still cite it. These deferrals name verified-live roadmap node ids instead and record why; repointing the stale siblings belongs to the lane that owns them. cargo check -p v1-compiler clean, run locally with CTRL_BUILD_BYPASS_SHIMS=1 (ctrl-build executes remotely and leaves the local tree untouched, so a green from it would prove nothing here). The first cut of the frame deferral was a /// block before a thread_local! invocation and drew "unused doc comment" - it attaches to no item, so the marker would have been dropped; converted to //. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Witness the four read-failure causes, and drop a cast that only fails when run The four arms landed in the previous commit with no executing consumer, which is the shape this lane keeps producing. Four witnesses now execute them: four_pull_request_read_failures_stay_four_distinct_causes - matches the coproduct rather than the rendered sentence, so a future edit that collapsed two arms into one phrasing is a compile error instead of a silently identical string that keeps the claim green. a_status_refusal_renders_operation_repository_status_and_body - asserts the operation is named through its OperationRef and the path is NOT, following ls_remote_operation_ref_note's derivation for the sibling reader. a_transport_refusal_carries_no_status_at_all - asserts the absence. A sentinel zero would be a plausible value standing where the honest answer is that the question does not apply. every_pull_request_read_failure_refuses_rather_than_reporting_unpublished - the remotes are read-and-empty, so the pull-request side is the only thing that can refuse; a cause handled by falling through to the remote reading would show up as BranchNotPublished and red. THE CAST THAT COMPILED AND DIED. The first cut wrote `401 as HttpStatus` and compiled with 0 blocking errors; four of the five witnesses then failed on the first run with `cannot cast Int to HttpStatus`. HttpStatus is `Int where range(min: 100, max: 599)` and a refined position takes the bare literal - which is what the replay test's denied_observation already does. The tell I should have read before writing it: `grep -rn "as HttpStatus" dag/` returned only my own new sites, so I had invented the idiom rather than followed one. `to_string(status as Int)` went with it; to_string accepts the refined Int directly. Executed, not compiled: 5/5 PASS via claim_batch on this tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete rest_outcome_transported, which had no consumers (review 46657) One occurrence in the tree: its own definition. A predicate nobody calls is specification-without-execution, in the PR whose whole purpose is removing that from the REST surface - so the review's either/or resolves to delete rather than tag. A disposition tag would have made an unused predicate declared rather than used, and DESIGN 5 treats a dead scaffold as a wall-now class rather than something to annotate. The distinction it drew is real and the type still carries it: RestTransportRefused is the only arm where no status exists, which is the difference between "the remote said nothing" and "we never reached the remote". RestOutcome expresses that structurally, so a consumer matches the arm it cares about instead of folding four states to a Bool and losing which of the three transported ones occurred. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Drop three backslash-escaped apostrophes the new lexer correctly refuses CI red at 280ceed: parse error in roadmap_dispatch_actuator.dag, "expected expression, found Unknown". The file carried A\'s and B\'s inside a double-quoted note - an apostrophe needs no escape there, so the sequence was always wrong. It was introduced by an auto-commit of my own work (b81026f) and is not on main. WHY IT BROKE NOW rather than when it was written: #7585 merged, closing the unknown-escape fail-open. The old lexer passed an unrecognized escape through silently; the new one refuses it as a located ShUnknown token, which is what "found Unknown" is. The escape did not become wrong - it became AUDIBLE, which is the entire point of that PR. WHY MY LOCAL CHECK SAID IT WAS FINE, recorded because it nearly produced the wrong report: the binary was built before the main merge, so it still had the permissive lexer and compiled the file clean. I was one step from telling the operator this looked like a CI-side problem. Rebuilt against the current tree, then ran the control on the SAME binary - reintroducing one escape reproduces the exact CI message, and removing it compiles 0 blocking. Compile-green under a stale binary proves nothing about the tree CI parses. Swept every .dag file this branch touches for the same sequence; this was the only one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct a note this PR's own code made false `pull_observation_transport_bound_note` still declared that a non-2xx "does not reach this function as a value" and that "Publication cannot claim a live trip" -- both true when the paragraph was written and both falsified by this same PR, which adds `outcome: RestOutcome` to `github.Pulls.List` and matches its four arms in `observe_pull_requests`. Caught by review 46728. The paragraph now states what is true and keeps the prior state, because the history is what names the defect: the raise-on-non-2xx behavior, why it made the refusal unreachable through a real call, and the live receipt that closed it -- absent credential refused locally with no request, present-but- rejected returned 401 with its body intact, valid credential read 30 pulls. The last is the discriminating control: a mis-wired outcome field would plausibly have emptied the pulls projection on success too. Also merges main. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds a lower-grain REST exchange observation and exact invocation-keyed replay seam selected through the existing effect HandlerBinding. Real HTTP and replay now feed one operation-decision fold, while a generic scoped witness evaluation frame captures expected interpreter refusals without leaking bindings.
Replaces the loopback-server Rust witness with independently discovered .dag claims and committed probe operations. Missing, ambiguous, and sibling fixtures refuse without network fallback; the obsolete witness binary, Cargo target, CI roster rows, and generated workflow references are deleted.
Test plan