cleanup: reduce boilerplate to merge local predicates

[TWal]

Fixes #37 .

Writing a thorough explanation of what is happening because this is quite subtle!

Adding unfolds

The main problem we had is that the correctness theorem for merging local predicates ensures the has_local_bytes_state_predicate property on the protocol invariants.

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

Lines 83 to 88 in f8a8c8b

	val mk_global_local_bytes_state_predicate_correct: invs:protocol_invariants -> lpreds:list (string & local_bytes_state_predicate) -> Lemma
	(requires
	invs.trace_invs.state_pred.pred == mk_global_local_bytes_state_predicate lpreds /\
	List.Tot.no_repeats_p (List.Tot.map fst lpreds)
	)
	(ensures for_allP (has_local_bytes_state_predicate invs) lpreds)

However, the property we have in SMT patterns is has_local_state_predicate

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

Line 113 in f8a8c8b

SMTPat (has_local_state_predicate invs spred)]

or has_pki_invariant

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

Line 116 in f8a8c8b

SMTPat (has_pki_invariant invs);

These higher-level properties on the global protocol invariants are ultimately defined using has_local_bytes_state_predicate, e.g.

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

Lines 67 to 68 in f8a8c8b

	let has_local_state_predicate #a #ls invs spred =
	has_local_bytes_state_predicate invs (ls.tag, (local_state_predicate_to_local_bytes_state_predicate spred))

The main trick used in this pull-request is to add the unfold keyword to these higher-level properties, as illustrated in the following minimal example:

assume val protocol_invariants: Type0

// p_low is similar to `has_local_bytes_state_predicate`
assume val p_low: protocol_invariants -> prop
// q is any property that would have p_low as precondition
assume val q: protocol_invariants -> prop

// p_high is similar to `has_local_state_predicate`
unfold // note the unfold!
val p_high: protocol_invariants -> prop
let p_high invs = p_low invs

// we have a theorem that has an SMT pattern with `p_high`
assume val p_low_implies_q:
  invs:protocol_invariants ->
  Lemma
  (requires p_high invs)
  (ensures q invs)
  [SMTPat (p_high invs)]
  // the SMT pattern is unfolded to
  // [SMTPat (p_low invs)]

// but the squashed theorem we have in scope is on p_low
assume val global_invs: protocol_invariants
assume val p_low_global_invs: squash (p_low global_invs)

let test () =
  // Thanks to the unfold, the SMT pattern is triggered!
  assert(q global_invs)

Ensuring uniqueness of typeclass resolution for parseable_serializeable

On the example of NSL, the message format for nsl_session could be obtained in two ways.

First, via the direct parseable_serializeable instance:

dolev-yao-star-extrinsic/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.fst

Lines 26 to 27 in f8a8c8b

	instance parseable_serializeable_bytes_nsl_session: parseable_serializeable bytes nsl_session
	= mk_parseable_serializeable ps_nsl_session

Second, via the local_state instance

dolev-yao-star-extrinsic/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.fst

Lines 29 to 32 in f8a8c8b

	instance local_state_nsl_session: local_state nsl_session = {
	tag = "NSL.Session";
	format = parseable_serializeable_bytes_nsl_session;
	}

which defines parseable_serializeable as a sub-typeclass

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

Lines 8 to 12 in f8a8c8b

	class local_state (a:Type0) = {
	tag: string;
	[@@@FStar.Tactics.Typeclasses.tcinstance]
	format: parseable_serializeable bytes a;
	}

Why this is a problem?

Looking more closely at

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

Lines 40 to 43 in f8a8c8b

	val local_state_predicate_to_local_bytes_state_predicate:
	{|crypto_invariants|} ->
	#a:Type -> {|parseable_serializeable bytes a|} ->
	local_state_predicate a -> local_bytes_state_predicate

we see that it is parametrized by a parseable_serializeable typeclass instance.
Therefore, resolving the implicits of

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

Lines 67 to 68 in f8a8c8b

	let has_local_state_predicate #a #ls invs spred =
	has_local_bytes_state_predicate invs (ls.tag, (local_state_predicate_to_local_bytes_state_predicate spred))

we obtain

let has_local_state_predicate #a #ls invs spred =
  has_local_bytes_state_predicate invs (ls.tag, (local_state_predicate_to_local_bytes_state_predicate #invs.crypto_invs #a #ls.format spred))

if we prove the same thing, but replace #ls.format with the direct instance of parseable_serializeable, then it will not match the correct SMT pattern!
This is why only having one instance is useful, eventhough all typeclass instances we obtain are equal (by reduction).

Un-inline the tag of map types

For the same reason of trying to match closely the final unfolded value, in map states we must use for the tag (local_state_map pki_key pki_value).tag instead of map_types_pki.tag (even though they are equal by reduction)

One last issue

I noticed that the normalization trick we use in the examples do not work well when we only have one predicate… I opened FStarLang/FStar#3353 about that.
In the meantime, adding a dummy event predicate works as a workaround.

[TWal]

Now that the F* issue is fixed, I think this is working well. There is still FStarLang/FStar#3360, but it's fine (we need a fuel/ifuel of 1 when we only have one local predicate).

Now, the boilerplate is 5 LoC per global predicate (right now we have 2, the state predicate and event predicate), whereas before we also had these 5 LoC and additional 2 LoC per local predicate (and there can be many).

The next steps would be to simplify the 5 LoC boilerplate per global predicate, for that I guess we would need to meta-program something…

[fabian-hk]

This looks very good and makes the code much cleaner! I have only one question above, and then it can be merged from my perspective.

[TWal]

I think this is close to the least amount of boilerplate we can have without tactics, I will still try a tactic-based version before merging, because this goes in a different direction, then we can compare and choose the best one!

[fabian-hk]

@TWal, what is the status of this PR? I think it is a significant improvement over the current version, and we can merge it.

[TWal]

It seems to be working well but I am a bit scared that the SMT patterns are quite big, and I have no idea whether that scales or not when protocols get bigger (hence SMT patterns also get bigger). So before that I wanted to test other directions, one is a tactic-based version (I have a proof-of-concept locally but I'm afraid it is not general enough), another is #49. If we choose the direction of this current PR, I guess we should at least ask F* folks whether having big SMT patterns is something to be worried about or not.