ch:simple-object-inference: ch:simple-object-inference

Problem, result, and invariant. Implement the corrected overwrite solver step at one selected label. Given an input row equation, it must generate its presence branches or its shared-row obligations. Every returned branch denotes only solutions of the equation, and each of the four concrete old-presence shapes selects a returned branch. The observable result is the six-case report in appendix E.

Representation. Use distinct datatypes for field types, absent/present descriptors, the four shape cases, equations, solver outputs, and presence obligations. A pair of Booleans could encode shapes compactly, but named constructors make branch omission visible in diagnostics. Hard-coding a list of four shapes beside a separate counterexample would not test a solver; therefore solve consumes RowEquation and constructs the branch or obligation output inspected by every later case.

First complete version. Implement right-biased update equality: old descriptors are ignored and the two new field types must agree. Show that empty and old-Boolean inputs become equal after integer update, while the invalid injective decomposition rejects them. Then make solve (SymbolicOverwrite FInt FInt) return the four named branches.

Soundness, coverage, and the source boundary. For each generated branch, construct concrete old descriptors with that shape and check the updated rows equal. Separately construct one witness of each of the four shapes and require its shape to occur in the output list. Check both list length four and coverage: deletion and duplication cannot compensate for one another. Separately represent rows over $\{a,b\}$. Updating at $a$ must make the empty and $a$-only rows equal to updated null, while a retained $b$-field must make the rows unequal. This bounded source regression does not claim to enumerate the full row universe.

The shared-row transition and concatenation case. Give solve a distinct shared-row input and require a PresenceObligations output containing the integer obligation. This is an actual transition, not a count of prewritten obligations. Keep the separate 1991 concatenation observation small: an absent right field selects the left origin and a present right field selects the right origin.

A failing version. Delete LeftPresent from the symbolic branch list. The program still typechecks, but the length check and the concrete left-present witness both fail. Replacing the shared-row output by the same equation would also destroy the obligation case and model the corrigendum’s termination bug.

Acceptance test. Run the four commands in appendix E. Require the exact six PASS lines, the final count, and audit output []. Verify independently that removing any one branch fails kappa test; restore the accepted digest before the final run.

Mathematical boundary. The executable is a finite regression for a one-label solver step and a two-label source boundary. It illustrates branch generation, concrete soundness/coverage witnesses, foreign-field rejection for $W$, and the shared-row transition. It proves neither global solver termination nor the corrigendum’s finite-complete-set theorem, and it never asserts that two row shapes cover the countable label universe.