Add initValue0DefaultBranch test case to btree remove module - #1535
Conversation
The default arm in initValue0 (fjs/types/btree/remove/module.f.mjs) was the only one of four sibling invariant guards without a direct proof, leaving it as the sole uncovered branch in that module. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RWJ1asnmKEWY3pXHW5qyhq
Deploying with
|
| Status | Name | Latest Commit | Preview URL | Updated (UTC) |
|---|---|---|---|---|
| ✅ Deployment successful! View logs |
functionalscript | 076a03a | Commit Preview URL Branch Preview URL |
Aug 13 2026, 09:21 PM |
o2alexanderfedin
left a comment
There was a problem hiding this comment.
Approving. This closes the exact gap the #1509 review left open as a follow-up — initValue0's default arm was the one of the four that no test reached — and it closes it for real, not just plausibly.
Reviewed at 076a03a0 (the head moved from d8450b62 to the merge of main mid-review; the merge brings in only #1533, the fjs/types/btree/remove/ diff is byte-identical, and every number below was re-measured at 076a03a0). Baseline throughout is origin/main = 67fb2dac.
Two-sided mutation check
Broke initValue0's default arm so it returns instead of throwing:
default: { return /** @type {any} */([[v1]]) }- On this PR —
pass: 2548, fail: 1, total: 2549, and the single failure is
import("./fjs/types/btree/remove/module.f.mjs").proof.throw.initValue0DefaultBranch().
Nothing else moves. - The identical mutation on
origin/main—pass: 2548, fail: 0, total: 2548. It kills nothing.
That is the two-sided result that distinguishes real new coverage from a case that merely passes. It also settles that the throw genuinely originates in initValue0's default arm: if the case were throwing incidentally somewhere else, removing that throw would not have failed it.
The two weaknesses this PR family has shown
#1525/#1528 shape — a mutant that keeps the right observable but corrupts the branch. The analogue here is a mutant that still throws from the default arm but reaches it under the wrong condition. Broadened the guard:
if (/** @type {any} */(a) !== undefined) { // was: if (a === null)The new case still passes under this (its a is null, so the default arm is still hit and still throws), so if it were the only thing pinning initValue0 the mutant would survive the suite. It does not survive: pass: 2540, fail: 1, killed by the sibling fjs/types/btree/remove/proof.f.mjs proof.test(). So the branch is pinned by the suite as a whole, unlike #1525/#1528.
#1518 shape — the assertion pinning too little. Changing the thrown value to 'MUTANT-different-message' survives: pass: 2541, fail: 0. The proof.throw bucket asserts only that it throws, never what. Worth naming as the honest limit of the case, but I do not think it is a defect here — it is exactly what the three sibling cases (reduceValue0DefaultBranch, reduceValue2DefaultBranch, initValue1DefaultBranch) do, and it is the inverse of the #1518 problem rather than a repeat of it: there a pinned message let a branch change slip through; here the branch change is caught (above) and only the message is unpinned.
Coverage delta
npm run cov (works in this environment since #1512 — it reports real, non-vacuous numbers on both trees):
origin/main |
this PR | |
|---|---|---|
fjs/types/btree/remove/module.f.mjs — branch |
98.55 | 100.00 |
| all files — branch | 98.25 | 98.27 |
Line and function coverage of the module were already 100.00 on both sides; the branch column is the whole delta, and it is the arm this PR adds.
Rest of the battery
npm test:pass: 2549, fail: 0vs2548onorigin/main— exactly +1, the new case, no collateral.npm run prepackfrom a freshly cleaned tree: exit 0.- CHANGELOG: none needed. §8.3 — this is a proof-only addition inside the existing
proofobject, matching the #1509/#1515/#1525/#1528 precedent for exactly this shape of change.
Summary
Added a missing test case for the
initValue0function with default branch handling in the btree remove module's proof suite.Key Changes
initValue0DefaultBranchtest case that validatesinitValue0behavior when called withnullas the first argument and a tree structure containing nested branches as the second argumentImplementation Details
The new test case follows the existing pattern of other default branch tests in the proof object, specifically mirroring the structure of
initValue1DefaultBranchbut testing theinitValue0function variant with appropriate test data.https://claude.ai/code/session_01RWJ1asnmKEWY3pXHW5qyhq