We can access the type of an object x using x?.
This may enable us to simplify some definitions and functions using wellTyped.

The function foo below has a pre-condition (Pre) logically equivalent to false.
As a consequence any code in the body (Body) and any post-condition (Post) will satisfy the pre-post constraints (the function can not be run for any input, so it is trivially correct).
Indeed, Dafny verifies foo as the verification conditions is: is Pre && Body && !Post SAT? the answer being no as Pre == false.
There is no logical flaw or bug in the SMT-solver or the Dafny verification engine, but it may be helpful to issue a warning when a pre-condition is equivalent to false.

function method foo(x: nat) : nat
    requires x < 2 && x > 2
    ensures foo(x) >= 10
{
    x + 1
}

Reported to Dafny repo issue 620

In view of the discussion we had with Protolambda, it seems that the SSZ module could be simplified.

We may focus on:

1. provide serialise/deserialise for each type (without an super type Serialisable of RawSerialisable)
2. prove the indempotence for each type separately.

The assumption in using SSZ is that clients agree on a channel for each type and the should communicate data for this type.
This may help us to simplify the current type system that may be over-complicated.

see ethereum/consensus-specs#1789

Due to a missing pre-condition in state_transition, process_slots can be called with parameters that violate the assert statement:

def process_slots(state: BeaconState, slot: Slot) -> None:
    assert state.slot <= slot
    while state.slot < slot:
        ...

When using bit vectors in Trait, the Dafny compiler throws an exception.

Bug report (and example) created see issue 549

Expected results and current state may be updated at that stage.

Using sizeOf on variable-sized objects should be avoided.

https://github.com/PegaSysEng/eth2.0-dafny/blob/acb7b2c86731193bd0969b9c4b1bc24b493fdd19/src/dafny/ssz/Merkleise.dfy#L31

Later we may refine the Serialisable type into FixedSizeSer and VarSizeSer and use FixedSizeSer for the type of the parameter of SizeOf.

The eth2.0 specs perform a sequence of if statements to update the finalised_checkpoint of a given state.
In the specification of updateFinalisedCheckpoint those statements are supposed to performed in a given order (with priority).
This differs from the eth2.0 specs where the conditions of the if are checked in sequence and a subsequent if side-effect can override a previous one.

At the moment the code pertaining to the last update all(bits[0..2]) && s.current_justified_checkpoint.epoch == current_epoch - 1 is ignored.

To do:

1. investigate whether the ifs should be exclusive
2. fix the spec (updateFinalisedCheckpoint) accordingly and the implementation (process_justification_and_finalization).

Please review

• int_to_bytes,
• bytes_to_int,
• lemmaBytesToIntIsTheInverseOfIntToBytes,
• lemmaIntToBytesIsTheInverseOfBytesToInt

in
beacon/helpers/Math.dfy

There is a bug in the get_next_powewr_of_2 in the eth2.0 spec.
For 0 it returns 0.
Same bug exists for get_previous_power_of_2.

Bug report filed issue 1695.

Under the environment of extension version v2.3.0 in VS Code, there exists an error that says the assertion may not hold for the case Uint32

Here is the screenshot:

The original code snippet:

