names of split predicate input types

[cwaldm]

The comments are not matching the use of the types: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/028a6d86f7d5016b9e91ec4e857c025faa4e39f6/src/lib/utils/DY.Lib.SplitPredicate.fst#L62-L65

It seems that raw_data_t is used for local predicates and labeled_data_t for global predicates.

Which leads to a second question: Why are the types called this way? And not for example (and maybe more intuitively) local_data_t and global_data_t or local_input_t / global_input_t?

On the other hand, I don't fully understand the meaning of global, local and top-level in this part as well (so local and global are maybe not as intuitive) https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/028a6d86f7d5016b9e91ec4e857c025faa4e39f6/src/lib/utils/DY.Lib.SplitPredicate.fst#L21-L24

[TWal]

Ah you are right, the two comments should be exchanged.

The idea behind the names is that the input for the global predicate contains both a label and some other (un-labeled, or "raw") data. Therefore it is "labeled data".

Here is a diagram:

      (global input)
       labeled data
<----------------------->
<-------><-------------->
  label      raw data
           (local input)

Your proposition is more intuitive with regard to what input is used with what predicate, but it might be less intuitive with regard to what input contains the label, and what input is unlabelled. But we can change it like this if you prefer!

Regarding the comment between local, global and top-level, a good example is the pki.

The protocols_invariant instance is not defined at the top-level (i.e. with a val and let), but is a parameter of the theorems on pki functions: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/028a6d86f7d5016b9e91ec4e857c025faa4e39f6/src/lib/state/DY.Lib.State.PKI.fst#L120 and there is a precondition relating the local predicate and the protocol invariants: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/028a6d86f7d5016b9e91ec4e857c025faa4e39f6/src/lib/state/DY.Lib.State.PKI.fst#L126 therefore, you can use this theorem on any protocol invariants that was constructed with this local invariant inside.

Is it clarifying the situation?

[cwaldm]

local, global, top-level

I think, I understand the idea that the PKI functions don't have to care about all of the invariants, but they are only concerned with the predicates local to the PKI "layer" (which are somehow contained in the global invariants). Is that the right intuition of what local and global refer to? I.e., local means local to each layer (for example some predicates for PKI, or some predicates for the communication layer ...), whereas global refers to the overall collection of the local predicates on the protocol layer (thereby specifying which stack of layers the protocol is built on)?

But what is "top-level" then referring to? Isn't the protocol layer top-level where we have the global invariants?

Also, looking at https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/028a6d86f7d5016b9e91ec4e857c025faa4e39f6/src/lib/state/DY.Lib.State.Labeled.fst#L43-L71 I don't fully understand the difference of apply_local_pred and apply_global_pred. And related: what is the difference of session_pred and state_predicate ? (But maybe this discussion should move to a separate issue about the split predicate method.)

labeled data

I think the term "labeled data" is confusing, since we also use "label" for the intended audiences (knowable_by ...) which are not what we mean here, right? Maybe "tagged" is a better fit here (which also appears in some of the comments)?

[TWal]

I think, I understand the idea that the PKI functions don't have to care about all of the invariants, but they are only concerned with the predicates local to the PKI "layer" (which are somehow contained in the global invariants). Is that the right intuition of what local and global refer to?

Yes, exactly!

But what is "top-level" then referring to? Isn't the protocol layer top-level where we have the global invariants?

Sorry for the confusing terminology, I mean "top-level" as something defined at the top of a file, that every function can refer to, using val and let, as opposed to "local" variables that are available only within the scope of one function. (Here, "local" is about the programming language terminology, not about the predicates, I hope it is not more confusing!)

One proof style would be to define the protocols invariants at the top-level, so that every lemma can access it, and because it hopefully has many good properties we can prove every function used in the protocol (e.g. the PKI functions, the protocol functions, etc). Another proof style, which is the one suggested by the comment, is to parametrize the various lemmas with any protocol invariants, as long as it satisfies a precondition (e.g. has_pki_invariants). Then, if we construct protocol invariants that satisfy all the preconditions, it will be usable by all the lemmas we need.

In the NSL example, this good protocol_invariants is constructed here: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/34f51ea6f12d1c7eacc1776a50e43a51112bb1dd/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst#L84-L106

What may be confusing is that the NSL example uses a hybrid proof style, where this protocol invariant is used as an argument to the PKI lemmas (because it satisfies the correct precondition), and is referenced as a top-level protocol invariants in the NSL proofs. But we could change the NSL proofs to be parametric in any protocol invariants that satisfy a precondition like has_typed_session_pred nsl_protocol_invs (nsl_session_label, nsl_session_pred).

I hope this is clarifying things? Please let me know if it isn't.

I don't fully understand the difference of apply_local_pred and apply_global_pred.

I agree that they look very similar! Maybe the split predicate for events is easier to understand: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/34f51ea6f12d1c7eacc1776a50e43a51112bb1dd/src/lib/event/DY.Lib.Event.Typed.fst#L60-L65 In the event predicate, the global predicate has a tag (which is a string depicting which type of event is triggered) and some event content (which is a bytes), whereas the local predicate only deals with the event content (the bytes).

In the state predicate, the difference is that in apply_global_pred the bytes contains a serialization of this type: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/028a6d86f7d5016b9e91ec4e857c025faa4e39f6/src/lib/state/DY.Lib.State.Labeled.fst#L13-L18 whereas in apply_local_pred, the bytes contains the content field of the above type, similar to the event predicate.

And related: what is the difference of session_pred and state_predicate ? (But maybe this discussion should move to a separate issue about the split predicate method.)

I guess they are roughly the same, the "state" vs "session" should be uniformised as discussed in #6. Otherwise, session_pred is a local state predicate, whereas state_predicate is a global state predicate. The names should be changed to reflect this meaning, you are right that they are unclear as-is. I opened issue #15.

I think the term "labeled data" is confusing, since we also use "label" for the intended audiences (knowable_by ...) which are not what we mean here, right? Maybe "tagged" is a better fit here (which also appears in some of the comments)?

I agree, it should be done to clean up the code, I opened the issue #14.

About the "layer" terminology, and the culinary metaphore

In the case of the split predicate, I wouldn't talk about "layers" like a lasagna, because it conveys the idea that there is an order on the different layers, i.e. the ones at the bottom and the ones at the top.

I would rather use a metaphore with raviolis: the NSL proof relies on three different raviolis, the PKI ravioli, the PrivateKeys ravioli, and the NSL session ravioli, which are independent of each other.

But maybe this consideration should be left as separate discussion!

[cwaldm]

Thanks! I now understand the local and global predicates a bit better. And I prefer the parameterized style, you suggested.

I think, if we swap the comments for the "data" types, https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/a078d683c92c1cf8b9d1dc00f0a6a3925b2b86cd/src/lib/utils/DY.Lib.SplitPredicate.fst#L62-L65 and add some more description to https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/a078d683c92c1cf8b9d1dc00f0a6a3925b2b86cd/src/lib/utils/DY.Lib.SplitPredicate.fst#L21-L24 (in particular, clarifying what top-level means), we can close this issue and continue the various other discussions that came up in separate issues.

[TWal]

Closed by #26