The paragraph above named two claims: delivery by \(\Delta \), and the one \(\Fnet \) cannot make — every message fetched was sent, by the party it names. A third, no delivery before sending, again needs no game: an index not yet in \(\V {list}\), or already drained, fails \(\Clean _{\op {addr}}\), so \(\San \) repairs \(S\) to \(\emptyset \) and nothing not yet real is released early either (Section 18.2 made the same point for \(\Fnet \)’s buffer). The finalizations \(\op {FinLive}\) and \(\op {FinAuth}\) below formalize the other two, transplanting Section 18.2’s pair rather than starting over — the shell of relay, log, finalize does not change between a diffusion channel and an addressed one, and neither do the names, these being the same two properties asked of a different channel. Both take the search reading. What changes is which of the two \(\Fac \) can keep: both, this time, and the second is the point of the whole design. That the transplant is name for name is the sharpest way to put the difference between the two channels — one game, asked of \(\Fnet \) and of \(\Fac \), answered differently.
Both are played over the game system \(\gamma := \{\Gm \} \cup \{\Fac ,\Gclock \}\), with \(\Fac .\admits := \{\Gm .\PID \}\) pinned and \(\Fac .\Ps \subseteq \Gm .\Ps \) — the same tightness argument as Section 18.2, and for the same reason, \(\Fac \)’s fields already following \(\Fnet \)’s pattern (Section 19.1). No caller but \(\Gm \) passes \(\opl {Guard}\) at \(\Fac \), so every entry \(\op {Send}\) ever places in \(\V {list}\), and every record \(\op {Fetch}\) ever returns, passes through the relays below and is recorded. The interface box states \(\Gm .\uses \) in full. Inside an interface at \(\id \) we write \(\id _{\Fac }\) for \((\Fac .\PID ,\id .P)\) and \(\id _{\Gclock }\) for \((\Gclock .\PID ,\id .P)\), the second the notation of Section 17.2.
Game shell over \(\Fac \) and \(\Gclock \); the finalizations follow
\(\PID := (\Gm .F,0,0)\), \(\Ps := \Fac .\Ps \cup \{Z\}\), \(\admits := \Zpid \), \(\uses := \{(\Fac ,\serves _{\Gm }),\,(\Gclock ,\serves )\}\), \(\pars := \none \)
\(\op {Initialize}()\):
\(\id .\op {Send}(Q,\msg )\) from \(\id '\)
auto
\(\id .\op {Fetch}()\) from \(\id '\)
\(\id .\op {Leak}()\) from \(\id '\)
The finalizations of \(\Gm \); the shell over \(\Fac \) and \(\Gclock \) is shared
\(\id .\op {FinLive}()\) from \(\id '\) (liveness)
\(\id .\op {FinAuth}()\) from \(\id '\) (authentication)
Three things about the code, two of them familiar. Both relays read the clock themselves for the same reason as Section 18.2’s: the two readings coincide because no core of \(\gamma \) runs between them, \(\op {Read}\) placing no call of its own. \(\op {Send}\)’s relay keeps \(\Fac .\op {Send}\)’s own return, \(\ok \), having nothing else to report — unlike \(\Fnet \)’s, which had a message id to pass back and \(\Fac \) never hands out. And authentication’s verdict needs no search over senders or times, unlike its namesake’s: a fetched record already names \(P\) and \(\tau _s\), so the win condition is a direct check that the exact tuple was never sent, not an existential one over what might have produced it — the address \(\Fac \) carries is doing, in the verdict, exactly what it does at the interface.
Proposition 19.1 (\(\Fac \) has liveness). For every \(\Zenv \in \ZenvSet _{\gamma ,\gamma }\) and every occupant \(\mathcal {X}\) of the adversary slot, \(\Pr [\Win _{\op {FinLive}}] = 0\). So \(\{\Fac ,\Gclock \}\) has liveness within \(0\) against \(\bigl (\ZenvSet _{\gamma ,\gamma },\Xset \bigr )\) in the sense of Definition 5.8, for \(\Xset \) the class of all occupants.
Proof. Suppose \((\atom {send},P,Q,\tau _s,\msg ) \in \V {tr}\), written at some activation of the \(\op {Send}\) relay (line 5). Its own clock read and \(\Fac .\op {Send}\)’s internal one (line 4) agree, by the argument of Section 18.2: no core of \(\gamma \) runs between them, \(\Fac \)’s guard and corruption check finding \(\id .P\) honest since the relay ran at all, and \(\op {Read}\) itself placing no call. So the core wrote some fresh \(m\) with \(\V {list}[m] = (P,Q,\tau _s,\msg )\) at that moment.
Suppose too \((\atom {fetch},Q,\tau ,M) \in \V {tr}\) with \(\tau \geq \tau _s + \Delta \). If \(\V {list}[m]\) still holds \((P,Q,\tau _s,\msg )\) when that fetch’s core runs, then \(m \in R\) by line 12 — the entry names \(Q\), and \(\tau _s + \Delta \leq \tau \) by hypothesis, for \(\tau \) its own reading of the clock and, by the same argument again, the relay’s — so \((P,Q,\tau _s,\msg ) \in M\) whatever the slot answers at line 13 and whatever \(\San \) does with it, neither touching \(R\). If instead \(\V {list}[m]\) had already been cleared, that happened only at line 16 of some earlier fetch by \(Q\) — the one line that ever clears an entry — and only on indices already placed in that fetch’s own \(R \cup S\), hence already present in that earlier fetch’s own \(M\). Either way \((P,Q,\tau _s,\msg )\) appears in some fetch of \(Q\)’s, and the verdict at line 18 gives \(0\). □
Proposition 19.2 (\(\Fac \) has authentication). For every \(\Zenv \in \ZenvSet _{\gamma ,\gamma }\) and every occupant \(\mathcal {X}\) of the adversary slot, \(\Pr [\Win _{\op {FinAuth}}] = 0\). So \(\{\Fac ,\Gclock \}\) has authentication within \(0\) against \(\bigl (\ZenvSet _{\gamma ,\gamma },\Xset \bigr )\) in the sense of Definition 5.8, for \(\Xset \) the class of all occupants — the property Section 18.2 proved \(\Fnet \) lacks, held here instead.
Proof. Suppose \((\atom {fetch},Q,\tau ,M) \in \V {tr}\) with \(Q \notin \Cs \) and \((P,Q,\tau _s,\msg ) \in M\). By \(\Fac .\op {Fetch}\)’s code, \(M = \{\V {list}[m] : m \in R \cup S\}\), and both index sets draw only on \(\V {list}\) as it already stands: \(R\) by its own pattern match (line 12), and \(S\) after sanitizing, since \(\Clean _{\op {addr}}\) admits only indices \(i\) with \(\V {list}[i] = (\cdot ,Q,\cdot ,\cdot )\) already and line 3 (Chapter 12) picks among values meeting that predicate — neither manufactures an index \(\V {list}\) does not hold. So \((P,Q,\tau _s,\msg ) \in M\) only if \(\V {list}[m] = (P,Q,\tau _s,\msg )\) for some \(m\) at some point.
The only line that ever writes \(\V {list}[m]\) to a value other than \(\none \) is \(\op {Send}\)’s own core, and by tightness — \(\Fac .\admits = \{\Gm .\PID \}\) pinned — that core runs only on calls \(\Gm \)’s relay places: not the environment, not the adversary, not a machine hosted at an invented instance of the game’s name. So the write producing \((P,Q,\tau _s,\msg )\) happened at some activation of the \(\op {Send}\) relay, and by the coinciding-read argument of the previous proof it was logged there as exactly \((\atom {send},P,Q,\tau _s,\msg )\). Hence \((\atom {send},P,Q,\tau _s,\msg ) \in \V {tr}\), and the verdict at line 28 gives \(0\). □
As with \(\Gclock \) and \(\Fnet \), both properties transfer by Corollary 5.11 only if the game system’s cores place no responsive call — and here, as there, neither does: Section 19.1’s “Both slot calls are responsive” covers \(\op {Send}\)’s notification and \(\op {Fetch}\)’s query alike. A system \(\pi \) put in place of \(\{\Fac ,\Gclock \}\) must then have both transfers argued directly, for the reason Remark 9.4 gives, exactly as \(\Fnet \)’s own notification cost Section 18.2 the same thing.
Unlike the network, nothing here is left standing only as a negative result. Proposition 19.2 is the win condition Section 18.2 transplanted from \(\Fnet \) and could not close, closed here instead — and the two proofs, laid side by side, locate the whole difference in one fact: whether tightness can trace a fetched record back to a \(\op {Send}\) that produced it. For \(\Fac \) it always can, \(\V {list}\) having no other way to gain an entry; for \(\Fnet \) it cannot, line 16 being exactly the other way in. Two chapters, one game transplanted twice, and the address is the entire difference between them.
That the transplant keeps the names is what makes the comparison sayable at all. The finalization \(\op {FinAuth}\) is not two properties that resemble each other but one win condition — fetched, addressed, never sent — asked of two channels, and the answer is \(1\) for \(\Fnet \) and \(0\) for \(\Fac \). Under the shape Chapter 5 replaced, where each property carried its own game, the two would have been \(\Gm _{\op {Auth}}\) and \(\Gm _{\op {Auth}}'\) and the sameness would have been a remark; here it is the notation.