Skip to content

Commit

Permalink
FIP-0086: Specify power table scaling & comm tree (#983)
Browse files Browse the repository at this point in the history 
* Add commitments tree root to the ECTipset
* Redefined the Tipset as a list of CIDs.
* Clarified that the power table is a bare CBOR list (no wrappingstructure).
* Make the Epoch a uint64 instead of an int.
* Specify power table scaling
  • Loading branch information
@Stebalien
Stebalien authored Apr 11, 2024
1 parent 196b68f commit 75c550d
Showing 1 changed file with 39 additions and 35 deletions.
74 changes: 39 additions & 35 deletions FIPS/fip-0086.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -270,17 +270,16 @@ type Payload struct {
}
type ECTipset struct {
Epoch int
Epoch uint64
Tipset []CID // Tipset key, a canonical array of a tipset's block header CIDs.
PowerTable CID // Commitment to resulting power table.
Commitments [32]byte // Root of a Merkle tree containing additional commitments, defaults to 0.
}
// Table of nodes with power > 0 and their public keys.
// This is expected to be calculated from the EC chain state and provided to GossiPBFT.
// Ordered by (power descending, participant ascending).
type PowerTable {
Entries []PowerTableEntry
}
type PowerTable = []PowerTableEntry
type PowerTableEntry struct {
ParticipantID ActorID
Expand All @@ -300,8 +299,13 @@ A set of messages $M$ that does not contain equivocating messages is called _cle

#### Predicates and functions used in the protocol

* `Power(p | P) ∈ [0, 1]`
* Returns the relative QAP of participant $p$ (or set of participants $p$) in EC, defined by the power table corresponding to $baseChain$. The returned value is a fraction of the total QAP of all participants in the power table.
* `Power(p | P) ∈ [0x0000, 0xffff]`
* Returns the relative QAP of participant $p$ in EC as an integer in the range `[0x0000, 0xffff]`, defined by the power table corresponding to $baseChain$.
* If $p$ is a set of participants, the returned value is $\sum_{p\prime \in p} \texttt{Power}(p\prime | P)$. That is, the sum of the $\texttt{Power}$ of the participants in the set.
* Otherwise, the returned value is a fraction of the total QAP of all participants in the power table scaled to an integer in the range $[0, 2^{16})$, rounded down ($\lfloor (2^{16}-1) \times \texttt{QAP}(p) / \texttt{QAP}(P) \rfloor$).
* `IsStrongQuorum(p | P)`
* Returns $True$ if $\texttt{Power}(p) \ge \lceil ⅔\texttt{Power}(P) \rceil$ where $p$ is a subset of the participants and $P$ is the set of all members in the power table.
* $\texttt{Power}(P)$ will likely be less than $\mathrm{0xffff}$ due to compounded rounding errors.
* `isPrefix(a,b)`
* Returns $True$ if chain $a$ is a prefix of chain $b$. (Each chain is also a prefix of itself.)
* `HasStrongQuorum(prefix,M)`
Expand All @@ -310,12 +314,12 @@ A set of messages $M$ that does not contain equivocating messages is called _cle
```
Let P={p : ∃ m∈ M: m.sender=p AND isPrefix(prefix,m.value)}
```
then the predicate returns $True$ iff $\texttt{Power}(P)>2/3$
then the predicate returns $True$ iff $\texttt{IsStrongQuorum}(P)$.
* `HasStrongQuorumValue(M)`
* Where $M$ is a clean set of messages of the same type and the same round
* The predicate returns $True$ iff there is a value $v$, such that there is a set $P$ of participants who are senders of messages in $M$ such that their message value is exactly $v$ and $\texttt{Power}(P)>2/3$. More precisely:
* The predicate returns $True$ iff there is a value $v$, such that there is a set $P$ of participants who are senders of messages in $M$ such that their message value is exactly $v$ and $IsStrongQuorum(P)$. More precisely:
```
HasStrongQuorumValue(M) = ∃ v: Power({p : ∃ m∈ M: m.sender=p AND m.value=v})>2/3
HasStrongQuorumValue(M) = ∃ v: IsStrongQuorum({p : ∃ m∈ M: m.sender=p AND m.value=v})
```
* `StrongQuorumValue(M)`
* Returns $v$ if $\texttt{HasStrongQuorumValue}(M)$ holds, $nil$ otherwise.
Expand Down Expand Up @@ -373,8 +377,8 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF:

28: BEBroadcast <PREPARE, value, instance, round>; trigger(timeout)
29: collect a clean set M of valid <PREPARE, proposal, instance, round> msgs \* match PREPARE value against local proposal
until Power(M) > ⅔ OR timeout expires
30: if (Power(M) > ⅔) \* strong quorum of PREPAREs for local proposal
until IsStrongQuorum(M) OR timeout expires
30: if IsStrongQuorumPower(M) \* strong quorum of PREPAREs for local proposal
31: value ← proposal \* vote for deciding proposal (COMMIT)
32: evidence ← Aggregate(M) \* strong quorum of PREPAREs is evidence
33: else
Expand All @@ -384,7 +388,7 @@ GossiPBFT(instance, inputChain, baseChain, participants) → decision, PoF:
36: BEBroadcast <COMMIT, value, instance, evidence, round>; trigger(timeout)
37: collect a clean set M of valid COMMIT messages from this round
until (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄)
OR (timeout expires AND Power(M)>2/3)
OR (timeout expires AND IsStrongQuorum(M))
38: if (HasStrongQuorumValue(M) AND StrongQuorumValue(M) ≠ 丄) \* decide
39: evidence ← Aggregate(M)
39: BEBroadcast <DECIDE, StrongQuorumValue(M), evidence>
Expand Down Expand Up @@ -455,29 +459,29 @@ The $\texttt{ValidEvidence}()$ predicate is defined below. Note that QUALITY and
```
ValidEvidence(m):

(m = <CONVERGE, value, round, evidence, ticket> | valid CONVERGE
AND (∃ M: Power(M) > ⅔ AND m.evidence=Aggregate(M) | evidence is a strong quorum
AND ((∀ m' ∈ M: m'.step = COMMIT AND m'.value = 丄) | of COMMIT msgs for 丄
OR (∀ m' ∈ M: m'.step = PREPARE AND | or PREPARE msgs for
m'.value = m.value)) | CONVERGE value
AND (∀ m' ∈ M: m'.round = m.round-1) | from previous round to CONVERGE
AND (∀ m' ∈ M: m'.instance = m.instance))) | from the same instance as CONVERGE


OR (m = <COMMIT, value, round, evidence> | valid COMMIT
AND (∃ M: Power(M) > ⅔ AND m.evidence=Aggregate(M) | evidence is a strong quorum
AND ∀ m' ∈ M: m'.step = PREPARE | of PREPARE messages
AND ∀ m' ∈ M: m'.round = m.round | from the same round as COMMIT
AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance as COMMIT
AND ∀ m' ∈ M: m'.value = m.value) | for the same value as COMMIT, or
OR (m.value = 丄) AND m.evidence=nil) | COMMIT is for 丄 with no evidence

OR (m = <DECIDE, value, round, evidence> | valid DECIDE
AND (∃ M: Power(M) > ⅔ AND m.evidence=Aggregate(M) | evidence is a strong quorum
AND ∀ m' ∈ M: m'.step = COMMIT | of COMMIT messages
AND ∀ m', m'' ∈ M: m'.round = m''.round | from the same round as each other
AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance as DECIDE
AND ∀ m' ∈ M: m'.value = m.value) | for the same value as DECIDE
(m = <CONVERGE, value, round, evidence, ticket> | valid CONVERGE
AND (∃ M: IsStrongQuorum(M) AND m.evidence=Aggregate(M) | evidence is a strong quorum
AND ((∀ m' ∈ M: m'.step = COMMIT AND m'.value = 丄) | of COMMIT msgs for 丄
OR (∀ m' ∈ M: m'.step = PREPARE AND | or PREPARE msgs for
m'.value = m.value)) | CONVERGE value
AND (∀ m' ∈ M: m'.round = m.round-1) | from previous round to CONVERGE
AND (∀ m' ∈ M: m'.instance = m.instance))) | from the same instance as CONVERGE


OR (m = <COMMIT, value, round, evidence> | valid COMMIT
AND (∃ M: IsStrongQuorum(M) AND m.evidence=Aggregate(M) | evidence is a strong quorum
AND ∀ m' ∈ M: m'.step = PREPARE | of PREPARE messages
AND ∀ m' ∈ M: m'.round = m.round | from the same round as COMMIT
AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance as COMMIT
AND ∀ m' ∈ M: m'.value = m.value) | for the same value as COMMIT, or
OR (m.value = 丄) AND m.evidence=nil) | COMMIT is for 丄 with no evidence

OR (m = <DECIDE, value, round, evidence> | valid DECIDE
AND (∃ M: IsStrongQuorum(M) AND m.evidence=Aggregate(M) | evidence is a strong quorum
AND ∀ m' ∈ M: m'.step = COMMIT | of COMMIT messages
AND ∀ m', m'' ∈ M: m'.round = m''.round | from the same round as each other
AND ∀ m' ∈ M: m'.instance = m.instance | from the same instance as DECIDE
AND ∀ m' ∈ M: m'.value = m.value) | for the same value as DECIDE
```
### Evidence verification complexity
Expand Down

0 comments on commit 75c550d

Please sign in to comment.