Skip to content

Give GitHubEffect a REST performer whose shape is hermetically verdicted - #10923

Merged
briansrls merged 17 commits into
mainfrom
session/bright-seal-548
Sep 10, 2026
Merged

briansrls merged 17 commits into
mainfrom
session/bright-seal-548

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 10, 2026 •

Copy link
Copy Markdown
Contributor

Summary

  • Bind GitHub REST as one transport rest realization (github.Http) with credentials as a Secret input, not argv and not an interface EnvVar.
  • Classify every RestOutcome from not-success: undocumented statuses refuse, 5xx/timeout/undecodable mutations are commit-ambiguous via mutation_status_is_commit_ambiguous, and a failure arm never widens.
  • First bound HTTP consumer is GET /user (a read). GitHubEffect path/method mapping is derived so JIT mint can post generate-jitconfig without this PR absorbing that lane.

What this PR establishes

A modeled REST realization whose shape is verdicted hermetically (classify fold plus perform_authenticated_user_read_binds_the_hermetic_fixture_login against the fixture login hermetic-mock-authenticated-user). That is not evidence that the performer reaches GitHub.

Neither wet witness ever executed. On required-witnesses-floor run 34430707763 (job 102725432805, head efaa5fd) both identities were NO-ROUTE / route-gap-before-verdict and never reached GitHub. They were deleted rather than kept as a promise.

Successor (capability, not a witness)

A required-lane route that may perform network effects against a real credential. Until that lane exists, a live 401 cannot gate. Restoring the functions, enrolling BinWitnessWet as it stands, or adding floor_route_gap on GetAuthenticatedUser does not supply that capability.

Test plan

  • Hermetic test.claim.github_effect_perform on the required witness floor (classify + path/method + fixture-login bind)

Rung: classify and the hermetic bind are mechanically preventable on the required floor. Live GitHub HTTP is unexecuted. Not structural.

…ification.

The first executing consumer is GET /user so a read proves the path without a commit-ambiguous mutation; JIT mint and R2 mint are left to their owners.

Co-authored-by: Cursor <cursoragent@cursor.com>
Brian Searls and others added 3 commits September 10, 2026 03:35
BinWitnessWet is not a required-floor lane, so those identities stayed planned without a terminal verdict. Keep the hermetic classify/path tests the floor actually runs.

Co-authored-by: Cursor <cursoragent@cursor.com>
…the fixture identity.

The floor needs an arm on the REST operation. One static mock cannot be both a live 401 and a live user, so the hermetic witness asserts the fixture spelling rather than GitHub.

Co-authored-by: Cursor <cursoragent@cursor.com>
… capability.

The hermetic mock is shape evidence. The successor is a required-lane network route against a real credential, not restoring functions onto a lane that cannot run them.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot gunbai-bot Bot changed the title Give GitHubEffect an executing REST performer Give GitHubEffect a REST performer whose shape is hermetically verdicted Sep 10, 2026
gunbai-bot Bot pushed a commit that referenced this pull request Sep 10, 2026
… no production dispatch, honest mitigatable rung, and every X envelope refusal.

Shadow Y stays beside recovered init until Y execs at host boot and the image is built from it; mint remains a #10923 frontier, not a performer.

Co-authored-by: Cursor <cursoragent@cursor.com>
…surface frontier.

A Bool true for every inhabitant restates the type. method and path stay for the named later GitHubEffect REST perform; this change does not absorb that mint.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63065 (two findings), verified against head after this commit:

  1. github_effect_is_mutation / always-green witness — agreed. Every GitHubEffect arm is a mutation by construction, so the fold and every_github_effect_is_a_mutation were a decoration. Deleted. Classify still takes mutation: Bool; a GitHubEffect perform will pass true. GET /user stays github.Http with mutation: false.

  2. method/path with no production perform — agreed they are not routed by perform_github_authenticated_user_read. Landing a GitHubEffect REST perform in this PR would absorb JIT mint, which this lane was told not to. Stated as a declared §3c frontier beside the folds: github_effect_http_surface_consumer_frontier. Named consumer is a GitHubEffect REST perform that issues those values and classifies as a mutation. Trigger: that import and call exist. Not satisfied by another witness.

— sent from bright-seal-548

AuthenticatedUser was a nickname for the same GitHub account subject sibling REST modules already consume. The hermetic fixture now includes type so the existing shape is fully inhabited.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63075: agreed. AuthenticatedUser was a nickname for extdeps.github.github.GitHubUser. GET /user now decodes that type; the hermetic fixture carries type: User as well as login and id. GitHubAuthenticatedUserRead is still the operation outcome, not a second user shape.

— sent from bright-seal-548

…ng rows.