/** Deserialise. 
     *  
     *  @param  xs  A sequence of bytes.
     *  @param  s   A target type for the deserialised object.
     *  @returns    Either a Success if `xs` could be deserialised
     *              in an object of type s or a Failure oytherwise.
     *  
     *  @note       It would probabaly be good to return the suffix of `xs`
     *              that has not been used in the deserialisation as well.
     */
     function method deserialise(xs : seq<byte>, s : Tipe) : Try<Serialisable>
        requires !(s.Container_? || s.List_? || s.Vector_?)
        ensures match deserialise(xs, s) 
            case Success(r) => wellTyped(r)
            case Failure => true 
    {
        match s
            case Bool_ => if |xs| == 1 && 0 <= xs[0] <= 1 then
                                var r : Serialisable := Bool(byteToBool(xs));
                                Success(r)
                            else 
                                Failure
                            
            case Uint8_ => if |xs| == 1 then
                                var r : Serialisable := Uint8(uintDes(xs));
                                Success(r)
                             else 
                                Failure

            //  The following cases must check that the result is wellTyped.
            //  If wellTyped and RawSerialisable, the result is a Serialisable.
            case Uint16_ => if |xs| == 2 then
                                //  Verify wellTyped before casting to Serialisable
                                assert(wellTyped(Uint16(uintDes(xs))));
                                //  If wellTyped and RawSerialisable, result is a Serialisable
                                var r : Serialisable := Uint16(uintDes(xs));
                                Success(r)                               
                            else 
                                Failure
            
            case Uint32_ => if |xs| == 4 then
                                assert(wellTyped(Uint32(uintDes(xs))));
                                var r : Serialisable := Uint32(uintDes(xs));
                                Success(r)                               
                            else 
                                Failure

            case Uint64_ => if |xs| == 8 then
                                constAsPowersOfTwo();
                                assert(wellTyped(Uint64(uintDes(xs))));
                                var r : Serialisable := Uint64(uintDes(xs));
                                Success(r)  
                             else 
                                Failure

            case Uint128_ => if |xs| == 16 then
                                constAsPowersOfTwo();
                                assert(wellTyped(Uint128(uintDes(xs))));
                                var r : Serialisable := Uint128(uintDes(xs));
                                Success(r)  
                             else 
                                Failure

            case Uint256_ => if |xs| == 32 then
                                constAsPowersOfTwo();
                                assert(wellTyped(Uint256(uintDes(xs))));
                                var r : Serialisable := Uint256(uintDes(xs));
                                Success(r)                              
                            else 
                                Failure
                                
            case Bitlist_(limit) => if (|xs| >= 1 && xs[|xs| - 1] >= 1) then
                                        var desBl := fromBytesToBitList(xs);
                                        //  Check that the decoded bitlist can fit within limit.
                                        if |desBl| <= limit then
                                            var r : Serialisable := Bitlist(desBl,limit);
                                            Success(r)
                                        else
                                            Failure
                                    else
                                        Failure

            case Bitvector_(len) => if isValidBitVectorEncoding(xs, len) then            
                                        var r : Serialisable := Bitvector(fromBytesToBitVector(xs,len));
                                        Success(r)
                                    else
                                        Failure

            case Bytes_(len) => if 0 < |xs| == len then
                                  var r : Serialisable := Bytes(xs);
                                  Success(r)
                                else Failure
    }

The path to that line: /eth2.0-dafny/src/dafny/ssz/Serialise.dfy(201,39): Error: assertion might not hold

Is there any solution for this, or it doesn't matter? Many thanks in advance!

This issue is reported as issue 2136 eth2.0-specs.

Avoid creating "computation" overflows when not necessary

Overview of the Issue

In some part of the code of the Eth2.0 specs, some computations are performed on bounded integers (e.g. uint64) and may result in underflows/overflows.
For instance if a is uint64, computing 3 * a may result in an overflow as there result may not fit in the 64 bits.

Overflows can contribute to reject blocks:

State transitions that cause a uint64 overflow or underflow are also considered invalid. [beacon chain transition function].

As a result a block can be rejected even if it is actually well-formed and not responsible for the overflows.
(A related question is whether the previous statement applies only to uint64 or any underflow/overflow.)

Avoiding spurious under/overflows

However, it is possible to rewrite some parts of the specs in a way that avoids creating spurious overflows.
Spurious overflows can appear because a computation of a property of a given value is implemented using unsafe operations,
but the property could be checked without these unsafe operations.

Example: assume a and b are uint64.
The following code may result in an overflow when a >= MAX_UNIT64 - 1:

if (b >= 2) 
  if (a + 2 <= b)  // possible overflow for a + 2 that may not be a `uint64`
  ....

This code snippet can be rewritten in a safer equivalent version:

if (b >= 2) 
  if (a <= b - 2)  // b - 2 >= 0 and does not underflow not overflow.
  ....

Occurrences of this issue in part of the Eth2.0 specs

The code for process_justification_and_finalization may be made safer avoiding spurious overflows.

The following piece of code may be rewritten in a safer non-overflow-prone version:

# Process finalizations
if get_current_epoch(state) <= GENESIS_EPOCH + 1:
       return

// after this location, get_current_epoch(state) > GENESIS_EPOCH + 1 >= 2 and we can use this fact to
// evaluate the following conditions without any overflows. 
bits = state.justification_bits
# The 2nd/3rd/4th most recent epochs are justified, the 2nd using the 4th as source
if all(bits[1:4]) and old_previous_justified_checkpoint.epoch + 3 == current_epoch:
     state.finalized_checkpoint = old_previous_justified_checkpoint
