Semantics of Message'Last inside message types

[treiher]

Context and Problem Statement

Message'Last is differently interpreted in PyRFLX and in the generated SPARK code:

• PyRFLX: Last bit of last field
• SPARK code: Last bit of usable buffer (Ctx.Last)

The need for Message'Last originated in the specification of Ethernet II Frames, where the size of the Payload field is defined by the available space in the buffer. Similar cases also exist in TLS Heartbeat Messages and TCP Segments. Message'Last is also used to check if a field is the last field based on the available space in the buffer, e.g., in TLS Handshake Client Hello.

In the message specifications of HTTP/2 and TCP PyRFLX's interpretation is used to specify an invariant for the message size (this also led to #554). These invariants don't make sense considering the interpretation in the generated SPARK code, as the message size would need to be known before a message is parsed or serialized, even for messages with length fields (i.e., the to be parsed buffer or the target buffer would need to be restricted to the size of the message before parsing or serialization).

Considered Options

O1 Differentiate between Buffer'Last and Message'Last

Buffer'Last is added and corresponds to current semantics of Message'Last in the generated SPARK code. Message'Last is kept with the semantics of PyRFLX. #555 needs to be enforced for Message'Last.

+ Enable specification of global invariants for message size (#554)

O2 Change semantics in PyRFLX

Message is renamed to Buffer and PyRFLX is changed so that Buffer'Last has the same semantics as in the generated SPARK code. #555 is obsolete.

+ Less complexity
− Prevents specification of global invariants for message size (#554)

O3 Use parameters for buffer size, keep Message'Last

As the buffer size is only known outside the specification, it is passed into the specification as a parameter (cf. #609).

   type Frame (Length : Length) is
      message
         Ether_Type : Ether_Type
            then Payload
               with Size => 8 * Length - Ether_Type'Size;
         Payload : Opaque
            if Payload'Size / 8 >= 46 and Payload'Size / 8 <= 1500;
      end message;

Keep Message attributes, but allow references to Message'Last and Message'Size only in conditions towards FINAL (cf. #555). Message'First can be used anywhere.

O4 Change semantics in SPARK

Message'Last represents the last bit of the last field (as in PyRFLX) and must only be used in size aspects for last fields (i.e., fields with a link to FINAL). In SPARK, this could be represented by adding a component Ctx.Written_Last as proposed in #844.

Allow references to Message'Last and Message'Size only in conditions towards FINAL (cf. #555). Message'First can be used anywhere.

+ Message size needs not to be known before writing message

O5 Change semantics in SPARK and forbid use of Message in size aspects

As there is only one correct use of Message in a size aspect in O4, namely an expression that defines the field size as the message size minus the size of all previous fields, this special case could be as well represented by an opaque field without a size aspect.

Allow references to Message'Last and Message'Size only in conditions towards FINAL (cf. #555). Message'First can be used anywhere.

+ Message size needs not to be known before writing message
+ Remove the need for an unnecessary size aspect
− Forgotten size aspects could be misinterpreted

O6 Change semantics in SPARK and allow opaque fields without size aspects

Same as O5, but allow explicit specification of size of opaque fields using Message for opaque fields without successor.

Allow references to Message'Last and Message'Size only in conditions towards FINAL (cf. #555). Message'First can be used anywhere.

+ Message size needs not to be known before writing message
+ Remove the need for an unnecessary size aspect
− Forgotten size aspects could be misinterpreted

Decision Outcome

O3 O6

[senier]

@treiher @jklmnn Isn't this ticket resolved now when #743 and #609 are done?

[treiher]

The checks as described in O3 need to be added to the model verification. The description in #555 did not exactly match the intended outcome, so I have closed #555 in favor of this issue.

[treiher]

The representation of the buffer size as parameters (O3) does not fit well to the channel interface in sessions. The parameter representing the buffer size would need to be set before a Channel'Read, although that information is not known at this time. The modification of a parameter during Channel'Read would be a change of the semantics (and IMHO a rather unexpected). Also, a change of the syntax would be required, as it would need to be defined which parameter represents the buffer size. All these changes would make the handling of such messages more complex. Because of this, O3 seems not to be a good solution anymore.

For the current channel interface, a solution is required that does not require the knowledge of the message size before the message is read from a channel / before the message buffer is written. On the specification side, O3 cannot fulfill this requirement. In SPARK, the Ctx.Last cannot be used to define the message size, as this discriminant must not be changed after the initialization of a context. Thus, O2 is not a viable option. Adding a component Ctx.Written_Last as proposed in #844 could be a solution. The differentiation between Buffer and Message in O1 would also not make sense when using Ctx.Written_Last.

I have added two new options. O4 should fulfill all requirements, O5 might be seen as an optimization of O4.

@senier Do you think continuing with an implementation of O4 makes sense or do we want to have a discussion?

[senier]

The idea presented in O5 is interesting (and having the only valid use of Message'Size replaced by something implicit may also avoid some false expectations). Unless you're sure that O5 saves us a lot of effort, I'd continue with O4 and discuss O5 as a potential optimization.

[treiher]

Alright, then I will continue with O4. The changes for O4 should be limited to the generator. For O5, also the model and PyRFLX will need to be changed, but that can also be done after completing the changes for O4.