Flood gossip protocol

Flood is a basic push gossip protocol: every time a node receives a transaction, it forwards (or "pushes") the transaction to all its peers, except to the peer(s) from which it received the transaction.

This protocol is built on top of the mempool and p2p modules.

Table of contents

This document was written using the literature programming paradigm. Code snippets are written in Quint and can get "tangled" into a Quint file.

Messages

Nodes communicates only one type of message carrying a full transaction.

type Message =
    | TxMsg(TX)

State

Flood's state consists of the underlying mempool state (variable mempool) and P2P state (variables incomingMsgs and peers).

Additionally, for each transaction in each node's mempool, we keep track of the peer IDs from whom the node received the transaction.

var senders: NodeID -> TxID -> List[NodeID]

We define the senders as a list instead of a set because the DOG protocol needs to know who is the first sender of a transaction.

Note that a transaction won't have a sender when it is in the cache but not in the mempool. Senders are only needed for disseminating (valid) transactions that are in the mempool.

<details> <summary>Auxiliary definitions</summary>

def Senders(node) = senders.get(node)

The set of senders of transaction txID:

def sendersOf(node, txID) = 
    node.Senders().mapGetDefault(txID, List())

Function addSender adds a sender to tx's list of senders (_txSenders), if optionalSender has a value that's not already in the list.

pure def addSender(_txSenders, tx, optionalSender) = 
    match optionalSender {
    | Some(sender) => _txSenders.update(hash(tx), ss => 
        if (ss.includes(sender)) ss else ss.append(sender))
    | None => _txSenders
    }

</details>

Initial state

Flood's initial state is the underlying mempool's initial state (MP_init) and an empty mapping of transactions to senders.

action init = all {
    MP_init,
    senders' = NodeIDs.mapBy(n => Map()),
}

State transitions (actions)

These are the state transitions of the system. Note that generic actions are imported from the mempool and p2p specs. The missing implementation details (tryAddTx, handleMessage, mkTargetNodes) are described in the rest of the section.

User-submitted transactions: when a node receives a transaction from a user, it tries to add it to the mempool.
```
nondet node = oneOf(nodesInNetwork)
nondet tx = oneOf(AllTxs)
node.receiveTxFromUser(tx, tryAddTx),
```

Peer message handling: a node processes messages received from a peer.

nondet node = oneOf(nodesInNetwork)
node.receiveFromPeer(handleMessage),

Transaction dissemination: a node sends a transaction in its mempool to a subset of target nodes.

nondet node = oneOf(nodesInNetwork)
all {
    node.disseminateNextTx(mkTargetNodes, TxMsg),
    senders' = senders,
},

A node joins the network.

all {
    pickNodeAndJoin,
    mempool' = mempool,
    senders' = senders,
},

A node disconnects from the network.

nondet node = oneOf(nodesInNetwork) 
all {
    require(size(nodesInNetwork) > 1),
    // Disconnect node and remove node from other peers' connections.
    peers' = peers
        .disconnect(node)
        .updateMultiple(nodesInNetwork, ps => ps.exclude(Set(node))),
    incomingMsgs' = incomingMsgs,
    mempool' = mempool,
    senders' = senders,
},

Adding transactions to the mempool

A node attempting to add a transaction to its mempool processes the transaction according to whether it has seen it before, that is, if the transaction exists in the mempool cache.

A first-time transaction is one that the node does not have in its cache.
A duplicate transaction is one that the node has received multiple times, and thus it's cached.

action tryAddTx(node, _incomingMsgs, optionalSender, tx) = 
    if (not(hash(tx).in(node.Cache())))
        node.tryAddFirstTimeTx(_incomingMsgs, optionalSender, tx)
    else
        node.processDuplicateTx(_incomingMsgs, optionalSender, tx)

In this action the sender is optional. When there's a sender, it means that the transaction comes from a peer; otherwise it comes directly from a user.

Adding first-time transactions

tryAddFirstTimeTx attempts to add a first-time transaction tx to a node's mempool:

it caches tx,
if tx is valid, it appends tx to txs, and
updates its senders.

action tryAddFirstTimeTx(node, _incomingMsgs, optionalSender, tx) = all {
    mempool' = mempool.update(node, st => {
        cache: st.cache.join(hash(tx)),
        txs: if (valid(tx)) st.txs.append(tx) else st.txs,
        ...st }),
    senders' = senders.update(node, ss =>
        if (valid(tx)) ss.addSender(tx, optionalSender) else ss),
    incomingMsgs' = _incomingMsgs,
    peers' = peers,
}

Handling duplicate transactions

Action processDuplicateTx processes a duplicate transaction tx by updating the list of senders, only if tx is already in the mempool (txs).

action processDuplicateTx(node, _incomingMsgs, optionalSender, tx) = all {
    senders' = senders.update(node, ss =>
        if (node.Txs().includes(tx)) ss.addSender(tx, optionalSender) else ss),
    mempool' = mempool,
    incomingMsgs' = _incomingMsgs,
    peers' = peers,
}

Handling incoming messages

Upon receiving a message with transaction tx from a peer (i.e., the sender), the node attempts to add tx to its mempool.

action handleMessage(node, _incomingMsgs, sender, msg) =
    match msg {
    | TxMsg(tx) => node.tryAddTx(_incomingMsgs, Some(sender), tx)
    }

The argument _incomingMsgs is passed just to update the queues of incoming messages, when applicable (Flood does not reply with any message but DOG does).

Transaction dissemination

In Flood, a node sends a transaction to all its peers except those who previously sent it.

mkTargetNodes defines the set of peers to whom node will send tx. It is passed as an argument to the generic transaction dissemination action.

def mkTargetNodes(node, tx) =
    node.Peers().exclude(node.sendersOf(hash(tx)).listToSet())

Properties

Function txInAllMempools returns true if the given transaction tx is in the mempool of all nodes.

def txInAllMempools(tx) =
    NodeIDs.forall(n => n.Txs().includes(tx))

Property If a transaction is in the mempool of any node, then eventually the transaction will reach the mempool of all nodes (maybe more than once, and assuming transactions are not removed from mempools).

temporal txInPoolGetsDisseminated = 
    AllTxs.forall(tx => 
        NodeIDs.exists(node =>
            node.Txs().includes(tx) implies eventually(txInAllMempools(tx))))

Invariant If node A sent a transaction tx to node B (A is in the list of tx's senders), then B does not send tx to A (the message won't be in A's incoming messages).

val dontSendBackToSender =
    NodeIDs.forall(nodeA => 
        NodeIDs.forall(nodeB => 
            AllTxs.forall(tx =>
                nodeB.sendersOf(hash(tx)).includes(nodeA) 
                implies
                not(nodeA.IncomingMsgs().includes((nodeB, TxMsg(tx))))
    )))

← Back to Documentation