search

REPROSEC / dolev-yao-star-extrinsic

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

Do a holistic renaming of the various predicates #22

Open TWal opened 1 month ago

TWal commented 1 month ago

As noticed by @cwaldm when discussing on #19, we have many predicate types and it would be nice to have some consistency between them.

I think in general the types are named foo_predicate, and the predicate is named either:

There is also the question of predicate vs invariant. I think I tried to use predicate for types that actually contain the predicates, and invariant for things that are more collection of predicates.

In Core: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/src/core/DY.Core.Bytes.fst#L237-L267 https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/src/core/DY.Core.Trace.Invariant.fst#L30-L50 https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/src/core/DY.Core.Trace.Invariant.fst#L54-L58 https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/src/core/DY.Core.Trace.Invariant.fst#L66-L70

In DY.Lib.Event: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/src/lib/event/DY.Lib.Event.Typed.fst#L41-L42

In DY.Lib.State: https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/src/lib/state/DY.Lib.State.Tagged.fst#L25-L41 https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/src/lib/state/DY.Lib.State.Typed.fst#L22-L38 https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/src/lib/state/DY.Lib.State.Map.fst#L27-L37

In particular, @cwaldm proposed to rename state_predicate into global_state_predicate to oppose it to local_state_predicate. I would rather keep the names of DY.Core agnostic to what is done in DY.Lib and keep the name as-is, but add some documentation above state_predicate to explain that it is a global predicate and that separating it into several local state predicates is done in DY.Lib.

cwaldm commented 1 month ago

I also wondered about predicate and invariant. I prefer to have only one of those, since I don't really see a difference. After all, they are all invariants, right? (For all of the above we even have explicit *_pred_later Lemmas.) Or is the idea, that a predicate is just a predicate and only becomes an invariant in combination with the pred_later lemma? In which case, we should only be using preds, and maybe rename those lemmas to something like pred_is_invariant? But then I'd like to call containers of preds together with a pred_later lemma invariants, e.g., the crypto_predicates in Core.Bytes only contain predicates that are acutally invariants, so I'd call them crypto_invariants instead. I guess the question is: do we have predicates that are not invariants?

Maybe, we can even define an invariant typeclass consisting of a predicate and the later lemma and make all of the above (aead_pred, sign_pred, state_pred...) instances of this class? (So that we don't have to explicitly write the later lemmas manually.)

For the core state_predicate: I agree, that the core library shouldn't need to look at the libraries on top of it. So yes, we should probably keep the name as is. But adding a comment above it is useful. I also would like to add a comment before the local_state_predicate to reference back to the core global pred and highlight the difference there (again).

qaphla commented 1 month ago

I would argue that our crypto predicates (e.g., aead_pred) are not invariants, at least not in the same sense as the other ones, in that they don't say anything at the trace level. I suppose they're a bytes-level invariant of sorts, but even then, I think the actual invariant is something derived from aead_pred, rather than aead_pred itself --- in particular, I guess I would say that the corresponding invariant to aead_pred is the AeadEnc case of bytes_invariant:

https://github.com/REPROSEC/dolev-yao-star-extrinsic/blob/452210f88ac1180710f93ebecbb6394e38b970fa/src/core/DY.Core.Bytes.fst#L328-L355

Specifically, lines 339-355.

Packaging an invariant with its later lemma makes sense to me, though I'm not sure how we'd avoid writing the later lemma in doing so, unless you mean avoiding needing to call it so much (which is also good).

TWal commented 1 month ago

@qaphla Good catch. Indeed, it looks like we could renaming everything "invariant" except the "crypto predicates".

@cwaldm To use a generic "predicate that is preserved by trace extension" type, we would need to uncurry all the predicates, e.g. the state invariant would become trace -> (principal & nat & bytes) -> prop instead of the current trace -> principal -> nat -> bytes -> prop. I don't think it's worth trying to factorize this too much, I think the actual state of things is readable enough, and it would only benefit the crypto predicates, because all the state invariants also have the pred_knowable constraint that is difficult to generalize.