diff --git a/dag/extdeps/google/sheets.dag b/dag/extdeps/google/sheets.dag index a4a02bed875..205cfadaa3c 100644 --- a/dag/extdeps/google/sheets.dag +++ b/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 { + 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? } diff --git a/dag/gunbc/recurring_failure_mode/readback_scoped_to_exclude_the_effect_it_verifies.dag b/dag/gunbc/recurring_failure_mode/readback_scoped_to_exclude_the_effect_it_verifies.dag index d5b5f8f95ed..81fd1238765 100644 --- a/dag/gunbc/recurring_failure_mode/readback_scoped_to_exclude_the_effect_it_verifies.dag +++ b/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." diff --git a/dag/gunbc/review_sheet_converge_cli.dag b/dag/gunbc/review_sheet_converge_cli.dag index 752f4d568f3..f8319aaf8fb 100644 --- a/dag/gunbc/review_sheet_converge_cli.dag +++ b/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], "") } } diff --git a/dag/gunbc/review_sheet_format_actuator.dag b/dag/gunbc/review_sheet_format_actuator.dag index 62684ebd481..a73778ea202 100644 --- a/dag/gunbc/review_sheet_format_actuator.dag +++ b/dag/gunbc/review_sheet_format_actuator.dag @@ -37,7 +37,12 @@ import gunbc.review_sheet_projection { import extdeps.google.sheets import extdeps.google.sheets { SheetsColor, - spreadsheet_first_sheet_id, + sheets_field_mask, + sheets_field_sheet_id, + sheets_field_frozen_row_count, + sheets_field_conditional_formats, + sheets_field_user_entered_format, + sheets_sheet_id_read, SpreadsheetRead, SheetsSheetRead, SheetsColorRead, @@ -46,6 +51,14 @@ import extdeps.google.sheets { sheets_color_channel_read, } import v2.std.algebra { fold_list } +import gunbc.review_sheet_tab_locator { LocatedReviewTab } +import extdeps.google.sheets { + A1RangeEncoding, + A1RangeEncoded, + A1TitleApostropheUnsupported, + a1_range_encode, + a1_range_encoding_text, +} // THE PALETTE IS CITED AND THE CHANNELS ARE DERIVED. gunbc.design.catalog carries okabe_ito as a // CitedUpstream set anchored at jfly.uni-koeln.de, and it is the right set for this sheet for a @@ -218,16 +231,136 @@ fn classify_format_step(step: NonEmptyStr, outcome: RestOutcome) -> FormatStepOu } } -fn freeze_header(spreadsheet_id: NonEmptyStr) -> FormatStepOutcome uses net: Network { - let r = sheets.Spreadsheets.SetFrozenRows( - spreadsheet_id: spreadsheet_id as String, - sheet_id: spreadsheet_first_sheet_id, +// THE REQUESTS ARE DERIVED BEFORE ANY OF THEM IS SENT, AND THAT IS WHAT MAKES THE ADDRESSING +// WITNESSABLE. Every batchUpdate below names a sheetId, and until this change every one of them +// named a first-sheet constant of 0 (since deleted with its last consumer) -- so the formatter wrote to +// whatever tab happened to be first, in a file whose tab identity nothing had established. The +// sheetId now comes from a gunbc.review_sheet_tab_locator LocatedReviewTab, which has no +// constructor outside the function that read the workbook's metadata. +// +// The request records exist so that the addressing is a VALUE a claim can read rather than an +// argument inside an effect. format_request_plan is a pure fold from the located tab and the +// schema to every request this actuator would send, and test.claim.review_sheet_format_target_witness +// asserts that each one carries the located sheetId; the step functions take a request and pass +// its fields through. WHAT THAT DOES NOT ESTABLISH, said plainly: the claim reads the plan, not the +// wire, so it discriminates a plan built from the constant and does NOT discriminate a step +// rewritten to ignore the request it was handed. Closing that needs the mock corpus to carry the +// three batchUpdate operations, which it does not. +// THE REQUEST RECORDS ARE SEALED, AND THAT IS WHAT KEEPS THE EFFECTS BEHIND THE LOCATED TAB. +// These records exist so the addressing is a VALUE a claim can read rather than an argument buried +// in an effect. As ordinary records that was a bypass of the whole discipline above: every +// batchUpdate function below takes one, none of them was admission-restricted, and a record anyone +// could author meant a foreign module could call freeze_header or format_review_sheet with a +// spreadsheet id and sheet id it chose -- formatting an arbitrary tab of an arbitrary workbook +// without obtaining a LocatedReviewTab, validating a header schema, or running the converge at all +// (side-chat hold on gunbc#11725). The production entry required a located tab; the effects did not. +// +// THE CLOSURE IS ON THE INPUT, NOT ON THE CALLERS, for the same reason the carrier's was. Sealing +// five effectful functions to their exact predecessors would work and would leave confinement +// depending on an admission list staying complete as this module grows -- the two-lists-with-no-join +// defect that has already cost this branch a false seal claim and two silent mutation gaps. Instead +// every request record is sole_constructor and the ONLY expressions that build them are the three +// builders below, each of which requires a LocatedReviewTab. An unconstructible argument needs no +// guard on the function that consumes it: the effect functions stay unrestricted because there is +// no way to reach them except through a plan derived from a tab that was actually read. +// +// WHAT THAT LEAVES OPEN, said rather than implied: read_format_at takes a range String beside the +// located tab, so a caller holding a genuine tab may read any range WITHIN that spreadsheet. The +// subject stays confined -- the spreadsheet and tab are the located ones -- and it is a read, not a +// mutation. Narrowing the range to a derived value is the next rung and nothing today needs it. +type FreezeRowsRequest sole_constructor { + spreadsheet_id: String + sheet_id: Int + frozen_row_count: Int +} + +type HeaderBandRequest sole_constructor { + spreadsheet_id: String + sheet_id: Int + start_row: Int + end_row: Int + start_col: Int + end_col: Int +} + +type StandingRuleRequest sole_constructor { + spreadsheet_id: String + sheet_id: Int + start_row: Int + start_col: Int + end_col: Int + match_text: String + rule_index: Int +} + +fn freeze_rows_request(tab: LocatedReviewTab) -> FreezeRowsRequest { + FreezeRowsRequest { + spreadsheet_id: tab.spreadsheet_id as String, + sheet_id: tab.sheet_id, frozen_row_count: review_sheet_header_row_count, + } +} + +fn header_band_request(tab: LocatedReviewTab, validated: ValidatedHeaderSchema) -> HeaderBandRequest { + HeaderBandRequest { + spreadsheet_id: tab.spreadsheet_id as String, + sheet_id: tab.sheet_id, + start_row: 0, + end_row: review_sheet_header_row_count, + start_col: 0, + end_col: review_sheet_header_count(validated: validated), + } +} + +fn standing_rule_request( + tab: LocatedReviewTab, + match_text: String, + rule_index: Int, + standing_col: Int, +) -> StandingRuleRequest { + StandingRuleRequest { + spreadsheet_id: tab.spreadsheet_id as String, + sheet_id: tab.sheet_id, + start_row: review_sheet_header_row_count, + start_col: standing_col, + end_col: standing_col + 1, + match_text: match_text, + rule_index: rule_index, + } +} + +type FormatRequestPlan sole_constructor { + freeze: FreezeRowsRequest + header: HeaderBandRequest + opportunity: StandingRuleRequest + arbitrage: StandingRuleRequest + incompatible: StandingRuleRequest + required: StandingRuleRequest + replay: StandingRuleRequest +} + +fn format_request_plan(tab: LocatedReviewTab, validated: ValidatedHeaderSchema, standing_col: Int) -> FormatRequestPlan { + FormatRequestPlan { + freeze: freeze_rows_request(tab: tab), + header: header_band_request(tab: tab, validated: validated), + opportunity: standing_rule_request(tab: tab, match_text: "Opportunity", rule_index: 0, standing_col: standing_col), + arbitrage: standing_rule_request(tab: tab, match_text: "Arbitrage", rule_index: 1, standing_col: standing_col), + incompatible: standing_rule_request(tab: tab, match_text: "Incompatible", rule_index: 2, standing_col: standing_col), + required: standing_rule_request(tab: tab, match_text: "Required", rule_index: 3, standing_col: standing_col), + replay: standing_rule_request(tab: tab, match_text: "Replay", rule_index: 4, standing_col: standing_col), + } +} + +fn freeze_header(q: FreezeRowsRequest) -> FormatStepOutcome uses net: Network { + let r = sheets.Spreadsheets.SetFrozenRows( + spreadsheet_id: q.spreadsheet_id, + sheet_id: q.sheet_id, + frozen_row_count: q.frozen_row_count, ) classify_format_step(step: "freeze header row" as NonEmptyStr, outcome: r.outcome) } -fn format_header_band(spreadsheet_id: NonEmptyStr, validated: ValidatedHeaderSchema) -> FormatStepOutcome uses net: Network { +fn format_header_band(q: HeaderBandRequest) -> FormatStepOutcome uses net: Network { match header_background_color() { SheetsColorUnderivable { cause: c } => FormatStepRefused { step: "header band" as NonEmptyStr, cause: c } @@ -237,12 +370,12 @@ fn format_header_band(spreadsheet_id: NonEmptyStr, validated: ValidatedHeaderSch FormatStepRefused { step: "header band" as NonEmptyStr, cause: c } SheetsColorDerived { color: fg } => { let r = sheets.Spreadsheets.FormatCellRange( - spreadsheet_id: spreadsheet_id as String, - sheet_id: spreadsheet_first_sheet_id, - start_row: 0, - end_row: review_sheet_header_row_count, - start_col: 0, - end_col: review_sheet_header_count(validated: validated), + spreadsheet_id: q.spreadsheet_id, + sheet_id: q.sheet_id, + start_row: q.start_row, + end_row: q.end_row, + start_col: q.start_col, + end_col: q.end_col, background: bg, foreground: fg, bold: true, @@ -253,44 +386,30 @@ fn format_header_band(spreadsheet_id: NonEmptyStr, validated: ValidatedHeaderSch } } -fn color_standing( - spreadsheet_id: NonEmptyStr, - match_text: String, - color: SheetsColorReading, - rule_index: Int, - standing_col: Int, -) -> FormatStepOutcome uses net: Network { +fn color_standing(q: StandingRuleRequest, color: SheetsColorReading) -> FormatStepOutcome uses net: Network { match color { SheetsColorUnderivable { cause: c } => FormatStepRefused { - step: join(["standing colour for ", match_text], "") as NonEmptyStr, + step: join(["standing colour for ", q.match_text], "") as NonEmptyStr, cause: c, } - SheetsColorDerived { color: fg } => color_standing_derived( - spreadsheet_id: spreadsheet_id, match_text: match_text, color: fg, - rule_index: rule_index, standing_col: standing_col) + SheetsColorDerived { color: fg } => color_standing_derived(q: q, color: fg) } } -fn color_standing_derived( - spreadsheet_id: NonEmptyStr, - match_text: String, - color: SheetsColor, - rule_index: Int, - standing_col: Int, -) -> FormatStepOutcome uses net: Network { +fn color_standing_derived(q: StandingRuleRequest, color: SheetsColor) -> FormatStepOutcome uses net: Network { let r = sheets.Spreadsheets.AddTextColorRule( - spreadsheet_id: spreadsheet_id as String, - sheet_id: spreadsheet_first_sheet_id, - start_row: review_sheet_header_row_count, - start_col: standing_col, - end_col: standing_col + 1, - match_text: match_text, + spreadsheet_id: q.spreadsheet_id, + sheet_id: q.sheet_id, + start_row: q.start_row, + start_col: q.start_col, + end_col: q.end_col, + match_text: q.match_text, foreground: color, - rule_index: rule_index, + rule_index: q.rule_index, ) classify_format_step( - step: join(["standing colour for ", match_text], "") as NonEmptyStr, + step: join(["standing colour for ", q.match_text], "") as NonEmptyStr, outcome: r.outcome, ) } @@ -346,25 +465,15 @@ type FormatReport { // The steps are named individually rather than folded over the roster because each is an EFFECT // and the report names which one refused. A fold would answer "one of five failed", which is the // shape of diagnostic this session has repeatedly had to go back and re-derive. -fn format_review_sheet(spreadsheet_id: NonEmptyStr, validated: ValidatedHeaderSchema, standing_col: Int) -> FormatReport uses net: Network { +fn format_review_sheet(plan: FormatRequestPlan) -> FormatReport uses net: Network { FormatReport { - freeze: freeze_header(spreadsheet_id: spreadsheet_id), - header: format_header_band(spreadsheet_id: spreadsheet_id, validated: validated), - opportunity: color_standing( - spreadsheet_id: spreadsheet_id, match_text: "Opportunity", - color: standing_admitted_color(), rule_index: 0, standing_col: standing_col), - arbitrage: color_standing( - spreadsheet_id: spreadsheet_id, match_text: "Arbitrage", - color: standing_admitted_color(), rule_index: 1, standing_col: standing_col), - incompatible: color_standing( - spreadsheet_id: spreadsheet_id, match_text: "Incompatible", - color: standing_refused_color(), rule_index: 2, standing_col: standing_col), - required: color_standing( - spreadsheet_id: spreadsheet_id, match_text: "Required", - color: standing_refused_color(), rule_index: 3, standing_col: standing_col), - replay: color_standing( - spreadsheet_id: spreadsheet_id, match_text: "Replay", - color: standing_refused_color(), rule_index: 4, standing_col: standing_col), + freeze: freeze_header(q: plan.freeze), + header: format_header_band(q: plan.header), + opportunity: color_standing(q: plan.opportunity, color: standing_admitted_color()), + arbitrage: color_standing(q: plan.arbitrage, color: standing_admitted_color()), + incompatible: color_standing(q: plan.incompatible, color: standing_refused_color()), + required: color_standing(q: plan.required, color: standing_refused_color()), + replay: color_standing(q: plan.replay, color: standing_refused_color()), } } @@ -422,20 +531,20 @@ type FormatObservation // THE SECOND READ IS UNRANGED AND CARRIES NO GRID DATA, so the conditional rules are not filtered // away by a range chosen to bound something else. It is cheap for the same reason: sheet metadata // without grid data does not grow with the census. -fn read_format_meta(spreadsheet_id: NonEmptyStr, grid: SpreadsheetRead) -> FormatObservation uses net: Network { +fn read_format_meta(tab: LocatedReviewTab, grid: SpreadsheetRead) -> FormatObservation uses net: Network { let meta = sheets.Spreadsheets.GetSpreadsheetMetadata( - spreadsheet_id: spreadsheet_id as String, + spreadsheet_id: tab.spreadsheet_id as String, fields: review_sheet_format_meta_field_mask, ) match classify_rest_outcome(standing: RestReadExchange { rest: meta.outcome }) { RestExchangeSucceeded => - match first_sheet(read: meta.result) { + match located_sheet(read: meta.result, sheet_id: tab.sheet_id) { Absent => FormatUnreadable { - cause: "spreadsheets.get answered with no sheets for the metadata read, so the frozen row count and the conditional rules could not be observed" as NonEmptyStr + cause: "the metadata read answered with no sheet carrying the located sheetId, so the frozen row count and the conditional rules of the tab this converge addresses could not be observed" as NonEmptyStr } Present { value: meta_sheet } => - match header_format_of(read: grid) { + match header_format_of(read: grid, sheet_id: tab.sheet_id) { HeaderFormatUnreadable { cause: c } => FormatUnreadable { cause: c } HeaderFormatRead { format: h } => FormatObserved { @@ -476,11 +585,11 @@ type HeaderFormatReading = HeaderFormatRead { format: SheetsCellFormatRead? } | HeaderFormatUnreadable { cause: NonEmptyStr } -fn header_format_of(read: SpreadsheetRead) -> HeaderFormatReading { - match first_sheet(read: read) { +fn header_format_of(read: SpreadsheetRead, sheet_id: Int) -> HeaderFormatReading { + match located_sheet(read: read, sheet_id: sheet_id) { Absent => HeaderFormatUnreadable { - cause: "the grid read answered with no sheets, so the first sheet's header format could not be read and nothing may be adopted from it" as NonEmptyStr + cause: "the grid read answered with no sheet carrying the located sheetId, so the header format of the tab this converge addresses could not be read and nothing may be adopted from it" as NonEmptyStr } Present { value: sheet } => HeaderFormatRead { format: observed_header_format(sheet: sheet) } } @@ -505,11 +614,32 @@ fn header_format_of(read: SpreadsheetRead) -> HeaderFormatReading { // The split is along what each question actually needs. Grid data is expensive and MUST stay bounded // to the header row. The frozen row count and the conditional rules are sheet metadata, need no grid // data at all, and must NOT be range-filtered. -data review_sheet_format_grid_field_mask: String = "sheets.data.rowData.values.userEnteredFormat" +// BOTH MASKS NOW REQUEST THE sheetId, AND OMITTING IT BROKE THE PRODUCTION PATH OUTRIGHT. +// When the readback stopped taking the head of the sheet list and started selecting the sheet +// whose sheetId is the LOCATED one, these two masks kept their old spelling -- so the selector +// keyed on a field the request had told Sheets not to send. The grid mask asked for no +// properties at all, so no sheet ever matched and converge_review_sheet_format answered +// FormatConvergeRefused for every workbook; the metadata mask carried properties without the id, +// so absent-is-zero made it match only when the located tab happened to be tab zero -- the exact +// assumption this change exists to remove, reintroduced in the one place nothing was looking +// (review 68553). +// +// The masks are composed from extdeps.google.sheets field-path rows rather than spelled here, so +// the path the decode keys on and the path the request asks for are ONE declaration. That is the +// repair: the defect was not a forgotten string, it was a mask and a decode being two +// representations of one fact with nothing joining them, which is what let widening the reading +// and widening the request come apart. +data review_sheet_format_grid_field_mask: String = sheets_field_mask(paths: [sheets_field_sheet_id, sheets_field_user_entered_format]) -data review_sheet_format_meta_field_mask: String = "sheets.properties.gridProperties.frozenRowCount,sheets.conditionalFormats" +data review_sheet_format_meta_field_mask: String = sheets_field_mask(paths: [sheets_field_sheet_id, sheets_field_frozen_row_count, sheets_field_conditional_formats]) -data review_sheet_header_range: String = "A1:Q1" +// THE RANGE IS QUALIFIED BY THE LOCATED TITLE, and the bare form this replaced is the READ side of +// the same defect the constant sheetId was on the write side. gunbc.review_sheet_sheets +// a1_readback_standing already refuses an unqualified A1 range in as many words -- "BatchUpdate +// would hit the first tab" -- and this module was sending one. The title comes from the located +// tab, never from the Drive file's display name: they are written by different systems into +// different places and renaming one does not touch the other. +data review_sheet_header_cells: String = "A1:Q1" // THE FIRST ELEMENT OF A LIST, ONCE PER TYPE, AND THE GENERIC IT REPLACES DID NOT SURVIVE CONTACT. // An earlier revision wrote one generic first_of folding over List with `none` as the initial @@ -556,22 +686,43 @@ fn first_cell(items: List) -> SheetsCellDataRead? { ) } -fn first_sheet_of(items: List) -> SheetsSheetRead? { +// THE SHEET IS SELECTED BY ITS LOCATED ID, NOT BY BEING FIRST. Both folds this replaced took the +// head of the response's sheet list, which is the same assumption the constant sheetId made on the +// write side wearing a different hat: a readback that inspects the first tab while the writes +// address the located one would report UNVERIFIED for a correctly formatted sheet, or -- worse, in +// the case the two happen to coincide today -- report VERIFIED for a tab nobody wrote to. The +// readback and the write must address the same tab for the readback to be evidence at all. +// THE ABSENT-IS-ZERO RULE IS CALLED, NOT RESTATED. An earlier cut of this predicate spelled the +// proto3 omission inline as `Absent => sheet_id == 0`, in the same change that declared +// extdeps.google.sheets sheets_sheet_id_read as the single authority for exactly that fact +// (review 68663). Two spellings of one rule is the fork DESIGN section 3 exists to prevent, and it +// is the same defect shape this change already repaired between the field masks and the decode: +// correcting or widening the omission rule must be ONE edit, not an edit plus a search. Absent +// PROPERTIES stays distinct and stays here -- a sheet whose properties were never read is not a +// sheet whose sheetId was omitted, and only the second is a zero. +fn sheet_read_has_id(sheet: SheetsSheetRead, sheet_id: Int) -> Bool { + match sheet.properties { + Absent => false + Present { value: props } => sheets_sheet_id_read(id: props.sheetId) == sheet_id + } +} + +fn sheet_with_id(items: List, sheet_id: Int) -> SheetsSheetRead? { fold_list( items, none, (acc, x) => match acc { Present { value: v } => Present { value: v } - Absent => Present { value: x } + Absent => if sheet_read_has_id(sheet: x, sheet_id: sheet_id) { Present { value: x } } else { none } }, ) } -fn first_sheet(read: SpreadsheetRead) -> SheetsSheetRead? { +fn located_sheet(read: SpreadsheetRead, sheet_id: Int) -> SheetsSheetRead? { match read.sheets { Absent => none - Present { value: sheets } => first_sheet_of(items: sheets) + Present { value: ss } => sheet_with_id(items: ss, sheet_id: sheet_id) } } @@ -624,15 +775,53 @@ fn observed_header_format(sheet: SheetsSheetRead) -> SheetsCellFormatRead? { } } -fn read_format(spreadsheet_id: NonEmptyStr) -> FormatObservation uses net: Network { +// THE TITLE IS ENCODED BY THE CODEC THAT LANDED, NOT BY A RULE THIS MODULE INVENTED. An earlier +// cut of this branch carried gunbc.review_sheet_sheets a1_tab_qualification, which REFUSED a title +// containing a space, an apostrophe, a bang or a colon on the stated ground that no encoder +// existed and writing a second one beside gunbc#11703 would be the fork that PR exists to prevent. +// #11703 has since landed as extdeps.google.sheets a1_range_encode, so that function's own +// dissolution trigger -- "it retires when 11703 lands an encoder this function can call instead of +// declining" -- has fired, and it is deleted rather than left standing beside its replacement. +// +// THE DELETION ALSO REMOVES AN OVER-PROHIBITION, which is worth naming because it was the more +// interesting defect. Quoting makes a space, a bang and a colon perfectly legal in an A1 title; +// refusing them was forbidding more of the world than the evidence supported, and the cost of that +// arm was invisible -- a correctly formattable workbook declining to format, with the refusal +// reading like rigour (DESIGN section 4d). The codec refuses exactly one thing, an apostrophe, +// because its WIRE SPELLING is genuinely unobserved and it says so with a read obligation. +type HeaderRangeStanding + = HeaderRangeWire { range: String } + | HeaderRangeUnqualifiable { cause: NonEmptyStr } + +fn review_sheet_header_range(tab: LocatedReviewTab) -> HeaderRangeStanding { + match a1_range_encode(title: tab.title, cells: Present { value: review_sheet_header_cells }) { + A1RangeEncoded { wire: w } => HeaderRangeWire { range: w } + A1TitleApostropheUnsupported { title: t } => + HeaderRangeUnqualifiable { + cause: a1_range_encoding_text(e: A1TitleApostropheUnsupported { title: t }) as NonEmptyStr + } + } +} + +fn read_format(tab: LocatedReviewTab) -> FormatObservation uses net: Network { + match review_sheet_header_range(tab: tab) { + HeaderRangeUnqualifiable { cause: c } => + FormatUnreadable { + cause: join(["the located tab's title cannot qualify an A1 range, so the header read would have been unqualified and would have hit whichever tab is first: ", c as String], "") as NonEmptyStr + } + HeaderRangeWire { range: r } => read_format_at(tab: tab, range: r) + } +} + +fn read_format_at(tab: LocatedReviewTab, range: String) -> FormatObservation uses net: Network { let grid = sheets.Spreadsheets.GetSpreadsheet( - spreadsheet_id: spreadsheet_id as String, - range: review_sheet_header_range, + spreadsheet_id: tab.spreadsheet_id as String, + range: range, fields: review_sheet_format_grid_field_mask, include_grid_data: true, ) match classify_rest_outcome(standing: RestReadExchange { rest: grid.outcome }) { - RestExchangeSucceeded => read_format_meta(spreadsheet_id: spreadsheet_id, grid: grid.result) + RestExchangeSucceeded => read_format_meta(tab: tab, grid: grid.result) RestExchangeStatusRefused { status, body } => FormatUnreadable { cause: join(["spreadsheets.get answered ", to_string(status), ": ", body], "") as NonEmptyStr @@ -711,8 +900,22 @@ type FormatConvergeOutcome // THE READBACK IS THE SAME READ THE CONVERGE OPENED WITH, not a trusted echo of the writes. A // batchUpdate answering 200 has told us what it did, not what the sheet now carries, and the // distance between those two is where the first live run lost an hour. +// THE SUBJECT IS A LOCATED TAB, NOT A FILE ID. The parameter used to be the spreadsheet's file id +// alone, which named the workbook and left every request inside it to address tab zero. A +// LocatedReviewTab names the workbook AND the tab, and it has no constructor outside +// gunbc.review_sheet_tab_locator, so a caller cannot reach this function with a tab it asserted +// rather than observed. +// +// WHAT THIS CONVERGE VERIFIES, STATED AT ITS ACTUAL STRENGTH. format_is_converged compares three +// facts read back off the located tab: the frozen row count exactly, the header cell's background +// and foreground at swatch width, and the NUMBER of conditional format rules. It does not compare +// each rule's condition or colour, so a tab carrying five unrelated rules reads as converged; it +// does not check the header band's extent or the standing column's position; and it reads +// userEnteredFormat, so it verifies what this repository wrote rather than what a viewer sees. +// FormatAppliedAndVerified means those three facts hold on the tab that was addressed -- which is +// the fact this change adds, and it is a smaller claim than "the sheet is formatted". fn converge_review_sheet_format( - spreadsheet_id: NonEmptyStr, + tab: LocatedReviewTab, validated: ValidatedHeaderSchema, ) -> FormatConvergeOutcome uses net: Network { match standing_column_index(validated: validated) { @@ -721,12 +924,12 @@ fn converge_review_sheet_format( cause: "the supplied schema carries no ListingStanding column, so there is no column to colour by standing and painting a positional guess would colour whatever now sits there" as NonEmptyStr } StandingColumnAt { index: standing_col } => - converge_format_with_standing(spreadsheet_id: spreadsheet_id, validated: validated, standing_col: standing_col) + converge_format_with_standing(tab: tab, validated: validated, standing_col: standing_col) } } fn converge_format_with_standing( - spreadsheet_id: NonEmptyStr, + tab: LocatedReviewTab, validated: ValidatedHeaderSchema, standing_col: Int, ) -> FormatConvergeOutcome uses net: Network { @@ -743,7 +946,7 @@ fn converge_format_with_standing( SheetsColorUnderivable { cause: c } => FormatConvergeRefused { cause: c } SheetsColorDerived { color: fg } => converge_with_desired( - spreadsheet_id: spreadsheet_id, validated: validated, standing_col: standing_col, + tab: tab, validated: validated, standing_col: standing_col, inclusive_max: m, header_bg: bg, header_fg: fg) } } @@ -751,14 +954,14 @@ fn converge_format_with_standing( } fn converge_with_desired( - spreadsheet_id: NonEmptyStr, + tab: LocatedReviewTab, validated: ValidatedHeaderSchema, standing_col: Int, inclusive_max: Int, header_bg: SheetsColor, header_fg: SheetsColor, ) -> FormatConvergeOutcome uses net: Network { - let observed = read_format(spreadsheet_id: spreadsheet_id) + let observed = read_format(tab: tab) match observed { FormatUnreadable { cause: c } => FormatConvergeRefused { @@ -769,8 +972,8 @@ fn converge_with_desired( FormatAlreadyConverged } else { verify_applied_format( - spreadsheet_id: spreadsheet_id, - report: format_review_sheet(spreadsheet_id: spreadsheet_id, validated: validated, standing_col: standing_col), + tab: tab, + report: format_review_sheet(plan: format_request_plan(tab: tab, validated: validated, standing_col: standing_col)), inclusive_max: inclusive_max, header_bg: header_bg, header_fg: header_fg, @@ -780,14 +983,14 @@ fn converge_with_desired( } fn verify_applied_format( - spreadsheet_id: NonEmptyStr, + tab: LocatedReviewTab, report: FormatReport, inclusive_max: Int, header_bg: SheetsColor, header_fg: SheetsColor, ) -> FormatConvergeOutcome uses net: Network { if format_report_all_applied(r: report) { - if format_is_converged(o: read_format(spreadsheet_id: spreadsheet_id), inclusive_max: inclusive_max, header_bg: header_bg, header_fg: header_fg) { + if format_is_converged(o: read_format(tab: tab), inclusive_max: inclusive_max, header_bg: header_bg, header_fg: header_fg) { FormatAppliedAndVerified { report: report } } else { FormatAppliedUnverified { diff --git a/dag/gunbc/review_sheet_tab_locator.dag b/dag/gunbc/review_sheet_tab_locator.dag new file mode 100644 index 00000000000..02df06b35c5 --- /dev/null +++ b/dag/gunbc/review_sheet_tab_locator.dag @@ -0,0 +1,393 @@ +module gunbc.review_sheet_tab_locator + +import std.types { NonEmptyStr, String, Int, List } +import std.resources { Network } +import std.decl_ref { decl_ref } +import extdeps.transports.rest { + RestOutcome, + RestReadExchange, + RestExchangeSucceeded, + RestExchangeStatusRefused, + RestExchangeUnreached, + RestExchangeUndecodable, + RestExchangeCommitAmbiguous, + classify_rest_outcome, +} +import extdeps.google.sheets +import extdeps.google.sheets { + SpreadsheetRead, + SheetsSheetRead, + SheetsSheetPropertiesRead, + sheets_sheet_id_read, + sheets_sheet_index_read, + sheets_field_mask, + sheets_field_sheet_id, + sheets_field_sheet_title, + sheets_field_sheet_index, +} +import v2.std.algebra { fold_list } + +// A FILE IS NOT A TAB, AND UNTIL THIS MODULE THE CORPUS ONLY EVER ESTABLISHED THE FILE. +// gunbc.review_sheet_spreadsheet_actuator converge_review_spreadsheet finds or creates the Drive +// file by a marker property and returns a file_id. That settles WHICH SPREADSHEET. It says nothing +// about which of the tabs inside it is the review tab, and a spreadsheet is a container of tabs: +// gunbc.review_sheet_sheets already refuses an unqualified A1 range with "BatchUpdate would hit the +// first tab", and gunbc.review_sheet_format_actuator addressed extdeps.google.sheets +// a first-sheet constant of 0 on every one of its batchUpdate steps. Both were +// assuming the answer to a question nobody had asked upstream. +// +// THE ADMISSION RULE IS EXACTLY-ONE, AND IT IS CHOSEN RATHER THAN DEFAULTED. +// A spreadsheet carrying exactly one tab HAS a review tab and no adjudication is required: the one +// tab's observed sheetId and observed title are adopted as read. Two or more is TabAmbiguous and +// this module refuses to pick, because nothing it can observe distinguishes them -- index order is +// a workbook layout fact, not a statement about which tab the review lives in, and "take the first" +// is the very assumption being removed rather than a weaker version of it. +// +// WHY NOT THE OTHER RULE (converge a specifically named tab and read it back). It is the stronger +// rule and it is the one this lane should end at. It needed two things this corpus lacked, and +// ONE OF THEM HAS SINCE ARRIVED: the A1 title codec, gunbc#11703, landed as extdeps.google.sheets +// a1_range_encode while this change was in review, so saying what a valid title is and how it +// quotes inside a range is now a solved problem and this module's formatter calls it. +// +// WHAT REMAINS IS THE WRITE HALF, and it is the whole of the remaining gap: naming a tab means a +// spreadsheets.batchUpdate addSheet request, which extdeps.google.sheets does not model at all -- +// there is no operation to issue, not merely an awkward one. So exactly-one stays the rule today, +// and the trigger for revisiting it is now singular and checkable rather than a pair: an addSheet +// operation on the sheets.Spreadsheets service. +// +// Building exactly-one first is not a weaker substitute for that convergence; it is its +// OBSERVATION HALF, which the named-tab rule needs anyway to read its own write back. Nothing here +// has to be deleted when the write half lands: a named converge adds an Apply arm ahead of this +// read, and this read stays the independent readback (DESIGN section 3d -- selection precedes +// convergence, and a convergence primitive reads back independently). +// +// AND THE FIT IS REAL RATHER THAN CONVENIENT. The only creator of this file is +// converge_review_spreadsheet, which calls drive.Files.CreateFile with the Google Sheets MIME type +// and nothing else; a spreadsheet minted that way has exactly one tab. 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. Refusing to a human is +// the right answer to a state only a human created. + +// THE FILE'S DISPLAY NAME IS NEVER READ HERE AND THAT IS THE POINT OF THE MODULE. +// gunbc.review_sheet_converge_cli ci_prospect_sheet_name is the Drive file's name, written by +// files.create into the file's metadata. The tab's title is written by Sheets into the workbook +// when the file is minted, and upstream's default is "Sheet1" -- the two facts have different +// authors, different storage and no upstream relation, and renaming one does not touch the other. +// Inferring either from the other would produce an A1 range naming a tab that does not exist, which +// Sheets answers 400 for; worse, the SAME inference on a workbook that happens to agree would +// answer 200 and hide the defect until the day somebody renamed the file. There is no import of +// review_sheet_converge_cli in this module, so the inference is unavailable rather than declined. +type ReviewTabCandidate { + sheet_id: Int + title: NonEmptyStr + index: Int +} + +// THE LOCATED CARRIER IS SEALED, AND IT IS SEALED FOR THE SAME REASON THE HOLD PLANS ARE. +// gunbc.durable_exclusive_hold_file_store states the discipline: a plan is minted ONLY by a +// function that performed the read itself, is sole_constructor, and carries the subject it was +// read from -- so a caller cannot author a coordinate and hand it to a writer. The shape of the +// harm is the same one class down here. A hand-built LocatedReviewTab { sheet_id: 0 } committed to +// the formatter reinstates exactly the constant this change removes, and it does so while WEARING +// THE NAME of an observation: every downstream refusal reads "the located tab", and the located +// tab was a literal. So the record has no constructor outside this module, and the one mint below +// is further admit_callers-sealed so that even inside it, only the function that performed the +// metadata read may call it. +// +// WHICH PATH THE SEAL IS EVIDENCED ON, because DESIGN section 4b(1) takes a class's rung as the +// MINIMUM across its in-scope paths and citing the strongest one is inflation. The evidence here +// is source -> v1 interpretation: the probe's refusals are raised by the seed's +// parsed_sole_constructor_properties, which is the compiler claim_batch runs. On the NATIVE v2 +// path the modifier is consumed by G0 and the construction property is not minted, so the wall is +// not recorded there -- that is the standing corpus-wide drop +// gunbc.rung_drop.g0_type_decl_modifier_parse_without_sealing_property, which covers every +// sole_constructor type rather than anything this module introduces, and it is named here so the +// claim above is read at the strength it actually has. +// +// WHAT THE SEAL DOES NOT CLOSE, said here rather than left to be discovered. It does not make the +// READ honest -- a locator handed a truthful response still depends on Sheets having answered about +// the spreadsheet we asked about, and the spreadsheet_id carried on the record is this process's +// own argument rather than a value read back out of the response. The response does carry +// spreadsheetId, and cross-checking it is the next rung; it is not done here because +// GetSpreadsheetMetadata's field mask selects sheets.properties and would have to widen, and a +// widened mask changes what every existing caller of that operation pays. DESIGN section 4b(2): +// this is a class below its ceiling naming its trigger, which is a spreadsheetId in the mask. +type LocatedReviewTab sole_constructor { + spreadsheet_id: NonEmptyStr + sheet_id: Int + title: NonEmptyStr +} + +// FOUR ARMS AND NO FIFTH, and the three that are not TabLocated are three different remedies. +// TabAbsent is a spreadsheet with no tabs at all, which Sheets does not produce and a truncated +// field mask does -- the remedy is to look at the request. TabAmbiguous is a person's edit and the +// remedy is a person. TabUnreadable is anything that stopped this from being an observation: a +// refused status, an unreachable endpoint, a tab whose properties or title the response did not +// carry. Folding the last two together would send an operator to adjudicate tabs when the real +// answer was a 403. +type ReviewTabStanding + = TabLocated { tab: LocatedReviewTab } + | TabAbsent + | TabAmbiguous { candidates: List } + | TabUnreadable { cause: NonEmptyStr } + +// A TAB WHOSE IDENTITY THE RESPONSE DID NOT CARRY IS A READING THAT FAILED, NOT A TAB WITH +// DEFAULTS. sheetId and index are Int and absent means zero -- the proto3 omission +// extdeps.google.sheets sheets_sheet_id_read is the single authority for, the same rule the colour +// channels and frozenRowCount already run under. title is a String whose default is empty, and +// upstream has no tab named "", so an absent title is the response failing to say what the tab is +// called. Substituting anything there -- the file name, "Sheet1", the index -- would be this module +// AUTHORING the identity it exists to observe. +type ReviewTabCandidateReading + = CandidateRead { candidate: ReviewTabCandidate } + | CandidateUnreadable { cause: NonEmptyStr } + +fn review_tab_candidate_of(sheet: SheetsSheetRead) -> ReviewTabCandidateReading { + match sheet.properties { + Absent => + CandidateUnreadable { + cause: "spreadsheets.get answered with a sheet carrying no properties at all, so neither its sheetId nor its title was read and nothing may be adopted from it" as NonEmptyStr + } + Present { value: props } => review_tab_candidate_of_properties(props: props) + } +} + +fn review_tab_candidate_of_properties(props: SheetsSheetPropertiesRead) -> ReviewTabCandidateReading { + match props.title { + Absent => + CandidateUnreadable { + cause: "spreadsheets.get answered with a sheet whose properties carry no title; a tab title has no proto3 default that upstream ever produces, so this is an unread field rather than an unnamed tab, and naming it from anything else would invent the tab's identity" as NonEmptyStr + } + Present { value: t } => review_tab_candidate_titled(props: props, title: t) + } +} + +fn review_tab_candidate_titled(props: SheetsSheetPropertiesRead, title: String) -> ReviewTabCandidateReading { + if title == "" { + CandidateUnreadable { + cause: "spreadsheets.get answered with a sheet whose title is the empty string; upstream names no tab that, so the field was present and meaningless rather than read" as NonEmptyStr + } + } else { + CandidateRead { + candidate: ReviewTabCandidate { + sheet_id: sheets_sheet_id_read(id: props.sheetId), + title: title as NonEmptyStr, + index: sheets_sheet_index_read(index: props.index), + } + } + } +} + +// THE SCAN CARRIES EVERY CANDIDATE AND THE FIRST UNREADABLE CAUSE, because both are needed by +// different arms: the candidates are what TabAmbiguous must show an operator, and one unreadable +// sheet poisons the whole reading rather than being skipped -- a tab this module could not read is +// a tab it cannot rule out as the review tab, so silently dropping it would turn a two-tab +// workbook into a confident one-tab answer. That is the absorbing fallback DESIGN section 5 +// refuses, and it is the exact widen this scan exists to avoid. +type ReviewTabScan { + candidates: List + unreadable: NonEmptyStr? +} + +fn advance_review_tab_scan(acc: ReviewTabScan, sheet: SheetsSheetRead) -> ReviewTabScan { + match review_tab_candidate_of(sheet: sheet) { + CandidateUnreadable { cause: c } => + match acc.unreadable { + Present { value: first } => ReviewTabScan { candidates: acc.candidates, unreadable: Present { value: first } } + Absent => ReviewTabScan { candidates: acc.candidates, unreadable: Present { value: c } } + } + CandidateRead { candidate: cand } => + ReviewTabScan { candidates: concat(acc.candidates, [cand]), unreadable: acc.unreadable } + } +} + +fn review_tab_scan_of(sheets_read: List) -> ReviewTabScan { + fold_list( + sheets_read, + ReviewTabScan { candidates: [], unreadable: none }, + (acc, s) => advance_review_tab_scan(acc: acc, sheet: s), + ) +} + +// THE CLASSIFICATION AUTHORIZES NOTHING, AND THAT SPLIT IS THE WHOLE REPAIR. +// An earlier cut of this module had SIX exported functions returning ReviewTabStanding and sealed +// two of them, then claimed "both routes to the mint are sealed". That claim enumerated the doors +// that had been locked rather than the doors: review_tab_located_from built the record literal +// with no admission at all, so a foreign module could author one ReviewTabCandidate, call it, and +// hand a LocatedReviewTab to the formatter having performed no Sheets read -- the exact forgery +// sole_constructor exists to prevent, reached through a wrapper instead of through the record. +// review_tab_standing_of_scan and review_tab_standing_of_candidates were the same escape one hop +// further out. The rostered class: AN ADMITTED CALL EDGE DOES NOT CONFINE A VALUE WHEN AN EXPORTED +// WRAPPER RETURNS THAT VALUE OR A CARRIER CONTAINING IT, and the obligation it carries is to +// enumerate EVERY exported return path containing the confined type, not every function one +// happens to have sealed. +// +// Sealing the chain link by link would have worked and is the weaker answer, because it leaves the +// confinement depending on a list staying complete as the module grows -- the same two-lists +// problem this branch has now hit three times. So the folds no longer return the carrier AT ALL. +// They answer a ReviewTabClassification, which is freely constructible and freely returned because +// it authorizes nothing: it says what the response looked like, never that anything was read. The +// only function in this corpus that turns a classification into a LocatedReviewTab is the sealed +// conversion below, reachable only from the live-read route. +// +// The benefit beyond confinement is that the classification is PURE and needs no admission, so a +// witness discriminates the exactly-one / none / many / unreadable decision at full payload +// without being admitted to anything -- the earlier cut had to admit eight witness functions to +// the mint to assert those same facts, and every one of those admissions was a hole. +type ReviewTabClassification + = ClassifiedExactlyOne { candidate: ReviewTabCandidate } + | ClassifiedNone + | ClassifiedMany { candidates: List } + | ClassifiedUnreadable { cause: NonEmptyStr } + +fn classify_review_tabs(read: SpreadsheetRead) -> ReviewTabClassification { + match read.sheets { + Absent => ClassifiedNone + Present { value: ss } => classify_review_tab_scan(scan: review_tab_scan_of(sheets_read: ss)) + } +} + +// AN UNREADABLE TAB IS CHECKED BEFORE THE COUNT, deliberately. A workbook whose second sheet came +// back without properties has an unknown number of tabs, so answering "exactly one" from the one +// that parsed would be a confident answer derived from an incomplete reading. +fn classify_review_tab_scan(scan: ReviewTabScan) -> ReviewTabClassification { + match scan.unreadable { + Present { value: c } => ClassifiedUnreadable { cause: c } + Absent => classify_review_tab_candidates(candidates: scan.candidates) + } +} + +// THE ONE-ELEMENT LIST IS RE-OPENED RATHER THAN INDEXED, because there is no total indexing +// operation to reach for and a fold that cannot find its single element must say so rather than +// substitute one. The Absent arm is unreachable given count == 1 and is still a refusal: a fold +// whose impossible arm invents a tab is the same defect as the constant, arriving later. +fn classify_review_tab_candidates(candidates: List) -> ReviewTabClassification { + if count(candidates) == 0 { + ClassifiedNone + } else { + if count(candidates) == 1 { + match first_review_tab_candidate(items: candidates) { + Absent => + ClassifiedUnreadable { + cause: "the scan counted exactly one candidate tab and then could not read it back out of its own list" as NonEmptyStr + } + Present { value: c } => ClassifiedExactlyOne { candidate: c } + } + } else { + ClassifiedMany { candidates: candidates } + } + } +} + +// THE ONE CONVERSION, AND THE ONLY EXPRESSION IN THIS CORPUS THAT BUILDS THE RECORD. Everything +// above is a reading; this is the step that says a tab was LOCATED, so it is the step that must be +// unreachable except from a caller that actually performed the read. It is admitted to exactly one +// production caller -- the live outcome route -- and to the named claims that assert the located +// payload, which cannot be asserted any other way once the folds stop returning the carrier. +fn review_tab_standing_from_classification( + spreadsheet_id: NonEmptyStr, + classified: ReviewTabClassification, +) -> ReviewTabStanding admit_callers: [ + decl_ref(module_path: "gunbc.review_sheet_tab_locator", decl_name: "review_tab_standing_of_outcome"), + decl_ref(module_path: "test.claim.review_sheet_tab_locator_witness", decl_name: "the_conversion_of_exactly_one_carries_the_observed_id_the_observed_title_and_the_read_subject"), + decl_ref(module_path: "test.claim.review_sheet_format_target_witness", decl_name: "located_tab_for_witness") +] { + match classified { + ClassifiedNone => TabAbsent + ClassifiedUnreadable { cause: c } => TabUnreadable { cause: c } + ClassifiedMany { candidates: cs } => TabAmbiguous { candidates: cs } + ClassifiedExactlyOne { candidate: c } => + TabLocated { + tab: LocatedReviewTab { spreadsheet_id: spreadsheet_id, sheet_id: c.sheet_id, title: c.title } + } + } +} + +fn first_review_tab_candidate(items: List) -> ReviewTabCandidate? { + fold_list( + items, + none, + (acc, x) => + match acc { + Present { value: v } => Present { value: v } + Absent => Present { value: x } + }, + ) +} + +// THE MASK IS THE THREE PROPERTIES THIS MODULE READS AND NOTHING ELSE. It selects no grid data, so +// the read does not grow with the census, and it names the three fields the candidate is built +// from -- a mask wider than the reading is a cost nobody asked for, and one narrower is a field +// that silently arrives absent. +data review_tab_locator_field_mask: String = sheets_field_mask(paths: [sheets_field_sheet_id, sheets_field_sheet_title, sheets_field_sheet_index]) + +// THE READ THAT MAKES THE MINT LEGITIMATE. Every arm that is not a 200 is TabUnreadable carrying +// the transport's own account of why, because a locator that answered TabAbsent to a 403 would +// send an operator to look for a missing tab in a spreadsheet they cannot open. +fn locate_review_tab(spreadsheet_id: NonEmptyStr) -> ReviewTabStanding uses net: Network { + let meta = sheets.Spreadsheets.GetSpreadsheetMetadata( + spreadsheet_id: spreadsheet_id as String, + fields: review_tab_locator_field_mask, + ) + review_tab_standing_of_outcome(spreadsheet_id: spreadsheet_id, outcome: meta.outcome, read: meta.result) +} + +// SEALED FOR THE SAME REASON THE MINT IS. This function calls the mint, so leaving it open would +// be a second door into a located tab: a caller handing it RestOk beside an authored response +// would obtain exactly what sole_constructor exists to prevent. A seal with an unsealed caller is +// not a weaker seal, it is no seal. +fn review_tab_standing_of_outcome( + spreadsheet_id: NonEmptyStr, + outcome: RestOutcome, + read: SpreadsheetRead, +) -> ReviewTabStanding admit_callers: [ + decl_ref(module_path: "gunbc.review_sheet_tab_locator", decl_name: "locate_review_tab"), + decl_ref(module_path: "test.claim.review_sheet_tab_locator_witness", decl_name: "a_refused_status_is_unreadable_and_carries_the_status_rather_than_reading_as_absent") +] { + match classify_rest_outcome(standing: RestReadExchange { rest: outcome }) { + RestExchangeSucceeded => + review_tab_standing_from_classification( + spreadsheet_id: spreadsheet_id, + classified: classify_review_tabs(read: read), + ) + RestExchangeStatusRefused { status, body } => + TabUnreadable { + cause: join(["the tab metadata read answered ", to_string(status), ": ", body], "") as NonEmptyStr + } + RestExchangeUnreached { cause } => + TabUnreadable { + cause: join(["the tab metadata read never reached Sheets: ", cause as String], "") as NonEmptyStr + } + RestExchangeUndecodable { status, cause } => + TabUnreadable { + cause: join(["the tab metadata read answered ", to_string(status), " with a body this model could not decode: ", cause as String], "") as NonEmptyStr + } + RestExchangeCommitAmbiguous { detail } => + TabUnreadable { + cause: join(["the tab metadata read is a read and reported an ambiguous commit: ", detail], "") as NonEmptyStr + } + } +} + +fn review_tab_candidate_text(c: ReviewTabCandidate) -> String { + join(["sheetId ", to_string(c.sheet_id), " titled ", c.title as String, " at index ", to_string(c.index)], "") +} + +fn review_tab_standing_text(s: ReviewTabStanding) -> String { + match s { + TabLocated { tab: t } => + join(["located tab: sheetId ", to_string(t.sheet_id), " titled ", t.title as String, " in ", t.spreadsheet_id as String], "") + TabAbsent => "no tab: spreadsheets.get answered with no sheets for this spreadsheet, so there is nothing to format" + TabAmbiguous { candidates: cs } => + join( + [ + "AMBIGUOUS: this spreadsheet carries ", to_string(count(cs)), + " tabs and nothing observable says which is the review tab (", + join(map(cs, c => review_tab_candidate_text(c: c)), "; "), + "); only an operator can adjudicate", + ], + "", + ) + TabUnreadable { cause: c } => join(["tab UNREADABLE: ", c as String], "") + } +} diff --git a/dag/test/claim/review_sheet_format_target_witness_test.dag b/dag/test/claim/review_sheet_format_target_witness_test.dag new file mode 100644 index 00000000000..0a1492cc1f5 --- /dev/null +++ b/dag/test/claim/review_sheet_format_target_witness_test.dag @@ -0,0 +1,317 @@ +module test.claim.review_sheet_format_target_witness + +import std.types { Bool, String, NonEmptyStr, Int, List } +import std.decl_ref { decl_ref } +import extdeps.google.sheets { + SpreadsheetRead, + SheetsSheetRead, + SheetsSheetPropertiesRead, + sheets_field_sheet_id, + sheets_sheet_id_read, +} +import gunbc.review_sheet_tab_locator { + ReviewTabStanding, + TabLocated, + TabAbsent, + TabAmbiguous, + TabUnreadable, + LocatedReviewTab, + review_tab_standing_from_classification, + ReviewTabCandidate, + ClassifiedExactlyOne, +} +import gunbc.review_sheet_format_actuator { + FormatRequestPlan, + format_request_plan, + review_sheet_format_grid_field_mask, + review_sheet_format_meta_field_mask, + located_sheet, + HeaderRangeStanding, + HeaderRangeWire, + HeaderRangeUnqualifiable, + review_sheet_header_range, + review_sheet_header_cells, +} +import gunbc.review_sheet_projection { + ci_prospect_sheet_schema, + validate_header_schema, + ValidatedHeaderSchema, + HeaderSchemaValidated, + HeaderSchemaRefused, +} + +// THE SUBJECT IS THE ADDRESSING, NOT THE FORMATTING. gunbc.review_sheet_format_actuator sends +// three kinds of batchUpdate request and every one of them names a sheetId. Until this change all +// seven named a first-sheet constant of 0 -- so the +// formatter wrote to whichever tab happened to be first in a workbook whose tab identity nothing +// had established. format_request_plan derives all seven from a located tab BEFORE any is sent, +// which is what makes the addressing a value a claim can read. +// +// WHAT THIS DISCRIMINATES AND WHAT IT DOES NOT. It reddens on a plan built from the constant, on a +// plan that takes its id from anywhere but the located tab, and on a header range that is not +// qualified by the located title. It does NOT reach the wire: a step function rewritten to ignore +// the request it was handed would pass this, and closing that needs the three batchUpdate +// operations in extdeps.google.sheets_mock_corpus, which carries only GetValues and +// BatchUpdateValues. That is the trigger, stated rather than implied. + +// THE ONLY WAY TO A LocatedReviewTab, HERE AS ANYWHERE -- AND THIS FUNCTION IS ITSELF SEALED. +// The carrier is sole_constructor and its one conversion is admit_callers-sealed, so this witness +// cannot write the record it needs. But being an ADMITTED caller is not the same as being a +// confined one: an earlier cut left this function exported and unrestricted while it was admitted +// to the mint, so any module in the corpus could import it and obtain a located tab from values +// it chose (side-chat hold on gunbc#11725). An admitted call edge does not confine a value when +// an exported wrapper returns that value or a carrier containing it -- so the wrapper is sealed +// to the exact claims that consume it, by name, and adding a claim means adding a row here. +fn located_tab_for_witness(sheet_id: Int, title: String) -> ReviewTabStanding admit_callers: [ + decl_ref(module_path: "test.claim.review_sheet_format_target_witness", decl_name: "plan_sheet_ids_with"), + decl_ref(module_path: "test.claim.review_sheet_format_target_witness", decl_name: "the_header_read_range_is_qualified_by_the_located_tab_title"), + decl_ref(module_path: "test.claim.review_sheet_format_target_witness", decl_name: "a_title_with_a_space_is_quoted_by_the_codec_rather_than_declined"), + decl_ref(module_path: "test.claim.review_sheet_format_target_witness", decl_name: "a_title_with_an_apostrophe_declines_the_range_rather_than_guessing_an_escape") +] { + review_tab_standing_from_classification( + spreadsheet_id: "1ciProspectSheetFileId" as NonEmptyStr, + classified: ClassifiedExactlyOne { + candidate: ReviewTabCandidate { sheet_id: sheet_id, title: title as NonEmptyStr, index: 0 } + }, + ) +} + +data witness_located_sheet_id: Int = 1836271154 + +// THE FOLD IS THE WITNESS'S, NOT THE ACTUATOR'S. An earlier cut declared +// format_plan_sheet_ids beside format_request_plan, where no production caller ever read it -- +// a declaration whose only consumer is a claim, which DESIGN section 3c calls dangling +// (review 68522). FormatRequestPlan's fields are readable from here, so the claim reads the +// record production really builds and the actuator declares nothing for the test's benefit. +fn plan_sheet_ids(plan: FormatRequestPlan) -> List { + [ + plan.freeze.sheet_id, plan.header.sheet_id, plan.opportunity.sheet_id, + plan.arbitrage.sheet_id, plan.incompatible.sheet_id, plan.required.sheet_id, + plan.replay.sheet_id, + ] +} + +// THE FORMATTER NOW REQUIRES TWO SEALED CARRIERS AND NEITHER CAN BE SUPPLIED BY ASSERTION. +// gunbc#11705 landed ValidatedHeaderSchema while this change was in review, so the plan takes a +// validated schema beside the located tab. The witness obtains the first the only way anyone can, +// by running validate_header_schema over the real production schema -- which also makes this an +// inhabitance claim for that mint: if ci_prospect_sheet_schema ever stopped validating, every +// claim below would report the refusal rather than silently testing a shape nothing produces. +fn validated_for_witness() -> ValidatedHeaderSchema? { + match validate_header_schema(schema: ci_prospect_sheet_schema()) { + HeaderSchemaValidated { validated: v } => Present { value: v } + HeaderSchemaRefused { refusal: _, reason: _ } => none + } +} + +fn plan_sheet_ids_for(sheet_id: Int, title: String) -> List { + match validated_for_witness() { + Absent => [] + Present { value: v } => plan_sheet_ids_with(sheet_id: sheet_id, title: title, validated: v) + } +} + +fn plan_sheet_ids_with(sheet_id: Int, title: String, validated: ValidatedHeaderSchema) -> List { + match located_tab_for_witness(sheet_id: sheet_id, title: title) { + TabLocated { tab: t } => + plan_sheet_ids(plan: format_request_plan(tab: t, validated: validated, standing_col: 3)) + TabAbsent => [] + TabAmbiguous { candidates: _ } => [] + TabUnreadable { cause: _ } => [] + } +} + +// EVERY REQUEST, NOT ONE OF THEM. The freeze, the header band and the five conditional rules are +// seven separate batchUpdates and each carries its own sheetId, so a mutation that reverts ONE of +// them to the constant is exactly the defect a claim over a single request would miss. +test fn every_batch_update_request_in_the_plan_addresses_the_located_sheet_id() -> Bool { + plan_sheet_ids_for(sheet_id: witness_located_sheet_id, title: "Prospects 2026") + == [ + witness_located_sheet_id, witness_located_sheet_id, witness_located_sheet_id, + witness_located_sheet_id, witness_located_sheet_id, witness_located_sheet_id, + witness_located_sheet_id, + ] +} + +// THE POSITIVE CONTROL FOR THE ABOVE, and it is what makes the claim a measurement rather than a +// tautology. The witness id is deliberately not zero, so if the plan were still built from the +// first-sheet constant the claim above would read seven zeros; this asserts the two values really +// are distinguishable, so a green above cannot be an accident of them coinciding. +// +// IT COMPARES AGAINST THE LITERAL BECAUSE THE CONSTANT NO LONGER EXISTS. extdeps.google.sheets +// spreadsheet_first_sheet_id was deleted with its last production consumer (review 68663): once +// the formatter addressed a located tab, the only reference left in the corpus was this line, and +// a declaration whose only consumer is the claim about its own absence is the DESIGN section 3c +// dangling shape -- the same rule this change applied to itself for format_plan_sheet_ids. The +// discriminating power is unchanged: zero is what the removed assumption yielded. +test fn the_witness_sheet_id_is_not_the_first_sheet_index_the_formatter_used_to_address() -> Bool { + (witness_located_sheet_id == 0) == false +} + +// THE HEADER READ IS QUALIFIED BY THE LOCATED TITLE. An unqualified A1 range reads the first tab, +// which gunbc.review_sheet_sheets a1_readback_standing refuses in as many words -- and the +// formatter's readback was sending one. A readback that inspects a different tab from the one the +// writes address is not evidence about the writes at all. +test fn the_header_read_range_is_qualified_by_the_located_tab_title() -> Bool { + match located_tab_for_witness(sheet_id: witness_located_sheet_id, title: "Prospects2026") { + TabLocated { tab: t } => + match review_sheet_header_range(tab: t) { + HeaderRangeWire { range: r } => r == join(["'Prospects2026'", "!", review_sheet_header_cells], "") + HeaderRangeUnqualifiable { cause: _ } => false + } + TabAbsent => false + TabAmbiguous { candidates: _ } => false + TabUnreadable { cause: _ } => false + } +} + +// A TITLE WITH A SPACE ENCODES, AND THIS CLAIM ASSERTED THE OPPOSITE UNTIL gunbc#11703 LANDED. +// While no encoder existed this branch refused such a title, and the claim here pinned that +// refusal. Quoting makes a space legal, so the refusal was forbidding more than the evidence +// supported (DESIGN section 4d) and the claim was pinning the over-prohibition in place. Both are +// replaced by the real behaviour: extdeps.google.sheets a1_range_encode wraps the title and the +// range is usable. A claim is not owed its old verdict when the world it described has changed. +test fn a_title_with_a_space_is_quoted_by_the_codec_rather_than_declined() -> Bool { + match located_tab_for_witness(sheet_id: witness_located_sheet_id, title: "Prospects 2026") { + TabLocated { tab: t } => + match review_sheet_header_range(tab: t) { + HeaderRangeWire { range: r } => r == join(["'Prospects 2026'", "!", review_sheet_header_cells], "") + HeaderRangeUnqualifiable { cause: _ } => false + } + TabAbsent => false + TabAmbiguous { candidates: _ } => false + TabUnreadable { cause: _ } => false + } +} + +// AND THE ONE THING THE CODEC REALLY CANNOT SPELL STILL REFUSES. An apostrophe inside a quoted A1 +// title has no observed wire spelling -- extdeps.google.sheets a1_title_apostrophe_spelling_standing +// is TranscribedUncited and names the live read that would settle it -- so the encoder declines +// rather than guessing a doubling rule, and the formatter carries that refusal out with the +// codec's own text instead of substituting its own account of why. +test fn a_title_with_an_apostrophe_declines_the_range_rather_than_guessing_an_escape() -> Bool { + match located_tab_for_witness(sheet_id: witness_located_sheet_id, title: "Jon's Data") { + TabLocated { tab: t } => + match review_sheet_header_range(tab: t) { + HeaderRangeUnqualifiable { cause: c } => string_contains(s: c as String, pattern: "apostrophe") + HeaderRangeWire { range: _ } => false + } + TabAbsent => false + TabAmbiguous { candidates: _ } => false + TabUnreadable { cause: _ } => false + } +} + +// THE READBACK MUST BE ABLE TO FIND THE TAB THE WRITES ADDRESS, AND FOR ONE REVISION IT COULD NOT. +// Selecting the sheet by its located sheetId was landed while both field masks still asked for no +// sheetId, so the selector keyed on a field the request had suppressed: the grid read matched no +// sheet at all and the converge refused every workbook, and the metadata read matched only tab +// zero (review 68553). Every claim above stayed green through it, because all of them read the +// REQUEST PLAN and none of them ran the DECODE against a response shaped by the mask. These three +// close that gap at the seam where it opened. + +fn sheet_with_properties(sheet_id: Int) -> SheetsSheetRead { + SheetsSheetRead { + properties: Present { + value: SheetsSheetPropertiesRead { + sheetId: Present { value: sheet_id }, + title: none, + index: none, + gridProperties: none, + } + }, + data: none, + conditionalFormats: none, + } +} + +fn read_of(sheets_read: List) -> SpreadsheetRead { + SpreadsheetRead { spreadsheetId: none, sheets: Present { value: sheets_read } } +} + +// (a) THE DECODE FINDS THE LOCATED TAB, and it is asked for a non-zero id beside a zero one so a +// selector that still answered "the first sheet" would pick the wrong record and fail here. +test fn the_readback_selects_the_sheet_carrying_the_located_id_not_the_first_one() -> Bool { + match located_sheet( + read: read_of(sheets_read: [sheet_with_properties(sheet_id: 0), sheet_with_properties(sheet_id: 918273645)]), + sheet_id: 918273645, + ) { + Absent => false + Present { value: sheet } => + match sheet.properties { + Absent => false + Present { value: props } => + match props.sheetId { + Absent => false + Present { value: id } => id == 918273645 + } + } + } +} + +// (b) A RESPONSE CARRYING NO PROPERTIES FINDS NOTHING, which is the shape the narrow grid mask +// produced. The arm itself is correct -- an unread sheet may not be adopted -- and the defect was +// that the REQUEST guaranteed this arm for every tab. Asserting it here pins the decode's honest +// behaviour so the mask claims below carry the whole weight of the repair. +test fn a_response_with_no_properties_locates_no_sheet_rather_than_defaulting_to_the_first() -> Bool { + match located_sheet( + read: read_of(sheets_read: [SheetsSheetRead { properties: none, data: none, conditionalFormats: none }]), + sheet_id: 918273645, + ) { + Absent => true + Present { value: _ } => false + } +} + +// (c) BOTH MASKS REQUEST THE FIELD THE SELECTOR KEYS ON. This is the claim that would have caught +// the defect, and it is an identity join rather than a spelling check: the masks are composed +// from extdeps.google.sheets sheets_field_sheet_id and this asserts that same row is present in +// each, so a mask narrowed back to its old spelling reddens here. +test fn both_readback_masks_request_the_sheet_id_the_selector_keys_on() -> Bool { + string_contains(s: review_sheet_format_grid_field_mask, pattern: sheets_field_sheet_id) + && string_contains(s: review_sheet_format_meta_field_mask, pattern: sheets_field_sheet_id) +} + +// (d) THE ORDINARY WORKBOOK, WHICH NO CLAIM ABOVE REACHES. Every id asserted so far is explicitly +// present and non-zero, chosen so a lingering first-sheet assumption could not pass by +// coincidence. That left the COMMON 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 +// on essentially every real run the response carries properties with NO sheetId and the located id +// is 0. The selector reaches that case through extdeps.google.sheets sheets_sheet_id_read, and a +// predicate that answered false to an absent id would refuse the very workbooks this pipeline +// creates while every claim above stayed green. +// +// This gap was found by writing a mutation and discovering nothing reddened, which is the same +// lesson as review 68553 one layer in: the claims clustered where the thinking was, and the case +// left unexercised was the ordinary one. +fn sheet_with_omitted_id() -> SheetsSheetRead { + SheetsSheetRead { + properties: Present { + value: SheetsSheetPropertiesRead { sheetId: none, title: none, index: none, gridProperties: none } + }, + data: none, + conditionalFormats: none, + } +} + +test fn a_tab_zero_workbook_whose_response_omits_the_sheet_id_is_still_located() -> Bool { + match located_sheet(read: read_of(sheets_read: [sheet_with_omitted_id()]), sheet_id: 0) { + Absent => false + Present { value: sheet } => + match sheet.properties { + Absent => false + Present { value: props } => sheets_sheet_id_read(id: props.sheetId) == 0 + } + } +} + +// AND THE OMISSION IS NOT A WILDCARD. The arm above must not become "an absent id matches +// anything": a workbook whose response omitted the id is tab zero, so a selector looking for a +// non-zero located tab must NOT adopt it. Without this, widening the absent arm to satisfy the +// claim above would silently reinstate take-the-first for every tab. +test fn an_omitted_sheet_id_does_not_match_a_non_zero_located_tab() -> Bool { + match located_sheet(read: read_of(sheets_read: [sheet_with_omitted_id()]), sheet_id: 918273645) { + Absent => true + Present { value: _ } => false + } +} diff --git a/dag/test/claim/review_sheet_tab_locator_witness_test.dag b/dag/test/claim/review_sheet_tab_locator_witness_test.dag new file mode 100644 index 00000000000..6977b868881 --- /dev/null +++ b/dag/test/claim/review_sheet_tab_locator_witness_test.dag @@ -0,0 +1,242 @@ +module test.claim.review_sheet_tab_locator_witness + +import std.types { Bool, String, NonEmptyStr, Int, List } +import extdeps.google.sheets { + SpreadsheetRead, + SheetsSheetRead, + SheetsSheetPropertiesRead, + sheets_sheet_id_read, + sheets_sheet_index_read, +} +import extdeps.transports.rest { RestOutcome, RestStatusRefused } +import gunbc.review_sheet_tab_locator { + ReviewTabStanding, + TabLocated, + TabAbsent, + TabAmbiguous, + TabUnreadable, + ReviewTabCandidate, + LocatedReviewTab, + classify_review_tabs, + review_tab_standing_from_classification, + ReviewTabClassification, + ClassifiedExactlyOne, + ClassifiedNone, + ClassifiedMany, + ClassifiedUnreadable, + review_tab_standing_of_outcome, +} + +// THE RESPONSES ARE SUPPLIED AT THIS INTERFACE AND THAT IS THE RULE RATHER THAN A SHORTCUT. +// DESIGN section 3's witness rule: a claim discriminates at ONE interface, and its inputs belong +// there as supplied values rather than as the output of executing the layers beneath. The subject +// here is classify_review_tabs -- what a spreadsheets.get response classifies as -- so +// the response is constructed. Executing Sheets to obtain one would make every claim below a claim +// about the network. +// +// THE PAIRED INHABITANCE, so this is not shape agreement standing in for execution. The real +// producer is gunbc.review_sheet_tab_locator locate_review_tab, whose route is +// gunbc.review_sheet_converge_cli converge_drive_half_cli -> format_located_tab -> +// locate_review_tab -> converge_review_sheet_format, and the last claim in this file asserts THAT +// ROUTE's own pure half: review_tab_standing_of_outcome, the function locate_review_tab hands its +// live outcome to, turns a real transport refusal into TabUnreadable rather than TabAbsent. The +// mint is admit_callers-sealed to that function and to the claims below by name, so no third +// caller can obtain a located tab from a supplied response. + +fn sheet_read(sheet_id: Int, title: String, index: Int) -> SheetsSheetRead { + SheetsSheetRead { + properties: Present { + value: SheetsSheetPropertiesRead { + sheetId: Present { value: sheet_id }, + title: Present { value: title }, + index: Present { value: index }, + gridProperties: none, + } + }, + data: none, + conditionalFormats: none, + } +} + +fn sheet_read_from_properties(props: SheetsSheetPropertiesRead) -> SheetsSheetRead { + SheetsSheetRead { properties: Present { value: props }, data: none, conditionalFormats: none } +} + +fn spreadsheet_read_of(sheets_read: List) -> SpreadsheetRead { + SpreadsheetRead { spreadsheetId: none, sheets: Present { value: sheets_read } } +} + +data witness_spreadsheet_id: NonEmptyStr = "1ciProspectSheetFileId" + +// (1) EXACTLY ONE TAB IS LOCATED, AND THE PAYLOAD IS ASSERTED RATHER THAN THE VARIANT. The ids are +// chosen so that neither could be produced by the assumption being removed: sheetId 1836271154 is +// not the constant zero, and the title "Prospects 2026" is not the Drive file's display name +// ("CI prospect sheet", gunbc.review_sheet_converge_cli ci_prospect_sheet_name). A mutation taking +// either from anywhere but properties fails this claim on the value, not on the arm. +test fn one_tab_is_located_with_the_observed_sheet_id_and_the_observed_title() -> Bool { + match classify_review_tabs( + read: spreadsheet_read_of(sheets_read: [sheet_read(sheet_id: 1836271154, title: "Prospects 2026", index: 0)]), + ) { + ClassifiedExactlyOne { candidate: c } => (c.sheet_id == 1836271154) && ((c.title as String) == "Prospects 2026") + ClassifiedNone => false + ClassifiedMany { candidates: _ } => false + ClassifiedUnreadable { cause: _ } => false + } +} + +// THE ONE CLAIM THAT NEEDS THE SEALED CONVERSION, and it is the only witness function admitted to +// it. Everything above discriminates the CLASSIFICATION, which authorizes nothing and therefore +// needs no admission -- an earlier cut admitted eight witness functions to the mint to assert the +// same facts, and every one of those admissions was a route a foreign module could take. This one +// asserts what the conversion produces: the observed id, the observed title, and the spreadsheet +// the read was performed against, which is the only place all three appear together. +test fn the_conversion_of_exactly_one_carries_the_observed_id_the_observed_title_and_the_read_subject() -> Bool { + match review_tab_standing_from_classification( + spreadsheet_id: witness_spreadsheet_id, + classified: ClassifiedExactlyOne { + candidate: ReviewTabCandidate { sheet_id: 4, title: "Sheet1" as NonEmptyStr, index: 0 } + }, + ) { + TabLocated { tab: t } => + (t.sheet_id == 4) + && ((t.title as String) == "Sheet1") + && ((t.spreadsheet_id as String) == (witness_spreadsheet_id as String)) + TabAbsent => false + TabAmbiguous { candidates: _ } => false + TabUnreadable { cause: _ } => false + } +} + +// (2) ZERO TABS IS ABSENT. A spreadsheet the response says has no sheets is a spreadsheet with +// nothing to format, and the remedy is to look at the request that asked -- not to send an +// operator hunting for an unreadable workbook. +test fn no_tabs_is_absent_rather_than_unreadable() -> Bool { + match classify_review_tabs(read: spreadsheet_read_of(sheets_read: [])) { + ClassifiedNone => true + ClassifiedExactlyOne { candidate: _ } => false + ClassifiedMany { candidates: _ } => false + ClassifiedUnreadable { cause: _ } => false + } +} + +test fn an_absent_sheets_field_is_absent_rather_than_unreadable() -> Bool { + match classify_review_tabs(read: SpreadsheetRead { spreadsheetId: none, sheets: none }) { + ClassifiedNone => true + ClassifiedExactlyOne { candidate: _ } => false + ClassifiedMany { candidates: _ } => false + ClassifiedUnreadable { cause: _ } => false + } +} + +fn candidate_ids(cs: List) -> List { + map(cs, c => c.sheet_id) +} + +fn candidate_titles(cs: List) -> List { + map(cs, c => c.title as String) +} + +// (3) TWO TABS ARE AMBIGUOUS AND BOTH ARE CARRIED. This is the claim the whole module exists for: +// the failure being removed is "take the first", which would answer TabLocated with sheetId 0 here +// and is exactly what the constant did. The candidate list is asserted at its payload so that an +// arm returning an empty TabAmbiguous -- refusing without saying what it saw -- also fails. +test fn two_tabs_are_ambiguous_and_the_candidates_carry_both_observed_ids_and_titles() -> Bool { + match classify_review_tabs( + read: spreadsheet_read_of( + sheets_read: [ + sheet_read(sheet_id: 0, title: "Sheet1", index: 0), + sheet_read(sheet_id: 918273645, title: "Prospects 2026", index: 1), + ], + ), + ) { + ClassifiedMany { candidates: cs } => + (count(cs) == 2) + && (candidate_ids(cs: cs) == [0, 918273645]) + && (candidate_titles(cs: cs) == ["Sheet1", "Prospects 2026"]) + ClassifiedExactlyOne { candidate: _ } => false + ClassifiedNone => false + ClassifiedUnreadable { cause: _ } => false + } +} + +// (4) AN UNREADABLE TAB. A sheet whose properties carry no title is not a tab named nothing: the +// proto3 default for a string is empty and upstream produces no tab with an empty title, so the +// field was not read. Substituting the Drive file's name there is mutation M2 in reverse and is +// what this arm forbids. +test fn a_tab_with_no_observed_title_is_unreadable_rather_than_named_by_this_module() -> Bool { + match classify_review_tabs( + read: spreadsheet_read_of( + sheets_read: [ + sheet_read_from_properties( + props: SheetsSheetPropertiesRead { sheetId: Present { value: 7 }, title: none, index: none, gridProperties: none } + ), + ], + ), + ) { + ClassifiedUnreadable { cause: c } => string_contains(s: c as String, pattern: "no title") + ClassifiedExactlyOne { candidate: _ } => false + ClassifiedNone => false + ClassifiedMany { candidates: _ } => false + } +} + +// (5) ONE UNREADABLE TAB POISONS THE WHOLE READING. A workbook whose second sheet came back +// without properties has an UNKNOWN number of tabs, so answering "exactly one" from the sheet that +// did parse is a confident answer derived from an incomplete reading -- the absorbing fallback +// DESIGN section 5 refuses, arriving as a skip rather than as a widen. +test fn an_unreadable_tab_beside_a_readable_one_poisons_the_reading_rather_than_being_skipped() -> Bool { + match classify_review_tabs( + read: spreadsheet_read_of( + sheets_read: [ + sheet_read(sheet_id: 55, title: "Prospects 2026", index: 0), + SheetsSheetRead { properties: none, data: none, conditionalFormats: none }, + ], + ), + ) { + ClassifiedUnreadable { cause: c } => string_contains(s: c as String, pattern: "no properties at all") + ClassifiedExactlyOne { candidate: _ } => false + ClassifiedNone => false + ClassifiedMany { candidates: _ } => false + } +} + +// (6) AN ABSENT sheetId IS ZERO AND MUST NOT REFUSE. This is the arm that keeps the locator usable +// on the workbooks this pipeline actually creates: Sheets omits a field equal to its proto3 +// default, a freshly minted workbook's only tab has sheetId 0, so the common case arrives with the +// id ABSENT. Reading it as zero is the decode extdeps.google.sheets sheets_sheet_id_read owns and +// the colour channels already ran under -- it is not a substituted default, and the claim is here +// so that a future tightening of the title arm cannot quietly take this one with it. +test fn the_first_tabs_absent_sheet_id_reads_as_zero_rather_than_refusing() -> Bool { + match classify_review_tabs( + read: spreadsheet_read_of( + sheets_read: [ + sheet_read_from_properties( + props: SheetsSheetPropertiesRead { sheetId: none, title: Present { value: "Sheet1" }, index: none, gridProperties: none } + ), + ], + ), + ) { + ClassifiedExactlyOne { candidate: c } => (c.sheet_id == 0) && ((c.title as String) == "Sheet1") + ClassifiedNone => false + ClassifiedMany { candidates: _ } => false + ClassifiedUnreadable { cause: _ } => false + } +} + +// (7) THE LIVE ROUTE'S OWN PURE HALF. locate_review_tab performs the read and hands the outcome +// here, so this is the function standing between a transport answer and a standing. A 403 is not +// a spreadsheet with no tabs, and answering TabAbsent to one would send an operator looking for a +// missing tab in a workbook they cannot open. The Absent-versus-refused distinction is the class +// gunbc.recurring_failure_mode rosters as absent_reads_identically_to_never_looked. +test fn a_refused_status_is_unreadable_and_carries_the_status_rather_than_reading_as_absent() -> Bool { + match review_tab_standing_of_outcome( + spreadsheet_id: witness_spreadsheet_id, + outcome: RestStatusRefused { status: 403, body: "caller lacks Sheets access" }, + read: SpreadsheetRead { spreadsheetId: none, sheets: none }, + ) { + TabUnreadable { cause: c } => string_contains(s: c as String, pattern: "403") + TabAbsent => false + TabLocated { tab: _ } => false + TabAmbiguous { candidates: _ } => false + } +} diff --git a/dag/test/claim/review_sheet_tab_refusal_probe_witness_test.dag b/dag/test/claim/review_sheet_tab_refusal_probe_witness_test.dag new file mode 100644 index 00000000000..f72b91dc018 --- /dev/null +++ b/dag/test/claim/review_sheet_tab_refusal_probe_witness_test.dag @@ -0,0 +1,155 @@ +module test.claim.review_sheet_tab_refusal_probe_witness + +import std.types { String, Bool, Int, List } +import extdeps.filesystem.filesystem_io +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, CompileDiagnosticCensusRow, CensusObserved, CensusNotRunnable, +} + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// THE FORGED LOCATED TABS, ENROLLED AS EXECUTED REDS. The locator's claim is that a caller cannot +// author a located tab -- not the record, not through the mint, not through the mint's caller -- +// and on the source-to-.dag acceptance path that claim is STRUCTURAL: the invalid state has no +// constructor in accepted code. DESIGN section 4b rules that this does not excuse the check. A +// state unrepresentable in the accepted corpus is still representable as SOURCE HANDED TO THE +// COMPILER BY A FIXTURE, and the compiler refusing it is the enrollable evidence. So +// test.probe.review_sheet_tab_forged_probe authors all three routes, this witness hands that +// source to the compiler through the same diagnostic-census harness the hold-plan and data-class +// probes use, and requires a BLOCKING row of the NAMED CLASS at the NAMED SUBJECT for each. A +// probe refusing for any other reason would be measuring another wall, which is why neither a +// nonzero exit nor a total count is what is asserted. + +data probe_dir: String = "dag/test/probe/" + +fn probe_source(name: String) -> String { + filesystem_read(path: probe_dir + name + ".dag").content +} + +fn census_of(source: String) -> CompileDiagnosticCensus { + compile_dag_diagnostic_census(source) +} + +fn blocking_count_for_class_and_subject(c: CompileDiagnosticCensus, wanted: String, subject: String) -> Int { + match c { + CensusNotRunnable { cause: _ } => -1 + CensusObserved { rows: rows } => + rows + |> filter(r => (r.diagnostic_class as String) == wanted && r.subject_name == subject && r.blocking) + |> fold(init: 0, f: (acc, r) => acc + r.count) + } +} + +// THE CONTROL IS SCOPED TO CLASS AND SUBJECT, NOT A TOTAL, AND THE TOTAL WAS TRIED FIRST. +// gunbc.compile_diagnostic_census says outright that CensusObserved carries EVERY diagnostic the +// compile produced, the imported closure included -- so a fixture importing any production module +// can never read zero blocking rows, and a control asserting blocking_total == 0 is a check whose +// RED is unauthorable: a decoration under DESIGN section 4b rather than a weak wall. It was +// written that way here and it failed, which is the only reason this note can be honest about it. +// +// The same authority names the two forms that ARE exact over one census: a count scoped to a class +// AND a subject_name, and a differential between two censuses differing on one axis. The three +// claims below are the first form, and together with the three probe claims they are also the +// second: same class, same subject, one axis moved -- a source that MENTIONS the locator versus a +// source that FORGES against it. That pairing is what makes the probe's refusals attributable to +// the forgeries rather than to naming the module at all, which a total could never have shown. +data harness_control_source: String = "module probe_review_sheet_tab_harness_control\nimport std.types { String }\nimport gunbc.review_sheet_tab_locator { review_tab_locator_field_mask }\nfn mask() -> String { review_tab_locator_field_mask }\n" + +test fn a_source_that_only_names_the_locator_forges_no_located_tab() -> Bool { + blocking_count_for_class_and_subject( + c: census_of(source: harness_control_source), + wanted: "SoleConstructorViolation", subject: "LocatedReviewTab", + ) == 0 +} + +test fn a_source_that_only_names_the_locator_is_refused_at_neither_sealed_mint() -> Bool { + (blocking_count_for_class_and_subject( + c: census_of(source: harness_control_source), + wanted: "ConstructorCallAdmissionRefused", subject: "review_tab_standing_from_classification", + ) == 0) + && (blocking_count_for_class_and_subject( + c: census_of(source: harness_control_source), + wanted: "ConstructorCallAdmissionRefused", subject: "review_tab_standing_of_outcome", + ) == 0) +} + +// (a) THE RECORD HAS NO CONSTRUCTOR OUTSIDE THE LOCATOR. A hand-built located tab carrying the +// constant sheet id is the exact regression this change removes, reintroduced under the name of an +// observation; it refuses at the record literal rather than being caught downstream. +test fn a_forged_located_tab_cannot_be_authored_outside_the_locator() -> Bool { + blocking_count_for_class_and_subject( + c: census_of(source: probe_source(name: "review_sheet_tab_forged_probe")), + wanted: "SoleConstructorViolation", subject: "LocatedReviewTab", + ) >= 1 +} + +// (b) THE MINT REFUSES AN UNADMITTED CALLER. sole_constructor alone would still let any module +// call the one function that builds the record with a response it authored, so the seal on the +// mint is what makes the record's seal mean anything. +test fn an_unadmitted_caller_cannot_mint_a_located_tab_from_a_supplied_classification() -> Bool { + blocking_count_for_class_and_subject( + c: census_of(source: probe_source(name: "review_sheet_tab_forged_probe")), + wanted: "ConstructorCallAdmissionRefused", subject: "review_tab_standing_from_classification", + ) >= 1 +} + +// (c) AND SO DOES THE MINT'S CALLER, at its own name. A seal with an unsealed caller is not a +// weaker seal, it is no seal, and the census keys the row by the CALLEE's declaration name -- so +// this is an identity join on the second door rather than a second count of the first. +test fn an_unadmitted_caller_cannot_reach_the_mint_through_the_outcome_classifier() -> Bool { + blocking_count_for_class_and_subject( + c: census_of(source: probe_source(name: "review_sheet_tab_forged_probe")), + wanted: "ConstructorCallAdmissionRefused", subject: "review_tab_standing_of_outcome", + ) >= 1 +} + +// (d) AND THE WITNESS WRAPPER REFUSES TOO, which is the door the side-chat hold on gunbc#11725 +// found open. test.claim.review_sheet_format_target_witness located_tab_for_witness is ADMITTED to +// the conversion, and for one revision that was all it was: exported, unrestricted, and therefore +// a route by which any module could obtain a located tab from values it chose. An admitted call +// edge does not confine a value when an exported wrapper returns that value or a carrier +// containing it, so the wrapper carries its own admission list and this asserts it by name. +test fn an_unadmitted_caller_cannot_reach_a_located_tab_through_the_witness_wrapper() -> Bool { + blocking_count_for_class_and_subject( + c: census_of(source: probe_source(name: "review_sheet_tab_forged_probe")), + wanted: "ConstructorCallAdmissionRefused", subject: "located_tab_for_witness", + ) >= 1 +} + +// (e) THE FORMAT EFFECTS CANNOT BE REACHED WITHOUT A LOCATED TAB. Each batchUpdate function takes +// a request record, and while those records were ordinary a foreign module could author one and +// format an arbitrary tab of an arbitrary workbook without a LocatedReviewTab, a validated schema +// or a converge -- the production entry required a located tab and the effects did not. The +// closure is on the INPUT rather than on the five callers: every record is sole_constructor and +// its only mints require a located tab, so the refusal lands at the RECORD. That is why these +// four claims name record types rather than callees, and it is the stronger form -- an +// unconstructible argument cannot reach those functions by any route, named or unnamed, so +// confinement does not depend on an admission list staying complete as the module grows. +test fn a_freeze_request_cannot_be_authored_outside_the_located_builders() -> Bool { + blocking_count_for_class_and_subject( + c: census_of(source: probe_source(name: "review_sheet_tab_forged_probe")), + wanted: "SoleConstructorViolation", subject: "FreezeRowsRequest", + ) >= 1 +} + +test fn a_header_band_request_cannot_be_authored_outside_the_located_builders() -> Bool { + blocking_count_for_class_and_subject( + c: census_of(source: probe_source(name: "review_sheet_tab_forged_probe")), + wanted: "SoleConstructorViolation", subject: "HeaderBandRequest", + ) >= 1 +} + +test fn a_standing_rule_request_cannot_be_authored_outside_the_located_builders() -> Bool { + blocking_count_for_class_and_subject( + c: census_of(source: probe_source(name: "review_sheet_tab_forged_probe")), + wanted: "SoleConstructorViolation", subject: "StandingRuleRequest", + ) >= 1 +} + +test fn a_whole_format_plan_cannot_be_authored_outside_the_located_builders() -> Bool { + blocking_count_for_class_and_subject( + c: census_of(source: probe_source(name: "review_sheet_tab_forged_probe")), + wanted: "SoleConstructorViolation", subject: "FormatRequestPlan", + ) >= 1 +} diff --git a/dag/test/probe/review_sheet_tab_forged_probe.dag b/dag/test/probe/review_sheet_tab_forged_probe.dag new file mode 100644 index 00000000000..3062aec4b9e --- /dev/null +++ b/dag/test/probe/review_sheet_tab_forged_probe.dag @@ -0,0 +1,156 @@ +module test.probe.review_sheet_tab_forged_probe + +// THIS MODULE MUST NOT RESOLVE. A located review tab is minted only by +// gunbc.review_sheet_tab_locator, and only by the function that performed the spreadsheets.get +// metadata read -- the same egress discipline gunbc.durable_exclusive_hold_file_store states for +// its sealed plans. The three forgeries below are the three routes a caller would otherwise take, +// and each one reinstates the defect the locator exists to remove. +// +// (a) THE RECORD ITSELF. A hand-built LocatedReviewTab { sheet_id: 0 } is the constant +// the first-sheet constant 0 wearing the name of an observation: handed to +// converge_review_sheet_format it addresses tab zero again, and every refusal downstream of it +// reads "the located tab" while the located tab was a literal. LocatedReviewTab is +// sole_constructor, so this refuses at the record as SoleConstructorViolation. +// +// (b) THE CONVERSION, CALLED WITH AN AUTHORED CLASSIFICATION. review_tab_standing_from_classification +// is the only expression in the corpus that builds the record, and a caller handing it a +// ClassifiedExactlyOne it wrote would obtain a TabLocated for a tab it chose rather than one it +// read. Sealed to the live outcome route and two named claims, so this refuses. +// +// (d) THE WITNESS WRAPPER. Being ADMITTED to the conversion did not make this function confined: +// while it was exported and unrestricted, any module could import it and get a located tab from +// values it chose, which is the escape the side-chat hold on gunbc#11725 named. It is now sealed +// to the exact claims that consume it, so this call refuses at its name. +// +// (c) THE CONVERSION'S CALLER. review_tab_standing_of_outcome takes the transport outcome beside the +// response, so leaving it open would be a second door: RestOk beside an authored body reaches the +// same mint. It is sealed for exactly that reason and refuses at its own name. +// +// The witness test.claim.review_sheet_tab_refusal_probe_witness enrolls this probe and asserts +// each refusal class at its subject by name. dag/test/probe/ sits under the whole-tree +// strict-resolve exclusion, so this source reaches the compiler only through that witness. + +import std.types { NonEmptyStr, String, Int } +import std.resources { Network } +import extdeps.transports.rest { RestOutcome, RestOk } +import extdeps.google.sheets { SpreadsheetRead, SheetsSheetRead, SheetsSheetPropertiesRead } +import gunbc.review_sheet_tab_locator { + LocatedReviewTab, + ReviewTabStanding, + ReviewTabCandidate, + ReviewTabClassification, + ClassifiedExactlyOne, + review_tab_standing_from_classification, + review_tab_standing_of_outcome, +} +import test.claim.review_sheet_format_target_witness { located_tab_for_witness } +import gunbc.review_sheet_format_actuator { + FreezeRowsRequest, + HeaderBandRequest, + StandingRuleRequest, + FormatRequestPlan, + FormatStepOutcome, + FormatReport, + freeze_header, + format_header_band, + color_standing, + format_review_sheet, + standing_admitted_color, +} + +fn forged_located_tab_over_the_constant_sheet_id(spreadsheet_id: NonEmptyStr) -> LocatedReviewTab { + LocatedReviewTab { + spreadsheet_id: spreadsheet_id, + sheet_id: 0, + title: "CI prospect sheet" as NonEmptyStr, + } +} + +fn authored_single_tab_response(sheet_id: Int, title: String) -> SpreadsheetRead { + SpreadsheetRead { + spreadsheetId: none, + sheets: Present { + value: [ + SheetsSheetRead { + properties: Present { + value: SheetsSheetPropertiesRead { + sheetId: Present { value: sheet_id }, + title: Present { value: title }, + index: Present { value: 0 }, + gridProperties: none, + } + }, + data: none, + conditionalFormats: none, + }, + ] + }, + } +} + +fn mint_a_located_tab_from_an_authored_classification(spreadsheet_id: NonEmptyStr) -> ReviewTabStanding { + review_tab_standing_from_classification( + spreadsheet_id: spreadsheet_id, + classified: ClassifiedExactlyOne { + candidate: ReviewTabCandidate { sheet_id: 0, title: "Sheet1" as NonEmptyStr, index: 0 } + }, + ) +} + +fn mint_a_located_tab_through_the_witness_wrapper() -> ReviewTabStanding { + located_tab_for_witness(sheet_id: 0, title: "Sheet1") +} + +fn mint_a_located_tab_from_an_authored_ok_outcome(spreadsheet_id: NonEmptyStr) -> ReviewTabStanding { + review_tab_standing_of_outcome( + spreadsheet_id: spreadsheet_id, + outcome: RestOk, + read: authored_single_tab_response(sheet_id: 0, title: "Sheet1"), + ) +} + +// (e) THE FORMAT EFFECTS, REACHED WITHOUT A LOCATED TAB AT ALL. Each batchUpdate function takes a +// request record, and while those records were ordinary this module could author one and format an +// arbitrary tab of an arbitrary workbook -- no LocatedReviewTab, no validated schema, no converge. +// The production entry required a located tab; the effects did not, which is the same +// admitted-edge-does-not-confine-a-value class one layer out from the carrier. Every record is now +// sole_constructor with its only mints requiring a LocatedReviewTab, so each literal below refuses +// at the RECORD rather than at the callee -- a stronger closure than sealing the five functions, +// because an unconstructible argument cannot reach them by any route, named or unnamed. +fn forge_a_freeze_of_an_arbitrary_tab() -> FormatStepOutcome uses net: Network { + freeze_header( + q: FreezeRowsRequest { spreadsheet_id: "someone-elses-workbook", sheet_id: 7, frozen_row_count: 1 } + ) +} + +fn forge_a_header_band_on_an_arbitrary_tab() -> FormatStepOutcome uses net: Network { + format_header_band( + q: HeaderBandRequest { + spreadsheet_id: "someone-elses-workbook", sheet_id: 7, + start_row: 0, end_row: 1, start_col: 0, end_col: 17, + } + ) +} + +fn forge_a_standing_rule_on_an_arbitrary_tab() -> FormatStepOutcome uses net: Network { + color_standing( + q: StandingRuleRequest { + spreadsheet_id: "someone-elses-workbook", sheet_id: 7, + start_row: 1, start_col: 3, end_col: 4, match_text: "Opportunity", rule_index: 0, + }, + color: standing_admitted_color(), + ) +} + +fn forge_every_mutation_from_an_authored_plan( + freeze: FreezeRowsRequest, + header: HeaderBandRequest, + rule: StandingRuleRequest, +) -> FormatReport uses net: Network { + format_review_sheet( + plan: FormatRequestPlan { + freeze: freeze, header: header, opportunity: rule, arbitrage: rule, + incompatible: rule, required: rule, replay: rule, + } + ) +}