Skip to content

Mint the Sheets calling home, model the Drive API, and converge the two steps that needed a human - #11485

Merged
briansrls merged 42 commits into
mainfrom
session/zesty-crane-846
Sep 18, 2026
Merged

briansrls merged 42 commits into
mainfrom
session/zesty-crane-846

Conversation

@briansrls

@briansrls briansrls commented Sep 16, 2026 •

Copy link
Copy Markdown
Contributor

sheets_calling_strategy has always been CreatePurposeScopedProject; what was Absent was the id, because sheets_evidence_lead found no clean adopt target. Operator ruling 2026-09-16 mints it: gunbai-sheets, writer review-sheet-writer@gunbai-sheets.iam.gserviceaccount.com.

The refusals survive selection

SheetsCallingHome gains a Selected arm carrying refused_api_surface_project and refused_writer forward. gunbai-secrets is not merely unchosen — it is refused as an API surface because custody and API surface are separated in the target state, and a Selected arm holding only project_id would let a later lane move Sheets back there as a simplification. On the selected arm the refusal predicates get stronger: the unresolved arm could only say secrets was the project being refused, while the selected arm also says the home is not it.

Selection is not observation

Selecting the project settles where Sheets is called from and establishes nothing about whether it exists, has the API on, or has granted the writer anything. Enablement enters the operator admission as ServiceEnablementUnobserved — not Disabled, which would claim a serviceusage read never performed. Under EnsureObserveOnly that is EnsureInaccessible -> Refuse, so the admission names its obligation and no path reaches Admitted.

Two predicates replaced, not deleted

sheets_calling_home_is_unresolved and sheets_home_is_create_purpose_scoped_unminted asserted a state that is now spent — but what they protected (the home never silently becomes the secrets project, and never a sandbox) is live precisely at resolution. Both witnesses assert the surviving property against the Selected arm rather than being dropped with the state they guarded.

extdeps.google.drive

drives.get, permissions.list/create, files.list/create, cited and versioned. Three modelled facts worth naming:

  • Shared-drive roles are not the file-sharing roles. The console's "Content manager" is the API's fileOrganizer; organizer is "Manager", which administers membership — the authority a write-only automation must not hold. Variants, not a string, so the escalation must be authored deliberately.
  • supportsAllDrives is a constant on every call, never a caller parameter: without it a shared-drive id reads as 404, meaning "you did not ask about shared drives" rather than "it is not there", and a caller that could pass false could ask a question whose refusal it would misread.
  • The full drive scope is named rather than drive.file, because a membership write targets a resource this app did not create, which drive.file cannot express.

gunbc.review_sheet_drive_converge

Two ensures, because the two steps needed a human for different reasons. Membership is bootstrap-shaped — the writer cannot grant itself access to a drive it is not in, so that ensure runs under a credential that already manages the drive, once per drive. The spreadsheet is recurrence-shaped — files.create mints a new file every call, so the answer is an identity chosen before the call. appProperties carries it, private to this app, and deliberately not the file NAME: a rename must not make the next converge believe its sheet is gone and mint a replacement beside it.

Residency is recorded as the Customer Acquisition shared drive, grounded on the operator's read of the drive details panel rather than on the id's format.

Evidence

Executed on srv1 (claim_batch), not derived:

  • sheets_calling_home_is_selected_and_does_not_default_to_secrets — PASS
  • gunb_test_and_other_projects_are_gaps_not_observed_homes — PASS
  • committed_project_and_writer_are_selected_not_secrets_defaults — PASS
  • fleet_admission_is_the_estate_calling_home_not_a_second_standing — PASS
  • fleet_admission_does_not_admit_while_enablement_is_unobserved — PASS

The exhaustiveness check earned its keep here: adding the Selected variant refused four predicates that read fields only the unresolved arm carries, which no amount of reading had caught.

Sixteen further witnesses cover the Drive folds, their results reported in-thread when they land. The load-bearing pair is incompleteSearch: an empty file list beside "I could not look everywhere" must refuse, and the same empty list with a complete search must create — without the second, a fold that refused everything would pass the first while making the converge unable to create anything.

Not in this change

This section was materially stale and is corrected here — it described the first push, and the PR grew a long way past it over nine review rounds. Reviewers were reading a scope statement that had stopped being true, which is my error and worth naming rather than quietly rewriting.

What the earlier text got wrong:

  • It said "no bytes have reached Google". Bytes have. gunbc.review_sheet_values_actuator is in this change, and its executed consumer wrote 58 rows to the live sheet on 2026-09-16. The Drive membership and spreadsheet converges have run against the real API — the appProperties defect and the trailing-blank comparison defect were both found by live runs, not by witnesses.
  • It said the actuator "is not here either". Four actuators are here: Drive membership, spreadsheet, values, and the GCP bootstrap.
  • It said projects.get/projects.create and serviceAccounts.get "do not [exist]". All three exist now, and GetProject returns a GcpProjectResourceV3 carrying the lifecycle state a converge must read.

What is genuinely not in this change:

  • live_sheets_transport_frontier is still open. It binds live Sheets transport to the identity-keyed review_sheet_ensure path, which is a different obligation from "has any byte been written" — and it stays open for a reason that matters: converge_sheet_values is a whole-range equality-and-replacement actuator. The moment the sheet carries operator-entered columns, a whole-range rewrite would clear them. That path needs an identity-keyed projection that preserves operator fields before it becomes the recurring route.
  • No public entry point calls converge_sheet_values. Its caller lived in gunbc-private and is preserved on an unmerged branch, not in this tree, so the fold sits behind a declared frontier.
  • The census that would produce rows is not here. Two modules that attempted it were held out of this PR: one was dangling, and one forked gunbc.runner.runner_label_resolution, which already owns the runs-on label question against per-vendor catalogs.
  • Formatting is not here. It has no call site, which is why it was held.

🤖 Generated with Claude Code

sheets_calling_strategy has always been CreatePurposeScopedProject; what was
Absent was the id, because sheets_evidence_lead found no clean adopt target.
Operator ruling 2026-09-16 mints it: gunbai-sheets, writer review-sheet-writer@,
created by hand because no agent holds a GCP admin credential.

SheetsCallingHome gains a Selected arm that CARRIES THE REFUSALS FORWARD.
gunbai-secrets is not merely unchosen: it is refused as an API surface because
custody and API surface are separated in the target state, and a Selected arm
holding only project_id would let a later lane move Sheets back there as a
simplification. gunbai_secrets_enabled_services_are_closed still asserts Sheets
is off there; a live serviceusage read reproduced that independently.

SELECTION IS NOT OBSERVATION. Selecting the project settles where Sheets is
called from and establishes nothing about whether it exists, has the API on, or
has granted the writer anything. Enablement therefore enters the operator
admission as ServiceEnablementUnobserved, not Disabled -- Disabled would claim a
serviceusage read never performed against a project the operator creates by
hand. Under EnsureObserveOnly that is EnsureInaccessible -> Refuse, so the
admission names its obligation and no path reaches Admitted.

Two predicates were REPLACED, not deleted. sheets_calling_home_is_unresolved and
sheets_home_is_create_purpose_scoped_unminted asserted a state that is now spent,
but what they protected -- the home never silently becomes the secrets project,
and never a sandbox -- is live precisely at resolution. Both witnesses assert the
surviving property against the Selected arm instead of being dropped with it.

Residency is modelled because the operator chose a shared drive, and that changes
the SHAPE of the human step rather than its target: a My Drive sheet is reached by
sharing that sheet, which spreadsheet_share_intervention says recurs for every new
sheet; a shared drive is reached by making the writer a member once, retiring the
recurrence. Content Manager, not Manager: the writer adds and edits files and does
not administer membership. What this does NOT assert is that a shared drive
survives a tightened external-sharing policy -- that is an inference from the
2026-09-11 console read, not a read of the shared-drive case, and an SA is outside
gunb.ai either way.

live_sheets_transport_frontier is deliberately untouched. No bytes have reached
Google, so the Scaffold stands; dissolving it on code-written-ness would be rung
inflation, and the mock corpus proves replay, not transport.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review September 16, 2026 22:06
Brian Searls and others added 7 commits September 16, 2026 22:19
The exhaustiveness check caught what I had missed: four predicates read fields
that only the unresolved arm carries, so adding a variant forced each to decide
rather than letting a stale answer through. On the selected arm two of them get
STRONGER -- the unresolved arm could only say secrets was the project being
refused, while the selected arm also says the home is not it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…dency

