Verification of message size

[treiher]

In the generated SPARK code messages must be byte-aligned. This also applies to messages in sequences. The bit size of all messages (in a sequence) must be a multiple of eight.

The following specification should be rejected, as one instance of TLV::Message has a size of just 2 bit:

package TLV is

   type Tag is (Msg_Data => 1, Msg_Error => 3) with Size => 2;
   type Length is mod 2**14;

   type Message is
      message
         Tag    : Tag
            then Length
               if Tag = Msg_Data
            then null
               if Tag = Msg_Error;
         Length : Length
            then Value
               with Size => Length * 8;
         Value  : Opaque;
       end message;

   type Messages is array of Message;

end TLV;

[treiher]

Allowing messages with a bit size which is not a multiple of eight complicates the generated SPARK code. Since I am not aware of any real-world example where this is the case, I would argue for a general prohibition of such message specifications. @senier Do you have any objections to that?

[senier]

We had a similar discussion for RecordFuzz lately. I'm not aware of such a protocol either (and, in all cases the underlying representation will be bytes anyways - what values will the last 1-7 bit have if the message size is not multiple of 8 bit). We should implement a model verification step that proofs that the size is multiple of 8 bit on all paths.