Protocol Change Proposal

Summary

@zeu5 brought up a problem in the filtering of messages. As a result we propose to update [PBTS-RECEPTION-STEP.0] to:

In the reception step at process p at local time now_p, upon receiving a message m:

• if the message m is of type PROPOSE and satisfies now_p - PRECISION - MSGDELAY < m.time < now_p + PRECISION, then mark the message as timely.

Problem Definition

The check to test the validity of the time proposed by the proposer is crucial for correctness. I am not sure how we came up with the current check, but here are the arguments for the proposed new check:

• Let T be the local time at a correct validator p when the a correct proposer sends m
• By precision we have
  • (A): T - PRECISION < m.time
  • (B): m.time < T + PRECISION.
• Let now_p be the time when m is received by p
• By the delay assumption we have:
  • (C) T <= now_p
  • (D) now_p <= T + MSGDELAY, that is, now_p - MSGDELAY <= T
• Eliminating T in (A) using (D) we get
  • (E) now_p - MSGDELAY - PRECISION < m.time
• Eliminating T in (B) using (C) we get
  • (F) m.time < now_p + PRECISION

The formulas (E) and (F) thus constitute the new check.

Proposal

• We need to recheck the property.
• We need to update the property in the spec as well as the mention in the formula in ADR-071

For Admin Use

• Not duplicate issue
• Appropriate labels applied
• Appropriate contributors tagged
• Contributor assigned/self-assigned