Operator-supplied 2026-09-16. The id shape is consistent with a shared drive
rather than a folder inside one (19 chars leading 0A, against a ~33 char My Drive
folder id leading 1), and a shared drive's root folder id IS the drive id, which
is why the url reads /folders/. That is a read of the FORMAT and not of the
resource: no Drive-scoped credential has resolved this id yet, so the drives.get
that would ground it is recorded as an open obligation rather than a discharged
one, and the drive NAME is what the operator called it in conversation.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…panel

The id shape only suggested a shared drive. The operator's read -- Type: Shared
drive, Owner gunb.ai, Security limitations: none -- settles type and name by
observation, at the grain of what the panel displays: the membership list is a
separate fact and is not established here. The no-limitations reading also
narrows why the UI refused the writer: not this drive restricting external
principals, but the sharing dialog declining a gserviceaccount.com address at
all, which is why the converge must take the API path.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…eadsheet

extdeps.google.drive: drives.get, permissions.list/create, files.list/create,
cited and versioned. Three modelled facts worth naming. Shared-drive roles are
not the file-sharing roles -- the console's Content manager is the API's
fileOrganizer, and organizer is Manager, which administers MEMBERSHIP and is
exactly the authority a write-only automation must not hold, so they are
variants rather than a string. supportsAllDrives is a constant on every call,
not a caller parameter: without it a shared-drive id reads as 404, which means
'you did not ask about shared drives' and not 'it is not there'. And the full
drive scope is named rather than drive.file, because a membership write targets
a resource this app did not create, which drive.file cannot express.

gunbc.review_sheet_drive_converge: two ensures, because the two steps needed a
human for DIFFERENT reasons. Membership is bootstrap-shaped -- the writer cannot
grant itself access to a drive it is not in, so that one ensure runs under a
credential that already manages the drive, once per drive. The spreadsheet is
recurrence-shaped: files.create mints a new file every call, so the answer is an
identity chosen BEFORE the call. appProperties carries it, private to this app,
and deliberately not the file NAME -- a rename must not make the next converge
believe its sheet is gone and mint a replacement beside it.

Three arms exist to refuse rather than fold to absence, and each one is a way a
converge mints a duplicate: an unread permissions field is not an empty list; a
writer present with an unmodeled role is not an absent member; and Drive
answering incompleteSearch beside an empty result is not an observation of
absence. Duplicates refuse and never select -- two files under one key means a
create was retried after its answer was lost, and choosing either abandons
whatever was written to the other.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ions

Two real faults the typecheck named. The language has no list destructuring
patterns, so the empty/one/many split is count and first rather than [] and
[x, ...rest]. And DESIGN 4c admits an annotation only above a MODULE-SCOPE
declaration: my reasoning sat inside fn bodies and inside service blocks, where
it names no subject. Lifting it is not a loss -- the supportsAllDrives argument
and the not-idempotent argument are about the whole service, which is where they
now sit.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Optional's absent arm is spelled none in a returning position -- Absent there
resolved as the Optional coproduct itself against a DrivePermissionRole branch.
Comparing the raw against drive_permission_role_wire rather than string literals
also stops the wire spellings existing twice in one module.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sixteen claims over the two folds. The load-bearing pair is incompleteSearch:
Drive answering an empty list beside 'I could not look everywhere' must refuse,
and the SAME empty list with a complete search must create -- without the second
claim a fold that refused everything would pass the first while making the
converge unable to create anything at all.

The other discriminations are the same shape. An absent permissions field is
unreadable; an empty permissions list is absence. A writer present with a role
this model cannot read is unreadable, not absent, because a second grant would
not change its role. A different principal holding organizer is still absence
for OUR writer. Organizer satisfies and is not corrected downward. And duplicates
refuse naming both ids, because picking either abandons what was written to the
other.

Inputs are supplied at one boundary -- a Drive response shape -- rather than
reached for over the network: these are claims about what the fold DECIDES, and
executing the transport to obtain a response would pay a round trip per assertion
to test something else. The inhabitance claim that Drive really emits these
shapes is the live converge run, which is a separate receipt and is not claimed
here.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot gunbai-bot Bot changed the title Customer Acquisition Mint the Sheets calling home, model the Drive API, and converge the two steps that needed a human Sep 16, 2026
Brian Searls and others added 20 commits September 16, 2026 22:57
…again

review_sheet_drive_converge decides; this module is the only place that performs.
The split is why fifteen witnesses could establish the decisions without a
network, and this module is what those witnesses deliberately do not execute.

A GRANT IS FOLLOWED BY A READ, and the same read the converge already performs.
permissions.create is a mutation, so a lost answer leaves the write unknown --
classify_rest_outcome names that RestExchangeCommitAmbiguous. Retrying would be
wrong, since a second grant against an existing principal is not a correction,
and reporting success would be worse. Membership is a readable fact, so the
ambiguous arm re-reads rather than assuming; and the success arm re-reads too,
because a create answering 200 has told us what it did, not what is now true.

MembershipGrantUnverified exists so the third state has a name. A grant that was
neither confirmed absent nor observed present is not a success and not a refusal,
and collapsing it into either is the fabricated answer this repository keeps
finding.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
THE SPREADSHEET'S AMBIGUITY IS THE HARDER ONE, and it is why the key is chosen
before the call. A lost answer from files.create may have minted a spreadsheet
whose id this process never saw; nothing in the response recovers it, because
there was no response. The only route back to that file is a property written
ONTO it at creation, so the recovery read is not a nicety -- it is the whole
reason a create is allowed at all. Membership had the same shape and a milder
consequence: a lost permissions.create leaves a principal, and re-reading
settles it. A lost files.create leaves a FILE, and without the key the next pass
finds nothing and mints a second one while the first holds whatever was written
to it.

THE BOOTSTRAP IS THE REPAIR OF MY OWN OUT-OF-BAND ACTUATION. The project, the two
API enablements and the writer were created with curl against an operator token;
that worked and left no trace any program can read. The test of this repair is
that running it now answers already-converged for all three rather than creating
anything.

Two refusals worth their own arms. CreateProject returns a long-running
Operation, so ProjectCreateAccepted is not ProjectAlreadyPresent: only a later
projects.get establishes the project exists, and reporting an accepted request as
a resource is the fabrication this separation prevents. And a 404 is an answer
while a 403 is not -- Resource Manager answers 403 for a project that exists but
is invisible to this caller, so folding it to absence would authorize a create
whose only outcome is a 409, reporting a permission problem as a name collision.

New operations: ResourceManager GetProject/CreateProject and IamAdmin
GetServiceAccount, the readback halves that idempotency needs.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… create

Nine claims over the pure folds. Two are the discriminating ones. A 403 is not
absence -- Resource Manager answers it for a project that exists and is invisible
to this caller, so folding it would authorize a create whose only outcome is a
409, reporting a permission problem as a name collision and sending the reader to
the wrong fix. And an unmodeled service state is FOREIGN, not Disabled:
STATE_UNSPECIFIED is in the cited enum, and treating it as disabled would enable
a service whose state we failed to read.

DELETE_REQUESTED gets its own claim for the same reason. The id is taken, so a
create refuses, and a converge that called the project absent would report a
naming collision whose real cause is a pending deletion.

The performing half is not executed here and is not claimed: the converge's
inhabitance receipt is a live run, and asserting these folds is what will make
that run's outcome interpretable.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Adds the performing halves that were missing -- services.enable and the service
account create-with-readback -- and the CLI that sequences every step in
dependency order.

TWO REFUSALS IN THE ENTRY POINT ARE DELIBERATE. The project step is not called
here: creating a project needs org-level authority the writer will never hold, so
folding it in would mean this entry point only ever succeeds under an org admin's
credential, which is the standing privilege the estate's blast-radius discipline
avoids. And the steps do not short-circuit on the first refusal, because a run
that stops at the first problem reports one obstacle per invocation and makes an
operator clear four in four rounds; every step is observed independently so one
run names everything between here and converged.

CONVERGED IS NARROWER THAN NOT-REFUSED. services.enable and projects.create are
both long-running, so Accepted is progress and not a converged state; an
unverified create is likewise neither success nor refusal. All three leave the
run non-zero, and re-running after an accepted enable is the intended path.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…tation

