Hi Ernie,
Sorry for the ambiguity, I meant the parsing to be (interesting
protocol) specifications, not interesting (protocol specifications).
That is, there are interesting protocols (e.g. Paxos) whose
specifications (at most one value chosen, and ... implies some value
chosen) require at most trivial quantification. Someone who
understands nothing about why Paxos works can therefore check Paxos
(or any other protocol for consensus) with TLC.
There may be some confusion here. One verifies a spec L by showing
that it refines some other (higher-level) spec H. Existential
quantification (variable hiding) in L is irrelevant. It's the
existentially quantified variables in H that must be expressed in
terms of the variables (hidden or not) in L. So quantification
is irrelevant for checking Paxos--that is, for showing that Paxos
satisfies some other property.
An implementation of Paxos that uses all the same variables as Paxos,
so the refinement mapping is trivial, is pretty uninteresting. For
example, my specification of Paxos describes message passing in terms
of a single variable that is the set of all messages that have ever
been sent. No one is going to implement Paxos using a set the
remembers all sent messages. An actual implementation will describe
message passing in terms of various message queues, using
acknowledgements and retransmission to handle message loss, etc.
Since a real implementation won't remember all messages that have ever
been sent, it will need a history variable. In simple Paxos
implementations, it's easy to add the set of all messages ever sent as
a history variable, so the part of the refinement mapping that
describes the Paxos spec's representation of the set of all previously
sent messages in terms of the implementation's variables becomes
trivial. But that's not always the case. For example, my proof of
correctness of the Liskov-Paxos Byzantine agreement protocol shows
that the algorithm implements ordinary Paxos. More precisely, it
implements (a variant of) Paxos whose processes are the non-malicious
processes in the Liskov-Paxos algorithm. The refinement mapping is
not trivial.
Leslie