# The 2nd/3rd most recent epochs are justified, the 2nd using the 3rd as source
if all(bits[1:3]) and old_previous_justified_checkpoint.epoch + 2 == current_epoch:
       state.finalized_checkpoint = old_previous_justified_checkpoint
# The 1st/2nd/3rd most recent epochs are justified, the 1st using the 3rd as source
if all(bits[0:3]) and old_current_justified_checkpoint.epoch + 2 == current_epoch:
       state.finalized_checkpoint = old_current_justified_checkpoint
# The 1st/2nd most recent epochs are justified, the 1st using the 2nd as source
if all(bits[0:2]) and old_current_justified_checkpoint.epoch + 1 == current_epoch:
       state.finalized_checkpoint = old_current_justified_checkpoint

The last three ifs statement can be rewritten as old_previous_justified_checkpoint.epoch == current_epoch - k, k = 1,2 (using a subtraction rather an addition to avoid any overflow.)
The first one old_previous_justified_checkpoint.epoch + 3 == current_epoch falls into two case:

• current_epoch == 2 and that case, this condition cannot be true as old_previous_justified_checkpoint.epoch is a uint64 and thus non-negative
• current_epoch > 2 and in this case we can replace the test using a minus operator. Overall this can be rewritten as:

As a result it is equivalent to:

 if all(bits[1:4]) and current_epoch >= 3 && old_previous_justified_checkpoint.epoch == current_epoch - 3:
        state.finalized_checkpoint = old_previous_justified_checkpoint

Another occurrence of possible overflows is in the computation of supermajority in the same function:

if get_attesting_balance(state, matching_target_attestations) * 3 >= get_total_active_balance(state) * 2:
...

The values get_attesting_balance(state, matching_target_attestations) and get_total_active_balance(state) are uint64 and multiplying them may generate an overflow exception.
This issue can be mitigated by converting the value of uint128 and perform the comparison with this type.

Formal verification that previous proposed patches are correct

The formal proof that the previous changes mitigate the overflow issues described above can be found in the Dafny verified version of process_justification_and_finalization.

state_transition and on_block are currently using blockheaders instead of blocks.

Before adding process_operations, it is necessary to move to using blocks as blockheaders do not have the body of a block (that contains the operations).

Some overflows may happen in several helper functions of the Beacon Chain.

Possible overflow in assert statement in get_block_root_at_slot

The following code snippet contains a assert statement that may result in an overflow:

def get_block_root_at_slot(state: BeaconState, slot: Slot) -> Root:
    """
    Return the block root at a recent ``slot``.
    """
    assert slot < state.slot <= slot + SLOTS_PER_HISTORICAL_ROOT  
    return state.block_roots[slot % SLOTS_PER_HISTORICAL_ROOT]

note: the above assert is not a pre-condition to guarantee the absence of array-out-of-bounds error when dereferencing state.block_roots (this never happens because block_roots has size SLOTS_PER_HISTORICAL_ROOT) but a functional property of the system (requesting the block root for a slot that is too far in the past should not be permitted).

The pre-condition of the previous function should be strengthened to prevent slot + SLOTS_PER_HISTORICAL_ROOT from overflowing:

function method get_block_root_at_slot(state: BeaconState, slot: Slot) : Root
     requires slot as int + SLOTS_PER_HISTORICAL_ROOT as int < 0x10000000000000000 //  Max uint64 + 1
     requires slot < state.slot <= slot + SLOTS_PER_HISTORICAL_ROOT
{
        state.block_roots[slot % SLOTS_PER_HISTORICAL_ROOT]
}

Possible overflow in compute_start_slot_at_epoch

Because Epoch ranges over uint64, the multiplication can overflow in the following code snippet:

def compute_start_slot_at_epoch(epoch: Epoch) -> Slot:
    """
    Return the start slot of ``epoch``.
    """
    return Slot(epoch * SLOTS_PER_EPOCH)

The pre-condition should be strengthened to:

function method compute_start_slot_at_epoch(epoch: Epoch) : Slot
    requires epoch as int * SLOTS_PER_EPOCH as int < 0x10000000000000000    // max unit64 + 1
{
    epoch * SLOTS_PER_EPOCH as Slot
}

Other functions impacted by the previous strengthening of pre-conditions