An operation without an outcome field cannot be classified: extdeps.transports.rest
records that dispatch_rest raises a rendered TypeError rather than returning a
status, so a caller cannot reach the status, cannot reach the body, and cannot
persist either. Five operations this converge calls were in that state --
GetService, EnableService, GetProject, GetServiceAccount, CreateServiceAccount --
so classify_rest_outcome had nothing to read. This is the same specification-
without-execution that type's own annotation describes, met from the calling side.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbc run passes arguments only as --arg name=value, which is argv, and
gunbc.credential_argv_exposure measures what that means on this fleet: no
hidepid, cmdline 0444, runner slots in the host pid namespace, so an argv word is
readable by any job payload a pull request can influence. A re-measurement on
2026-09-16 reproduced it and added the other half -- environ is 0400 and
cross-user reads are denied -- which is why auth_source EnvVar is the fix and not
a smaller hazard of the same kind. github.Workflows already reads GITHUB_TOKEN
this way; the Drive service now reads GUNBC_REVIEW_SHEET_TOKEN the same way, and
no Drive operation takes a token a caller could interpolate.

converge_drive_half_cli takes NO ARGUMENTS, so there is nothing to put on a
command line at all. It is also the half worth running first: the three GCP steps
were actuated by hand and observed converged, so running them proves a Noop,
while membership and the spreadsheet have never executed.

The GCP services keep auth_input because they are shared with other consumers,
and changing a credential shape under them is not this lane's to make.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ness

The live run refused twice with AuthDeclaredButUnwired while the variable was
demonstrably set in the process environment -- a probe under the same wrapper
read it back at full length. The cause is in the config parse, not the
invocation: svc_auth_source reads the name through extract_string_value, which
pulls a string LITERAL from the node and does not evaluate an expression, so
EnvVar { name: drive_token_env } resolved to nothing and the transport correctly
reported the variable absent. github.Workflows spells GITHUB_TOKEN as a literal
for the same reason.

That forces one name into two places, which DESIGN section 3 would otherwise
refuse, so the duplicate is pinned by a claim rather than left to diligence: if
either spelling moves, every Drive call refuses as a missing credential rather
than as a renamed one, and that is a diagnosis nobody would reach quickly.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The first live run proved the difference the expensive way. A create body of
{ key: K, value: V } does not set a property named K -- it sets two properties
literally named key and value, so the file exists and no search for a
property NAMED K can find it. The run reported UNVERIFIED rather than success,
which is the arm working: had it trusted the create's own 200, the next pass
would have minted a second sheet beside an invisible first.

The property name is now a literal in the body, because the body builder emits
field names as written and cannot take one from a parameter -- the same forced
duplication as the auth env var, and pinned the same way, by a claim that fails
if the written name and the searched name drift apart. A drift there produces a
file that exists and cannot be found, which reads as a create that did not take.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…r than assumes

live_sheets_transport_frontier reserved a caller for the Sheets service, which
until now had zero call sites -- the frontier stated as a number. This is that
caller: read, compare, write only on difference, read again.

THE READBACK IS NOT THE WRITE'S OWN RESPONSE. batchUpdate answers with counts of
what it changed, which is a statement about the request and not about the sheet;
a separate values.get is what establishes the cells hold what was sent, and it is
the same read the next converge performs. RAW and FORMATTED_VALUE are consumed
from review_sheet_sheets rather than restated: USER_ENTERED would parse a derived
string so the readback would differ from what was written, and the converge would
report a conflict against its own output.

EQUALITY IS LINEAR AND THREE-VALUED. Indexing one list while folding the other is
quadratic because skip walks, and section 6 fixes a proven quadratic regardless
of the realized n. Both sides are serialised once instead. That is sound only
while no cell contains the separator, which is a property of the DATA and not of
this code -- a repository description can contain anything -- so the comparison
does not assume it: RowsIncomparable is its own arm, and the caller refuses on it
rather than reporting an equality it cannot establish. A false equality skips a
write the sheet needs; a false difference rewrites an identical sheet forever.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The lexer does not take a unicode escape, so the unit separators became long
printable sentinels -- checked by cells_carry_separator either way, which is why
the choice is safe rather than lucky. A raw control byte in source would be worse
than an implausible string that is guarded.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…t live write

ValueRange.values is Optional because a RESPONSE may omit it -- values.get on an
empty range returns no values field. But an Optional does not serialise to a bare
array: it carries its variant, so a request body built from ValueRange reaches
Sheets as {values:{_variant:Present,value:[[...]]}} and is refused with
Unknown name _variant.

THE MOCK CORPUS COULD NOT CATCH THIS. PublishedMockCase fixes the RESPONSE shape,
so a witness over it agrees with a request encoding nobody ever sent -- shape
agreement standing in for execution, and the wire is where the two part company.

The defect is not only in the new code. review_sheet_sheets
value_range_from_derived_write builds the same Optional form and has never
executed; it is the caller live_sheets_transport_frontier reserved, and it needs
ValueRangeWrite before its first write. That is a defect in a landed module,
found by running one, not a gap in a new one.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The first live write established it. 58 rows went out at 17 cells each and came
back at 15 or 17, the 15s being exactly the rows whose Decision and Note are
empty. The readback is semantically identical and structurally shorter, so a
literal comparison reports a difference the sheet does not have -- and the
converge would rewrite an identical sheet on every run, forever.

Both sides are now trimmed to their last non-empty cell. That is the
normalisation the API itself performs, not a tolerance invented to make a check
pass: an empty cell in the MIDDLE of a row still compares, so a cleared Decision
is still a difference.

UNVERIFIED was the correct answer to the run that found this. Had the write
trusted its own success the sheet would have been right and the converge would
have been wrong about it forever, which is the harder failure to notice.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Okabe-Ito is the right set for the Standing column for a reason beyond
availability: it is constructed to stay distinguishable under common colour
vision deficiencies, and Standing is the column a reader scans fastest. A palette
chosen for looking pleasant would fail exactly the reader who most needs the
distinction.

Each channel triple is transcribed beside the swatch it comes from, and the
duplication is forced: a Sheets colour channel is a Float in [0,1], a swatch
channel is an 8-bit Int, and this corpus has no Int-to-Float conversion, so
158/255 cannot be computed here. The arithmetic is written out so a reader can
check it; the dissolution is that conversion landing in std.

A FORMAT WRITE HAS NO READBACK and the module says so. Reading a cell's format
means spreadsheets.get with includeGridData, a response shape this module does
not model, so these steps report what the API answered and nothing about what the
sheet looks like. Formatting is therefore not idempotent-by-observation, and
conditional rules accumulate, which is why the rule steps take an explicit index.

Evidence-insufficient rows are deliberately uncoloured: they are most of the
sheet, and colouring them would spend the reader's attention on the rows that
earned the least of it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rclaim

All three findings verified against the code and all three were right.

THE CITATION NAMED A MODULE THAT DOES NOT EXIST. extdeps.google.sheets claimed
gunbc.extdeps_google_sheets_token_pin kept the env-var spellings from drifting;
git grep finds only the citation. That is the positional-citation failure DESIGN
section 3 forbids, in its worst form -- a reference to nothing, asserting a
guarantee nobody wrote. test.claim.review_sheet_transport_pin_witness now exists
and the citation names it.

THE PLAN CARRIED A KEY NOTHING COULD USE. SpreadsheetCreatePlan held
app_property_key while CreateFile writes the property name as a body literal, so
the field suggested a choice the caller does not have and the actuator never read
it. Removed, and the annotation now states which side the pin reaches: the query
is built from the declaration and a claim can read it back; the body literal is
emitted as syntax and no claim in this corpus can reach it.

THE MODULE OVERCLAIMED ITS OWN FRONTIER. It said it was the transport
live_sheets_transport_frontier reserved; that frontier reserves a caller for
review_sheet_ensure, which this module does not call. The frontier is still open.
And this module has no importer here at all -- its consumer is in gunbc-private,
invisible to every consumption check this repository runs -- so it now carries a
declared frontier with a trigger rather than reading as dangling.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…by reading

A RATE IS NOT A BILL. This module carried per-minute prices and nothing about
whether a SKU is charged, so a consumer could multiply a rate by observed minutes
for any repository and get a number that should be zero. For a prospect model
that is the difference between a payer and a non-payer, and it was being reached
by reasoning until an operator asked for the source.

