ABCI++ markdown integration into Tendermint (for spec) (#327)

spec/abci++/v0.md

@@ -0,0 +1,156 @@
+# Tendermint v0 Markdown pseudocode
+
+This translates the latex code for Tendermint consensus from the Tendermint paper into markdown.
+
+### Initialization
+
+```go
+h_p ← 0
+round_p ← 0
+step_p is one of {propose, prevote, precommit}
+decision_p ← Vector()
+lockedRound_p ← -1
+lockedValue_p ← nil
+validValue_p ← nil
+validRound_p ← -1
+```
+
+### StartRound(round)
+
+```go
+function startRound(round) {
+    round_p ← round
+    step_p ← propose
+    if proposer(h_p, round_p) = p {
+        if validValue_p != nil {
+            proposal ← validValue_p
+        } else {
+            proposal ← getValue()
+        }
+        broadcast ⟨PROPOSAL, h_p, round_p, proposal, validRound_p⟩
+    } else {
+        schedule OnTimeoutPropose(h_p,round_p) to be executed after timeoutPropose(round_p)
+    }
+}
+```
+
+### ReceiveProposal
+
+In the case where the local node is not locked on any round, the following is ran:
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, −1) from proposer(h_p, round_p) while step_p = propose do {
+    if valid(v) ∧ (lockedRound_p = −1 ∨ lockedValue_p = v) {
+        broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩ 
+    } else {
+        broadcast ⟨PREVOTE, h_p, round_p, nil⟩ 
+    }
+    step_p ← prevote
+}
+```
+
+In the case where the node is locked on a round, the following is ran:
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, vr⟩ from proposer(h_p, round_p)
+  AND 2f + 1 ⟨PREVOTE, h_p, vr, id(v)⟩
+  while step_p = propose ∧ (vr ≥ 0 ∧ vr < round_p) do {
+    if valid(v) ∧ (lockedRound_p ≤ vr ∨ lockedValue_p = v) {
+        broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩
+    } else {
+        broadcast ⟨PREVOTE, h_p, round_p, nil⟩
+    }
+    step_p ← prevote
+}
+```
+
+### Prevote timeout
+
+Upon receiving 2f + 1 prevotes, setup a timeout.
+
+```go
+upon 2f + 1 ⟨PREVOTE, h_p, vr, *⟩ with step_p = prevote for the first time, do {
+    schedule OnTimeoutPrevote(h_p, round_p) to be executed after timeoutPrevote(round_p)
+}
+```
+
+with OnTimeoutPrevote defined as:
+
+```go
+function OnTimeoutPrevote(height, round) {
+    if (height = h_p && round = round_p && step_p = prevote) {
+        broadcast ⟨PRECOMMIT, h_p, round_p, nil⟩
+        step_p ← precommit
+    }
+}
+```
+
+### Receiving enough prevotes to precommit
+
+The following code is ran upon receiving 2f + 1 prevotes for the same block
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, *⟩
+  from proposer(h_p, round_p)
+  AND 2f + 1 ⟨PREVOTE, h_p, round_p, id(v)⟩ 
+  while valid(v) ∧ step_p >= prevote for the first time do {
+    if (step_p = prevote) {
+        lockedValue_p ← v
+        lockedRound_p ← round_p
+        broadcast ⟨PRECOMMIT, h_p, round_p, id(v)⟩
+        step_p ← precommit
+    }
+    validValue_p ← v
+    validRound_p ← round_p
+}
+```
+
+And upon receiving 2f + 1 prevotes for nil:
+
+```go
+upon 2f + 1 ⟨PREVOTE, h_p, round_p, nil⟩ 
+  while step_p = prevote do {
+    broadcast ⟨PRECOMMIT, h_p, round_p, nil⟩
+    step_p ← precommit
+}
+```
+
+### Precommit timeout
+
+Upon receiving 2f + 1 precommits, setup a timeout.
+
+```go
+upon 2f + 1 ⟨PRECOMMIT, h_p, vr, *⟩ for the first time, do {
+    schedule OnTimeoutPrecommit(h_p, round_p) to be executed after timeoutPrecommit(round_p)
+}
+```
+
+with OnTimeoutPrecommit defined as:
+
+```go
+function OnTimeoutPrecommit(height, round) {
+    if (height = h_p && round = round_p) {
+        StartRound(round_p + 1)
+    }
+}
+```
+
+### Upon Receiving 2f + 1 precommits
+
+The following code is ran upon receiving 2f + 1 precommits for the same block
+
+```go
+upon ⟨PROPOSAL, h_p, r, v, *⟩
+  from proposer(h_p, r)
+  AND 2f + 1 ⟨ PRECOMMIT, h_p, r, id(v)⟩ 
+  while decision_p[h_p] = nil do {
+    if (valid(v)) {
+        decision_p[h_p] ← v
+        h_p ← h_p + 1
+        reset lockedRound_p, lockedValue_p,validRound_p and validValue_p to initial values
+        StartRound(0)
+    }
+}
+```
+
+If we don't see 2f + 1 precommits for the same block, we wait until we get 2f + 1 precommits, and the timeout occurs.

spec/abci++/v1.md

@@ -0,0 +1,162 @@
+# Tendermint v1 Markdown pseudocode
+
+This adds hooks for the existing ABCI to the prior pseudocode
+
+### Initialization
+
+```go
+h_p ← 0
+round_p ← 0
+step_p is one of {propose, prevote, precommit}
+decision_p ← Vector()
+lockedValue_p ← nil
+validValue_p ← nil
+validRound_p ← -1
+```
+
+### StartRound(round)
+
+```go
+function startRound(round) {
+    round_p ← round
+    step_p ← propose
+    if proposer(h_p, round_p) = p {
+        if validValue_p != nil {
+            proposal ← validValue_p
+        } else {
+            txdata ← mempool.GetBlock()
+            // getBlockProposal fills in header
+            proposal ← getBlockProposal(txdata)
+        }
+        broadcast ⟨PROPOSAL, h_p, round_p, proposal, validRound_p⟩
+    } else {
+        schedule OnTimeoutPropose(h_p,round_p) to be executed after timeoutPropose(round_p)
+    }
+}
+```
+
+### ReceiveProposal
+
+In the case where the local node is not locked on any round, the following is ran:
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, −1) from proposer(h_p, round_p) while step_p = propose do {
+    if valid(v) ∧ (lockedRound_p = −1 ∨ lockedValue_p = v) {
+      broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩ 
+    } else {
+      broadcast ⟨PREVOTE, h_p, round_p, nil⟩ 
+    }
+    step_p ← prevote
+}
+```
+
+In the case where the node is locked on a round, the following is ran:
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, vr⟩
+ from proposer(h_p, round_p)
+ AND 2f + 1 ⟨PREVOTE, h_p, vr, id(v)⟩ 
+  while step_p = propose ∧ (vr ≥ 0 ∧ vr < round_p) do {
+    if valid(v) ∧ (lockedRound_p ≤ vr ∨ lockedValue_p = v) {
+        broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩
+    } else {
+        broadcast ⟨PREVOTE, h_p, round_p, nil⟩
+    }
+    step_p ← prevote
+}
+```
+
+### Prevote timeout
+
+Upon receiving 2f + 1 prevotes, setup a timeout.
+
+```go
+upon 2f + 1 ⟨PREVOTE, h_p, vr, -1⟩ 
+  with step_p = prevote for the first time, do {
+    schedule OnTimeoutPrevote(h_p, round_p) to be executed after timeoutPrevote(round_p)
+}
+```
+
+with OnTimeoutPrevote defined as:
+
+```go
+function OnTimeoutPrevote(height, round) {
+    if (height = h_p && round = round_p && step_p = prevote) {
+        broadcast ⟨PRECOMMIT, h_p, round_p, nil⟩
+        step_p ← precommit
+    }
+}
+```
+
+### Receiving enough prevotes to precommit
+
+The following code is ran upon receiving 2f + 1 prevotes for the same block
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, *⟩
+ from proposer(h_p, round_p)
+ AND 2f + 1 ⟨PREVOTE, h_p, vr, id(v)⟩ 
+  while valid(v) ∧ step_p >= prevote for the first time do {
+    if (step_p = prevote) {
+        lockedValue_p ← v
+        lockedRound_p ← round_p
+        broadcast ⟨PRECOMMIT, h_p, round_p, id(v)⟩
+        step_p ← precommit
+    }
+    validValue_p ← v
+    validRound_p ← round_p
+}
+```
+
+And upon receiving 2f + 1 prevotes for nil:
+
+```go
+upon 2f + 1 ⟨PREVOTE, h_p, round_p, nil⟩ 
+  while step_p = prevote do {
+    broadcast ⟨PRECOMMIT, h_p, round_p, nil⟩
+    step_p ← precommit
+}
+```
+
+### Precommit timeout
+
+Upon receiving 2f + 1 precommits, setup a timeout.
+
+```go
+upon 2f + 1 ⟨PRECOMMIT, h_p, vr, *⟩ for the first time, do {
+    schedule OnTimeoutPrecommit(h_p, round_p) to be executed after timeoutPrecommit(round_p)
+}
+```
+
+with OnTimeoutPrecommit defined as:
+
+```go
+function OnTimeoutPrecommit(height, round) {
+    if (height = h_p && round = round_p) {
+        StartRound(round_p + 1)
+    }
+}
+```
+
+### Upon Receiving 2f + 1 precommits
+
+The following code is ran upon receiving 2f + 1 precommits for the same block
+
+```go
+upon ⟨PROPOSAL, h_p, r, v, *⟩
+  from proposer(h_p, r)
+  AND 2f + 1 ⟨ PRECOMMIT, h_p, r, id(v)⟩ 
+  while decision_p[h_p] = nil do {
+    if (valid(v)) {
+        decision_p[h_p] ← v
+        h_p ← h_p + 1
+        reset lockedRound_p, lockedValue_p,validRound_p and validValue_p to initial values
+        ABCI.BeginBlock(v.header)
+        ABCI.DeliverTxs(v.data)
+        ABCI.EndBlock()
+        StartRound(0)
+    }
+}
+```
+
+If we don't see 2f + 1 precommits for the same block, we wait until we get 2f + 1 precommits, and the timeout occurs.

