{'fraction_non_alphanumeric': 0.0346533032000262, 'fraction_numerical': 0.009138252923258327, 'mean_word_length': 4.450196358443413, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 1, 'https://': 1, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Verification of the Incremental Merkle Tree Algorithm with Dafny

The Deposit Smart Contract (DSC) is an instrumental component of the Ethereum 2.0 Phase 0 infrastructure. We have developed the first machine-checkable version of the incremental Merkle tree algorithm used in the DSC. We present our new and original correctness proof of the algorithm along with the Dafny machine-checkable version. The main results are: 1) a new proof of total correctness; 2) a software artefact with the proof in the form of the complete Dafny code base and 3) new provably correct optimisations of the algorithm.


Introduction
Blockchain-based decentralised platforms process transactions between parties and record them in an immutable distributed ledger. Those platforms were once limited to handle simple transactions but the next generation of platforms will routinely run decentralised applications (DApps) that enable users to make complex transactions (sell a car, a house or more broadly, swap assets) without the need for an institutional or governmental trusted third-party.
Smart Contracts. More precisely, the transactions are programmatically performed by programs called smart contracts. If there are real advantages having smart contracts act as third-parties to process transactions, there are also lots of risks that are inherent to computer programs: they can contain bugs. Bugs can trigger runtime errors like division by zero or arrayout-of-bounds. In a networked environment these types of vulnerabilities can be exploited by malicious attackers over the network to disrupt or take control of the computer system. Other types of bugs can also compromise the business logic of a system, e.g., an implementation may contain subtle errors (e.g., using a += operator in C instead of =+) that make them deviate from the initial intended specifications.
Unfortunately it is extremely hard to guarantee that programs and henceforth smart contracts implement the correct business logics, that they are free of common runtime errors, or that they never run into a non-terminating computation. 1 There are notorious examples of smart contract vulnerabilities that have been exploited and publicly reported: in 2016, a reentrance vulnerability in the Decentralised Autonomous Organisation (DAO) smart contract was exploited to steal more than USD50 Million. There may be several non officially reported similar attacks that have resulted in the loss of assets. 1 In the Ethereum ecosystem, programs can only use a limited amount of resources, determined by the gas limit. So one could argue that non-terminating computations are not problematic as they cannot arise: when the gas limit is reached a computation is aborted and has no side effects. It follows that a non-terminating computation (say an infinite loop due to a programming error) combined with a finite gas limit will abort and will result in the system being unable to successfully process some or all valid transactions and this is a serious issue.
The Deposit Smart Contract in Ethereum 2.0. The next generation of Ethereumbased networks, Ethereum 2.0, features a new proof-of-stake consensus protocol. Instead of miners used in Ethereum 1.x, the new protocol relies on validators to create and validate blocks of transactions that are added to the ledger. The protocol is designed to be faulttolerant to up to 1/3 of Byzantine (i.e., malicious or dishonest) validators. To discourage validators to deviate from an honest behaviour, they have to stake some assets in Ether (a crypto-currency), and if they are dishonest they can be slashed and lose (part of) their stake. The process of staking is handled by the Deposit Smart Contract (DSC): a validator sends a transaction ("stake some Ether") by calling the DSC. The DSC has a state and can update/record the history of deposits that have occurred so far. As a result the DSC is a mission-critical component of Ethereum 2.0, and any errors/crashes could result in inaccurate tracking of the deposits or downtime which in turn may compromise the integrity/availability of the whole system. This could be mitigated if the DSC was a simple piece of code, but, for performance reasons, it relies on sophisticated data structures and algorithms to maintain the list of deposits so that they can be communicated over the network efficiently: the history of deposits is summarised as a unique number, a hash, computed using a Merkle (or Hash) tree. The tree is built incrementally using the incremental Merkle tree algorithm, and as stated in [21]: "The efficient incremental algorithm leads to the DSC implementation being unintuitive, and makes it non-trivial to ensure its correctness." Related Work. In this context, it is not surprising that substantial efforts, auditing, review [3], testing and formal verification [20,21] has been invested to guarantee the reliability and integrity (e.g., resilience to potential attacks) of the DSC. The DSC has been the focus of an end-to-end analysis [21], including the bytecode 2 that is executed on the Ethereum Virtual Machine (EVM). However, the incremental Merkle tree algorithm has not been mechanically verified yet, even though a pen and paper proof has been proposed [20] and partially mechanised using the K-framework [5]. An example of the limitations of the mechanised part of the proof in [20] is that it does not contain a formal (K-)definition of Merkle trees. The mechanised sections (lemmas 7 and 9) pertain to some invariants of the algorithm but not to a proper correctness specification based on Merkle trees. The K-framework and KEVM, the formalisation of the EVM in K, has been used to analyse a number of other smart contracts [25]. There are several techniques and tools 3 e.g., [8,9,1,6,28], for auditing and analysing smart contracts written in Solidity (a popular language to write Ethereum smart contracts) or EVM bytecode, but they offer limited capabilities to verify complex functional requirements.
Interesting properties of incremental Merkle trees were established in [19] using the MONA prover. This work does not prove the algorithms in the DSC which are designed to minimise gas consumption and hence split into parts: insert a value in a tree, and compute the root hash. Moreover, some key lemmas in the proofs could not be discharged by MONA.
The gold standard in program correctness is a complete logical proof that can be mechanically checked by a prover. This is the problem we address in this paper: to design a machinecheckable proof for the DSC algorithms (not the bytecode) using the Dafny language and verifier. The DSC has been deployed in November 2020. To the best of our knowledge, our analysis, completed in October 2020, provided the first fully mechanised proof that the code logic was correct, and free of runtime errors. There seem to be few comparable case-studies of Dafny-verified (or other verification-aware programming languages like Whiley [23]) code bases. The most notorious and complex one is probably the IronFleet/IronClad [10] distributed system, along with some non-trivial algorithms like DPPL [2] or Red-Black trees [24], or operating systems, FreeRTOS scheduler [16], and ExpressOS [15]. Other proof assistants like Coq [22], Isabelle/HOL [18] or Lean [17] have also been extensively used to write machinecheckable proofs of algorithms [12,27,7,26] and software systems [11,14].
Our Contribution. We present a thorough analysis of the incremental Merkle tree algorithm used in the DSC. Our results are available as software artefacts, written using the CAVawarded Dafny 4 verification-aware programming language [13]. This provides a self-contained machine checkable and reproducible proof of the DSC algorithms. Our contribution is manyfold and includes: a new original simple proof of the incremental Merkle tree algorithm. In contrast to the previous non-mechanised proof in [20] we do not attempt to directly prove the existing algorithm, but rather to design and refine it. Our proof is parametric in the height of the tree, and hash functions; a logical specification using a formal definition of Merkle trees, and a new functional version of the algorithm that is proved correct against this specification; the functional version is used to specify the invariants for the proof of the imperative original version [4] of the algorithm; a repository 5 with the complete Dafny source code of the specification, the algorithms and the proofs, and comprehensive documentation; some new provably correct simplifications/optimisations; some reflections on the practicality of using a verification-aware programming language like Dafny and some lessons learned from this experience.

