Mapping values of two scalar types

senier commented 2 years ago

Context and Problem Statement

In protocols the values of two scalar types sometimes have to be mapped onto / converted into each other in a way that cannot be done by a calculation. The most prominent example are algorithms selected in a protocol session which result in response messages of different lengths:

package Test is

   type Alg is (Alg1,  -- 1 byte response
                Alg2,  -- 2 byte response
                Alg3)  -- 4 byte response
      with Size => 8;
   type Len is mod 2 ** 16;

   type Request is
      message
         Alg : Alg;
      end message;

   type Response (Len : Len) is
      message
         Data : Opaque
            with Size => 8 * Len;
      end message;

   generic
      Transport : Channel with Readable, Writable;
   session S with
      Initial => Receive,
      Final => Done
   is
      Request : Request;
      Response : Response;
   begin
      state Receive is
      begin
         Transport'Read (Request);
      transition
         goto Done
            if Request'Valid /= True
         goto Prepare_Response
      end Receive;

      state Prepare_Response
      is
      begin
         Response := Response'(Len => 1, -- FIXME: Depends on Request.Alg
                               Data => [1]);
      transition
         goto Send_Response
      exception
         goto Done
      end Prepare_Response;

      state Send_Response is
      begin
         Transport'Write (Response);
      transition
         goto Done
      end Send_Response;

      state Done is null state;
   end S;

end Test;

Use Cases

Determine size of DIGESTS response based on selected hash algorithm in SPDM protocol (7.4)

Considered Options

O1

Use states to select the corresponding value:


   generic
      Transport : Channel with Readable, Writable;
   session S with
      Initial => Receive,
      Final => Done
   is
      Request : Request;
      Response : Response;
      Len : Len;
   begin
      state Receive is
      begin
         Transport'Read (Request);
      transition
         goto Done
            if Request'Valid /= True
         goto Set_Alg1_Length
            if Request.Alg = Alg1
         goto Set_Alg2_Length
            if Request.Alg = Alg2
         goto Set_Alg3_Length
            if Request.Alg = Alg3
         goto Prepare_Response
      end Receive;

      state Set_Alg1_Length is
      begin
         Len := 1;
      transition
         goto Prepare_Response
      end Set_Alg1_Length;

      state Set_Alg2_Length is
      begin
         Len := 2;
      transition
         goto Prepare_Response
      end Set_Alg2_Length;

      state Set_Alg3_Length is
      begin
         Len := 4;
      transition
         goto Prepare_Response
      end Set_Alg3_Length;

      state Prepare_Response
      is
      begin
         Response := Response'(Len => Len,
                               Data => [1]);
      transition
         goto Send_Response
      exception
         goto Done
      end Prepare_Response;

      state Send_Response is
      begin
         Transport'Write (Response);
      transition
         goto Done
      end Send_Response;

      state Done is null state;
   end S;

+ No changes required − Very verbose − Potentially many additional states − Totality not enforced

O2

Use sequences and list comprehension:

   generic
      Transport : Channel with Readable, Writable;
   session S with
      Initial => Receive,
      Final => Done
   is
      Request : Request;
      Response : Response;
   begin
      state Receive is
      begin
         Transport'Read (Request);
      transition
         goto Done
            if Request'Valid /= True
         goto Prepare_Response
      end Receive;

      state Prepare_Response
      is
         Maps : Maps;
         Lens : Maps;
         Sel  : Map;
      begin
         Maps'Append (Map'(Alg => Alg1, Len => 1));
         Maps'Append (Map'(Alg => Alg2, Len => 2));
         Maps'Append (Map'(Alg => Alg3, Len => 4));
         Lens := [for M in Maps if M.Alg = Request.Alg => M];
         Sel := Lens'Head;
         Response := Response'(Len => Sel.Len,
                               Data => [1]);
      transition
         goto Send_Response
      exception
         goto Done
      end Prepare_Response;

      state Send_Response is
      begin
         Transport'Write (Response);
      transition
         goto Done
      end Send_Response;

      state Done is null state;
   end S;