spec/abci++/v2.md

@@ -0,0 +1,180 @@
+# Tendermint v2 Markdown pseudocode
+
+This adds a single-threaded implementation of ABCI++,
+with no optimization for splitting out verifying the header and verifying the proposal.
+
+### Initialization
+
+```go
+h_p ← 0
+round_p ← 0
+step_p is one of {propose, prevote, precommit}
+decision_p ← Vector()
+lockedValue_p ← nil
+validValue_p ← nil
+validRound_p ← -1
+```
+
+### StartRound(round)
+
+```go
+function startRound(round) {
+    round_p ← round
+    step_p ← propose
+    if proposer(h_p, round_p) = p {
+        if validValue_p != nil {
+            proposal ← validValue_p
+        } else {
+            txdata ← mempool.GetBlock()
+            // getUnpreparedBlockProposal takes tx data, and fills in the unprepared header data
+            unpreparedProposal ← getUnpreparedBlockProposal(txdata)
+            // ABCI++: the proposer may reorder/update transactions in `unpreparedProposal`
+            proposal ← ABCI.PrepareProposal(unpreparedProposal)
+        }
+        broadcast ⟨PROPOSAL, h_p, round_p, proposal, validRound_p⟩
+    } else {
+        schedule OnTimeoutPropose(h_p,round_p) to be executed after timeoutPropose(round_p)
+    }
+}
+```
+
+### ReceiveProposal
+
+In the case where the local node is not locked on any round, the following is ran:
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, −1) from proposer(h_p, round_p) while step_p = propose do {
+    if valid(v) ∧ ABCI.ProcessProposal(h_p, v).accept ∧ (lockedRound_p = −1 ∨ lockedValue_p = v) {
+        broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩ 
+    } else {
+        broadcast ⟨PREVOTE, h_p, round_p, nil⟩ 
+        // Include any slashing evidence that may be sent in the process proposal response
+        for evidence in ABCI.ProcessProposal(h_p, v).evidence_list {
+            broadcast ⟨EVIDENCE, evidence⟩ 
+        }
+    }
+    step_p ← prevote
+}
+```
+
+In the case where the node is locked on a round, the following is ran:
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, vr⟩
+  from proposer(h_p, round_p)
+  AND 2f + 1 ⟨PREVOTE, h_p, vr, id(v)⟩ 
+  while step_p = propose ∧ (vr ≥ 0 ∧ vr < round_p) do {
+    if valid(v) ∧ ABCI.ProcessProposal(h_p, v).accept ∧ (lockedRound_p ≤ vr ∨ lockedValue_p = v) {
+        broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩
+    } else {
+        broadcast ⟨PREVOTE, h_p, round_p, nil⟩
+        // Include any slashing evidence that may be sent in the process proposal response
+        for evidence in ABCI.ProcessProposal(h_p, v).evidence_list {
+            broadcast ⟨EVIDENCE, evidence⟩ 
+        }
+    }
+    step_p ← prevote
+}
+```
+
+### Prevote timeout
+
+Upon receiving 2f + 1 prevotes, setup a timeout.
+
+```go
+upon 2f + 1 ⟨PREVOTE, h_p, vr, -1⟩ 
+  with step_p = prevote for the first time, do {
+    schedule OnTimeoutPrevote(h_p, round_p) to be executed after timeoutPrevote(round_p)
+}
+```
+
+with OnTimeoutPrevote defined as:
+
+```go
+function OnTimeoutPrevote(height, round) {
+    if (height = h_p && round = round_p && step_p = prevote) {
+        precommit_extension ← ABCI.ExtendVote(h_p, round_p, nil)
+        broadcast ⟨PRECOMMIT, h_p, round_p, nil, precommit_extension⟩
+        step_p ← precommit
+    }
+}
+```
+
+### Receiving enough prevotes to precommit
+
+The following code is ran upon receiving 2f + 1 prevotes for the same block
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, *⟩
+  from proposer(h_p, round_p)
+  AND 2f + 1 ⟨PREVOTE, h_p, vr, id(v)⟩ 
+  while valid(v) ∧ step_p >= prevote for the first time do {
+    if (step_p = prevote) {
+        lockedValue_p ← v
+        lockedRound_p ← round_p
+        precommit_extension ← ABCI.ExtendVote(h_p, round_p, id(v))
+        broadcast ⟨PRECOMMIT, h_p, round_p, id(v), precommit_extension⟩
+        step_p ← precommit
+    }
+    validValue_p ← v
+    validRound_p ← round_p
+}
+```
+
+And upon receiving 2f + 1 prevotes for nil:
+
+```go
+upon 2f + 1 ⟨PREVOTE, h_p, round_p, nil⟩ 
+  while step_p = prevote do {
+    precommit_extension ← ABCI.ExtendVote(h_p, round_p, nil)
+    broadcast ⟨PRECOMMIT, h_p, round_p, nil, precommit_extension⟩
+    step_p ← precommit
+}
+```
+
+### Upon receiving a precommit
+
+Upon receiving a precommit `precommit`, we ensure that `ABCI.VerifyVoteExtension(precommit.precommit_extension) = true`
+before accepting the precommit. This is akin to how we check the signature on precommits normally, hence its not wrapped
+in the syntax of methods from the paper.
+
+### Precommit timeout
+
+Upon receiving 2f + 1 precommits, setup a timeout.
+
+```go
+upon 2f + 1 ⟨PRECOMMIT, h_p, vr, *⟩ for the first time, do {
+    schedule OnTimeoutPrecommit(h_p, round_p) to be executed after timeoutPrecommit(round_p)
+}
+```
+
+with OnTimeoutPrecommit defined as:
+
+```go
+function OnTimeoutPrecommit(height, round) {
+    if (height = h_p && round = round_p) {
+        StartRound(round_p + 1)
+    }
+}
+```
+
+### Upon Receiving 2f + 1 precommits
+
+The following code is ran upon receiving 2f + 1 precommits for the same block
+
+```go
+upon ⟨PROPOSAL, h_p, r, v, *⟩
+  from proposer(h_p, r)
+  AND 2f + 1 ⟨ PRECOMMIT, h_p, r, id(v)⟩ 
+  while decision_p[h_p] = nil do {
+    if (valid(v)) {
+        decision_p[h_p] ← v
+        h_p ← h_p + 1
+        reset lockedRound_p, lockedValue_p,validRound_p and validValue_p to initial values
+        ABCI.FinalizeBlock(id(v))
+        StartRound(0)
+    }
+}
+```
+
+If we don't see 2f + 1 precommits for the same block, we wait until we get 2f + 1 precommits, and the timeout occurs.

spec/abci++/v3.md

@@ -0,0 +1,201 @@
+# Tendermint v3 Markdown pseudocode
+
+This is a single-threaded implementation of ABCI++,
+with an optimization for the ProcessProposal phase.
+Namely, processing of the header and the block data is separated into two different functions.
+
+### Initialization
+
+```go
+h_p ← 0
+round_p ← 0
+step_p is one of {propose, prevote, precommit}
+decision_p ← Vector()
+lockedValue_p ← nil
+validValue_p ← nil
+validRound_p ← -1
+```
+
+### StartRound(round)
+
+```go
+function startRound(round) {
+    round_p ← round
+    step_p ← propose
+    if proposer(h_p, round_p) = p {
+        if validValue_p != nil {
+            proposal ← validValue_p
+        } else {
+            txdata ← mempool.GetBlock()
+            // getUnpreparedBlockProposal fills in header
+            unpreparedProposal ← getUnpreparedBlockProposal(txdata)
+            proposal ← ABCI.PrepareProposal(unpreparedProposal)
+        }
+        broadcast ⟨PROPOSAL, h_p, round_p, proposal, validRound_p⟩
+    } else {
+        schedule OnTimeoutPropose(h_p,round_p) to be executed after timeoutPropose(round_p)
+    }
+}
+```
+
+### ReceiveProposal
+
+In the case where the local node is not locked on any round, the following is ran:
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v_header, −1) from proposer(h_p, round_p) while step_p = propose do {
+    prevote_nil ← false
+    // valid is Tendermints validation, ABCI.VerifyHeader is the applications
+    if valid(v_header) ∧ ABCI.VerifyHeader(h_p, v_header) ∧ (lockedRound_p = −1 ∨ lockedValue_p = id(v_header)) {
+        wait to receive proposal v corresponding to v_header
+        // We split up the app's header verification from the remainder of its processing of the proposal
+        if ABCI.ProcessProposal(h_p, v).accept {
+            broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩ 
+        } else {
+            prevote_nil ← true
+            // Include any slashing evidence that may be sent in the process proposal response
+            for evidence in ABCI.ProcessProposal(h_p, v).evidence_list {
+                broadcast ⟨EVIDENCE, evidence⟩ 
+            }
+        }
+    } else {
+        prevote_nil ← true
+    }
+    if prevote_nil {
+        broadcast ⟨PREVOTE, h_p, round_p, nil⟩ 
+    }
+    step_p ← prevote
+}
+```
+
+In the case where the node is locked on a round, the following is ran:
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v_header, vr⟩
+  from proposer(h_p, round_p)
+  AND 2f + 1 ⟨PREVOTE, h_p, vr, id(v_header)⟩ 
+  while step_p = propose ∧ (vr ≥ 0 ∧ vr < round_p) do {
+    prevote_nil ← false
+    if valid(v) ∧ ABCI.VerifyHeader(h_p, v.header) ∧ (lockedRound_p ≤ vr ∨ lockedValue_p = v) {
+        wait to receive proposal v corresponding to v_header
+        // We split up the app's header verification from the remainder of its processing of the proposal
+        if ABCI.ProcessProposal(h_p, v).accept {
+            broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩
+        } else {
+            prevote_nil ← true
+            // Include any slashing evidence that may be sent in the process proposal response
+            for evidence in ABCI.ProcessProposal(h_p, v).evidence_list {
+                broadcast ⟨EVIDENCE, evidence⟩ 
+            }
+        }
+    } else {
+        prevote_nil ← true
+    }
+    if prevote_nil {
+        broadcast ⟨PREVOTE, h_p, round_p, nil⟩
+    }
+    step_p ← prevote
+}
+```
+
+### Prevote timeout
+
+Upon receiving 2f + 1 prevotes, setup a timeout.
+
+```go
+upon 2f + 1 ⟨PREVOTE, h_p, vr, -1⟩ 
+  with step_p = prevote for the first time, do {
+    schedule OnTimeoutPrevote(h_p, round_p) to be executed after timeoutPrevote(round_p)
+}
+```
+
+with OnTimeoutPrevote defined as:
+
+```go
+function OnTimeoutPrevote(height, round) {
+    if (height = h_p && round = round_p && step_p = prevote) {
+        precommit_extension ← ABCI.ExtendVote(h_p, round_p, nil)
+        broadcast ⟨PRECOMMIT, h_p, round_p, nil, precommit_extension⟩
+        step_p ← precommit
+    }
+}
+```
+
+### Receiving enough prevotes to precommit
+
+The following code is ran upon receiving 2f + 1 prevotes for the same block
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, *⟩
+  from proposer(h_p, round_p)
+  AND 2f + 1 ⟨PREVOTE, h_p, vr, id(v)⟩ 
+  while valid(v) ∧ step_p >= prevote for the first time do {
+    if (step_p = prevote) {
+        lockedValue_p ← v
+        lockedRound_p ← round_p
+        precommit_extension ← ABCI.ExtendVote(h_p, round_p, id(v))
+        broadcast ⟨PRECOMMIT, h_p, round_p, id(v), precommit_extension⟩
+        step_p ← precommit
+    }
+    validValue_p ← v
+    validRound_p ← round_p
+}
+```
+
+And upon receiving 2f + 1 prevotes for nil:
+
+```go
+upon 2f + 1 ⟨PREVOTE, h_p, round_p, nil⟩ 
+  while step_p = prevote do {
+    precommit_extension ← ABCI.ExtendVote(h_p, round_p, nil)
+    broadcast ⟨PRECOMMIT, h_p, round_p, nil, precommit_extension⟩
+    step_p ← precommit
+}
+```
+
+### Upon receiving a precommit
+
+Upon receiving a precommit `precommit`, we ensure that `ABCI.VerifyVoteExtension(precommit.precommit_extension) = true`
+before accepting the precommit. This is akin to how we check the signature on precommits normally, hence its not wrapped
+in the syntax of methods from the paper.
+
+### Precommit timeout
+
+Upon receiving 2f + 1 precommits, setup a timeout.
+
+```go
+upon 2f + 1 ⟨PRECOMMIT, h_p, vr, *⟩ for the first time, do {
+    schedule OnTimeoutPrecommit(h_p, round_p) to be executed after timeoutPrecommit(round_p)
+}
+```
+
+with OnTimeoutPrecommit defined as:
+
+```go
+function OnTimeoutPrecommit(height, round) {
+    if (height = h_p && round = round_p) {
+        StartRound(round_p + 1)
+    }
+}
+```
+
+### Upon Receiving 2f + 1 precommits
+
+The following code is ran upon receiving 2f + 1 precommits for the same block
+
+```go
+upon ⟨PROPOSAL, h_p, r, v, *⟩
+  from proposer(h_p, r)
+  AND 2f + 1 ⟨ PRECOMMIT, h_p, r, id(v)⟩ 
+  while decision_p[h_p] = nil do {
+    if (valid(v)) {
+        decision_p[h_p] ← v
+        h_p ← h_p + 1
+        reset lockedRound_p, lockedValue_p,validRound_p and validValue_p to initial values
+        ABCI.FinalizeBlock(id(v))
+        StartRound(0)
+ }
+}
+```
+
+If we don't see 2f + 1 precommits for the same block, we wait until we get 2f + 1 precommits, and the timeout occurs.

