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.

However, the property we have in SMT patterns is has_local_state_predicate

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

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:

Why this is a problem?

Looking more closely at

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.