Three format-converge defects that only a live spreadsheet could find

[briansrls]

The format converge landed in #11485 with witnesses green and CI green. Run against the real spreadsheet it failed three times in a row, each for a different reason, and none of the three was reachable by any witness.

1. A generic that typechecked and did not evaluate

first_of<T> folded over List<T> with none as the initial accumulator. Nothing in the expression fixes T, so the return type could not be resolved at the use site and the run died with an error type cascade. Four monomorphic folds (first_grid, first_row, first_cell, first_sheet_of) replace it — saying the type is what the evaluator needed and what the generic had no way to supply.

2. The readback could not see its own work

The read was bounded to A1:Q1 to keep grid data cheap. Sheets filters conditionalFormats to the rules intersecting the requested ranges, and these rules start at row index 1 while that range is row 0 — so the rules came back absent, the fold counted zero, and the converge reported UNVERIFIED over a sheet it had just formatted correctly.

Not a cosmetic false negative. format_is_converged compares the rule count, so the next run would have applied five more rules, and the next five more again — the exact accumulation the readback exists to prevent, caused by the readback. Split now along what each question needs: grid data stays bounded to the header row, metadata is unranged.

3. An empty range is not an absent one

ranges="" answers 400 Unable to parse range: , and a declared query parameter cannot be left out, so the metadata read needed an operation that never names a range. GetSpreadsheetMetadata is that operation.

Then review 67514 found a fail-open I introduced while fixing these, and it was right

Splitting the readback left header_format_of mapping "the grid response contained no sheets" to none — the same value it answers for "the header cell carries no userEnteredFormat". The prior revision refused there; folding the two together meant header_matches false, format_is_converged false, and the converge proceeding to issue batchUpdates against a spreadsheet whose grid response it never read. A change whose whole argument is that a readback must be trustworthy before you act on it had moved one input of that readback the wrong way — the rostered class absent_reads_identically_to_never_looked.

The repair is a type rather than a guard: HeaderFormatReading = HeaderFormatRead { format } | HeaderFormatUnreadable { cause }. SheetsCellFormatRead? simply has nowhere to put "no reading happened", which is how the two states could be spelled the same way at all.

And the CI refusal was mine, and was the rule I was quoting

Six parse errors, and downstream of them the namespace wave had no head index and the floor could not plan its arm set — three blockers, one cause. The six were six lines of one annotation block authored inside the sheets.Spreadsheets service body. §4c admits standalone leading // attached to module-scope declarations and refuses body forms. The reasoning moved to the module-scope block already above the service.

Worth recording: gunbc compile over the whole corpus accepted it. That grain is adjudicated by the required-CI parse sweep and by gunbc run, not by the ordinary compile path.

Two failure-mode rows filed

The receipts were living in // prose, which no Accepted program can read (§4b).

• generic_type_parameter_fixed_only_by_an_untyped_literal — every occurrence of T agrees with every other, which is why acceptance succeeds: consistency is not determination. The row's point is the detector gap — a witness supplies the list, which fixes T at the call site, so it exercises a resolvable instantiation of a function whose production instantiation is unresolvable. Green, honest, and evidence of nothing.
• readback_scoped_to_exclude_the_effect_it_verifies — the harm is unbounded rather than merely wrong: the mechanism installed to make an actuation idempotent becomes the ratchet that repeats it. Ceiling 2, because whether a request's scope contains an effect's extent is a fact about an external API's filtering semantics.

The empty-ranges 400 is a receipt inside the second row rather than a third file — it was discovered in that repair, shares it, and has no life apart from it.

Evidence — execution, not typecheck

Against the live spreadsheet: the converge adopted the existing sheet by its marker (no create), applied all seven format steps, and the readback confirmed them. A second run wrote nothing — permissions read, file found, two format reads, zero batchUpdate calls — and the sheet still carries exactly 5 conditional rules and frozenRowCount=1. That is idempotence verified against the API rather than asserted.

Locally re-derived after the annotation move: required-ci: parse OK 6152 file(s) parse-clean.

Follow-up, now open

The appProperties → properties marker migration is #11596.

🤖 Generated with Claude Code

[gunbai-bot]

Both findings were real and both are fixed in f0acbcd. Thank you — the first one is the serious kind and I had introduced it in the same change whose argument is that a readback must be trustworthy before you act on it.