WHAT THE DOCS SETTLE, read 2026-09-17. For private repositories each account
receives a quota of free minutes depending on its plan; the use of standard
hosted runners is free in public repositories; and larger runners are always
charged for, even when used by public repositories or when quota is available.
The per-plan allowance is a PRIVATE-repository quota -- public standard-runner
minutes are free and never draw on it. Reading that allowance as a universal cap
is the plausible misreading these types exist to make unwritable, and it is the
reading an operator and I each held for a while.

WHAT EXECUTION SETTLED. The ARM SKU refused classification for an hour because
GitHub has shipped ARM under both standard and larger terms. Two probe runs on
this public repository answered it: ubuntu-24.04-arm billed 0 ms beside an
ubuntu-latest control that also billed 0. A larger runner is charged EVEN on a
public repository, so a hosted runner billing zero there is not one. The control
is what makes that an argument rather than an anecdote -- x86 had answered zero
half an hour earlier, so the ARM zero is about the SKU and not the repository,
the plan, or the day.

RunnerClassUnread survives the SKU that needed it: the next hosted SKU arrives
unclassified, and for a prospect model an unread SKU must answer not-billable
rather than invent a payer.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Both findings verified against the code and both were right.

THE ALLOWANCE IS A DURATION AND std.measure ALREADY OWNS THAT CONCEPT. It sat on
a bare Int three lines from per_minute: MoneyPerMinute, pulled from the same
import block, so the module was importing a measure carrier and minting a second
authority for minutes in the same breath. That is the failed decomposition
DESIGN section 2 names -- a fresh leaf for a concept that exists. It now carries
Minute, and the values are built with minute(count:) rather than written as
scalars.

TWO MODULES WERE DANGLING AND NEITHER SAID SO. The billability fold and the whole
format actuator have no importer in this repository; their consumers are in
gunbc-private, which the public corpus cannot import, so every consumption check
here sees them as unreached and is right to. Both now carry a declared frontier.

The format one deserved a sharper statement than the values actuator got, and
this is the part worth reading: the values actuator genuinely HAS an out-of-repo
consumer that has executed, so its frontier records an invisible edge. Formatting
has no caller in EITHER repository -- the private entry point converges values
and does not call it -- so it is an artifact with no final consumer anywhere, and
the row says that rather than borrowing the values actuator's excuse.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… overclaim

THE ARGV ENTRY POINT IS DELETED RATHER THAN DOCUMENTED. converge_review_sheet_cli
took the operator credential as a CLI argument while this same change carries the
measured reason that must not happen -- cmdline is 0444 on this fleet and runner
slots share the host pid namespace, so an argv word is readable by any job
payload a pull request can influence. Its comment admitted the hazard and carried
on, which is the escape hatch section 5 refuses. It was also a second path beside
a modelled one: converge_drive_half_cli takes no arguments at all, six lines
below. A parallel authority strictly worse than the route beside it is the one a
hurried reader copies. The gap it papered over is real and is NOT closed by
deleting it -- the GCP operations still take a token as an operation input, and
an argv-free entry for them lands when those services gain an auth_source read.

A FIELD NAMED FOR CELLS CARRIED A ROW COUNT. updated_cells was populated with
value_range_row_count, so a consumer reading it got a plausible number that was
not the fact its name names. Deleted rather than computed: batchUpdate does
report totalUpdatedCells so it could have been filled honestly, but nothing
consumed the field, and inventing a consumer to justify it is how a model grows
facts nobody asked for.

THE PALETTE CLAIM COVERED COLOURS IT DID NOT HOLD FOR. The module asserted its
colours come from the cited palette rather than from taste; three do, and two do
not. White is a ground rather than a hue from a set, and the thin-standing grey
is hand-picked -- Okabe-Ito has black and no mid grey, so that tone came from me.
The header now says three of five, and each exception is marked at its own row,
because a reader deciding whether to trust these values needs to know which were
derived and which were chosen.

Finding three's text was truncated before its detail reached me and there is no
artifact fetch available from here, so this addresses the contradiction I could
verify at that location rather than the one that may have been reported. If it
named something else at review_sheet_format_actuator.dag:66, say so and I will
take it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
CI refused at floor_class=structural on the same defect review 67130 named, found
independently: a witness read app_property_key, a field removed while addressing
review 67120. I broke it fixing something else and did not re-run the suite, so a
green I had reported was stale by the time I repeated it. That is the failure
mode this session keeps finding in its own work -- a claim carried forward after
the ground moved.

A PAGE IS NOT THE LIST, and both Drive folds treated it as one. permissions.list
and files.list each request nextPageToken and neither fold read it, so a writer
absent from page one read as MembershipAbsent and would have granted a permission
that may already exist, and one matching file on page one read as SheetObservedOne
and would have adopted while page two held another. That is the incompleteSearch
failure one function away, reached by a different route: a partial look folded
into a complete observation. Both now refuse on a present token, with a claim each
and the existing fixtures extended to say which case they are.

THE SERVICEUSAGE WIRE HAD TWO DECIDERS. enablement_from_state re-spelled ENABLED
and DISABLED as literals while gcp_service_enablement
service_enablement_from_state_wire already folds that wire through the cited
closed sum -- and does it better, since it knows STATE_UNSPECIFIED rather than
falling through. The local one is deleted and the existing fold consumed.

41 claims green by execution across the three affected suites.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…o consumer

CI was red on six parse errors, all one class: source annotations inside a
declaration body in extdeps.github.workflow_runs. DESIGN 4c admits annotations
only at module-item grain, and an `operation` lives inside the `service`
declaration's body. The file already carried an annotation saying exactly that,
written two commits ago; the rationale for the attempt_filter parameter is now
hoisted onto the service beside it.

Review 67147 finding 1 -- durations. PrestartReading.seconds, JobTiming's two
Int fields, CancellationReading.cancelled_occupancy_seconds and both occupancy
folds carried bare Int for a quantity std.measure already owns. The review
quotes this PR's own sentence from extdeps.pricing.github_actions back at it:
"a bare Int here would be a second authority for minutes, which is the failed
decomposition DESIGN section 2 names." It applies verbatim here, and this is
the module whose occupancy a billing consumer multiplies against MoneyPerMinute,
so the unit carrier is exactly where the two must meet. Now Second, second(),
second_count() and measure_add from std.measure.

Two defects surfaced while doing it rather than declaring it. The first draft
cast `(started - created) as Nat`; test.claim.runner.runner_microvm_network_witness
already records that `i as Nat` COMPILES and then fails at claim execution with
"cannot cast Int to Nat", taking six witnesses red on the floor while every
targeted compile stayed clean. The epochs are Nat at the boundary instead, so no
cast exists. The new annotation also cited `gunbc.actions_billing` as the
consumer -- no such module; a fabricated citation inside the fix for a citation
finding. It names extdeps.pricing.github_actions, verified to resolve.

Review 67147 finding 2 -- gunbc.review_sheet_format_actuator, 252 lines whose
own annotation admits formatting has no caller in either repository. DESIGN 3c
is unambiguous that a dangling declaration is red however well modeled, and
DESIGN 6 that a trigger added after review makes a proposal eligible for a
decision rather than resolving the objection. Held out of this PR on branch
held/review-sheet-format until its call site lands. Removing it alone would have
relocated the finding into extdeps.google.sheets, where SheetsColor,
SetFrozenRows, FormatCellRange, AddTextColorRule and their three citations
existed only for that consumer, so they are held with it (473 -> 312 lines).

Evidence: required-ci witnesses lane on srv1, parse and declarations phases
green at this tree. The remaining two local-repo-wet refusals
(self_host_logic_{behavioral,seed_unavailable}_witness) are not from this diff:
neither witness's import closure (207 and 85 modules) reaches any module touched
here, and both report observed=passed on main's own CI run 35054088258. They
reproduce on a clean worktree and are specific to this session's srv1 invocation.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Brian Searls and others added 8 commits September 17, 2026 07:20
…oducts

CI refused the floor on a non-exhaustive match, and the first fix here was wrong
in a way worth recording: it patched the one site CI named. There were four. The
earlier commit widened DriveMembershipObservation with MembershipPageIncomplete
and ReviewSpreadsheetObservation with SheetPageIncomplete and did not re-derive
their consumers, so the symptom appeared at whichever site the compiler reached
first. DESIGN section 6b names this exactly -- a fix whose diff touches only the
link where the symptom appeared, with no statement of why that link is the
earliest unjustified boundary. The boundary is the type change, and the census is
the fail-closed substrate itself: every real consumer refuses loudly, so the floor
lists them. All four arms now refuse rather than widen, because one page of a
longer list establishes neither presence nor absence. The spreadsheet noop arm is
the load-bearing one: without it a converge could adopt a sheet while a second
file carrying the same app-properties key sat unread on page two, which is the
duplicate-mint this converge exists to prevent.

