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

dag/extdeps/google/sheets.dag

@@ -453,7 +453,34 @@ type SheetsColor {
   blue: Float
 }
 
-data spreadsheet_first_sheet_id: Int = 0
+// THE FIELD PATHS A MASK IS BUILT FROM, NAMED ONCE, BECAUSE A MASK AND A DECODE ARE ONE FACT.
+// A spreadsheets.get field mask is a list of upstream field paths, and every consumer that spells
+// one as a literal is authoring a second representation of what its own decode reads. That fork
+// is not theoretical: the format actuator's readback was changed to select a sheet by its
+// sheetId while its two masks still asked for no sheetId at all, so the selector looked for a
+// field the request had told Sheets not to send -- the grid read matched no sheet whatsoever and
+// the converge refused every time (review 68553). Nothing caught it because a mask literal and a
+// decode fold have no relation a compiler or a claim can check.
+//
+// These rows are that relation. A consumer composes its mask from the same named path its decode
+// keys on, so widening the reading and widening the request are one edit rather than two that can
+// drift. They are extdeps facts because the spelling is upstream's, not ours.
+data sheets_field_sheet_id: String = "sheets.properties.sheetId"
+
+data sheets_field_sheet_title: String = "sheets.properties.title"
+
+data sheets_field_sheet_index: String = "sheets.properties.index"
+
+data sheets_field_frozen_row_count: String = "sheets.properties.gridProperties.frozenRowCount"
+
+data sheets_field_conditional_formats: String = "sheets.conditionalFormats"
+
+data sheets_field_user_entered_format: String = "sheets.data.rowData.values.userEnteredFormat"
+
+fn sheets_field_mask(paths: List<String>) -> String {
+  join(paths, ",")
+}
+
 
 // THE READ SIDE OF A COLOUR, AND IT IS NOT THE WRITE SIDE'S TYPE. Google's JSON omits a field whose
 // value equals the proto3 default, so a channel of zero comes back ABSENT rather than 0.0 -- the
@@ -474,6 +501,20 @@ fn sheets_color_channel_read(channel: Float?) -> Float {
   }
 }
 
