From 647cb45d7b50ea5f6ece58c708bffd6303c4cae7 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 08:52:21 +0100 Subject: [PATCH 01/26] PBTS model: precision, accuracy, and delay defs --- .../pbts-sysmodel_002_draft.md | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 832d11c9a..74bd0be3e 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -30,7 +30,7 @@ There exists a system parameter `PRECISION`, such that for any two processes `p` and `q`, with local clocks `C_p` and `C_q`, that read their local clocks at the same real-time `t`, we have: -- If `p` and `q` are equipped with synchronized clocks, then `|C_p(t) - C_q(t)| < PRECISION` +- If `p` and `q` are equipped with synchronized clocks, then `|C_p(t) - C_q(t)| <= PRECISION` `PRECISION` thus bounds the difference on the times simultaneously read by processes from their local clocks, so that their clocks can be considered synchronized. @@ -41,7 +41,7 @@ The [first draft][sysmodel_v1] of this specification included a second clock-rel that relates the values read by processes from their synchronized clocks with real time: - If `p` is a process is equipped with a synchronized clock, then at real time - `t` it reads from its clock time `C_p(t)` with `|C_p(t) - t| < ACCURACY` + `t` it reads from its clock time `C_p(t)` with `|C_p(t) - t| <= ACCURACY` The adoption of `ACCURACY` as the upper bound on the difference between clock readings and real time, however, renders the `PRECISION` parameter redundant. @@ -56,7 +56,7 @@ This allows us to adopt a relaxed version of the above `ACCURACY` definition: ##### **[PBTS-CLOCK-FAIR.0]** - At real time `t` there is at least one correct process `p` which clock marks - `C_p(t)` with `|C_p(t) - t| < ACCURACY` + `C_p(t)` with `|C_p(t) - t| <= ACCURACY` Then, through [PBTS-CLOCK-PRECISION] we can extend this relation of clock times with real time to every correct process, which will have a clock with accuracy @@ -81,15 +81,14 @@ an upper bound, the *maximum time* assigned to a proposal. #### **[PBTS-MSG-D.0]** -There exists a system parameter `MSGDELAY` for end-to-end delays of messages carrying proposals, -such for any two correct processes `p` and `q`, and any real time `t`: +There exists a system parameter `MSGDELAY` for end-to-end delays of proposal messages, +such for any two correct processes `p` and `q`: -- If `p` sends a message `m` carrying a proposal at time `ts`, -then if `q` receives the message and learns the proposal, -`q` does that at time `t` such that `ts <= t <= ts + MSGDELAY`. +- If `p` sends a message `m` carrying a proposal at real time `t`, then if `q` + receives `m`, it does that at time `t'` such that `t <= t' <= t' + MSGDELAY`. While we don't want to impose particular restrictions regarding the format of `m`, -we need to assume that their size is upper bounded. +we need to assume that their *size is upper bounded*. In practice, using messages with a fixed-size to carry proposals allows for a more accurate estimation of `MSGDELAY`, and therefore is advised. From 12ee640c419d69dcb590677dc10bbb95cf75d7e4 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 09:20:07 +0100 Subject: [PATCH 02/26] PBTS model: consensus properties reviewed --- .../pbts-sysmodel_002_draft.md | 31 ++++++++++++++----- 1 file changed, 24 insertions(+), 7 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 74bd0be3e..097089251 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -99,23 +99,40 @@ In this section we define the properties of Tendermint consensus #### **[PBTS-PROPOSE.0]** -A proposer proposes a consensus value `v` with an associated proposal time `v.time`. +A proposer proposes a consensus value `v` that includes a proposal time `v.time`. + +> We then restrict the allowed decisions along the following lines: #### **[PBTS-INV-AGREEMENT.0]** -[Agreement] No two correct processes decide on different values `v`. (This implies that no two correct processes decide on different proposal times `v.time`.) +> [Agreement] No two correct processes decide on different values `v`. +> (This implies that no two correct processes decide on different proposal +> times `v.time`.) #### **[PBTS-INV-VALID.0]** -[Validity] If a correct process decides on value `v`, -then `v` satisfies a predefined `valid` predicate. +> [Validity] If a correct process decides on value `v`, then `v` satisfies a +> predefined `valid` predicate. + +The `valid` predicate, in particular, verifies if proposal times are +[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity). + +This requires considering values proposed in different instances of consensus. +Let `decisions` be the array of values decided in instances of consensus, +indexed by their height: + +#### **[PBTS-VALID-MONOTONICITY.0]** + +- If `valid(v)`, where `v` is a value proposed at height `h` of consensus, + then for all heights `h' < h : v.time > decisions[h'].time`. #### **[PBTS-INV-TIMELY.0]** -[Time-Validity] If a correct process decides on value `v`, -then the associated proposal time `v.time` satisfies a predefined `timely` predicate. +> [Time-Validity] If a correct process decides on value `v`, then `v.time` +> satisfies a predefined `timely` predicate. -> Both [Validity] and [Time-Validity] must be observed even if up to `2f` validators are faulty. +Both [Validity] and [Time-Validity] must be observed even if up to `2f` +validators are faulty. ### Timely proposals From 814f9c48a88d4974c16dbfec37e2f42a385775c3 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 09:30:30 +0100 Subject: [PATCH 03/26] PBTS model: reinforcing alignment with UTC --- .../proposer-based-timestamp/pbts-sysmodel_002_draft.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 097089251..c98d47f73 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -4,13 +4,15 @@ #### **[PBTS-CLOCK-NEWTON.0]** -There is a reference Newtonian real-time `t` (UTC). +There is a reference Newtonian real-time `t`. No process has direct access to this reference time, used only for specification purposes. +The reference real-time is assumed to be aligned with the Coordinated Universal Time (UTC). ### Synchronized clocks -Processes are assumed to be equipped with synchronized clocks. +Processes are assumed to be equipped with synchronized clocks, +aligned with the Coordinated Universal Time (UTC). This requires processes to periodically synchronize their local clocks with an external and trusted source of the time (e.g. NTP servers). @@ -58,7 +60,7 @@ This allows us to adopt a relaxed version of the above `ACCURACY` definition: - At real time `t` there is at least one correct process `p` which clock marks `C_p(t)` with `|C_p(t) - t| <= ACCURACY` -Then, through [PBTS-CLOCK-PRECISION] we can extend this relation of clock times +Then, through [PBTS-CLOCK-PRECISION.0] we can extend this relation of clock times with real time to every correct process, which will have a clock with accuracy bound by `ACCURACY + PRECISION`. But, for the sake of simpler specification we can assume that the `PRECISION`, From 7c18359a7f55af3941ac2f8bd75cab939538a207 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 09:38:08 +0100 Subject: [PATCH 04/26] PBTS model: precision parameter embodies accuracy --- .../pbts-sysmodel_002_draft.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index c98d47f73..c165e658a 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -61,11 +61,15 @@ This allows us to adopt a relaxed version of the above `ACCURACY` definition: `C_p(t)` with `|C_p(t) - t| <= ACCURACY` Then, through [PBTS-CLOCK-PRECISION.0] we can extend this relation of clock times -with real time to every correct process, which will have a clock with accuracy -bound by `ACCURACY + PRECISION`. -But, for the sake of simpler specification we can assume that the `PRECISION`, -which is a worst-case parameter that applies to all correct processes, -includes the best `ACCURACY` achieved by any of them. +with real time to every correct process: + +- At real time `t` the synchronized clock of any correct process `p` marks + `C_p(t)` with `|C_p(t) - t| <= ACCURACY + PRECISION` + +But, for the sake of simplicity, we can assume that `PRECISION >> ACCURACY`, +and therefore the `PRECISION` parameter embodies the `ACCURACY` obtained +through the periodic synchronization of local clocks with an external and +trusted source of the time. ### Message Delays From f778591c464a0cd93b79a660c9fd478da5b80781 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 13:52:57 +0100 Subject: [PATCH 05/26] PBTS model: discussion about accuracy shortened --- .../pbts-sysmodel_002_draft.md | 74 +++++++++---------- 1 file changed, 35 insertions(+), 39 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index c165e658a..1f908cd19 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -1,5 +1,12 @@ # PBTS: System Model and Properties +## Outline + + - [System model](#system-model) + - [Synchronized clocks](#synchronized-clocks) + - [Message delays](#message-delays) + - [Problem Statement](#problem-statement) + ## System Model #### **[PBTS-CLOCK-NEWTON.0]** @@ -29,47 +36,36 @@ and drifts of local clocks from real time. #### **[PBTS-CLOCK-PRECISION.0]** There exists a system parameter `PRECISION`, such that -for any two processes `p` and `q`, with local clocks `C_p` and `C_q`, -that read their local clocks at the same real-time `t`, we have: +for any two processes `p` and `q`, with local clocks `C_p` and `C_q`: -- If `p` and `q` are equipped with synchronized clocks, then `|C_p(t) - C_q(t)| <= PRECISION` +- If `p` and `q` are equipped with synchronized clocks, + then for any real-time `t` we have `|C_p(t) - C_q(t)| <= PRECISION`. `PRECISION` thus bounds the difference on the times simultaneously read by processes from their local clocks, so that their clocks can be considered synchronized. #### Accuracy -The [first draft][sysmodel_v1] of this specification included a second clock-related parameter, `ACCURACY`, -that relates the values read by processes from their synchronized clocks with real time: - -- If `p` is a process is equipped with a synchronized clock, then at real time - `t` it reads from its clock time `C_p(t)` with `|C_p(t) - t| <= ACCURACY` +A second relevant clock parameter is accuracy, which binds the values read by +processes from their clocks to real time. -The adoption of `ACCURACY` as the upper bound on the difference between clock -readings and real time, however, renders the `PRECISION` parameter redundant. -In fact, if we assume that clocks readings are at most `ACCURACY` from real -time, we would therefore be assuming that they cannot be more than `2 * ACCURACY` -apart from each other, thus establishing a worst-case upper bound for `PRECISION`. -The approach we take is to assume that processes clocks are periodically -synchronized with an external source of time, thus improving their accuracy. -This allows us to adopt a relaxed version of the above `ACCURACY` definition: +##### **[PBTS-CLOCK-ACCURACY.0]** -##### **[PBTS-CLOCK-FAIR.0]** +For the sake of completeness, we define a parameter `ACCURACY` such that: - At real time `t` there is at least one correct process `p` which clock marks - `C_p(t)` with `|C_p(t) - t| <= ACCURACY` + `C_p(t)` with `|C_p(t) - t| <= ACCURACY`. -Then, through [PBTS-CLOCK-PRECISION.0] we can extend this relation of clock times -with real time to every correct process: +As a consequence, applying the definition of `PRECISION`, we have: - At real time `t` the synchronized clock of any correct process `p` marks - `C_p(t)` with `|C_p(t) - t| <= ACCURACY + PRECISION` + `C_p(t)` with `|C_p(t) - t| <= ACCURACY + PRECISION`. -But, for the sake of simplicity, we can assume that `PRECISION >> ACCURACY`, -and therefore the `PRECISION` parameter embodies the `ACCURACY` obtained -through the periodic synchronization of local clocks with an external and -trusted source of the time. +The reason for not adopting `ACCURACY` as a system parameter is the assumption +that `PRECISION >> ACCURACY`. +This allows us to consider, for practical purposes, that the `PRECISION` system +parameter embodies the `ACCURACY` model parameter. ### Message Delays @@ -85,7 +81,7 @@ defining a lower bound, a *minimum time* that a correct process assigns to propo While *minimum delay* for delivering a proposal to a destination allows defining an upper bound, the *maximum time* assigned to a proposal. -#### **[PBTS-MSG-D.0]** +#### **[PBTS-MSG-DELAY.0]** There exists a system parameter `MSGDELAY` for end-to-end delays of proposal messages, such for any two correct processes `p` and `q`: @@ -111,34 +107,34 @@ A proposer proposes a consensus value `v` that includes a proposal time `v.time` #### **[PBTS-INV-AGREEMENT.0]** -> [Agreement] No two correct processes decide on different values `v`. -> (This implies that no two correct processes decide on different proposal -> times `v.time`.) +- [Agreement] No two correct processes decide on different values `v`. This + implies that no two correct processes decide on different proposal times + `v.time`. #### **[PBTS-INV-VALID.0]** -> [Validity] If a correct process decides on value `v`, then `v` satisfies a -> predefined `valid` predicate. +- [Validity] If a correct process decides on value `v`, then `v` satisfies a + predefined `valid` predicate. The `valid` predicate, in particular, verifies if proposal times are -[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity). +[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity), +which requires considering values from different instances of consensus. + +##### **[PBTS-VALID-MONOTONICITY.0]** -This requires considering values proposed in different instances of consensus. Let `decisions` be the array of values decided in instances of consensus, indexed by their height: -#### **[PBTS-VALID-MONOTONICITY.0]** - - If `valid(v)`, where `v` is a value proposed at height `h` of consensus, then for all heights `h' < h : v.time > decisions[h'].time`. #### **[PBTS-INV-TIMELY.0]** -> [Time-Validity] If a correct process decides on value `v`, then `v.time` -> satisfies a predefined `timely` predicate. +- [Time-Validity] If a correct process decides on value `v`, then `v.time` + satisfies a predefined `timely` predicate. -Both [Validity] and [Time-Validity] must be observed even if up to `2f` -validators are faulty. +> Both [Validity] and [Time-Validity] must be observed even if up to `2f` +> validators are faulty. ### Timely proposals From c363be2f6552c0e8311c9ed355468cabf11a9a42 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 14:15:52 +0100 Subject: [PATCH 06/26] PBTS model: proposal time monotonocity rephrased --- .../pbts-sysmodel_002_draft.md | 21 ++++++++----------- 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 1f908cd19..3d98ac565 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -107,26 +107,23 @@ A proposer proposes a consensus value `v` that includes a proposal time `v.time` #### **[PBTS-INV-AGREEMENT.0]** -- [Agreement] No two correct processes decide on different values `v`. This - implies that no two correct processes decide on different proposal times - `v.time`. +- [Agreement] No two correct processes decide on different values `v`. + +This implies that no two correct processes decide on different proposal times +`v.time`. #### **[PBTS-INV-VALID.0]** - [Validity] If a correct process decides on value `v`, then `v` satisfies a predefined `valid` predicate. -The `valid` predicate, in particular, verifies if proposal times are -[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity), -which requires considering values from different instances of consensus. - -##### **[PBTS-VALID-MONOTONICITY.0]** +With respect to PBTS, the `valid` predicate requires proposal times to be +[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity): -Let `decisions` be the array of values decided in instances of consensus, -indexed by their height: +##### **[PBTS-INV-MONOTONICITY.0]** -- If `valid(v)`, where `v` is a value proposed at height `h` of consensus, - then for all heights `h' < h : v.time > decisions[h'].time`. +- If a correct process decides on value `v = decision[h]` at height `h` of + consensus, then for every height `h' < h : decision[h'].time < v.time`. #### **[PBTS-INV-TIMELY.0]** From 4374a1e6f23ae2751700eb2c81f675142ba9b300 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 08:52:21 +0100 Subject: [PATCH 07/26] PBTS model: precision, accuracy, and delay defs --- .../pbts-sysmodel_002_draft.md | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 832d11c9a..74bd0be3e 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -30,7 +30,7 @@ There exists a system parameter `PRECISION`, such that for any two processes `p` and `q`, with local clocks `C_p` and `C_q`, that read their local clocks at the same real-time `t`, we have: -- If `p` and `q` are equipped with synchronized clocks, then `|C_p(t) - C_q(t)| < PRECISION` +- If `p` and `q` are equipped with synchronized clocks, then `|C_p(t) - C_q(t)| <= PRECISION` `PRECISION` thus bounds the difference on the times simultaneously read by processes from their local clocks, so that their clocks can be considered synchronized. @@ -41,7 +41,7 @@ The [first draft][sysmodel_v1] of this specification included a second clock-rel that relates the values read by processes from their synchronized clocks with real time: - If `p` is a process is equipped with a synchronized clock, then at real time - `t` it reads from its clock time `C_p(t)` with `|C_p(t) - t| < ACCURACY` + `t` it reads from its clock time `C_p(t)` with `|C_p(t) - t| <= ACCURACY` The adoption of `ACCURACY` as the upper bound on the difference between clock readings and real time, however, renders the `PRECISION` parameter redundant. @@ -56,7 +56,7 @@ This allows us to adopt a relaxed version of the above `ACCURACY` definition: ##### **[PBTS-CLOCK-FAIR.0]** - At real time `t` there is at least one correct process `p` which clock marks - `C_p(t)` with `|C_p(t) - t| < ACCURACY` + `C_p(t)` with `|C_p(t) - t| <= ACCURACY` Then, through [PBTS-CLOCK-PRECISION] we can extend this relation of clock times with real time to every correct process, which will have a clock with accuracy @@ -81,15 +81,14 @@ an upper bound, the *maximum time* assigned to a proposal. #### **[PBTS-MSG-D.0]** -There exists a system parameter `MSGDELAY` for end-to-end delays of messages carrying proposals, -such for any two correct processes `p` and `q`, and any real time `t`: +There exists a system parameter `MSGDELAY` for end-to-end delays of proposal messages, +such for any two correct processes `p` and `q`: -- If `p` sends a message `m` carrying a proposal at time `ts`, -then if `q` receives the message and learns the proposal, -`q` does that at time `t` such that `ts <= t <= ts + MSGDELAY`. +- If `p` sends a message `m` carrying a proposal at real time `t`, then if `q` + receives `m`, it does that at time `t'` such that `t <= t' <= t' + MSGDELAY`. While we don't want to impose particular restrictions regarding the format of `m`, -we need to assume that their size is upper bounded. +we need to assume that their *size is upper bounded*. In practice, using messages with a fixed-size to carry proposals allows for a more accurate estimation of `MSGDELAY`, and therefore is advised. From 9ceb5044205ec2906f3d0a07f81163ec6da0cfba Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 09:20:07 +0100 Subject: [PATCH 08/26] PBTS model: consensus properties reviewed --- .../pbts-sysmodel_002_draft.md | 31 ++++++++++++++----- 1 file changed, 24 insertions(+), 7 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 74bd0be3e..097089251 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -99,23 +99,40 @@ In this section we define the properties of Tendermint consensus #### **[PBTS-PROPOSE.0]** -A proposer proposes a consensus value `v` with an associated proposal time `v.time`. +A proposer proposes a consensus value `v` that includes a proposal time `v.time`. + +> We then restrict the allowed decisions along the following lines: #### **[PBTS-INV-AGREEMENT.0]** -[Agreement] No two correct processes decide on different values `v`. (This implies that no two correct processes decide on different proposal times `v.time`.) +> [Agreement] No two correct processes decide on different values `v`. +> (This implies that no two correct processes decide on different proposal +> times `v.time`.) #### **[PBTS-INV-VALID.0]** -[Validity] If a correct process decides on value `v`, -then `v` satisfies a predefined `valid` predicate. +> [Validity] If a correct process decides on value `v`, then `v` satisfies a +> predefined `valid` predicate. + +The `valid` predicate, in particular, verifies if proposal times are +[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity). + +This requires considering values proposed in different instances of consensus. +Let `decisions` be the array of values decided in instances of consensus, +indexed by their height: + +#### **[PBTS-VALID-MONOTONICITY.0]** + +- If `valid(v)`, where `v` is a value proposed at height `h` of consensus, + then for all heights `h' < h : v.time > decisions[h'].time`. #### **[PBTS-INV-TIMELY.0]** -[Time-Validity] If a correct process decides on value `v`, -then the associated proposal time `v.time` satisfies a predefined `timely` predicate. +> [Time-Validity] If a correct process decides on value `v`, then `v.time` +> satisfies a predefined `timely` predicate. -> Both [Validity] and [Time-Validity] must be observed even if up to `2f` validators are faulty. +Both [Validity] and [Time-Validity] must be observed even if up to `2f` +validators are faulty. ### Timely proposals From f404b2709351ee29ca287cd9fa3c502ae26a0d4c Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 09:30:30 +0100 Subject: [PATCH 09/26] PBTS model: reinforcing alignment with UTC --- .../proposer-based-timestamp/pbts-sysmodel_002_draft.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 097089251..c98d47f73 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -4,13 +4,15 @@ #### **[PBTS-CLOCK-NEWTON.0]** -There is a reference Newtonian real-time `t` (UTC). +There is a reference Newtonian real-time `t`. No process has direct access to this reference time, used only for specification purposes. +The reference real-time is assumed to be aligned with the Coordinated Universal Time (UTC). ### Synchronized clocks -Processes are assumed to be equipped with synchronized clocks. +Processes are assumed to be equipped with synchronized clocks, +aligned with the Coordinated Universal Time (UTC). This requires processes to periodically synchronize their local clocks with an external and trusted source of the time (e.g. NTP servers). @@ -58,7 +60,7 @@ This allows us to adopt a relaxed version of the above `ACCURACY` definition: - At real time `t` there is at least one correct process `p` which clock marks `C_p(t)` with `|C_p(t) - t| <= ACCURACY` -Then, through [PBTS-CLOCK-PRECISION] we can extend this relation of clock times +Then, through [PBTS-CLOCK-PRECISION.0] we can extend this relation of clock times with real time to every correct process, which will have a clock with accuracy bound by `ACCURACY + PRECISION`. But, for the sake of simpler specification we can assume that the `PRECISION`, From cbc2a9194a73e6009c9b0ffd11dde94b0e9f0a10 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 09:38:08 +0100 Subject: [PATCH 10/26] PBTS model: precision parameter embodies accuracy --- .../pbts-sysmodel_002_draft.md | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index c98d47f73..c165e658a 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -61,11 +61,15 @@ This allows us to adopt a relaxed version of the above `ACCURACY` definition: `C_p(t)` with `|C_p(t) - t| <= ACCURACY` Then, through [PBTS-CLOCK-PRECISION.0] we can extend this relation of clock times -with real time to every correct process, which will have a clock with accuracy -bound by `ACCURACY + PRECISION`. -But, for the sake of simpler specification we can assume that the `PRECISION`, -which is a worst-case parameter that applies to all correct processes, -includes the best `ACCURACY` achieved by any of them. +with real time to every correct process: + +- At real time `t` the synchronized clock of any correct process `p` marks + `C_p(t)` with `|C_p(t) - t| <= ACCURACY + PRECISION` + +But, for the sake of simplicity, we can assume that `PRECISION >> ACCURACY`, +and therefore the `PRECISION` parameter embodies the `ACCURACY` obtained +through the periodic synchronization of local clocks with an external and +trusted source of the time. ### Message Delays From 1aa4be51c39c00a72616a7cf9996d9b8dd425c24 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 13:52:57 +0100 Subject: [PATCH 11/26] PBTS model: discussion about accuracy shortened --- .../pbts-sysmodel_002_draft.md | 74 +++++++++---------- 1 file changed, 35 insertions(+), 39 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index c165e658a..1f908cd19 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -1,5 +1,12 @@ # PBTS: System Model and Properties +## Outline + + - [System model](#system-model) + - [Synchronized clocks](#synchronized-clocks) + - [Message delays](#message-delays) + - [Problem Statement](#problem-statement) + ## System Model #### **[PBTS-CLOCK-NEWTON.0]** @@ -29,47 +36,36 @@ and drifts of local clocks from real time. #### **[PBTS-CLOCK-PRECISION.0]** There exists a system parameter `PRECISION`, such that -for any two processes `p` and `q`, with local clocks `C_p` and `C_q`, -that read their local clocks at the same real-time `t`, we have: +for any two processes `p` and `q`, with local clocks `C_p` and `C_q`: -- If `p` and `q` are equipped with synchronized clocks, then `|C_p(t) - C_q(t)| <= PRECISION` +- If `p` and `q` are equipped with synchronized clocks, + then for any real-time `t` we have `|C_p(t) - C_q(t)| <= PRECISION`. `PRECISION` thus bounds the difference on the times simultaneously read by processes from their local clocks, so that their clocks can be considered synchronized. #### Accuracy -The [first draft][sysmodel_v1] of this specification included a second clock-related parameter, `ACCURACY`, -that relates the values read by processes from their synchronized clocks with real time: - -- If `p` is a process is equipped with a synchronized clock, then at real time - `t` it reads from its clock time `C_p(t)` with `|C_p(t) - t| <= ACCURACY` +A second relevant clock parameter is accuracy, which binds the values read by +processes from their clocks to real time. -The adoption of `ACCURACY` as the upper bound on the difference between clock -readings and real time, however, renders the `PRECISION` parameter redundant. -In fact, if we assume that clocks readings are at most `ACCURACY` from real -time, we would therefore be assuming that they cannot be more than `2 * ACCURACY` -apart from each other, thus establishing a worst-case upper bound for `PRECISION`. -The approach we take is to assume that processes clocks are periodically -synchronized with an external source of time, thus improving their accuracy. -This allows us to adopt a relaxed version of the above `ACCURACY` definition: +##### **[PBTS-CLOCK-ACCURACY.0]** -##### **[PBTS-CLOCK-FAIR.0]** +For the sake of completeness, we define a parameter `ACCURACY` such that: - At real time `t` there is at least one correct process `p` which clock marks - `C_p(t)` with `|C_p(t) - t| <= ACCURACY` + `C_p(t)` with `|C_p(t) - t| <= ACCURACY`. -Then, through [PBTS-CLOCK-PRECISION.0] we can extend this relation of clock times -with real time to every correct process: +As a consequence, applying the definition of `PRECISION`, we have: - At real time `t` the synchronized clock of any correct process `p` marks - `C_p(t)` with `|C_p(t) - t| <= ACCURACY + PRECISION` + `C_p(t)` with `|C_p(t) - t| <= ACCURACY + PRECISION`. -But, for the sake of simplicity, we can assume that `PRECISION >> ACCURACY`, -and therefore the `PRECISION` parameter embodies the `ACCURACY` obtained -through the periodic synchronization of local clocks with an external and -trusted source of the time. +The reason for not adopting `ACCURACY` as a system parameter is the assumption +that `PRECISION >> ACCURACY`. +This allows us to consider, for practical purposes, that the `PRECISION` system +parameter embodies the `ACCURACY` model parameter. ### Message Delays @@ -85,7 +81,7 @@ defining a lower bound, a *minimum time* that a correct process assigns to propo While *minimum delay* for delivering a proposal to a destination allows defining an upper bound, the *maximum time* assigned to a proposal. -#### **[PBTS-MSG-D.0]** +#### **[PBTS-MSG-DELAY.0]** There exists a system parameter `MSGDELAY` for end-to-end delays of proposal messages, such for any two correct processes `p` and `q`: @@ -111,34 +107,34 @@ A proposer proposes a consensus value `v` that includes a proposal time `v.time` #### **[PBTS-INV-AGREEMENT.0]** -> [Agreement] No two correct processes decide on different values `v`. -> (This implies that no two correct processes decide on different proposal -> times `v.time`.) +- [Agreement] No two correct processes decide on different values `v`. This + implies that no two correct processes decide on different proposal times + `v.time`. #### **[PBTS-INV-VALID.0]** -> [Validity] If a correct process decides on value `v`, then `v` satisfies a -> predefined `valid` predicate. +- [Validity] If a correct process decides on value `v`, then `v` satisfies a + predefined `valid` predicate. The `valid` predicate, in particular, verifies if proposal times are -[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity). +[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity), +which requires considering values from different instances of consensus. + +##### **[PBTS-VALID-MONOTONICITY.0]** -This requires considering values proposed in different instances of consensus. Let `decisions` be the array of values decided in instances of consensus, indexed by their height: -#### **[PBTS-VALID-MONOTONICITY.0]** - - If `valid(v)`, where `v` is a value proposed at height `h` of consensus, then for all heights `h' < h : v.time > decisions[h'].time`. #### **[PBTS-INV-TIMELY.0]** -> [Time-Validity] If a correct process decides on value `v`, then `v.time` -> satisfies a predefined `timely` predicate. +- [Time-Validity] If a correct process decides on value `v`, then `v.time` + satisfies a predefined `timely` predicate. -Both [Validity] and [Time-Validity] must be observed even if up to `2f` -validators are faulty. +> Both [Validity] and [Time-Validity] must be observed even if up to `2f` +> validators are faulty. ### Timely proposals From b8c2f9fa1e930bbebc5babe038638780c9d4ea1c Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Wed, 9 Mar 2022 14:15:52 +0100 Subject: [PATCH 12/26] PBTS model: proposal time monotonocity rephrased --- .../pbts-sysmodel_002_draft.md | 21 ++++++++----------- 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 1f908cd19..3d98ac565 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -107,26 +107,23 @@ A proposer proposes a consensus value `v` that includes a proposal time `v.time` #### **[PBTS-INV-AGREEMENT.0]** -- [Agreement] No two correct processes decide on different values `v`. This - implies that no two correct processes decide on different proposal times - `v.time`. +- [Agreement] No two correct processes decide on different values `v`. + +This implies that no two correct processes decide on different proposal times +`v.time`. #### **[PBTS-INV-VALID.0]** - [Validity] If a correct process decides on value `v`, then `v` satisfies a predefined `valid` predicate. -The `valid` predicate, in particular, verifies if proposal times are -[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity), -which requires considering values from different instances of consensus. - -##### **[PBTS-VALID-MONOTONICITY.0]** +With respect to PBTS, the `valid` predicate requires proposal times to be +[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity): -Let `decisions` be the array of values decided in instances of consensus, -indexed by their height: +##### **[PBTS-INV-MONOTONICITY.0]** -- If `valid(v)`, where `v` is a value proposed at height `h` of consensus, - then for all heights `h' < h : v.time > decisions[h'].time`. +- If a correct process decides on value `v = decision[h]` at height `h` of + consensus, then for every height `h' < h : decision[h'].time < v.time`. #### **[PBTS-INV-TIMELY.0]** From 46fed3c16a8aa667f4ea755a47079fa3dcdab5e8 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Fri, 11 Mar 2022 08:28:26 +0100 Subject: [PATCH 13/26] PBTS model: Safety Invariants subsection --- .../pbts-sysmodel_002_draft.md | 22 ++++++++++++++----- 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 3d98ac565..c66902087 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -6,6 +6,8 @@ - [Synchronized clocks](#synchronized-clocks) - [Message delays](#message-delays) - [Problem Statement](#problem-statement) + - [Safety Invariants](#safety-invariants) + - [Temporal Safety](#temporal-safety) ## System Model @@ -49,7 +51,6 @@ from their local clocks, so that their clocks can be considered synchronized. A second relevant clock parameter is accuracy, which binds the values read by processes from their clocks to real time. - ##### **[PBTS-CLOCK-ACCURACY.0]** For the sake of completeness, we define a parameter `ACCURACY` such that: @@ -97,13 +98,15 @@ for a more accurate estimation of `MSGDELAY`, and therefore is advised. ## Problem Statement In this section we define the properties of Tendermint consensus -(cf. the [arXiv paper][arXiv]) in this new system model. +(cf. the [arXiv paper][arXiv]) in this system model. #### **[PBTS-PROPOSE.0]** A proposer proposes a consensus value `v` that includes a proposal time `v.time`. -> We then restrict the allowed decisions along the following lines: +### Safety Invariants + +We then restrict the allowed decisions along the following lines: #### **[PBTS-INV-AGREEMENT.0]** @@ -118,12 +121,19 @@ This implies that no two correct processes decide on different proposal times predefined `valid` predicate. With respect to PBTS, the `valid` predicate requires proposal times to be -[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity): +[monotonic](./pbts-algorithm_002_draft.md#time-monotonicity) over heights of +consensus: ##### **[PBTS-INV-MONOTONICITY.0]** -- If a correct process decides on value `v = decision[h]` at height `h` of - consensus, then for every height `h' < h : decision[h'].time < v.time`. +- If a correct process decides on value `v` at the height `h` of consensus, + thus setting `decision[h] = v`, then `v.time > decision[h'].time` for all + previous heights `h' < h`. + +The monotonicity of proposal times, and external validity in general, +implicitly assumes that heights of consensus are executed in order. + +### Temporal Safety #### **[PBTS-INV-TIMELY.0]** From 2553c3564319d3f840c99ab2c03b3fa79f417f96 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Tue, 15 Mar 2022 09:48:41 +0100 Subject: [PATCH 14/26] PBTS model: MSGDELAY description shortened --- .../pbts-sysmodel_002_draft.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index c66902087..2b4df9f32 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -87,13 +87,13 @@ an upper bound, the *maximum time* assigned to a proposal. There exists a system parameter `MSGDELAY` for end-to-end delays of proposal messages, such for any two correct processes `p` and `q`: -- If `p` sends a message `m` carrying a proposal at real time `t`, then if `q` - receives `m`, it does that at time `t'` such that `t <= t' <= t' + MSGDELAY`. +- If `p` sends a proposal message `m` at real time `t` and `q` receives `m` at + real time `t'`, then `t <= t' <= t' + MSGDELAY`. -While we don't want to impose particular restrictions regarding the format of `m`, -we need to assume that their *size is upper bounded*. -In practice, using messages with a fixed-size to carry proposals allows -for a more accurate estimation of `MSGDELAY`, and therefore is advised. +Notice that, as a system parameter, `MSGDELAY` should be observed for any +proposal message broadcast by correct processes: it is a *worst-case* parameter. +As message delays depends on the message size, the above requirement implicty +indicates that the size of proposal messages is either fixed or upper bounded. ## Problem Statement From 69deb3847919df38f1aee67f83ff1033d8ce4e17 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Tue, 15 Mar 2022 10:38:41 +0100 Subject: [PATCH 15/26] PBTS model: timely proposals definition refined --- .../pbts-sysmodel_002_draft.md | 45 ++++++++++++------- 1 file changed, 29 insertions(+), 16 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 2b4df9f32..8ac6a0e25 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -7,7 +7,7 @@ - [Message delays](#message-delays) - [Problem Statement](#problem-statement) - [Safety Invariants](#safety-invariants) - - [Temporal Safety](#temporal-safety) + - [Timely Proposals](#timely-proposals) ## System Model @@ -21,7 +21,7 @@ The reference real-time is assumed to be aligned with the Coordinated Universal ### Synchronized clocks Processes are assumed to be equipped with synchronized clocks, -aligned with the Coordinated Universal Time (UTC). +aligned with the Coordinated Universal Time (UTC). This requires processes to periodically synchronize their local clocks with an external and trusted source of the time (e.g. NTP servers). @@ -102,7 +102,8 @@ In this section we define the properties of Tendermint consensus #### **[PBTS-PROPOSE.0]** -A proposer proposes a consensus value `v` that includes a proposal time `v.time`. +A proposer proposes a consensus value `v` that includes a proposal time +`v.time`. ### Safety Invariants @@ -133,27 +134,39 @@ consensus: The monotonicity of proposal times, and external validity in general, implicitly assumes that heights of consensus are executed in order. -### Temporal Safety +### Timely proposals + +PBTS introduces a synchronous property that restrict the allowed decisions +based on the proposal time `v.time` associated with a proposed value `v`. +The property is based in the `timely` predicate defined in the following: #### **[PBTS-INV-TIMELY.0]** -- [Time-Validity] If a correct process decides on value `v`, then `v.time` - satisfies a predefined `timely` predicate. +- [Time-Validity] If a correct process decides on value `v`, then the proposal + message proposing `v` was considered `timely` by at least `f+1` processes. -> Both [Validity] and [Time-Validity] must be observed even if up to `2f` -> validators are faulty. +The `timely` predicate is evaluated when a process receives a proposal in a +round of consensus. +A proposal is a tuple `(v, v.time, v.round)`, where `v` is the proposed value, +`v.time` the proposal time, and `v.round` is the round at which `v` was first +proposed (and `v.time` was assigned). +While the same proposal can be proposed multiple time, in different rounds of +consensus, we are interested on the first time it was proposed: -### Timely proposals +##### **[PBTS-RECEPTION-STEP.0]** + +Let `p` be a correct process which is at round `r` of consensus: + +- `receiveTime_p[r]` is the time `p` reads from its local clock when it + receives the proposal `(v, v.time, v.round)` with `v.round = r`. -The `timely` predicate is evaluated when a process receives a proposal. -Let `now_p` be time a process `p` reads from its local clock when `p` receives a proposal. -Let `v` be the proposed value and `v.time` the proposal time. -The proposal is considered `timely` by `p` if: +##### **[PBTS-TIMELY.0]** -#### **[PBTS-RECEPTION-STEP.1]** +The proposal `(v, v.time, v.round)` for `v` is considered `timely` by a correct +process `p` if: -1. `now_p >= v.time - PRECISION` and -1. `now_p <= v.time + MSGDELAY + PRECISION` +1. `receiveTime_p[v.round] >= v.time - PRECISION` and +1. `receiveTime_p[v.round] <= v.time + MSGDELAY + PRECISION` ### Timely Proof-of-Locks From 50f079a8caac5cd83fc7a0a146a7449f250cbbc3 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Tue, 15 Mar 2022 10:51:08 +0100 Subject: [PATCH 16/26] PBTS model: some formatting changes --- .../pbts-sysmodel_002_draft.md | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 8ac6a0e25..c09218590 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -92,7 +92,7 @@ such for any two correct processes `p` and `q`: Notice that, as a system parameter, `MSGDELAY` should be observed for any proposal message broadcast by correct processes: it is a *worst-case* parameter. -As message delays depends on the message size, the above requirement implicty +As message delays depends on the message size, the above requirement implicitly indicates that the size of proposal messages is either fixed or upper bounded. ## Problem Statement @@ -143,30 +143,31 @@ The property is based in the `timely` predicate defined in the following: #### **[PBTS-INV-TIMELY.0]** - [Time-Validity] If a correct process decides on value `v`, then the proposal - message proposing `v` was considered `timely` by at least `f+1` processes. + of `v` was considered `timely` by at least `f+1` processes. The `timely` predicate is evaluated when a process receives a proposal in a round of consensus. + A proposal is a tuple `(v, v.time, v.round)`, where `v` is the proposed value, `v.time` the proposal time, and `v.round` is the round at which `v` was first -proposed (and `v.time` was assigned). +proposed---so `v.time` and `v.round` were assigned. While the same proposal can be proposed multiple time, in different rounds of -consensus, we are interested on the first time it was proposed: +consensus, the `timely` predicate is verfied in the first time it was proposed: -##### **[PBTS-RECEPTION-STEP.0]** +#### **[PBTS-PROPOSAL-RECEPTION.0]** Let `p` be a correct process which is at round `r` of consensus: - `receiveTime_p[r]` is the time `p` reads from its local clock when it receives the proposal `(v, v.time, v.round)` with `v.round = r`. -##### **[PBTS-TIMELY.0]** +#### **[PBTS-TIMELY.0]** The proposal `(v, v.time, v.round)` for `v` is considered `timely` by a correct process `p` if: 1. `receiveTime_p[v.round] >= v.time - PRECISION` and -1. `receiveTime_p[v.round] <= v.time + MSGDELAY + PRECISION` +1. `receiveTime_p[v.round] <= v.time + MSGDELAY + PRECISION`. ### Timely Proof-of-Locks From abae01085af08769a3a1f960fc0e3d0c8510bfdf Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Tue, 15 Mar 2022 16:24:53 +0100 Subject: [PATCH 17/26] PBTS model: timely predicate definition --- .../pbts-sysmodel_002_draft.md | 60 +++++++++++-------- 1 file changed, 34 insertions(+), 26 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index c09218590..c77d52bdc 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -6,8 +6,7 @@ - [Synchronized clocks](#synchronized-clocks) - [Message delays](#message-delays) - [Problem Statement](#problem-statement) - - [Safety Invariants](#safety-invariants) - - [Timely Proposals](#timely-proposals) + - [Timely Proposals](#timely-proposals) ## System Model @@ -100,14 +99,12 @@ indicates that the size of proposal messages is either fixed or upper bounded. In this section we define the properties of Tendermint consensus (cf. the [arXiv paper][arXiv]) in this system model. -#### **[PBTS-PROPOSE.0]** +### **[PBTS-PROPOSE.0]** A proposer proposes a consensus value `v` that includes a proposal time `v.time`. -### Safety Invariants - -We then restrict the allowed decisions along the following lines: +> We then restrict the allowed decisions along the following lines: #### **[PBTS-INV-AGREEMENT.0]** @@ -134,39 +131,50 @@ consensus: The monotonicity of proposal times, and external validity in general, implicitly assumes that heights of consensus are executed in order. -### Timely proposals - -PBTS introduces a synchronous property that restrict the allowed decisions -based on the proposal time `v.time` associated with a proposed value `v`. -The property is based in the `timely` predicate defined in the following: - #### **[PBTS-INV-TIMELY.0]** - [Time-Validity] If a correct process decides on value `v`, then the proposal - of `v` was considered `timely` by at least `f+1` processes. + time `v.time` was considered `timely` by `f+1` correct processes. -The `timely` predicate is evaluated when a process receives a proposal in a -round of consensus. +PBTS introduces a `timely` predicate that restricts the allowed decisions based +on the proposal time `v.time` associated with a proposed value `v`. +As as synchronous predicate, the time at which it is evaluated impacts on +whether a process accepts of reject a value based on its proposal time. +For this reason, the Time-Validity property refers to the previous evaluation +of the `timely` predicate, as detailed in the following. -A proposal is a tuple `(v, v.time, v.round)`, where `v` is the proposed value, -`v.time` the proposal time, and `v.round` is the round at which `v` was first -proposed---so `v.time` and `v.round` were assigned. -While the same proposal can be proposed multiple time, in different rounds of -consensus, the `timely` predicate is verfied in the first time it was proposed: +## Timely proposals -#### **[PBTS-PROPOSAL-RECEPTION.0]** +For PBTS, a `proposal` is a tuple `(v, v.time, v.round)`, where: + +- `v` is the proposed value; +- `v.time` is the associated proposal time; +- `v.round` is the round at which `v` was first proposed. -Let `p` be a correct process which is at round `r` of consensus: +We introduce this definition of proposal because, while a value `v` and its +associated proposal time `v.time` can be proposed in multiple rounds, the +`timely` predicate is only evaluated at round `v.round`. + +> Considering the algorithm in the [arXiv paper][arXiv], a new proposal is +> produced by a proposer `p` when its `validValue_p` is unset. +> The produced proposal thus have `v.round = round_p` and it is broadcast in a +> Proposal message of round `v.round` with the `validRound` field set to `-1`. + +The `timely` predicate is evaluated when a process receives a proposal. +More precisely, let `p` be a correct process: + +#### **[PBTS-PROPOSAL-RECEPTION.0]** - `receiveTime_p[r]` is the time `p` reads from its local clock when it - receives the proposal `(v, v.time, v.round)` with `v.round = r`. + receives the proposal `(v, v.time, v.round)`. #### **[PBTS-TIMELY.0]** -The proposal `(v, v.time, v.round)` for `v` is considered `timely` by a correct -process `p` if: +The proposal `(v, v.time, v.round)` is considered `timely` by a correct process +`p` if: -1. `receiveTime_p[v.round] >= v.time - PRECISION` and +1. `receiveTime_p[v.round]` is set, and +1. `receiveTime_p[v.round] >= v.time - PRECISION`, and 1. `receiveTime_p[v.round] <= v.time + MSGDELAY + PRECISION`. ### Timely Proof-of-Locks From a94be39c03bb413fc87605d51d7a3bb0bdcfa6c8 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Tue, 15 Mar 2022 17:03:49 +0100 Subject: [PATCH 18/26] PBTS model: timely proof-of-lock re-defined --- .../pbts-sysmodel_002_draft.md | 39 +++++++++++-------- 1 file changed, 22 insertions(+), 17 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index c77d52bdc..21cde2c58 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -134,7 +134,7 @@ implicitly assumes that heights of consensus are executed in order. #### **[PBTS-INV-TIMELY.0]** - [Time-Validity] If a correct process decides on value `v`, then the proposal - time `v.time` was considered `timely` by `f+1` correct processes. + time `v.time` was considered `timely` by at least `f+1` correct processes. PBTS introduces a `timely` predicate that restricts the allowed decisions based on the proposal time `v.time` associated with a proposed value `v`. @@ -158,7 +158,7 @@ associated proposal time `v.time` can be proposed in multiple rounds, the > Considering the algorithm in the [arXiv paper][arXiv], a new proposal is > produced by a proposer `p` when its `validValue_p` is unset. > The produced proposal thus have `v.round = round_p` and it is broadcast in a -> Proposal message of round `v.round` with the `validRound` field set to `-1`. +> Proposal message of with the `validRound` field set to `-1`. The `timely` predicate is evaluated when a process receives a proposal. More precisely, let `p` be a correct process: @@ -177,31 +177,36 @@ The proposal `(v, v.time, v.round)` is considered `timely` by a correct process 1. `receiveTime_p[v.round] >= v.time - PRECISION`, and 1. `receiveTime_p[v.round] <= v.time + MSGDELAY + PRECISION`. +A correct process at round `v.round` of consensus only sends a `PREVOTE` for +`v` if the associated proposal time `v.time` is considered `timely`. + ### Timely Proof-of-Locks -We denote by `POL(v,r)` a *Proof-of-Lock* of value `v` at the round `r` of consensus. -`POL(v,r)` consists of a set of `PREVOTE` messages of round `r` for the value `v` -from processes whose cumulative voting power is at least `2f + 1`. +A *Proof-of-Lock* is a set of `PREVOTE` messages of round of consensus for the +same value from processes whose cumulative voting power is at least `2f + 1`. +We denote as `POL(v,r)` a proof-of-lock of value `v` at round `r`. + +For PBTS, we are particularly interested in the `POL(v,v.round)` produced in +the round `v.round` at which a value `v` was first proposed. +We call it a *timely* proof-of-lock for `v` because it can only be observed +if processes with cumulative voting power `f+1` considered it `timely`. +More precisely: -#### **[PBTS-TIMELY-POL.1]** +#### **[PBTS-TIMELY-POL.0]** If -- there is a valid `POL(v,r*)` for height `h`, and -- `r*` is the lowest-numbered round `r` of height `h` for which there is a valid `POL(v,r)`, and +- there is a valid `POL(v,r*)` with `r* = v.round`, and - `POL(v,r*)` contains a `PREVOTE` message from at least one correct process, -Then, where `p` is a such correct process: +Then, let `p` is a such correct process: -- `p` received a `PROPOSE` message of round `r*` and height `h`, and -- the `PROPOSE` message contained a proposal for value `v` with proposal time `v.time`, and -- a correct process `p` considered the proposal `timely`. +- `p` received a `PROPOSE` message of round `r* = v.round`, and +- the `PROPOSE` message contained a proposal `(v, v.time, v.round)`, and +- `p` considered the proposal `timely`. -The round `r*` above defined will be, in most cases, -the round in which `v` was originally proposed, and when `v.time` was assigned, -using a `PROPOSE` message with `POLRound = -1`. -In any case, at least one correct process must consider the proposal `timely` at round `r*` -to enable a valid `POL(v,r*)` to be observed. +The presence of a `PREVOTE` from a correct process `p` in a timely proof-of-lock is +guaranteed provided that the voting power of Byzantine processes is bound by `2f `. ### Derived Proof-of-Locks From 3d7014e0f5c107c5d93b5f3e07650ca9aef403f9 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Tue, 15 Mar 2022 18:30:52 +0100 Subject: [PATCH 19/26] PBTS model: derived proof-of-lock requirements * The property needs to be properly demonstrated. --- .../pbts-sysmodel_002_draft.md | 81 +++++++++---------- 1 file changed, 39 insertions(+), 42 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 21cde2c58..7afc9bb1f 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -134,14 +134,14 @@ implicitly assumes that heights of consensus are executed in order. #### **[PBTS-INV-TIMELY.0]** - [Time-Validity] If a correct process decides on value `v`, then the proposal - time `v.time` was considered `timely` by at least `f+1` correct processes. + time `v.time` was considered `timely` by at least one correct process. PBTS introduces a `timely` predicate that restricts the allowed decisions based on the proposal time `v.time` associated with a proposed value `v`. As as synchronous predicate, the time at which it is evaluated impacts on whether a process accepts of reject a value based on its proposal time. For this reason, the Time-Validity property refers to the previous evaluation -of the `timely` predicate, as detailed in the following. +of the `timely` predicate, detailed in the following. ## Timely proposals @@ -151,22 +151,24 @@ For PBTS, a `proposal` is a tuple `(v, v.time, v.round)`, where: - `v.time` is the associated proposal time; - `v.round` is the round at which `v` was first proposed. -We introduce this definition of proposal because, while a value `v` and its -associated proposal time `v.time` can be proposed in multiple rounds, the -`timely` predicate is only evaluated at round `v.round`. +We introduce this definition of proposal because a value `v` and its +associated proposal time `v.time` can be proposed in multiple rounds, but the +evaluation of the `timely` predicate is only relevant at round `v.round`. > Considering the algorithm in the [arXiv paper][arXiv], a new proposal is > produced by a proposer `p` when its `validValue_p` is unset. > The produced proposal thus have `v.round = round_p` and it is broadcast in a > Proposal message of with the `validRound` field set to `-1`. +#### **[PBTS-PROPOSAL-RECEPTION.0]** + The `timely` predicate is evaluated when a process receives a proposal. More precisely, let `p` be a correct process: -#### **[PBTS-PROPOSAL-RECEPTION.0]** - - `receiveTime_p[r]` is the time `p` reads from its local clock when it - receives the proposal `(v, v.time, v.round)`. + receives the proposal of round `r`. + +Note that process must be in round `r` to receive a proposal of round `r`. #### **[PBTS-TIMELY.0]** @@ -177,8 +179,8 @@ The proposal `(v, v.time, v.round)` is considered `timely` by a correct process 1. `receiveTime_p[v.round] >= v.time - PRECISION`, and 1. `receiveTime_p[v.round] <= v.time + MSGDELAY + PRECISION`. -A correct process at round `v.round` of consensus only sends a `PREVOTE` for -`v` if the associated proposal time `v.time` is considered `timely`. +A correct process at round `v.round` only sends a `PREVOTE` for `v` if the +associated proposal time `v.time` is considered `timely`. ### Timely Proof-of-Locks @@ -189,58 +191,53 @@ We denote as `POL(v,r)` a proof-of-lock of value `v` at round `r`. For PBTS, we are particularly interested in the `POL(v,v.round)` produced in the round `v.round` at which a value `v` was first proposed. We call it a *timely* proof-of-lock for `v` because it can only be observed -if processes with cumulative voting power `f+1` considered it `timely`. -More precisely: +if at least one correct process considered it `timely`: #### **[PBTS-TIMELY-POL.0]** If -- there is a valid `POL(v,r*)` with `r* = v.round`, and -- `POL(v,r*)` contains a `PREVOTE` message from at least one correct process, +- there is a valid `POL(v,r)` with `r = v.round`, and +- `POL(v,v.round)` contains a `PREVOTE` message from at least one correct process, Then, let `p` is a such correct process: -- `p` received a `PROPOSE` message of round `r* = v.round`, and +- `p` received a `PROPOSE` message of round `v.round`, and - the `PROPOSE` message contained a proposal `(v, v.time, v.round)`, and -- `p` considered the proposal `timely`. +- `p` considered the proposal time `v.time` `timely`. -The presence of a `PREVOTE` from a correct process `p` in a timely proof-of-lock is -guaranteed provided that the voting power of Byzantine processes is bound by `2f `. +The existence of a such correct process `p` is guaranteed provided that the +voting power of Byzantine processes is bounded by `2f`. ### Derived Proof-of-Locks -#### **[PBTS-DERIVED-POL.1]** +The existence of `POL(v,r)` is a requirement for the decision of `v` at round +`r` of consensus. + +At the same time, the Time-Validity property established that if `v` is decided +then a timely proof-of-lock `POL(v,v.round)` must have been produced. + +So, we need to demonstrate here that any valid `POL(v,r)` is either a timely +proof-of-lock or it is derived from a timely proof-of-lock: + +#### **[PBTS-DERIVED-POL.0]** If -- there is a valid `POL(v,r)` for height `h`, and +- there is a valid `POL(v,r)`, and - `POL(v,r)` contains a `PREVOTE` message from at least one correct process, Then -- there is a valid `POL(v,r*)` for height `h`, with `r* <= r`, and -- `POL(v,r*)` contains a `PREVOTE` message from at least one correct process, and -- a correct process considered the proposal for `v` `timely` at round `r*`. - -The above relation derives from a recursion on the round number `r`. -It is trivially observed when `r = r*`, the base of the recursion, -when a timely `POL(v,r*)` is obtained. -We need to ensure that, once a timely `POL(v,r*)` is obtained, -it is possible to obtain a valid `POL(v,r)` with `r > r*`, -without the need of satisfying the `timely` predicate (again) in round `r`. -In fact, since rounds are started in order, it is not likely that -a proposal time `v.time`, assigned at round `r*`, -will still be considered `timely` when the round `r > r*` is in progress. - -In other words, the algorithm should ensure that once a `POL(v,r*)` attests -that the proposal for `v` is `timely`, -further valid `POL(v,r)` with `r > r*` can be obtained, -even though processes do not consider the proposal for `v` `timely` any longer. - -> This can be achieved if the proposer of round `r' > r*` proposes `v` in a `PROPOSE` message -with `POLRound = r*`, and at least one correct processes is aware of a `POL(v,r*)`. -> From this point, if a valid `POL(v,r')` is achieved, it can replace the adopted `POL(v,r*)`. +- there is a valid `POL(v,v.round)` with `v.round <= r`, +- so a correct process considered the proposal for `v` `timely` at round `v.round`. + +The above relation is trivially observed when `r = v.round`, as `POL(v,r)` must +be a timely proof-of-lock. +(Notice that, by the definition of `v.round`, we cannot have `r < v.round`). + +For `r > v.round` we need to demonstrate that if there is a valid `POL(v,r)`, +then a timely `POL(v,v.round)` was previously obtained. ### SAFETY From a742dc3e8a6aedc2e3ead99c001d77974f35c782 Mon Sep 17 00:00:00 2001 From: Daniel Date: Mon, 21 Mar 2022 09:18:44 +0100 Subject: [PATCH 20/26] Apply suggestions from William Co-authored-by: William Banfield <4561443+williambanfield@users.noreply.github.com> --- .../proposer-based-timestamp/pbts-sysmodel_002_draft.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 7afc9bb1f..a1e47ed8f 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -138,10 +138,10 @@ implicitly assumes that heights of consensus are executed in order. PBTS introduces a `timely` predicate that restricts the allowed decisions based on the proposal time `v.time` associated with a proposed value `v`. -As as synchronous predicate, the time at which it is evaluated impacts on +As a synchronous predicate, the time at which it is evaluated impacts on whether a process accepts of reject a value based on its proposal time. For this reason, the Time-Validity property refers to the previous evaluation -of the `timely` predicate, detailed in the following. +of the `timely` predicate, detailed in the following section. ## Timely proposals From 79b4fde8c03e41bbaf9d033cd8601cedbfb24ee8 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 21 Mar 2022 10:42:04 +0100 Subject: [PATCH 21/26] PBTS model: reference to arXiv algorithm on timely --- .../pbts-sysmodel_002_draft.md | 28 +++++++++++-------- 1 file changed, 17 insertions(+), 11 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index a1e47ed8f..1ba25ebaf 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -139,7 +139,7 @@ implicitly assumes that heights of consensus are executed in order. PBTS introduces a `timely` predicate that restricts the allowed decisions based on the proposal time `v.time` associated with a proposed value `v`. As a synchronous predicate, the time at which it is evaluated impacts on -whether a process accepts of reject a value based on its proposal time. +whether a process accepts or reject a proposal time. For this reason, the Time-Validity property refers to the previous evaluation of the `timely` predicate, detailed in the following section. @@ -151,14 +151,18 @@ For PBTS, a `proposal` is a tuple `(v, v.time, v.round)`, where: - `v.time` is the associated proposal time; - `v.round` is the round at which `v` was first proposed. -We introduce this definition of proposal because a value `v` and its -associated proposal time `v.time` can be proposed in multiple rounds, but the -evaluation of the `timely` predicate is only relevant at round `v.round`. - > Considering the algorithm in the [arXiv paper][arXiv], a new proposal is -> produced by a proposer `p` when its `validValue_p` is unset. -> The produced proposal thus have `v.round = round_p` and it is broadcast in a -> Proposal message of with the `validRound` field set to `-1`. +> produced by the `getValue()` method, invoked by the proposer `p` of round +> `round_p` when its `validValue_p` is unset. +> +> The first round at which a value `v` is proposed is then the round `round_p` +> at which the proposer `p` broadcast a `PROPOSAL` message for `v` with +> `validRound_p == -1`. + +We include the proposal round `v.round` in the proposal defintion becase a +value `v` and its associated proposal time `v.time` can be proposed in multiple +rounds, but the evaluation of the `timely` predicate is only relevant at round +`v.round`. #### **[PBTS-PROPOSAL-RECEPTION.0]** @@ -166,9 +170,7 @@ The `timely` predicate is evaluated when a process receives a proposal. More precisely, let `p` be a correct process: - `receiveTime_p[r]` is the time `p` reads from its local clock when it - receives the proposal of round `r`. - -Note that process must be in round `r` to receive a proposal of round `r`. + `p` is at round `r` and receives the proposal of round `r`. #### **[PBTS-TIMELY.0]** @@ -179,6 +181,10 @@ The proposal `(v, v.time, v.round)` is considered `timely` by a correct process 1. `receiveTime_p[v.round] >= v.time - PRECISION`, and 1. `receiveTime_p[v.round] <= v.time + MSGDELAY + PRECISION`. +> Considering the algorithm in the [arXiv paper][arXiv], the `timely` predicate +> is evaluated by a process `p` when it receives a `PROPOSAL` message of its +> current round `round_p` with `validRound == -1`. + A correct process at round `v.round` only sends a `PREVOTE` for `v` if the associated proposal time `v.time` is considered `timely`. From 21051f255a0345a604cf44106dc969b73601e6b6 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 21 Mar 2022 10:49:53 +0100 Subject: [PATCH 22/26] PBTS model: typos fixed --- .../pbts-sysmodel_002_draft.md | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index 1ba25ebaf..c1f324e04 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -151,26 +151,26 @@ For PBTS, a `proposal` is a tuple `(v, v.time, v.round)`, where: - `v.time` is the associated proposal time; - `v.round` is the round at which `v` was first proposed. +We include the proposal round `v.round` in the proposal definition because a +value `v` and its associated proposal time `v.time` can be proposed in multiple +rounds, but the evaluation of the `timely` predicate is only relevant at round +`v.round`. + > Considering the algorithm in the [arXiv paper][arXiv], a new proposal is > produced by the `getValue()` method, invoked by the proposer `p` of round -> `round_p` when its `validValue_p` is unset. +> `round_p` when starting its proposing round with a nil `validValue_p`. > -> The first round at which a value `v` is proposed is then the round `round_p` -> at which the proposer `p` broadcast a `PROPOSAL` message for `v` with +> The first round at which a value `v` is proposed is then the round at which +> the proposal for `v` was produced, and broadcast in a `PROPOSAL` message with > `validRound_p == -1`. -We include the proposal round `v.round` in the proposal defintion becase a -value `v` and its associated proposal time `v.time` can be proposed in multiple -rounds, but the evaluation of the `timely` predicate is only relevant at round -`v.round`. - #### **[PBTS-PROPOSAL-RECEPTION.0]** The `timely` predicate is evaluated when a process receives a proposal. More precisely, let `p` be a correct process: -- `receiveTime_p[r]` is the time `p` reads from its local clock when it - `p` is at round `r` and receives the proposal of round `r`. +- `receiveTime_p[r]` is the time `p` reads from its local clock when `p` is at + round `r` and receives the proposal of round `r`. #### **[PBTS-TIMELY.0]** @@ -181,13 +181,13 @@ The proposal `(v, v.time, v.round)` is considered `timely` by a correct process 1. `receiveTime_p[v.round] >= v.time - PRECISION`, and 1. `receiveTime_p[v.round] <= v.time + MSGDELAY + PRECISION`. -> Considering the algorithm in the [arXiv paper][arXiv], the `timely` predicate -> is evaluated by a process `p` when it receives a `PROPOSAL` message of its -> current round `round_p` with `validRound == -1`. - A correct process at round `v.round` only sends a `PREVOTE` for `v` if the associated proposal time `v.time` is considered `timely`. +> Considering the algorithm in the [arXiv paper][arXiv], the `timely` predicate +> is evaluated by a process `p` when it receives a valid `PROPOSAL` message +> from the proposed of the current round `round_p` with `validRound == -1`. + ### Timely Proof-of-Locks A *Proof-of-Lock* is a set of `PREVOTE` messages of round of consensus for the From f7b8788cf6aa71b42dbee50ff5662e51888771aa Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 21 Mar 2022 12:15:11 +0100 Subject: [PATCH 23/26] PBTS model: derived POL "demonstration" --- .../pbts-sysmodel_002_draft.md | 34 +++++++++++++++---- 1 file changed, 27 insertions(+), 7 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index c1f324e04..a53628643 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -208,9 +208,9 @@ If Then, let `p` is a such correct process: -- `p` received a `PROPOSE` message of round `v.round`, and -- the `PROPOSE` message contained a proposal `(v, v.time, v.round)`, and -- `p` considered the proposal time `v.time` `timely`. +- `p` received a `PROPOSAL` message of round `v.round`, and +- the `PROPOSAL` message contained a proposal `(v, v.time, v.round)`, and +- `p` was in round `v.round` and evaluated the proposal time `v.time` as `timely`. The existence of a such correct process `p` is guaranteed provided that the voting power of Byzantine processes is bounded by `2f`. @@ -220,7 +220,7 @@ voting power of Byzantine processes is bounded by `2f`. The existence of `POL(v,r)` is a requirement for the decision of `v` at round `r` of consensus. -At the same time, the Time-Validity property established that if `v` is decided +At the same time, the Time-Validity property establishes that if `v` is decided then a timely proof-of-lock `POL(v,v.round)` must have been produced. So, we need to demonstrate here that any valid `POL(v,r)` is either a timely @@ -235,15 +235,35 @@ If Then -- there is a valid `POL(v,v.round)` with `v.round <= r`, -- so a correct process considered the proposal for `v` `timely` at round `v.round`. +- there is a valid `POL(v,v.round)` with `v.round <= r` which is a timely proof-of-lock. The above relation is trivially observed when `r = v.round`, as `POL(v,r)` must be a timely proof-of-lock. -(Notice that, by the definition of `v.round`, we cannot have `r < v.round`). +Notice that we cannot have `r < v.round`, as `v.round` is defined as the first +round at which `v` was proposed. For `r > v.round` we need to demonstrate that if there is a valid `POL(v,r)`, then a timely `POL(v,v.round)` was previously obtained. +We observe that a condition for observing a `POL(v,r)` is the proposer of round +`r` having broadcast a `PROPOSAL` message for `v`. +As `r > v.round`, we can affirm that `v` was not produced in round `r`. +So `v` was, by the protocol operation, the highest *valid value* known by the +proposer when it started the round. +A value `v` becomes a valid value when there is `POL(v,r')` with `r' < r'`. +Even though the proposer `p` can be incorrect, the fact of a `POL(v,r)` was +produced ensures that at least one correct process also observed a `POL(v,r')`. + +> Considering the algorithm in the [arXiv paper][arXiv], `v` was proposed by +> the proposer `p` of round `r == round_p` because it has `validValue_p == v`. +> The `PROPOSAL` message of round `r` proposing `v`, in this case, has its +> `validRound` field set to `r' == validRound_p >= v.round`. + +So, if there is a `POL(v,r)` with `r > v.round`, then there is a valid +`POL(v,r')` with `v.round <= r' < r'. +From this point, the reasoning becomes recursive: either `r' == v.round` and +`POL(v,r')` is a timely proof-of-lock, or there is another `POL(v,r'')` with +`r'' < r'`, recursively leading to the first scenario (as `r` necessarily +decreases at each recursive iteration). ### SAFETY From 9a6de9719a908ad5ca5447ee4bab4106c48e5242 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 21 Mar 2022 12:25:43 +0100 Subject: [PATCH 24/26] PBTS model: fix formatting, r' renamed to vr --- .../pbts-sysmodel_002_draft.md | 24 ++++++++++--------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index a53628643..bf22e5ae6 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -162,7 +162,7 @@ rounds, but the evaluation of the `timely` predicate is only relevant at round > > The first round at which a value `v` is proposed is then the round at which > the proposal for `v` was produced, and broadcast in a `PROPOSAL` message with -> `validRound_p == -1`. +> `vr = -1`. #### **[PBTS-PROPOSAL-RECEPTION.0]** @@ -186,7 +186,7 @@ associated proposal time `v.time` is considered `timely`. > Considering the algorithm in the [arXiv paper][arXiv], the `timely` predicate > is evaluated by a process `p` when it receives a valid `PROPOSAL` message -> from the proposed of the current round `round_p` with `validRound == -1`. +> from the proposer of the current round `round_p` with `vr = -1`. ### Timely Proof-of-Locks @@ -249,20 +249,22 @@ We observe that a condition for observing a `POL(v,r)` is the proposer of round As `r > v.round`, we can affirm that `v` was not produced in round `r`. So `v` was, by the protocol operation, the highest *valid value* known by the proposer when it started the round. -A value `v` becomes a valid value when there is `POL(v,r')` with `r' < r'`. +A value `v` becomes a valid value when there is `POL(v,vr)` with `vr < r'`. Even though the proposer `p` can be incorrect, the fact of a `POL(v,r)` was -produced ensures that at least one correct process also observed a `POL(v,r')`. +produced ensures that at least one correct process also observed a `POL(v,vr)`. > Considering the algorithm in the [arXiv paper][arXiv], `v` was proposed by -> the proposer `p` of round `r == round_p` because it has `validValue_p == v`. -> The `PROPOSAL` message of round `r` proposing `v`, in this case, has its -> `validRound` field set to `r' == validRound_p >= v.round`. +> the proposer `p` of round `round_p` because its `validValue_p` variable was +> set to `v`. +> +> The broadcast `PROPOSAL` message, in this case, has its `vr > -1`, which can +> only be accepted by processes that observed a `POL(v, vr)`. So, if there is a `POL(v,r)` with `r > v.round`, then there is a valid -`POL(v,r')` with `v.round <= r' < r'. -From this point, the reasoning becomes recursive: either `r' == v.round` and -`POL(v,r')` is a timely proof-of-lock, or there is another `POL(v,r'')` with -`r'' < r'`, recursively leading to the first scenario (as `r` necessarily +`POL(v,vr)` with `v.round <= vr < r`. +From this point, the reasoning becomes recursive: either `vr == v.round` and +`POL(v,vr)` is a timely proof-of-lock, or there is another `POL(v,vr')` with +`vr' < vr`, recursively leading to the first scenario (as `vr` necessarily decreases at each recursive iteration). ### SAFETY From a9637f6a7597e7adf4e6ff7ecc7699db80db18e1 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 21 Mar 2022 12:30:16 +0100 Subject: [PATCH 25/26] PBTS model: minor fixes --- .../proposer-based-timestamp/pbts-sysmodel_002_draft.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index bf22e5ae6..f3e593d52 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -159,7 +159,6 @@ rounds, but the evaluation of the `timely` predicate is only relevant at round > Considering the algorithm in the [arXiv paper][arXiv], a new proposal is > produced by the `getValue()` method, invoked by the proposer `p` of round > `round_p` when starting its proposing round with a nil `validValue_p`. -> > The first round at which a value `v` is proposed is then the round at which > the proposal for `v` was produced, and broadcast in a `PROPOSAL` message with > `vr = -1`. @@ -256,13 +255,12 @@ produced ensures that at least one correct process also observed a `POL(v,vr)`. > Considering the algorithm in the [arXiv paper][arXiv], `v` was proposed by > the proposer `p` of round `round_p` because its `validValue_p` variable was > set to `v`. -> > The broadcast `PROPOSAL` message, in this case, has its `vr > -1`, which can > only be accepted by processes that observed a `POL(v, vr)`. So, if there is a `POL(v,r)` with `r > v.round`, then there is a valid `POL(v,vr)` with `v.round <= vr < r`. -From this point, the reasoning becomes recursive: either `vr == v.round` and +From this point, the reasoning becomes recursive: either `vr = v.round` and `POL(v,vr)` is a timely proof-of-lock, or there is another `POL(v,vr')` with `vr' < vr`, recursively leading to the first scenario (as `vr` necessarily decreases at each recursive iteration). From 0bf5e6baa6d82cf7e3dd1dee4f50d98da83f3d75 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 21 Mar 2022 20:00:11 +0100 Subject: [PATCH 26/26] PBTS model: derived POL proof ammended --- .../pbts-sysmodel_002_draft.md | 34 +++++++++++-------- 1 file changed, 20 insertions(+), 14 deletions(-) diff --git a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md index f3e593d52..67f28439d 100644 --- a/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md +++ b/spec/consensus/proposer-based-timestamp/pbts-sysmodel_002_draft.md @@ -7,6 +7,10 @@ - [Message delays](#message-delays) - [Problem Statement](#problem-statement) - [Timely Proposals](#timely-proposals) + - [Timely Proof-of-Locks](#timely-proof-of-locks) + - [Derived Proof-of-Locks](#derived-proof-of-locks) + - [Safety](#safety) + - [Liveness](#liveness) ## System Model @@ -243,27 +247,29 @@ round at which `v` was proposed. For `r > v.round` we need to demonstrate that if there is a valid `POL(v,r)`, then a timely `POL(v,v.round)` was previously obtained. -We observe that a condition for observing a `POL(v,r)` is the proposer of round -`r` having broadcast a `PROPOSAL` message for `v`. +We observe that a condition for observing a `POL(v,r)` is that the proposer of +round `r` has broadcast a `PROPOSAL` message for `v`. As `r > v.round`, we can affirm that `v` was not produced in round `r`. -So `v` was, by the protocol operation, the highest *valid value* known by the -proposer when it started the round. -A value `v` becomes a valid value when there is `POL(v,vr)` with `vr < r'`. -Even though the proposer `p` can be incorrect, the fact of a `POL(v,r)` was -produced ensures that at least one correct process also observed a `POL(v,vr)`. +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`. +The above operation considers a *correct* proposer, but since a `POL(v,r)` was +produced (by hypothesis) we can affirm that at least one correct process (also) +observed a `POL(v,vr)`. > Considering the algorithm in the [arXiv paper][arXiv], `v` was proposed by > the proposer `p` of round `round_p` because its `validValue_p` variable was > set to `v`. -> The broadcast `PROPOSAL` message, in this case, has its `vr > -1`, which can -> only be accepted by processes that observed a `POL(v, vr)`. +> The `PROPOSAL` message broadcast by the proposer, in this case, had `vr > -1`, +> and it could only be accepted by processes that also observed a `POL(v,vr)`. -So, if there is a `POL(v,r)` with `r > v.round`, then there is a valid +Thus, if there is a `POL(v,r)` with `r > v.round`, then there is a valid `POL(v,vr)` with `v.round <= vr < r`. -From this point, the reasoning becomes recursive: either `vr = v.round` and -`POL(v,vr)` is a timely proof-of-lock, or there is another `POL(v,vr')` with -`vr' < vr`, recursively leading to the first scenario (as `vr` necessarily -decreases at each recursive iteration). +If `vr = v.round` then `POL(vr,v)` is a timely proof-of-lock and we are done. +Otherwise, there is another valid `POL(v,vr')` with `v.round <= vr' < vr`, +and the same reasoning can be applied until we get `vr' = v.round` and observe +a timely proof-of-lock (which is guaranteed, as `vr` necessarily decreases at +each recursive iteration). ### SAFETY