Review 67201 finding 1 -- extdeps.github.workflow_runs runner_name. Main deleted
this field with the rationale that interesting is not a consumer, and that a
frontier admits a declaration whose consumer lands in a named later change. This
PR put it back and its annotation claimed the consumer had arrived:
gunbc.actions_job_observation runner_provenance. It had not. That module imports
only std, v2.std.algebra and gunbc.actions_runner_label, never this one, and
runner_provenance takes a bare String no fold sources from this field. The claim
was a route asserted in prose while the diff carried none -- DESIGN section 4c:
an annotation is never evidence that a machine claim holds. Deleted again, with
the rationale restored and this second attempt recorded beside it so the next
lane does not re-add it on the same reasoning. The depot-1mw2k81zm2 example is
kept, because it is why RunnerProvenance has three arms rather than two.

Review 67201 finding 2 -- extdeps.pricing.github_actions. The frontier row's prose
said "these declarations" while its bind named one, leaving
github_actions_plan_allowances and allowance_applies dangling outside it. A
frontier naming less than it covers is its own defect, so each now carries a
FrontierRow with its own trigger through std.roster_frontier, the carrier this
corpus already uses for per-declaration frontiers.

Evidence: required-ci witnesses lane on srv1 -- parse, declarations and the
touched-subject compile all green at this tree, no non-exhaustive match remaining.
The two local-repo-wet refusals are unchanged and are not from this diff: neither
witness's import closure (207 and 85 modules) reaches a module touched here, and
both report observed=passed on main's CI run 35054088258.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Two subtrees in this change are dangling and said so only in a leading
annotation. DESIGN section 4c rules that out as evidence: no Accepted program can
read a comment, so a prose classification is invisible to every consumption check
this corpus runs, and the rest of this change already used typed carriers for the
same state (review_sheet_values_consumer_frontier,
actions_billability_consumer_frontier, actions_allowance_consumer_frontier_rows).
The two now agree.

Checking the finding changed the answer twice, and both are worth recording.

First, the trigger the prose named was "when those services gain an auth_source
read". Drive and Sheets gained exactly that IN THIS PR, so the question was
whether the condition had already fired -- in which case the honest fix is to land
the route, not to declare a frontier. It has not: the GCP operations
(serviceusage, iam, iam_admin) take their token as an operation input, auth Bearer
with auth_input, because they are shared with consumers this lane does not own.
That is why the drive half has a working argv-free entry and this half does not,
and it is the capability each row below names.

Second, the review listed six declarations in the CLI and three in the bootstrap.
Deriving the unreachable closure from each module's entry points instead gives
eleven and five: the review did not name ReviewSheetConvergeReport,
review_sheet_writer_account_id, review_sheet_writer_display_name,
ProjectConvergeOutcome or read_project. Fixing exactly what was reported would
have shipped a frontier naming less than it covers, which is the defect the
previous commit fixed in extdeps.pricing.github_actions. Each declaration gets its
own FrontierRow through std.roster_frontier, the carrier this corpus already uses.

The surviving annotation points at the roster instead of restating the set, so
there is one authority for what is deferred rather than two copies that drift.

Evidence: required-ci witnesses lane on srv1 -- parse, declarations and the
touched-subject compile green, no CITED-MODULE-ABSENT, so every decl_ref in the
new rows resolves. Also required-ci green end to end on GitHub at the parent
commit e249b97, which independently confirms the two local-repo-wet refusals
seen here are specific to this session's srv1 invocation: CI passes them.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ailable

Every finding here is a DESIGN section 5 violation written while this same PR
quoted section 5 at other modules. All three are real and all three are fixed.

1. gunbc.actions_job_observation folded an unread interval to zero occupancy and
summed it. A population of one executed 27-second job and one unread timing
reported 27, which reads as a complete measurement of a population that was not
completely measured -- the absorbing fallback in its purest form, since the zero
widens the answer rather than refusing it. job_occupancy now returns
OccupancyReading, and the sum absorbs in the correct direction: one unreadable
job makes the total unreadable. The distinction the old code erased is the point:
JobNeverStarted IS a reading of zero, because a job that never started occupied a
runner for zero seconds; JobTimingUnread is the absence of a reading. Three
witnesses land with it, which the review correctly noted were missing -- the
discriminating red on an unread timing, the same for the sum, and a control that
stops both from being satisfied by a fold that simply refuses everything. All
three PASS by execution through claim_batch, not by typecheck.

This defect also exists in the scratch analysis that produced this lane's
occupancy figures: that script assigned zero seconds to any job whose interval
was missing or implausible and then summed, so those totals are lower bounds over
a population with unmeasured holes counted as zeros. The modelled path now
refuses where the prototype zeroed, which is the reason to build it here.

2. extdeps.pricing.github_actions published two Bool questions that could not say
unread, and collapsed unread to false in both -- meaning OPPOSITE things. For
actions_usage_is_billable, false said "this costs its owner nothing"; for
allowance_applies, false said "the allowance does not apply", the direction that
charges in full. One Bool, two contradictory meanings, in one module, and the
first was labelled fail-closed in its own comment, which is exactly the trap
section 5 names by name. Both are three-valued now
(ActionsBillableVerdict, AllowanceApplicability), so the fail-closed direction a
prospect model wants stays a choice the caller makes visibly rather than a
collapse baked in where it cannot be seen. The two frontier rows follow the
renames.

3. extdeps.cloud.gcp.iam GetProject declared state in its output while mapping
200 to GcpProject, which is { project_id, project_number, name } and has no such
field. The state is load-bearing -- gunbc.sheets_bootstrap_converge reads it to
tell ACTIVE from DELETE_REQUESTED, which is the difference between a project that
is absent and one that is neither absent nor usable. Resource Manager v3
projects.get returns the project resource, so GcpProjectResourceV3 is declared
beside the service that returns it, exactly as GcpPredefinedRole sits beside
gcp.IamRoles, and GcpProject stays the estate-observation shape it already was.
Keeping the names apart is what stops the estate's project_number from being read
as a field this response carries, because it does not. The now-unused import
member is dropped.

Evidence: required-ci witnesses lane on srv1 -- parse, declarations and the
touched-subject compile over all 24 seed modules green, no non-exhaustive match
left by the new coproducts. The four occupancy claims PASS under claim_batch. The
two local-repo-wet refusals are unchanged and environment-specific to this srv1
invocation; CI passed them end to end at e249b97.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…are held out

Review 67238 is right that gunbc.actions_runner_label and
gunbc.actions_job_observation are dangling: no production module imports either,
and nothing feeds a real ListJobs response into job_timing or runner_provenance.
It offered two remedies -- land the consumer, or roster the closure as frontier
rows. Checking the corpus before taking either found a third fact that rules the
second one out.

THE LABEL QUESTION ALREADY HAS AN AUTHORITY. gunbc.runner.runner_label_resolution
resolves a runs-on label to a provider and an architecture, snapshot-dated, with
refusals for a label claimed by two catalogs. It is backed by
gunbc.runner.runner_provider_survey, whose roster enrolls ubicloud, blacksmith,
depot, warpbuild, namespace, buildkite, circleci, gitlab, aws_codebuild,
semaphore, runs_on and GitHub's own standard hosted labels -- every provider that
actions_runner_label re-answers with an eight-name prefix roster it authored from
a sample. It is consumed in production by gunbc.public_workload_census through
observed_provider_standing. So the module is a second authority for one question,
answering with a prefix guess where a cited vendor catalog exists, which DESIGN
section 3 rules out; and runner_provider_survey carries an annotation recording
that this same fork was caught in review once already, when an earlier revision
re-authored GitHub's hosted labels as free strings. Rostering frontier rows would
have admitted a fork as debt, which is why the review's second remedy is not the
one taken.

A third fork the review did not name, fixed here rather than held:
extdeps.pricing.github_actions declared ActionsRepositoryVisibility as
PublicRepository | PrivateRepository, character for character
extdeps.github.repository.RepositoryVisibility including both variant spellings,
while extdeps.github.hosted_runners already keys its per-visibility runner specs
off the real one. That is section 3 nicknaming -- a second name for one concept --
and it put two answers to "is this repository public" on either side of one
billing question. Consolidated onto the existing authority.

