search

REPROSEC / dolev-yao-star-extrinsic

DY* with extrinsic proofs
https://reprosec.org/
Mozilla Public License 2.0
8 stars 0 forks source link

Decide (and document) on a convention for typeclass instance names #20

Closed TWal closed 1 month ago

TWal commented 1 month ago

Following a discussion on #19 with @cwaldm, we noticed a lack of consistent style for typeclass instance names, for example https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/6fe7c9d40a097a5bdb2622fe95a0ebf8e9df3f75/examples/nsl_pk/DY.Example.NSL.Protocol.Total.fst#L67 or https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/6fe7c9d40a097a5bdb2622fe95a0ebf8e9df3f75/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.fst#L26 .

It is not affecting the rest of the code too much because hopefully typeclass instances are resolved automatically by F*, but it would be nice to have some consistency across them.

cwaldm commented 1 month ago

I think, I slightly prefer the first version, that is "class" followed by "type", since this is the same order as for the actual instance declaration. (Arguably, for the above examples I might even include the bytes and write parseable_serializeable_bytes_message.)

cwaldm commented 1 month ago

What about classes that don't have a type argument? For example: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst#L103-L106 Following the convention, it should probably be protocol_invariants_nsl, so that the class name comes first again.

Independently of naming, I think every instance declaration should be explicit and name the class even if this is not strictly needed. For example: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst#L52-L55 should be changed to instance nsl_crypto_invs : crypto_invariants = ....

Is there a reason, why we have https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst#L17-L18 instead of the combined instance nsl_crypto_usages : crypto_usages = default_crypto_usages ?

TWal commented 1 month ago

I agree with you!

No, there is no reason why there is the val + instance, we could combine them.

TWal commented 1 month ago

Closed by #29.