# A Formal Analysis of the Mimblewimble Cryptocurrency Protocol +
## Appendix B Background on the Z Notation  
The Z notation is a formal method based on first-order logic and Zermelo-Fraenkel set theory. Any Z specification takes the form of a state machine--not necessarily a finite one. This machine is defined by giving its state space and the transitions between those states. The state space is given by declaring a tuple of typed state variables. A transition, called operation in Z, is defined by specifying its signature, its preconditions and its postconditions. The signature of an operation includes input, state and output variables. Each operation can change the state of the machine. State change is described by giving the relation between before-state and after-state variables. In order to introduce the Z notation we will use a simple example. Think in the savings accounts of a bank. Each account is identified by a so-called account number. The bank requires to keep record of just the balance of each account. Since account numbers are used just as identifiers we can abstract them away, not caring about their internal structure. Z provides so-called basic or given types for these cases. The Z syntax for introducing a basic type is:  
\[[\textit{ACCNUIM}]\]  
In this way, it is possible to declare variables of type _ACCNUIM_ and it is possible to build more complex types involving it--for instance the type of all sets of account numbers is \(\mathbb{P}\,\textit{ACCNUIM}\). We represent the money that clients can deposit and withdraw and the balance of savings accounts as natural numbers. The type for the integer numbers, \(\mathbb{Z}\), is built-in in Z. The notation also includes the set of natural numbers, \(\mathbb{N}\). Then, we define:  
\[\textit{MONEY}==\mathbb{N}\]  
\[\textit{BALANCE}==\mathbb{N}\]  
In other words, we introduce two synonymous for the set of natural numbers so the specification is more readable. The state space is defined as follows:  
\[\textit{Bank}\]  
\[\textit{balances}:\textit{ACCNUIM}\ \rightarrow\ \textit{BALANCE}\]  
This construction is called schema; each schema has a name that can be used in other schemas. In particular this is a state schema because it only declares state variables. In effect, it declares one state variable by giving its name and type. Each state of the system corresponds to a particular valuation of this variable. The type constructor \(\rightarrow\) definespartial functions. (It must be noted that the Z type system is not as strong as the type systems of other formalisms, such as Coq. So we will be as formal as is usual in the Z community regarding its type system). Then, _balances_ is a partial function from _ACCNIM_ onto _BALANCE_. It makes sense to define such a function because each account has a unique _ACCNIM_; and it makes sense to make _balances_ partial because not every account number is used all the time at the bank (i.e., when an account is opened the bank assigns it an unused account number; and when an account is closed its account number is no longer used). Now, we can define the initial state of the system as follows:  
_InitBank_  
_Bank_  
_balances_ = \(O\)  
_InitBank_ is another schema. The upper part is the declaration part and the lower part is the predicate part--this one is optional and is absent from _Bank_. In the declaration part we can declare variables or use schema inclusion. The latter means that we can write the name of another schema instead of declaring their variables. This allows us to reuse schemas. In this case the predicate part says that the state variable is equal to the empty set. It is important to remark that the = symbol is logical equality and not an imperative assignment--Z has no notion of control flow. In Z, functions are sets of ordered pairs. Being sets they can be compared with the empty set. The symbol \(O\) is polymorphic in Z: it is the same for all types. Now we can define an operation of the system (i.e., a state transition) specifying how an account is opened. _NewAccountOk_  
_Bank_  
_n_? _ACCNUM_  
_n_? _dom_ _balances_  
_balances_ = _balances_ \(\cup\) {_n_?