Definition of const in imported module breaks some proofs

[franck44]

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.

[franck44]

There are better ways to initialise seq (and other data structures in Dafny).
For examples, seq<int can be initialised like so:
s := seq<int>(3, _ => 7)

which produces [7,7,7.