Right-to-left parsing

[treiher]

One TLS 1.3 message needs to be parsed from right to left. An optional and variable number of zero bytes must be read until a marker (Content_Type) is found. All bytes left to the marker represent the content of the message.

We think the fields should be specified in the order in that the fields will be parsed (i.e. in reversed order of the actual message format):

   type TLS_Inner_Plaintext is
      message
         Zeros : Padding
            with Marker => Content_Type;
         Tag : Content_Type
            then Content
               with Length => Message'Length - Zeros'Length - Tag'Length
               if Tag = APPLICATION
                  or ((Tag = ALERT or Tag = HANDSHAKE)
                      and Message'Length - Zeros'Length - Tag'Length > 0)
         Content : Payload;
      end message
         with Order => Right_To_Left;

The shown example also depends on #61 and #62.