As a result functions calling compute_start_slot_at_epoch or get_block_root_at_slot should have their pre-conditions strengthened.
This includes get_block_root

def get_block_root(state: BeaconState, epoch: Epoch) -> Root:
    """
    Return the block root at the start of a recent ``epoch``.
    """
    return get_block_root_at_slot(state, compute_start_slot_at_epoch(epoch))

the pre-condition of which should be:

function method get_block_root(state: BeaconState, epoch: Epoch) : Root    
     requires state.slot as int + SLOTS_PER_HISTORICAL_ROOT as int < 0x10000000000000000 // Max uint64 + 1
     requires epoch as int * SLOTS_PER_EPOCH as int < 0x10000000000000000   
     requires compute_start_slot_at_epoch(epoch) < state.slot <= compute_start_slot_at_epoch(epoch) + SLOTS_PER_HISTORICAL_ROOT  
{ 
        var e := compute_start_slot_at_epoch(epoch);
        get_block_root_at_slot(state, e)
}

The Eth2 .md spec prescribes that the behaviour of int_to_bytes and bytes_to_int should be dependent on the value of the ENDIANNESS constant.

In the current Dafny specification, little endianness is hardcoded for both functions.

To note that little endianness is also hardcoded for both functions in the Eth2 K-Spec.

In the Gasper helpers and proofs, change the MAX_VALIDATORS_PER_COMMITTEE to another (new) constant which is the size of the set of validators and not necessarily the MAX number of validators per committee.

Moreover, this can change over time, so at some point, it should be replaced by the current size of the set of validators.

Using Dafny 3.0.0, a (new?) info has showed up:
"Auto-accumulator tail-recursive".
This is not an error or warning but may deserve some attention: how do we suppress this info from showing up, like induction info?

And example is the tail recursive function timeSeq in utils/Helpers.dfy:

 function method {:tailrecursion true} timeSeq<T>(t : T, k : nat) : seq<T> 
        ensures |timeSeq(t,k)| == k
        ensures forall i :: 0 <= i < k ==> timeSeq(t,k)[i] == t
        decreases k
    {
        if k == 0 then []
        else [t] + timeSeq(t, k - 1)
    }

Even with {:tailrecursion true} attribute the info appears using Dafny 3.

Simplified version of process_deposit without checking signatures and valid Merkle branch.

https://github.com/PegaSysEng/eth2.0-dafny/blob/acb7b2c86731193bd0969b9c4b1bc24b493fdd19/src/dafny/ssz/Merkleise.dfy#L58

type Bytes = seq // i.e. the output of serialisation
//type serialisedElement = seq // i.e. the output of serialisation
// bounds? should be at least 1 byte (if representing serialised output)
// maybe call serialisedBytes or serialisedElement?

The Eth2 specs frequently use assert statements to validate methods arguments.
This is a known source of security vulnerabilities:

• CWE-617: Reachable Assertion
• And also MET01-J. Never use assertions to validate method arguments from the The CERT Oracle Secure Coding Standard for Java.

Eth2 issue is issue 1797
following a previous issue

The eth2.0 specs seem to use different strategies to compute the result of the function. Sometimes as side-effects and sometimes not.

This does not help to understand what is actually computed and can be dangerous.
This has been reported in issue 1932.

Surprisingly, the definition of constants as

const SEQ_EMPTY_32_BYTES := timeSeq<Byte>(0,32)

or

const EMPTY_BYTES32 := Bytes32(SEQ_EMPTY_32_BYTES)

in Eth2Types.dfy seem to have an impact on seemingly unrelated datatypes in other files.
For instance, when defined as above, the proofs of the lemmas bitlistDecodeEncodeIsIdentity and bitlistEncodeDecodeIsIdentity are broken (the base case in the inductive proofs).

If I comment out the const and use

timeSeq(0 as Byte, 32) // for const SEQ_EMPTY_32_BYTES := timeSeq<Byte>(0,32)

and

Bytes32(timeSeq(0 as Byte, 32)) // for EMPTY_BYTES32

everything seems to be fine and the proofs can be checked by Dafny.
The first proof can be fixed by asserting that timeSeq(false,8) is equal for FALSE_BYTE.
The second I have no idea.

Anyhow, that seems very surprising that definitions of constants that are not used in the module BitlistSeDes can break proofs.

For now I will revert to the use of timeSeq in Eth2Types.dfy but this may need further investigation.

