Type Transcriptions

Type Transcriptions

[Shark8]

I recently started a little project intended to implement TLS 1.2 in Ada 
2012 and SPARK; reading through the RFC and transcribing the types has 
been relatively straightforward.

However there is one hiccup; a certain class of record-type is dependent 
on the values in another record, yet distinctly separate; ex:


       struct {
          opaque nonce_explicit[SecurityParameters.record_iv_length];
          aead-ciphered struct {
              opaque content[TLSCompressed.length];
          };
       } GenericAEADCipher;

where SecurityParameters is

       struct {
           ConnectionEnd          entity;
           PRFAlgorithm           prf_algorithm;
           BulkCipherAlgorithm    bulk_cipher_algorithm;
           CipherType             cipher_type;
           uint8                  enc_key_length;
           uint8                  block_length;
           uint8                  fixed_iv_length;
           uint8                  record_iv_length;
           MACAlgorithm           mac_algorithm;
           uint8                  mac_length;
           uint8                  mac_key_length;
           CompressionMethod      compression_algorithm;
           opaque                 master_secret[48];
           opaque                 client_random[32];
           opaque                 server_random[32];
       } SecurityParameters;

Now I've already transcribed the SecurityParameters parameters record, 
but it seems to me that since these other types are dependent on the 
SecurityParameters, I could change it into a generic package with the 
record's current components being input parameters.

Any advice on which route to take would be greatly appreciated.

Re: Type Transcriptions

[Brad Moore]

On 14-04-21 01:21 AM, Shark8 wrote:
> I recently started a little project intended to implement TLS 1.2 in Ada
> 2012 and SPARK; reading through the RFC and transcribing the types has
> been relatively straightforward.
>
> However there is one hiccup; a certain class of record-type is dependent
> on the values in another record, yet distinctly separate; ex:
>
>
>        struct {
>           opaque nonce_explicit[SecurityParameters.record_iv_length];
>           aead-ciphered struct {
>               opaque content[TLSCompressed.length];
>           };
>        } GenericAEADCipher;
>
> where SecurityParameters is
>
>        struct {
>            ConnectionEnd          entity;
>            PRFAlgorithm           prf_algorithm;
>            BulkCipherAlgorithm    bulk_cipher_algorithm;
>            CipherType             cipher_type;
>            uint8                  enc_key_length;
>            uint8                  block_length;
>            uint8                  fixed_iv_length;
>            uint8                  record_iv_length;
>            MACAlgorithm           mac_algorithm;
>            uint8                  mac_length;
>            uint8                  mac_key_length;
>            CompressionMethod      compression_algorithm;
>            opaque                 master_secret[48];
>            opaque                 client_random[32];
>            opaque                 server_random[32];
>        } SecurityParameters;
>
> Now I've already transcribed the SecurityParameters parameters record,
> but it seems to me that since these other types are dependent on the
> SecurityParameters, I could change it into a generic package with the
> record's current components being input parameters.
>
> Any advice on which route to take would be greatly appreciated.

I'd suggest trying to make GenericAEADCipher a discriminated record 
type, with the two length values as the discriminants, and then the 
arrays are sized using the discriminants. No Generics needed.

Brad

Re: Type Transcriptions

[Yannick Duchêne (Hibou57)]

Le Mon, 21 Apr 2014 18:54:23 +0200, Brad Moore <brad.moore@shaw.ca> a  
écrit:

> I'd suggest trying to make GenericAEADCipher a discriminated record  
> type, with the two length values as the discriminants, and then the  
> arrays are sized using the discriminants. No Generics needed.
>
> Brad
>

I guess Shark8 would already have figured it if this could be as simple.  
He says this, which is important: “certain class of record-type is  
dependent on the values in another record, yet distinctly separate”. With  
two separated things, a discriminant is not applicable. Or may be I've not  
understood.

-- 
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Re: Type Transcriptions

[Shark8]

On 21-Apr-14 12:11, Yannick Duchêne (Hibou57) wrote:
> Le Mon, 21 Apr 2014 18:54:23 +0200, Brad Moore <brad.moore@shaw.ca> a
> écrit:
>
>> I'd suggest trying to make GenericAEADCipher a discriminated record
>> type, with the two length values as the discriminants, and then the
>> arrays are sized using the discriminants. No Generics needed.
>>
>> Brad
>>
>
> I guess Shark8 would already have figured it if this could be as simple.
> He says this, which is important: “certain class of record-type is
> dependent on the values in another record, yet distinctly separate”.
> With two separated things, a discriminant is not applicable. Or may be
> I've not understood.

