I have gone through the PBTS spec and have a bunch of comments. Instead of polluting PR #8600 with comments not specific to the PR, I have decided to open this issue. Please let me know if there is a better way to do it.

Main comments:

1. I do not think it is clear what MSGDELAY exactly means until proposalReceptionTime(p,r) is defined. My problem is that before this definition, it is unclear whether MSGDELAY only accounts for the message delivery delay (in the network sense) or also for the process receiving the proposal having entered the corresponding height and round. I think making sure this is clear from the beginning is fundamental for the spec. Also, sometimes the spec uses receive, others delivery, which makes things even more confusing.
2. I have some problems with the assumption that PRECISION>>ACCURACY. I think an upper-bound on PRECISION can be derived from (1)|Cp(t) - t| <= ACCURACY, given (2)|Cp(t) - Cq(t)| <= PRECISION. So I think we cannot really assume PRECISION>>ACCURACY. Let me informally elaborate a bit (and please correct me if I am wrong):
   • Consider two processes p and q, whose clocks are in the extremes. So by (1), Cp(t) - t = ACCURACY and t - Cq(t) = ACCURACY.
   • Then, Cp(t) - Cq(t) <= 2*ACCURACY .
   • Thus, by (2), PRECISION<=2*ACCURACY .
3. I don't quite follow the proof of Derived Proof-of-Locks.
   • "As r > v.round, we can affirm that v was not produced in round r".
     I am not sure how you get this. Are you assuming that v is unique and can be produced only once? I think we need a case split here. Assume p is the correct process that sent PREVOTE. Then either (i) p had nothing locked, (ii) was locked on v, (iii) locked on something else at a round < v_r.
   • "since a POL(v,r) was produced (by hypothesis) we can affirm that at least one correct process (also) observed a POL(v,v_r)"
     This assumes that the proposer picks up an existing value with vr != -1. We should consider other cases, even if to discard them by showing that are unfeasible.
   • "the above reasoning can be recursively applied until we get v_r' = v.round and observe a timely proof-of-lock"
     I would spell out the inductive argument. Once you prove that there exists a POL(v, vr) such that vr<r, then the required follows trivially from the induction hypothesis.
4. (Extra) It would be nice to have an intuition why safety and liveness hold.

Minor comments to improve presentation:

• I think we could improve the description of BFTTime with minimal changes.
  • Reshuffle things a bit. Before describing how it is implemented, I would describe what it guarantees: monotonicity and that it is not influenced by Byzantine validators. It is all there, but scattered. Then it is easy to relate the implementation decisions to the properties.
  • I would better motivate why having a relation to realtime is important, maybe with a simple example. So instead of linking a different file, I would simply copy what's there, here (or parts). Even for me, it is still unclear what may breaks.
• "Timestamps are retrieved from the validators' local clocks, with the only restriction that they must be monotonic"
  The use of monotonic here is consfusing. For me that sentence only means that the local time at a validator must grow monotonically. While the next sentence clarifies it, I wouldn't use monotonic here.
• "Validators can accept or reject a proposed block. A block is only accepted if its timestamp is acceptable".
  There are several reason why a validator may reject a proposal. I would rephrase that to something like: "Validators can accept or reject a proposed block based on the proposed timestamp. A proposed timestamp..."
• "Synchronous parameters"
  I would define what you mean by synchronous parameters. Are those parameters that capture time somewhat? One option is to remove synchronous from the sentence.
• "the end-to-end delay for delivering a message to all correct validators is bounded by MSGDELAY".
  As argued above, this needs to be very clearer. I believe that end-to-end delay is vague.
• "PRECISION and MSGDELAY are consensus parameters"
  What does this imply and why is a requirement. i.e., do things break if we do not assume this?
• "The left inequality of the timely predicate establishes that proposed timestamps should be in the past, when adjusted by the clocks PRECISION"
  I cannot really parse this sentence. I would rather say that proposed timestamps can be in the future by PRECISION at most. I think in essence, it says the same probably, but I find the former sentence confusing.
• "level detail"
  level of detail
• "The assumption that processes have access to synchronized clocks ensures that proposal times assigned by correct processes have a bounded relation with the real time"
  I think you need more than synchronized clocks. e.g., message delay bound (as in partial Synchrony) , the time for a validator to enter a legit round of a specific height is bound...
• "If p sends a proposal message m at real time t and q receives m at real time t', then t <= t' <= t + MSGDELAY."
  I would avoid the verb receive in general when talking to MSGDELAY, I find it very confusing.
• "For PBTS, a proposal is a tuple (v, v.time, v.round), where:"
  Maybe clarify that the analysis ignores heights?. Or say given an instance of consensus...
• "proposalReceptionTime(p,r) is the time p reads from its local clock when p is at round r and receives the proposal of round r."
  This really comes to late. There should be a text explaining this at the beginning.
• "let p is a such correct process:"
  let p BE such correct...
• "Instead, by the protocol operation, v was a valid value for the proposer of round r, which means that if the proposer has observed a POL(v,vr) with vr < r."
  This does not really add anything to the proof, meaning that assumes a correct proposer.