Incremental Merkle Trees
Merkle Trees. A complete (or perfect) binary tree is such that each non-leaf node has exactly two children, and the two children have the same height. An example of a complete binary tree is given in Fig. 1. A Merkle (or hash) tree is a complete binary tree the nodes of which are decorated with hashes (fixed-size bit-vectors). The hash values of the leaves are given and the hash values of the internal (non-leaf) nodes are computed by combining the values of their children with a binary function hash. It follows that a Merkle tree is a complete binary tree decorated with a synthesised attribute defined by a binary function. Merkle trees are often used in distributed ledger systems to define a property of a collection of elements e.g., a list L of values. This property can then be used instead of the collection itself to verify, 6 using a mechanism called Merkle proofs, that data received from a node in the distributed system is not corrupted. This is a crucial optimisation as the size of the collection is usually large (typically up to 2 32 ) and using a compact representation is instrumental to obtain time and space efficient communication and a reasonable transactions' processing throughput.
In this work, we are not concerned with Merkle proofs but rather with the (efficient) computation of the hash attribute on a Merkle tree.
The actual function used to compute the values of the internal nodes is not relevant in the incremental Merkle tree algorithms' functional logics and without loss of generality we may treat it as a parameter i.e., a given binary function. 7 In the sequel we assume that the decorations of the nodes are integers, and we use in the examples a simple function hash : Int × Int −→ Int defined by hash(x, y) = x − y − 1 instead of an actual (e.g., sha256based) hash function. The Incremental Merkle Tree Problem. A typical use case of a Merkle tree in the context of Ethereum 2.0 is to represent properties of lists that grow monotonically. In the DSC, a Merkle tree is used to record the list of validators and their stakes or deposits. A compact representation of this list, as the root hash of a Merkle tree, is communicated to the nodes in the network rather than the tree (or list) itself. However, as mentioned before, each time a new deposit is appended to the list, computing the new root hash using a standard synthesised-attribute computation algorithm requires exponential time in h. This is clearly impractical in a distributed system like Ethereum in which the height of the tree is 32 and the number of nodes is 2 33 − 1.
Given (a tree height) h > 0, L a list with |L| < 2 h , and e a new element to add to L, the incremental Merkle tree problem (IMTP) is defined as follows: 9 Can we find α(L) a polynomial-space abstraction of T (L) such that we can compute in polynomial-time: 1) the root hash of T (L) from α(L), and 2) the abstraction α(L + [e]) from α(L) and e?
Linear-time/space algorithms to solve the IMTP were originally proposed by V. Buterin in [4]. However, the correctness of these algorithms is not obvious. In the next section, we analyse the IMTP, and we present the main properties that enable us to design polynomial-time recursive algorithms and to verify them.

