search

REPROSEC / dolev-yao-star-extrinsic

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

Change argument order for bytes predicates? #33

Open cwaldm opened 1 month ago

cwaldm commented 1 month ago

I was wondering, whether it makes sense to change the order of arguments for some of the bytes predicates to support a readable use of infix notation.

I just read https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/07c8e3f07509c8a933cde446e48eaefc9eb9a695/src/core/DY.Core.Trace.Invariant.fst#L47 and needed some time to figure out what is knowable by what. My suggestion would be to change https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/07c8e3f07509c8a933cde446e48eaefc9eb9a695/src/core/DY.Core.Bytes.fst#L516 to val is_knowable_by: {|crypto_invariants|} -> trace -> bytes -> label -> prop so that we can write nicely 

content `is_knowable_by trace` label

And similarly for https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/07c8e3f07509c8a933cde446e48eaefc9eb9a695/src/core/DY.Core.Bytes.fst#L525 and https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/07c8e3f07509c8a933cde446e48eaefc9eb9a695/src/core/DY.Core.Bytes.fst#L531 if we change to bytes -> trace and trace -> bytes -> label respectively, we can write

content `is_publishable` trace
content `is_secret trace` label

The key predicates are a bit more debatable, but I could imagine changing, say, https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/07c8e3f07509c8a933cde446e48eaefc9eb9a695/src/core/DY.Core.Bytes.fst#L537 to val is_verification_key: {|crypto_invariants|} -> trace -> bytes -> (string & label) -> prop to write

content `is_verification_key trace` (string, label)

I know that all of the suggestions are contradicting our "most general argument first" guideline https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/07c8e3f07509c8a933cde446e48eaefc9eb9a695/CONTRIBUTING.md?plain=1#L65 but I think changing the order really helps readability (and not having to think about the argument ordering when calling the predicates -- for example, I don't think it is intuitive to start is_knowable_by with the label, or having the bytes as last argument for is_verification_key). I understand that the label is the most general thing from the perspective of the predicates, but when we call the functions we always have a fixed trace and rather use different labels than traces, so I think having trace as first argument is intuitive in some sense.

Another option would be to rename the predicates to something, where intuitively the label comes first. I can't think of good names though. Happy to discuss.

TWal commented 1 month ago

I agree that for is_knowable_by, the order you propose would have more aesthetics when used infix. Why not for is_secret, but for is_publishable it is weird that the trace is now on the right and not in the middle.

On proof engineering considerations, I think this would clearly be a step back, the line you mentioned in CONTRIBUTING is there for a reason, and was actually written with is_knowable_by in mind. The rationale for that convention is written just below https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/07c8e3f07509c8a933cde446e48eaefc9eb9a695/CONTRIBUTING.md?plain=1#L68-L70

We do use the curryfication on the bytes, meaning that it must be the last argument: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/07c8e3f07509c8a933cde446e48eaefc9eb9a695/src/lib/comparse/DY.Lib.Comparse.Glue.fst#L91 https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/07c8e3f07509c8a933cde446e48eaefc9eb9a695/examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst#L77-L78

The label being the first argument is also important I think, for example we could define is_publishable by curryfication:

let is_publishable = is_knowable_by public

Because the bytes must come last, and the label must come first, the trace has no choice but to be in the middle, hence I think the argument order of is_knowable_by should not be changed.

The example of is_publishable above also shows that the name is_knowable_by makes sense, as it reads in plain english when we remove the underscores.

On a higher-level, I think we are entering the realm of bikeshedding and we should concentrate our efforts (time and energy) on more important things. Some of the recent renamings were much needed because they were a clear improvement (e.g. #14), but for things that are a result of a compromise, I don't think it's worth spending much efforts on shifting the compromise. DY* cannot be 100% perfect for everyone, because everyone has a different notion of perfectness.