LibraBFT2.txt

type BlockId
type Block = struct {
    parent: BlockId,
    round: uint,
}

function Hash(Block): BlockId
const blocks: [BlockId]Block 
axiom forall id: BlockId. Hash(blocks[id]) == id

const h: uint // number of honest replicas
const f: uint // number of faulty replicas
axiom h > 2f

const root: BlockId // root of block tree
axiom blocks[root].round == 0 && blocks[root].parent == root

type HonestReplicaId = 1..h // ids of honest replicas
type HonestQuorum = {q: Set<HonestReplicaId> | size(q) >= h - f} // all possible quorums of honest nodes

// primitive function that returns true iff id' can reach id by following parent link 0 or more times
function Reaches(id': BlockId, id: BlockId): bool;

function Consistent(id': BlockId, id: BlockId) : bool {
    Reaches(id', id) || Reaches(id, id')
}

//// global model variables

// all collected votes sent by honest replicas
var voteStore: [BlockId]Set<HonestReplicaId>

// id of the latest globally-committed block
var globallyCommitted: BlockId

//// per-replica variables

// all blocks on which quorum has been established
var qcStore: [HonestReplicaId]Set<BlockId>

// monotonically increasing round of the last voted block
var lastVoteRound: [HonestReplicaId]uint

// monotonically increasing round of the preferred block
var preferredBlockRound: [HonestReplicaId]uint

//// procedures

procedure Initialize()
{
    voteStore := (lambda id: BlockId. if id = root then HonestReplicaId else {})
    globallyCommitted := root
    qcStore := (lambda r: HonestReplicaId. { root })
    lastVoteRound := (lambda r: HonestReplicaId. 0)
    preferredBlockRound := (lambda r: HonestReplicaId. 0)
}

//// start things off
procedure Main() {
    var r: HonestReplicaId
    var blockId: BlockId

    // propose or commit nondeterministically
    if * {
        async OnProposal(r, blockId)
    } 
    else if * {
        async OnQuorumCertificate(r, blockId)
    } 
    else {
        async OnCommit(r, blockId)
    }

    // keep going nondeterministically
    if * {
        async Main()
    }
}

//// helper procedure to add quorum certificate
procedure TryAddQuorumCertificate(r: HonestReplicaId, blockId: BlockId) : bool 
reads  qcStore, voteStore, preferredBlockRound
writes qcStore, preferredBlockRound
{
    var numHonestVoters: uint
    var numEquivocators: uint
    var b'', b': Block

    // numHonestVoters is the number of honest votes seen by this replica
    assume numHonestVoters <= size(voteStore[blockId])
    // numEquivocators is the number of faulty replicas who voted for blockId
    assume numEquivocators <= f
    if numHonestVoters + numEquivocators >= h {
        qcStore[r] := qcStore[r] + blockId
    }

    // possibly update preferred block
    if blockId in qcStore[r] {
        b'' := blocks[blockId]
        b'  := blocks[b''.parent]
        if b'.round > preferredBlockRound[r] {
            preferredBlockRound[r] := b'.round
        }
    }

    blockId in qcStore[r]
}

//// possibly vote
procedure TryVote(r: HonestReplicaId, newBlockId: BlockId) 
reads voteStore, lastVoteRound, preferredBlockRound
writes voteStore, lastVoteRound
{
    var newBlock, b'': Block

    newBlock := blocks[newBlockId]
    b'' := blocks[newBlock.parent]
    if newBlock.round > lastVoteRound[r] && b''.round >= preferredBlockRound[r] {
        lastVoteRound[r] := newBlock.round
        voteStore[newBlockId] := voteStore[newBlockId] + r
    }
}

//// event handler at a replica to process a proposal
procedure OnProposal(r: HonestReplicaId, newBlockId: BlockId)
reads  qcStore, preferredBlockRound
writes qcStore, preferredBlockRound
{
    var newBlock: Block

    newBlock := blocks[newBlockId]
    if !TryAddQuorumCertificate(r, newBlock.parent) {
        return
    }
    
    async TryVote(r, newBlockId)
}

//// event handler at a replica to add a quorum certificate
procedure OnQuorumCertificate(r: HonestReplicaId, blockId: BlockId)
reads  qcStore, voteStore, preferredBlockRound
writes qcStore, preferredBlockRound
{
    TryAddQuorumCertificate(r, blockId)
}

//// event handler at a replica to commit a block
procedure OnCommit(r: HonestReplicaId, id'': BlockId)
reads  qcStore, globallyCommitted
writes globallyCommitted
{
    var id', id: BlockId
    var b'', b', b: Block

    if !(id'' in qcStore[r]) {
        return
    }
    b'' := blocks[id'']
    id' := b''.parent
    b'  := blocks[id']
    id  := b'.parent
    b := blocks[id]
    if b''.round == b'.round + 1 && b'.round == b.round + 1 {
        assert Consistent(id, globallyCommitted)
        if Reaches(id, globallyCommitted) {
            globallyCommitted := id
        }
    }
}

////  Invariants

function OneChain(id: BlockId, id': BlockId): bool
{
    id = blocks[id'].parent
}

function ContiguousOneChain(id: BlockId, id': BlockId): bool
{
    id = blocks[id'].parent && blocks[id].round + 1 == blocks[id'].round
}

function TwoChain(id: BlockId, id': BlockId, id'': BlockId) : bool 
{
    OneChain(id, id') && OneChain(id', id'')
}

function ContiguousTwoChain(id: BlockId, id': BlockId, id'': BlockId) : bool 
{
    ContiguousOneChain(id, id') && ContiguousOneChain(id', id'')
}

forall r in HonestReplicaId. forall id, id' in qcStore[r]. 
    OneChain(id, id') ==> (id' == root || blocks[id].round < blocks[id'].round)

forall r in HonestReplicaId. forall id, id' in qcStore[r]. 
    blocks[id].round == blocks[id'].round ==> id == id'

forall r in HonestReplicaId. forall id, id', id'' in qcStore[r].
    TwoChain(id, id', id'') ==>
        (exists q: HonestQuorum. (forall x: HonestReplicaId. x in q ==> preferredBlockRound[x] >= blocks[id].round))

forall r in HonestReplicaId. forall id, id', id'' in qcStore[r].
    ContiguousTwoChain(id, id', id'') ==>
        (forall x in qcStore[r]. blocks[x].round > blocks[id''].round ==> Reaches(x, id))

forall rx, ry in HonestReplicaId. forall xid, xid', xid'' in qcStore[rx]. forall yid, yid', yid'' in qcStore[ry].
    ContiguousTwoChain(xid, xid', xid'') && ContiguousTwoChain(yid, yid', yid'') ==> Consistent(xid, yid)