Review-sheet located-tab authority: a sealed TabLocated, and the formatter on it

[briansrls]

Summary

File identity does not establish tab identity. converge_review_spreadsheet finds or creates the Drive file by a marker property and returns a file_id. Nothing located which tab inside it is the review tab, so converge_review_sheet_format addressed a first-sheet constant of 0 on all seven of its batchUpdate steps, and its readback took the head of the sheet list — the same assumption on the read side, which would make a "verified" readback evidence about a tab nobody wrote to.

gunbc.review_sheet_tab_locator observes spreadsheets.get sheet properties and answers TabLocated { tab } | TabAbsent | TabAmbiguous { candidates } | TabUnreadable { cause }.

The admission rule is exactly-one, cited rather than defaulted. The only creator of this file is drive.Files.CreateFile with the Sheets MIME type, which mints a one-tab workbook — so a second tab is not a state this pipeline produces. It is a state a person produced in a browser, and a person who added a tab is the only one who can say which tab the review is now in. Two or more is TabAmbiguous carrying every candidate; "take the first" is the assumption being removed, not a weaker version of it.

Why not the named-tab rule. It is the stronger rule and the one this lane should end at. It needed two things the corpus lacked, and one arrived mid-review: the A1 title codec (gunbc#11703) landed as a1_range_encode, so this branch's own a1_tab_qualification was deleted by its stated dissolution trigger rather than left beside its replacement. What remains is the write half — batchUpdate addSheet, which extdeps.google.sheets does not model at all — so the trigger for revisiting is now singular and checkable. Exactly-one is not a substitute for that convergence; it is its observation half, which a named converge needs anyway to read its own write back (DESIGN §3d).

The title is never inferred from the Drive file's display name. Different authors, different storage, no upstream relation. The module does not import the one that holds the file name, so the inference is unavailable rather than declined.

Confinement, and how it got there

Two side-chat holds found the same class at two layers, both defects of mine. The repair in each case was to confine the input by construction rather than seal the callers by list, because an admission list leaves correctness depending on that list staying complete.

The carrier. I claimed "both routes to the mint are sealed" after sealing two functions. Confinement is a property of every exported path that can return the value — there were six, and three were open, including review_tab_located_from, which built the record literal with no admission at all. The probe passed throughout because it only tried the doors I already knew about.

Repair: the folds return ReviewTabClassification, which is freely constructible and authorizes nothing. Exactly one sealed conversion turns ClassifiedExactlyOne into a LocatedReviewTab. A wrapper added later must call it and is refused. This also deleted eight witness admissions that were themselves routes — the classification is pure, so the witnesses assert the same payloads without being admitted to anything.

The effects. I introduced the request records so the addressing would be a value a claim could read. That improved the evidence and opened a bypass: the records were ordinary and the five network functions taking them were unrestricted, so any module could format an arbitrary tab of an arbitrary workbook with no located tab, no validated schema, no converge.

Repair: all four records are sole_constructor, minted only by the three builders, each requiring a LocatedReviewTab. The effect functions need no admission list — an unconstructible argument cannot reach them by any route, named or unnamed.

Surviving return paths, enumerated from source: the sealed conversion, its sealed caller, located_tab_for_witness sealed to its four exact consumers, and locate_review_tab — deliberately open, because performing the read is what earns the carrier.

Also in this diff

• extdeps.google.sheets: SheetsSheetPropertiesRead gains title and index; sheets_sheet_id_read / sheets_sheet_index_read are the single home for the proto3 absent-is-zero rule. An absent title deliberately does not get that treatment — its default is "", which upstream never produces.
• Mask/decode single authority. Field paths are named rows and all three masks compose from the same row the decode keys on, so widening the reading and widening the request are one edit.
• The formatter composes with gunbc#11705's ValidatedHeaderSchema: a validated schema says what to write, a located tab says where, and it now requires both.
• spreadsheet_first_sheet_id deleted with its last consumer; four prose citations repointed.

What the formatter verifies, at its actual strength

FormatAppliedAndVerified means three facts read back off the located tab: frozen row count exactly, header background and foreground at swatch width, and the number of conditional rules. It does not compare each rule's condition or colour, does not check the header band's extent or the standing column's position, and reads userEnteredFormat — what this repository wrote, not what a viewer sees.

Test plan

Run in-session (real 31 GiB cgroup; the BuildBuddy runner OOM-kills at rc=137 on a false declared budget). Exit statuses read unpiped.

./target/release/claim_batch --source-root dag --source-root src/v2 --entry <file> --functions <all>

file	result
review_sheet_tab_locator_witness_test.dag	RC=0, 9/9
review_sheet_format_target_witness_test.dag	RC=0, 10/10
review_sheet_tab_refusal_probe_witness_test.dag	RC=0, 10/10

29/29 claims. 20 mutations applied and reddening, with the applied-count checked against the expected total on every run.

Two clean diagonals — M7/M8/M14/M15 (carrier seals) and M17–M20 (record seals) each redden exactly their own claim and nothing else. That is what rules out eight seal claims resting on fewer than eight walls.

CI proves the compiler builds and nothing else. Since gunbc#11742 the witnesses check is one hosted job running cargo build --release -p v1-compiler --bin gunbc; it executes none of these claims. The local runs above and the mutation table are the discriminating evidence.

Declared limits

• The formatter claim reads the request plan, not the wire. It discriminates a plan built from the constant; it would not discriminate a step rewritten to ignore its request. Trigger: the three batchUpdate operations absent from sheets_mock_corpus.
• LocatedReviewTab.spreadsheet_id is this process's own argument, not read back from the response. Cross-checking needs the field mask to widen, which costs every caller of that operation. Next-rung trigger, recorded in the module.
• read_format_at takes a range beside the located tab, so a holder of a genuine tab may read any range within that spreadsheet. Subject confined; read, not mutation.
• The seal is evidenced on source→v1 interpretation. The native v2 path consumes sole_constructor without minting the construction property — the standing corpus-wide drop g0_type_decl_modifier_parse_without_sealing_property, named rather than elided, per §4b(1)'s minimum-across-paths rule.
• The probe does not separately call color_standing_derived — harmless, since it requires the same sealed StandingRuleRequest and has no alternate coordinate input. Noted for a follow-up.

What this PR cost, recorded because it is the useful part

Five findings across three REQUEST_CHANGES rounds and two side-chat holds. Every one lived in a join between two things, not inside either. Mask ↔ decode. Predicate ↔ the authority declared for it ten lines away. Present-id claims ↔ the omitted-id arm the pipeline actually hits. Sealed functions ↔ the full set of return paths. A confined carrier ↔ the unconfined records reaching the same effects.

The sharpest: review 68553 found that converge_review_sheet_format refused every workbook, and 18 green claims, 8 reddening mutations and a then-real required floor all passed over it — because every claim read the request plan and nothing executed the seam beside it. That recognition rule is filed as a second specimen on gunbc.recurring_failure_mode.readback_scoped_to_exclude_the_effect_it_verifies: when a claim set is built around one layer, the defect it cannot see is the join to the layer beside it.

Two harness lessons, both caught by counting rather than reading a verdict: a mutation runner silently applied 11 of 13 while printing success, and M2 kept passing while quietly becoming evidence for a different claim after a refactor. Anchor rot fails loudly; evidence relocation does not.

🤖 Generated with Claude Code

[gunbai-bot]

Both findings in review 68522 were right, and both are fixed by deletion rather than justification. Head is now a1e7d114f0.

review_tab_is_located — deleted. Confirmed dangling exactly as described: format_located_tab matches ReviewTabStanding directly, so the only callers were the three inside one claim. The function, that claim (only_the_located_arm_reports_located) and its admit_callers row are gone together — a dangling production function should cost the claim that was its only caller, and keeping the claim while deleting the function would have been the same defect wearing a test's clothes. That also resolves the secondary is_*-over-a-coproduct point without needing to weigh it separately.

format_plan_sheet_ids — moved into the witness. You were right that the weaker form of the question still applies. FormatRequestPlan's fields are readable from the witness, so the claim now folds the record production really builds, and the actuator declares nothing that exists only for a test to read. The claim it serves is unchanged and still reddens when the plan is built from spreadsheet_first_sheet_id.

Two things done alongside, both because the branch had to take a main merge (it predated heal_candidate.dag from #11547, which is what the heal-generated-artifacts failure was — not this diff):

• All 18 claims and all 8 mutations were re-run after the deletions and after the merge. A mutation table that passed before a 10-commit merge is not evidence about the tree being pushed. 18/18 green, 8/8 mutations still redden their named claim.
• Rung honesty. The merge brought in gunbc.rung_drop.g0_type_decl_modifier_parse_without_sealing_property — the native v2 path consumes sole_constructor without minting the construction property. The probe evidence here runs on the v1 seed, where the wall is real, so the module now names that standing corpus-wide drop. DESIGN §4b(1) takes a class's rung as the minimum across its in-scope paths, and without the note the seal would have read stronger than it is.

Thanks for the note on the sealed carrier and the forged-source probe — the reason both are there is that a hand-built LocatedReviewTab { sheet_id: 0 } is the constant this PR removes, wearing the name of an observation.

[gunbai-bot]

Review 68553 is correct in full, and it found a hard production break that I introduced. Head is now 7727a727fd.

Confirmed exactly as described. When the readback stopped taking the head of the sheet list and started selecting by the located sheetId, I left both masks alone, so the selector keyed on a field the request had suppressed:

• grid mask carried no properties at all → sheet_read_has_id took its Absent => false arm for every sheet → located_sheet returned none → header_format_of answered HeaderFormatUnreadable unconditionally → converge_review_sheet_format refused every workbook, not just non-zero ones.
• metadata mask carried properties without the id → absent-is-zero matched only when the located tab was tab zero, which is the assumption this branch exists to remove, reintroduced where nothing was looking.

You also identified why my evidence was blind to it, and that is the more useful half of the finding: every formatter claim read the request PLAN, and the defect sat between the request MASK and the DECODE — a seam no claim executed. Eighteen green claims and eight reddening mutations passed straight through a break that made the production path unconditionally refuse. And the module's own prose stated the rule it was violating, which is worth recording as its own lesson: prose adjacent to a defect does not prevent it, because no Accepted program reads a comment.

The repair is not the two strings. Patching the literals would have left the actual fault: a mask and a decode are two representations of one fact — which fields this read needs — with nothing joining them, which is precisely what let widening the reading and widening the request come apart. The field paths are now rows in extdeps.google.sheets (sheets_field_sheet_id and friends) and all three masks compose from them, so the path the decode keys on and the path the request asks for are one declaration. The locator's mask, which happened to be correct, is composed the same way rather than left as the odd one out.

New evidence at the seam that had none, each confirmed to redden by a mutation run rather than asserted:

mutation	claim reddened
M9 — grid mask narrowed back to its old spelling	both_readback_masks_request_the_sheet_id_the_selector_keys_on
M10 — metadata mask narrowed back	same claim
M11 — sheet_with_id takes the first sheet regardless of id	the_readback_selects_the_sheet_carrying_the_located_id_not_the_first_one and a_response_with_no_properties_locates_no_sheet_rather_than_defaulting_to_the_first

M11 is the pre-change behaviour of that fold, so its double red is the check that the selector's repair is load-bearing at all. Full re-verification on the pushed head is running; I will post the counts when it lands.

[gunbai-bot]

Both findings in review 68663 are correct and fixed. Head is now 6db37b50bd.

1. sheet_read_has_id re-expressed the absent-is-zero rule. Right, and the placement makes it worse than a generic §3 fork: it sat about ten lines from the mask repair, in the same branch that had just written the join-the-two-ends argument into readback_scoped_to_exclude_the_effect_it_verifies as a general lesson. Writing the rule down did not make me apply it, which is its own small receipt for why construction beats a documented discipline. The predicate now reads sheets_sheet_id_read(id: props.sheetId) == sheet_id. Absent properties deliberately stays a separate false — a sheet whose properties were never read is not a sheet whose sheetId was omitted, and only the second is a zero.

2. spreadsheet_first_sheet_id was dangling. Confirmed: after this branch removed its last production consumer, git grep returned only the control claim asserting the witness id differs from it, plus prose. That is the §3c shape this branch applied to itself two commits earlier for format_plan_sheet_ids, so it goes the same way. The control compares against the literal 0 with unchanged discriminating power — zero is precisely what the removed assumption yielded. I also repointed the four prose citations that named the deleted symbol; a citation that no longer resolves is the decay §3's cite-the-symbol rule exists to prevent, and leaving four behind would have made the deletion half-done.

A gap neither review raised, found by writing the mutation for finding 1. M12 restates the fork inline as Absent => false — and nothing reddened. Every formatter id I had asserted was explicitly present and non-zero, chosen so a lingering first-sheet assumption could not pass by coincidence, and that choice left the ordinary case uncovered: converge_review_spreadsheet mints a one-tab workbook whose only tab is sheetId 0, and Sheets omits a field equal to its proto3 default, so nearly every real response carries properties with no sheetId at all. The production path runs that arm constantly and no claim touched it.

Two claims now pin it from both sides, each confirmed by a mutation:

mutation	claim reddened
M12 — absent id → false	a_tab_zero_workbook_whose_response_omits_the_sheet_id_is_still_located
M13 — absent id → true (wildcard)	an_omitted_sheet_id_does_not_match_a_non_zero_located_tab

M13 is the one that matters for durability: a single "an omitted id is still located" claim is satisfiable by making the absent arm match anything, which would reinstate take-the-first for every tab — the defect this branch exists to remove, arriving through the fix for a coverage gap.

Current state at this head: 23/23 claims green, 13/13 mutations redden their named claim. This is the third review to find that my claims cluster where my attention was and miss the join beside it, so I have recorded that recognition rule on the failure-mode row rather than only fixing the instance.

[briansrls]

SOURCE HOLD — exact head 29908a583dd6fa4eef1adfbe2f7a76b0ddd2c406

GitHub would not accept a formal REQUEST_CHANGES because the connected identity is also the PR author.

The located-tab decomposition and the mask/decode repair are correct in source. The locator mask is built from the exact ID/title/index field rows its candidate decoder reads. The formatter grid mask requests sheetId + userEnteredFormat; the metadata mask requests sheetId + frozenRowCount + conditionalFormats; both readbacks select by the located id, and the omitted-zero arm goes through sheets_sheet_id_read. I am also treating the required check only as a compiler build after #11742, not as claim execution.

One structural hold remains: the sealed carrier has several unrestricted alternate mints/egress paths.

review_tab_located_from(spreadsheet_id, candidates) directly constructs LocatedReviewTab, accepts an ordinary caller-authored List<ReviewTabCandidate>, returns ReviewTabStanding, and has no admit_callers. review_tab_standing_of_candidates and review_tab_standing_of_scan are likewise unrestricted exported wrappers returning that carrier. A foreign module can import any of them, supply one authored candidate, obtain TabLocated, and pass the tab to the formatter without calling either sealed function or performing any read.

There is a second escape in evidence: test.claim.review_sheet_format_target_witness::located_tab_for_witness(sheet_id, title) is an admitted caller of review_tab_standing_from_read, takes ordinary authored coordinates, and returns ReviewTabStanding without its own caller boundary. Any module can import that witness helper and obtain the confined value. This is exactly the rostered admitted_call_edge_with_unrestricted_value_egress class: sealing the direct edge does not close an exported wrapper that returns the sealed value.

The current forged probe tests only the record literal, review_tab_standing_from_read, and review_tab_standing_of_outcome, so all five probe claims can stay green while these routes compile.

Required closure:

1. Preferably keep the pure scan/candidate folds non-authorizing and let only the store-reading closure mint LocatedReviewTab; otherwise seal every return-bearing link in the production chain (review_tab_located_from -> review_tab_standing_of_candidates -> review_tab_standing_of_scan -> review_tab_standing_from_read) to its sole caller.
2. Delete or close located_tab_for_witness so it cannot return a located carrier to unrestricted callers. Inline the locator call into the exact test functions, return only projected test facts, or seal the helper to its exact test callers.
3. Extend the forged probe to call each surviving alternate route by exact callee name. Removing one boundary at a time must red only that route's claim.

Do not repair this merely by adding another admitted wrapper while leaving its return unrestricted; that moves the proxy one hop. The exactly-one rule, ambiguity payload, formatter targeting, field-mask seam, and declared spreadsheet-id/rung limits otherwise need no redesign.

[briansrls]

SOURCE HOLD — exact head d13ad65925131bf56d4ae3ebacee4a88e63190c8

The previous carrier-egress hold is closed. The classification split is the preferred repair: classify_review_tabs, classify_review_tab_scan, and classify_review_tab_candidates now return non-authorizing ReviewTabClassification; review_tab_standing_from_classification is the only current production expression constructing LocatedReviewTab; review_tab_standing_of_outcome is sealed to the live reader; and the witness wrapper is sealed to its four primitive-returning consumers. The forged probe now covers the record, conversion, outcome classifier, and witness wrapper by exact callee name. The mask/decode seam, omitted-zero handling, exactly-one policy, and declared evidence limits remain sound.

One separate located-tab bypass remains in gunbc.review_sheet_format_actuator.

This PR makes the formatter's request records ordinary public values:

• FreezeRowsRequest
• HeaderBandRequest
• StandingRuleRequest
• FormatRequestPlan

and leaves every effectful consumer unrestricted:

fn freeze_header(q: FreezeRowsRequest) -> FormatStepOutcome uses net: Network
fn format_header_band(q: HeaderBandRequest) -> FormatStepOutcome uses net: Network
fn color_standing(q: StandingRuleRequest, ...) -> FormatStepOutcome uses net: Network
fn color_standing_derived(q: StandingRuleRequest, ...) -> FormatStepOutcome uses net: Network
fn format_review_sheet(plan: FormatRequestPlan) -> FormatReport uses net: Network

A foreign module can author a request carrying any spreadsheet_id and sheet_id, call one of those functions, and reach SetFrozenRows, FormatCellRange, or AddTextColorRule without ever obtaining a LocatedReviewTab, validating a schema, running the read-before-decide converge, or reaching converge_review_sheet_format. In particular, format_review_sheet can issue all seven writes from one caller-authored FormatRequestPlan.

That contradicts this change's central boundary: the production root consumes a located tab, but it is not the only route to the effects. This is the same alternate-effect-door shape already closed for issue_batch_request and the fabric release helpers.

Required closure:

1. Confine format_review_sheet to the converge path that derives its plan from LocatedReviewTab + ValidatedHeaderSchema.
2. Confine freeze_header and format_header_band to format_review_sheet, color_standing to format_review_sheet, and color_standing_derived to color_standing; or inline the effectful chain so no exported function accepting an ordinary request record reaches Sheets.
3. Add an outside-caller probe for every surviving effectful callee. Construct the ordinary request/plan values directly and require ConstructorCallAdmissionRefused at each exact subject. Unsealing one callee at a time should red only its claim.

The carrier repair itself needs no further redesign. The hold is now confined to making the located-tab requirement dominate the actual format writes, not merely the preferred converge entry.

[briansrls]

SOURCE APPROVE — exact head 902bc390fbba434120405a6e5170380f247df1d0.

GitHub would not accept a formal APPROVE because the connected identity is also the PR author.

The prior effects-bypass hold is closed on the stronger input boundary.

All four effect-bearing records are now sole_constructor: FreezeRowsRequest, HeaderBandRequest, StandingRuleRequest, and FormatRequestPlan. In the production module, each record has one literal/construction function, and every such builder requires a LocatedReviewTab; the header/whole-plan builders additionally consume ValidatedHeaderSchema. The mutation functions therefore accept only authority propagated from the located subject rather than caller-authored spreadsheet/sheet coordinates. No raw-id effect entry remains.

The forged probe authors each record directly and attempts the freeze, header-band, standing-rule, and whole-plan effect families. The witness keys a blocking SoleConstructorViolation to each exact record type. The reported M17–M20 diagonal — unsealing one record reds only its matching claim — is the right discriminator that these are four independent walls rather than duplicate observations of one diagnostic.

The previous carrier-egress repair remains intact: pure scan folds return non-authorizing ReviewTabClassification; the one classification-to-LocatedReviewTab conversion and its outcome wrapper are sealed; the witness wrapper is sealed to its exact consumers; only the real metadata-reading locate_review_tab is open.

The declared read_format_at(tab, range) limit is accurate: the located spreadsheet subject remains fixed while the read range is caller-selectable, and no mutation is exposed through that seam.

CI evidence is scoped correctly. On this exact head the hosted workflow compiled and linted the compiler; it executed no Daglang claim floor. The source ruling therefore relies on the exact-head source plus the reported local 29/29 claims and 20 mutation runs, not on the green required check.

Non-blocking packet corrections: the probe directly invokes four effect entries, not color_standing_derived itself; that fifth entry is nevertheless covered by the same sealed StandingRuleRequest input and has no alternate argument route. The PR body also still carries earlier claim counts and the superseded “both functions” confinement description. Neither changes the approved source.

No source hold remains.