Made some more changes to the timestamp requirements. As it stood, there was no way to say that T_R >= m.clock for some honest m, as in the original draft. I changed things so that there is a well defined set Starters(R) of at least N-2F honest members that must start the round before it can be finalized, and that T_R is sandwiched between two such starters (with the annoying "max logic" still there).
I think now it is pretty clear that T_R >= m.clock for some honest m.
I am finding that it is super annoying and error prone to axiomatize these timestamp properties...I hope the current revision is good enough because I don't think it is worth it for me to spend too much more time tinkering with this.
Made some more changes to the timestamp requirements. As it stood, there was no way to say that T_R >= m.clock for some honest m, as in the original draft. I changed things so that there is a well defined set Starters(R) of at least N-2F honest members that must start the round before it can be finalized, and that T_R is sandwiched between two such starters (with the annoying "max logic" still there).
I think now it is pretty clear that T_R >= m.clock for some honest m.
I am finding that it is super annoying and error prone to axiomatize these timestamp properties...I hope the current revision is good enough because I don't think it is worth it for me to spend too much more time tinkering with this.