Both modules are held on branch held/actions-job-census with their review 67230
refusal fixes intact. What the follow-up owes is stated in the workflow_runs
annotation rather than left for the next lane to rediscover: a label may not be
re-answered, because runner_label_resolution owns it; a runner NAME is a different
vocabulary with no existing authority, and that is the part worth rebuilding.

This removes the occupancy model, so it also removes this lane's only modelled
path for the job-census figures. That is the correct order: the census is built on
the label authority or not at all.

Evidence: required-ci witnesses lane on srv1 -- parse, declarations and the
touched-subject compile green with both modules removed and the visibility
consolidation in, no dangling reference to either module left in the tree. The two
local-repo-wet refusals are environment-specific to this srv1 invocation; CI
passed them end to end at e249b97.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Three annotations named drive_token_env_matches_the_configured_literal,
sheets_token_env_matches_the_configured_literal and
app_property_key_matches_the_created_property as what stops a declaration and a
transport literal drifting apart. They do not. Each compares the DECLARATION to a
THIRD copy of the string written inside the claim, and none reads the auth_source
literal in the service config or the appProperties literal in the create body.
Editing the transport literal alone -- the exact drift the annotations describe --
leaves all three green.

The distinction that makes this worth a row rather than a correction: these are
not decorations in the DESIGN section 4b sense, because they CAN go red. Edit the
data row and they fail. A reviewer asking "does this check have an authorable
red" finds one and stops. The red they have is not the red they were cited for,
so the question that separates them is not whether the check can fail but whether
it can fail FOR THE STATED CAUSE. The annotations are corrected to say what the
claims establish -- that the row did not move without the claim moving with it --
and to say what they cannot reach. Section 4c is the governing rule and it was
broken three times in one change: an annotation is never evidence that a machine
claim holds.

The real wall is construction, not a better claim. The duplicate exists only
because the config parse reads auth_source through extract_string_value, which
pulls a literal rather than evaluating a reference; a parse that resolved a
declaration reference would leave one spelling and nothing to drift from. No
claim over the current shape can exceed rung 2, because no fold in this corpus
can read a service config's literals. That capability is the next-rung trigger.

The class is filed as gunbc.recurring_failure_mode
a_pin_claim_compares_two_copies_while_a_third_drifts, with the discriminator that
makes it checkable: a subject appearing three times -- declaration, unread
literal, and the claim's own copy -- where the assertion joins the two that a
single edit moves together. The sound sibling sits in the same file and is named
in the row: drive_and_sheets_read_one_credential compares two DECLARATIONS with
no third copy between them, and is the stronger claim precisely because of it.
Only the row file is committed; roster.dag and docs/design-failure-modes.md are
gitignored generated artifacts, and membership is the directory.

Evidence: required-ci witnesses lane on srv1 -- parse, declarations and the
touched-subject compile green; the docs projection actuator regenerates clean
with the new row enrolled (REGEN_EXIT=0), which is what establishes the row
typechecks and the roster resolves it. The two local-repo-wet refusals are
environment-specific to this srv1 invocation; CI passed them at e249b97.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…en discarded

read_service_enablement matched all four non-succeeding REST classifications and
folded every one into ServiceEnablementUnobserved { project, service_id }, binding
status, body, cause and detail to _. The operator saw "serviceusage GetService is
unobserved for <id>; an unread state is not a disabled one" and nothing else, so a
403 where the writer lacks serviceusage.services.get, a host that was never
reached, and a body this model could not decode were indistinguishable -- three
states needing three different human actions, behind one sentence. DESIGN section
5 requires a typed, LOCATED diagnostic, and located means located where the reader
can act: the classification was performed and then thrown away one line later.

The pattern was already correct fifteen lines above. read_project, in this same
module, carries each cause into ProjectUnreadable { reason }. That is what makes
this a defect rather than a gap -- the module had the convention and one fold did
not follow it.

ServiceEnablementUnobserved now carries cause: NonEmptyStr, and each arm says
which of the four it was, including the commit-ambiguity arm that should not arise
on a read exchange and says so if it does. All sixteen sites are updated. The one
in gunbc.review_sheet_operator is not a REST failure at all and reads better for
having to say so out loud: the home was selected from the estate, no serviceusage
read has ever been performed against it, and "unobserved" there means never looked
rather than looked and failed. gcp_service_enablement carries the rationale on the
arm, since it is the arm's shape that was wrong rather than any one caller.

Method note, because the last several rounds turned on it: every sibling reader in
the module was checked for the same collapse before fixing this one (only this
fold had it), and the sixteen construction sites were verified by brace-matching
each literal rather than by a line grep, which had already given one false
negative on multi-line constructions.

Evidence: required-ci witnesses lane on srv1 -- parse, declarations and the
touched-subject compile green with the widened arm, no construction left missing
the field and no match site left non-exhaustive. The two local-repo-wet refusals
are environment-specific to this srv1 invocation; CI passed them at e249b97.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… fix missed

Review 67242 found three annotations citing pin claims as coverage for a red they
cannot produce. The fix corrected three sites and left three: the claim comments
in review_sheet_drive_converge_witness, CreateFile's citation in
extdeps.google.drive, and the module header of review_sheet_transport_pin_witness.
All three still advertised the tie. So this is the same defect, uncorrected, in
the commit that rostered it as a failure mode -- and the rostered row prescribes
the census that would have caught it: count the copies of the value.

That makes three rounds in this PR where the named sites were fixed and the class
was not: one non-exhaustive match of four, nine frontier declarations of sixteen,
and now three annotations of six. The census here was every citation of the three
claim names, not the lines the review quoted.

What the claims reach is now stated at each site, and the pin-witness header
separates the two kinds rather than calling them all a tie:
sheets_token_env_matches_the_configured_literal joins a declaration to a copy
inside the claim and goes green if the transport literal moves alone;
drive_and_sheets_read_one_credential compares two DECLARATIONS with no third copy
and is a real cross-module tie; search_query_carries_the_declared_property_key
reads the query BUILT from the declaration and ties it to the search for real.
CreateFile now says outright that nothing pins its body literal to
review_sheet_app_property_key, and names the search-side claim as the contrast.

The receipts stay beside the claims that could not have caught them, deliberately.
The first live run failed on exactly this property-name mismatch, and a claim cited
as catching that, which cannot, is worse than no claim -- which is the sentence
DESIGN section 4b already carries and this PR already quotes.

Annotation-only: no type, fold or claim body changed, so no verdict should move.

Evidence: required-ci witnesses lane on srv1 -- parse, declarations and the
touched-subject compile green, phases_failed unchanged at the two local-repo-wet
refusals that are environment-specific to this srv1 invocation and that CI passed
at e249b97. Two further "pinned by" citations exist outside this PR's diff, in
test.claim.frame_boundary_witness_test and gunbc.cli_run_repo_grant; they are not
touched here and are flagged rather than widened into this change.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… String

attempt_filter took a String defaulted to "latest" and passed it to the wire, so
"Latest", "all " and "" were all writable and all reached GitHub, where a rejected
or silently ignored filter changes which attempts a capacity census counts -- the
consumer this operation's own annotation names. DESIGN section 4b rung 4: the
invalid state should have no constructor.

The first fix here was a hand-written wire fold, which would have been wrong twice.
This corpus already models coproduct-to-wire as data: std.serialization
CoproductWireContract, which extdeps.github.workflow_runs_contracts already uses
for WorkflowRunStatus and WorkflowRunConclusion. A hand fold would have been a
second authority for one encoding AND dangling, since the transport derives the
wire form from the contract -- the fork-plus-dangling pair that got two modules
held out of this PR already.

So: a two-variant coproduct, and the spelling comes from a contract.
StripPrefixAndSnakeCase { prefix: "Attempts" } lets the variants be AttemptsLatest
and AttemptsAll -- readable, and not the bare Latest and All that would be among
the most collidable names in a tree resolving bare references -- while emitting
exactly the latest and all the endpoint documents.

The class was censused across the whole diff rather than fixed at the named line.
Every other String in an operation input is genuinely open (owner, repo, run_id),
and the Strings in DrivePermission are response-side wire fields that already
decode through a refusal arm. attempt_filter was the only offender.

