Make the behaviour of int_to_bytes and bytes_to_int in Math.dfy dependent on the ENDIANNESS constant

Question

Closed this issue 4 years ago · 3 comments

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.

Answer 1 · 2020-05-06T21:38:14.000Z

I think little endian is the choice for the spec, and there is no consideration to move to big endianness.
Am I missing something?

Answer 2 · 2020-05-07T01:35:10.000Z

I think little endian is the choice for the spec, and there is no consideration to move to big endianness.

You are likely to be right, it is probably inconceivable that the endianness may be changed now.

However, the Eth2 spec still specifies that int_to_bytes and bytes_to_int should be dependent on the value of ENDIANNESS.

Answer 3 · 2020-06-16T06:55:06.000Z

Closing this as seems to be resolved.