Recursive Incremental Merkle Tree Algorithm
In this section we present the main ideas of the recursive algorithms to insert a new value in a Merkle tree and to compute the new root hash (after a new value in inserted) by re-using (dynamic programming) previously computed results. 7 In the code base, the hash function is uninterpreted and its type is generic. 8 The height is the length of the longest path from the root to any leaf. 9 Polynomial in the height of the tree h. The operator + is list concatenation.

Notations.
A path π from the root of a tree to a node can be defined as a sequence of bits (left or right) in {0, 1} * . In a Merkle tree of height h, the length, |π|, of π is at most h. ν(π) is the node at the end of π. If |π| = h then ν(π) is a leaf. For instance ν(ε) is the root of the tree, ν(0) in Fig. 1 is the node carrying the value −8 and ν(1.0.0) is a leaf. The right sibling of a left node of the form ν(π.0) is the node ν(π.1). Left siblings are defined symmetrically. A node in a Merkle tree is associated with a level which is the distance from the node to a leaf in the tree. Leaves are at level 0 and the root is at level h. In a Merkle tree, level 0 has 2 h leaves that can be indexed left to right from 0 to 2 h − 1. The n-th leaf of the tree for 0 ≤ n < 2 h is the leaf at index n. Given a path π, if the leaves on the right of ν(π) all have the default value 0, the values of the right siblings on the path π only depend on the level of the sibling in the tree. For example, the leaves on the right of π 1 (orange in Fig. 1) all have the default value 0. The root hash of a tree in which all the leaves have the same default value only depends on the level of the root: 0 at level 0, hash(0, 0) at level 1, hash(hash(0, 0), hash(0, 0)) at level 2 and so on. Let zero l be defined by: zero l = 0 if l = 0 else hash(zero l−1 0 , zero l−1 0 ). Given a path π, if all the leaves on the right of ν(π) have the default value, any right sibling value at level l on π is equal to zero l .
As an example in Fig. 1, the right siblings on π 1 = 1.0.0 have values 0 at level 0, node ν(1.0.1), and hash(0, 0) = zero 1 = −1 at level 1, node ν(1.1). If a path p leads to a node with the default value 0 and all the leaves right of ν(p) have the default value 0, the root hash depends only on the values of the left and default right siblings. Hence the root hash can be obtained by computeRootUp(p, left, right, 0). For the path pi2 = [1, 0, 1] (Fig. 1 As a result, to compute the root hash of a tree T (L), we can use a compact abstraction α(L) of T (L) composed of the left siblings vector b and the right siblings default values z ( Fig. 1) of the path to the |L|-th leaf in T (L).
Insertion: Update the Left Siblings. Assume π 1 is a path to the n-th leaf and n < 2 h −1 (not the last leaf), where the next value v is to be inserted. As we have shown before, if we have b 1 holding the values of left siblings of π 1 , z and v, we can compute the new attribute values of the nodes on π 1 and the new root hash after v is inserted. Let π 2 be the path to the n + 1-th leaf. If we can compute the values b 2 of the left siblings of π 2 as a function of b 1 , z and v, we have an efficient algorithm to incrementally compute the root hash of a Merkle tree: we keep track of the values of the left siblings b on the path to the next available leaf, and iterate this process each time a new value is inserted.
The related forms of π 1 (a path) and π 2 (the successor path) are useful to figure out how to incrementally compute the left siblings vector b 2 for π 2 : as the initial prefix w is the same in π 1 and π 2 , the values of the left siblings on the nodes of w are the same in b 1 and b 2 ; all the nodes in the suffix 0 k of π 2 are left nodes and have right siblings. It follows that the corresponding k values in b 2 are irrelevant as they correspond to right siblings, and we can re-use the corresponding b 1 values; hence b 2 is equal to b 1 except possibly for the level of the node at ν(w.0).  In the next section we describe how to verify the recursive algorithms and the versions implemented in the DSC.

Verification of the Algorithms
In order to verify the implemented (imperative style/Solidity) versions of the algorithms of the DSC, we first prove total correctness of the recursive versions (Section 3) and them use them to prove the code implemented in the DSC.
In this section, the Dafny code has been simplified and sometimes even altered while retaining the main features, for the sake of clarity. The code in this section may not compile. We provide the links to the files with the full code in the text and refer the reader to those files.
Correctness Specification. The (partial) correctness of our algorithms reduces to checking that they compute the same values as the ones obtained with a synthesised attribute on a Merkle tree. We have specified the data types Tree, MerkleTree and CompleteTrees and the relation between Merkle trees and lists of values (see trees folder.) The root hash of a MerkleTree t is t.rootv. The (specification) function buildMerkle(h, L, hash) returns a MerkleTree of height h, the leaves of which are given by the values (right-padded) L, and the values on the internal nodes agree with the definition of the synthesised attribute hash, i.e., what we previously defined in Section 2 as T (L). It follows that buildMerkle(h, L, hash).rootv is the root hash of a Merkle tree with leaves L. Total Correctness. The total correctness proof for the computeRootUp function amounts to showing that 1) the algorithm always terminates and 2) the result of the computation is the same as the hash of the root of the tree. In Dafny, to prove termination, we need to provide a ranking function (strictly decreasing and bounded from below.) The length of the path p is a suitable ranking function (see the decreases clause in Listing A.1) and is enough for Dafny to prove termination of computeRootUp.
We establish property 2) by proving a lemma (Listing A.3): the pre-conditions (requires) of the lemma are the assumptions, and the post-conditions (ensures) the intended property. The body of the lemma (with a non-interpreted hash function) which provides the machinecheckable proof is available in the computeRootPath.dfy file. This lemma requires that the tree r is a Merkle tree, and that the lists left (resp. right) store the values of left (resp. right) siblings of the nodes on a path p. Moreover, the value at the end of p should be seed. Under these assumptions the conclusion (ensures) is that computeRootUp returns the value of the root hash of r. The proof of lemma computeRootUpIsCorrectForTree requires a few intermediate sub-lemmas of moderate difficulty. The main step in the proof is to establish an equivalence between a bottom-up computation computeRootUp and the top-down definition of (attributed) Merkle trees. All the proofs are by induction on the tree or the path. The complete Dafny code for algorithm is available in computeRootPath.dfy file.
Termination for insertValue is proved by using a ranking function (decreases clause in Listing ]A.2). The functional correctness of insertValue reduces to proving that, assuming left (resp. right) contains the values of the left (resp. right) siblings of the nodes on p, then insertValue(p, left, right, seed) returns the values of the nodes that are left siblings on the successor path. The specification of the corresponding lemma is given in Listing A.4. The code for this lemma is in the NextPathInCompleteTreesLemmas.dfy file. The main proof is based on several sub-lemmas that are not hard conceptually but cannot be easily discharged using solely the built-in Dafny induction strategies. They require some intermediate proof hints (verified calculations) to deal with all the nodes on the path p. Note that for this lemma, we require that the leaves are indexed (from left to right) to be able to uniquely identify each leaf of r. Index Based Algorithms. The algorithms that implement the DSC do not use a bitvector to encode a path, but rather, a counter that records the number of values inserted so far and the height of the tree. In order to prove the algorithms actually implemented in the DSC, we first recast the computeRootUp and insertValue algorithms to use a counter and the height h of a tree. In this step, we use a parameter k that is the index of the next available leaf where a new value can be inserted. The leaves are indexed left to right from 0 to 2 h − 1 and hence k is the number of values that have been inserted so far. It follows that the leaves with indices k ≤ i ≤ 2 h − 1 have the default value. The correspondence between the bitvector encoding of the path to the leaf at index k and the value k is straightforward: the encoding of the path p is the value of k in binary over h bits. We can rewrite left computeRootUp to use use k and h (computeRootUpWithIndex, Listing A.5) and prove it computes the same value as computeRootUp. A similar proof can be established for the insertValue algorithm. The index based algorithms and the proofs that they are equivalent (compute the same values as) to computeRootUp and insertValue are available in the IndexBasedAlgorithm.dfy file. Dafny can discharge the equivalence proofs with minimal proof hints using the builtin induction strategies.
Listing A.5. ComputeRootUpWithIndex. Total Correctness of the Algorithms Implemented in the DSC. In this section we present the final proof of (total) correctness for the algorithms implemented in the DSC (Solidity-like version.) Our proof establishes that the imperative versions, with while loops and dynamic memory allocation (for arrays) are correct, terminate and are memory safe.
The DSC is an object and has a state defined by a few variables: count is the number of inserted values (initially zero), branch is a vector that stores that value of the left siblings of the path leading to the leaf at index count, and zero hashes is what we previously defined as z. The algorithm that computes the root hash of the Merkle tree in the DSC is get deposit root(). get deposit root() does not have any seed parameter as it computes the root hash using the default value (0). The correctness proof of get deposit root() uses the functional (proved correct) algorithm computeRootUpWithIndex as an invariant. Listing A.6 is a simplified version (for clarity) of the full code available in the DepositSmart.dfy file.
Listing A.7. The deposit method. The algorithm that inserts a value v in the tree is deposit(v) in the implemented version of the DSC. Listing A.7 is an optimised version of the original algorithm. The simplification is explained in Section 5. The correctness of the algorithm is defined by ensuring that, if at the beginning of the computation the vectors branch (resp, zero hashes) contain values of the left (resp. right) siblings of the path leading to the leaf at index count, then at the end of the computation, after v is inserted, this property still holds. The proof of this invariant requires a number of proof hints for Dafny to verify it. We use the functional version of the algorithm to specify a loop invariant (not provided in Listing A.7).
The termination proof is easy using size as the decreasing ranking function. However, a difficulty in this proof is memory safety, i.e. to guarantee that the index i used to access branch[i] is within the range of the indices of branch.
We have also proved the initialisation functions init zero hashes() and constructor. The full code of the imperative version of the DSC is available in the DepositSmart.dfy file.