Those rows were unclassified prose restating the annotations; they are not a rung_drop and were not consumed as program data.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63082: agreed. github_effect_perform_rung_note and github_http_handler_layering_note were unclassified String commentary duplicating the // blocks. Deleted the rows; kept and slightly completed the // annotations. This is not a gunbc.rung_drop: the live GET path never executed, so there is no drop of a previously higher rung to roster.

— sent from bright-seal-548

…e frontier.

github.Http named the transport. The perform algebra had no production caller and no §3c row; the hermetic witness is not that consumer.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63092, both findings, verified:

  1. Perform module dangling — agreed. Added github_effect_perform_consumer_frontier beside the algebra. Named consumer is a production func that calls perform_github_authenticated_user_read or classifies a GitHubEffect RestOutcome via classify_github_http_outcome. Trigger: that import and call exist outside test.claim. Not satisfied by another witness.

    The wet-witness deletion sentence is gone. Those functions never existed on origin/main; live GET /user is simply not executed in this change.

  2. service github.Http — agreed. Renamed to github.Users (module extdeps.github.users, file users.dag) to match the upstream Users family and the citation already on the module.

— sent from bright-seal-548

The dispatch path and verb already belonged to CreateDispatch; github_effect_http_path was a second join of the same endpoint.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63098: agreed. DispatchWorkflow was re-joining POST /repos/…/actions/workflows/…/dispatches, which github.Workflows.CreateDispatch already owns. Path and verb now live as workflow_dispatch_path / workflow_dispatch_http_method beside that operation; CreateDispatch and github_effect_http_path / github_effect_http_method consume them. Same move as org_generate_jitconfig_path.

— sent from bright-seal-548

The interpreter and rust emitter read method/path as source text, not eval_expr. Binding the shared fold there issued WORKFLOW_DISPATCH_HTTP_METHOD as the verb. GitHubEffect still consumes workflow_dispatch_path and workflow_dispatch_http_method as Strings.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63106: agreed. I verified eval of method uses authored_name_at (so workflow_dispatch_http_method becomes WORKFLOW_DISPATCH_HTTP_METHOD) and the rust emitter lowercases the identifier into client.workflow_dispatch_http_method. CreateDispatch is restored to method: POST and the interpolating path template — the only form both realizations support. github_effect_http_path / github_effect_http_method still consume workflow_dispatch_path and workflow_dispatch_http_method so DispatchWorkflow does not re-join the endpoint as a second fold. The transport row cannot be that fold until method/path are eval_expr.

— sent from bright-seal-548

…xpressions.

The interpolating template and workflow_dispatch_path are one endpoint in two spellings because method/path are source text, not eval_expr. Binding the fold there issued a fabricated verb. The trigger is that capability, not a copied-string witness.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63114: agreed — the fold and the CreateDispatch template are two spellings of one path, and a comment saying they must stay in sync is not a join.

Deriving the transport row from the fold is still the wrong arm: both realizations read method/path as source text, and binding the fold there issued WORKFLOW_DISPATCH_HTTP_METHOD (review 63106). The fork is now a declared row, workflow_dispatch_transport_eval_frontier: named capability is rest transport method/path as eval_expr in both realizations; trigger is that, sufficient to delete this row and the interpolating template; not satisfied by a witness that compares the fold to a copied string, and not satisfied by issuing an identifier as a verb.

— sent from bright-seal-548

… drop the dispatch path fork.

classify_github_http_outcome was a third name for the same not-success algebra already written at CreateSecret, AddVersion, and DeleteSecret. Those sites now consume classify_rest_outcome. CreateDispatch's interpolating template is again the only dispatch path; GitHubEffect no longer re-joins it.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63120, both findings:

  1. Agreed — classify_github_http_outcome was not GitHub-specific. The fold is now classify_rest_outcome / RestExchangePerformance in extdeps.transports.rest, beside mutation_status_is_commit_ambiguous (moved there from secret provision). create_secret_for_attempt, add_initial_version, and delete_observed_secret consume it. GET /user still classifies as a read (mutation: false). Reads with extra policy (404 = absence) stay local.

  2. Agreed that a declared frontier does not join the two dispatch path spellings. Deriving the transport row from the fold is still the fabricated-verb arm (review 63106). Deleted workflow_dispatch_path / workflow_dispatch_http_method and the GitHubEffect method/path mapping that re-joined the endpoint. CreateDispatch's template is the path authority. A later GitHubEffect perform for dispatch should call that operation, not a second String.

— sent from bright-seal-548

… not a caller Bool.

