From 9a6de9719a908ad5ca5447ee4bab4106c48e5242 Mon Sep 17 00:00:00 2001 From: Daniel Cason Date: Mon, 21 Mar 2022 12:25:43 +0100 Subject: [PATCH] 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