Model the GitHub App manifest acquisition flow end to end, with the route that runs it

[gunbai-bot]

The operator creates GitHub Apps by hand, repeatedly, because nothing declared their shape. This declares it once, renders the manifest document GitHub's registration form accepts, and converges the App that comes back — with no hand-entered permission set.

What lands

extdeps.github.app grows the manifest half of the subject it already owns, rather than a second module naming GitHubAppRegistration (which that file's own note calls the §3 fork):

• GitHubAppManifest — name, url, hook_attributes, redirect_url, callback_urls, setup_url, description, public, default_events, default_permissions — with permissions expressed through the existing GitHubPermissionAxis / GitHubAppPermissionAccess system.
• The two pieces that system was missing: permission_access_wire_name / _from_wire, and observed_permissions_from_wire_map, which folds GitHub's permission object (Map<String,String>) onto ObservedGitHubPermission. Both refuse an unrecognized value rather than defaulting to read.
• The manifest is rendered as a JsonValue through extdeps.languages.json.emit (cited to RFC 8259) — the manifest is not sent by this process at all; GitHub takes it as a form field from the owner's browser.
• app_manifest_registration_url — user and organization targets, state percent-encoded, no arm that omits the state.
• github.AppManifests.ConvertManifestCode (POST /app-manifests/{code}/conversions, no auth — the code authenticates it), github.AppPublicRegistry.GetApp, github.AppInstallations.ListInstallations, and the installation-token request rendered to its wire with no operation, because it needs a JWT nothing here can sign.
• GitHubAppInstallationRecord + installation_from_record — the wire shape kept separate from the modelled GitHubAppInstallation, so an unreadable repository_selection refuses instead of widening to SelectionAll (the arm that would over-report the API budget).

gunbc.github_app_acquisition declares the census App and converges it: observe → decide (std.upsert_decision) → actuate → independent readback. gunbc.instruments.github_app_acquire is the argv-free route — four entry points.

Identity: why a second run adopts

The name is the identity and it is a constant. GitHub App names are globally unique, so a second registration under it is refused upstream, and nothing derives the name from a clock or nonce — a name carrying one would make every re-run succeed and accumulate one App per run, each pem lost on the next.

acquisition record	public read	verdict	decision
acquired	agrees with manifest	Converged	Noop — this is the adoption
acquired	absent	Conflict	Refuse — the duplicate-mint guard
acquired	drifted	Drifted	Refuse (the manifest flow creates Apps, it cannot edit one)
never acquired	an App answers	Conflict	Refuse
never acquired	not addressable, code in hand	Absent	Apply
never acquired	no code	Absent	Refuse, naming the human step

The slug is not guessed from the name: GitHub publishes no rule for that transformation, and a 404 against a guessed slug is indistinguishable from a real absence — the confusion that authorizes a duplicate mint.

The record is read, not transcribed. The conversion response carries the id and slug, so asking a human to type them into a data row is asking them to be the wire. The actuation writes an identity document beside the pem and the next run parses it; census_app_declared_adoption survives only for an App created before this converge existed. Two sources naming different Apps is a Conflict, never a precedence rule, and a half-written handoff refuses rather than reading as never-acquired.

Credential custody

The exchange returns the pem once and no endpoint reissues it, so the credentials are written with Filesystem.WriteOwnerOnly at 0600 before the readback runs — any later refusal, a disagreeing readback included, would otherwise destroy the only copy. A create-only preflight refuses a stale handoff while the code is still unspent; the interpolated name is checked so a separator cannot write the key outside the git-ignored directory; a failed write says the App is unrecoverable in those words, because the key cannot be printed to rescue it. The declared SecretRef sites are the destination and the local files are a handoff, with a frontier row that retires when the local hop is gone.

A second exchange of the same code gets 404 — ExchangeCodeNotLive, distinct from "the App is missing". A mutation whose outcome could not be read is ExchangeOutcomeUnknown, carrying the instruction to read the account's Apps before retrying.

The human steps, split one per act

Three identities, each keyed on the App, each an enrolled frontier row:

• submit — irreducibly human: GitHub requires owner consent and exposes no API. Trigger: browser automation driving the form under an owner session.
• capture — a declared choice, not a limit: the operator copies the code from the address bar only because redirect_url points at a host this fleet does not serve; a redirect catcher takes it today with no browser automation. A witness reds if that wording is softened back into a limitation.
• supply — an adopted App's pem, recorded as permanent: browser automation does not touch it, because there is nothing to click.

Where it stops

Nothing in this corpus can sign RS256, so no App JWT is minted here. The exchange needs none, which is why that half runs in-process. GET /app/installations reads its JWT from GITHUB_APP_JWT at the transport; its route exists and refuses twice without fabricating a budget (the transport refuses before sending with no JWT; GitHub 401s with a bogus one), with a frontier row for the green it cannot yet produce.

Evidence

50 witnesses pass. Four entry points execute; three run live against GitHub:

• public_app_record_wire_receipt → exit 0: a real GET /apps/dependabot 200 decoding into the modelled record, and a real 404 reaching AppRecordAbsent.
• custody_write_receipt → exit 0: real bytes through WriteOwnerOnly, read back, removed.
• census_app_installations_receipt → both refusals, neither fabricating a budget.
• With a handoff planted and no source edit, the observe entry read the record, performed a live GET /apps/gunbc-global-census, took the 404 and answered Conflict/Refuse.

Compile check clean on every file, proven non-blind by a planted in-body annotation. Stage0 mirror regenerated for uri_from_wire: 33 lines added, 0 deleted, first_generation_equal=true.

Also files a_summary_line_names_scope_in_verdict_position — a failure-mode row for something found while reading the CI failure, filed rather than fixed because repairing the floor's reporting from here is scope creep.

Review history

Two REQUEST_CHANGES, both finding real defects: a hand-rolled JSON emit forking extdeps.languages.json.emit (review 67410), and an acquire path that created a real App and dropped its private key (review 67436). Both are fixed at the root.

Not merging this myself

Asking the operator for the merge, per the working agreement.

🤖 Generated with Claude Code

[gunbai-bot]

Addressed in 0fcd4bec — review 67410's finding was correct and is fixed at the root, and it turned out to be the same root as the CI red.

The fork, and why the refusal went with it. You were right on both halves, including the part I had reasoned my way into backwards. I hand-rolled five string helpers and refused quote/backslash, on the reasoning that writing an escaper here would fork the JSON authority. The reasoning was right; the conclusion was wrong in both directions — the fork was the five helpers (extdeps.languages.json.emit already declares those exact names, cited to RFC 8259), and refusing a legal character the real emitter handles correctly is a §4d over-prohibition standing in for the escaper I declined to consume. Both the manifest and the installation-token body now build a JsonValue and call serialize_json; ManifestFieldUnrenderable and manifest_text_is_renderable are deleted. Thanks also for catching that my comment pointed at std.serialization — variant wire-contract modelling, not string emit.

The two witnesses that asserted the refusal are replaced by two that exercise the escaper rather than assert its absence: an injected "public":false in the name and in redirect_url must survive as data while the real member stays true. They go red if the serializer is swapped for concatenation. The string-contains assertions are updated to emit's canonical ": " / ", " spacing, exactly as you noted.

The CI red had the same root, one layer down. gunbc.roadmap_spawner calls json_bool at line 425 and does not import it — its block imports the other ten json_* names it uses and not that one. It was a bare cross-module reference resolving only because exactly one candidate existed; my local json_bool made it two, the reference attributed to gunbc.roadmap_spawner.json_bool, and the effect-summary join refused against a declaration that does not exist. Deleting my fork removes the trigger. I also added json_bool to that import list — one line in a module this PR does not otherwise touch, because the undeclared import is the earliest unjustified boundary (§6b), and a bare reference that resolves only while nobody else has minted the name is a trap armed for the next person rather than a working import.

Three more collisions, found by census rather than by CI. PushEvent, PullRequestEvent and WorkflowRunEvent collided with extdeps.github.actions_token GitHubWorkflowEvent and extdeps.github.workflow_run_event. The family is now spelled Webhook*, and the overlap with GitHubWorkflowEvent is a declared divergence with its reason beside it plus a frontier row naming the consolidation — the §3b middle value, not a silent second cut of one upstream catalogue.

42 witnesses pass, heal_repair_declaration exits 0 locally, all four files 0 blocking errors under the compile check (proven non-blind by a planted in-body annotation).

— sent from neat-pike-677

[gunbai-bot]

Addressed in 94b4a46c. Review 67436's finding was correct and was the most important defect in this PR, and an operator ruling on the human step landed alongside it.

The acquire path was dropping the private key

Confirmed exactly as described: ExchangeIssued went to a diagnostic instructing the operator to store credentials that were never written anywhere and cannot appear in a diagnostic, plan.custody was never consumed, and this module's prose claimed gunbc.secret_provision wrote them while nothing in the closure imported it. That path created a real App and lost it — unrecoverable rather than retryable, since GitHub returns the key once.

The credentials are now written with Filesystem.WriteOwnerOnly at 0600 before the readback runs. That ordering matters for a second reason the finding implies: the old code lost the key on any later refusal, a disagreeing readback included — and the readback is the step most likely to fail transiently. Around it:

• a create-only preflight, because WriteOwnerOnly refuses rather than clobbering; discovering a stale file after the exchange would burn a one-shot code and then fail the write, so the check runs while the code is still live;
• a path-safety wall on the interpolated name, so a separator cannot put the key outside the git-ignored directory;
• custody_write_receipt, an executing receipt that round-trips real bytes through the same function the acquire path calls and removes them — the pairing obligation for a write that runs once in the life of the App and cannot be rehearsed.

The declared SecretRef sites remain the destination; the local files are a handoff, with a frontier row that retires when the local hop is gone, not when a second hop is added beside it.

The human steps, split one per act (operator ruling)

One FleetOnce identity bundled four things, which made a step a redirect catcher could take today look as irreducible as the one GitHub genuinely requires a human for. Now three identities, each keyed on the App rather than the fleet, each an enrolled frontier row rather than a bare DissolutionCondition nothing counts: submit (irreducibly human; trigger named), capture (a declared choice, and its instruction says so — a witness reds if that is softened back into a limitation), supply (an adopted App's pem, recorded as permanent: browser automation does not touch it because there is nothing to click).

The fourth step is gone, not remodelled

The conversion response carries the id and slug, so asking a human to type them into a data row was asking them to be the wire. The actuation writes an identity document beside the pem and the next run parses it. census_app_declared_adoption survives only for an App created before this converge existed; two sources naming different Apps is a Conflict, never a precedence rule; and a half-written handoff refuses rather than reading as never-acquired, which would authorize a registration duplicating the App that file is about.

Verified by execution: with a handoff planted and no source edit, the observe entry read the record, performed a live GET /apps/gunbc-global-census, took the 404 and answered Conflict/Refuse.

A defect found mid-fix: the write keyed paths on the returned slug while the read keyed on the declared name — they would have found each other only if GitHub's name-to-slug transform were the identity, which this module refuses to assume everywhere else. Both key on the name now; the slug lives inside the document as data rather than as a path.

Also in this push

The stage0 mirror for uri_from_wire (extdeps_uri.rs), which was the one real CI failure. Checked for reverts before copying the candidate: 33 lines added, 0 deleted. first_generation_equal=true, cargo fmt --all --check clean.

A failure-mode row, a_summary_line_names_scope_in_verdict_position, for something found while reading that failure: the generated-artifact phase prints FAIL populations=registry-projections,stage0-mirrors while registry-projections' own line reports drifted=0. The summary enumerates the phase's scope in verdict position, so it cannot be read correctly without the lines above it. The row states the ceiling constructively (derive the summary from the outcome set) and explicitly refuses the documentary remedy as the answer. Filing rather than fixing, since widening into the floor's reporting from an App-acquisition change is scope creep.

50 witnesses pass.

— sent from neat-pike-677

[gunbai-bot]

Addressed in ccd6f724. Both findings in review 67504 were correct.

The trigger could only be discharged by editing the code it describes

Confirmed exactly as stated: census_app_installations_receipt returned exit_failure on the fully successful decode path, so the frontier row's "dissolves when this entry point returns ExitSuccess against a live GET" named a state the function had no arm for.

The underlying reason is worth naming, because it is the same dishonesty this PR objects to elsewhere: I used the refusal reason as a print channel, since it is what surfaces text. That reported a successful budget read as a failed run, and the unsatisfiable trigger was the second-order consequence. The listing now goes to a report file and the success path returns ExitSuccess, so acquiring the App and exporting a valid GITHUB_APP_JWT is sufficient to discharge the row and nothing else is required.

I also wrote that reachability into the row explicitly — including that it was briefly false — rather than just fixing the code. A trigger whose reachability is assumed is how this class recurs, and the row is the thing a future reader consults.

The refusal arms are unchanged and still measured: still produces .

One directory, not four spellings

Also correct, and I'd sharpen why it isn't cosmetic beyond what you wrote: the three paths carry a manifest code, which is a bearer credential that creates an App under whatever manifest its flow declared. The directory is load-bearing because it is git-ignored, so an edit moving the custody authority would have left three credential paths outside the ignore rule with nothing failing. All four now derive from census_app_custody_handoff_directory, the new installations report included — a listing is not a credential, but it names every account this App can read and the exact token requests that would mint against them, so it does not belong in a tracked path either.

Verified the derived paths are byte-identical to the literals they replace, so no existing handoff file is stranded — checked by execution, not by reading the concatenation.

Two new witnesses: one reds if any handoff path stops deriving from the declared directory, one pins the report's count and per-installation token request. 52 pass.

and are green on the previous head; the floor lane was still running when this went up.

— sent from neat-pike-677

[gunbai-bot]

Correction to my previous comment: three code spans in it were eaten by shell expansion before it posted (backticks inside a double-quoted --body). The three mangled sentences, intact:

• The refusal arms are unchanged and still measured: GITHUB_APP_JWT=bogus still produces refused with status 401.
• required-witnesses-build and heal-generated-artifacts are green on the previous head; the floor lane was still running when that comment went up.

Nothing else in it changed meaning — but a comment whose evidence lines were silently emptied is exactly the kind of thing worth correcting rather than leaving for a reader to squint at.

— sent from neat-pike-677

[gunbai-bot]

Addressed in d4af95ae. Both findings in review 67524 were correct.

The bare reference I had just finished fixing elsewhere

Confirmed: gunbc.github_app_acquisition called uri_wire while importing only { Uri, uri_https }, resolving purely because exactly one candidate exists in the tree. You're right that this is the same trap commit 3 of this PR diagnosed and repaired for json_bool — reintroduced one file over, while I was writing the memory about it. Imported now.

The one-line fix isn't the interesting part. I censused every file this PR touches for identifiers called but neither declared locally nor imported, rather than fixing only the instance you found. uri_wire was the only real hit; every other flag turned out to be prose inside a string literal. That check costs seconds and belonged before the first push — I'd been treating this class as something to remember rather than something to test for.

A fabricated inhabitant of a non-emptiness type

Also correct, and your framing of why it matters is the right one: uri_from_wire is the general decode side of the URI authority, so every consumer downstream inherits whatever it mints. And the sibling comparison lands — conversion_issuance checks c.slug == "" and installation_from_record checks record.app_slug == "" before their casts, in this same PR, so this was the odd one out rather than a house style.

It refuses now, at the one constructor. The witness reds on "https://" and on a relative reference, and additionally pins that the round trip still preserves scheme text inside a locator (https://x.example/redirect?to=https://y) — that is the property the rejoin exists for, and the thing an emptiness guard could plausibly have broken while looking correct.

Mirror

Regenerated for the uri.dag change: 14 deletions this time against zero last time, which is the shape that should stop you. Read rather than assumed — all fourteen are inside uri_from_wire (the inline join hoisted into a let, and the if line that gained the conjunct), nothing else in the file moved. first_generation_equal=true, cargo fmt --all --check clean, 53 witnesses pass.

— sent from neat-pike-677

[gunbai-bot]

Addressed in 73810c6a. Both findings in review 67544 were correct.

Seven copies, not three

Verified, and the count is worse than the finding states: besides the three in extdeps.github.app and the two fleet copies you name, gunbc.product.fan_tach_health:188 and v2.compiler.00_compile:511 carry the same shape. Seven.

std.list first_duplicate_by_key is the one authority now, and the three sites in this file consume it. It takes a key projection rather than an equality function, and that is precisely what lets it be linear — an arbitrary fn(T,T) -> Bool admits no index, so every realization of it is quadratic; a key the caller can name is one a Map can hold. Every one of those sites already had such a key (a wire name, a header, a declaration ref) and was comparing through it, so the projection isn't a new fact being invented to make the fix work. webhook_event_eq was a bare alias of == and is gone with it.

On not forking std.keyed_roster — I checked it before minting, since "there is already an authority for this" is the obvious objection to a new helper. keyed_roster_build answers a different question: it constructs a validated carrier whose success arm proves one value per key, and it declares itself O(n²) in its own note. So consuming it would have satisfied the duplication half of your finding and left the cost half exactly where it was. The relationship is stated at the declaration rather than left for a reader to adjudicate, and the honest end state — keyed_roster's own detection consuming this kernel — is named there as a rewire of that module, not taken here.

The settings URLs

Also correct. Both are Uri values now, with app_manifest_registration_base_url projecting through uri_wire. Your framing is the right one: it's in a file whose every citation in this same diff is Uri { scheme: Https, locator: … }, so the text spelling was the odd one out — and it loses the distinction uri_scheme_is_http exists to make.

Witnesses

55 pass. The kernel's own claim pins which element it returns — the second occurrence, the point at which repetition becomes observable in a single pass — because that is the case a nested fold and a map scan could silently disagree on while both looking right. It also pins that two elements with distinct keys are not duplicates, which is the direction a key projection could plausibly get wrong.

Neither std.list nor extdeps.github.app has a stage0 mirror, so no regen is owed for this commit — checked rather than assumed.

— sent from neat-pike-677

[gunbai-bot]

Addressed in 6fbea18f. Review 67573 is correct, and this was an unrecoverable-loss bug rather than a sequencing preference — the best finding on this PR.

The defect

custody_preflight exists to catch a stale handoff while the code is still live, because WriteOwnerOnly is create-only. It was called from persist_then_read_back, which runs after exchange_census_app_code. So with a stale .gunbc/github-app-<name>.pem from a prior run, the flow would create a real App, refuse the write, and lose a private key no endpoint reissues — under a name now permanently taken — for a condition one Filesystem.Read before the POST would have caught.

How a comment kept it there

This is the part I want to name, because it's the mechanism rather than the symptom. The justification read "THE ISSUED SLUG IS ONLY KNOWN AFTER THE EXCHANGE, so its preflight runs here rather than before the POST." That was true when written — the handoff was addressed by the returned slug. This PR later moved the addressing to the declared name, as its own mid-fix correction, and I did not move the comment with it. The annotation then stood as a second, false authority for the sequencing and actively justified the loss the preflight exists to prevent. Exactly §4c.

So the failure wasn't writing a wrong comment; it was changing the construction and leaving a right-at-the-time comment in place, where it went on being read as a reason.

The fix

custody_preflight is hoisted into census_app_acquire_with_code ahead of the exchange. Its refusals now say NOTHING WAS EXCHANGED and the code is still live, and name the recoverable remedy — move the files aside, re-run within the hour — instead of "delete the App and start over."

persist_then_read_back keeps a write-failure arm on purpose: a path clear a moment ago can still fail on a full disk, a permission change, or a racing process, and those are genuinely only discoverable at the write. Everything reaching it now holds a created App and an in-memory key, so every arm there is an unrecoverable-loss arm and says so.

The note also now states why the check can run that early — the handoff is addressed by the declared name — because the ordering depends on that fact, and if the addressing ever moves back to the returned slug the loss arm comes back.

Evidence

Executed: with a stale pem planted and a code file present, the acquire entry refuses and zero calls to /app-manifests are made. The code stays live.

Made re-derivable as custody_preflight_receipt, which plants a file and asserts the preflight discriminates — clear reads clear, occupied reads occupied, on real disk. That check exists because correct ordering alone cannot rule out a preflight that answers CustodyPathsClear unconditionally: it would sit in exactly the right place and prevent nothing.

55 witnesses pass.

— sent from neat-pike-677

[gunbai-bot]

Addressed in 3135435e. Review 67588 is correct, and it lands on the one call in this flow whose failure destroys the subject.

write_secret_file collapsed WriteOwnerOnly's typed success: Bool into a String — "" for success, wrote.error otherwise — and persist_issued_credentials re-derived success as error != "". A failed write reporting an empty error string would have read as a successful handoff: CredentialsHandedOff returned, readback_exit printing "the credentials are on disk at …", and the pem gone. A heuristic standing exactly where an observation existed, and you're right that extdeps.filesystem.filesystem_io refuses the same move in its own annotation one screen earlier.

SecretFileWrite (SecretFileWritten | SecretFileWriteRefused { path, cause }) is that fact carried rather than re-derived, minted from wrote.success at the one site that observes it. I also took the shape that made the sentinel tempting: then_write_secret / then_write_optional_secret sequence the three writes by short-circuiting on the refusal arm, so the nested if/else ladder is gone and a fourth write cannot forget to check.

Both arms executed, not just the happy one:

• success — custody_write_receipt exits 0; bytes round-trip through the real WriteOwnerOnly and are removed.
• refusal — planting a file at the probe's pem path makes the real create-only write fail, and it now reports the custody write refused at <path>: File exists (os error 17). Under the old shape, noticing that at all depended on the error string being non-empty.

The repair was audited rather than assumed — the diff's deletions are exactly the sentinel code and nothing else. 55 witnesses pass.

On CI evidence, stated plainly

I have been pushing faster than CI can finish, and each push cancels the previous run: d4af95ae and ccd6f724 were both cancelled, and the last completed success on this branch was 94b4a46c, several commits back. So the local evidence above (witnesses, compile checks, executed receipts, first_generation_equal=true) is real, but CI has not yet confirmed any of the last several rounds.

I pushed this one anyway rather than waiting, on the judgement that CI evidence for a head carrying a known credential-loss defect is worth less than evidence for the corrected head. From here I am holding — no further pushes until this run reaches a terminal conclusion, and if another finding arrives I will fix it locally and batch rather than restart the clock again.

— sent from neat-pike-677

[briansrls]

REQUEST CHANGES — source-reviewed exact head 3135435e9c0d0fb39450f6c3d0426e237ff8e559.

This is substantial and several custody/readback decisions are strong, but the route does not yet acquire the usable API-budget subject the PR claims.

1. The manifest-registration entry does not implement GitHub's manifest handshake. app_manifest_registration_url builds a URL carrying only state, and the intervention says to open it and paste JSON into GitHub's form. GitHub's manifest flow requires a POST to the settings endpoint with the JSON-encoded document in a form field named manifest; the GitHub page reached by this GET is not the missing POST form. Emit an executable local/served form (or automate the browser) that submits manifest and state to the declared target. Until then the route cannot create the declared preconfigured App.

2. The readback drops two parts of identity it already carries. The acquisition record has app_id and the declared identity has the owner/registration target, but reconcile_acquisition_record compares only slugs and census_app_agreement compares only slug, permissions and events. A deleted/recreated App reusing the slug—or a record under the wrong owner—can be reported converged while the stored PEM belongs to a different App. Bind agreement to App ID, slug and declared owner/target; two records with the same slug and different IDs are a conflict.

3. App creation is not installation, and the budget route can green on zero installations. No route or human intervention installs the App. census_app_installations_receipt returns ExitSuccess after a successful empty listing, and its frontier dissolves on that success. Thus it can retire while the App has no installation token, no installation-scoped budget and no usable census credential. Model the intended installation/selection, require the expected nonempty installation set, and make budget availability depend on a successfully minted installation token—not merely a 200 listing.

4. The installation listing is silently partial. GitHub paginates this endpoint (default 30, max 100), while ListInstallations has no page input or page walk and the report renders installations=N as a complete count. Carry pagination/completeness and refuse a partial budget inventory.

5. The “permanent” adopted-key human step contradicts the modeled upstream. GitHub's settings page can generate a new private key for an existing App; the PR's own intervention names that remedy. Browser automation can therefore drive new-key generation. The original bytes are unrecoverable, but supplying a usable key is not permanently irreducible. Rewrite the standing and dissolution trigger accordingly.

6. Conversion authentication is presently an unverified contract mismatch. ConvertManifestCode declares no auth because the code is said to authenticate the exchange, while GitHub's current REST example includes an Authorization bearer header. Either model the supported credential precisely or provide a live conversion receipt before claiming the route runs end to end.

The custody preflight, create-only 0600 write, immediate persistence before readback, and unknown-mutation refusal are worth retaining. The root repair is to finish the actual POST→redirect→exchange→install→token chain, with one identity carried across every stage.