+ No changes required − Convoluted syntax − Inefficient code (space and time) − Intent is not conveyed clearly in specification − Totality not enforced

O3

Introduce case expression:


   generic
      Transport : Channel with Readable, Writable;
   session S with
      Initial => Receive,
      Final => Done
   is
      Request : Request;
      Response : Response;
   begin
      state Receive is
      begin
         Transport'Read (Request);
      transition
         goto Done
            if Request'Valid /= True
         goto Prepare_Response
      end Receive;

      state Prepare_Response
      is
      begin
         Response := Response'(Len => (case Request.Alg is
                                       when Alg1 => 1,
                                       when Alg2 => 2,
                                       when Alg3 => 4),
                               Data => [1]);
      transition
         goto Send_Response
      exception
         goto Done
      end Prepare_Response;

      state Send_Response is
      begin
         Transport'Write (Response);
      transition
         goto Done
      end Send_Response;

      state Done is null state;
   end S;

+ Concise + Conveys the intent clearly + Totality can be enforced + Probably easy to transform to SPARK − Somewhat redundant to existing state transitions − Inefficient when same mapping is required in multiple places − Reusability questionable

O4

Use external function:

   generic
      Transport : Channel with Readable, Writable;
      with function Alg_Len (Alg : Alg) return Len;
   session S with
      Initial => Receive,
      Final => Done
   is
      Request : Request;
      Response : Response;
   begin
      state Receive is
      begin
         Transport'Read (Request);
      transition
         goto Done
            if Request'Valid /= True
         goto Prepare_Response
      end Receive;

      state Prepare_Response
      is
         Len : Len;
         Alg : Alg;
      begin
         Alg := Request.Alg;
         Len := Alg_Len (Alg);
         Response := Response'(Len => Len,
                               Data => [1]);
      transition
         goto Send_Response
      exception
         goto Done
      end Prepare_Response;

      state Send_Response is
      begin
         Transport'Write (Response);
      transition
         goto Done
      end Send_Response;

      state Done is null state;
   end S;

+ Concise + No changes required − Intent is not conveyed in specification at all − Totality not enforced − Code changes may break specification − Proof may become hard or impossible

O5

Introduce a dedicated mapping type (concrete syntax to be defined):

package Test is

   type Alg is (Alg1,  -- 1 byte response
                Alg2,  -- 2 byte response
                Alg3)  -- 4 byte response
      with Size => 8;
   type Len is mod 2 ** 16;

   type Alg_Len is map (Alg) of Len;

   type Request is
      message
         Alg : Alg;
      end message;

   type Response (Len : Len) is
      message
         Data : Opaque
            with Size => 8 * Len;
      end message;

   generic
      Transport : Channel with Readable, Writable;
   session S with
      Initial => Receive,
      Final => Done
   is
      Request : Request;
      Response : Response;
      Alg_Len : Alg_Len := (Alg1 => 1, Alg2 => 2, Alg3 => 4);
   begin
      state Receive is
      begin
         Transport'Read (Request);
      transition
         goto Done
            if Request'Valid /= True
         goto Prepare_Response
      end Receive;

      state Prepare_Response
      is
      begin
         Response := Response'(Len => Alg_Len (Request.Alg),
                               Data => [1]);
      transition
         goto Send_Response
      exception
         goto Done
      end Prepare_Response;

      state Send_Response is
      begin
         Transport'Write (Response);
      transition
         goto Done
      end Send_Response;

      state Done is null state;
   end S;

end Test;

+ Concise + Intent conveyed clearly + Potentially easy to translate into SPARK (using arrays) + Totality can be enforced + Efficient − Reusability questionable

O6

Introduce expression functions and case expressions:

package Test is

   type Alg is (Alg1,  -- 1 byte response
                Alg2,  -- 2 byte response
                Alg3)  -- 4 byte response
      with Size => 8;
   type Len is mod 2 ** 16;

   function Alg_Len (Alg : Alg) return Len is (case Alg is
                                               when Alg1 => 1,
                                               when Alg2 => 2,
                                               when Alg3 => 4);

   type Request is
      message
         Alg : Alg;
      end message;

   type Response (Len : Len) is
      message
         Data : Opaque
            with Size => 8 * Len;
      end message;

   generic
      Transport : Channel with Readable, Writable;
   session S with
      Initial => Receive,
      Final => Done
   is
      Request : Request;
      Response : Response;
   begin
      state Receive is
      begin
         Transport'Read (Request);
      transition
         goto Done
            if Request'Valid /= True
         goto Prepare_Response
      end Receive;

      state Prepare_Response
      is
      begin
         Response := Response'(Len => Alg_Len (Request.Alg),
                               Data => [1]);
      transition
         goto Send_Response
      exception
         goto Done
      end Prepare_Response;

      state Send_Response is
      begin
         Transport'Write (Response);
      transition
         goto Done
      end Send_Response;

      state Done is null state;
   end S;

end Test;

+ Concise + Intent conveyed clearly + Totality can be enforced + Efficient + Reusable + Expressive − May be overkill for problem to solve

O7a

Introduce a dedicated mapping type:

package Test is

   type Alg is (Alg1,  -- 1 byte response
                Alg2,  -- 2 byte response
                Alg3)  -- 4 byte response
      with Size => 8;
   type Len is mod 2 ** 16;

   for Alg use mapping Alg_Len to Len is (Alg1 => 1,
                                          Alg2 => 2,
                                          Alg3 => 4);
end Test;

O7b

Introduce a dedicated mapping type:

package Test is

   type Alg is (Alg1,  -- 1 byte response
                Alg2,  -- 2 byte response
                Alg3)  -- 4 byte response
      with Size => 8;
   type Len is mod 2 ** 16;

   mapping Alg_Len (Alg) to Len is 
      (Alg1 => 1,
       Alg2 => 2,
       Alg3 => 4);

end Test;

+ Concise + Intent conveyed clearly + Potentially easy to translate into SPARK (using arrays) + Totality can be enforced + Efficient − Not reusable − Unusual syntax − Two new keywords for one new feature

Decision Outcome

O6

sttaft commented 2 years ago

FWIW, the list comprehension syntax does not match that provided by Ada 2022 "filters" -- filters use "when M.Alg = Request_Alg" rather than "if ...", hence "[for M in Maps when M.Alg = Request.Alg => M];" This also might not produce exactly one result.

The "dedicated mapping type" could use Ada 2022 syntax for container aggregates (these use "[...]" rather than "(...)") and Ada 2012 syntax for indexing and be supported by SPARK directly. Not sure what you mean by "reusability" concerns.

A simple array aggregate would seem to be the simplest, however, in that that provides totality and efficiency.

treiher commented 2 years ago

@sttaft Thanks for your input!

FWIW, the list comprehension syntax does not match that provided by Ada 2022 "filters" -- filters use "when M.Alg = Request_Alg" rather than "if ...", hence "[for M in Maps when M.Alg = Request.Alg => M];" This also might not produce exactly one result.

We actually changed syntax for list comprehensions in the meantime to be more consistent to Ada 2022 (cf. #702), although we decided to still deviate by using the if keyword instead of when. when would have been a new keyword for the RecordFlux language, and we did not see a good reason for introducing when just for comprehensions.

The "dedicated mapping type" could use Ada 2022 syntax for container aggregates (these use "[...]" rather than "(...)") and Ada 2012 syntax for indexing and be supported by SPARK directly. Not sure what you mean by "reusability" concerns.

The concern is that we are adding this new language construct just for this very specific issue. I think newly added feature should ideally cover multiple use cases.

A simple array aggregate would seem to be the simplest, however, in that that provides totality and efficiency.

Do you propose adding an array type similar to Ada? That is not yet part of the language, but we could certainly consider it as an option.

AdaCore / RecordFlux