Correctness & Mechanised proof of the incremental tree algorithm

[franck44]

Hi,

there is a comment in the Solidity code of the smart contract (with the assert(false)) that seems to indicate that there is some uncertainty about the correctness of the code.

In this repo there is a formal and mechanised proof (in Dafny) that the deposit() function his correct, and indeed that the assert(false) will never trigger. (there is also a simplification of the algorithm that is proved correct).

In the REAME for the deposit SC there is a reference to a (non-mechanised) correctness proof (RV). Our repo provides the first fully mechanised proof (including correctness, termination, memory safety, initialisation) of the DSC (excluding the byte-code) and could probably be referenced there too.

[mratsim]

How much is the gas cost using your minimal proven formally verified contract compared to the one deployed?

[franck44]

I have not verified the bytecode. The simplified version of the deposit() function in the contract is:

method deposit(v : int) 
    requires deposit_count < power2(TREE_HEIGHT) - 1 
{   
    var root := v;
    var size : nat := deposit_count;
    var i : nat := 0;
    
    while size % 2 == 1 {
        root := hash(branch[i], root);
        size := size / 2;
        i := i + 1;
    } 
    //  i is guaranteed to satisfy 0 <= i < TREE_HEIGHT 
    //  This ensures the absence of out of bounds error in the following update 
    branch[i] := root;
    deposit_count := deposit_count + 1;
}

It does not check the (while loop) test i < TREE_HEIGHT in an enclosing while because this test always evaluates to true.

[franck44]

@mratsim I have tried to get an estimate of the Gas cost with the online compiler at http://remix.ethereum.org/ but the details of the compilation returns "infinite" for the deposit() function.

[MrChico]

The assertion in the code isn't an indication of any uncertainty. It is simply put there for demonstrative purposes, to document the fact that the code is unreachable and to serve as a "real world" target for providing tools. Since the code is actually unreachable, the assertion does not incur any additional gas costs.

[franck44]

@MrChico The solidity code (below) reads this code should be unreachable

The fact that the code is unreachable is not trivial to prove ... and that's what I did in this repo. As far as I know this is the first complete formal mechanised proof of correctness of the DSC.

Apart from that, the current deposit code has an external for loop and an internal return that can end the loop:

...
bytes32 node = sha256(abi.encodePacked(
            sha256(abi.encodePacked(pubkey_root, withdrawal_credentials)),
            sha256(abi.encodePacked(amount, bytes24(0), signature_root))
        ));
uint size = deposit_count;
for (uint height = 0; height < DEPOSIT_CONTRACT_TREE_DEPTH; height++) {
    if ((size & 1) == 1) {
        branch[height] = node;
            return;
     }
     node = sha256(abi.encodePacked(branch[height], node));
     size /= 2;
}
// As the loop should always end prematurely with the `return` statement,
// this code should be unreachable. We assert `false` just to be safe.
assert(false);

with a test height < DEPOSIT_CONTRACT_TREE_DEPTH. This test always evaluates to true and is unnecessary (the formal mechanised proof is in the Dafny repo I mentioned above). This test may incur some gas cost and can be safely omitted.

The simplified version is :

...
bytes32 node = sha256(abi.encodePacked(
            sha256(abi.encodePacked(pubkey_root, withdrawal_credentials)),
            sha256(abi.encodePacked(amount, bytes24(0), signature_root))
        ));
// deposit_count can be increment here instead and in that case the while loop test is size % 2 == 0
uint size = deposit_count;
uint height = 0;
while (size % 2 == 1)   {
   node = sha256(abi.encodePacked(branch[height], node));
   size /= 2;
   height += 1;   
}
// height is guaranteed to satisfy 0 <= height < branch.length
branch[height] = node;
deposit_count += 1;

and the following proofs have been mechanised (in Dafny):

1. no array-out-of-bounds: height is always in the range of branch indices and
2. termination is guaranteed if deposit_count < MAX_DEPOSIT_COUNT = 2**DEPOSIT_CONTRACT_TREE_DEPTH - 1

The total correctness of both algorithms (deposit() and get_deposit_root()) with respect to a Merkle tree specification is also part of the proof code (e.g. get_deposit_root() always returns what would be returned if we build a Merkle tree).

[franck44]

@mratsim @MrChico There seems to be medium interest and activity in this thread, so feel free to close this issue.