Findings and Lessons Learned
Methodology. In contrast to the previous attempts to analyse the DSC, we have adopted a textbook approach and used standard algorithms' design techniques (e.g., dynamic programming, refinement, recursion.) This has several advantages over a direct proof (e.g., [20]) of the imperative code including: the design of simple algorithms and proofs; recursive and language-agnostic recursive versions of the algorithms; new and provably correct simplifications/optimisations. Algorithmic Considerations. Our implementations and formal proofs have resulted in the identification of two previously unknown/unconfirmed optimisations. First, it is not necessary to initialise the vector of left siblings, b, and the algorithms are correct for any initial value of this vector.
Second, the original version of the deposit algorithm (which we have proved correct too) has the form 13 given in Listing A.8. Our formal machine-checkable proof revealed 14 that indeed the condition C1 is always true and the loop always terminates because C2 eventually becomes true. As witnessed by the comment after the loop in the Solidity code of the DSC, this property was expected but not confirmed, and the Solidity contract authors did not take the risk to simplify the code. Our result shows that the algorithm can be simplified to while not(C2) do ... od. w h i l e C1 do i f C2 r e t u r n ; . . . od // As the loop should always end prematurely with the 'return ' statement , // this code should be unreachable . We assert 'false ' just to be safe . a s s e r t ( f a l s e ) ; } This is interesting not only from a safety and algorithmic perspectives, but also because it reduces the computation cost (in gas/Ether) of executing the deposit method. This simplification proposal is currently being discussed with the DSC developer, however the currently deployed version still uses the non-optimised code.
Verification Effort. The verification effort for this project is 12 person-weeks resulting in 3500 lines of code and 1000 lines of documentation. This assumes familiarity with program verification, Hoare logic and Dafny. Table 1, page 14 provides some insights into the code base.
The filenames in green are the ones that require the less number of hints for Dafny to check a proof. In this set of files the hints mostly consist of simple verified calculations (e.g., empty sequence is a neutral element for lists [] + l == l + [] == l.) Most of the results on sequences (helpers package) and simplifications of sequences of bits (seqofbits package) are in this category and require very few hints. This also applies for the proofs 15 of the algorithms package, e.g., proving that the versions using the index of a leaf instead of the binary encoding of a path are equivalent.
The filenames in orange require some non-trivial proof hints beyond the implicit induction strategies built in Dafny. For instance in NextPathInCompleteTrees.dfy and PathInComplete-Trees.dfy, we had to provide several annotations and structure for the proofs. This is due to the fact that the proofs involve properties on a Merkle tree t 1 and its successor t 2 (after a value is inserted) which is a new tree, and on a path π 1 in t 1 and its successor π 2 in t 2 .
The filenames in red require a lot of hints. For the files in the synthattribute package it is mostly calculation steps. Some steps are not absolutely necessary but adding them reduces the verification time by on order of magnitude (on our system configuration, MacBookPro 16GBRAM). The hardest proof is probably the correctness of the deposit method in De-positSmart.dfy. The proof requires non trivial lemmas and invariants. The difficulty stems from a combination of factors: first the while loop of the algorithm (Listing A.7) maintains a constraint between size and i, the latter being used to access the array elements in branch.
Proving that there is no array-of-bounds error (i.e., i is within the size of branch) requires to prove some arithmetic properties. Second, the proof of the main invariant (Listing A.7) using the functional specification computeLeftSiblingsOnNextpathWithIndex is complex and had to be structured around additional lemmas.
Overall, almost 90% of the lines of code are (non-executable) proofs, and function definitions used in the proofs. The verified algorithms implemented in the DSC functional are provided in DepositSmart.dfy and account for less than 10% of the code.
Considering the criticality of the DSC, 12 person-weeks can be considered a moderate effort well worth the investment: the result is an unparalleled level of trustworthiness that can inspire confidence in the Ethereum platform. According to our experts (ConsenSys Diligence) in the verification of Smart Contracts, the size of such an effort is realistic and practical considering the level of guarantees provided. The only downside is the level of verification expertise required to design the proofs.
The trust base in our work is composed of the Dafny verification engine (verification conditions generator) and the SMT-solver Z3.
Dafny Experience. Dafny is rather has excellent documentation, support for data structures, functional (side-effect free) and object-oriented programming. The automated verification engine has a lot of built-in strategies (e.g., induction, calculations) and a good number of specifications are proved fully automatically without providing any hints. The Dafny proof strategies and constructs that we mostly used are verified calculations and induction. The 15 The file CommuteProof.dfy in this package is not needed for the main proof but was originally used and provides an interesting result, so it is still in code base. side-effect free proofs seem to be handled much more efficiently (time-wise) than the proofs using mutable data structures.
In the current version we have used the autocontracts attribute for the DSC object which is a convenient way of proving memory safety using a specific invariant (given by the Valid predicate). This could probably be optimised as Dafny has some support to specify precisely the side-effects using frames (based on dynamic framing.) Overall, Dafny is a practical option for the verification of mission-critical smart contracts, and a possible avenue for adoption could be to extend the Dafny code generator engine to support Solidity, a popular language for writing smart contracts for the Ethereum network, or to automatically translate Solidity into Dafny. We are currently evaluating these options with our colleagues at ConsenSys Diligence, as well as the benefits of our technique to the analysis of other critical smart contracts.
The software artefacts including the implementations, proofs, documentation and a Docker container to reproduce the results are freely available as a GitHub repository at https://github. com/ConsenSys/deposit-sc-dafny.