spec/abci++/v4.md

@@ -0,0 +1,199 @@
+# Tendermint v4 Markdown pseudocode
+
+This is a multi-threaded implementation of ABCI++,
+where ProcessProposal starts when the proposal is received, but ends before precommitting.
+
+### Initialization
+
+```go
+h_p ← 0
+round_p ← 0
+step_p is one of {propose, prevote, precommit}
+decision_p ← Vector()
+lockedValue_p ← nil
+validValue_p ← nil
+validRound_p ← -1
+```
+
+### StartRound(round)
+
+```go
+function startRound(round) {
+    round_p ← round
+    step_p ← propose
+    if proposer(h_p, round_p) = p {
+        if validValue_p != nil {
+            proposal ← validValue_p
+        } else {
+            txdata ← mempool.GetBlock()
+            // getUnpreparedBlockProposal fills in header
+            unpreparedProposal ← getUnpreparedBlockProposal(txdata)
+            proposal ← ABCI.PrepareProposal(unpreparedProposal)
+        }
+        broadcast ⟨PROPOSAL, h_p, round_p, proposal, validRound_p⟩
+    } else {
+        schedule OnTimeoutPropose(h_p,round_p) to be executed after timeoutPropose(round_p)
+    }
+}
+```
+
+### ReceiveProposal
+
+In the case where the local node is not locked on any round, the following is ran:
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, −1) from proposer(h_p, round_p) while step_p = propose do {
+    if valid(v) ∧ ABCI.VerifyHeader(h_p, v.header) ∧ (lockedRound_p = −1 ∨ lockedValue_p = v) {
+        // We fork process proposal into a parallel process
+        Fork ABCI.ProcessProposal(h_p, v)
+        broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩ 
+    } else {
+        broadcast ⟨PREVOTE, h_p, round_p, nil⟩ 
+    }
+    step_p ← prevote
+}
+```
+
+In the case where the node is locked on a round, the following is ran:
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, vr⟩
+  from proposer(h_p, round_p)
+  AND 2f + 1 ⟨PREVOTE, h_p, vr, id(v)⟩ 
+  while step_p = propose ∧ (vr ≥ 0 ∧ vr < round_p) do {
+    if valid(v) ∧ ABCI.VerifyHeader(h_p, v.header) ∧ (lockedRound_p ≤ vr ∨ lockedValue_p = v) {
+        // We fork process proposal into a parallel process
+        Fork ABCI.ProcessProposal(h_p, v)
+        broadcast ⟨PREVOTE, h_p, round_p, id(v)⟩
+    } else {
+        broadcast ⟨PREVOTE, h_p, round_p, nil⟩
+    }
+    step_p ← prevote
+}
+```
+
+### Prevote timeout
+
+Upon receiving 2f + 1 prevotes, setup a timeout.
+
+```go
+upon 2f + 1 ⟨PREVOTE, h_p, vr, -1⟩ 
+  with step_p = prevote for the first time, do {
+    schedule OnTimeoutPrevote(h_p, round_p) to be executed after timeoutPrevote(round_p)
+}
+```
+
+with OnTimeoutPrevote defined as:
+
+```go
+def OnTimeoutPrevote(height, round) {
+    if (height = h_p && round = round_p && step_p = prevote) {
+        // Join the ProcessProposal, and output any evidence in case it has some.
+        processProposalOutput ← Join ABCI.ProcessProposal(h_p, v)
+        for evidence in processProposalOutput.evidence_list {
+            broadcast ⟨EVIDENCE, evidence⟩ 
+        }
+
+        precommit_extension ← ABCI.ExtendVote(h_p, round_p, nil)
+        broadcast ⟨PRECOMMIT, h_p, round_p, nil, precommit_extension⟩
+        step_p ← precommit
+    }
+}
+```
+
+### Receiving enough prevotes to precommit
+
+The following code is ran upon receiving 2f + 1 prevotes for the same block
+
+```go
+upon ⟨PROPOSAL, h_p, round_p, v, *⟩
+  from proposer(h_p, round_p)
+  AND 2f + 1 ⟨PREVOTE, h_p, vr, id(v)⟩ 
+while valid(v) ∧ step_p >= prevote for the first time do {
+    if (step_p = prevote) {
+        lockedValue_p ← v
+        lockedRound_p ← round_p
+        processProposalOutput ← Join ABCI.ProcessProposal(h_p, v)
+        // If the proposal is valid precommit as before.
+        // If it was invalid, precommit nil.
+        // Note that ABCI.ProcessProposal(h_p, v).accept is deterministic for all honest nodes.
+        precommit_value ← nil
+        if processProposalOutput.accept {
+            precommit_value ← id(v)
+        }
+        precommit_extension ← ABCI.ExtendVote(h_p, round_p, precommit_value)
+        broadcast ⟨PRECOMMIT, h_p, round_p, precommit_value, precommit_extension⟩
+        for evidence in processProposalOutput.evidence_list {
+            broadcast ⟨EVIDENCE, evidence⟩ 
+        }
+
+        step_p ← precommit
+    }
+    validValue_p ← v
+    validRound_p ← round_p
+}
+```
+
+And upon receiving 2f + 1 prevotes for nil:
+
+```go
+upon 2f + 1 ⟨PREVOTE, h_p, round_p, nil⟩ 
+  while step_p = prevote do {
+    // Join ABCI.ProcessProposal, and broadcast any evidence if it exists.
+    processProposalOutput ← Join ABCI.ProcessProposal(h_p, v)
+    for evidence in processProposalOutput.evidence_list {
+        broadcast ⟨EVIDENCE, evidence⟩ 
+    }
+
+    precommit_extension ← ABCI.ExtendVote(h_p, round_p, nil)
+    broadcast ⟨PRECOMMIT, h_p, round_p, nil, precommit_extension⟩
+    step_p ← precommit
+}
+```
+
+### Upon receiving a precommit
+
+Upon receiving a precommit `precommit`, we ensure that `ABCI.VerifyVoteExtension(precommit.precommit_extension) = true`
+before accepting the precommit. This is akin to how we check the signature on precommits normally, hence its not wrapped
+in the syntax of methods from the paper.
+
+### Precommit timeout
+
+Upon receiving 2f + 1 precommits, setup a timeout.
+
+```go
+upon 2f + 1 ⟨PRECOMMIT, h_p, vr, *⟩ for the first time, do {
+    schedule OnTimeoutPrecommit(h_p, round_p) to be executed after timeoutPrecommit(round_p)
+}
+```
+
+with OnTimeoutPrecommit defined as:
+
+```go
+def OnTimeoutPrecommit(height, round) {
+    if (height = h_p && round = round_p) {
+        StartRound(round_p + 1)
+    }
+}
+```
+
+### Upon Receiving 2f + 1 precommits
+
+The following code is ran upon receiving 2f + 1 precommits for the same block
+
+```go
+upon ⟨PROPOSAL, h_p, r, v, *⟩
+  from proposer(h_p, r)
+  AND 2f + 1 ⟨ PRECOMMIT, h_p, r, id(v)⟩ 
+  while decision_p[h_p] = nil do {
+    if (valid(v)) {
+        decision_p[h_p] ← v
+        h_p ← h_p + 1
+        reset lockedRound_p, lockedValue_p,validRound_p and validValue_p to initial values
+        ABCI.FinalizeBlock(id(v))
+        StartRound(0)
+    }
+}
+```
+
+If we don't see 2f + 1 precommits for the same block, we wait until we get 2f + 1 precommits, and the timeout occurs.