Recursive-effect and concurrent-object boundaries

The event family is indexed by response type. Trees have return, visible, and silent observations; recursive calls must occur below a visible continuation or silent observation. Weak equivalence is the nested inductive–coinductive relation of definition 86.4, and is termination sensitive.

Weak equivalence is locally proved to be an equivalence and a bind congruence. Interpreter identity and composition are proved up to that relation. Tagged signature sums and the finite successor-server observation theorem use the same frozen signature.

Guardedness is not claimed complete for all productive host functions. Silent divergence is not identified with return. No fairness, scheduler, compiler-correctness, or arbitrary-host-function productivity theorem is exported. The Kappa corpus checks one finite server prefix and mutation, not the source’s Rocq development.

Thread names are the finite subtype . A specification contains state, initial state, labelled steps, and sequential-consistency evidence. The artifact-local $\mathsf{Prog}$ is coinductive and includes silent divergence; its mutually corecursive substitution inserts the artifact’s administrative silent steps. $\mathsf{Prog}$ and $\mathsf{Impl}$ are constructor-preservingly related to interaction trees but do not import that library. Horizontal tensor uses one shared thread-name set, tagged event signatures, and a shared tagged active map; this prevents a thread from crossing between component protocols while permitting it to use either component at different times. Linking, identity modules, tensor, trace refinement, $\mathsf{K}(V)=V▹\mathsf{idM}$, and compositional linearizability have the types displayed in chapter 87.

Module unit/associativity, compatibility of linking with module composition, and tensor distribution are locally proved at the artifact-local program equivalence. There is no LTS unit equation $V▹\mathsf{idM}=V$: this term is $\mathsf{K}(V)$ and may expose more overlay traces than $V$. Observational refinement, both locality directions, and horizontal/vertical composition are reconstructed at the LTS signature. The restricted set-specialization theorem is book-owned and assumes finite nonempty classes, at most one operation per thread per class, real-time and per-thread order, and one shared pending-call completion convention.

The atomic and interval specializations retain their distinct source hypotheses. The exchanger is an atomic counterexample and a paired-set example; it does not prove that every possibility set is nonsingleton. The one-shot write-snapshot comparison is not a corollary of the restricted set theorem. The Kappa checker reports only bounded fixture results.

A possibility contains target state, call status, and return status. A possibility set is a predicate and may be empty as data; commit and return obligations separately require an inhabited successor. Assertions range over interaction states and possibility predicates. The program-safety judgment is coinductive: it is the greatest relation closed by its return, visible, and silent rules, so a guarded silent loop is admitted when its invariant satisfies the silent obligation. Commit, silent, and return obligations quantify the exact thread-local step, unchanged-thread maps, possibility coverage, status consumption, reset state, and guarantee. The frozen $\mathsf{VerifyImpl}$ record contains rely, guarantee, precondition, postcondition, and continuation families, including $\mathsf{all}\mathsf{\_}\mathsf{return}$.

The ambiguous-queue pruning theorem is book-owned. The generic lock theorem uses atomic adjacency and mutual exclusion. Soundness is proved by the idle, continuation, and underlay-call thread-state invariant. Semantic completeness constructs all five assertion families from saturated possibility sets and is an existence theorem, not an inference algorithm.

The exchanger proof uses a singleton possibility; the queue fixture forces two. No liveness, weak-memory, crash, practical automation, or theorem transfer to another concurrent separation logic is claimed. Native Rocq replay and the finite Kappa explorer check different evidence.