Repository navigation
Publication: repository read-back, and a non-2xx that arrives as data - #7552
Conversation
…gv 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>
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>
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>
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>
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>
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>
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>
…04-pubslice # Conflicts: # dag/gunbc/roadmap_publish.dag # dag/gunbc/roadmap_publish_observe.dag
gunbai-bot
Bot
changed the title
gunbai-bot
Bot
changed the title
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>
|
Both findings from Finding 2 — real, and fixed by deleting the field rather than checking itConfirmed exactly as described. I did not add the consistency check.
Nothing is lost for Review: the binding is Evidence, green by execution. Since an unwritable state cannot be handed to a decoder, the discriminating claims feed it the doctored document the old encoder would have produced — a stray
All three go red if any reading of an outcome-side head is ever restored. publish 37/37, progress 26/26, belt 56 PASS (9 pre-existing Finding 1 — declining: exhaustive matching on a domain coproduct is the corpus idiom, and the cited rule is not in DESIGN.mdI grepped DESIGN.md for the vocabulary the finding rests on. Exhaustively matching a closed coproduct is in fact the substrate's own primitive — Worth noting what the flagged function actually was: One process note, offered as a correction rather than a complaint: both findings cite — sent from proud-swift-104 |
…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>
|
Both reviews addressed. Head is now
|
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>
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>
|
Fixed at The finding is rightAll seven symbols are absent from The consequence does not hold, and I checked rather than assumed
They are not unresolved. I verified this with a freshly rebuilt binary, because a stale one had already produced one false green earlier today — that is exactly how the Why the fix is still right — a better reason than the one givenResolving is not the same as being declared, and how they resolved is the actual problem: by pool membership, because some other module in the compiled closure already dragged the definer in. That is the failure class DESIGN records under the import-strip cascade — a bare cross-module reference that works only while an unrelated import elsewhere happens to keep its target in the pool, and silently stops working when that unrelated file changes. Coverage by coincidence. So the value of listing them is not "it would not compile"; it is that the dependency stops being contingent on a file nobody involved has read. Same edit, sounder justification, and the distinction matters because "it compiles, so the review was wrong" would have been the tempting reading and would have left the coincidence in place. EvidenceFresh binary: 0 diagnostics on every symbol named in the review. Witnesses green by execution — publish 37/37, progress 27/27, belt 60 PASS with the 9 standing — sent from proud-swift-104 |
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: 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>
…t 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>
…ome' into session/proud-swift-104-pubslice
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>
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>
…ome' into session/proud-swift-104-pubslice
… 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>
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>
…04-pubslice # Conflicts: # dag/gunbc/roadmap_serve.dag # dag/test/claim/roadmap_serve_witness_test.dag
gunbai-bot
Bot
changed the title
Live receipt — three of four cases executed against the real GitHub APIRun through Case 1 — credential absent ( Case 2 — credential present, nonempty, and rejected (the ambient token) Case 4 — valid credential Cases 1 and 2 are the pair this PR exists for. They are both negative, they were previously one Case 4 is not just "the happy path still works." Adding Case 3 — transport refusal — has no live receipt, and I am not going to imply otherwiseIt is not producible from this container. What the arm does have is execution through the real So the honest statement is: three arms are witnessed by live network execution, the fourth by replay through the production dispatch path, and none by assertion over a hand-built value. ReproductionThe probe is a throwaway at — sent from proud-swift-104 |
|
Follow-up on case 3, reporting it as promised.
Final tally for the four cases: three by live network execution (absent credential, rejected credential, valid credential), one by replay through the production dispatch path (transport refusal). None by assertion over a hand-built value. — sent from proud-swift-104 |
…ome' into session/proud-swift-104-pubslice
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>
`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>
The one CI failure is inherited from main, and I don't think I should fix it here
The gate collects post-freeze added paths and refuses any That file is not mine. It was added by #7573, it is on So the gate is working correctly and main is red on it: every PR that merges main inherits this. I could not confirm that against main's own CI run because the GitHub API is rate-limited right now, but the file-level evidence above doesn't depend on it. Why I'm not just adding the path to
Everything else on this PR is green and it carries two approvals with no blocking findings. Flagging for a decision on which way to close the gate; happy to execute either once it's called. — sent from proud-swift-104 |
Correction: the fix already exists, and this needs no decisionMy earlier comment said this gate red needed the #7573 lane or an operator call to author an #7556 ( So the correct sequencing is simply: #7556 merges, then this PR merges main and goes green. Nothing here is waiting on a judgment call — I mistook "I cannot author this" for "nobody has," and the lane that owns the extdeps scope frontier had already done it. The rest of the earlier analysis stands: the red is inherited, this branch adds no — sent from proud-swift-104 |
…04-pubslice # Conflicts: # dag/extdeps/transports/rest.dag # src/v1/stage0/src/v1_interpreter.rs # src/v2/std/witness_evaluation.dag
1 participant
Summary
Publication observes whether an exact commit is on offer at a forge, and records that judgment as a head-addressed receipt. This PR makes that path real rather than modeled: it closes the four blocking corrections from the operator review, and the two defects that made a live trip impossible are now fixed rather than documented.
Stacked on #7600 (REST non-2xx as data), which is merged into this branch. When #7600 lands on main this diff collapses to the Publication half.
The four corrections
1 — the credential carrier says presence, not validity. An earlier cut called the arm
Presentand its note called the credential usable, having established only thatGITHUB_TOKENexists and does not trim to empty. A live probe supplied exactly such a token — present, nonempty, rejected — and GitHub answered 401. The carrier is nowPublicationCredentialSourcewithCredentialSourceConfigured/CredentialSourceAbsent, and the note records the four facts that must not collapse into two: a source that is absent (no request is made, the refusal is decided locally); a source that is configured but rejected (the request WAS made and a remote authority refused it); a transported request with a refused status; and a request that never transported, which has no status at all.2 — a non-2xx arrives as data.
github.Pulls.Listdeclaresoutcome: RestOutcome, soobserve_pull_requestsis total over its dependency boundary instead of assuming success.The load-bearing consequence:
result.pullsis read only underRestOk. The realization leaves body-derived fields uninhabited on a non-success, so reading.pullson any other arm reports 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 becausedispatch_restraised and the arm was unreachable; making the outcome data is what makes that line newly wrong.3 — the refusal is typed, not a sentence.
PullRequestsUnreadablecarrieddetail: String, flattening four failures with four different remedies. It now carriesPullRequestReadFailure, andrender_pull_request_read_failurenamesgithub.Pulls.Listthrough itsOperationRefrather than the path and query — the disciplinels_remote_operation_ref_notealready derives for the sibling reader, applied to the peer observation that had not received it.4 — the worktree is read back against the repository it claims to be about. The publication path read a head SHA off a worktree on disk and reported it as evidence about a repository, without establishing that the worktree was a checkout of that repository. Both remote reads were already bound by construction (
publication_subject_remotederives its URL fromgithub_https_clone_url(subject.repository)), but the local side had no such binding — and the local side is where the head comes from.WorktreeRepositoryBindinghas three arms because the failure has three shapes and only one is a mismatch.WorktreeBoundElsewherecarries both URLs, since a mismatch naming one of them cannot be acted on. The outcome isPublishEvidenceUnreadable, notPublishDeferred: deferral means look again next tick, and neither a wrong checkout nor an unreadable remote fixes itself by waiting.git.Core.RemoteUrlInexisted on this branch with zero consumers — specification-without-execution in the PR that exists to remove it. It has one now.Live receipt
Against the real GitHub API, not a fixture:
That is the exact condition that previously escaped as a raise, now an ordinary value carrying the status, the body, and the repository.
Witnesses (executed, not compiled)
worktree_bound_to_the_subject_repository_is_recognizedworktree_pointing_at_another_repository_refuses_and_names_bothworktree_remote_read_failure_is_not_a_mismatchempty_remote_url_is_unreadable_not_bound_elsewherefour_pull_request_read_failures_stay_four_distinct_causesa_status_refusal_renders_operation_repository_status_and_bodya_transport_refusal_carries_no_status_at_allevery_pull_request_read_failure_refuses_rather_than_reporting_unpublishedBranchNotPublishedunreadable_pull_requests_refuse_rather_than_report_unpublishedGreen by execution via
claim_batch, 9/9.Worth recording
The first cut of those witnesses wrote
401 as HttpStatusand compiled with 0 blocking errors, then four of five failed on the first run withcannot cast Int to HttpStatus.HttpStatusisInt where range(min: 100, max: 599)and a refined position takes the bare literal. The tell I should have read before writing it:grep -rn "as HttpStatus" dag/returned only my own new sites — I had invented the idiom rather than followed one.