Eth2.0-specs issue 2138 calls for comments to ask entry for SSZ implementations.

Proposed this repo as an entry as it contains an almost complete set of serialise/deserialise for there SSZ types.

Dafny does not seem to be able to verify the proof of lemma bitvectorEncodeDecodeIsIdentity.
The failing case is for |xb| == 1 and we may add a few hints in the calculations to fix that.

Some files need custom verification options to be checked efficiently.
It would be nice if the batch processing (script verifyAll.sh) could run the verification of each file with a default/custom verification configuration.

In simple-serialize.md, within the Merkelization section it says:

We now define Merkleization hash_tree_root(value) of an object value recursively:

merkleize(pack(value)) if value is a basic object or a vector of basic objects.

This part should exclude bitvectors as they are dealt with separately.

A suggested wording to correct this typo could be:

merkleize(pack(value)) if value is a basic object or a vector of basic objects, excluding bitvectors.

Bug report filed, issue #1892

See ethereum/consensus-specs#1788

Seems like at least two defs of BeaconBlock co-exist:

class BeaconBlock(Container):
    slot: Slot
    proposer_index: ValidatorIndex
    parent_root: Root
    state_root: Root
    body: BeaconBlockBody

and another one

class BeaconBlock(Container):
    slot: Slot
    parent_root: Root
    state_root: Root
    body: BeaconBlockBody

Seems like APACHE is the preferred license in PegaSys for this kind of work.
After approval, we may add the license to the repo, and a header (copyright) to the files.

Various issues with the wording of the Merkleisation section of the SSZ spec.

Bug report filed, issue #1893.

Reduce size and complexity of files.

To do on the beacon folder first:

• create files with types only, e.g. AttestationsTypes.dfy
• create files with functions (if possible no lemmas), e.g Attestations.s.dfy
• create files with proofs, e.g. Attestations.p.dfy
• try to split functions and group them meaningfully (e.g. in Helpers, split epoch and other stuff)
• create subfolders of beacon (e.g. epoch, generalProofs)

Commit a0a4a69 adds the Container constructor to Serialisable but it does not add the related serilisation and deserialisation functions.
Also, in order to avoid breaking the verification for the existing serialisation functions and lemmas, it adds a requires clause to

• serialise
• deserialise
• wellTypedDoesNotFail
• seDesInvolutive
• serialiseIsInjective

constraining the type of input parameter to be in the set {Bool_,Uint8_,Bitlist_,Bytes32_}

The ssz spec and the py-ssz implementation of the pack function imply a return of at least one chunk. However, if the pack function calls the to_chunks function to generate the return value, then an output of at least one chunk is not guaranteed.

Reported to py-ssz: ethereum/py-ssz#110 (comment)

The following are more general specifications for the functions int_to_bytes and bytes_to_int than those currently in the Dafny specification:

    function int_to_bytes(n: uint64, length: uint64) : seq<uint8>
    requires n as nat < power(256,length as nat)
    ensures |int_to_bytes(n,length)| == length as int
    ensures forall i | 8 <= i < |int_to_bytes(n,length)| :: int_to_bytes(n,length)[i] == 0

    function bytes_to_int(s: seq<uint8>):uint64
    requires forall i | 8 <= i < |s| :: s[i] == 0
    ensures bytes_to_int(s) as nat < power(256,8)

Design scripts to collect statistics about Dafny files.

• number of lines of code (started in count_lines.py)
• call graph (call_graph.py)

A detailed account of this bug is available as issue 922 in the dafny-lang repo.

simple-serialise for vectors and unions is not cristal clear.
Some clarification is needed to understand the encoding.

Reported and discussed in issue 1630

Deserialise in py-ssz bitlists accepts input ending with a 0-byte which cannot be a serialised bit lists.

Reported to py-ssz: issue 109

While moving to using const for empty blocks, genesis state etc, in the ForkChoice module, a Dafny/Boogie error showed up.
After some trimming of the code where the error originated, I managed to obtain a simple version exhibiting the same problem.
There is a work around and the problem as been reported to the dafny-lang developers as issue 904.

The bitfield_bytes(bits) function in the eth2.0 spec doesn't specify the correct output.
It returns bytes rather than chunks..

Bug report filed issue #1787

Archive current snapshot as a branch and clean up master branch.

Ref commit is dd3a5b9