Evidence: required-ci witnesses lane on srv1 -- parse, declarations and the
touched-subject compile green; phases_failed unchanged at the two local-repo-wet
refusals that are environment-specific to this srv1 invocation and that CI passed
at e249b97.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls added this pull request to the merge queue Sep 17, 2026

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

HOLD — reviewed exact head a765573983a4df4f428dd0c0d18cb2f908357540.

GitHub will not permit this account to submit REQUEST_CHANGES on its own PR, but I do not consider this head safe to merge. Four correctness gaps remain:

  1. The recurring sheet identity is not bound to the declared writer or even to one OAuth application. review_sheet_drive_converge says membership runs under a bootstrap credential and later converges run as the writer, but converge_drive_half invokes membership and spreadsheet convergence in one call while every Drive/Sheets operation reads the same untyped GUNBC_REVIEW_SHEET_TOKEN. Nothing observes the token principal or OAuth client. This matters because Drive appProperties are private to the requesting app/OAuth client: a sheet created under an operator/Cloud-SDK token can be invisible to a later service-account client, causing SheetAbsent and a duplicate create. The demonstrated second-run Noop used the same credential and does not establish the intended bootstrap→writer transition. Split the bootstrap and recurring routes (or their auth sources), bind the recurring credential to the selected writer and stable app identity, and wet-test create/adopt using the actual recurring writer credential.

  2. The new typed frontier groups are not enrolled in the frontier census. review_sheet_whole_estate_consumer_frontier_rows, sheets_bootstrap_project_consumer_frontier_rows, and actions_allowance_consumer_frontier_rows are absent from gunbc.census_closure_frontier. Their comments say the typed rows make the gaps visible to consumption/dissolution checks, but the sole roster those checks fold cannot reach them. Enroll all three groups and add a closure witness so this cannot recur.

  3. The billing surface re-collapses two materially different states. actions_usage_billable_verdict maps both ChargedAgainstPlanQuota and AlwaysChargedPerMinute to BillingConfirmed { billable: true }, while the frontier prose says this separates a payer from a free-tier user. Private standard usage can be fully covered by included quota; no plan balance or exhaustion observation is supplied. Separately, allowance_applicability(sku) returns AllowanceApplies for every standard SKU even though public-standard usage never touches the allowance; visibility is not an input. Preserve the ConsumesPlanAllowance versus AlwaysCharged distinction through the consumer, and make allowance applicability visibility-aware. Positive spend still requires account allowance standing.

  4. converge_sheet_values accepts column-major ValueRange but silently compares and writes it as rows. compare_value_ranges ignores majorDimension, and value_range_for_write hard-codes ROWS. A COLUMNS desired value can therefore be reported equal to a row-major readback or be written with changed semantics. Narrow the actuator to a row-major carrier, or explicitly decode/refuse/transpose DimensionColumns before comparison and write.

The current witnesses run is green, but none of these four boundaries is exercised by it. Please remove this head from the merge queue until they are closed.

… duplicate

P0. The spreadsheet's identity was an appProperties value, and extdeps.google.drive
said in its own annotation that appProperties is PRIVATE to the calling
application -- then the converge was built so that its create and its search were
always going to run under DIFFERENT OAuth clients: the bootstrap under an
operator's Cloud SDK credential, the recurrence under review-sheet-writer@. A
property private to the creating app is invisible to the searching app, so the
first run as the writer would have searched, found nothing, and created a SECOND
spreadsheet -- the exact duplicate this converge exists to make impossible. The
live no-op that looked like proof used one credential for both halves, so it could
not have caught it, and no witness over a mock corpus ever could.

The repair removes the hazard rather than adding an identity obligation nothing
here can check: Drive `properties` are visible to any application with access to
the file, so the marker survives the credential transition that is the entire
point of the writer account. The trade is stated on the carrier -- another app can
see and in principle write the key, so it is namespaced, and a collision surfaces
as SheetDuplicated, which is already a refusal rather than a silent adoption.

P1. Three frontier groups added by this PR were not enrolled in
gunbc.census_closure_frontier, so the dissolution census could not see them. A
declared frontier that nothing can count is the defect it was meant to declare.
All three are now in census_closure_frontier_row_groups().

P1. The billing model collapsed "uses allowance" into "payer", twice.
actions_usage_billable_verdict mapped ChargedAgainstPlanQuota to billable: true
while allowance_applicability answered AllowanceApplies for the same SKU -- one
module, two answers. Inside GitHub Free's 2,000 or Team's 3,000 included minutes a
private standard job costs its owner nothing, so the old fold would have ranked
every private repository as a payer, which is precisely the false positive a spend
census must not produce. It now answers BillingDependsOnConsumedAllowance and
names the account fact this repo does not observe. Separately
allowance_applicability took no visibility and answered AllowanceApplies for
public standard usage, which never touches the private allowance at all; it is
visibility-aware now, with AllowanceNeverMetered for that case.

P1. The values actuator read ValueRange.values as rows without consulting
majorDimension and hard-coded "ROWS" on write, so a COLUMNS-major range would have
compared a transposition and then written it back with changed semantics. There is
a typed reading now that refuses COLUMNS, and absent correctly means ROWS -- the
same proto3 omission that hides a zero colour channel.

Also in this change: the format actuator returns with its colours DERIVED rather
than transcribed, and with a readback. std.coercion enrols Int -> Float and
std.integer derives the 8-bit maximum, so (158 as Float) / (uint8_max as Float) is
computed here and the earlier claim that the corpus could not do it was false. A
colour that cannot be derived is a reading that refuses, never a default.
spreadsheets.get is modelled with a field mask and one range, so the converge can
ADOPT instead of re-applying -- which is what stops conditional rules accumulating
on every pass -- and colours compare at half an 8-bit step because std.algebra
declares Float an ApproximateFieldProfile carrier and exact equality would rewrite
the sheet forever. The module's Scaffold is deleted because the consumer landed:
converge_drive_half_cli formats the spreadsheet its own converge just verified.