You have the right of it.
Using discriminants is the natural way to do it, but doing so would (in 
actuality) break sticking to the spec as the record-type would have 
fields which don't exist in the spec.

I suppose the better way to phrase it is:
"Is it better to strictly stick to the spec, letting generic 
instantiation take care of these 'extra-typal' parameters, *OR* doing 
things the natural Ada way, and worrying about 'fixing-up' things in, 
say, 'Input and 'Output operations."

Re: Type Transcriptions

[Jeffrey Carter]

On 04/21/2014 11:51 AM, Shark8 wrote:
>
> I suppose the better way to phrase it is:
> "Is it better to strictly stick to the spec, letting generic instantiation take
> care of these 'extra-typal' parameters, *OR* doing things the natural Ada way,
> and worrying about 'fixing-up' things in, say, 'Input and 'Output operations."

My vote is for the Ada way, as long as the functionality is correct. Making it 
clear, easy to read and understand, and correct are the important things.

-- 
Jeff Carter
"I like it when the support group complains that they have
insufficient data on mean time to repair bugs in Ada software."
Robert I. Eachus
91

Re: Type Transcriptions

[Shark8]

[-- Attachment #1: Type: text/plain, Size: 1109 bytes --]

On 21-Apr-14 13:42, Jeffrey Carter wrote:
> On 04/21/2014 11:51 AM, Shark8 wrote:
>>
>> I suppose the better way to phrase it is:
>> "Is it better to strictly stick to the spec, letting generic
>> instantiation take
>> care of these 'extra-typal' parameters, *OR* doing things the natural
>> Ada way,
>> and worrying about 'fixing-up' things in, say, 'Input and 'Output
>> operations."
>
> My vote is for the Ada way, as long as the functionality is correct.
> Making it clear, easy to read and understand, and correct are the
> important things.

To be fair, going the generic-package route isn't necessarily /not/ the 
Ada way -- it's just not, IIUC, all that common. There's an interesting 
Technical Report [attached] on how generic-packages and records share a 
/lot/ of underlying ideas that are identical.

This would, however require some sort of mechanism to keep sessions 
associated with the Security_Parameters; this sort of situation is where 
something like package-pointers would be an interesting solution -- 
IIRC, Randy mentioned the idea as one of them as AI ideas that had been 
rejected.

[-- Attachment #2: www.cs.dartmouth.edu/reports/TR86-104.pdf --]
[-- Type: application/pdf, Size: 763193 bytes --]

Re: Type Transcriptions

[Ludovic Brenta]

Shark8 <OneWingedShark@gmail.com> writes:
> On 21-Apr-14 12:11, Yannick Duchêne (Hibou57) wrote:
>> Le Mon, 21 Apr 2014 18:54:23 +0200, Brad Moore <brad.moore@shaw.ca> a
>> écrit:
>>
>>> I'd suggest trying to make GenericAEADCipher a discriminated record
>>> type, with the two length values as the discriminants, and then the
>>> arrays are sized using the discriminants. No Generics needed.
>>>
>>> Brad
>>>
>>
>> I guess Shark8 would already have figured it if this could be as simple.
>> He says this, which is important: “certain class of record-type is
>> dependent on the values in another record, yet distinctly separate”.
>> With two separated things, a discriminant is not applicable. Or may be
>> I've not understood.
>
> You have the right of it.
> Using discriminants is the natural way to do it, but doing so would
> (in actuality) break sticking to the spec as the record-type would
> have fields which don't exist in the spec.
>
> I suppose the better way to phrase it is:
> "Is it better to strictly stick to the spec, letting generic
> instantiation take care of these 'extra-typal' parameters, *OR* doing
> things the natural Ada way, and worrying about 'fixing-up' things in,
> say, 'Input and 'Output operations."

Ada 2012 has a very nice new feature: unchecked unions (clause B.3.3);
it is a discriminated record with an aspect says that the discriminants
are *not* in the record, but stored elsewhere instead.  I have used them
in my tiny Ada binding to the X C binding (XCB), like so:

      type Detail_T (Response_Type : Response_Type_T := Reply) is record
         case Response_Type is
            when Key_Press | Key_Release =>
               Keycode : Interfaces.Unsigned_8;
            when Button_Press | Button_Release | Motion_Notify =>
               Detail  : Button_T;
            when others =>
               Padding : Interfaces.Unsigned_8;
         end case;
      end record
         with Unchecked_Union;

      type Response_T (Sent : Boolean; Response_Type : Response_Type_T) is
         record
            Detail   : Detail_T (Response_Type);
            [other components omitted]
         end record;
      for Response_T use record
         Sent          at 0 range 7 .. 7;
         Response_Type at 0 range 0 .. 6;
      end record;


This says that the Response_T has two discriminants, stored as the first
two components, and that the second discriminant, Response_Type, also
constrains the component Detail, but Detail does not contain a copy of
this discriminant.

This sounds awfully similar to the spec you're trying to implement :)

In this case, Ada 2012 saves the day!

-- 
Ludovic Brenta.

Re: Type Transcriptions

[Adam Beneschan]

On Monday, April 21, 2014 1:33:47 PM UTC-7, Ludovic Brenta wrote:
 
> In this case, Ada 2012 saves the day!

Maybe it saved the day in your case, but it's not applicable to the OP's needs.  Unchecked_Union is really only for variant records (since it was intended to provide a way to interface to C routines that need "union" types).  The rules say that Unchecked_Union may apply only to a variant record type, and the discriminant can't be used as a constraint on a component except for another Unchecked_Union record--definitely not on an array subtype which is what the OP would need.  (RM B.3.3(8))

Also, Unchecked_Unions were added in Ada 2005, not 2012.  (In Ada 2005, it was a pragma.)

                         -- Adam

Re: Type Transcriptions

[Shark8]

On 21-Apr-14 14:33, Ludovic Brenta wrote:
> Shark8 <OneWingedShark@gmail.com> writes:
>> On 21-Apr-14 12:11, Yannick Duchêne (Hibou57) wrote:
>>> Le Mon, 21 Apr 2014 18:54:23 +0200, Brad Moore <brad.moore@shaw.ca> a
>>> écrit:
>>>
>>>> I'd suggest trying to make GenericAEADCipher a discriminated record
>>>> type, with the two length values as the discriminants, and then the
>>>> arrays are sized using the discriminants. No Generics needed.
>>>>
>>>> Brad
>>>>
>>>
>>> I guess Shark8 would already have figured it if this could be as simple.
>>> He says this, which is important: “certain class of record-type is
>>> dependent on the values in another record, yet distinctly separate”.
>>> With two separated things, a discriminant is not applicable. Or may be
>>> I've not understood.
>>
>> You have the right of it.
>> Using discriminants is the natural way to do it, but doing so would
>> (in actuality) break sticking to the spec as the record-type would
>> have fields which don't exist in the spec.
>>
>> I suppose the better way to phrase it is:
>> "Is it better to strictly stick to the spec, letting generic
>> instantiation take care of these 'extra-typal' parameters, *OR* doing
>> things the natural Ada way, and worrying about 'fixing-up' things in,
>> say, 'Input and 'Output operations."
>
> Ada 2012 has a very nice new feature: unchecked unions (clause B.3.3);
> it is a discriminated record with an aspect says that the discriminants
> are *not* in the record, but stored elsewhere instead.  I have used them
> in my tiny Ada binding to the X C binding (XCB), like so:
>
>        type Detail_T (Response_Type : Response_Type_T := Reply) is record
>           case Response_Type is
>              when Key_Press | Key_Release =>
>                 Keycode : Interfaces.Unsigned_8;
>              when Button_Press | Button_Release | Motion_Notify =>
>                 Detail  : Button_T;
>              when others =>
>                 Padding : Interfaces.Unsigned_8;
>           end case;
>        end record
>           with Unchecked_Union;
>
>        type Response_T (Sent : Boolean; Response_Type : Response_Type_T) is
>           record
>              Detail   : Detail_T (Response_Type);
>              [other components omitted]
>           end record;
>        for Response_T use record
>           Sent          at 0 range 7 .. 7;
>           Response_Type at 0 range 0 .. 6;
>        end record;
>
>
> This says that the Response_T has two discriminants, stored as the first
> two components, and that the second discriminant, Response_Type, also
> constrains the component Detail, but Detail does not contain a copy of
> this discriminant.
>
> This sounds awfully similar to the spec you're trying to implement :)
>
> In this case, Ada 2012 saves the day!
>

Thanks for the info.
Unfortunately it is of no help: the [non-]discriminant cannot be used to 
set the length of the internal 'vector' (the array).