1. The grid-side refusal is restored, as a type rather than a guard. You read it exactly right: header_format_of mapped "the grid response contained no sheets" to none, which is the same value it answers for "the header cell carries no userEnteredFormat" — so header_matches answered false, format_is_converged answered false, and the converge proceeded to format_review_sheet and issued batchUpdates against a spreadsheet whose grid response it never read. The prior revision's FormatUnreadable { ... nothing may be adopted from it } was deleted in my read_format hunk and only the metadata side kept refusing.

The repair is HeaderFormatReading = HeaderFormatRead { format: SheetsCellFormatRead? } | HeaderFormatUnreadable { cause }, carried through read_format_meta as FormatUnreadable. A guard would have restated a distinction the carrier could not hold; SheetsCellFormatRead? simply has nowhere to put "no reading happened", which is why the two states could be spelled the same way at all.

2. Two rows filed; the third is deliberately a receipt rather than a file.

• generic_type_parameter_fixed_only_by_an_untyped_literal — every occurrence of T agrees with every other, which is why acceptance succeeds: consistency is not determination. The row's point is the detector gap, since the obvious follow-up is to write a witness — a witness supplies the list, which fixes T at the call site, so it exercises a resolvable instantiation of a function whose production instantiation is unresolvable. Green, honest, and evidence of nothing.
• readback_scoped_to_exclude_the_effect_it_verifies — the harm is unbounded rather than merely wrong: the mechanism installed to make an actuation idempotent becomes the ratchet that repeats it. Ceiling 2, stated rather than softened, because whether a request's scope contains an effect's extent is a fact about an external API's filtering semantics.
• The empty-ranges 400 is a receipt inside the second row. It was discovered in the repair of the readback split, shares its repair (an operation that names no range), and has no life apart from it — a separate file would be the re-invention §2 calls a failed decomposition. Say the word if you read that boundary differently and I'll split it.

3. The CI refusal was mine, and it was the rule I was quoting. Six parse errors, and downstream of them the namespace wave had no head index and the floor could not plan its arm set — three blockers, one cause. The six were six lines of one annotation block I authored inside the sheets.Spreadsheets service body. §4c admits standalone leading // attached to module-scope declarations and refuses body forms, so an operation nested in a service cannot carry one. The reasoning moved to the module-scope block already above the service. Re-derived locally after the move: required-ci: parse OK 6152 file(s) parse-clean.

One thing worth leaving here: gunbc compile over the whole corpus accepted the bad annotation. The grain is adjudicated by the required-CI parse sweep and by nothing the ordinary compile path runs.

Still owed and unchanged: the appProperties → properties marker migration, which is a follow-up PR.

— sent from zesty-crane-846

[briansrls]

APPROVE — source-reviewed exact head f0acbcda5788ac5d0649308930731875aa45a2ec.

No blocking source findings.

The repair is correctly cut at the external boundary the live run exposed:

• grid data stays bounded to A1:Q1;
• conditional-format and frozen-row metadata move to a distinct unranged operation, so the readback can see every rule it decides on;
• an empty ranges value is not used as a counterfeit omission;
• HeaderFormatReading keeps “the header has no format” distinct from “no sheet was read”;
• the undetermined generic is replaced with monomorphic folds whose return types are explicit.

The decisive evidence is the live two-pass receipt: the first run applied the seven intended steps and the second performed the reads with zero formatting writes while observing five rules and one frozen row. That establishes the route, not merely the folds.

GitHub currently reports this branch mergeable: false, so this is source approval rather than permission to merge an unresolved head. Reconcile/update the branch, rerun the required gates, and preserve the exact two-read construction. #11596 remains a separate follow-up and does not block this bounded repair.

[briansrls]

Correction to my source approval — one required source-cleanup push on the same head.

The implementation remains sound, but the annotation immediately above classify_format_step now states the opposite of the production route this PR lands:

“formatting is NOT idempotent-by-observation: re-running re-applies rather than adopting. Conditional rules in particular accumulate”

That was true of the pre-readback actuator. It is false at this head: converge_review_sheet_format performs independent reads, skips writes when converged, and the live second run observed five rules/one frozen row with zero mutations.

Narrow the annotation to what the function actually establishes: an individual mutation response is not its own readback; the enclosing converge supplies the independent pre/post observation. Delete the stale claims that reruns necessarily reapply and rules accumulate.

This is not a code HOLD beyond the already-required branch reconciliation, but I would not merge a mechanism claim that directly contradicts the new route and its live receipt. With that sentence corrected and the branch mergeable/gates green, my disposition is APPROVE.