A one-word mutation: false on CreateSecret could reclassify a 5xx as retryable; the standing constructors make that a different type, and the module is renamed to the GET /user fold it actually holds.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63124 (REQUEST_CHANGES on classify_rest_outcome taking a caller Bool, and on gunbc.github_effect_perform holding no GitHubEffect performer):

  1. classify_rest_outcome now takes RestExchangeStanding (RestReadExchange | RestMutationExchange), not mutation: Bool. CreateSecret / AddVersion / DeleteSecret wrap RestMutationExchange; GET /user wraps RestReadExchange. A one-word flip of mutation: false on CreateSecret is unwritable. Call sites still choose the constructor until dispatch/emit can carry standing from the op readonly flag — that is rest_exchange_standing_from_operation_readonly_frontier in extdeps.transports.rest, not a silent Bool. Hermetic witnesses still assert 5xx-on-read is refusal and 5xx-on-mutation is commit-ambiguous.

  2. The module is now gunbc.github_authenticated_user_read (perform_github_authenticated_user_read only). There is still no GitHubEffect performer; JIT/R2 mint stays out of this PR.

— sent from bright-seal-548

…not RestExchangeUndecodable.

RestExchangeUndecodable already means the body could not be read; a 200 user with an empty login is a different domain fact.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63128: confirmed. After RestExchangeSucceeded, an empty decoded login was minted as RestExchangeUndecodable, which already means the body could not be read. That path is now GitHubAuthenticatedUserLoginAbsent { user } on GitHubAuthenticatedUserRead — a domain arm, not a RestExchange* reuse. Transport refusals stay on GitHubAuthenticatedUserRefused.

— sent from bright-seal-548

…s observation-only.

RestExchangeRefused already meant no response arrived; the new performance arm with status and body was a second contract under the same name.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

review 63130: confirmed. RestExchangePerformance.RestExchangeRefused { status, body } collided with RestExchangeObservation.RestExchangeRefused { cause } (no response arrived). The performance arm is now RestExchangeStatusRefused. Observation RestExchangeRefused is unchanged. classify_rest_outcome and the secret/printer/GET /user witnesses follow the new constructor.

— sent from bright-seal-548

…n bind RestOk.

mock_response runs with an empty env; a bare RestOk there is an undefined variable, so the fixture-login witness never reached a terminal verdict.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

CI on b577499: required-witnesses-floor (witnesses is the aggregator). The PR-owned red is test.claim.github_authenticated_user_read.perform_authenticated_user_read_binds_the_hermetic_fixture_login — mock_response evaluated RestOk with an empty env (undefined variable), so the changed witness had no terminal verdict. The mock outcome is now the module data row hermetic_get_authenticated_user_outcome (9753cf5).

The other adjudicate blockers (parse 17 on megarac_media_attach.dag body annotations, namespace-wave-admission) are origin/main, not this diff.

— sent from bright-seal-548

The last push left users.dag unparseable, so the module index refused and every required lane failed before the floor.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

CI on 9753cf5: all four reds were one parse. users.dag had an extra } after mock_response, so the module index refused (expected item declaration). Build, heal, floor (measurement_unreached), and the witnesses aggregator all followed from that. Extra brace removed in 2c3783a.

— sent from bright-seal-548

@gunbai-bot

gunbai-bot Bot commented Sep 10, 2026

Copy link
Copy Markdown
Contributor Author

CI on 2c3783a: required-witnesses-floor is red; witnesses is the aggregator. Build and heal passed. Every changed github_authenticated_user_read witness planned-and-passed, including perform_authenticated_user_read_binds_the_hermetic_fixture_login.

The two adjudicate blockers are origin/main, not this diff: parse 17 on dag/gunbc/machine_intake/megarac_media_attach.dag (source annotation inside a declaration body), then namespace-wave-admission (no head index) as the follow-on. This branch does not contain that file. I am not absorbing the megarac annotation-grain repair here.

— sent from bright-seal-548

gunbai-bot Bot pushed a commit that referenced this pull request Sep 10, 2026
… no production dispatch, honest mitigatable rung, and every X envelope refusal.

Shadow Y stays beside recovered init until Y execs at host boot and the image is built from it; mint remains a #10923 frontier, not a performer.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls
briansrls merged commit 4024a3a into main Sep 10, 2026
2 of 4 checks passed
@briansrls
briansrls deleted the session/bright-seal-548 branch September 10, 2026 14:59
gunbai-bot Bot pushed a commit that referenced this pull request Sep 10, 2026
…sclassified it

The wave wall refuses this PR's own repair. It classifies

  base {} -> head {extdeps.transports.rest}

as NewPoolCoincidenceResolution, which refuses. By the 2026-08-27
operator ruling in gunbc.compiler_frontend_program_interlock, an author
writing the import that resolves a name the module was ALREADY SPELLING
is AuthoredReferenceResolution, which auto-admits -- a distinction that
ruling drew after the wall refused gunbc#9485, also a one-line import
repair. This is that case exactly.

