// The Dafny implementation cannot dictate endianness.
//= compliance/data-format/message-header.txt#2.5
//= type=exception
//# The message header is a sequence of bytes that MUST be in big-endian
//# format.

// Not useful as a specification.
//= compliance/data-format/message-header.txt#2.5.1.6
//= type=exception
//# A Message ID MUST uniquely identify the message (message.md).

// This can't be tested.
//= compliance/data-format/message-header.txt#2.5.1.6
//= type=test
//# While
//# implementations cannot guarantee complete uniqueness, implementations
//# MUST use a good source of randomness when generating messages IDs in
//# order to make the chance of duplicate IDs negligible.

//