Merge pull request #1152 from ethereum/deposit-contract-justin

Custom genesis trigger, and deposit contract cleanups
This commit is contained in:
Danny Ryan 2019-06-12 10:54:11 -06:00 committed by GitHub
commit 12293a91b4
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
6 changed files with 94 additions and 248 deletions

File diff suppressed because one or more lines are too long

View File

@ -1,140 +1,103 @@
MIN_DEPOSIT_AMOUNT: constant(uint256) = 1000000000 # Gwei
FULL_DEPOSIT_AMOUNT: constant(uint256) = 32000000000 # Gwei
CHAIN_START_FULL_DEPOSIT_THRESHOLD: constant(uint256) = 65536 # 2**16
DEPOSIT_CONTRACT_TREE_DEPTH: constant(uint256) = 32
SECONDS_PER_DAY: constant(uint256) = 86400
MAX_64_BIT_VALUE: constant(uint256) = 18446744073709551615 # 2**64 - 1
MAX_DEPOSIT_COUNT: constant(uint256) = 4294967295 # 2**DEPOSIT_CONTRACT_TREE_DEPTH - 1
PUBKEY_LENGTH: constant(uint256) = 48 # bytes
WITHDRAWAL_CREDENTIALS_LENGTH: constant(uint256) = 32 # bytes
AMOUNT_LENGTH: constant(uint256) = 8 # bytes
SIGNATURE_LENGTH: constant(uint256) = 96 # bytes
MAX_DEPOSIT_COUNT: constant(uint256) = 4294967295 # 2**DEPOSIT_CONTRACT_TREE_DEPTH - 1
Deposit: event({
pubkey: bytes[48],
withdrawal_credentials: bytes[32],
amount: bytes[8],
signature: bytes[96],
merkle_tree_index: bytes[8],
index: bytes[8],
})
Eth2Genesis: event({deposit_root: bytes32, deposit_count: bytes[8], time: bytes[8]})
zerohashes: bytes32[DEPOSIT_CONTRACT_TREE_DEPTH]
branch: bytes32[DEPOSIT_CONTRACT_TREE_DEPTH]
deposit_count: uint256
full_deposit_count: uint256
chainStarted: public(bool)
# Compute hashes in empty sparse Merkle tree
zero_hashes: bytes32[DEPOSIT_CONTRACT_TREE_DEPTH]
@public
def __init__():
for i in range(DEPOSIT_CONTRACT_TREE_DEPTH - 1):
self.zerohashes[i+1] = sha256(concat(self.zerohashes[i], self.zerohashes[i]))
self.zero_hashes[i + 1] = sha256(concat(self.zero_hashes[i], self.zero_hashes[i]))
@public
@private
@constant
def to_little_endian_64(value: uint256) -> bytes[8]:
assert value <= MAX_64_BIT_VALUE
# array access for bytes[] not currently supported in vyper so
# reversing bytes using bitwise uint256 manipulations
# Reversing bytes using bitwise uint256 manipulations
# Note: array accesses of bytes[] are not currently supported in Vyper
# Note: this function is only called when `value < 2**64`
y: uint256 = 0
x: uint256 = value
for i in range(8):
for _ in range(8):
y = shift(y, 8)
y = y + bitwise_and(x, 255)
x = shift(x, -8)
return slice(convert(y, bytes32), start=24, len=8)
@public
@constant
def get_deposit_root() -> bytes32:
root: bytes32 = 0x0000000000000000000000000000000000000000000000000000000000000000
node: bytes32 = 0x0000000000000000000000000000000000000000000000000000000000000000
size: uint256 = self.deposit_count
for h in range(DEPOSIT_CONTRACT_TREE_DEPTH):
if bitwise_and(size, 1) == 1:
root = sha256(concat(self.branch[h], root))
for height in range(DEPOSIT_CONTRACT_TREE_DEPTH):
if bitwise_and(size, 1) == 1: # More gas efficient than `size % 2 == 1`
node = sha256(concat(self.branch[height], node))
else:
root = sha256(concat(root, self.zerohashes[h]))
node = sha256(concat(node, self.zero_hashes[height]))
size /= 2
return root
return node
@public
@constant
def get_deposit_count() -> bytes[8]:
return self.to_little_endian_64(self.deposit_count)
@payable
@public
def deposit(pubkey: bytes[PUBKEY_LENGTH],
withdrawal_credentials: bytes[WITHDRAWAL_CREDENTIALS_LENGTH],
signature: bytes[SIGNATURE_LENGTH]):
# Prevent edge case in computing `self.branch` when `self.deposit_count == MAX_DEPOSIT_COUNT`
# NOTE: reaching this point with the constants as currently defined is impossible due to the
# uni-directional nature of transfers from eth1 to eth2 and the total ether supply (< 130M).
# Avoid overflowing the Merkle tree (and prevent edge case in computing `self.branch`)
assert self.deposit_count < MAX_DEPOSIT_COUNT
# Validate deposit data
deposit_amount: uint256 = msg.value / as_wei_value(1, "gwei")
assert deposit_amount >= MIN_DEPOSIT_AMOUNT
assert len(pubkey) == PUBKEY_LENGTH
assert len(withdrawal_credentials) == WITHDRAWAL_CREDENTIALS_LENGTH
assert len(signature) == SIGNATURE_LENGTH
deposit_amount: uint256 = msg.value / as_wei_value(1, "gwei")
assert deposit_amount >= MIN_DEPOSIT_AMOUNT
# Emit `Deposit` log
amount: bytes[8] = self.to_little_endian_64(deposit_amount)
log.Deposit(pubkey, withdrawal_credentials, amount, signature, self.to_little_endian_64(self.deposit_count))
index: uint256 = self.deposit_count
# add deposit to merkle tree
i: int128 = 0
size: uint256 = index + 1
for _ in range(DEPOSIT_CONTRACT_TREE_DEPTH):
if bitwise_and(size, 1) == 1:
break
i += 1
size /= 2
zero_bytes_32: bytes32
pubkey_root: bytes32 = sha256(concat(pubkey, slice(zero_bytes_32, start=0, len=16)))
# Compute `DepositData` root
zero_bytes32: bytes32 = 0x0000000000000000000000000000000000000000000000000000000000000000
pubkey_root: bytes32 = sha256(concat(pubkey, slice(zero_bytes32, start=0, len=64 - PUBKEY_LENGTH)))
signature_root: bytes32 = sha256(concat(
sha256(slice(signature, start=0, len=64)),
sha256(concat(slice(signature, start=64, len=32), zero_bytes_32))
sha256(concat(slice(signature, start=64, len=SIGNATURE_LENGTH - 64), zero_bytes32)),
))
value: bytes32 = sha256(concat(
node: bytes32 = sha256(concat(
sha256(concat(pubkey_root, withdrawal_credentials)),
sha256(concat(
amount,
slice(zero_bytes_32, start=0, len=24),
signature_root,
sha256(concat(amount, slice(zero_bytes32, start=0, len=32 - AMOUNT_LENGTH), signature_root)),
))
))
for j in range(DEPOSIT_CONTRACT_TREE_DEPTH):
if j < i:
value = sha256(concat(self.branch[j], value))
else:
break
self.branch[i] = value
# Add `DepositData` root to Merkle tree (update a single `branch` node)
self.deposit_count += 1
log.Deposit(
pubkey,
withdrawal_credentials,
amount,
signature,
self.to_little_endian_64(index),
)
size: uint256 = self.deposit_count
for height in range(DEPOSIT_CONTRACT_TREE_DEPTH):
if bitwise_and(size, 1) == 1: # More gas efficient than `size % 2 == 1`
self.branch[height] = node
break
node = sha256(concat(self.branch[height], node))
size /= 2
if deposit_amount >= FULL_DEPOSIT_AMOUNT:
self.full_deposit_count += 1
if self.full_deposit_count == CHAIN_START_FULL_DEPOSIT_THRESHOLD:
timestamp_day_boundary: uint256 = (
as_unitless_number(block.timestamp) -
as_unitless_number(block.timestamp) % SECONDS_PER_DAY +
2 * SECONDS_PER_DAY
)
new_deposit_root: bytes32 = self.get_deposit_root()
log.Eth2Genesis(new_deposit_root,
self.to_little_endian_64(self.deposit_count),
self.to_little_endian_64(timestamp_day_boundary))
self.chainStarted = True

View File

@ -26,7 +26,6 @@ from .utils import (
# Constants
MIN_DEPOSIT_AMOUNT = 1000000000 # Gwei
FULL_DEPOSIT_AMOUNT = 32000000000 # Gwei
CHAIN_START_FULL_DEPOSIT_THRESHOLD = 65536 # 2**16
DEPOSIT_CONTRACT_TREE_DEPTH = 32
TWO_TO_POWER_OF_TREE_DEPTH = 2**DEPOSIT_CONTRACT_TREE_DEPTH
@ -63,45 +62,6 @@ def registration_contract(w3, tester):
return registration_deployed
@pytest.fixture(scope="session")
def chain_start_full_deposit_thresholds():
return [randint(1, 5), randint(6, 10), randint(11, 15)]
@pytest.fixture(params=[0, 1, 2])
def modified_registration_contract(
request,
w3,
tester,
chain_start_full_deposit_thresholds):
# Set CHAIN_START_FULL_DEPOSIT_THRESHOLD to different threshold t
registration_code = get_deposit_contract_code()
t = str(chain_start_full_deposit_thresholds[request.param])
modified_registration_code = re.sub(
r'CHAIN_START_FULL_DEPOSIT_THRESHOLD: constant\(uint256\) = [0-9]+',
'CHAIN_START_FULL_DEPOSIT_THRESHOLD: constant(uint256) = ' + t,
registration_code,
)
assert modified_registration_code != registration_code
contract_bytecode = compiler.compile_code(modified_registration_code)['bytecode']
contract_abi = compiler.mk_full_signature(modified_registration_code)
registration = w3.eth.contract(
abi=contract_abi,
bytecode=contract_bytecode)
tx_hash = registration.constructor().transact()
tx_receipt = w3.eth.waitForTransactionReceipt(tx_hash)
registration_deployed = w3.eth.contract(
address=tx_receipt.contractAddress,
abi=contract_abi
)
setattr(
registration_deployed,
'chain_start_full_deposit_threshold',
chain_start_full_deposit_thresholds[request.param]
)
return registration_deployed
@pytest.fixture
def assert_tx_failed(tester):
def assert_tx_failed(function_to_test, exception=eth_tester.exceptions.TransactionFailed):

View File

@ -49,28 +49,6 @@ def deposit_input():
)
@pytest.mark.parametrize(
'value,success',
[
(0, True),
(10, True),
(55555, True),
(2**64 - 1, True),
(2**64, False),
]
)
def test_to_little_endian_64(registration_contract, value, success, assert_tx_failed):
call = registration_contract.functions.to_little_endian_64(value)
if success:
little_endian_64 = call.call()
assert little_endian_64 == (value).to_bytes(8, 'little')
else:
assert_tx_failed(
lambda: call.call()
)
@pytest.mark.parametrize(
'success,deposit_amount',
[
@ -151,8 +129,7 @@ def test_deposit_log(registration_contract, a0, w3, deposit_input):
assert log['withdrawal_credentials'] == deposit_input[1]
assert log['amount'] == deposit_amount_list[i].to_bytes(8, 'little')
assert log['signature'] == deposit_input[2]
assert log['merkle_tree_index'] == i.to_bytes(8, 'little')
assert log['index'] == i.to_bytes(8, 'little')
def test_deposit_tree(registration_contract, w3, assert_tx_failed, deposit_input):
log_filter = registration_contract.events.Deposit.createFilter(
@ -172,7 +149,7 @@ def test_deposit_tree(registration_contract, w3, assert_tx_failed, deposit_input
assert len(logs) == 1
log = logs[0]['args']
assert log["merkle_tree_index"] == i.to_bytes(8, 'little')
assert log["index"] == i.to_bytes(8, 'little')
deposit_data = DepositData(
pubkey=deposit_input[0],
@ -184,53 +161,3 @@ def test_deposit_tree(registration_contract, w3, assert_tx_failed, deposit_input
leaf_nodes.append(hash_tree_root_result)
root = compute_merkle_root(leaf_nodes)
assert root == registration_contract.functions.get_deposit_root().call()
def test_chain_start(modified_registration_contract, w3, assert_tx_failed, deposit_input):
t = getattr(modified_registration_contract, 'chain_start_full_deposit_threshold')
# CHAIN_START_FULL_DEPOSIT_THRESHOLD is set to t
min_deposit_amount = MIN_DEPOSIT_AMOUNT * eth_utils.denoms.gwei # in wei
full_deposit_amount = FULL_DEPOSIT_AMOUNT * eth_utils.denoms.gwei
log_filter = modified_registration_contract.events.Eth2Genesis.createFilter(
fromBlock='latest',
)
index_not_full_deposit = randint(0, t - 1)
for i in range(t):
if i == index_not_full_deposit:
# Deposit with value below FULL_DEPOSIT_AMOUNT
modified_registration_contract.functions.deposit(
*deposit_input,
).transact({"value": min_deposit_amount})
logs = log_filter.get_new_entries()
# Eth2Genesis event should not be triggered
assert len(logs) == 0
else:
# Deposit with value FULL_DEPOSIT_AMOUNT
modified_registration_contract.functions.deposit(
*deposit_input,
).transact({"value": full_deposit_amount})
logs = log_filter.get_new_entries()
# Eth2Genesis event should not be triggered
assert len(logs) == 0
# Make 1 more deposit with value FULL_DEPOSIT_AMOUNT to trigger Eth2Genesis event
modified_registration_contract.functions.deposit(
*deposit_input,
).transact({"value": full_deposit_amount})
logs = log_filter.get_new_entries()
assert len(logs) == 1
timestamp = int(w3.eth.getBlock(w3.eth.blockNumber)['timestamp'])
timestamp_day_boundary = timestamp + (86400 - timestamp % 86400) + 86400
log = logs[0]['args']
assert log['deposit_root'] == modified_registration_contract.functions.get_deposit_root().call()
assert int.from_bytes(log['time'], byteorder='little') == timestamp_day_boundary
assert modified_registration_contract.functions.chainStarted().call() is True
# Make 1 deposit with value FULL_DEPOSIT_AMOUNT and
# check that Eth2Genesis event is not triggered
modified_registration_contract.functions.deposit(
*deposit_input,
).transact({"value": full_deposit_amount})
logs = log_filter.get_new_entries()
assert len(logs) == 0

View File

@ -95,7 +95,7 @@
- [`initiate_validator_exit`](#initiate_validator_exit)
- [`slash_validator`](#slash_validator)
- [Genesis](#genesis)
- [`Eth2Genesis`](#eth2genesis)
- [Genesis trigger](#genesis-trigger)
- [Genesis state](#genesis-state)
- [Genesis block](#genesis-block)
- [Beacon chain state transition function](#beacon-chain-state-transition-function)
@ -370,12 +370,12 @@ class PendingAttestation(Container):
```python
class Eth1Data(Container):
# Block hash
block_hash: Bytes32
# Root of the deposit tree
deposit_root: Bytes32
# Total number of deposits
deposit_count: uint64
# Block hash
block_hash: Bytes32
```
#### `HistoricalBatch`
@ -1156,20 +1156,45 @@ def slash_validator(state: BeaconState,
## Genesis
### `Eth2Genesis`
### Genesis trigger
When enough deposits of size `MAX_EFFECTIVE_BALANCE` have been made to the deposit contract an `Eth2Genesis` log is emitted triggering the genesis of the beacon chain. Let:
Before genesis has been triggered and whenever the deposit contract emits a `Deposit`, log call the function `is_genesis_trigger(deposits: List[Deposit], timestamp: uint64) -> bool` where:
* `eth2genesis` be the object corresponding to `Eth2Genesis`
* `genesis_eth1_data` be object of type `Eth1Data` where
* `genesis_eth1_data.deposit_root = eth2genesis.deposit_root`
* `genesis_eth1_data.deposit_count = eth2genesis.deposit_count`
* `genesis_eth1_data.block_hash` is the hash of the Ethereum 1.0 block that emitted the `Eth2Genesis` log
* `genesis_deposits` be the object of type `List[Deposit]` with deposits ordered chronologically up to and including the deposit that triggered the `Eth2Genesis` log
* `deposits` is the list of all deposits, ordered chronologically, up to and including the deposit triggering the latest `Deposit` log
* `timestamp` is the Unix timestamp in the Ethereum 1.0 block that emitted the latest `Deposit` log
When `is_genesis_trigger(deposits, timestamp) is True` for the first time let:
* `genesis_deposits = deposits`
* `genesis_time = timestamp - timestamp % SECONDS_PER_DAY + 2 * SECONDS_PER_DAY` where `SECONDS_PER_DAY = 86400`
* `genesis_eth1_data` be the object of type `Eth1Data` where:
* `genesis_eth1_data.block_hash` is the Ethereum 1.0 block hash that emitted the log for the last deposit in `deposits`
* `genesis_eth1_data.deposit_root` is the deposit root for the last deposit in `deposits`
* `genesis_eth1_data.deposit_count = len(genesis_deposits)`
*Note*: The function `is_genesis_trigger` has yet to be agreed by the community, and can be updated as necessary. We define the following testing placeholder:
```python
def is_genesis_trigger(deposits: List[Deposit], timestamp: uint64) -> bool:
# Process deposits
state = BeaconState()
for deposit in deposits:
process_deposit(state, deposit)
# Count active validators at genesis
active_validator_count = 0
for validator in state.validator_registry:
if validator.effective_balance == MAX_EFFECTIVE_BALANCE:
active_validator_count += 1
# Check effective balance to trigger genesis
GENESIS_ACTIVE_VALIDATOR_COUNT = 2**16
return active_validator_count == GENESIS_ACTIVE_VALIDATOR_COUNT
```
### Genesis state
Let `genesis_state = get_genesis_beacon_state(genesis_deposits, eth2genesis.genesis_time, genesis_eth1_data)`.
Let `genesis_state = get_genesis_beacon_state(genesis_deposits, genesis_time, genesis_eth1_data)`.
```python
def get_genesis_beacon_state(deposits: List[Deposit], genesis_time: int, genesis_eth1_data: Eth1Data) -> BeaconState:
@ -1246,7 +1271,7 @@ def process_slot(state: BeaconState) -> None:
### Epoch processing
Note: the `# @LabelHere` lines below are placeholders to show that code will be inserted here in a future phase.
*Note*: the `# @LabelHere` lines below are placeholders to show that code will be inserted here in a future phase.
```python
def process_epoch(state: BeaconState) -> None:

View File

@ -9,15 +9,12 @@
- [Table of contents](#table-of-contents)
- [Introduction](#introduction)
- [Constants](#constants)
- [Gwei values](#gwei-values)
- [Contract](#contract)
- [Ethereum 1.0 deposit contract](#ethereum-10-deposit-contract)
- [Arguments](#arguments)
- [`deposit` function](#deposit-function)
- [Deposit amount](#deposit-amount)
- [Withdrawal credentials](#withdrawal-credentials)
- [Amount](#amount)
- [Event logs](#event-logs)
- [`Deposit` logs](#deposit-logs)
- [`Eth2Genesis` log](#eth2genesis-log)
- [`Deposit` log](#deposit-log)
- [Vyper code](#vyper-code)
<!-- /TOC -->
@ -28,66 +25,40 @@ This document represents the specification for the beacon chain deposit contract
## Constants
### Gwei values
| Name | Value | Unit |
| - | - | - |
| `FULL_DEPOSIT_AMOUNT` | `32 * 10**9` | Gwei |
### Contract
| Name | Value |
| - | - |
| `DEPOSIT_CONTRACT_ADDRESS` | **TBD** |
| `DEPOSIT_CONTRACT_TREE_DEPTH` | `2**5` (= 32) |
| `CHAIN_START_FULL_DEPOSIT_THRESHOLD` | `2**16` (= 65,536) |
## Ethereum 1.0 deposit contract
The initial deployment phases of Ethereum 2.0 are implemented without consensus changes to Ethereum 1.0. A deposit contract at address `DEPOSIT_CONTRACT_ADDRESS` is added to Ethereum 1.0 for deposits of ETH to the beacon chain. Validator balances will be withdrawable to the shards in Phase 2 (i.e. when the EVM 2.0 is deployed and the shards have state).
### Arguments
### `deposit` function
The deposit contract has a `deposit` function which takes the amount in Ethereum 1.0 transaction, and arguments `pubkey: bytes[48], withdrawal_credentials: bytes[32], signature: bytes[96]` corresponding to `DepositData`.
The deposit contract has a public `deposit` function to make deposits. It takes as arguments `pubkey: bytes[48], withdrawal_credentials: bytes[32], signature: bytes[96]` corresponding to a `DepositData` object.
#### Deposit amount
The amount of ETH (rounded down to the closest Gwei) sent to the deposit contract is the deposit amount, which must be of size at least `MIN_DEPOSIT_AMOUNT` Gwei. Note that ETH consumed by the deposit contract is no longer usable on Ethereum 1.0.
#### Withdrawal credentials
One of the `DepositData` fields is `withdrawal_credentials`. It is a commitment to credentials for withdrawals to shards. The first byte of `withdrawal_credentials` is a version number. As of now, the only expected format is as follows:
One of the `DepositData` fields is `withdrawal_credentials`. It is a commitment to credentials for withdrawing validator balance (e.g. to another validator, or to shards). The first byte of `withdrawal_credentials` is a version number. As of now, the only expected format is as follows:
* `withdrawal_credentials[:1] == BLS_WITHDRAWAL_PREFIX_BYTE`
* `withdrawal_credentials[1:] == hash(withdrawal_pubkey)[1:]` where `withdrawal_pubkey` is a BLS pubkey
The private key corresponding to `withdrawal_pubkey` will be required to initiate a withdrawal. It can be stored separately until a withdrawal is required, e.g. in cold storage.
#### Amount
#### `Deposit` log
* A valid deposit amount should be at least `MIN_DEPOSIT_AMOUNT` in Gwei.
* A deposit with an amount greater than or equal to `FULL_DEPOSIT_AMOUNT` in Gwei is considered as a full deposit.
## Event logs
### `Deposit` logs
Every Ethereum 1.0 deposit, of size at least `MIN_DEPOSIT_AMOUNT`, emits a `Deposit` log for consumption by the beacon chain. The deposit contract does little validation, pushing most of the validator onboarding logic to the beacon chain. In particular, the proof of possession (a BLS12-381 signature) is not verified by the deposit contract.
### `Eth2Genesis` log
When `CHAIN_START_FULL_DEPOSIT_THRESHOLD` of full deposits have been made, the deposit contract emits the `Eth2Genesis` log. The beacon chain state may then be initialized by calling the `get_genesis_beacon_state` function (defined [here](./0_beacon-chain.md#genesis-state)) where:
* `genesis_time` equals `time` in the `Eth2Genesis` log
* `latest_eth1_data.deposit_root` equals `deposit_root` in the `Eth2Genesis` log
* `latest_eth1_data.deposit_count` equals `deposit_count` in the `Eth2Genesis` log
* `latest_eth1_data.block_hash` equals the hash of the block that included the log
* `genesis_validator_deposits` is a list of `Deposit` objects built according to the `Deposit` logs up to the deposit that triggered the `Eth2Genesis` log, processed in the order in which they were emitted (oldest to newest)
Every Ethereum 1.0 deposit emits a `Deposit` log for consumption by the beacon chain. The deposit contract does little validation, pushing most of the validator onboarding logic to the beacon chain. In particular, the proof of possession (a BLS12-381 signature) is not verified by the deposit contract.
## Vyper code
The source for the Vyper contract lives [here](./../../deposit_contract/contracts/validator_registration.v.py).
The deposit contract source code, written in Vyper, is available [here](https://github.com/ethereum/eth2.0-specs/blob/dev/deposit_contract/contracts/validator_registration.v.py).
*Note*: To save ~10x on gas, this contract uses a somewhat unintuitive progressive Merkle root calculation algo that requires only O(log(n)) storage. See https://github.com/ethereum/research/blob/master/beacon_chain_impl/progressive_merkle_tree.py for an implementation of the same algo in Python tested for correctness.
For convenience, we provide the interface to the contract here:
* `__init__()`: initializes the contract
* `get_deposit_root() -> bytes32`: returns the current root of the deposit tree
* `deposit(pubkey: bytes[48], withdrawal_credentials: bytes[32], signature: bytes[96])`: adds a deposit instance to the deposit tree, incorporating the input arguments and the value transferred in the given call. *Note*: The amount of value transferred *must* be at least `MIN_DEPOSIT_AMOUNT`. Each of these constants are specified in units of Gwei.
*Note*: To save on gas the deposit contract uses a progressive Merkle root calculation algorithm that requires only O(log(n)) storage. See [here](https://github.com/ethereum/research/blob/master/beacon_chain_impl/progressive_merkle_tree.py) for a Python implementation, and [here](https://github.com/runtimeverification/verified-smart-contracts/blob/master/deposit/formal-incremental-merkle-tree-algorithm.pdf) for a formal correctness proof.