It lands in the wrong arm because locally_authored_claim_added decides
authorship with names_leaf, which reads `c.members` and never `c.target`.
The base names the leaf from the wrong module and the head names it from
the right one, so `names_leaf(head) && !names_leaf(base)` is false. The
predicate can see a name appearing where it was ABSENT; it cannot see a
name whose SOURCE changed.

What makes that a defect rather than a rough edge: a REDUNDANT blanket
import would have tripped the blanket_targets branch and auto-admitted.
The wall is easier to satisfy by writing worse code, so it teaches the
wrong repair. I did not write the blanket import -- noticing you are
implementing a workaround is the line-stop signal (DESIGN section 5) --
and escalated instead. Admit was ruled; the predicate fix lands
separately against a green main, because repairing a wall in the same
motion that asks it for an exception makes the exception look bought.

The row also fixes the attribution, which I had wrong twice: neither
contributing change is wrong in isolation. #10925 wrote the import when
the fn WAS declared in secret_provision_actuator; #10923 then deleted it,
rehoming it correctly and leaving one edge at the old address. The defect
exists only in their composition.

Roster was empty at this base -- verified against 495cde7 rather than
against my other worktree, which carried two rows deleted upstream. The
row carries its own deletion trigger.

cargo check -p v1-compiler: Finished, 0 errors.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016jFtgPtXxTj1kE8wwZUNsG
briansrls pushed a commit that referenced this pull request Sep 10, 2026
…le that declares it (#10945)

* Import mutation_status_is_commit_ambiguous from the module that declares it

main is red on the declarations phase:

  declarations FAIL IMPORT-MEMBER-ABSENT dag/gunbc/cloudflare/r2_token_mint_run.dag:69:3
  imports `mutation_status_is_commit_ambiguous` from `gunbc.secret_provision_actuator`,
  which declares no such name

The symbol has exactly one declaration in the corpus, `extdeps.transports.rest` at
rest.dag:111, and `secret_provision_actuator.dag:238`'s own annotation already names
that as its home. The importing module ALREADY imports `extdeps.transports.rest` at
line 8, so this moves one name between two import lists that both exist. Nothing is
renamed, added or deleted.

Measured on both arms through `gunbc compile --entry
dag/gunbc/cloudflare/r2_token_mint_run.dag`, discriminating rather than asserted:

  unfixed (origin/main)   1 blocking error(s), 815 advisory
  fixed                   0 blocking error(s), 815 advisory, 132 files emitted

The advisory count is identical across the arms, so the edit moved exactly the one
thing it claims to. Note the compile exits 0 while carrying a blocking error, so the
count line is the signal and the exit code is not.

Cut as its own change rather than folded into the census PR that surfaced it: one PR,
one question.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016jFtgPtXxTj1kE8wwZUNsG

* Admit the stranded-caller repair's binding delta, and say the wall misclassified it

The wave wall refuses this PR's own repair. It classifies

  base {} -> head {extdeps.transports.rest}

as NewPoolCoincidenceResolution, which refuses. By the 2026-08-27
operator ruling in gunbc.compiler_frontend_program_interlock, an author
writing the import that resolves a name the module was ALREADY SPELLING
is AuthoredReferenceResolution, which auto-admits -- a distinction that
ruling drew after the wall refused gunbc#9485, also a one-line import
repair. This is that case exactly.

It lands in the wrong arm because locally_authored_claim_added decides
authorship with names_leaf, which reads `c.members` and never `c.target`.
The base names the leaf from the wrong module and the head names it from
the right one, so `names_leaf(head) && !names_leaf(base)` is false. The
predicate can see a name appearing where it was ABSENT; it cannot see a
name whose SOURCE changed.

What makes that a defect rather than a rough edge: a REDUNDANT blanket
import would have tripped the blanket_targets branch and auto-admitted.
The wall is easier to satisfy by writing worse code, so it teaches the
wrong repair. I did not write the blanket import -- noticing you are
implementing a workaround is the line-stop signal (DESIGN section 5) --
and escalated instead. Admit was ruled; the predicate fix lands
separately against a green main, because repairing a wall in the same
motion that asks it for an exception makes the exception look bought.

The row also fixes the attribution, which I had wrong twice: neither
contributing change is wrong in isolation. #10925 wrote the import when
the fn WAS declared in secret_provision_actuator; #10923 then deleted it,
rehoming it correctly and leaving one edge at the old address. The defect
exists only in their composition.

Roster was empty at this base -- verified against 495cde7 rather than
against my other worktree, which carried two rows deleted upstream. The
row carries its own deletion trigger.

cargo check -p v1-compiler: Finished, 0 errors.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_016jFtgPtXxTj1kE8wwZUNsG

---------

Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 10, 2026
…h sides had live rows

The same file conflicted as last merge, but not the same case, and the difference decides the
resolution. Last time this branch had 40 SCM rows and `main` had reached an EMPTY roster, so
keeping ours dropped nothing. THIS TIME BOTH SIDES CARRY LIVE ROWS: ours are the 40 SCM deltas,
main's is one for the gunbc#10945 stranded-caller repair. Choosing either side whole would delete
obligations the other still owes, and a delta nobody adjudicated is exactly what this wall exists
to refuse -- so the rosters are APPENDED, 41 rows.

Main's account of the stranding is kept verbatim rather than summarised, because it is the history
of a defect rather than this branch's commentary, and because it independently reached the
attribution this session had already corrected to: neither contributing change was wrong alone.
#10925 wrote the import while the fn was still declared in `secret_provision_actuator`; #10923 then
deleted it, rehoming it to `extdeps.transports.rest`; the defect lived only in their composition.
Main's note adds the detail this session did not have -- #10923's floor concluded four hours before
#10925 landed, so the verdict that would have caught the stranding was computed against a base that
did not yet contain the importer it was about to strand. A concluded verdict, correct about the
world it measured, in a world that no longer existed at merge time.

TWO DEFECTS OF MINE ON THE WAY IN, both caught by a check rather than by my reading. The union was
written by a script that took `&[` to mean the array literal and matched the TYPE ANNOTATION
`&[TransitionAdmission]`, emitting a malformed row header -- found by reading the resulting array
instead of trusting the script's success line, which is the false-deletion shape this branch hit
earlier. Then the appended row carried the wrong indentation for its nesting, and the pre-commit
hook refused the commit; that is the hook doing its job, not an obstacle to route around.
`cargo check -p v1-compiler --lib` ran on the working tree (the runner reports applying the patch,
so it checked this edit rather than a committed SHA) and finished clean.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
briansrls pushed a commit that referenced this pull request Sep 10, 2026
…ed arm emits (#10927)

* Model per-attempt steps 3-9 so a grant disagreement or empty credential cannot reach the jailer.

The host boot script's jailer exec had no authority; this ordered planner consumes the existing network and attempt modules, mints only after grant_authorizes_reservation, and treats a clean VMM exit as non-evidence that work ran.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Make PlacementBeforeExec a real coproduct so the jailer planner typechecks.

A one-arm `type X = Variant` was an alias to an unresolved name, which refused the floor with a cascade into FreeMonoid.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Carry the staged-Y cutover in the corpus: unbound capability trigger, no production dispatch, honest mitigatable rung, and every X envelope refusal.

Shadow Y stays beside recovered init until Y execs at host boot and the image is built from it; mint remains a #10923 frontier, not a performer.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Carry JIT envelope size as ByteSize instead of a bare Int.

Floor, ceiling, EnvelopeStanding magnitudes, and the admit comparison now use std.measure so credential size is not a second unit.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Restore the mke2fs populate annotation to its subject, and create the workspace before formatting it.

Leading // now attaches to the declaration it describes. The planner emits busybox dd (sparse 4 GiB) then mke2fs, matching X's two-step workspace rather than format-only.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Make authorized launch imply placement, and delete permanently-green Bool wrappers.

LaunchAuthorized no longer carries PlacementNotEstablished. VMM standing is only WorkNotEstablished, matched at the witness. PID1 refusals stay outside the plan by having no constructor.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Rename the authorized-path witness so it claims field and argv binding, not consumption.

The witness inspects a plan; it does not run a jailer.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Delete the false constants and the witnesses that could only red by editing them.

Shadow standing, recovered dissolution, and the jailer cgroup-version flag are import-graph and annotation facts. The remaining frontier witness matches UnboundDissolution versus BoundDissolution.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Make VMM work-standing a record type, not a one-constructor alias.

`type WorkStandingFromVmm = WorkNotEstablished { ... }` was the same coproduct-as-alias defect that made GrantCommitted unresolvable against FreeMonoid.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Name an admission-axis refusal instead of reporting an in-bounds payload as over-ceiling.

credential_bytes_admit is three conjuncts; reconstructing the cause from size alone fabricated EnvelopePayloadAboveCeiling when the axis standing was not AxisRequired.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Stage jail-root artifacts so authorized launch binds host files to in-jail drives.

Create and format work.img under the jailer chroot root, copy kernel and rootfs there, and make the witness check dd of= against the workspace drive's path_on_host. JIT device write stays an unbound frontier until the mint lands.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Drop the unused jailer tarball path and the attempt-dir workspace nickname.

The authorized planner already places work.img under the jailer chroot; a second attempt-root work.img function was a second answer to the same question. Isolation stays on the attempt-owned jail base.

Co-authored-by: Cursor <cursoragent@cursor.com>

* Refuse an empty issuance list in the zero-byte credential witness.

An empty issued_pairs arm returning true would green the floor RED without exercising EnvelopePayloadBelowFloor.

Co-authored-by: Cursor <cursoragent@cursor.com>

---------

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls pushed a commit that referenced this pull request Sep 10, 2026
…in_offers_single_cabinet (#10968)

main is RED on the declarations check:

  required-ci: declarations FAIL IMPORT-MEMBER-ABSENT
    dag/test/claim/colo_nj_central_south_census_test.dag:13:51
    `test.claim.colo_nj_central_south_census` imports `grain_admits_single_cabinet`
    from `test.claim.colo_cabinet_density_witness`, which declares no such name

NEITHER CONTRIBUTING CHANGE IS WRONG IN ISOLATION, and the composition is the defect.
#10865 (a675b70, merged 19:45:49Z) renamed `grain_admits_single_cabinet` to
`grain_offers_single_cabinet` in the shared witness module and updated every call site it
could see. #10864 (de7622e, merged 19:46:19Z) imports the old name, which existed when
that PR was written. The two merged THIRTY SECONDS APART, both MERGEABLE/CLEAN with all four
required checks green, and neither floor verdict could contain the other's change.

This is the third instance today of one class: a stranded caller, produced by two changes
whose verdicts were each concluded, correct, and computed against a base that excluded the
other. The earlier two were the megarac §4c break (#10630) and the
`mutation_status_is_commit_ambiguous` rehoming (#10925 wrote the edge, #10923 deleted its
target). A 30-second gap is the sharpest form: waiting longer for a floor to conclude does
not help when both floors HAD concluded.

The repair follows the rename rather than reverting it. `grain_offers_single_cabinet` carries
the identical signature `(g: RetailGrainStanding) -> Bool` and the identical body — it folds
`retail_grain_single_cabinet_wording` to a Bool — so this is a pure spelling change at eight
call sites, and the new name is the one the shared module now declares.

EVIDENCE
- GREEN by execution: `gunbc compile --entry dag/test/claim/colo_nj_central_south_census_test.dag`
  -> rc=0, `0 blocking error(s)`, `compiled: 61 files emitted`, zero IMPORT-MEMBER-ABSENT.
  The completion marker is quoted beside the count deliberately: a count with no completion
  marker beside it is a claim about the pipeline rather than about the subject.
- RED control, on the real acceptance path: main's own required floor on de7622e, run
  34522373789, reporting this exact finding. The failing content is the parent of this commit.

Both contributing lanes are archived, so this was cut by a blocked lane rather than routed.


Claude-Session: https://claude.ai/code/session_01998xs4ojJKWGptxcuxVWHN

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 11, 2026
…ures; the private gap as a typed stall; the within-tree half re-homed

Answers review 63772 / 63786 (a transcribed measurement with no producer) and the
manager's 2026-09-11 rulings, by landing the producer rather than softening the
claim.

THE INSTRUMENT. v1_compiler.bin.joint_claim_join computes, per change, the
export-surface entries removed (declared | variants | reexported, base minus
head) and the import claims added and retired, from only the diff-touched files
on both sides through namespace_wave_admission base_records and diff_sides, and
joins every admitted pair. A claim is joined only while LIVE when the entry
leaves: not retired by the removing change itself, and in retrospective mode not
retired by any change that landed between the pair. raw_candidates is reported
beside findings so the width the exclusion removes stays a number. Seven
fixture-boundary controls, real parser, real join: one positive control per
instance shape (variant deleted, name renamed, re-export dropped), one RED per
exclusion, one for the pair predicate, one for a claim already at the base.

WHAT IT ANSWERS, cited by invocation in the plan and not transcribed:
`joint_claim_join 6a54695^..f078c59` (first-parent main since
2026-08-28, default 3-day window) reports subjects=373 raw_candidates=236
findings=4 -- exactly the three 2026-09-10 instances (instance 1 is two names).
The two candidates the first-exclusion-only run reported as findings were both a
third commit retiring the claim between the pair (#10617 for the harness one; the
DensityMarketedMax one likewise); two artefacts with one cause was a defect in the
retrospective's pair predicate, built in as the second exclusion with its own
control rather than described.

TWO CORRECTIONS THE INSTRUMENT MADE TO THE SCOPE. Instance 2 (#10923 x #10925)
was a MOVE, not a dropped re-export: the base declared
mutation_status_is_commit_ambiguous in secret_provision_actuator and #10923
re-homed it; the instrument reports `(declared)` and the plan's table now says so.
The dropped re-export stays covered by the surface and keeps its control.

THE RULINGS. Checkpoint 2 stops at the pull-requests:read permission row on a
required job (the operator's trade); the dashboard reader is costed in section
4.1 and preferred on every axis but authority. The private gap is a typed
GuaranteeStall row (joint_claim_join_private_corpus_unindexed_stall) with the
overlay's extra-source-root trigger as its grounding, not prose. The within-tree
field-set case is NOT a checkpoint here: its home is
witness_that_fails_to_compile_is_absent_rather_than_red, and this change appends
a receipt there widening the trigger from claim-root files to the ruled capability
-- every construction site of a type whose field set changed, regardless of gate
closure -- per section 4b(3), rather than minting a second authority.

Hand Rust is enumerated in gunbc.joint_claim_join_seed_growth (33 items, no impl
block, every one citable) and rostered in seed_growth_admission.

Verified remotely: clippy -D warnings clean on the bin, 7/7 tests, the
retrospective above, and v1_src_dag_parse over the corpus with every new .dag
present: 5461 files parse-clean, no findings.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QzQcQRu3WKxJuWV2zaiHSW
briansrls pushed a commit that referenced this pull request Sep 11, 2026
…t 1: joint_claim_join, the instrument behind its figures (#11044)

* Scope the jointly-incompatible-open-PR mitigation: a claim-channel x surface join over the declaration index, advisory-first

Three 2026-09-10 reds on main were pairs of individually-green, textually
disjoint PRs whose union does not compile. This records the scope of a
mitigation and builds nothing, answering the four questions the brief asked
before any shape:

THE CUT. All three public instances are one finding kind, ImportMemberAbsent,
and only one was a deletion: #10865 was a rename, and #10923 dropped a
RE-EXPORT with no declaration deleted anywhere. The cut is therefore the
surface predicate the declarations rider already applies, import_surface_has
(declared | variants | reexported) as a base-minus-head DELTA, not the kind of
edit. The general case is every claim channel the index carries -- imports,
citations, rostered rows (#10769, #10718 are the same shape through the other
two) -- and the residuals the index cannot see are named: field rename,
arity/signature, and pure freshness (private #49 x #50).

THE COST. namespace_wave_admission already reconstructs a base index beside
the head index from only the diff-touched files, per run, in the witnesses
lane; the join is A(I) & R(D) minus the claims D itself retires, a set
intersection, not a pairwise compile. Measured retrospectively over 374
first-parent commits since 2026-08-28: the raw join is a 207-hit candidate
list (the superset trap); with the one exclusion it is 5 hits, 4 of them the
three brief instances, the fifth an ordering artefact an open-PR-set join
excludes by construction. Recall 3/3 on the window's ImportMemberAbsent reds.

THE PLACEMENT. No new job (roster closed): a rider on the parse phase, like
rostered_row_join, advisory, reporting and annotating without pushing a phase
failure; the one emitted-workflow change is a pull-requests: read permission
row. The freshness caveat of a push-time verdict is stated as the reason this
sits beneath the ceiling.

THE REFUSAL. One finding per removed entry x claiming site: the (module,
name) and which surface it left, the sibling PR and head, the claiming module,
in_declaration and SourceLocation; NotEvaluated when the open-PR set is
unobservable, never an empty hit set.

gunbc-private: no parse phase, the overlay is outside DAG_PARSE_SWEEP_ROOTS,
so the join is public-only today; 113/114 private modules import from public,
a cross-repo exposure no public PR is ever compiled against, named and left
to warm-badger-62's lane.

Ceiling stays with gunbc.plans.ci_merge_freshness and the landed, deferred
receipt_is_admissible; this record retires with it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QzQcQRu3WKxJuWV2zaiHSW

* chore: regenerate drifted generated artifacts (ci auto-heal)

Ledger-Repair-Judged: docs/design-rung-drops.md

* Checkpoint 1: joint_claim_join, the instrument behind the scope's figures; the private gap as a typed stall; the within-tree half re-homed

Answers review 63772 / 63786 (a transcribed measurement with no producer) and the
manager's 2026-09-11 rulings, by landing the producer rather than softening the
claim.

THE INSTRUMENT. v1_compiler.bin.joint_claim_join computes, per change, the
export-surface entries removed (declared | variants | reexported, base minus
head) and the import claims added and retired, from only the diff-touched files
on both sides through namespace_wave_admission base_records and diff_sides, and
joins every admitted pair. A claim is joined only while LIVE when the entry
leaves: not retired by the removing change itself, and in retrospective mode not
retired by any change that landed between the pair. raw_candidates is reported
beside findings so the width the exclusion removes stays a number. Seven
fixture-boundary controls, real parser, real join: one positive control per
instance shape (variant deleted, name renamed, re-export dropped), one RED per
exclusion, one for the pair predicate, one for a claim already at the base.

WHAT IT ANSWERS, cited by invocation in the plan and not transcribed:
`joint_claim_join 6a54695^..f078c59` (first-parent main since
2026-08-28, default 3-day window) reports subjects=373 raw_candidates=236
findings=4 -- exactly the three 2026-09-10 instances (instance 1 is two names).
The two candidates the first-exclusion-only run reported as findings were both a
third commit retiring the claim between the pair (#10617 for the harness one; the
DensityMarketedMax one likewise); two artefacts with one cause was a defect in the
retrospective's pair predicate, built in as the second exclusion with its own
control rather than described.

TWO CORRECTIONS THE INSTRUMENT MADE TO THE SCOPE. Instance 2 (#10923 x #10925)
was a MOVE, not a dropped re-export: the base declared
mutation_status_is_commit_ambiguous in secret_provision_actuator and #10923
re-homed it; the instrument reports `(declared)` and the plan's table now says so.
The dropped re-export stays covered by the surface and keeps its control.

THE RULINGS. Checkpoint 2 stops at the pull-requests:read permission row on a
required job (the operator's trade); the dashboard reader is costed in section
4.1 and preferred on every axis but authority. The private gap is a typed
GuaranteeStall row (joint_claim_join_private_corpus_unindexed_stall) with the
overlay's extra-source-root trigger as its grounding, not prose. The within-tree
field-set case is NOT a checkpoint here: its home is
witness_that_fails_to_compile_is_absent_rather_than_red, and this change appends
a receipt there widening the trigger from claim-root files to the ruled capability
-- every construction site of a type whose field set changed, regardless of gate
closure -- per section 4b(3), rather than minting a second authority.

Hand Rust is enumerated in gunbc.joint_claim_join_seed_growth (33 items, no impl
block, every one citable) and rostered in seed_growth_admission.

Verified remotely: clippy -D warnings clean on the bin, 7/7 tests, the
retrospective above, and v1_src_dag_parse over the corpus with every new .dag
present: 5461 files parse-clean, no findings.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QzQcQRu3WKxJuWV2zaiHSW

* State the population compile's boundary on the row: compilability of the claim-root population, not evaluation of it

A file that compiles and whose test fns are declared but never reached from the
entry passes that wall untouched (cool-badger-34's four fns, 2026-09-11). That
hole is discriminating_arm_built_but_never_enrolled's, named as the neighbour so
the word POPULATION is not later cited for a scope the trigger never claimed.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QzQcQRu3WKxJuWV2zaiHSW

---------

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>
gunbai-bot Bot pushed a commit that referenced this pull request Sep 11, 2026
…t main's new witnesses hit

Two blockers on 761f9af, and only one of them was the roster.

1. THE RECEIPT. Required floor run 34651932681 reported all three gunbc#11071 rows as CONSUMED
ADMISSION ... already satisfied at the base, and refused with 3 consumed admission(s) due for
deletion on this roster-touching change. Deleted. Third time this branch has carried another lane's
fresh rows through a merge and had the wall order their deletion, and the union was right all three
times: what deletes a row is the receipt, never the expectation, however reliable the expectation
has become. Main's TRIGGER paragraph stays -- it records when they came due.

2. A SEMANTIC MERGE CONFLICT I CAUSED. The floor also refused with

  fabric_m0_commit_witness_test.dag:194: type mismatch:
    expected 'Coproduct(CasStoreFailure)', got 'Coproduct(CasUnreadableSlot)'

This branch changed `CasStoreRefused` to carry a `CasStoreFailure` rather than a `CasUnreadableSlot`
directly, because a conditional write can reach the store, satisfy its precondition, and still fail
to PUBLISH -- reporting that as a malformed head was the conflation the widening removed. Main then
landed fabric-M0 witnesses written against the old shape. NEITHER SIDE IS WRONG ALONE; the defect
exists only in their composition, which is exactly the stranded-caller shape that took main down
earlier this week with #10923 and #10925. The difference is that this time the type change is mine,
so the repair is mine: I am the one composing them.

THE FLOOR NAMED TWO SITES AND THERE WERE FOUR, across three files -- it stopped early. Repairing
only the cited lines would have left two more to surface on the next run, which is the same
fix-the-quoted-instance-rather-than-retire-the-claim pattern this branch recorded two commits ago
when a narrowed word survived forty lines below its own correction. All four now wrap as
`CasSlotObservationRefused { cause: ... }`, and the constructor is imported where it was missing.
Verified by sweeping for the old shape corpus-wide rather than by re-reading the error: 0 remain.

Roster census after deletion: 40 rows, 31 SCM_MERGE_BASE_COHOME + 9 SCM_SOURCE_RECOVERY_REHOME.
All three fabric modules resolve clean; cargo check -p v1-compiler --lib finished clean; section 4c:
0 violations.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant