Improve message API

[treiher]

• [ ] Use Index/Length for all parameters instead of Bit_Index/Bit_Length (in Initialize procedures)
  • At some point we decided to only allow byte-aligned bounds, so there is no need anymore to set bounds with bit granularity.
• [ ] Add Structural_Valid_Message (Ctx) as precondition for Size and Byte_Size
  • Both functions return the sum of the sizes of all verified fields, and thus could lead to unexpected results for non-verified or invalid messages.