ch:compositional-linearizability: ch:compositional-linearizability

Problem, calculus, and result. Implement the finite trace checker for the frozen $\mathsf{Spec}$, $\mathsf{Impl}$, identity-saturation, and tensor fixtures of chapter 87. It must accept the atomic counter, report the canonical four-event atomic-exchanger counterexample, accept the paired-set exchanger, and accept the horizontal two-counter fixture at the named bounds.

Representation and invariant. Parse each supplied name into a closed fixture tag. Represent calls and returns by constructors carrying a thread and a value. The breadth-first frontier is ordered by depth, then thread, tag, and value. Its invariant is that every shorter trace precedes every longer trace and equal-depth traces use the declared tie order. A general graph parser would accept more inputs, but it would enlarge the trusted parsing layer and conceal the four frozen fixtures. Closed fixture tags keep the executable claim finite and inspectable.

First complete version. Implement fixture parsing, event equality, trace equality, and a verdict type carrying either a checked depth or the first separating trace. Run the atomic counter through depth $6$ and require a bounded PASS.

Remaining cases in theorem order. Add the atomic exchanger and require the exact call-$0$, call-$1$, return-$0$, return-$1$ counterexample. Add the paired-set transition and check it through depth $4$. Add tagged horizontal composition and project each trace to its two counter components before checking depth $6$.

A failing version. Reverse the equal-depth thread tie order. The checker then reports the thread-$1$-first exchanger trace. That trace is also separating, but it is not the canonical witness required by the chapter’s decidable acceptance test, so the mutation test rejects it.

Acceptance test. Require the three bounded PASS lines, the exact four-event FAIL line, the tie-order mutation verdict, the final five-case summary, and audit output []. The word bounded must occur on every PASS line.

Mathematical boundary. The run illustrates the finite counterexample and projection calculations used in theorem 87.7, theorem 87.8. It proves neither trace inclusion beyond the named depths nor locality or composition for arbitrary specifications.