Re: Type Transcriptions

[Brad Moore <brad.moore@shaw.ca>]

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