jcp: C26 — the one-writer requirement gets a conformance clause with teeth #352

Merged

dcharlot merged 1 commit from feat/c25-single-writer-conformance into main 2026-10-20 08:28:34 -04:00

Conversation 0 Commits 1 Files changed 2 +48

2026-10-20

Transaction Science

jcp: C26 — the one-writer requirement gets a conformance clause with teeth ...

#346 added §5's one-writer requirement and deliberately added no conformance
clause, on the grounds that numbering one the pack cannot test would claim
coverage that does not exist. This is that follow-up: the clause, and a check
that fails when the implementation stops providing it.

`C26 one writer per record: a second holder is refused` asserts three things on
the reference `FileJournal`:

- a second holder of a record another endpoint holds is **refused**, because two
  would each replay it, each re-establish the same remaining budget and each
  debit against it — spending it twice while every entry still verifies;
- the refusal is specifically a **contention**, not some other I/O failure a
  caller might paper over;
- the claim is **released when the holder goes away**, or a restart could never
  reopen the record it previously held, which would turn the requirement into a
  trap.

§9 gains the clause and the harness header gains its class, so the spec's list
and the pack agree.

**Proving the clause has teeth took two attempts, and the first was wrong.** I
first mutated the *check* — accepting a second holder, accepting any error kind
— and the suite stayed green. That is not a surviving defect: weakening a check
makes it vacuous, and a vacuous check passes. The meaningful direction for a
conformance clause is to break the **implementation** and require the clause to
catch it:

| implementation mutation | result |
|---|---|
| the lock does not exclude a second holder | C26 FAILED: "a second writer opened a record another endpoint holds" |
| no lock taken at all | C26 FAILED, same message |
| contention reported as a different error kind | C26 FAILED: "a contended record failed for the wrong reason" |

All three caught, with C26 named — which also settles that the clause is
actually executed by `all_checks_pass` rather than merely listed.

Noted while counting clause ids, not touched here: §9 declares a `C25 — flow`
the harness does not implement, and the harness has a `C19` (injection
resistance) §9 does not list. Both asymmetries predate this change.

Co-Authored-By: Claude Opus 5 <[email protected]>

3a57c1f21e

• View at this point in history

2026-10-20 04:03:44 -04:00