+fn sheets_sheet_id_read(id: Int?) -> Int {
+  match id {
+    Present { value: v } => v
+    Absent => 0
+  }
+}
+
+fn sheets_sheet_index_read(index: Int?) -> Int {
+  match index {
+    Present { value: v } => v
+    Absent => 0
+  }
+}
+
 type SheetsTextFormatRead {
   foregroundColor: SheetsColorRead?
   bold: Bool?
@@ -509,8 +550,29 @@ type SheetsGridPropertiesRead {
   frozenRowCount: Int?
 }
 
+// title AND index ARE THE TAB'S IDENTITY AND THEY ARE NOT THE FILE'S. A spreadsheet is a Drive
+// file with a display name, and every tab inside it carries its own title -- upstream calls the
+// file a Spreadsheet and each tab a Sheet, and sheets.properties.title is the tab's. Modelling
+// only sheetId left a consumer with no way to name the tab it had located, so the values path took
+// a title from its caller and the format path addressed sheet 0. Both are here because both come
+// back in one spreadsheets.get: sheetId is what a batchUpdate request addresses, title is what an
+// A1 range qualifies with, and index is the tab's position in the workbook, carried because the
+// response carries it and a consumer adjudicating two tabs needs to say which one it means.
+//
+// All three are Optional, and the three absences do NOT mean the same thing. sheetId and index
+// are Int and a first tab has 0 for both, which equals the proto3 default and is therefore OMITTED
+// from the JSON -- exactly as a zero colour channel and an unfrozen frozenRowCount are omitted, and
+// absent IS zero for the same reason. sheets_sheet_id_read and sheets_sheet_index_read are the only
+// places that say so, beside sheets_color_channel_read which already said it for a channel.
+//
+// title is NOT that case. Its proto3 default is the empty string and upstream never names a tab
+// with one, so an absent title is a response this model could not read rather than a tab called
+// nothing -- and a consumer that substituted a name there would be inventing the tab's identity.
+// Nothing here decides that; the type keeps the distinction and the consumer refuses on it.
 type SheetsSheetPropertiesRead {
   sheetId: Int?
+  title: String?
+  index: Int?
   gridProperties: SheetsGridPropertiesRead?
 }
 

dag/gunbc/recurring_failure_mode/readback_scoped_to_exclude_the_effect_it_verifies.dag

@@ -23,6 +23,12 @@ data readback_scoped_to_exclude_the_effect_it_verifies: RecurringFailureMode = R
 
     "**A SECOND, SMALLER FACT FROM THE SAME REPAIR, recorded here rather than as its own row because it has no life apart from this one: an EMPTY parameter is not an ABSENT parameter.** The first attempt at the unranged read passed `ranges=\"\"` and Sheets answered `400 Unable to parse range: `. A declared query parameter has no absent encoding, so removing a range from a request means an OPERATION THAT NAMES NO RANGE, not an operation whose range is empty -- which is why the repair added `GetSpreadsheetMetadata` beside `GetSpreadsheet` rather than passing a different value to the one that existed.",
 
+    "**A SECOND SPECIMEN, SAME MODULE, AND ITS DISCRIMINATOR IS DRIFT RATHER THAN A BOUND THAT WAS ALWAYS TOO SMALL (sharp-gull-485, gunbc#11725, review 68553, 2026-09-19).** `gunbc.review_sheet_format_actuator` stopped taking the head of the response's sheet list and began selecting the sheet whose `sheetId` is the LOCATED one -- and both field masks kept their old spelling. The grid mask requested no `properties` at all, so NO sheet matched and `converge_review_sheet_format` answered `FormatConvergeRefused` for every workbook; the metadata mask carried `properties` without the id, so absent-is-zero matched only tab zero, reinstating the take-the-first assumption that change existed to remove. Note what is different from the specimen above: the bound was CORRECT when it was authored and for every reading that then existed. The DECODE grew a new field dependency and the REQUEST was not widened with it, so the failure is a drift between two edits rather than a scope that never contained its subject.",
+
+    "**THE REPAIR GENERALISES THIS ROW'S RECOGNITION RULE, and is worth preferring to the split where it is available.** Naming the scope beside the extent is a discipline a reader performs, so it holds only while someone performs it -- and the specimen above shows it failing on the very next edit to the very same module. The stronger move is to remove the relationship's two ends: a mask and a decode are two representations of ONE fact, which fields this read needs, so the field paths become named rows (`extdeps.google.sheets` `sheets_field_sheet_id` and siblings) and every mask COMPOSES from the same row its decode keys on. Widening the reading and widening the request stop being two edits that can drift and become one declaration. That is construction where the rule above is validation (DESIGN section 5), and it is why this specimen's repair is not simply a wider literal.",
+
+    "**AND THE EVIDENCE LESSON IS SHARPER THAN THE PREVIOUS SPECIMEN'S.** That one concluded no witness could hold the wall because a witness never issues a request. True for the API's filtering semantics -- and it does NOT excuse this specimen, where the missing claim was cheap and purely local: whether the mask NAMES the field the decode keys on is decidable in the corpus, with no service involved. Eighteen claims, eight reddening mutations and a green required floor all passed over a production path that refused every workbook, because every formatter claim read the request PLAN and nothing ran the seam between the request MASK and the DECODE. The recognition rule that follows: when a claim set is built around one layer, the defect it cannot see is the JOIN to the layer beside it.",
+
     "RUNG FOUND AT: 1, mitigatable, and only because a human ran it. CEILING: 2, mechanically preventable, and the reason it stops there is honest rather than modest -- whether a request's scope contains an effect's extent is a fact about an EXTERNAL API's filtering semantics, which is DESIGN's outside-the-modeled-guarantee column and cannot be derived from the corpus. NEXT TRIGGER: a converge whose readback asserts, against a recorded prior actuation, that every fact it decides on was within the scope it requested -- the run that applies N rules and then reads back fewer than N refuses instead of re-applying.",
 
     "**WHY NO WITNESS COULD HAVE HELD THIS WALL, stated because the obvious follow-up is to write one.** Every witness supplies its own observation at the boundary it discriminates, so a witness over `format_is_converged` supplies a `FormatObservation` and asks what the function decides -- it cannot discover that a REQUEST does not return what the request asked for, because it never issues one. The missing evidence is the inhabitance half of the pairing obligation, and for an effectful external boundary the only instrument that carries it is an execution against the real service."

dag/gunbc/review_sheet_converge_cli.dag

@@ -10,6 +10,7 @@ import gunbc.review_sheet_format_actuator {
 import gunbc.review_sheet_projection {
   ci_prospect_sheet_schema,
   validate_header_schema,
+  ValidatedHeaderSchema,
   HeaderSchemaValidated,
   HeaderSchemaRefused,
 }
@@ -66,6 +67,15 @@ import gunbc.review_sheet_spreadsheet_actuator {
   spreadsheet_outcome_text,
 }
 import gunbc.review_sheet_drive_converge { ci_prospect_sheet_marker_value }
+import gunbc.review_sheet_tab_locator {
+  ReviewTabStanding,
+  TabLocated,
+  TabAbsent,
+  TabAmbiguous,
+  TabUnreadable,
+  locate_review_tab,
+  review_tab_standing_text,
+}
 
 // THE ONE ENTRY POINT. Everything an operator would otherwise do in a console is reachable from
 // here, and the sequence is the dependency order rather than a preference: the APIs cannot be
@@ -356,21 +366,40 @@ fn converge_drive_half_cli() -> ProcessExit uses net: Network {
 // just verified by readback. A converge that refused has no id to format, and formatting a sheet
 // whose identity was not settled is how the first live run wrote properties into a file nobody
 // could find again.
+// THE SKIP TEXT NAMES NO CAUSE OF ITS OWN, and that stopped being cosmetic when the locator
+// landed. It read "no converged spreadsheet", which was true while the only way to skip was a
+// spreadsheet that did not converge; there are now three more ways -- the tab is absent, ambiguous
+// or unreadable -- and the sentence would have asserted a converge failure that did not happen,
+// sending an operator to look at Drive for a problem that is inside the workbook. The carried
+// cause already says which it was, so the prefix says only that formatting did not run.
 type FormatDisposition
   = FormatAttempted { outcome: FormatConvergeOutcome }
   | FormatSkipped { cause: NonEmptyStr }
 
-// THE SCHEMA IS VALIDATED BEFORE THE FORMATTER IS REACHED, and a refusal SKIPS the format rather
-// than formatting to a guessed extent: converge_review_sheet_format takes ValidatedHeaderSchema,
-// so there is no arm of this fold that can hand it a schema whose header row is malformed.
+// TWO FACTS MUST BOTH BE ESTABLISHED BEFORE A SINGLE CELL IS FORMATTED, and they arrived from
+// different directions. gunbc#11705 made the SCHEMA a sealed ValidatedHeaderSchema so the
+// formatter cannot be handed a malformed header row; this branch made the TAB a sealed
+// LocatedReviewTab so it cannot be handed a guess about which tab to write to. They are
+// orthogonal -- a validated schema says what to write, a located tab says where -- and the
+// formatter now requires both, so neither can be supplied by assertion.
+//
+// The composition order is the cheap refusal first: validating the schema costs nothing and
+// reaches no network, while locating the tab is a spreadsheets.get. A run that cannot format
+// anyway should not spend a request discovering that.
 fn format_with_validated_schema(id: NonEmptyStr) -> FormatDisposition uses net: Network {
   match validate_header_schema(schema: ci_prospect_sheet_schema()) {
     HeaderSchemaRefused { refusal: _, reason: r } => FormatSkipped { cause: r }
-    HeaderSchemaValidated { validated: v } =>
-      FormatAttempted { outcome: converge_review_sheet_format(spreadsheet_id: id, validated: v) }
+    HeaderSchemaValidated { validated: v } => format_located_tab(file_id: id, validated: v)
   }
 }
 
+// THE FILE ID IS NOT ENOUGH AND THIS IS WHERE THAT WAS DISCOVERED. The converge above establishes
+// WHICH SPREADSHEET by a marker property on the Drive file; it establishes nothing about which tab
+// inside it the review lives in, and the formatter used to fill that gap with the constant zero.
+// The locator is now between them: the file id it reads from the converge is the spreadsheet it
+// asks Sheets about, and only a TabLocated reaches the formatter. Absent, ambiguous and unreadable
+// each skip formatting with the locator's own account of why, because formatting the wrong tab is
+// a silent wrong answer and skipping is a loud one.
 fn format_converged_spreadsheet(o: SpreadsheetConvergeOutcome) -> FormatDisposition uses net: Network {
   match o {
     SpreadsheetAdopted { file_id: id } => format_with_validated_schema(id: id)
@@ -380,10 +409,21 @@ fn format_converged_spreadsheet(o: SpreadsheetConvergeOutcome) -> FormatDisposit
   }
 }
 
+fn format_located_tab(file_id: NonEmptyStr, validated: ValidatedHeaderSchema) -> FormatDisposition uses net: Network {
+  let standing = locate_review_tab(spreadsheet_id: file_id)
+  match standing {
+    TabLocated { tab: t } =>
+      FormatAttempted { outcome: converge_review_sheet_format(tab: t, validated: validated) }
+    TabAbsent => FormatSkipped { cause: review_tab_standing_text(s: standing) as NonEmptyStr }
+    TabAmbiguous { candidates: _ } => FormatSkipped { cause: review_tab_standing_text(s: standing) as NonEmptyStr }
+    TabUnreadable { cause: _ } => FormatSkipped { cause: review_tab_standing_text(s: standing) as NonEmptyStr }
+  }
+}
+
 fn format_disposition_text(d: FormatDisposition) -> String {
   match d {
     FormatAttempted { outcome: o } => format_converge_text(o: o)
-    FormatSkipped { cause: c } => join(["formatting skipped, no converged spreadsheet: ", c as String], "")
+    FormatSkipped { cause: c } => join(["formatting skipped: ", c as String], "")
   }
 }