setTerraUserTelefono's actorDeleted refusal is RACE-ONLY, not dead: vUserGroups filters deletedAt so notMember fires first sequentially, leaving actorDeleted reachable only through a TOCTOU window - so it is untestable by construction in a dry run, not merely unexercised
FOUND 2026-08-31 BY db02-terra-cc BUILDING THE TERRA-152 ARMS FOR setTerraUserTelefono, AND IT IS NOT THE SAME FINDING AS TERRA-161 EVEN THOUGH IT LOOKS LIKE IT. Census row 9, actorDeleted, in public.setTerraUserTelefono (terra_45, lines 93-101). The hypothesis is that it cannot fire in ordinary sequential execution. THE ARGUMENT. Per terra_53 evidence, public.vUserGroups filters users.deletedAt IS NULL as one of its own predicates. The notMember check reads vUserGroups and runs FIRST. So a soft-deleted user is already invisible to that read, notMember fires, and control never reaches actorDeleted. The only path that reaches it is a TIME-OF-CHECK/TIME-OF-USE gap: the actor passes the vUserGroups EXISTS read, is soft-deleted by a concurrent transaction, and is then found deleted by the later users row read taken FOR UPDATE. WHY THIS IS THE OPPOSITE CONCLUSION TO TERRA-161 AND MUST NOT BE FILED AS THE SAME THING. TERRA-161 asks whether lastAdmin is DEAD CODE - a guard that can never fire and therefore protects nothing while reading as protection. This one, if the hypothesis holds, is RACE-ONLY CODE: unreachable sequentially precisely because it exists to catch a window that only opens under concurrency. That is not a defect, it is a correctly written defensive check, and whoever wrote it anticipated a race rather than duplicating an earlier guard. Filing the two under one heading would invite deleting this one. WHAT THE CENSUS SHOULD SAY, AND THIS IS THE POINT OF THE ROW. Row 9 is not UNEXERCISED in the same sense as rows 3, 5 and 7, which are blocked on a population that could exist. It is UNTESTABLE BY CONSTRUCTION in a single-script dry run, because a single script has no concurrency. Recording it in the same bucket as the population-blocked rows overstates what a future arms file could ever reach, and someone will eventually read the unexercised count as a to-do list. TWO THINGS ARE UNVERIFIED AND NEITHER SHOULD BE REPORTED AS SETTLED. First, that vUserGroups actually filters users.deletedAt IS NULL - that comes from terra_53 evidence rather than from a read of the view definition taken for this question. Second, the ordering claim itself, that the vUserGroups read precedes the FOR UPDATE read in every path through the body. Both are source and evidence reasoning, and guard ordering is exactly the thing that changes without its comments changing with it. WHAT WOULD CLOSE IT: read the live definition of vUserGroups and confirm the deletedAt filter; confirm the two reads' ordering in the live prosrc of setTerraUserTelefono. If both hold, record row 9 as race-only and untestable by a single-script dry run, and stop counting it against harness coverage. If either fails, then actorDeleted IS sequentially reachable and needs a real arm, which changes the answer rather than the framing. DO NOT MANUFACTURE THE FIXTURE. Building a sequential refuse arm needs a users row that is both a live terra member and soft-deleted, and no such row exists - all 159 live shared users hold a live terra membership. Creating one means writing users.deletedAt directly, outside the boundary function, and users is enamel-owned shared state that terra never writes. That bound is the same one recorded for userGroups on TERRA-152 and it is permanent, not pending.
Activity
-
CONFIRMED RACE-ONLY, AND THE ANSWER WAS ALREADY WRITTEN IN THE FILE THE CENSUS CITED. Both legs of the hypothesis hold, and there are now THREE independent derivations that agree. LEG 1, live catalog, db02-terra-cc: pg_get_viewdef on vUserGroups returns a join carrying u."deletedAt" IS NULL among its own predicates, read fresh rather than carried from terra_53 evidence. LEG 2, live pg_get_functiondef on setTerraUserTelefono: the vUserGroups EXISTS check precedes the users FOR UPDATE read on every path, no branch reaches FOR UPDATE first. I cannot re-run either read - this lane holds no database connection - so both rest on db02's execution, and that limit is stated rather than glossed. LEG 3 IS THE ONE NOBODY WENT LOOKING FOR AND IT IS IN THIS REPOSITORY. db/migrations/applied/terra_45_setTerraUserTelefono.sql lines 166 to 173 record dry-run arm A2, run at authoring time against the hardened body: "Actor's users row is soft-deleted -> ACTUAL: 'notMember', not 'actorDeleted' - vUserGroups already excludes a soft-deleted user (u.deletedAt IS NULL in its own join), so v_held is false before the deletedAt branch is ever reached in the steady state. Not a bug: the refusal requirement is met via the membership check. The named branch (now FOR UPDATE) exists to close the TOCTOU race and is structurally untested by this arm - would need a concurrent soft-delete mid-transaction to exercise, which a single-session dry-run cannot construct." THAT IS THE ENTIRE FINDING OF THIS ROW, WRITTEN BEFORE THE ROW EXISTED, WITH AN OBSERVED RESULT RATHER THAN AN ARGUMENT. The conclusion, the mechanism, the reason it is not a bug, and the exact reason a dry run cannot reach it - all of it. And it was not an inference: A2 is a recorded execution. THE DEFECT THIS EXPOSES IS IN THE CENSUS, NOT IN THE FUNCTION. pm/2026-08-31-sql-authorization-predicate-census.md cites terra_45 lines 93-101 for row 9 and marks it UNEXERCISED. The answer sits at lines 166-173 of the same file. The census read the predicate and did not read the file's own evidence section. Row 8 has the same problem: arm A1 records notMember returning with zero writes, and A3 records the positive path returning 'updated', both PASS, both at authoring time - so setTerraUserTelefono's refuse AND satisfied branches had execution evidence in the repository the whole time the census reported it had none. AND IT IS THE SAME ERROR CLASS THAT WAS ALREADY CORRECTED ONCE ON TERRA-152, ARRIVING THROUGH A DIFFERENT DOOR. The first correction was that the exercised half read ONE evidence directory out of three - my under-specification, corrected the same day. The fix was "read all three directories." That generalised to directories and not to FILES: this time the corpus was read completely and the individual file was not. A migration's header is evidence, and in this project it is often the ONLY evidence, because the dry-run transcripts are untracked (TERRA-163). Anyone building a coverage claim must read the cited file end to end, not the cited line range. WHAT THIS CHANGES AND WHAT IT DOES NOT. Row 9 is confirmed RACE-ONLY: correctly written defensive code catching a TOCTOU window between the two reads, unreachable sequentially by construction. It is NOT dead code and must not be filed with or resolved alongside TERRA-161, where the open question is whether lastAdmin can fire at all. Row 9 stops counting against harness coverage - a single-script dry run has no concurrency and never will. ONE COVERAGE BOUND CARRIED FORWARD FROM THE SAME HEADER, line 180: vUserGroups also filters isSynthetic IS FALSE, so no arm exercises a synthetic actor and there is no reachable path to do so. Recorded here because it is the same shape - a permanent bound documented in a header that a line-range citation would miss. NOT CLOSED BY THIS ROW: whether lastAdmin is genuinely dead (TERRA-161), and the untracked-transcript gap (TERRA-163) which is what makes these headers load-bearing in the first place.