Repository navigation
Conversation
…oute that runs it
The operator creates GitHub Apps by hand, repeatedly, because nothing declared
their shape. This declares it once and makes the App re-creatable from the
declaration, with one human click and no hand-entered permission set.
WHAT LANDS
extdeps.github.app grows the manifest half of its existing subject rather than a
second module naming GitHubAppRegistration: the manifest with its real upstream
fields, the JSON document the registration form accepts, the registration URL for
a user and for an organization, POST /app-manifests/{code}/conversions modeled
against the spec, GET /apps/{app_slug}, GET /app/installations, and the
installation-token request rendered to its wire. Permissions go through the
permission-axis system that was already there; the access wire fold and the
JSON-object permission decode are the two pieces it was missing.
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, three entry points
because the flow has a human in the middle of it.
IDENTITY, AND WHY RE-RUNNING ADOPTS
The name is the identity and it is a constant; GitHub App names are unique across
GitHub, so a second registration under it is refused upstream. Nothing here derives
the name from a clock or a nonce, because a name carrying one would make every
re-run SUCCEED and accumulate one App per run. A recorded App plus an agreeing
public read is Noop, and Noop is the adoption. A recorded App plus an ABSENT public
read is a Conflict, never an Absent that authorizes a registration - that arm is the
duplicate-mint class and it has its own witness.
CREDENTIAL CUSTODY
The exchange returns the pem once and no endpoint returns it again. The custody
sites are declared before the actuation that produces them, and a mutation whose
outcome could not be read is ExchangeOutcomeUnknown carrying the instruction to
read the account's Apps before retrying - because the App may exist and its only
private key was in the reply nobody read.
WHERE IT STOPS, HONESTLY
Nothing in this corpus can sign RS256, so no App JWT is minted here. The exchange
needs none - the code authenticates it - which is why this half runs in-process.
GET /app/installations reads its JWT from GITHUB_APP_JWT at the transport, minted
externally; its route exists, refuses twice without fabricating a budget, and
carries a frontier row for the green it cannot yet produce.
EVIDENCE
42 witnesses pass. Two entry points were run live against GitHub:
public_app_record_wire_receipt (a real 200 decoding into GitHubAppPublicRecord and
a real 404 reaching AppRecordAbsent) exits 0, and census_app_installations_receipt
reaches both its refusals - AuthDeclaredButUnwired with no JWT, 401 with a bogus
one. census_app_registration_instruction_receipt renders the real manifest document.
All six files are 0 blocking errors under the compile check, proven non-blind by a
planted in-body annotation.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…lisions that exposed a bare import Addresses review 67410 (cursor/auto, REQUEST_CHANGES), and fixes the CI red, which had the same root. THE FORK, AND WHY THE REFUSAL WENT WITH IT extdeps.github.app hand-rolled json_string / json_bool / json_member / json_object / json_array and then REFUSED any value carrying a quote or a backslash, reasoning that writing an escaper would fork the JSON authority. The reasoning was right and the conclusion was wrong in both directions. extdeps.languages.json.emit is cited to RFC 8259, declares those exact names, and escapes; the fork was the five helpers, and refusing a legal character the real emitter handles is DESIGN 4d over-prohibition standing in for the escaper I declined to consume. The manifest and the installation-token body now build a JsonValue and call serialize_json. ManifestFieldUnrenderable and manifest_text_is_renderable are deleted. Two witnesses asserting the refusal are replaced by two that exercise the escaper: an injected `"public":false` in a name and in redirect_url must survive as DATA, with the real member still true. They go red if the serializer is swapped for concatenation. 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; json_bool is added to that import list because the undeclared import is the earliest unjustified boundary (DESIGN 6b) and a bare reference that resolves only while nobody else has minted the name is a trap armed for the next person. 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 -- not a silent second cut of one upstream catalogue. 42 witnesses pass. heal_repair_declaration exits 0. All four files 0 blocking errors under the compile check. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e acquisition record instead of transcribing it
Addresses review 67436 (cursor/auto, REQUEST_CHANGES) and an operator ruling on
how the human step must be modelled. Regenerates the stage0 mirror for
uri_from_wire.
THE ACQUIRE PATH WAS DROPPING THE PRIVATE KEY
ExchangeIssued went to a diagnostic that told the operator to store the pem,
webhook secret and client secret while the Secret values themselves 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. GitHub returns an App private key once
and no endpoint reissues it, so that path created a real App and lost it.
The credentials are now written with Filesystem.WriteOwnerOnly at 0600 BEFORE
the readback runs -- an ordering the old code got wrong in a second way, since a
failed readback destroyed the key too, and the readback is the step most likely
to fail transiently. A create-only preflight refuses a stale handoff while the
code is still unspent rather than after it is burned, the interpolated name is
checked so a separator cannot write the key outside the git-ignored directory,
and custody_write_receipt is an EXECUTING receipt that round-trips real bytes
through the real write and removes them.
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 rather than
when a second hop is added beside it.
THE HUMAN STEPS, SPLIT ONE PER ACT (operator ruling, 2026-09-18)
One FleetOnce identity bundled four things and 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 today; trigger is browser automation driving the
form under an owner session.
CAPTURE - a DECLARED CHOICE, not a limit, 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.
AND THE FOURTH STEP IS GONE, NOT REMODELLED
The conversion response carries the id and the 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 the
file is about.
Verified by execution, not assertion: 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, and the slug lives inside the document
as data rather than as a path.
50 witnesses pass. Mirror install checked for reverts before copying: 33 lines
added, 0 deleted. first_generation_equal=true, cargo fmt clean.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ve from one directory Addresses review 67504 (claude/opus[1m], REQUEST_CHANGES). Both findings were correct. A TRIGGER THAT COULD ONLY BE DISCHARGED BY EDITING THE CODE IT DESCRIBES census_app_installations_receipt returned exit_failure on the FULLY SUCCESSFUL decode path, purely because the refusal reason is the channel that prints. Two things were wrong with that. It reported a successful budget read as a failed run — the same reporting dishonesty this PR objects to elsewhere. And it made this entry point's own frontier row unsatisfiable: the row says it dissolves when the function returns ExitSuccess against a live GET, and no ExitSuccess arm existed, so acquiring the App and exporting a valid JWT could never discharge it. DESIGN 4b(3) rules a drop is retired by its trigger and by nothing else. The listing now goes to a report file and the success path returns ExitSuccess, so the trigger is reachable without touching the function. The row says that explicitly, and says it was briefly false, because a trigger whose reachability is assumed is how this class recurs. ONE DIRECTORY, NOT FOUR SPELLINGS census_app_state_path, census_app_code_path and census_app_observed_state_path hand-spelled ".gunbc/…" while this module already imports census_app_custody_handoff_directory as the authority for it. Not cosmetic by the file's own argument: the directory is load-bearing BECAUSE it is git-ignored, so an edit moving the custody authority would have silently left three bearer-credential paths outside the ignore rule. All four derive now, including the new installations report — 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. Verified the derived paths are byte-identical to the literals they replace, so no existing handoff file is stranded. 52 witnesses pass; the two new ones red if a path stops deriving or the report stops carrying its token requests. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… of minting an empty NonEmptyStr
Addresses review 67524 (claude/opus[1m], REQUEST_CHANGES). Both findings correct.
THE BARE REFERENCE I HAD JUST FINISHED FIXING ELSEWHERE
gunbc.github_app_acquisition called uri_wire while importing only { Uri,
uri_https }. It resolved because exactly one uri_wire exists in the tree — which
is the same undeclared-import trap this PR's third commit diagnosed and repaired
for json_bool in roadmap_spawner, reintroduced one file over while the memory
about it was being written. uri_wire is imported now.
The instance is a one-line fix; the useful part is that I censused every file
this PR touches for identifiers called but neither declared locally nor
imported, rather than fixing the one the reviewer found. uri_wire was the only
real hit — every other flag was prose inside a string literal. That check is
cheap and belonged before the first push.
A FABRICATED INHABITANT OF A TYPE WHOSE WHOLE CONTENT IS NON-EMPTINESS
uri_from_wire cast the rejoined remainder `as NonEmptyStr` unguarded, so
"https://" produced a Uri whose locator is "" carrying NonEmptyStr. Its siblings
in this same PR guard exactly this shape before casting — conversion_issuance
checks c.slug == "", installation_from_record checks record.app_slug == "" — so
this was the odd one out, and it is the general decode side of the URI
authority, so every consumer downstream inherits whatever it mints. It refuses
now, at the one constructor rather than in consumers.
The witness reds on the bare scheme and on a relative reference, and pins that
the round trip still preserves scheme text INSIDE a locator
(https://x/redirect?to=https://y), which is the property the rejoin exists for
and the thing an emptiness guard could plausibly have broken.
MIRROR: regenerated for the uri.dag change. 14 deletions this time against zero
last time, so they were 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, fmt
clean, 53 witnesses pass.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… the settings URLs are Uri values
Addresses review 67544 (claude/opus[1m], REQUEST_CHANGES). Both findings correct.
SEVEN COPIES OF ONE CONCEPT, THREE OF THEM IN ONE FILE
first_duplicated_observed_permission, first_duplicated_permission and
first_duplicated_event were three copies of a nested fold inside
extdeps.github.app -- an outer scan whose every step ran an inner occurrence
count -- with webhook_event_eq a bare alias of == beside them. The corpus holds
four more of the same shape (gunbc.product.fan_tach_health,
gunbc.fleet.fleet_fan_tach_expectation, gunbc.fleet.fleet_fan_wiring,
v2.compiler.00_compile). DESIGN 2's test is that net concepts must not grow by
re-invention, and prevalence is evidence of the debt rather than precedent for a
third copy.
std.list first_duplicate_by_key is the one authority. It takes a KEY PROJECTION
rather than an equality function, and that is what makes it LINEAR: an arbitrary
fn(T,T)->Bool admits no index so every realization of it is quadratic, while a
key a caller can name is one a Map can hold. Every site already had such a key --
a wire name -- and was comparing through it, so the projection is not a new fact.
DESIGN 6 rules the cost half unconditionally: a quadratic fold is always fixed,
regardless of the realized n.
Its relation to std.keyed_roster is stated where it is declared rather than left
for a reader to adjudicate. keyed_roster_build answers a different question --
it constructs a validated carrier proving one value per key -- and declares
itself quadratic in its own note. This returns an element and builds nothing. The
honest end state is that keyed_roster's detection consumes this kernel; that is a
rewire of that module, not of this one, so it is named and not taken.
THE SETTINGS URLS ARE Uri VALUES, NOT TEXT STARTING WITH https
github_settings_apps_new_path and github_organizations_settings_prefix spelled
the scheme as characters inside a String and joined the rest, in a file whose
every citation is Uri { scheme: Https, locator: ... } and which imports the URI
authority. Two spellings of one scheme drift independently, and the text one
loses the distinction uri_scheme_is_http exists to make. Both are Uri now, with
app_manifest_registration_base_url projecting through uri_wire.
55 witnesses pass. The kernel's own claim pins WHICH element it returns -- the
second occurrence, the point at which repetition becomes observable in one pass
-- because that is the case a nested fold and a map scan could silently disagree
on, and it pins that distinct keys over equal elements are not duplicates.
Neither std.list nor extdeps.github.app has a stage0 mirror, so no regen is owed
for this commit.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ways said it belonged Addresses review 67573 (claude/opus[1m], REQUEST_CHANGES). Correct, and it was an unrecoverable-loss bug rather than a sequencing preference. WHAT WAS WRONG custody_preflight exists to catch a stale handoff file WHILE THE CODE IS STILL LIVE, because WriteOwnerOnly is create-only and a занятый path means the write fails. It was called from persist_then_read_back, which runs AFTER exchange_census_app_code. So with a stale .gunbc/github-app-<name>.pem left by a prior run, the flow created a real App, refused the write, and lost a private key that 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 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 the handoff was addressed by the returned slug. This PR moved the addressing to the declared NAME -- known before the POST -- as its own mid-fix correction, and did not move the comment. A stale annotation then stood as a second, false authority for the sequencing and justified exactly the loss the preflight exists to prevent. DESIGN 4c: an annotation may not assert what the construction does not do. THE FIX custody_preflight is hoisted into census_app_acquire_with_code ahead of exchange_census_app_code. Its refusal arms now say NOTHING WAS EXCHANGED and the code is still live, and name the recoverable remedy -- move the files aside and re-run within the hour -- instead of "delete the App and start over". persist_then_read_back keeps a write-failure arm, because a path clear a moment ago can still fail on a full disk, a permission change or a racing process, and those are only discoverable at the write. The note now also 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 returns. EVIDENCE Executed: with a stale pem planted and a code file present, the acquire entry refuses and ZERO calls to /app-manifests are made, so 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 -- because a preflight that answered clear unconditionally would sit in the right place and prevent nothing, and correct ordering alone cannot rule that out. 55 witnesses pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ly sentinel
Addresses review 67588 (claude/opus[1m], REQUEST_CHANGES). Correct, and on the
one call in this flow whose failure destroys the subject.
write_secret_file collapsed Filesystem.WriteOwnerOnly's typed success: Bool into
a String -- "" for success, wrote.error otherwise -- and persist_issued_credentials
then re-derived success as error != "". A failed write reporting an EMPTY error
string was therefore read as a successful handoff: CredentialsHandedOff returned,
readback_exit printing "the credentials are on disk at ...", and the pem that no
endpoint reissues gone. A heuristic standing exactly where an observation
existed, which extdeps.filesystem.filesystem_io refuses in its own annotation one
screen earlier, and which DESIGN 5 rules against directly -- prefer the single
authority the realization derives from over a check that flags the bad state
after the fact.
SecretFileWrite is that authority carried rather than re-derived:
SecretFileWritten | SecretFileWriteRefused { path, cause }, minted from
wrote.success at the one site that observes it. then_write_secret and
then_write_optional_secret sequence the three writes by short-circuiting on the
refusal arm, so the nested if/else that made the sentinel tempting is gone with
it, and an added write cannot forget to check.
EVIDENCE, BOTH ARMS EXECUTED
- 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)" -- a refusal carrying the real cause where the old shape
would have depended on that error string being non-empty to notice at all.
Repair audited rather than assumed: the diff's deletions are exactly the sentinel
code, nothing else. 55 witnesses pass.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
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.
Auto-opened by session-dashboard for session
zesty-crane-846.Pushing to
pr11552advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan