From 4cbdbbaac93b7a0baa204cbb37be0119d1bd2fec Mon Sep 17 00:00:00 2001 From: Zarko Milosevic Date: Thu, 1 Feb 2018 15:21:09 +0100 Subject: [PATCH] Add BFT time spec --- docs/specification/new-spec/bft-time.md | 42 +++++++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 docs/specification/new-spec/bft-time.md diff --git a/docs/specification/new-spec/bft-time.md b/docs/specification/new-spec/bft-time.md new file mode 100644 index 000000000..cbb1b65d4 --- /dev/null +++ b/docs/specification/new-spec/bft-time.md @@ -0,0 +1,42 @@ +# BFT time in Tendermint + +Tendermint provides a deterministic, Byzantine fault-tolerant, source of time. +Time in Tendermint is defined with the Time field of the block header. + +It satisfies the following properties: + +- Time Monotonicity: Time is monotonically increasing, i.e., given +a header H1 for height h1 and a header H2 for height `h2 = h1 + 1`, `H1.Time < H2.Time`. +- Time Validity: Given a set of Commit votes that forms the `block.LastCommit` field, a range of +valid values for the Time field of the block header is defined only by +Precommit messages (from the LastCommit field) sent by correct processes, i.e., +a faulty process cannot arbitrarily increase the Time value. + +In the context of Tendermint, time is of type int64 and denotes UNIX time in milliseconds, i.e., +corresponds to the number of milliseconds since January 1, 1970. Before defining rules that need to be enforced by the +Tendermint consensus protocol, so the properties above holds, we introduce the following definition: + +- median of a set of `Vote` messages is equal to the median of `Vote.Time` fields of the corresponding `Vote` messages + +We ensure Time Monotonicity and Time Validity properties by the following rules: + +- let rs denotes `RoundState` (consensus internal state) of some process. Then +`rs.ProposalBlock.Header.Time == median(rs.LastCommit) && +rs.Proposal.Timestamp == rs.ProposalBlock.Header.Time`. + +- Furthermore, when creating the `vote` message, the following rules for determining `vote.Time` field should hold: + + - if `rs.Proposal` is defined then + `vote.Time = max(rs.Proposal.Timestamp + 1, time.Now())`, where `time.Now()` + denotes local Unix time in milliseconds. + + - if `rs.Proposal` is not defined and `rs.Votes` contains +2/3 of the corresponding vote messages (votes for the + current height and round, and with the corresponding type (`Prevote` or `Precommit`)), then + + `vote.Time = max(median(getVotes(rs.Votes, vote.Height, vote.Round, vote.Type)), time.Now())`, + + where `getVotes` function returns the votes for particular `Height`, `Round` and `Type`. + The second rule is relevant for the case when a process jumps to a higher round upon receiving +2/3 votes for a higher + round, but the corresponding `Proposal` message for the higher round hasn't been received yet. + +