* Type Transcriptions
@ 2014-04-21 7:21 Shark8
2014-04-21 16:54 ` Brad Moore
0 siblings, 1 reply; 9+ messages in thread
From: Shark8 @ 2014-04-21 7:21 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Type Transcriptions
2014-04-21 7:21 Type Transcriptions Shark8
@ 2014-04-21 16:54 ` Brad Moore
2014-04-21 18:11 ` Yannick Duchêne (Hibou57)
0 siblings, 1 reply; 9+ messages in thread
From: Brad Moore @ 2014-04-21 16:54 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Type Transcriptions
2014-04-21 16:54 ` Brad Moore
@ 2014-04-21 18:11 ` Yannick Duchêne (Hibou57)
2014-04-21 18:51 ` Shark8
0 siblings, 1 reply; 9+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2014-04-21 18:11 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Type Transcriptions
2014-04-21 18:11 ` Yannick Duchêne (Hibou57)
@ 2014-04-21 18:51 ` Shark8
2014-04-21 19:42 ` Jeffrey Carter
2014-04-21 20:33 ` Ludovic Brenta
0 siblings, 2 replies; 9+ messages in thread
From: Shark8 @ 2014-04-21 18:51 UTC (permalink / raw)
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."
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Type Transcriptions
2014-04-21 18:51 ` Shark8
@ 2014-04-21 19:42 ` Jeffrey Carter
2014-04-22 6:06 ` Shark8
2014-04-21 20:33 ` Ludovic Brenta
1 sibling, 1 reply; 9+ messages in thread
From: Jeffrey Carter @ 2014-04-21 19:42 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Type Transcriptions
2014-04-21 18:51 ` Shark8
2014-04-21 19:42 ` Jeffrey Carter
@ 2014-04-21 20:33 ` Ludovic Brenta
2014-04-21 22:46 ` Adam Beneschan
2014-04-22 8:57 ` Shark8
1 sibling, 2 replies; 9+ messages in thread
From: Ludovic Brenta @ 2014-04-21 20:33 UTC (permalink / raw)
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.
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Type Transcriptions
2014-04-21 20:33 ` Ludovic Brenta
@ 2014-04-21 22:46 ` Adam Beneschan
2014-04-22 8:57 ` Shark8
1 sibling, 0 replies; 9+ messages in thread
From: Adam Beneschan @ 2014-04-21 22:46 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Type Transcriptions
2014-04-21 19:42 ` Jeffrey Carter
@ 2014-04-22 6:06 ` Shark8
0 siblings, 0 replies; 9+ messages in thread
From: Shark8 @ 2014-04-22 6:06 UTC (permalink / raw)
[-- 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 --]
^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: Type Transcriptions
2014-04-21 20:33 ` Ludovic Brenta
2014-04-21 22:46 ` Adam Beneschan
@ 2014-04-22 8:57 ` Shark8
1 sibling, 0 replies; 9+ messages in thread
From: Shark8 @ 2014-04-22 8:57 UTC (permalink / raw)
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).
^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2014-04-22 8:57 UTC | newest]
Thread overview: 9+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2014-04-21 7:21 Type Transcriptions Shark8
2014-04-21 16:54 ` Brad Moore
2014-04-21 18:11 ` Yannick Duchêne (Hibou57)
2014-04-21 18:51 ` Shark8
2014-04-21 19:42 ` Jeffrey Carter
2014-04-22 6:06 ` Shark8
2014-04-21 20:33 ` Ludovic Brenta
2014-04-21 22:46 ` Adam Beneschan
2014-04-22 8:57 ` Shark8
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox