A protocol is normally written against a subroutine later supplied by another protocol. Replacing one by the other is a set operation on systems.
Nothing so far stops the incoming \(\pi \) from landing on a process id the surrounding protocol already uses, which would leave a call ambiguously addressed. We rule this out rather than repair it.
Definition 4.2 (Well-formed replacement). The replacement of \(\varphi \) by \(\pi \) in \(\rho \) is well-formed if no process id occurs both in \(\rho \setminus \varphi \) and in \(\pi \), that is, if
Proposition 4.3 (Replacement). Let \(\rho \) and \(\pi \) be systems, let \(\varphi \subseteq \rho \), and let the replacement of \(\varphi \) by \(\pi \) in \(\rho \) be well-formed. Then \(\rho [\pi /\varphi ]\) is a system. If moreover \(\IDs (\pi ) = \IDs (\varphi )\), then \(\IDs (\rho [\pi /\varphi ]) = \IDs (\rho )\).
Proof. The process ids of \(\rho [\pi /\varphi ]\) are those of \(\rho \setminus \varphi \) together with those of \(\pi \). Each system carries distinct ids internally and well-formedness makes the two collections disjoint, so no id repeats; the members are standard and finitely many, both inherited from \(\rho \) and \(\pi \), so \(\rho [\pi /\varphi ]\) is a system. That first claim rests on the well-formedness of the replacement alone, \(\IDs (\pi ) = \IDs (\varphi )\) entering nowhere in it. Identities need no separate hypothesis: an identity carries its process id in the first component, so members with distinct ids have disjoint identity sets. For the identities themselves,
using \(\IDs (\pi ) = \IDs (\varphi )\) in the middle step and \(\varphi \subseteq \rho \) in the last. □
The two halves of the proposition are used differently below. That \(\rho [\pi /\varphi ]\) is a system lets Chapter 4 speak of it at all, and rests on well-formedness alone. That its identities are those of \(\rho \) needs \(\IDs (\pi ) = \IDs (\varphi )\), and no result in Chapter 4 assumes it: admissibility there is stated for a pair of systems through the union of their identity sets, and Proposition 4.16 and Theorem 4.20 say outright that no relation between the two is used. Where the equality is wanted, blocking supplies it.
Definition 4.2 settles process ids, and Proposition 4.3 identities. Neither addresses dependence, and dependence is where replacement can go wrong: the names \(\rho \setminus \varphi \) relies on are still occupied after \(\varphi \) gives way to \(\pi \), but every requirement is re-evaluated at the new occupant. Two conditions close the gap.
Informally, Theorem 4.4 below says that a well-formed replacement preserves \(\WF \) when the entries of the incoming \(\pi \) can be discharged in the new world, and some member of \(\pi \) stands in for \(\varphi \) wherever an entry of \(\rho \setminus \varphi \) was witnessed inside \(\varphi \). Hypothesis (ii) is what it means for \(\pi \) to be a drop-in for \(\varphi \), and emulation does not supply it.
Theorem 4.4 (Replacement preserves well-formedness). Let \(\rho \) and \(\pi \) be systems, let \(\varphi \subseteq \rho \), let the replacement of \(\varphi \) by \(\pi \) in \(\rho \) be well-formed in the sense of Definition 4.2, and let \(\WF (\rho )\). Suppose
Then \(\WF \bigl (\rho [\pi /\varphi ]\bigr )\).
Proof. Write \(\rho ' := \rho [\pi /\varphi ] = (\rho \setminus \varphi ) \cup \pi \), a system by the first claim of Proposition 4.3 — the second is not available here, \(\IDs (\pi ) = \IDs (\varphi )\) being no hypothesis of this theorem. Take \(\F \in \rho '^{+}\) and an entry \((\F ',R) \in \F .\uses \); we must place a witness in \(\rho '^{+}\). There are three cases, by where \(\F \) comes from.
If \(\F \in \pi \), hypothesis (i) is exactly the claim.
If \(\F \) is one of \(\Zenv \), \(\Adv \), \(\Corr \), its entries are settled once and for all, independently of the system: \(\Corr .\uses \) is empty, and the entries of \(\Zenv \) and \(\Adv \) name each other, with \(\Adv , \Zenv \in \rho '^{+}\) and \(\serves \) holding between them as Chapter 1 records. All three are global, so the session conjunct is waived.
If \(\F \in \rho \setminus \varphi \), then \(\F \in \rho ^{+}\), so \(\WF (\rho )\) supplies a witness \(\G \in \rho ^{+}\) for this entry. Either \(\G \notin \varphi \), in which case \(\G \) lies in \((\rho \setminus \varphi ) \cup \{\Zenv ,\Adv ,\Corr \} \subseteq \rho '^{+}\) and serves again: it is the same machine with the same fields, so \(\G .F\), \(\G .s\) and whatever \(R\) reads are unchanged, and \(\F \) is unchanged too. Or \(\G \in \varphi \), and hypothesis (ii) supplies a member of \(\pi \) meeting the same three conditions in its place. Either way the entry has a witness in \(\rho '^{+}\). □
Hypothesis (ii) is what it means for \(\pi \) to be a drop-in for \(\varphi \), and emulation does not supply it. Definition 4.11 compares behaviour at the boundary; it says nothing about the declared fields of the machines behind that boundary, and a \(\pi \) that emulates \(\varphi \) perfectly may still fail to admit a caller \(\varphi \) admitted, or serve a party \(\varphi \) served. The check is cheap — it ranges over the entries of \(\rho \setminus \varphi \) that pointed into \(\varphi \), and nothing else — but it is a check, and belongs beside well-formedness of the replacement rather than inside the composition theorem.