Section 15.2 instanced Definition 5.1 once; the clock is worth a second, not least because time is the one thing in this paper whose order is the content. We give one game \(\Gm \) over \(\Gclock \) carrying two properties: \(\opl {FinStead}\), steadiness, saying that the counter moves as the code promises — forward, by one, and only when pushed — and \(\opl {FinUna}\), unanimity, saying that it moves only when every honest registered party has pushed. Both take the search reading of Definition 5.8, winning either being meant to be impossible rather than hard.
They are played over the game system \(\gamma := \{\Gm \} \cup \{\Gclock \}\), with the clock taken as in Chapter 17 save one field: \(\admits := \{\Gm .\PID \}\), pinned. The change is forced. Tightness at \(\{\Gm \}\), which Definition 5.1 requires, asks the members under test to admit whole process ids, and a bare \(\Stdpid \) is exactly what Remark 6.5 refuses; Definition 5.7 says why in operational terms — an environment shares a global functionality, touching it as anyone may, and a property of a global \(\F \) is a property against an adversary that shares it. For these two properties sharing is not a nuisance but the negation of the claim: steadiness and unanimity are assertions about all the ticks there are, and a game can certify them only where its trace is all there is. So the clock is played privately, and the properties certified are of its code, which sharing does not change — the situation of Section 15.2 exactly, where the \(\Fsig \) that ships names its protocol and the \(\Fsig \) under test names the game.
Pinned, the clock is no longer global, so line 3 of \(\opl {Guard}\) asks for one session; the experiment sits in session \(0\) and the clock’s process id carries \(s = 0\), so the check passes. And no caller but \(\Gm \) now passes line 2 at the clock: not the environment or a machine it hosts, whose claims lie outside a pinned \(\admits \), and not the adversary, whose \(A\)-identities are refused before line 13 could even answer them the time. So the counter changes only inside line 15 below and the membership only inside the \(\op {Register}\) and \(\op {Deregister}\) relays beside it, and every change is recorded — a game whose verdict is “the time moved when no one pushed” has no other way to know. Inside an interface at \(\id \) we write \(\id _{\Gclock }\) for \((\Gclock .\PID ,\id .P)\), and every trace entry carries the answer \(\tau \) the clock gave.
One line has no analogue in Section 15.2: the relays refuse the root. There the relays at the root addressed a party \(\Fsig \) does not serve and were answered \(\rej \) at line 1, which the verdicts, existential over well-shaped tuples, never read. Steadiness reads every entry, so a \(\rej \) of the game’s own making cannot be allowed into the trace; refused at the relay, nothing is appended, and every entry in \(\V {tr}\) is an answer the clock actually gave. Against a replacement this bites, and rightly: a \(\pi \) answering an honest read anything but a number loses steadiness on the spot, a clock that cannot say the time being broken however it moves.
That line is the first thing a shared shell asks for that a single property would not. Unanimity does not need it — its verdict is existential, like \(\Fsig \)’s, and would read past a \(\rej \) as those did — so the refusal is steadiness’s demand alone, and the shell carries it because both finalizations hang off the shell. A shell is built to the strictest of the verdicts it serves, and the cost of that is paid by the others: unanimity is played on a trace cleaner than it needs. It is a cost worth naming, because it is the one thing sharing a shell can take away. Where a property would be weakened by another’s demand rather than merely over-served, the answer is a second game and not a second finalization.
Game shell over \(\Gclock \); the finalizations follow
\(\PID := (\Gm .F,0,0)\), \(\Ps := \Gclock .\Ps \cup \{Z\}\), \(\admits := \Zpid \), \(\uses := \{(\Gclock ,\serves _{\Gm })\}\), \(\pars := \none \)
\(\op {Initialize}()\):
\(\id .\op {Register}()\) from \(\id '\)
\(\id .\opdef {Deregister}()\) from \(\id '\)
\(\id .\opdef {Tick}()\) from \(\id '\)
auto
\(\id .\opdef {Read}()\) from \(\id '\)
\(\id .\op {Leak}()\) from \(\id '\)
The finalizations of \(\Gm \); the shell over \(\Gclock \) is shared
\(\id .\opdef {FinStead}()\) from \(\id '\) (steadiness)
\(\id .\opdef {FinUna}()\) from \(\id '\) (unanimity)
The verdicts, in words. The finalization \(\op {FinStead}\) returns \(1\) on an answer below its predecessor, an answer more than one above it, or an increase anywhere but at a tick: reads, registrations and departures must find the time where the last answer left it. A tick answered \(\tau _{j-1}+1\) is allowed — it is the tick that closed the round — and \(\tau _0 := 0\) is \(\op {Initialize}\)’s word taken as the first observation, so a first read answered \(1\) is already a counter that moved before anyone pushed. The finalization \(\op {FinUna}\) returns \(1\) if the counter passed some \(t\) although some party — honest at the close, registered by round \(t\) and never released — has no tick answered \(t\) or \(t+1\): no tick placed during round \(t\), that is, the answer \(t+1\) covering the one that closed it. The registration conjuncts read the trace, not the clock’s tables, so they too name only what the game itself did.
Two contrasts with Section 15.2, both instructive. There the trace was a sequence whose order no verdict read; here \(\op {FinStead}\) reads little else, time being an order and not much besides. And there both verdicts had to ask \(P \notin \Cs \) of every party they named; \(\op {FinStead}\) asks nothing of anyone, because at a corrupt party the game’s own wrapper intercepts before the core runs and records (Remark 5.4), so every entry in \(\V {tr}\) is an honest core’s answer already. The one verdict that must name honesty is \(\op {FinUna}\)’s, whose claim concerns parties that did not call, and it names it at the close — monotonicity (Section 3.5) again making that the stronger reading. That the two differ so — one reading the register, the other not; one reading order, the other membership — is what a shared shell is for: it is the oracles they have in common, not the verdicts, that made them one game.
Remark 17.1 (Agreement is steadiness read across parties). The property a shared clock is usually wanted for is agreement: honest parties hold a common view of the time. Here it is not a third game but a corollary of the verdict above, and by design. Line 28 quantifies over the trace interleaved, not party by party: between two consecutive \(\atom {tick}\) entries every answer must equal its predecessor, whoever asked, so two honest parties reading between the same two ticks are answered the same value or the game is won. Stated per party — each party’s own subsequence steady — the verdict would be strictly weaker, and agreement a separate property: a replacement could then answer \(P\) with \(5\) and \(Q\) with \(3\) in adjacent activations and fail neither property. What lets one verdict carry both claims is the execution model: a single token totally orders the trace, so “simultaneous reads” do not exist and a common view reduces to the consistency of adjacent entries. Two limits are worth naming. Agreement is among honest parties only, a corrupt party’s answers being the adversary’s (Remark 5.4); and it says nothing of a party that does not ask, whose view may grow stale while the clock runs ahead — staleness of the party, not disagreement of the clock, and nothing a functionality could promise a caller that never calls. A drift variant — views agreeing within some \(\Delta \), the loosely synchronized clocks of [11] — would be a genuine weakening of line 28, and under the present shape it is a third finalization rather than a third game: it reads the same trace of the same relays and differs in the verdict alone, which is exactly the test for hanging it off this shell.
Proposition 17.2 (\(\Gclock \) has both properties). For \(\op {Fin}\) either of \(\op {FinStead}\) and \(\op {FinUna}\), for every \(\Zenv \in \ZenvSet _{\gamma ,\gamma }\) and every occupant \(\mathcal {X}\) of the adversary slot, \(\Pr [\Win _{\op {Fin}}] = 0\). So \(\{\Gclock \}\) has each property within \(0\) against \(\bigl (\ZenvSet _{\gamma ,\gamma },\Xset \bigr )\) in the sense of Definition 5.8, for \(\Xset \) the class of all occupants.
Proof. One invariant carries both properties: the counter changes only inside a tick the trace records and by exactly one, and membership only inside recorded registrations and departures. Establishing it is the first paragraph’s work, and it turns on three things — tightness, so no caller but the game reaches the clock’s cores; the game reaching them only at honest parties, so no answer is mediated; and no core of \(\gamma \) handing the token to anything that could run one, the single call the clock’s cores place being responsive. Entries therefore append in execution order, each carrying the counter as its call returned. Steadiness then follows by comparing consecutive entries, since between them nothing runs. Unanimity is the longer half: it assumes the four conjuncts of the verdict and derives a contradiction from the invariant, using monotonicity of corruption to keep the party honest throughout. Everything rests on one invariant: the counter changes only inside a tick the trace records, and by exactly one; the membership only inside recorded registrations and departures. Both tables are written only in the cores of Chapter 17 — the counter at one line of \(\op {Update}\), stepping by one when the test of line 17 passes, \(\V {reg}\) in \(\op {Register}\) and \(\op {Deregister}\) — and those cores run only on calls passing \(\opl {Guard}\): with \(\admits \) pinned no caller but \(\Gm \) passes line 2, and \(\Gm \) calls only through the relays, at honest parties — at a corrupt one its own wrapper intercepted a step earlier and no core of \(\gamma \) ran — so no call is mediated and each core’s answer is the answer recorded. Moreover no core of \(\gamma \) hands the token to anything that could run one: the one call the clock’s cores place is the notification of line 20, which is responsive — \(\opl {Respond}\) refuses every call its answerer would place, whatever occupies the slot, and every mutation of \(\op {Update}\) precedes it in any case — and the relays’ one call is on the clock, that chain returning with no other machine of \(\gamma \) having run in between. Entries therefore append in execution order, each carrying the counter as its call returned.
For steadiness: before the first entry the counter is \(\op {Initialize}\)’s \(0 = \tau _0\). Between consecutive entries no core of \(\gamma \) runs, so the counter at entry \(j\) differs from that at entry \(j-1\) by the steps taken inside entry \(j\)’s own call: none for a read, a registration or a departure, none or one for a tick. Hence \(\tau _j \in \{\tau _{j-1}, \tau _{j-1}+1\}\) throughout, with the increment only at a tick, and line 28 gives \(0\).
For unanimity: suppose the four conjuncts of line 36 hold of some \(t\) and some \(P \in \Gclock .\Ps \setminus \Cs \) at the close — honest throughout, by monotonicity. A recorded registration answered \(\tau _r \leq t\) set \(\V {reg}[P] \gets 1\); only the cores of \(\op {Register}\) and \(\op {Deregister}\) write \(\V {reg}\), the game placed no \(\op {Deregister}\) at \(P\) — there is no \(\atom {dereg}\) entry — and the observers cannot reach an honest party, so \(\V {reg}[P] = 1\) from that moment on. Some entry answers \(\tau > t\), and by the invariant the answers are values the counter took, so it stepped from \(t\) to \(t+1\) inside some recorded tick; its line 17 read the flags of every party honest at that moment and registered then — \(P\) among them, the register only ever growing and \(\tau _r \leq t\) — so \(\V {tick}[P] = 1\). That flag is written only by the core of \(\op {Update}\) at \(P\) and cleared at every step of the counter and at every re-registration, so it was set while the counter stood at \(t\), by a tick of the game at \(P\); that tick answered \(t\), or \(t+1\) if it was itself the one that closed the round, and it was recorded. So \((\atom {tick},P,\tau ') \in \V {tr}\) for some \(\tau ' \in \{t,t+1\}\), contradicting the fourth conjunct, and line 36 gives \(0\). □
As with \(\Fsig \), the bound being \(0\) says only that the specification was written to have its properties; the content is the transfer, and here the notification of line 20 collects its price. Corollary 5.11 asks that the cores of the game system place no responsive call, and that line is one, so the transfer to a system \(\pi \) put in place of \(\{\Gclock \}\) must be argued directly, for the reason Remark 9.4 gives — and the same hypothesis guards Theorem 4.29, so a system built over the notifying clock forgoes dummy completeness with it. A clock without the notification — delete line 20 and the \(\uses \) entry — has both properties by the same proof and inherits them through the corollary with nothing to discharge.
The choice, note, is only which price, not whether. A notification through the ordinary \(\Adv (\cdot )\), the route \(\Fsig \) took, would hand the token to an adversary free to drive nested ticks before answering; answers would then append out of trace order, and steadiness would fail of the ideal clock itself — the two verdicts above are properties of \(\Gclock \) only because line 20 cannot be acted on before \(\op {Update}\) returns. So where \(\Fsig \) chose inheritance and paid with locality, a notifying clock must choose locality and pay with inheritance; the clock that pays neither is the one that tells the adversary nothing.