Repository navigation
Admit the census installation at a real identity grain (#11931 blocker) - #11980
Closed
gunbai-bot[bot] wants to merge 7 commits into
Closed
gunbai-bot[bot] wants to merge 7 commits into
gunbai-bot[bot] wants to merge 7 commits into
Conversation
…facts kept apart gunbc.github_app_acquisition told the operator to "paste the manifest below into the form's manifest field, and submit". There is no such field: a GET of GitHub's registration URL renders the ordinary App-creation form, which ignores manifests, and the manifest protocol is a POST carrying a `manifest` form parameter. The operator followed the step and reported exactly that -- while a witness asserting the instruction carried the URL and the manifest stayed green over it, because both were true and neither was the property that mattered. (a) The instruction is now an artifact. extdeps.github.app gains the upstream facts it was missing -- app_manifest_form_parameter_name, app_manifest_submission_document, app_install_url with its citation -- and the document is built as a std.markup Fragment serialized through extdeps.languages.html, so the manifest JSON reaches value="..." through escape_attribute. That escape is load-bearing: an unescaped quote closes the attribute at the first JSON key and the browser POSTs a TRUNCATED manifest, registering an App with permissions nobody declared. census_app_registration_instruction returns the intervention, the document and its path together, so an instruction naming an artifact nobody wrote is unconstructible; the entry point writes it and refuses to print the instruction if the write failed. (b) Four facts, separated. census_app_acquisition_standing refuses at the earliest fact that is not established and names it, and no later fact mints an earlier one. Registration is established by the independent public read agreeing, never by the record. Installation is a second consent at a second URL and refuses before registration rather than assembling one from the declared name; an installation naming another App's id does not install this one; an unreadable list is not an absence. Callback capture moved out of the instrument into the module, because four facts are not distinct if one is a local type inside the route that consumes it. CustodyStanding has one established arm and no constructor for "the key is at its destination" -- the second hop belongs as a row in the custody roster the ntfy-publisher-token-onto-gcp-custody node consolidates, and that is stated as pending rather than forked here. (c) Controls. The discriminating red is w_an_installation_and_a_key_do_not_establish _a_registration; a deliberate mutation that mints a receipt from an installation and a key with no registration reds it while the positive control and the neighbouring refusal claim stay green. Accepted positive control: w_all_three_facts_established_is_a_receipt_naming_all_three, which is the roadmap node's handback sentence. 64/64 claims green on the real tree. The registration effect is rostered in gunbc.auth.privileged_effect_census and the selection executes to HumanOnlyStep; unrostered_unreasoned_divergences and undecidable_sites are both empty. No receipt in this corpus establishes registration, installation or custody for the census App today, and census_app_acquisition_receipt says so in those words. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…e the frequency divergence with its measurement FINDING 2 (the sharper one). CensusAppAcquisitionReceipt.key_custody was typed CustodyStanding, so CustodyNotEstablished was representable inside a value whose whole meaning is "acquired", and acquisition_standing_line carried a defensive arm whose own text admitted it was unreachable. That arm was not a refusal -- it returned an ordinary line the caller writes to the receipt file on ExitSuccess, so the one state it existed to catch would have been REPORTED AS THE RECEIPT. That is validation standing where construction was available, at the same seam the diff was congratulating itself for closing one field earlier. The established fact is now its own record, CustodyAtHandoff, with no "not established" inhabitant; the receipt carries it, and the arm is deleted rather than made louder. FINDING 1. The row read FleetOnce while the step it embeds declares EveryProvision, with no reason stated -- DESIGN 3b's only red. I first made the row DERIVE its frequency from the step, which removes the fork by construction, and measured what that does: select_authorization_pattern returns NoAdmissiblePattern and the site lands in undecidable_sites, because EVERY candidate including HumanOnlyStep violates constraint_unattended_required. That verdict is the selection faithfully reporting a premise this row does not hold -- an effect GitHub requires an owner to perform is not one that must run unattended -- so adopting the step's value would assert something false about the effect in order to make two fields agree. The row keeps FleetOnce and the reason is now stated on it, with that measurement, moving it from the red value to the admitted middle one. What the divergence actually locates is one type carrying two questions: HumanInterventionFrequency is read as burden multiplicity by the intervention roster and as an attendance premise by unattended_required. Splitting it is a change to that authority and every consumer of it, which is not this row's to make; the row names it rather than papering over it. Kept from the first attempt: census_app_registration_submit_step, so the census embeds the step through one constructor instead of rebuilding it. Evidence on this tree: 64/64 claims green (rc=0); undecidable_sites == [] and unrostered_unreasoned_divergences == []. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The GET /app/installations ladder was authored twice in the same file -- the same ListInstallations call, the same five classify_rest_outcome arms, the same three decode arms -- once in census_app_installations_receipt and once in live_installation_standing. Two sources for one semantic fact, not two readers of one, and they had ALREADY DRIFTED inside the commit that introduced the second: the identical 401 condition carried two different sentences. read_census_app_installations is now the only place that performs and classifies the read; it returns the CensusAppInstallationReading the decoder already produced. The two entry points differ only in how they render it -- installations_read_exit for the report, installation_standing_for for the receipt. One ListInstallations call site and one classify_rest_outcome site remain in the file. The transport arms fold into InstallationsUnreadable, because every one of them answers the same question the same way and the arm already carries the reason that distinguishes them for a human. What does NOT collapse is unreadable into EMPTY: "the JWT was stale" and "the App has no installation" prescribe opposite acts and stay two arms, which w_an_unreadable_installation_list_is_not_an_absent_installation holds. That duplication undercut this PR's own thesis -- one fact, one establishment -- which is why it was worth fixing rather than annotating. Evidence on this tree: 64/64 claims green (rc=0); the instrument closure resolves and typechecks. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…erved absence
next_acquisition_step reaches the supply step whenever KEY CUSTODY is the missing
fact, and its text opened "This App was created outside this converge" -- a
provenance claim the receipt has not established. An App this converge registered
whose pem was never stored, or was later cleaned out of .gunbc/, is in exactly the
same unrecoverable position. That is an inference presented as established, DESIGN
4d's first arm, and the precise class this PR exists to remove, so it was worth
catching inside it rather than shipping it.
The premise lived in four places and all four are fixed, not just the sentence the
review named:
- the instruction, which now states the observed fact (no key at the custody
path) and the upstream rule (GitHub returns the key once and reissues it
never), and says explicitly that it asserts nothing about how the App came to
exist;
- the frontier row's reason, which said the same thing to the dissolution census
and now states the step's real scope;
- the SUPPLY line in the human-steps annotation;
- the function's own NAME. adopted_app_key_supply_intervention carried the
premise in the one place no rewording would reach, so it is
app_key_supply_intervention. The HumanInterventionIdentity string is unchanged,
so no rostered identity moves.
The remedy is untouched: it was always right.
w_the_key_supply_step_asserts_no_provenance_only_the_observed_absence is enrolled
and goes red if a provenance premise returns.
Evidence on this tree: 65/65 claims green (rc=0).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ded addressing, and drop a dead import
FINDING 1. census_app_submission_artifact_path built a write target by calling
custody_handoff_path directly, bypassing custody_handoff_addressing and its
custody_name_is_path_safe guard -- the guard the same module applies to the other
four per-App paths, and that this PR's own live_custody_standing still routes
through for the SAME name. The result is consumed by a real Filesystem.Write, so a
name carrying a separator escaped the git-ignored handoff directory with no typed
refusal while the modeled refusal for exactly that state sat one function away. No
live failure today -- the declared name is a path-safe literal -- but the asymmetry
was the defect.
Fixed by construction rather than by adding a check at the bypass:
- registration_form joins CustodyHandoffPaths, so the path is PRODUCED only by
the constructor that checks the name. My earlier reasoning for keeping it out
("it is not a secret") was about the wrong property: the record is the
ADDRESSING of the per-App files, and membership is "is this a path built from
the App name", not "is this file secret".
- app_registration_submit_intervention now takes the CustodyHandoffAddressING
rather than a String path, so NO consumer can reach it with an unchecked name
-- the census row included. Both arms are reachable, since the carrier admits
any NonEmptyStr, so this is a total fold over a real coproduct and not a
defensive arm over a state the constructor forbids.
- census_app_registration_instruction refuses with RegistrationInstructionUnavailable
on an unsafe name instead of handing back a write target.
- census_app_submission_artifact_path is deleted rather than left beside the
addressing, which would have been two producers for one path.
FINDING 2. census_app_submission_artifact_path was imported into the instrument and
never called -- a dead import this diff added, DESIGN 3c's own tell. It goes with
the deleted function.
THE NEW RED DISCRIMINATES, MEASURED. With custody_name_is_path_safe mutated to
answer true unconditionally:
FAIL w_an_unsafe_app_name_refuses_the_submission_artifact_instead_of_writing_it
FAIL w_a_slug_that_escapes_the_handoff_directory_is_refused (pre-existing, same guard)
PASS w_the_registration_form_is_one_of_the_addressed_handoff_paths
The structural claim stays green because it does not depend on the guard
discriminating, which is the separation intended.
Evidence on this tree: 67/67 claims green (rc=0); undecidable_sites == [].
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…hey stay two arms through the prescription THE DEFECT WAS MY OWN RULE BROKEN ONE LAYER ALONG. read_census_app_installations carries the annotation "what must NOT collapse is unreadable into EMPTY ... 'the JWT was stale' and 'the App has no installation' prescribe opposite acts", and the reading obeyed it -- InstallationStanding kept both arms, and so did the printed reason. census_app_acquisition_standing then folded both into one AcquisitionFactMissing::InstallationMissing, and next_acquisition_step matched that arm, DISCARDED the reason, and returned the consent instruction. So a stale-JWT 401 told the operator to go grant an installation that may already exist -- an inference asserted as the established missing act, DESIGN 4d's first arm, which is the class reviews 69488 and 69482 already removed from this diff. FIXED BY CONSTRUCTION, NOT BY RE-READING THE REASON. AcquisitionFactMissing now carries InstallationConsentMissing and InstallationReadingUnavailable as separate arms, and next_acquisition_step matches on the arm. Recovering the distinction by re-parsing the reason string would put it back in a consumer after the type had thrown it away -- the same shape as the unguarded path builder deleted one commit earlier, a wall standing one call away from what it guards. The unreadable arm prescribes minting a fresh App JWT and says explicitly NOT to install on the strength of an unread fact; acquisition_standing_line distinguishes them too. AND THE CONTROL NOW EXECUTES OVER THE PRESCRIPTION, which is the half that was missing. w_an_unreadable_installation_list_is_not_an_absent_installation asserts only that the REASON keeps the two apart and never reaches next_acquisition_step, so it was green while the prescription was wrong -- a wall that does not execute over the thing it names is not a wall. w_an_unreadable_installation_prescribes_the_credential_and_never_the_consent asserts both legs: unreadable sends the operator to the credential and NOT to the install page, consent does the opposite, and the two answers differ. MEASURED, WITH THE COLLAPSE REINSTATED: FAIL w_an_unreadable_installation_prescribes_the_credential_and_never_the_consent PASS w_an_unreadable_installation_list_is_not_an_absent_installation PASS w_all_three_facts_established_is_a_receipt_naming_all_three The old claim staying GREEN under the defect is the reviewer's point demonstrated rather than restated. Evidence on this tree: 68/68 claims green (rc=0). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…usted population
installation_standing_for filtered the listing by app_id and took the first
element; account, repository selection and observed permissions never reached
the admission, and one page was read as the whole population.
- CensusAppInstallationSubject { app_id, expected_account, repository_selection,
required_permissions }, derived from the registration's app id and the
declared consent (account gunb-ai, selected repositories, census manifest
permissions, held at least as strongly as declared).
- AdmittedCensusInstallation is sole_constructor: only admit_census_installation
mints one, and the receipt carries it (id and account), not a bare id.
- InstallationPopulation carries a std.page_fold outcome; an unclosed walk is
InstallationUnreadable, never absent. Zero matches is consent missing,
a deficient match is InstallationInsufficient, two on one account is
InstallationAmbiguous. Each reaches next_acquisition_step as its own arm.
- The live read cannot observe the Link header through the REST transport,
so its first page is named InstallationsFirstPageOnly and refused as
unreadable; the capability is a frontier row
(census_app_installation_population_frontier_rows).
Five controls, each shown red by a mutant of admit_census_installation
(drop the account term; empty the required permissions; raise the ambiguity
threshold; map PagesRefused to NotEstablished; never admit), baseline green
including w_an_unreadable_installation_prescribes_the_credential_and_never_the_consent.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
This was referenced Sep 21, 2026
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
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
lively-crab-711.Pushing to
session/lively-crab-711advances 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