A caveat on evidence. The srv1 floor reports namespace-wave-admission with 26
unadjudicated deltas, and that is an artifact of a stale base rather than a
finding: this worktree is a shallow clone, its computed base is c48a6be (the
#11403 merge), while CI's run against the true merge base 3774101 evaluated the
same phase and answered ADMITTED with phases_failed=0. Authoring admissions
against a base known to be wrong would mint exactly the stale rows that refuse
every PR's floor, so the phase is left for CI to adjudicate. Parse, declarations
and the touched-subject compile are green on srv1; the two local-repo-wet refusals
are the environment-specific pair CI passes.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot
gunbai-bot Bot removed this pull request from the merge queue due to a manual request Sep 17, 2026
Brian Searls and others added 5 commits September 17, 2026 19:08
…, and a validator never re-derived

Two findings, both real.

The identity key still carried the rationale for the bug the previous commit
removed. gunbc.review_sheet_drive_converge said the marker "is private to this
application (Drive scopes properties per-app), so it may be declared once and
trusted: another application cannot read or collide with it" -- which is exactly
why the earlier design searched under a credential that could not see its own
marker. The rename to `properties` moved the identifiers and the wire spelling and
left the reasoning behind, so the row that OWNS search identity still told the next
reader the superseded story. That is DESIGN section 3's meaning fork: one name, two
materially different obligations. The annotation now says what the key may still be
trusted for -- stable, chosen before the call, so a converge can ask for it again --
and what it may not: exclusivity. Another application can read and write it, which
is why two files carrying it has to be a representable state, and SheetDuplicated
is that state.

Worth recording how this survived: after the rename I swept for stale SYMBOL names
and found none, because the symbols had all moved together. I did not sweep for
stale REASONING, and prose does not fail to resolve.

The second finding is a live defect rather than prose.
admit_identified_spreadsheet_share built its expectation as
spreadsheet_share_intervention -- the My Drive route where an operator shares one
FILE -- while the entry supplies shared_drive_member_intervention for the live
residency. The two identities can never be equal, so an identified spreadsheet in a
shared drive would have refused forever. Residency routing was added at the entry
and the validator was never re-derived for it. It is invisible today only because
the live residency is still SpreadsheetAwaitingCreation; the create intervention's
own next step walks into it, so the first successful create would have produced a
permanent ReviewSheetOperatorRefused.

The repair is single authority rather than a second branch: the validator asks
review_sheet_access_intervention what to expect, which is the same function the
entry asks what to offer, so a residency added later changes both sides at once.
That required threading residency from the entry through
admit_review_sheet_operator and admit_review_sheet_after_enablement_ready, and the
fail-closed substrate then named every consumer that had to change -- a second
call site in the Workspace-domain branch and thirteen witness call sites, none of
which I would have found by reading.

Evidence: required-ci witnesses lane on srv1 -- parse, declarations,
namespace-wave-admission and the touched-subject compile all green, no call-shape
mismatch left. The two local-repo-wet refusals are the environment-specific pair
this session's srv1 invocation always shows and CI passes.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…without evidence

Review 67324: the format actuator authored `review_sheet_column_count: Int = 17`
and `standing_column_index: Int = 3` as bare literals, while
gunbc.review_sheet_projection already owns what a review sheet's columns are. Two
sources for "how wide is this sheet" and "which column is Standing", and the drift
would have been silent -- format_is_converged checks frozen rows, header colours
and a rule count, never extent or column position. One added derived column would
have left the header band stopping short and the conditional rule painting a
column that is no longer Standing, with every call answering success and the
converge still reporting converged.

Both are derived from a supplied ReviewSheetSchema now: the extent is a fold over
the roster, and the standing column is found by its ListingStanding KIND rather
than a position, so it survives the roster growing. A schema carrying no standing
column refuses instead of colouring index 3 and hoping.

The schema itself is declared once, in the module that owns review-sheet schemas,
and read back from the header row the live sheet actually carries: fifteen derived
columns plus Decision and Note, seventeen in total, Standing at index three --
matching the sheet the 2026-09-16 write produced. Two things in it are load-bearing
beyond this finding. Decision and Note carry the OperatorEntered kind, which is the
machine-readable form of the erasure hazard raised against the whole-range write
path: a consumer can now FIND the operator's columns rather than a human
remembering which they are. And the identity column is Repository, not Rank,
because rank changes on every re-rank and keying rows on it would make every row a
new row on each pass and destroy exactly those cells.

CI then failed four witnesses, correctly, and the cause was mine. Threading
residency through the admission path, I inserted the live shared-drive value at
every call site -- including twelve witnesses whose fixtures are the My Drive
file-share story. They asserted one residency while supplying another's evidence.
Each now names the residency it actually exercises.

That exposed the more useful gap: EVERY witness in that file passed a My Drive
fixture, so every one of them agreed with the broken validator, and the defect
review 67297 found had no discriminating red anywhere. Two claims land with this
change -- a discharged file share under a shared-drive residency must not admit,
and a discharged drive membership under the same residency must. The second is the
positive control that stops the first being satisfied by a validator that refuses
everything, which is the absorbing-fallback shape section 5 names.

Evidence: required-ci witnesses lane on srv1 green apart from the two
local-repo-wet refusals that are environment-specific to this session and that CI
passes; all four claims above PASS by execution under claim_batch, including the
two that were red.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…le state crossing raw

Two findings. The review also retracted an earlier flag against ValueRangeWrite's
majorDimension after checking that its sole construction site routes through the
typed fold; nothing to undo there.

extdeps.google.drive DrivePermission.type was decoded by nothing and read by
nothing. drive_principal_type_wire existed for the write side and
drive_principal_type_from_wire did not exist at all, so the membership fold matched
rows on EMAIL alone. That is not an unconsumed field, it is a safety gap: Drive
permissions of type domain and anyone carry a role exactly as a user grant does, so
a role-satisfying `anyone` row would have read as the writer being a member and
this converge would have reported a world-writable drive as converged. The decoder
lands, and a row names the writer only when it is a USER grant to that address. An
unrecognised type does not match and is not silently dropped -- membership answers
Absent only when no row matched, and a principal type this model cannot read is a
row it must not claim to have understood.

The GCP project lifecycle state crossed into gunbc.sheets_bootstrap_converge as a
raw String, compared against one literal "ACTIVE", with every other spelling
carried forward verbatim in ProjectObservedOtherState. DELETE_REQUESTED,
STATE_UNSPECIFIED and a value this model has never seen were one arm. The module
already carried the right pattern 140 lines later: gcp_service_enablement folds the
serviceusage state through extdeps' own closed sum. GcpProjectLifecycleState is now
that shape for projects, declared in the module that owns Resource Manager, and the
consumer folds through it.

ProjectStateUnreadable is its own arm rather than a third "other state", because a
value the upstream does not publish is not a lifecycle fact -- it is a response this
model could not read, and which of the two it is decides whether an operator goes
looking at the project or at the model. A claim lands with it, and the
gcp_project_state_active literal is now referenced nowhere: the value is derived
from the upstream fold instead of authored beside it.

Evidence: required-ci witnesses lane on srv1 green apart from the two
local-repo-wet refusals that are environment-specific to this session and that CI
passes; the three project-state claims PASS by execution under claim_batch,
including the new one.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…n and denied it

The previous commit closed a real gap -- a role-satisfying `anyone` permission read
as the writer being a member, so a world-writable drive would have reported as
converged -- and opened another one in the same fold. An unreadable principal type
answered false from permission_names_writer, which filtered the row out BEFORE any
role decode. A row carrying the writer's own address under a type this model cannot
read therefore left the matched set empty, the observation answered
MembershipAbsent, and Absent under EnsureMayApply is Apply: a create against a
principal that may already hold access. The sibling role path refuses exactly that
shape one fold below.

The annotation asserted the opposite in the same breath -- "it is also not silently
dropped" -- while dropping it from the filter is precisely a silent drop. That is
the third time in this lane's work that prose has claimed what the code does not
do, and it is the reason the claim below exists rather than a sentence.

A row is classified rather than filtered, because there are three facts and a Bool
holds two. RowNamesWriter, RowNamesWriterUnderUnreadableType and RowIsNotWriter
separate the case that matters: an unreadable type on a row that does NOT name the
writer is not about this membership and is skipped, while an unreadable type on a
row that DOES name it makes the whole observation unreadable.

Two claims land, and the control is not optional. The first is the discriminating
red for the fail-open. The second establishes that an exotic permission belonging
to someone ELSE does not poison the read -- without it, "refuse when confused"
would make any drive carrying one unusual permission permanently unconvergeable,
which is refusing-everything wearing a safety argument.

Evidence: required-ci witnesses lane on srv1 green apart from the two
local-repo-wet refusals that are environment-specific to this session and that CI
passes; all three membership claims PASS by execution under claim_batch, including
both new ones.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Rewriting committed_project_and_writer_are_unresolved_not_secrets_defaults for the
estate's move to a SELECTED home also deleted four independent conjuncts that had
nothing to do with that move. Their subjects did not change, so DESIGN section
4b(4) applies exactly: a climb deletes the production machinery it obsoletes and
the evidence stays enrolled. Nothing climbed here. The dangling imports left behind
were the tell -- buyer_review_workspace_sharing_reading and buyer_review_spreadsheet
appeared in the import list and nowhere else.

They return as four tests rather than one conjunction, which is the split the
witness-standing rule wants anyway: a conjunction forces every case through one
budget and reports "one of four failed" when each guards a different subject.

Two corrections to the finding as filed, both verified.

It is four, not five. The WIF intervention's NoDischargeSiteModeled standing is
already covered by fleet_secrets_wif_binding_is_still_undischarged, with a control,
so restoring it would have been a second copy of one fact rather than recovered
coverage.

And the live-access conjunct could not be restored as written. It asserted
ReviewSheetEstateUnresolved with subject sheets_calling_home -- true while the home
was unresolved and FALSE now, because selecting the home is the point of the
change. Restoring it verbatim would have asserted something untrue. The property
the wall establishes is unchanged and is what the replacement asserts: the
zero-argument entry, which reads the FLEET standing rather than a supplied
admission, does not open live access -- it now stops one step later, at a
serviceusage state nobody has observed. The sibling test drives the same fold from
an ADMITTED admission, so the open and closed directions are both executed.

Evidence: required-ci witnesses lane on srv1 green apart from the two
local-repo-wet refusals that are environment-specific to this session and that CI
passes; all four re-enrolled claims PASS by execution under claim_batch.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls added this pull request to the merge queue Sep 18, 2026
Merged via the queue into main with commit 568850f Sep 18, 2026
4 checks passed
@briansrls
briansrls deleted the session/zesty-crane-846 branch September 18, 2026 02:42
@gunbai-bot gunbai-bot Bot mentioned this pull request Sep 18, 2026
6 tasks
@briansrls
briansrls restored the session/zesty-crane-846 branch September 18, 2026 02:57
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