As per the K-spec, vectors seem to be used in a small numb er of cases.

This is taken from the K-spec, types.k file:

 block_roots: Vector[Hash, SLOTS_PER_HISTORICAL_ROOT]
    state_roots: Vector[Hash, SLOTS_PER_HISTORICAL_ROOT]
    proof: Vector[Hash, DEPOSIT_CONTRACT_TREE_DEPTH + 1]  # Merkle path to deposit data list root
  //Converts K-Map representation of a python List/Vector to a K-ValueList. Only implemented for used types.```
On top of that seems like `Bytes32`` which is a Vector of 32 uint8 is also used.

We may only consider the used typed as per the K-spec in our verification of Phase 0.

It seems that on_block(b) can be called many times with the same block, or with any block that is already in the store.
This results in the store not being modified and is a potential source of DoS attack.

This issue has been reported as issue 1891 in the Eth2.0 specs.

The two functions, in ssz
https://github.com/PegaSysEng/eth2.0-dafny/blob/7174b8d01b5c667af4a78cbf6a65c36e96ad2c32/src/dafny/ssz/BitListSeDes.dfy#L93
and in merkle
https://github.com/PegaSysEng/eth2.0-dafny/blob/7174b8d01b5c667af4a78cbf6a65c36e96ad2c32/src/dafny/merkle/Merkleise.dfy#L241

are similar.
The first one adds a trailing one to the argument list l before performing the same computation as the second one.
We may consider refactoring this code and use only one instance.

The Eth2.0-specs omit checks on keys's memberships in some cases and explicitly mention some (using asserts) at other times.
This seems to be a general inconsistency in the specs.
This inconsistency has been reported in issue 1930.

The value parameter in the serialise method of the class UInt is of type int.
Hence, it is not possible to serialise any value >= 2^32.

Ths bug must be filed on the PySSZ repo.

In the eth2.0-specs it specifies within simple-serialise.md (Illegal types section) reads:

Empty vector types (Vector[type, 0], Bitvector[0]) are illegal.

However in bitvector.py an error is raised only if bit_count is negative. An error should be raised if bit_count <= 0.

Bug report filed issue #111

In the current version and for the sake of simplicity, we will assume that a ValidatorIndex is within the bounds
of the MAX_VALIDATOR_PER_COMMITTEE.

This is not the case in practice. A Validator index is within the REGISTRY_LIMIT and there is a list of indices (chosen validator indices for a given slot) that encodes the set of selected validators.

As we do not deal with the random selection of validators, it is reasonable to assume the following simplification:
a validatorIndex is within the MAX_VALIDATOR_PWER_COMMITTEE range.

Later, we have to introduce indexedAttestation and map a given item in the list of aggregation_bits and map the list of bits the attesting_indices. See this link.

Bug report on the Dafny GitHub repo: dafny-lang/dafny#703

Copied here for reference

The following piece of code verifies correctly.

module M {
    predicate method p1(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }

    predicate method p2(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }    

    type T1 = x:nat | p1(x) witness 5
    type T2 = x:T1 | p2(x) witness 5

    method m(x:nat) returns (x':nat)
    {
        x' := 0;
    }
}

However, the verification of the following piece of code,

module M {
    predicate method p1(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }

    predicate method p2(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }    

    type T1 = x:nat | p1(x) witness 5
    type T2 = x:T1 | p2(x) witness 5

    method {:fuel p1,1,2} m(x:nat) returns (x':nat)
    {
        x' := 0;
    }
}

where the annotation {:fuel p1,1,2} has been added to method m, fails with error

test.dfy(19,35): Error: result of operation might violate subset type constraint for 'T1'
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else

Dafny program verifier finished with 4 verified, 1 error

The same happens if the annotation {:fuel 1,2} is added to the function p1 as follows.

module M {
    predicate method {:fuel p1,1,2} p1(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }

    predicate method p2(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }    

    type T1 = x:nat | p1(x) witness 5
    type T2 = x:T1 | p2(x) witness 5

    method m(x:nat) returns (x':nat)
    {
        x' := 0;
    }
}

List types limited to 0 values, i.e. List[type, 0], are not included in the list of illegal types in the SSZ specification.

However, line 177 of the py-ssz reference implementation, rules out LIst types limited to 0 values by requiring that the maximum length of homogenous composites must be at least 1.

Related Issue on the EF Eth2 Repo: Issue 1863