# A Formal Analysis of the Mimblewimble Cryptocurrency Protocol +
## 5 Model-Driven Verification
### Excerpt of a Z Model of a Consensus Protocol  
The following is part of a Z model of a consensus protocol based on the model developed by [PERSON] and [PERSON] [20]. For readers unfamiliar with the Z notation we have included some background in Appendix B. The time stamps used in the protocol are modeled as natural numbers. Then we have the type of addresses (_Addr_), the type of hashes (_Hash_), the type of proofs objects (_Proof_) and the type of transactions (_Tx_). Differently from [PERSON] and [PERSON]'s model (PS) we model addresses as a given type instead as natural numbers. In PS the only condition required for these types is that they come equipped with equality, which is the case in Z. \[ \begin{array}{l}\mathit{Time}==\mathbb{N}\\ \left[\mathit{Addr},\mathit{Hash},\mathit{Proof},\mathit{Tx}\right]\end{array} \]  
The block data structure is a record with three fields: _prev_, (usually) points to the parent block; _txs_, stores the sequence of transactions stored in the block; and _pf_ is a proof object required to validate the block. \[ \begin{array}{l}\mathit{Block}\\ \mathit{prev}:\mathit{Hash}\\ \mathit{txs}:\mathrm{seq}\mathit{Tx}\\ \mathit{pf}:\mathit{Proof}\end{array} \]  
Next, we define the following parameters of the model: _hashb_, a function computing the hash of a block; _hasht_, a function computing the hash of a transaction; _mkProof_, a function computing a proof object of a node; _VAF_, a relation used to validate proof objects; _txValid_, a relation used to validate transactions; and _txExtend_, a relation used to modify a set of pending transactions stored in a node. _VAF_ is constrained to triplets where the block whose proof is being considered is not one of the blocks of the chain being considered. \[ \begin{array}{l}\mathit{hashb}:\mathit{Block}\mapsto\mathit{Hash}\\ \mathit{hasht}:\mathit{Tx}\mapsto\mathit{Hash}\\ \mathit{mkProof}:\mathit{Addr}\times\mathrm{seq}\mathit{Block}\mapsto\mathit{ Proof}\\ \mathit{VAF}:\mathbb{P}(\mathit{Proof}\times\mathit{Time}\times\mathrm{seq} \mathit{Block})\\ \mathit{txValid}:\mathit{Tx}\leftrightarrow\mathrm{seq}\mathit{Block}\\ \mathit{txExtend}:\mathbb{P}\mathit{Tx}\times\mathit{Tx}\rightarrow\mathbb{P} \mathit{Tx}\\ \forall\,b:\mathit{Block},\ t:\mathit{Time},\ c:\mathrm{seq}\mathit{Block}\bullet( \mathit{b.pf},t,c)\in\mathit{VAF}\Rightarrow b\
otin\mathrm{ran}\,c\end{array} \]  
Another parameter of our model is the _genesis block_, called \(GB\), which should be provided by the client of the model. Clearly, \(GB\) is a block enjoining two particular properties: it has no parent and it contains no transactions. \( \begin{array}{l}\mathit{GB}:\mathit{Block}\\ \hline\mathit{GB}.\mathit{prev}=\mathit{hashb}\mathit{GB}\\ \mathit{GB}.\mathit{txs}=\langle\rangle\end{array} \)  
The local state space of a participating network node is given by four state variables: _this_, representing the address of the node; _as_, are the addresses of the peers this node is aware of; _bf_, is a block forest which records the minted and received blocks; and _tp_, is a set of received transactions, which will eventually be included in minted blocks. \( \begin{array}{l}\mathit{LocState}\\ \hline\mathit{this}:\mathit{Addr}\\ \mathit{as}:\mathbb{P}\mathit{Addr}\\ \mathit{bf}:\mathit{Hash}\leftrightarrow\mathit{Block}\\ \mathit{tp}:\mathbb{P}\mathit{Tx}\end{array} \)  
As nodes can send messages, we define their type. _NullMsg_ is used when, actually, the node does not send any message (think of it as the null statement in programming languages, that is, _skip_). Note that some messages contain some data, for example, _AddrMsg_ which communicates a set of peers by transmitting their addresses. \(