Repository navigation
Attach the trailing NO ROOM-FIT annotation in rack_mount.dag to the declaration it describes - #8215
Merged
Merged
Conversation
DESIGN section 4c models source annotations only as standalone leading blocks on module-scope declarations. Eighteen comment blocks across five witness modules sat INSIDE declaration bodies -- annotating individual clauses of a conjunction, arms of a match, or lets in the middle of a function -- which the compile-clean gate refuses with: compile-clean: source annotation sits inside a declaration body. Only module-item grain is modeled; move it above the declaration it describes. This is pre-existing main debt, not a regression from any one branch. The count is exact: 18 in-body blocks under dag/ against 18 diagnostics, and the same refusal reproduces on two unrelated branches whose only common factor is that both force the whole-tree compile-clean baseline. Main's own recent runs are cancelled or in-flight, so no green verdict has observed it -- the debt has been accumulating unseen across at least five merged PRs (#8045, #8073, #8122, #8147, #8184-era files). The prose is preserved, not deleted. Each block is hoisted into its declaration's leading block, merged with any block already there, keeping the clause labels as sentences. Where a leading block already said the same thing -- fleet_converge_cli's join-1 header covers every clause note it carried -- the in-body copy is dropped as the duplicate it was. Comment-only: `git diff` contains no non-comment line, so no behavior, no witness assertion, and no emitted byte moves. WHAT THIS DOES NOT DO: the diagnostic is typed but UNLOCATED -- it names no file, line, or declaration, though AnnotationAttachmentRefusal carries `origin: SourceSpan` on every arm and BodyGrainNotModeled is constructed with it. The consumer discards the span it was handed. That is a section 5 located-ness gap which cost this diagnosis a full CI cycle and a bisection commit; it is left as a separate finding rather than repaired here, so this stays comment-only and reviewable as such. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS
This was referenced Aug 13, 2026
Merged
…they discuss CORRECTION TO THIS PR'S OWN DIAGNOSIS. The first commit claimed 18 in-body blocks were the whole annotation debt, on the strength of an exact count match. The match was real but the population was not the whole one: I grepped the failing log for the body-grain message and never checked whether a SECOND refusal class was also present. It was. The #8211 log carried 11 "source annotation names no subject: no module item follows it" refusals beside the 18 body-grain ones, and clearing the body-grain class left that second class as the visible failure. That is the nearby-question error: I confirmed the count of the class I was looking at and read it as the count of the failure. The unattached class is 7 at this PR's base, and it splits in two. FIXED HERE -- two genuine trailing notes, each explaining why something does NOT exist and therefore having no following declaration to attach to. Both move above the declaration they already discuss, which is where they belong on the merits and not only to satisfy the gate: dag/product/rack_mount.dag -- the note argues the mounting APERTURE is not the external envelope, which is exactly what the function directly below it computes; it now leads rack_mounting_aperture_height. resolved_graph_cache_hand_rust_witness_test.dag -- the note records a deleted tautological witness and points at the surviving positive control; it now leads that control. NOT FIXED HERE, deliberately -- the remaining 5 are comments sitting directly above `service` declarations (extdeps git.Inspect, git.PublicationTransport, sec.Edgar, tailscale.Serve, gcp.IamRoles). A `service` produces no depth-1 occurrence index entry, so it is not an eligible annotation subject and prose above it attaches to nothing. Relocating that prose would make the corpus worse. git/inspect.dag's block is 24 lines of measured rationale for the service's operations -- which porcelain version is pinned and why, why IgnoredFiles is a second operation rather than a flag, verified by execution against git 2.43.0. Moving it off the declaration it describes to satisfy a gate would be contorting the source to fit a model gap, which is the opposite of what section 4c is for. So the honest reading is that `service` SHOULD be an eligible annotation subject and is not. That is a change to the occurrence index / annotation subject model in the v1 seed, not a comment edit, and it is raised rather than improvised: this PR stays comment-only, and the gate stays red on those 5 until that decision is made. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CuRVynkbQYGqjmf9AnyxsS
Main independently landed the same body-grain -> module-item-grain moves for the four conflicted witness files (ci_deploy, host_phase_status, posix_principal_allocation, resolved_graph_cache_hand_rust). Main's side is taken in all four: the class is fixed there, and re-landing a second wording of the same annotations would be a duplicate authority for one fact. What this branch still contributes after the merge is one hunk: dag/product/rack_mount.dag's trailing 'NO ROOM-FIT RELATION' annotation, which named no subject, now leads rack_mounting_aperture_height - the aperture quantity the absent relation would consume, and the quantity its own closing sentence reasons about. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
changed the title
… this branch was open
The compile-clean gate failed on this branch's merge head with the body-grain
refusal class -- the same class this PR was opened to clear. The refusals are
NOT this branch's: they arrived on main in four files added after this PR's
base (dag/std/affine_space.dag, dag/std/planar_projection.dag,
dag/product/rack_power.dag, dag/product/spatial_projection.dag), and merging
main brought them in.
That is worth naming rather than just fixing. Main cleared this class in the
witness corpus and simultaneously re-introduced it in new modules, so the
population is not shrinking on its own -- clearing it is a moving target until
the rule is enforced where the module is parsed, not swept afterwards.
Two shapes, both moved to module-item grain with the subject named in the
hoisted text so the prose does not become unmoored from what it discusses:
- variant-attached blocks (OpProjectPoint3, ProjectionSourceFrameRequired,
ViewUnitsAreNotMillimetres, OutletsExhausted, DepthOrderAmbiguous, and the
two borrowed ProjectionRefusal causes) hoisted into the leading block of
their type declaration;
- in-body blocks inside fn bodies (the zero-page-right refusal, the dimetric
direction, the outlet-before-capacity ordering, the load-count crossing,
the nearer-candidate role naming) hoisted above their enclosing fn.
One trailing block was also refusing under the second class, "names no subject":
rack_power.dag's NO DERATING note sat at end of file with nothing following it.
It now leads budget_capacity, the accessor returning the un-derated cited
capacity the note is about. Its dissolve-on trigger is carried across verbatim
and is pre-existing debt from main, not introduced here.
Corpus scan after this change: zero indented // lines and zero trailing blocks
across dag/ and src/v2.
NOT verified locally: the shimmed gunbc on this host predates //-annotation
support and reports a parse error on every module header block, so it is not an
oracle for this class. CI is.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 13, 2026
Clears inherited dag_compile_clean_gate red on rack_mount.dag and rack_power.dag from #8201 — not a press-0 fork.
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 13, 2026
This PR's CI failure was never its own. Its base predated #8201/#8215/#8216, so its floor run inherited the corpus-wide in-body and unattached source-annotation refusals; its single changed file carries neither form. #8235 has since moved all 87 body-grain annotations to module-item grain and main carries none. Merge only — no content of this PR is touched.
briansrls
added a commit
that referenced
this pull request
Aug 18, 2026
… standing (#8166) * PRESS-0 step 2: bridge codex press rate-limit buckets into the standing limit axis gunbc.codex_app_server_press already decoded per-bucket rate limits, and gunbc.provider_standing already modelled the limit axis, and nothing joined them — so the probe bridge left limits Unobserved and a measured bucket produced the same verdict as an unmeasured one. account_standing_authenticated_rate_limits_readable_note specifies this consumer by name and carries its own dissolution: read evidence.rate_limit_buckets per limit_id, project each CodexRateLimitBucketVerdict onto ProviderNativeLimitBucket, never route through ProviderAccountLimit, and never use CodexPressAccountReady as the limit axis. That is what this does. Bucket scope is load-bearing rather than stylistic: the account classification gates on the codex bucket alone, so it reports Ready while a sibling is exhausted. The discriminating witness is the case the note names — one observation set with codex exhausted and codex_bengalfox available yields DIFFERENT verdicts under draws naming each bucket. An account-scoped projection cannot produce that and fails the witness. CapacityUnknown becomes LimitObservationUnobserved, never LimitObservedAvailable: could-not-decode read as nothing-is-wrong would admit a dispatch against a bucket nobody measured. An empty bucket list becomes one located Unobserved; limit_observations_are_selection_eligible already refuses empty, so this adds a reason rather than changing the verdict. NOT DONE, and it still blocks selection: the entitlement axis. No probe grounds ProviderEntitlementObservation for codex, and EntitlementObservationUnobserved is not selection-eligible, so codex remains ineligible on the six-axis conjunction even with limits now observed. The press note is explicit that account standing is not account-wide entitlement, so I have not fabricated one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Dissolve the dead belt_observe entry points and correct a stale roster note Both raised by review on #8132 as non-blocking follow-ups. belt_observe and belt_observe_for_instance are deleted. They observed the tmux session NAME set only, which is precisely why a retained dead pane read as a live agent; dispatch and tick both call belt_sessions_observe_for_instance now, so the pair had no production caller left. belt_observe_from_result SURVIVES deliberately and is now witness-only. Its subject is the tmux stdout parse — nonzero exit with no documented no-server marker, unparseable line, empty set — reached by eight witnesses. Deleting it with its caller would have deleted that evidence, and §4b is explicit that a climb dissolves the lower-rung production handling and never the discriminating evidence. Its dissolve-on is named on the carrier: re-point those parse witnesses at classify_tmux_session_list with the refusal cases preserved one-for-one. belt_dispatch_all_status_labels_note said an "8th variant" makes the label match non-exhaustive, which stopped being true at twelve. The mechanism it describes is unchanged, so the sentence now names a new variant rather than a count — a count in prose beside a live roster is the stale-citation class, and it rots without anyone touching it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Carry the bucket subject on an undecoded limit, per review 51237 CONFIRMED, and the root is worse than the symptom. The bridge matched CodexBucketCapacityUnknown { limit_id: _ } — discarding a limit_id the producer already held — and mapped it to LimitObservationUnobserved, which limit_observation_blocks_dispatch answers `true` for against EVERY draw. So one bucket failing to decode refused a draw naming a measured, available sibling. This is a fail-CLOSED error, which is why the existing sibling witness did not catch it: the exhausted/available pair still discriminated because neither was unknown. Over-refusal reads as caution while it prices out capacity the observation proved was there. ProviderLimitObservation gains LimitSubjectUnobserved { subject, native_token, reason }, routed through limit_subject_covers_dispatch_draw like every other subject-bearing arm. It blocks a draw naming that bucket, and still blocks Unspecified and Automatic draws because those cover every native bucket — precision where the draw names a subject, fail-closed where it does not. It is distinct from LimitCapabilityGapUnobservable, which means the axis is unobservable on this surface at all and correctly never blocks. The zero-bucket case keeps the subject-less LimitObservationUnobserved: with no buckets there is no subject to carry and refusing every draw is right. Witnessed both directions — the sibling draw is admitted, and the undecoded bucket's own draw plus Unspecified and Automatic are all refused. limit_observation_blocks_dispatch was the only exhaustive match over the coproduct; the cursor standing match carries a catch-all. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Carry the native cause token on an exhausted bucket; name the dropped reset native_token carried limit_id, which the subject's native_key already carries — so the field restated the bucket and dropped the only thing it could have said. It now carries reached_type when the wire supplied one, falling back to limit_id because native_token is not optional and a bucket that reported exhaustion without a reached_type still has to name something actionable. resets_at is STILL DROPPED, and is now named on the carrier rather than discarded quietly. ProviderLimitObservation has no field to hold it — LimitUnavailableUntilReset is { subject, native_token, reason } — so "when does waiting become valid again" has nowhere to land. That is a model gap, not a projection choice, and serializing a timestamp into `reason` would put a machine fact in a prose field no consumer can read. Dissolve-on: LimitUnavailableUntilReset gains a typed reset instant. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Derive the limit credential from the press receipt, not from the caller Handback item 1 (review artifact 51237). provider_limit_observations_from_codex_press_evidence took the credential identity and the evidence as INDEPENDENT arguments, so a caller could take buckets observed under one CODEX_HOME and publish them as the standing of a different credential. The standing would be honestly decoded and attached to the wrong account — a forgery no arm refuses, because both arguments are individually valid. The receipt already carries the answer: CodexAccountPreflightSubject.credential is the exact ambient context the trip ran under. provider_limit_observations_from_codex_press_receipt derives the identity from it and gives the caller nowhere to supply one. CODEX_HOME is the identity because it IS the isolation mechanism (codex_state_root_isolation_note): two homes are two credential stores. codex_press_credential_identity takes the AmbientCodexCredentialContext rather than the whole subject — it depends on exactly what it needs, and that is also what makes it witnessable without a four-field fixture. Witnessed: two homes never collide, and the label is the home. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * JWKS: model the key set and the verification seam, which cannot yet verify The entitlement axis needs authenticated claims, and codex_auth's parse boundary is explicit that reading unverified claims is fine for showing which account a credential names and illegitimate for authorization. Selection eligibility is authorization. So the missing piece is signature verification, and this is its first half. Cited as three documents rather than one local vocabulary: RFC 7517 for the JWK and its members, RFC 7518 section 6.3.1 for the RSA parameters n and e, section 3.3 for RS256. They are independently versioned and independently extended. WHAT IT DELIBERATELY CANNOT DO. RSASSA-PKCS1-v1_5 is s^e mod n over a 2048-bit modulus plus a padding and digest check, and this corpus has no bignum, no modular exponentiation and no RSA primitive. That is a capability gap, not a modeling gap, and no amount of .dag closes it — it needs a realization handler bound to a host primitive, or bignum grounded in the substrate. So there is no fn here returning Bool for signature validity: such a function could only fabricate, and a `verified` that is always true because nothing checked it is the fabricated-plausible-output failure aimed at a security decision. jws_verification_unavailable is what every caller gets, naming the missing capability, counted rather than absorbed. n and e stay base64url strings for the same reason: decoding them needs the arithmetic the module does not have, so an Int carrier would claim a capability it lacks. Key selection is 0/1/many. RFC 7517 does not require kid uniqueness, so duplicates are a real wire state, and first-wins would decide which key authenticates a credential on list order. Absent and ambiguous stay distinct because refreshing the key set fixes one and not the other. An unmodeled key type decodes without material rather than failing the set — the key we need may be beside it. Recorded for whoever binds the handler: it must check the JWS header alg against what the key permits rather than trusting the header, because substituting none or an HMAC alg against an RSA public key is the standard JWS confusion attack. Dissolve-on: a bound handler with an executed positive control and a discriminating negative control. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * JWS: refuse the algorithm-confusion attacks, which need no bignum The header does not get to choose the algorithm. Both historical JWS confusion attacks work because the verifier read `alg` out of the token and did what the token asked: `none` strips the signature entirely, and HS256 against an RSA verifier signs with the PUBLIC key as an HMAC secret — public being the point. The defense is not a stronger primitive, it is deciding agreement from the KEY and only ever checking the header's claim against it. That is structure, not arithmetic, so it lands now rather than waiting for the exponentiation. Witnessed as attacks: an unsigned token refused against every key type, and HS256 against an RSA key as a mismatch. SCOPED DOWN MID-WRITE, and the reason is recorded on the carrier. I first modelled the compact split and header decode too, then found that string_split, drop, code_point_string and uint8_int do not exist — I had written four fabricated primitives, the same class as two earlier slips this session. The corpus consumes text by positional char folds (extdeps.auth.jwt jwt_first_colon_from is the idiom), so the split needs that fold written properly, and writing it badly means a verifier reading the wrong bytes. So the split, the segment-count check that refuses an unsecured JWS and a JWE, and the signing input are deferred with their dissolve-on named, rather than shipped as plausible code over primitives that do not exist. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Partition tick sessions by the coproduct, not a parallel string vocabulary Review artifact 51309 called this a follow-up modeling cleanup rather than a correctness gap, and that is right, but it is the nicknaming class so it is worth closing. belt_tick_session_is(s, arm: "running") compared string arms — a second naming scheme for BeltSessionLiveness, which already names exactly those states. The string version is strictly worse than the coproduct: a typo in an arm name compiles and silently empties a bucket, where a missing coproduct arm is a non-exhaustive match the compiler catches. belt_tick_session_class now returns BeltSessionLiveness and the four predicates match its arms. Node-awareness stays at this layer rather than moving into belt_session_liveness_from_process, because multiplicity is a fact about a node's ROWS while that function sees one row's process — the same split belt_node_session_liveness makes on the dispatch path. Landed on the stacked PR rather than #8132, which has three approvals sitting on a head whose CI run is finally in progress; restarting it for a cleanup the reviewer explicitly called non-blocking would trade a verified merge candidate for a tidier one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * JWS: land the compact split, so the segment count is checked The deferred half of the JWS structure. RFC 7515 section 7.1 is exactly three base64url segments joined by two periods, and the COUNT is a security fact rather than a parsing detail: two segments with an empty third is the unsecured JWS of section 6, five is a JWE. Verifiers that split on periods and read position two have accepted both as signed tokens, so each wrong count refuses by its own name. The signing input is carried on the split rather than rebuilt later, because RFC 7515 section 5.2 step 8 covers the ENCODED segments joined by a period, and reconstructing that from decoded parts is where a re-encoding difference silently produces different bytes than the ones the signature covers. THE SEGMENTER IS LOCAL AND THAT IS A COMPROMISE, stated on the carrier rather than hidden. Splitting on a separator is not a JWS concept and belongs in std, but no general split, index-of or substring exists in this corpus, and minting a std primitive is not a decision to take inside a JWS module. jws_segments is scoped and named for its subject. Dissolve-on: a general std separator fold lands and this becomes a call to it; a second consumer needing the same scan first is the signal to promote rather than copy. This closes the fabricated-primitive gap from the earlier commit — the scan is written against char_at / code_point / string_length, the idiom extdeps.auth.jwt already uses, rather than the string_split and drop I had invented. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Remove JWS/JWKS from the critical path; delete the rebindable evidence entry TWO CORRECTIONS, THE FIRST OF WHICH IS MINE TO OWN. JWT/JWKS IS NOT THE ENTITLEMENT JOIN. I built a signature-verification lane on the premise that entitlement required authenticated id_token claims, citing codex_auth's parse boundary. That note is correct and governs the auth.json id_token — a different surface. The app-server account/read response already carries the account realm, and the proof was a captured wire specimen in this repository's own test tree: {"result":{"account":{"type":"chatgpt","planType":"pro",...}}} That is the admitted Codex process answering an authenticated control request, not gunbc decoding an untrusted bearer token, so the prohibition never applied. I grepped for entitlement producers and for planType in the extdeps models; I did not read the response fixture, which settles it in one line. The lane is preserved on branch jwks-security-substrate rather than deleted — it is cited and correct as far as it goes — but it has no production consumer, cannot authenticate any constructible value, and brings this branch no closer to a provider turn. Keeping it here would make entitlement depend on a capability that does not exist. THE CREDENTIAL FIX WAS INCOMPLETE. Adding the receipt-taking entry point did not remove the forgery: provider_limit_observations_from_codex_press_evidence still took credential and evidence as independent arguments, so evidence observed under one CODEX_HOME could still be published as another account's standing. A safe path added beside an unsafe path leaves the unsafe path. Deleted — the only production entry consumes the complete receipt. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix the stale CapacityUnknown arm assertion left behind by the mixed-decode repair witness_capacity_unknown_is_not_capacity asserted LimitObservationUnobserved, the subject-less arm the bridge returned BEFORE review 51237. That repair moved CapacityUnknown onto LimitSubjectUnobserved so an undecoded bucket refuses its own draw without refusing a measured sibling; the witness was not re-read after the producer changed, so it reported the repair as a regression. The assertion is now stronger than a swapped label: it matches the subject and pins native_key, which is the fact the repair added and the whole reason the subject-carrying arm exists. The CI red is the discriminating receipt — the old arm fails against the current producer, the new one passes. Also merges main (#8182, #8180, #8164). * Decode the Codex account union and project entitlement from what it reports account/read's `account` member was decoded to "the object was nonempty" and stopped there, so an apiKey platform credential, an amazonBedrock contract and a personal ChatGPT subscription all reached the same Ready. Those are three different credential realizations, and a profile requiring personal ChatGPT OAuth is satisfied by exactly one of them. Grounded in the upstream schema rather than in our captured fixture: read from `codex app-server generate-json-schema --out` against @openai/codex 0.147.0, v2/GetAccountResponse.json. Two facts from it changed the design: Account is a CLOSED oneOf discriminated on `type` — apiKey | chatgpt | amazonBedrock — so the realm is an enumerable decode, not an open string. PlanType is a CLOSED 15-value enum whose members INCLUDE `unknown`. I was about to treat any nonempty planType as entitling, which would have read upstream's own I-do-not-know as a yes. It decodes cleanly and entitles nothing. The two negatives stay distinct because their remedies differ. A Bedrock account is REJECTED — read successfully, wrong realization, permanent until the credential changes. A plan or type outside the cited enum is UNOBSERVED — our pin is stale, repaired by editing a roster. Both refuse dispatch today, which is exactly why a witness asserting only "not available" would pass while the model conflated them. Entitlement policy lives at the bridge, not in the decoder: the press says what upstream reported, gunbc.codex_plan_is_entitling says which plans we draw on. OpenAI publishes no machine-readable plan→entitlement map, so the roster is a declared policy budget with `free` and `unknown` excluded by name, not a fabricated citation. Six witnesses, green by execution; mutating the roster's CodexPlanUnknown arm reds witness_upstream_unknown_plan_is_not_a_yes and leaves its sibling green. Downstream consumers re-run at full roster count: press 22/22, bridge 21/21, dispatch_selection 19/19, roadmap_dispatch_actuator 36/36. * Give the exhausted-bucket arm a typed cause and a typed reset LimitUnavailableUntilReset carried a required native_token and no reset, which produced two defects from one shape: The cause was `match reached_type { Present{t} => t Absent => limit_id }`. A bucket that reported exhaustion without naming a cause got the bucket's own id in the cause slot, so a reader could not tell an upstream-reported rate_limit_reached from our substitution. The substitution was not chosen — it was the only expression that typechecked, because a required field whose producer lacks a value MANUFACTURES a fallback. resets_at decoded off the wire and was dropped, so an arm named UntilReset could not say until when. Now ProviderNativeLimitCause (Reported{token} | Unreported) and ProviderLimitReset (ResetAt{at} | ResetInstantUnobserved). Both absent arms are reachable: rateLimitReachedType and resetsAt are optional upstream. An unobserved reset is not an immediate one — zero is the BEST possible reset and therefore the worst available default. THE WITNESS WAS PINNING THE DEFECT. witness_codex_bucket_projects_to_native_ bucket_never_account_scope asserted `t == "codex"` against a fixture declaring reached_type: none — so the value it held in place was the fallback itself. It now asserts NativeCauseUnreported, and a second fixture carrying both a cause and a reset proves the two project differently. Scope, declared: LimitWarning/Rejected/Exhausted/RateLimited keep bare tokens. They have one producer between them and no observed case of a missing token, so converting them would add an unreachable state. Trigger recorded on the arm. The superseded note is replaced rather than left beside the fix — it had named this exact change as its dissolve-on. Full-roster reruns: bridge 23/23, provider_standing 17/17, standing_selection 7/7, dispatch_selection 19/19, roadmap_dispatch_actuator 36/36, press 22/22. * Make the account-realm matches exhaustive instead of rostering new residue The non-fold residue ratchet found one unrostered site (stale count zero): my realm decoder matched JsonNull and JsonObject and swept the rest into `_`, and realm_from_account_read_frame did the same over the JsonMember arms. Rostering it was the wrong repair. A roster row carries a reason AND a dissolution trigger, so it is a net-new active dissolution obligation, and DESIGN §5 is explicit that a trigger is a lifecycle fact rather than permission — absent an operator verdict on this exact population, marked debt is refused exactly like unmarked debt. The obligation also would not have been true: there was nothing to dissolve to, because the exhaustive form was available now. Both matches now name every variant. JsonValue's four non-object non-null arms route through one named function rather than four copies of the same record, so exhaustiveness costs nothing in duplication. Verified: unrostered and stale counts both 0, the ratchet witness passes, and its two RED controls still hold. Bridge 23/23, press 22/22. * Cite the account schema from the pinned runtime, and narrow the entitling roster Two P0 corrections from analyst review, both real and both mine. P0-1 — the branch modeled a protocol no executable implements. I read the account schema from the codex that happened to be installed on this build host, 0.147.0, while every other fact in the module and the materialized bundle the turn executes are pinned at 0.146.0. I noticed the version gap while working and declared the new number in my notes instead of resolving the mixture. Measured against both executables rather than assumed: the Account union is structurally identical, but PlanType is 13 values at 0.146.0 and 15 at 0.147.0 — self_serve_business_prolite and enterprise_cbp_automation do not exist for the pinned runtime. So the model named two plans our executable cannot emit. The identical union is exactly why it was easy to miss: the part that changed was the part nobody diffed. Restated to 0.146.0, the version the runtime receipt admits. The two later strings now decode as CodexPlanTypeUnrecognized — a stale pin, which is the honest reading — and a witness asserts that rather than the note claiming it. The rule is not which version wins: a protocol fact comes from the exact executable the runtime admits, and a bump moves manifest, lock, artifacts, receipt and every fact together. P0-2 — the roster was a broad allow path from a locally authored assumption. It admitted every plan but free and unknown, in a note that simultaneously said no upstream plan-to-entitlement mapping exists. Narrowed to the single plan actually observed on the deployed credential, behind an explicit CodexPersonalSubscriptionPolicy so the set is unmistakably authored policy. A non-admitted plan reads UNOBSERVED, not REJECTED, on the same remedy line the module already draws: ratifying a plan is our-side like a stale pin, while an apiKey or Bedrock account is repaired only by changing the credential. Every previous assertion here was about a REFUSAL, which is why no witness noticed the widening. witness_deployed_profile_admits_exactly_the_observed_plan pins the admitted set at exactly one member, so a future admission reds first. Bridge 26/26, press 22/22, provider_standing 17/17, standing_selection 7/7, dispatch_selection 19/19, roadmap_dispatch_actuator 36/36, residue ratchet green with both RED controls holding. * PRESS-0 step 2: credential liveness split and HeldLease supervised turn Split account/read realm from rate-limit liveness: authentication derives from CodexCredentialLive (buckets returned) via the press receipt bridge, not from account/read alone — the continuity-receipt trap where chatgpt/pro coexists with a dead token. Model supervised execution on std.temporal_effect HeldLease in gunbc.codex_supervised_turn: turn/start admission refuses idle threads without a runner-written terminal receipt, and witnesses pin the trap. Wet srv1 shell-typed-invocation turn remains open on this vertical. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix parse error in codex_supervised_turn witness test. Leading == on a continuation line is invalid syntax; bind the policy comparison via let so the file parses and corpus discovery can run. Co-authored-by: Cursor <cursoragent@cursor.com> * Pin unobserved credential liveness in witness; mutation-checked traps. Extend witness_credential_liveness_splits_from_realm to assert CodexCredentialLivenessUnobserved maps to AuthenticationStandingUnobserved, not AuthenticationAuthenticated. Mutation checks confirm both traps red: idle-thread admission and unobserved-liveness authentication. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix compile-clean: remove unattached // prose from witness file. Standalone leading comment blocks lacked module-item subjects and failed dag_compile_clean_gate (64 annotation refusals). Rationale already lives in typed data witness_note rows per DESIGN 4c. Co-authored-by: Cursor <cursoragent@cursor.com> * Revert "Merge annotation-grain fix from #8215 to clear inherited compile-clean red." This reverts commit 50e02c3, reversing changes made to 1c97fc0. * Add supervised Codex turn runner for bounded wet execution. Implements run_codex_supervised_turn with HeldLease fencing, bundled-native app-server script (thread/start then turn/start), stdout parse, and runner-written terminal receipt with client_command_id; cites srv1 execution receipt for supervised-lease selection over detached reconciliation. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix non-fold residue in serialize_supervised_rpc_error. Replace JsonValue wildcard arm with exhaustive match over all six variants so non_fold_residue_no_unrostered_or_stale passes without a roster row. Co-authored-by: Cursor <cursoragent@cursor.com> * Add wet supervised-turn witness and srv1 handoff entry. Runner was already realized; this wires a falsifier-rehomed wet witness that materializes the bundled native, preflights via rateLimits, runs run_codex_supervised_turn, and asserts terminal receipt + client_command_id without belt dispatch. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix wet supervised-turn witness parse errors. Match-arm bodies need braces; split client_command_id check into let bindings so multi-line == does not follow && inside a match arm. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix wet witness parse: trailing == on continuation lines. Parser rejects continuation lines that START with == but accepts || (measured on main binary). Move == to end of prior line in wet_supervised_turn_terminal_ok; record defect in std.language_target_identity continuation_eq_operator_shape_note with hermetic witness repro controls. Co-authored-by: Cursor <cursoragent@cursor.com> * Record srv1 wet OOM receipt and add bisect witnesses. Full supervised wet witness killed at ~89 GiB with no child processes; move file to OfflineLocalRecipe, remove falsifier roster row, add bisect fns with declared MemoryMax envelopes for operator-bounded srv1 runs. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix wet bisect witness: bind registry_artifacts in match arm. Pattern used registry_artifacts: _ then referenced the name in the body, which fails compile before bisect step 1 can run. Co-authored-by: Cursor <cursoragent@cursor.com> * Isolate materialize leak: prepare split + lookup fold fix. Bisect confirmed leak in package_delivery.materialize_codex_runtime_bundle on main. Split prepare_codex_runtime_closure for narrower wet bisect; eliminate filter allocation in package_lock_lookup_node; record production defect note. No wet re-run until capped confirmation. Co-authored-by: Cursor <cursoragent@cursor.com> * Add wet bisect step 2b: select_codex_exact_target_closure only. Isolates closure selection and codex_wrapper_lookup / codex_target_package_lookup from materialize shell path for capped srv1 run at MemoryMax=2G. Co-authored-by: Cursor <cursoragent@cursor.com> * Drop wet bisect from witness enrollment until materialize is fixed. Convert bisect entrypoints from test fn to plain fn so Phase 0(b) admission does not count five UnclassifiedPathDeferral rows with zero consumers. Remove OfflineLocalRecipe exclusion row; file stays as operator-only reproduction via gunbc run. Co-authored-by: Cursor <cursoragent@cursor.com> * Add wet bisect step 2c: wrapper tarball acquire only. Isolates acquire_and_admit_registry_artifact for the wrapper after closure prepare — DownloadToFile plus sha512 verify, no platform pair or npm path. Co-authored-by: Cursor <cursoragent@cursor.com> * Add pre-shell materialize bisect entries after instrumented trace. Split source construct, prepare, and through_prepare from full materialize body eval; remove pre-mktemp from materialize wet witness so bisect has zero shell before materialize. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix wet bisect parse: data decl value must be same line as '='. Continuation-operator fix (#8259) does not cover declaration '=' breaks; corpus has zero split-line data rows. Co-authored-by: Cursor <cursoragent@cursor.com> * Add wet bisect rung: platform artifact acquire only. Ladder through through-prepare passes at 72f6ead; full materialize pins 8G — next isolate native platform tarball acquire. Co-authored-by: Cursor <cursoragent@cursor.com> * Add final materialize bisect seams: pair, npm ci, finish. Extract codex_runtime_install_from_prepared for install-through-verify; add through_pair_acquire, through_npm_ci_offline, and finish_after_install bisect entrypoints. Co-authored-by: Cursor <cursoragent@cursor.com> * Add finish-stage observe bisect rungs for materialize leak (#8166). One wet entrypoint per observe inside finish_codex_runtime_materialization_after_install plus a two-file tiny-tree fixture for observe_package_materialized_tree isolation. Co-authored-by: Cursor <cursoragent@cursor.com> * Remove duplicate npm import after main merge. Co-authored-by: Cursor <cursoragent@cursor.com> * Add single-file protocol schema interpreter bisect rung. wet_finish_parse_canonicalize_largest_protocol_schema_only installs Codex, generates the schema dir, then parse_json + canonicalize_json_value on only codex_app_server_protocol.schemas.json — no fold, manifest, serialize, or sha512. Co-authored-by: Cursor <cursoragent@cursor.com> * Restore package_delivery.dag after rebase conflict resolution. Auto-resolving rebase conflicts with main dropped PR materialize/bisect changes; restore the full #8166 package_delivery surface from pre-rebase tip. Co-authored-by: Cursor <cursoragent@cursor.com> * Take main's rack_power.dag to fix annotation grain CI red. Branch revert 45f81ae re-introduced body-grain // comments that main had already hoisted to module-item grain above PowerRefusal and rack_power_budget. Co-authored-by: Cursor <cursoragent@cursor.com> * Take main's spatial_projection and planar_projection annotation fixes. Complete the 45f81ae revert undo: hoist // comments to module-item grain in the two remaining files that rack_power fix alone did not cover. Co-authored-by: Cursor <cursoragent@cursor.com> * Drop false continuation_eq note; update accounting note for #8259. #8259 dissolved operator-leading continuation asymmetry for == and +. Remove the PR-only continuation_eq_operator_shape_note, restore main's continuation witness at src/v1/tests/claim/, and rewrite accounting_arithmetic_shape_note as a receipt rather than stale parser advice. Co-authored-by: Cursor <cursoragent@cursor.com> * Add parse-only rung for protocol schema JSON memory split. (#8272) Confirmed on srv1 under MemoryMax=8G: parse-only and parse+canonicalize both pin 8 GiB on codex_app_server_protocol.schemas.json (506,984 bytes, ~16,500x input). Defect is parse_json / JsonValue construction. Rebased onto press-0-step2 (8990f2a). Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com> Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com> * Address supervised-turn correctness floor for #8166. Keep stdin open through turn terminal, supervise process groups, persist client_command_id before turn/start, refresh in-session standing, and use generation-scoped lease binding; witnesses cover exit-0-not-observed. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix supervised turn JSON escaping and remove Python thread-id fork (#8166). Route turn/start through codex_app_server_turn_start_request_line (serialize_json), delete the embedded Python extractor, add typed supervised_thread_id_from_line for post-hoc decode, and mark the concat-built fifo coprocess as declared scaffold with dissolution toward host_effect_apply Phase 2. Co-authored-by: Cursor <cursoragent@cursor.com> * Document thread-id sed substitution assumption for supervised turn (#8166). Record that in-shell sed into the turn/start JSON line is interim and charset-unbound until protocol schema or typed transport lands. Co-authored-by: Cursor <cursoragent@cursor.com> * Delete supervised turn bash coprocess; wire typed host_effect transport (#8166). Operator RejectAndFinishNow: remove codex_supervised_turn_script (36 concat), retained_transport, and sed thread-id substitution. Add extdeps.llm.codex_app_server_stdio_session intent, CodexSupervisedWorkerTurn host effect, and gunbc.codex_supervised_turn_run routing through host_effect_apply; realize refuses until native session driver lands. Co-authored-by: Cursor <cursoragent@cursor.com> * Land Codex app-server stdio session driver for supervised turns (#8166). Native coprocess driver (pipe stdin, setsid, poll-to-terminal, process-group kill) ships as target/release/codex_app_server_stdio_session and is invoked through gunbc.host_effect_codex_supervised_turn via host_effect_apply CodexSupervisedWorkerTurn. turn/start uses JSON parse+re-serialize (no sed). ShellEffectApplied carries stderr for capture wiring. Co-authored-by: Cursor <cursoragent@cursor.com> * Register codex_app_server_stdio_session in self-host frontier for regen. Seed-retained intrinsic registration drives stage0_crate_layout_generated and emitted gunbc_stage0_crate_layout_generated so lib.rs and fresh self-compile agree on pub mod codex_app_server_stdio_session. Includes workflow regen drift from generated_artifact_gate main_wet. Co-authored-by: Cursor <cursoragent@cursor.com> * Enroll codex_app_server_stdio_session in extdeps scope frontier. Declare ExternalModelScope for the Codex app-server stdio session transport (citing github.com/openai/codex) and add the module to scope_carrier_paths so extdeps_scope_placement_gate admits the new extdeps file. Co-authored-by: Cursor <cursoragent@cursor.com> * Add CodexSupervisedWorkerTurn arm to converge_cli_applied_knob_count. Fleet converge CLI does not count supervised worker turns as applied knobs; return fallback like neighboring non-ConvergePlan HostEffect variants. Co-authored-by: Cursor <cursoragent@cursor.com> * Fail closed when Codex session preamble file cannot be read. Return exit 1 before spawning the coprocess instead of substituting an empty preamble (review 52819 / composer-2.5 REQUEST_CHANGES). Co-authored-by: Cursor <cursoragent@cursor.com> * Refuse invalid thread/turn-start-id argv instead of silent defaults. When --thread-start-id or --turn-start-id is present, a missing value or non-integer parse fails with exit 2 before spawn — same idiom as other required argv and the preamble read fix (review 52819 second instance). Omitted flags still default to 4 and 5. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix generation-store conflation for supervised turn exactly-once fence. Replace Int? collapse with CodexSupervisedGenerationRead coproduct, route store failures through codex_supervised_turn_generation_admission into turn-start refusals, and refuse when generation fence write fails. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix stdio session driver RPC id matching to exact JSON parse. Replace substring "id":{rpc_id} pre-filter with parsed id comparison so id 41 cannot satisfy rpc_id 4; aligns seed driver with codex_supervised_turn.dag exact-id matching. Co-authored-by: Cursor <cursoragent@cursor.com> * Remove frontier_probe_survey from release bin pack after roster deletion. Main deleted the bin with the self-host frontier roster; merge incorrectly re-enlisted it. Regenerate CI workflows via main_wet. Co-authored-by: Cursor <cursoragent@cursor.com> * Regen compiler_tests.rs after #8344 frontier roster deletion. Fresh seed rebuild + regen_stage0 --verify (divergence 0); removes stale Witness coercion/is_copy assertions dropped when frontier probe witnesses were deleted on main. Co-authored-by: Cursor <cursoragent@cursor.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: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com> Co-authored-by: Brian Searls <11205878+briansrls@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.
What this PR now contains
One hunk in
dag/product/rack_mount.dag: the trailingNO ROOM-FIT RELATION IN THIS INCREMENTannotation named no subject (§4c: a trailing block refuses), and now leads
rack_mounting_aperture_height— the aperture quantity the absent relation would consume, and thequantity its own closing sentence reasons about. Pure reorder; no semantic change.
Why the title changed
It previously read "Move 18 body-grain source annotations to module-item grain", which stopped
describing the diff. The 18 body-grain moves and the other trailing attachment landed
independently on main while this branch was open — a second session fixed the same refusal class
in
ci_deploy_witness_test.dag,host_phase_status_witness_test.dag,posix_principal_allocation_witness_test.dagandresolved_graph_cache_hand_rust_witness_test.dagwith different wording.
Merging main produced a conflict in exactly those four files: two independent solutions to one
problem. Main's side was taken in all four — the class is fixed there, and re-landing a second
wording of the same annotations would be a duplicate authority for one fact (§3). That is why the
diff collapsed from 18 hunks to 1, and the reviewer's question is answered: the other 17 are on
main, not missing.
Open judgment call
The remaining hunk is a judgment call, not a mechanical move. The annotation explains why a
room-fit relation is absent, so it has no natural subject; attaching it to
rack_mounting_aperture_heightis defensible but not forced. Deleting it instead is a legitimatealternative — in which case this PR is empty and should be closed rather than merged.