18.1 Functionality

The clock exists to be read, and the first reader is a network. Communication with a bounded delay is [11]’s; the diffusion form, delays measured on a shared clock, is the network the composable blockchain analyses run over [3]. The network \(\Fnet \) below is that functionality in the language of this paper — and the first example to use the clock rather than be it. Chapter 1 named a diffusion channel \(\Fdiffuse \) and owed no code; \(\Fnet \) is what such a channel looks like with time attached.

What it does is quickly said. The operation \(\opl {Send}\) timestamps the message by the clock — through \(\id _{\Gclock } := (\Gclock .\PID ,\id .P)\), the clock’s interface at the party being served, the notation of Section 17.2 — stores it, tells the adversary — the network is public — and answers a message id. The operation \(\opl {Fetch}\) asks the adversary what to reveal early, then answers everything released to the fetching party together with everything \(\Delta \) old. The division of power is the point: the adversary chooses when within \(\Delta \), and to whom first, and may add traffic of its own; what it cannot do is withhold an honest message past its time, and that bound sits in \(\op {Fetch}\)’s last line, where no answer of the slot reaches it. A message sent at time \(\tau \) is in every fetch from time \(\tau + \Delta \) on, whoever the adversary favoured first.

The fields.  They follow \(\Fsig \)’s pattern, not the clock’s. \(\PID \), \(\Ps \) and \(\admits \) are parameters: a network is local, one instance per session, its \(\admits \) naming the protocol it serves in the local pattern of Chapter 1 — and every instance reads the one shared clock, which is what makes “time \(\tau \)” comparable across sessions. \(\uses := \{(\Gclock ,\serves ),(\Adv ,\serves )\}\): the first entry requires the clock to serve every party the network does and is met, whatever session the network sits in, at the shared copy by the global disjunct of Definition 1.3 — a system containing \(\Fnet \) is well-formed only with the clock alongside — and the second covers the two slot calls below. \(\pars := \Delta \), a parameter a line of code actually reads, as \(\Frand \)’s \(n\) is (Chapter 13).

Scheduling is answered, not called.  [3] lets the adversary deliver a message early by acting on the network of its own accord. Transcribed literally that is an interface the adversary calls, so a local \(\admits \) containing \(\Apid \) — reachable from the slot in session \(0\) and in no other, the one shape Definition 7.2 excludes and relocation cannot carry. So the slot is asked instead: \(\op {Fetch}\) hands the adversary the time and takes back a pair \((S,I)\) — releases among the stored ids, injections of fresh traffic — sanitized inline, the good repair being canonical, as in Chapter 15. Both slot calls are responsive, the clock’s discipline. The operation \(\op {Send}\) mutates before it notifies; \(\op {Fetch}\) cannot, its mutations reading the answer, and responsiveness is what makes the difference immaterial: the token comes straight back, nothing else runs inside either call, and \(\Fsig \)’s re-entrance re-tests stay unnecessary here too.

Corruption, without a line of code.  A corrupt party’s \(\op {Send}\) and \(\op {Fetch}\) are intercepted by line 4 of the full interface before the cores run, so the buffer holds honest sends only, and the cores’ clock reads are never mediated — a timestamp is always the clock’s own word. What a corrupt party “sends”, the adversary supplies from the receiving side instead: the injections of line 16 enter the buffer with sender \(\none \) and timestamp \(\infty \), released to the fetching party alone — no age, and so no ripening into line 20’s guarantee, which is for the honest and never conscripts the adversary’s own traffic.

Three remarks on the code. Fetched pairs carry no sender: the network is an unauthenticated diffusion, [3]’s, and the injections are what unauthenticated means — a fetch may contain messages no one sent, the wire being the adversary’s to write. An authenticated diffusion is one field and one line away — return the sender the buffer already keeps, drop the injections. Authentication with addressing is a further step and a different object; Chapter 19 gives it. The table \(\V {rel}\) is sticky: what one fetch reveals no later fetch may hide, so a party’s view of the network only grows — and line 20 reads \(\V {rel}\) or the deadline, so the adversary’s silence past \(\Delta \) is simply ignored rather than punished. And \(\opl {Leak}\) returns the whole state, the network keeping no secrets: its contents were told to the adversary at line 8 as they arrived, and the release table is the slot’s own doing.