Formula-preserving whole-tab emptiness carrier + header-init planner (revised #11613)

[gunbai-bot]

FINAL STATE (hand-off, 2026-09-20 — the session was stopped by operator instruction under host load)

Head: 10afa61ce038f1a61e1bb9d616fa14d606bebc5b (pushed; two dashboard approvals, no findings; a side-chat REQUEST_CHANGES on 5a2eaaa asked for the M20 boundary extraction, which this head implements). Working tree clean; no unpushed work.

Witnesses at 10afa61 (local, interpreter sha256 34ac855d6b869902… built from 124208f — no Rust changed since; gunbc run --claim-run --dry-run, exit unpiped): review_sheet_header_init_witness_test 26/26 exit 0 (7 [hermetic:mock] hits); review_sheet_header_init_refusal_probe_witness_test 6/6 exit 0. At 5a2eaaa (no file they reach changed since): converge 92/92, batch_actuator 28/28, a1_title 5/5, header_schema 12/12, sheets_a1_title_codec 10/10, all exit 0.

Mutation table, 21 registered. Run AT 10afa61 (9 rows, each exit 1 with exactly the named claim red, all others green): M1 (render-option fn → FORMATTED) red on the_render_option_the_mint_passes_is_formula; M2, M3 (bounded / column-bounded admitted); M4 (tab equality removed; 2 claims); M5, M6 (COLUMNS-major / unrecognised dimension read as rows); M7 (unreadable judged empty); M20 (formula_reading_from_admission's occupied arm mints the carrier) red on an_occupied_admission_never_becomes_the_carrier; M21 (the admit_callers seal on formula_reading_from_admission removed) red on an_outside_module_calling_the_minting_boundary_is_refused_at_that_callee. Carried forward from 5a2eaaa, NOT re-run at 10afa61 (their subjects are byte-identical between the two heads; the witness gained two claims and renamed one, none of which they discriminate): M8 (unnamed returned range judged empty; 2 claims), M9–M12 (first_occupied_*: row-1-only / whitespace / column-A-only / =-as-blank), M13 (span truncated to Z), M14 (admission ignores the grid; 6 claims), M15 (planner drops the carrier refusal), M16, M17 (sole_constructor removed; probe claims), M18 (lowering COLUMNS-major), M19 (mint binds another spreadsheet — the literal moved into formula_reading_from_admission; runner re-pointed, not yet re-run). All 12 were red on their named claims at 5a2eaaa. Applied at 10afa61: 9 of 21. A future session finishes by running M8…M19 in a separate copy of the tree (the runner at /tmp/sharp-ant-467-mut-logs/runner.py in this session's persisted /tmp; each row ~3 min locally at normal load, and each was killed at the 10-minute mark at load >150), then re-running the five landed witnesses at the final head.

Declared, not hidden: the render option at the wire is an effect-seam limitation (the hermetic mock ignores valueRenderOption); the named ground is an H2 live qualification against a temporary tab holding =IF(TRUE,"","") whose FORMULA reading must come back occupied at that cell. BuildBuddy cannot run these witnesses (every row exit 137 on the 7.6 GB runner, with or without a budget), and its GetLog keeps only ~10 KB of a job's output.

Open for H2 (the parent's call, not made here): the write itself — this PR lowers to a ValueRangeWrite; #11717's sealed wire takes a TabBoundWritePlan whose AppendListingRow needs a listing_id a header row lacks.

Summary

Revises the parked gunbc#11613 planner against the two findings ruled this lane's subject: (2) a FORMATTED_VALUE read cannot prove a tab holds no value or formula, and (4) two exported routes returned the header-row write authorization with no observation. Nothing from #11613's branch is reused.

1. gunbc.review_sheet_formula_observation — FormulaWholeTabObservation is sole_constructor; its only mint observe_formula_whole_tab(spreadsheet_id, requested: SheetA1Range) uses net performs the read itself: admit_whole_tab_request refuses a bounded / column-bounded / unencodable request before any read is spent; the read is read_values_rendered(..., RenderFormula) (the values actuator's one values.get call site, now parameterised by render option, read_values delegating with FORMATTED_VALUE); the returned range is decoded with the landed codec (a1_range_title_decode, Sheets A1 sheet-title codec: always quote, refuse apostrophe titles, decode the guide's form #11703) and must name the requested tab; the grid must be row-major (value_range_row_major, whose refusal is now the typed RowMajorRefusal = RangeColumnsMajor | RangeDimensionUnrecognised { raw }). Every discrepancy is an arm of FormulaWholeTabRefusal (FormulaRequestRejected { cause: SheetRequestCause }, FormulaReadUnreadable, FormulaReadRangeUnqualified, FormulaReadRangeRefused { refusal: A1SheetTitleRefusal }, FormulaReadTabMismatch { requested, returned }, FormulaReadNotRowMajor { cause: RowMajorRefusal }). Emptiness is decided in the mint: every cell of every row must be exactly "" (whitespace is content), and the carrier is minted ONLY for an empty tab — it carries spreadsheet_id and tab and no grid. An occupied tab is the unsealed, typed, located FormulaWholeTabOccupied { spreadsheet_id, tab, first: OccupiedCell { sheet_row, column_index, raw } } arm of the reading, distinct from the request-shape and readback refusals. No render field. The annotation states the fact at its width: value/formula emptiness of the whole tab at the moment of that read, nothing about notes, formatting, validation, protected ranges, merges.
2. gunbc.review_sheet_header_init — plan_header_init(reading: FormulaWholeTabReading, validated: ValidatedHeaderSchema) -> HeaderInitPlan is the only mint of HeaderRowWriteAuthorization (sole_constructor; spreadsheet, tab, encoded row-1 range, span, header cells). The planner holds no grid: the write arm is reachable only from the sealed carrier, and an occupied reading maps to the located occupied arm by construction. Arms: HeaderInitWriteHeaderRow, HeaderInitTabOccupied { tab, first }, HeaderInitHeaderRowUnaddressable { tab, header_count, addressable_columns } (schema wider than a1_column_letters), HeaderInitTabTitleUnquotable (the codec's arm, unreachable in practice since the observation's tab already encoded at request time, kept so the fold is total), HeaderInitObservationRefused { refusal } (the carrier's refusals carried through). header_row_value_range_write(authorization) -> ValueRangeWrite is a projection off the sealed carrier (ROWS-major, one row).
3. No alternate mint. The carrier literal is written in exactly one function, formula_reading_from_admission(spreadsheet_id, admission) -> FormulaWholeTabReading — the pure map AFTER the read — which is admit_callers-sealed to observe_formula_whole_tab and to ONE exact Bool-returning witness claim (an_occupied_admission_never_becomes_the_carrier), so that boundary is executed against a supplied FormulaGridOccupied; the seal itself is measured by a compile-census probe (ConstructorCallAdmissionRefused at the callee by name, with a green control calling the public observer). formula_grid_admit(requested, read) and header_row_span(validated) are public so a witness can redden them and return a verdict / a span — neither the carrier, the authorization nor a plan.

Boundary stated, not claimed: WHO may call plan_header_init / observe_formula_whole_tab is not confined here (.dag has no module-private and the consumer is in another repository); the private H2 write permit in strategy.buyer_review_live confines it. H2 also performs the write: this PR lowers to a ValueRangeWrite and adds no second wire route beside #11717's sealed issue_batch_request (which takes a TabBoundWritePlan, whose AppendListingRow needs a listing_id a header row does not have — so H2 needs a header-row write primitive, or #11717's actuator widened; that is the parent's call and I have not made it).

Shared decisions factored, not copied: admit_whole_tab_request in review_sheet_sheets is now what review_sheet_ensure_assess uses too (same SheetRequestCause, one fold).

extdeps edit: extdeps.google.sheets GetValues gains a mock_response — an EMPTY whole tab named hermetic-mock-tab — following the github.Users / ntfy fixture precedent. This is what lets the mint be executed in a hermetic witness rather than declared. No hermetic witness called GetValues before (they refused fail-closed with "no mock_response"), so no existing evidence changes meaning.

Rung honesty (§4b), at the standing the evidence holds: (a) an occupied admission never becomes the carrier — EXECUTED at the minting boundary with a supplied occupied admission, and the planner-level ignore-the-grid is unwritable (no grid there); (b) that the mint reads under FORMULA rendering is NOT mechanically established: mock_response ignores valueRenderOption, so a call-site bypass is unobservable; the claim the_render_option_the_mint_passes_is_formula measures that function's value only. This is an effect-seam limitation until request-aware mocking or a live receipt — the named ground is an H2 live qualification against a temporary tab holding =IF(TRUE,"",""). Both sole_constructor walls are structural on the v1 seed's acceptance path only (native v2 parses the modifier without enforcing it: gunbc.rung_drop g0_type_decl_modifier_parse_without_sealing_property; the emitted-Rust mirror is a public struct). Not rung 4 unqualified. The source annotations carry exactly this standing.

Consumption (§3c): consumer is the private H2 transaction strategy.buyer_review_live, landing later. Frontier rows enrolled in gunbc.census_closure_frontier: observe_formula_whole_tab, plan_header_init, header_row_value_range_write, header_init_plan_text, each with that trigger. The live sequence H2 performs (FORMATTED read → ensure path if any content → else FORMULA read → only that carrier authorises header init; create-only admission rejected) is in the carrier's annotation.

Why the emptiness decision moved into the mint (the M14 correction)

The first cut of this PR carried the grid on the observation and let the planner scan it. The mutation table for that cut listed M14 — planner ignores the grid: an occupied observation still receives the header-row write — but I never entered it into the runner, because its RED looked unauthorable: the planner takes the sealed carrier, no witness can mint an occupied one, and the one hermetic fixture is empty. The parent asked for it to be accounted for and run. Run against that cut (match first_occupied_cell(rows: []) in plan_header_init), the mutation SURVIVED: exit 0, 24/24 PASS. The planner's safety arm — the arm finding (2) is about — was asserted and never measured, which is DESIGN §4b's "a red that is unauthorable in the accepted corpus is still authorable as a supplied value, and declining it is specification-without-execution".

The fix is construction, not another test: the emptiness decision now lives in the observation module's mint, FormulaWholeTabObservation exists only for an empty tab, and an occupied tab arrives at the planner as the unsealed, located FormulaWholeTabOccupied arm with no carrier at all. The planner has no grid to ignore, so the M14 of the first cut is now unwritable; the emptiness fold is executed over supplied grids at formula_grid_admit, the planner's occupied arm is executed with a supplied reading (an_occupied_reading_is_planned_as_occupied_never_as_a_write), and the re-pointed M14 (the mint's admission ignores the grid) reddens six claims. Both modules' annotations state this as the reason for their shape.

Evidence — local runs are the evidence

CI: after #11761/#11791 the witnesses lane builds the witness executor and runs the NOMINAL witnesses (one prepared subject, one fold) plus the generated-artifact check — a real baseline, but not the per-entry floor and not these claims; the per-entry local runs and the mutation table below are the discriminating evidence. Every run below is local, at head 10afa61ce03 (main merged through #11812) for the two new witnesses; the five landed witnesses at 5a2eaaa (no file they reach changed since), on an interpreter built from this tree at 124208f (no Rust changed since) into a private target dir (/cargo-target is host-shared and a neighbour's build replaced my first binary mid-run): CARGO_TARGET_DIR=/tmp/sharp-ant-467-target cargo build --release -p v1-compiler --bin gunbc, sha256 34ac855d6b869902…. A BuildBuddy dispatch of the same runs was attempted and every row was SIGKILLed (exit 137) on the 7.6 GB runner, as the brief predicted — remote runs are not evidence here. Driver: gunbc run --source-root dag --source-root src/v2 --entry <file> --claim-run --dry-run (hermetic; --dry-run selects the mock arm). It reports every claim and does not short-circuit (PASS count == test fn count on every green run). Exit statuses read unpiped.

entry	exit	PASS / test fn
dag/test/claim/review_sheet_header_init_witness_test.dag (new)	0	26 / 26
dag/test/claim/review_sheet_header_init_refusal_probe_witness_test.dag (new)	0	6 / 6
dag/test/claim/review_sheet_converge_witness_test.dag	0	92 / 92
dag/test/claim/review_sheet_batch_actuator_witness_test.dag (#11717)	0	28 / 28
dag/test/claim/review_sheet_header_schema_witness_test.dag	0	12 / 12
dag/test/claim/review_sheet_a1_title_witness_test.dag	0	5 / 5
dag/test/claim/sheets_a1_title_codec_witness_test.dag	0	10 / 10

What is executed vs supplied (§3). The mint runs end to end against the hermetic fixture: the_mint_observes_the_hermetic_empty_tab_binding_spreadsheet_and_tab (positive control for the construction wall, carrier obtained from its mint cross-module, fields read); an_empty_tab_and_a_valid_schema_authorise_the_header_row_at_a1_to_the_last_header (both mints → authorization, 'hermetic-mock-tab'!A1:D1, Listing|Title|Price|Decision); the_authorization_lowers_to_one_row_major_value_range_write; a_schema_wider_than_the_enrolled_letters_is_unaddressable_not_truncated (27 names / 26 letters, through the planner); the_mint_refuses_a_returned_tab_that_differs_from_the_requested_one (asks for Buyer Review, the fixture answers hermetic-mock-tab → FormulaReadTabMismatch { requested, returned }); bounded / column-bounded / unencodable requests refused with their SheetRequestCause — and the run log shows [hermetic:mock] sheets.Spreadsheets.GetValues exactly 7 times, one per successful-read claim, none for the three request-shape refusals: the refusal is before the read. The arms one fixture cannot answer are established against formula_grid_admit with the reading supplied: COLUMNS-major → RangeColumnsMajor; DIAGONAL → RangeDimensionUnrecognised { raw }; unreadable → cause carried; unqualified A1:B2 and malformed 'Review!A1:B2 → the codec's A1TitleUnterminatedQuote; tab checked before shape; qualified and whole-sheet spellings both admitted.

Finding (2) specimen: a_blank_rendering_formula_is_occupied_at_its_cell_under_formula_rendering — a read whose grid is [["=IF(TRUE,\"\",\"\")"]] is judged FormulaGridOccupied at row 1 column 0 with the formula text carried, so no carrier is minted; its control the_formatted_reading_of_that_cell_would_have_read_as_empty ([[""]] and [] are FormulaGridEmpty). Plus whitespace_is_content, a_blank_row_one_over_data_is_occupied_at_the_data_cell ([["",""],["","x"]] → r2c1), content_past_column_a_is_content, reading order, the planner's occupied arm over a supplied occupied reading, and the carry-through of a refused reading.

Refusal probes (dag/test/probe/review_sheet_formula_observation_forged_probe.dag, review_sheet_header_row_authorization_forged_probe.dag): asserted as exactly one blocking SoleConstructorViolation at the type BY NAME each. The harness control is two-part and the reason is measured: the census compiles the whole closure for Rust emission, and a source whose only import is extdeps.transports.rest { RestOutcome, RestOk } is already NOT total-clean on this tree, so a total-zero control over these modules is not authorable; part one asserts total-zero over the transport-free review_sheet_projection closure (harness live), part two asserts a no-forgery source over both modules is observed and carries ZERO SoleConstructorViolation rows at either subject.

Mutation table (written before the code; run in a separate worktree /tmp/sharp-ant-467-mut at the same head with the same binary; production mutated, witness run, source restored)

#	mutation (production only)	claim(s) that went RED	exit	PASS
M1	formula_whole_tab_render_option returns RenderFormattedValue	the_mint_reads_under_formula_rendering	1	24
M2	admit_whole_tab_request: A1EndClosed admitted as whole-tab	a_bounded_request_is_refused_with_the_bounded_cause	1	24
M3	admit_whole_tab_request: A1EndOpen admitted as whole-tab	a_column_bounded_request_is_refused_with_the_column_bounded_cause	1	24
M4	formula_grid_admit: returned-tab equality check removed	the_mint_refuses_a_returned_tab_that_differs_from_the_requested_one, the_admission_checks_the_tab_before_the_grid_shape	1	23
M5	value_range_row_major: COLUMNS-major read as rows	a_columns_major_grid_is_refused_naming_columns_major	1	24
M6	value_range_row_major: unrecognised majorDimension read as rows	an_unrecognised_major_dimension_is_refused_naming_the_spelling	1	24
M7	formula_grid_admit: ValuesUnreadable judged empty	an_unreadable_read_is_refused_carrying_its_cause	1	24
M8	formula_grid_admit: unnamed returned range judged empty for the requested tab	an_unqualified_returned_range_is_refused_rather_than_read_as_the_first_tab, a_malformed_returned_range_is_refused_with_the_codecs_cause	1	23
M9	first_occupied_cell: only row 1 examined (the parked planner's headers shape)	a_qualified_or_whole_sheet_returned_range_naming_the_requested_tab_is_admitted, a_blank_row_one_over_data_is_occupied_at_the_data_cell	1	23
M10	first_occupied_in_row: " " treated as blank	whitespace_is_content	1	24
M11	first_occupied_in_row: only column A examined	a_blank_row_one_over_data_is_occupied_at_the_data_cell, content_past_column_a_is_content, the_first_occupied_cell_is_the_first_in_reading_order	1	22
M12	first_occupied_in_row: a cell containing = treated as blank (FORMATTED-readback semantics)	a_blank_rendering_formula_is_occupied_at_its_cell_under_formula_rendering	1	24
M13	header_row_span: unaddressable width truncated to A1:Z1	a_schema_wider_than_the_enrolled_letters_is_unaddressable_not_truncated, the_header_row_span_runs_from_a1_to_the_last_header_on_row_one	1	23
M14	formula_grid_admit: the grid ignored (first_occupied_cell(rows: [])) — the re-pointed M14	a_qualified_or_whole_sheet_returned_range_naming_the_requested_tab_is_admitted, a_blank_rendering_formula_is_occupied_at_its_cell_under_formula_rendering, whitespace_is_content, a_blank_row_one_over_data_is_occupied_at_the_data_cell, content_past_column_a_is_content, the_first_occupied_cell_is_the_first_in_reading_order	1	19
M15	plan_header_init: carrier refusal dropped (replaced by a fixed arm)	a_refused_reading_is_carried_through_the_planner_with_its_cause	1	24
M16	sole_constructor removed from FormulaWholeTabObservation	a_formula_observation_cannot_be_authored_outside_the_mint	1	3
M17	sole_constructor removed from HeaderRowWriteAuthorization	a_header_row_authorization_cannot_be_authored_outside_the_planner	1	3
M18	header_row_value_range_write: majorDimension COLUMNS	the_authorization_lowers_to_one_row_major_value_range_write	1	24
M19	mint binds a different spreadsheet id than the one requested	the_mint_observes_the_hermetic_empty_tab_binding_spreadsheet_and_tab	1	24
M20	mint's FormulaGridOccupied arm mints the carrier anyway — declared survivor	none — survives (see below)	0	25

Registered 20, applied 20 (verified by name set: no row missing, none extra, no duplicates; results.txt carries one line per registered row). Rows M1–M19 except M20: exit 1 (unpiped), the named claim(s) FAIL and every other claim PASS (25 claims in the main witness, 4 in the probe witness). All rows run at 5a2eaaa in a separate copy of the tree, each restored before the next; the driver reports every claim, so no claim-removed re-runs were needed. The table was re-read after the restructure, not only re-run: M7/M8 initially named the deleted constructor FormulaGridAdmitted and refused to compile — the runner reported them UNEXPECTED (it requires the NAMED claim to fail, not merely a non-zero exit), and they were re-pointed to FormulaGridEmpty; M9–M12 moved with first_occupied_* from the planner to the observation module and now redden the same claims through formula_grid_admit; M14 is the re-pointed row above.

Declared blind spots: two, both inside the mint's own composition, which one empty fixture cannot exercise. (a) M1 reddens the pure formula_whole_tab_render_option; a mutation that bypasses it AT THE CALL SITE (passing RenderFormattedValue directly to read_values_rendered) is invisible because mock_response ignores its input. (b) M20: the mint's FormulaGridOccupied arm is unexecuted (the fixture is empty), so rewriting that arm to mint the carrier survives — 25/25 PASS, recorded as such. Both are the same class: an unexecuted arm of a 15-line function whose every decision is a pure fold that IS executed and mutated. Closing (b) needs a second hermetic response for one operation, which mock_response does not provide; that is the trigger, stated rather than hidden. The planner-level gap the first cut had (its M14) is closed by construction, not declared.

Not run live: no Sheets credential here; the first live execution is the private consumer's.

🤖 Generated with Claude Code

[briansrls]

REQUEST CHANGES — exact head 5a2eaaa0961fd5c2ff82238999e15dfb7ebeaeee

The revised design fixes the parked planner’s central shape: the planner no longer receives a grid it can ignore. formula_grid_admit classifies supplied FORMULA readings; only the current empty arm of observe_formula_whole_tab constructs FormulaWholeTabObservation; occupied and refused readings carry no carrier; and plan_header_init can authorize a header only from that carrier plus ValidatedHeaderSchema. The request-shape, returned-tab, row-major, whitespace/formula, width, and two sole-constructor boundaries are all correctly represented in source.

One blocking evidence/design gap remains: M20 is not the same kind of blind spot as the render-option call site, and it does not require a second transport mock to close.

M20 changes the mint’s local match so FormulaGridOccupied produces FormulaWholeTabEmpty { observation: ... }, and every claim stays green. That is the exact authority this PR exists to establish: an occupied FORMULA reading must not mint the carrier. The network read has already ended at this point; the remaining mapping

spreadsheet_id × FormulaGridAdmission → FormulaWholeTabReading

is pure and can be executed with a supplied FormulaGridOccupied. Extract that conversion as the one literal-construction site, call it from observe_formula_whole_tab, and admit it only to the live observer plus an exact non-egressing witness (or use an equivalent construction). Then the existing supplied occupied specimen can exercise the real carrier-minting boundary and M20 must red. No second mock_response is needed for that part.

The FORMULA-vs-FORMATTED call-site seam is different. The current mock ignores request inputs, so it genuinely cannot show which valueRenderOption reached the operation. That gap is honestly scoped and may remain declared, provided the claim is not named as though it observed the mint’s wire call. A temporary live tab containing a blank-rendering formula should be an H2 qualification before the buyer sheet is writable; it will ground this remaining effect seam.

Please also correct the source-level wording that says the occupied case or contrary render is “unwritable.” The PR body discloses M20 and the call-site bypass, but the authority module currently states the stronger guarantee without carrying those evidence limits. After the local admission→reading conversion is executed, only the wire-render limitation remains.

CI correction: on this exact head the current workflow did run a real floor job, including “Nominal witnesses (one prepared subject, one fold)” and the generated-artifact check, in addition to compiler and Clippy. So the baseline is stronger than the post-#11742 caveat states. It still does not change the deliberately surviving M20 mutation.

No redesign is requested for the formula-preserving read, the empty/occupied split, the header planner, the width refusal, or the future private write-permit boundary.

[briansrls]

APPROVE — exact head 10afa61ce038f1a61e1bb9d616fa14d606bebc5b

The M20 hold is closed. formula_reading_from_admission is now the sole carrier-literal site, is sealed to the real observer and one exact Bool-returning/non-egressing claim, and is executed against occupied, empty, and refused admissions. The outside-caller census claim plus the public-observer control independently measure that boundary. M20 and M21 are therefore discriminating evidence for the repaired subject.

Ruling on the unrerun rows: I do NOT require M8–M19 to be rerun before merge.

• M8–M18 legitimately carry forward. The exact-head delta from 5a2eaaa changes only review_sheet_formula_observation.dag plus the two new witness files; the production folds targeted by M8–M18 remain unchanged, as do the claims those mutations discriminate, aside from the separately accounted render-claim rename/additions.
• M19 is the one correction to the packet's “byte-identical subjects” wording: its carrier literal moved into formula_reading_from_admission, so its anchor was necessarily repointed. I am still not holding merge on a rerun. At this head the mapping visibly threads its spreadsheet_id into the empty carrier, the observer passes its own requested spreadsheet ID into that mapping, and the exact-head end-to-end claim reads and compares that field. A mutation binding another ID necessarily falsifies that claim. Treat M19 as source-inspected rather than exact-head mutation-measured.

The render-option call-site seam remains an honestly declared limitation and belongs in the H2 live qualification against a temporary tab holding a blank-rendering formula. It is not being represented as mechanically closed here.

Exact-head CI also ran a real nominal floor plus generated-artifact verification, compiler, and Clippy. The discriminating evidence remains the reported exact-head 26/26 and 6/6 local runs and M1–M7/M20/M21 mutation results.

No source or evidence hold remains. Do not spend additional loaded-host time rerunning M8–M19 for this merge.