Do a holistic renaming of the various predicates

[TWal]

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:

• bar_pred, baz_pred when there are several sub-predicates
• pred when there is only one predicate

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:

dolev-yao-star-extrinsic/src/core/DY.Core.Bytes.fst

Lines 237 to 267 in 452210f

	noeq
	type crypto_predicates (cusages:crypto_usages) = {
	aead_pred: tr:trace -> key:bytes{AeadKey? (get_usage key)} -> nonce:bytes -> msg:bytes -> ad:bytes -> prop;
	aead_pred_later:
	tr1:trace -> tr2:trace ->
	key:bytes{AeadKey? (get_usage key)} -> nonce:bytes -> msg:bytes -> ad:bytes ->
	Lemma
	(requires aead_pred tr1 key nonce msg ad /\ tr1 <$ tr2)
	(ensures aead_pred tr2 key nonce msg ad)
	;
	pkenc_pred: tr:trace -> pk:bytes{PkdecKey? (get_sk_usage pk)} -> msg:bytes -> prop;
	pkenc_pred_later:
	tr1:trace -> tr2:trace ->
	pk:bytes{PkdecKey? (get_sk_usage pk)} -> msg:bytes ->
	Lemma
	(requires pkenc_pred tr1 pk msg /\ tr1 <$ tr2)
	(ensures pkenc_pred tr2 pk msg)
	;
	sign_pred: tr:trace -> vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes -> prop;
	sign_pred_later:
	tr1:trace -> tr2:trace ->
	vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes ->
	Lemma
	(requires sign_pred tr1 vk msg /\ tr1 <$ tr2)
	(ensures sign_pred tr2 vk msg)
	;
	// ...
	}

dolev-yao-star-extrinsic/src/core/DY.Core.Trace.Invariant.fst

Lines 30 to 50 in 452210f

	noeq
	type state_predicate (cinvs:crypto_invariants) = {
	pred: trace -> principal -> nat -> bytes -> prop;
	// TODO: Do we want the later lemma?
	pred_later:
	tr1:trace -> tr2:trace ->
	prin:principal -> sess_id:nat -> content:bytes ->
	Lemma
	(requires pred tr1 prin sess_id content /\ tr1 <$ tr2)
	(ensures pred tr2 prin sess_id content)
	;
	pred_knowable:
	tr:trace ->
	prin:principal -> sess_id:nat -> content:bytes ->
	Lemma
	(requires pred tr prin sess_id content)
	(ensures
	is_knowable_by (principal_state_label prin sess_id) tr content
	)
	;
	}

dolev-yao-star-extrinsic/src/core/DY.Core.Trace.Invariant.fst

Lines 54 to 58 in 452210f

	noeq
	type trace_invariants (cinvs:crypto_invariants) = {
	state_pred: state_predicate cinvs;
	event_pred: trace -> principal -> string -> bytes -> prop;
	}

dolev-yao-star-extrinsic/src/core/DY.Core.Trace.Invariant.fst

Lines 66 to 70 in 452210f

	class protocol_invariants = {
	[@@@FStar.Tactics.Typeclasses.tcinstance]
	crypto_invs: crypto_invariants;
	trace_invs: trace_invariants crypto_invs;
	}

In DY.Lib.Event:

dolev-yao-star-extrinsic/src/lib/event/DY.Lib.Event.Typed.fst

Lines 41 to 42 in 452210f

	type event_predicate (a:Type0) {|event a|} =
	trace -> principal -> a -> prop

In DY.Lib.State:

dolev-yao-star-extrinsic/src/lib/state/DY.Lib.State.Tagged.fst

Lines 25 to 41 in 452210f

	noeq
	type local_bytes_state_predicate {|crypto_invariants|} = {
	pred: trace -> principal -> nat -> bytes -> prop;
	pred_later:
	tr1:trace -> tr2:trace ->
	prin:principal -> sess_id:nat -> content:bytes ->
	Lemma
	(requires pred tr1 prin sess_id content /\ tr1 <$ tr2)
	(ensures pred tr2 prin sess_id content)
	;
	pred_knowable:
	tr:trace -> prin:principal -> sess_id:nat -> content:bytes ->
	Lemma
	(requires pred tr prin sess_id content)
	(ensures is_knowable_by (principal_state_label prin sess_id) tr content)
	;
	}

dolev-yao-star-extrinsic/src/lib/state/DY.Lib.State.Typed.fst

Lines 22 to 38 in 452210f

	noeq
	type local_state_predicate {|crypto_invariants|} (a:Type) {|parseable_serializeable bytes a|} = {
	pred: trace -> principal -> nat -> a -> prop;
	pred_later:
	tr1:trace -> tr2:trace ->
	prin:principal -> sess_id:nat -> content:a ->
	Lemma
	(requires pred tr1 prin sess_id content /\ tr1 <$ tr2)
	(ensures pred tr2 prin sess_id content)
	;
	pred_knowable:
	tr:trace -> prin:principal -> sess_id:nat -> content:a ->
	Lemma
	(requires pred tr prin sess_id content)
	(ensures is_well_formed _ (is_knowable_by (principal_state_label prin sess_id) tr) content)
	;
	}

dolev-yao-star-extrinsic/src/lib/state/DY.Lib.State.Map.fst

Lines 27 to 37 in 452210f

	noeq type map_predicate {|crypto_invariants|} (key_t:eqtype) (value_t:Type0) {|mt:map_types key_t value_t|} = {
	pred: trace -> principal -> nat -> key_t -> value_t -> prop;
	pred_later: tr1:trace -> tr2:trace -> prin:principal -> sess_id:nat -> key:key_t -> value:value_t -> Lemma
	(requires pred tr1 prin sess_id key value /\ tr1 <$ tr2)
	(ensures pred tr2 prin sess_id key value)
	;
	pred_knowable: tr:trace -> prin:principal -> sess_id:nat -> key:key_t -> value:value_t -> Lemma
	(requires pred tr prin sess_id key value)
	(ensures is_well_formed_prefix mt.ps_key_t (is_knowable_by (principal_state_label prin sess_id) tr) key /\ is_well_formed_prefix mt.ps_value_t (is_knowable_by (principal_state_label prin sess_id) tr) value)
	;
	}

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]

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]

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:

dolev-yao-star-extrinsic/src/core/DY.Core.Bytes.fst

Lines 328 to 355 in 452210f

	| AeadEnc key nonce msg ad ->
	bytes_invariant tr key /\
	bytes_invariant tr nonce /\
	bytes_invariant tr msg /\
	bytes_invariant tr ad /\
	// the nonce is a public value
	// (e.g. it is often transmitted on the network)
	(get_label nonce) `can_flow tr` public /\
	// the standard IND-CCA assumption do not guarantee indistinguishability of additional data,
	// hence it must flow to public
	(get_label ad) `can_flow tr` public /\
	(
	(
	// Honest case:
	// - the key has the usage of AEAD key
	AeadKey? (get_usage key) /\
	// - the custom (protocol-specific) invariant hold (authentication)
	cinvs.preds.aead_pred tr key nonce msg ad /\
	// - the message is less secret than the key
	// (this is crucial so that decryption preserve publishability)
	(get_label msg) `can_flow tr` (get_label key)
	) \/ (
	// Attacker case:
	// the key and message are both public
	(get_label key) `can_flow tr` public /\
	(get_label msg) `can_flow tr` public
	)
	)

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]

@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.