peerkeys files
--------------

 <F>            live file, loaded on startup, updated by secnet
                 (only).  * in-memory peerkeys_current is kept
                 synced with this file

 <F>~update     update file from config manager, checked before
                 every key exchange.  config manager must rename
                 this file into place; it will be renamed and
                 then removed by secnet.

 <F>~proc       update file being processed by secnet.
                 only secnet may write or remove.

 <F>~incoming   update file from peer, being received by secnet
                 may be incomplete, unverified, or even malicious
                 only secnet may write or remove.

 <F>~tmp        update file from config manager, only mss may
                 write or rename

secnet discards updates that are not more recent than (by
serial) the live file.  But it may not process updates
immediately.

The implied keyset to be used is MAX(live, proc, update).

secnet does:
 check live vs proc, either mv proc live or rm proc
 if proc doesn't exist, mv update proc

make-secnet-sites does:
 write: rename something onto update
 read: read update,proc,live in that order and take max

We support only one concurrent secnet, one concurrent
writing make-secnet-sites, and any number of readers.
We want to maintain a live file at all times as that
is what secnet actually reads at startup and uses.

Proof that this is sound:
  Let us regard update,proc,live as i=0,1,2
  Files contain public key sets and are manipulated as
   a whole, and we may regard key sets with the same
   serial as equivalent.
  We talk below about reading as if it were atomic.
   Actually the atomic operation is open(2); the
   reading gets whatever that name refers to.  So
   we can model this as an atomic read.
  secnet eventually moves all data into the live file
   or deletes it, so there should be no indefinitely
   stale data; informally this means we can disregard
   the possibility of very old serials and regard
   serials as fully ordered.  (We don't bother with
   a formal proof of this property.)
  Consequently we will only think about the serial
   and not the contents.  We treat absent files as
   minimal (we will write -1 for convenience although
   we don't mean a numerical value).  We write S(i).

Invariant 1 for secnet's transformations is as follows:
  Each file S(i) is only reduced (to S'(i)) if for some j S'(j)
  >= S(i), with S'(j) either being >= S(i) beforehand, or
  updated atomically together with S(i).

Proof of invariant 1 for the secnet operations:
  (a) check live vs proc, proc>live, mv:
     j=2, i=1; S'(i)=-1, so S(i) is being reduced.  S'(j) is
     equal to S(i), and the rename is atomic [1], so S'(j) and
     S'(i) are updated simultaneously.  S(j) is being
     increased.  (There are no hazards from concurrent writers;
     only we ourselves (secnet) write to live or proc.)
  (b) check live vs proc, proc<=live, rm:
     j=2, i=1; S'(i)=-1, so S(i) is being reduced.  But
     S(j) is >= $(i) throughout.  (Again, no concurrent
     writer hazards.)
  (c) mv update proc (when proc does not exist):
     j=1, i=0; S(i) is being reduced to -1.  But simultaneously
     S(j) is being increased to the old S(i).  Our precondition
     (proc not existing) is not subject to a concurrent writer
     hazards because only we write to proc; our action is
     atomic and takes whatever update is available (if any).

Proof of soundness for the mss reading operation:
  Let M be MAX(\forall S) at the point where mss reads update.
  Invariant 2: when mss reads S(k), MAX(K, S(k)..S(2)) >= M,
  where K is the max S it has seen so far.  Clearly this is
  true for k=0 (with K==-1).  secnet's operations never break
  this invariant because if any S() is reduced, another one
  counted must be increased.  mss's step operation
  updates K with S(k), so MAX(K', S(k+1)..)=MAX(K, S(k)..),
  and updates k to k+1, preserving the invariant.
  At the end we have k=3 and K=>M.  Since secnet never
  invents serials, K=M in the absence of an mss update
  with a bigger S.

Consideration of the mss update operation:
  Successive serials from sites file updates etc. are supposed
  to be increasing.  When this is true, M is increased.  A
  concurrent reading mss which makes its first read after the
  update will get the new data (by the proofs above).  This
  seems to be the required property.

QED.

[1] From "Base Specifications issue 7",
 2.9.7 Thread Interactions with Regular File Operations
 All of the following functions shall be atomic with respect to
 each other in the effects specified in POSIX.1-2017 when they
 operate on regular files or symbolic links:
  ... rename ... open ...