From e11a6072b9c3090f4dfd27d0af7a6c2af39f3ab2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= <theophile@wallez.net>
Date: Mon, 23 Sep 2024 15:56:10 +0200
Subject: [PATCH] feat: make labels erasable (#54)

* feat: make labels erasable

* add unknown label

* improve user interface of `enable_bytes_well_formed_smtpats`
---
 .../DY.Example.DH.Protocol.Stateful.Proof.fst |   6 +-
 .../DY.Example.DH.Protocol.Total.Proof.fst    |   8 +-
 .../DY.Example.DH.SecurityProperties.fst      |   4 +-
 ...DY.Example.NSL.Protocol.Stateful.Proof.fst |   8 +-
 .../DY.Example.NSL.Protocol.Total.Proof.fst   |  16 +-
 src/core/DY.Core.Bytes.Type.fst               |  13 +-
 src/core/DY.Core.Bytes.fst                    | 948 ++++++++++++++----
 src/core/DY.Core.Label.Type.fst               |  46 +-
 src/core/DY.Core.Label.Unknown.fst            |   3 +
 src/core/DY.Core.Label.Unknown.fsti           |  15 +
 src/core/DY.Core.Trace.Manipulation.fst       |  15 +-
 src/core/DY.Core.Trace.Type.fst               |   6 +-
 src/lib/comparse/DY.Lib.Comparse.Glue.fst     |  13 +
 src/lib/crypto/DY.Lib.Crypto.AEAD.Split.fst   |   7 +
 .../DY.Lib.Crypto.PkEncryption.Split.fst      |   5 +
 .../crypto/DY.Lib.Crypto.Signature.Split.fst  |   5 +
 .../crypto/DY.Lib.Crypto.SplitPredicate.fst   |  13 +-
 src/lib/hpke/DY.Lib.HPKE.Lemmas.fst           |  47 +-
 src/lib/hpke/DY.Lib.HPKE.Split.fst            |   6 +
 src/lib/utils/DY.Lib.Printing.fst             |  19 +-
 20 files changed, 908 insertions(+), 295 deletions(-)
 create mode 100644 src/core/DY.Core.Label.Unknown.fst
 create mode 100644 src/core/DY.Core.Label.Unknown.fsti

diff --git a/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst
index f572055..cfa577c 100644
--- a/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst
+++ b/examples/iso_dh/DY.Example.DH.Protocol.Stateful.Proof.fst
@@ -19,7 +19,7 @@ let is_dh_shared_key tr alice bob k = exists si sj.
   // the label is either ``join (principal_state_label alice si) (principal_state_label bob sj)`` or
   // ``join (principal_state_label bob sj) (principal_state_label alice si)``.
   // This is because k is either build from ``dh x (dh_pk y)`` or ``dh y (dh_pk x)``.
-  get_label k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob sj) /\ 
+  get_label tr k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob sj) /\ 
   get_usage k == AeadKey "DH.aead_key" empty
 
 let dh_session_pred: local_state_predicate dh_session = {
@@ -277,7 +277,7 @@ let prepare_msg3_proof tr global_sess_id alice alice_si bob msg_id =
               assert(dh y res.gx == dh x res.gy);
               assert(k == k');
               
-              assert(exists si sj. get_label k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob sj));
+              assert(exists si sj. get_label tr k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob sj));
 
               assert(dh_key_and_event_respond1);
               ()
@@ -376,7 +376,7 @@ let verify_msg3_proof tr global_sess_id alice bob msg_id bob_si =
             );
 
             assert(is_corrupt tr (principal_label alice) \/
-              (exists si. get_label res.k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob bob_si)));
+              (exists si. get_label tr res.k `equivalent tr` join (principal_state_label alice si) (principal_state_label bob bob_si)));
             assert(get_usage res.k == AeadKey "DH.aead_key" empty);
             assert(is_corrupt tr (principal_label alice) \/
               (is_dh_shared_key tr alice bob res.k /\ event_triggered tr alice (Initiate2 alice bob gx gy res.k)));
diff --git a/examples/iso_dh/DY.Example.DH.Protocol.Total.Proof.fst b/examples/iso_dh/DY.Example.DH.Protocol.Total.Proof.fst
index a8cebc4..966eb09 100644
--- a/examples/iso_dh/DY.Example.DH.Protocol.Total.Proof.fst
+++ b/examples/iso_dh/DY.Example.DH.Protocol.Total.Proof.fst
@@ -38,7 +38,7 @@ let dh_crypto_preds = {
   sign_pred = {
     pred = (fun tr vk sig_msg ->
       get_signkey_usage vk == SigKey "DH.SigningKey" empty /\
-      (exists prin. get_signkey_label vk = principal_label prin /\ (
+      (exists prin. get_signkey_label tr vk == principal_label prin /\ (
         match parse sig_message sig_msg with
         | Some (SigMsg2 sig_msg2) -> (
           exists y. sig_msg2.gy == (dh_pk y) /\ event_triggered tr prin (Respond1 sig_msg2.alice prin sig_msg2.gx sig_msg2.gy y)
@@ -87,7 +87,7 @@ let compute_message1_proof tr alice bob x =
   // It just shows what we need to show to prove the lemma.
   let msgb = compute_message1 alice x in 
   assert(bytes_invariant tr msgb);
-  assert(get_label msgb `can_flow tr` public);
+  assert(get_label tr msgb `can_flow tr` public);
   assert(is_publishable tr msgb);
   ()
 
@@ -115,7 +115,7 @@ let decode_message1_proof tr msg1_bytes =
       // The following code is not needed for the proof.
       // It just shows what we need to show to prove the lemma.
       assert(bytes_invariant tr msg1.gx);
-      assert(get_label msg1.gx `can_flow tr` public);
+      assert(get_label tr msg1.gx `can_flow tr` public);
       ()
     )
     | None -> ()
@@ -236,7 +236,7 @@ let compute_message3_proof tr alice bob gx gy x sk_a n_sig =
 
   // The following code is not needed for the proof.
   // It just shows what we need to show to prove the lemma. 
-  assert(get_label sg `can_flow tr` public);
+  assert(get_label tr sg `can_flow tr` public);
   assert(bytes_invariant tr sg);
   assert(is_publishable tr sg);
 
diff --git a/examples/iso_dh/DY.Example.DH.SecurityProperties.fst b/examples/iso_dh/DY.Example.DH.SecurityProperties.fst
index 44b619a..8ffea1f 100644
--- a/examples/iso_dh/DY.Example.DH.SecurityProperties.fst
+++ b/examples/iso_dh/DY.Example.DH.SecurityProperties.fst
@@ -77,7 +77,7 @@ let initiator_forward_secrecy tr alice alice_si bob gx gy k =
   // (this assert is not needed and only there for pedagogical purposes)
   assert(
     is_corrupt tr (principal_label bob) \/
-    (exists bob_si. get_label k `equivalent tr` join (principal_state_label alice alice_si) (principal_state_label bob bob_si))
+    (exists bob_si. get_label tr k `equivalent tr` join (principal_state_label alice alice_si) (principal_state_label bob bob_si))
   );
 
   // We deduce from the following this assertion,
@@ -124,7 +124,7 @@ let responder_forward_secrecy tr alice bob bob_si gx gy k =
   // (this assert is not needed and only there for pedagogical purposes)
   assert(
     is_corrupt tr (principal_label alice) \/
-    (exists alice_si. get_label k `equivalent tr` join (principal_state_label alice alice_si) (principal_state_label bob bob_si))
+    (exists alice_si. get_label tr k `equivalent tr` join (principal_state_label alice alice_si) (principal_state_label bob bob_si))
   );
 
   // We deduce from the following this assertion,
diff --git a/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst b/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst
index e4f2394..905d4c8 100644
--- a/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst
+++ b/examples/nsl_pk/DY.Example.NSL.Protocol.Stateful.Proof.fst
@@ -54,13 +54,13 @@ let event_predicate_nsl: event_predicate nsl_event =
     match e with
     | Initiate1 alice bob n_a -> (
       prin == alice /\
-      get_label n_a == join (principal_label alice) (principal_label bob) /\
+      is_secret (join (principal_label alice) (principal_label bob)) tr n_a /\
       0 < DY.Core.Trace.Type.length tr /\
       rand_generated_at tr (DY.Core.Trace.Type.length tr - 1) n_a
     )
     | Respond1 alice bob n_a n_b -> (
       prin == bob /\
-      get_label n_b == join (principal_label alice) (principal_label bob) /\
+      is_secret (join (principal_label alice) (principal_label bob)) tr n_b /\
       0 < DY.Core.Trace.Type.length tr /\
       rand_generated_at tr (DY.Core.Trace.Type.length tr - 1) n_b
     )
@@ -320,8 +320,8 @@ let prepare_msg4 tr global_sess_id bob sess_id msg_id =
           // because we know the label of n_b (which is (join (principal_label alice) (principal_label bob))).
           // It is useful in the "modulo corruption" part of the proof.
           introduce (~((join (principal_label alice) (principal_label bob)) `can_flow tr` public)) ==> event_triggered tr alice (Initiate2 alice bob n_a n_b) with _. (
-            assert(exists alice' n_a'. get_label n_b `can_flow tr` (principal_label alice') /\ event_triggered tr alice' (Initiate2 alice' bob n_a' n_b));
-            eliminate exists alice' n_a'. get_label n_b `can_flow tr` (principal_label alice') /\ event_triggered tr alice' (Initiate2 alice' bob n_a' n_b)
+            assert(exists alice' n_a'. get_label tr n_b `can_flow tr` (principal_label alice') /\ event_triggered tr alice' (Initiate2 alice' bob n_a' n_b));
+            eliminate exists alice' n_a'. get_label tr n_b `can_flow tr` (principal_label alice') /\ event_triggered tr alice' (Initiate2 alice' bob n_a' n_b)
             returns _
             with _. (
               event_respond1_injective tr alice alice' bob n_a n_a' n_b
diff --git a/examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst b/examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst
index 62e9e86..613d540 100644
--- a/examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst
+++ b/examples/nsl_pk/DY.Example.NSL.Protocol.Total.Proof.fst
@@ -24,28 +24,30 @@ let crypto_predicates_nsl = {
   pkenc_pred = {
     pred = (fun tr pk msg ->
       get_sk_usage pk == PkKey "NSL.PublicKey" empty /\
-      (exists prin. get_sk_label pk = principal_label prin /\ (
+      (exists prin. get_sk_label tr pk == principal_label prin /\ (
         match parse message msg with
         | Some (Msg1 msg1) -> (
           let (alice, bob) = (msg1.alice, prin) in
           event_triggered tr alice (Initiate1 alice bob msg1.n_a) /\
-          get_label msg1.n_a == join (principal_label alice) (principal_label bob)
+          get_label tr msg1.n_a == join (principal_label alice) (principal_label bob)
         )
         | Some (Msg2 msg2) -> (
           let (alice, bob) = (prin, msg2.bob) in
           event_triggered tr bob (Respond1 alice bob msg2.n_a msg2.n_b) /\
-          get_label msg2.n_b == join (principal_label alice) (principal_label bob)
+          get_label tr msg2.n_b == join (principal_label alice) (principal_label bob)
         )
         | Some (Msg3 msg3) -> (
           let bob = prin in
           exists alice n_a.
-            get_label msg3.n_b `can_flow tr` (principal_label alice) /\
+            get_label tr msg3.n_b `can_flow tr` (principal_label alice) /\
             event_triggered tr alice (Initiate2 alice bob n_a msg3.n_b)
         )
         | None -> False
       ))
     );
-    pred_later = (fun tr1 tr2 pk msg -> ());
+    pred_later = (fun tr1 tr2 pk msg ->
+      parse_wf_lemma message (bytes_well_formed tr1) msg
+    );
   };
 }
 #pop-options
@@ -213,7 +215,7 @@ val decode_message3_proof:
   Lemma
   (requires
     // From the NSL state invariant
-    get_label n_b = join (principal_label alice) (principal_label bob) /\
+    get_label tr n_b == join (principal_label alice) (principal_label bob) /\
     // From the PrivateKeys invariant
     is_decryption_key (PkKey "NSL.PublicKey" empty) (principal_label bob) tr sk_b /\
     // From the network
@@ -225,7 +227,7 @@ val decode_message3_proof:
     | Some msg3 -> (
       (is_corrupt tr (principal_label alice) \/ is_corrupt tr (principal_label bob)) \/ (
         (exists alice n_a.
-          get_label msg3.n_b `can_flow tr` (principal_label alice) /\
+          get_label tr msg3.n_b `can_flow tr` (principal_label alice) /\
           event_triggered tr alice (Initiate2 alice bob n_a n_b))
       )
     )
diff --git a/src/core/DY.Core.Bytes.Type.fst b/src/core/DY.Core.Bytes.Type.fst
index bc31f38..c6402dd 100644
--- a/src/core/DY.Core.Bytes.Type.fst
+++ b/src/core/DY.Core.Bytes.Type.fst
@@ -62,7 +62,7 @@ and bytes =
   // Public values (strings, numbers, ...)
   | Literal: FStar.Seq.seq FStar.UInt8.t -> bytes
   // Randomly generated numbers. `time` is used to ensure two random numbers are distinct.
-  | Rand: usage:usage -> label:label -> len:nat{len <> 0} -> time:nat -> bytes
+  | Rand: usage:usage -> len:nat{len <> 0} -> time:nat -> bytes
 
   // Concatenation
   | Concat: left:bytes -> right:bytes -> bytes
@@ -116,7 +116,7 @@ let rec encode_usage usg =
 and encode_bytes b =
   match b with
   | Literal l -> 0::(encode_list [encode l])
-  | Rand usg lab len time -> 1::(encode_list [encode_usage usg; encode lab; encode (len <: nat); encode time])
+  | Rand usg len time -> 1::(encode_list [encode_usage usg; encode (len <: nat); encode time])
   | Concat left right -> 2::(encode_list [encode_bytes left; encode_bytes right])
   | AeadEnc key nonce msg ad -> 3::(encode_list [encode_bytes key; encode_bytes nonce; encode_bytes msg; encode_bytes ad])
   | Pk sk -> 4::(encode_list [encode_bytes sk])
@@ -133,7 +133,7 @@ and encode_bytes b =
   | KemSecretShared ss -> 15::(encode_list [encode_bytes ss])
 
 // --warn_error is a workaround for FStar/FStarLang#3220
-#push-options "--z3rlimit 25 --fuel 4 --ifuel 4 --warn_error +290"
+#push-options "--z3rlimit 25 --fuel 3 --ifuel 3 --warn_error +290"
 val encode_usage_inj: usg1:usage -> usg2:usage -> Lemma (requires encode_usage usg1 == encode_usage usg2) (ensures usg1 == usg2)
 val encode_bytes_inj: b1:bytes -> b2:bytes -> Lemma (requires encode_bytes b1 == encode_bytes b2) (ensures b1 == b2)
 let rec encode_usage_inj usg1 usg2 =
@@ -160,10 +160,13 @@ and encode_bytes_inj b1 b2 =
   encode_inj_forall (list (list int)) ();
   match b1, b2 with
   | Literal x1, Literal x2 ->
+    encode_list_inj [encode x1] [encode x2];
     encode_inj x1 x2
-  | Rand x1 x2 _ _, Rand y1 y2 _ _ ->
+  | Rand x1 x2 x3, Rand y1 y2 y3 ->
+    encode_list_inj [encode_usage x1; encode (x2 <: nat); encode x3] [encode_usage y1; encode (y2 <: nat); encode y3];
     encode_usage_inj x1 y1;
-    encode_inj x2 y2
+    encode_inj x2 y2;
+    encode_inj x3 y3
   | Pk x1, Pk y1
   | Vk x1, Vk y1
   | Hash x1, Hash y1
diff --git a/src/core/DY.Core.Bytes.fst b/src/core/DY.Core.Bytes.fst
index 94d2bf9..2f2da31 100644
--- a/src/core/DY.Core.Bytes.fst
+++ b/src/core/DY.Core.Bytes.fst
@@ -60,7 +60,7 @@ let rec length b =
   match b with
   | Literal buf ->
     Seq.length buf
-  | Rand usg label len time ->
+  | Rand usg len time ->
     len
   | Concat left right ->
     length left + length right
@@ -91,6 +91,124 @@ let rec length b =
   | KemSecretShared nonce ->
     32
 
+/// The well-formedness invariant preserved by any protocol using the DY* API,
+/// whether it is proved secure or not.
+/// It checks whether all `Rand`om bytes inside a given `bytes`
+/// correspond to a `RandGen` event in the trace.
+/// This property is weaker than the full-fledged `bytes_invariant` (see theorem `bytes_invariant_implies_well_formed`).
+/// It is a crucial precondition to ensure that the result of `get_label`
+/// is independent of the trace (see theorem `get_label_later`).
+
+[@@"opaque_to_smt"]
+val bytes_well_formed: trace -> bytes -> prop
+let rec bytes_well_formed tr b =
+  match b with
+  | Literal buf ->
+    True
+  | Rand usg len time ->
+    time < DY.Core.Trace.Type.length tr /\
+    RandGen? (get_event_at tr time)
+  | Concat left right ->
+    bytes_well_formed tr left /\
+    bytes_well_formed tr right
+  | AeadEnc key nonce msg ad ->
+    bytes_well_formed tr key /\
+    bytes_well_formed tr nonce /\
+    bytes_well_formed tr msg /\
+    bytes_well_formed tr ad
+  | Pk sk ->
+    bytes_well_formed tr sk
+  | PkEnc pk nonce msg ->
+    bytes_well_formed tr pk /\
+    bytes_well_formed tr nonce /\
+    bytes_well_formed tr msg
+  | Vk sk ->
+    bytes_well_formed tr sk
+  | Sign sk nonce msg ->
+    bytes_well_formed tr sk /\
+    bytes_well_formed tr nonce /\
+    bytes_well_formed tr msg
+  | Hash msg ->
+    bytes_well_formed tr msg
+  | DhPub sk ->
+    bytes_well_formed tr sk
+  | Dh sk pk ->
+    bytes_well_formed tr sk /\
+    bytes_well_formed tr pk
+  | KdfExtract salt ikm ->
+    bytes_well_formed tr salt /\
+    bytes_well_formed tr ikm
+  | KdfExpand prk info len ->
+    bytes_well_formed tr prk /\
+    bytes_well_formed tr info
+  | KemPub sk ->
+    bytes_well_formed tr sk
+  | KemEncap pk nonce ->
+    bytes_well_formed tr pk /\
+    bytes_well_formed tr nonce
+  | KemSecretShared nonce ->
+    bytes_well_formed tr nonce
+
+val bytes_well_formed_later:
+  tr1:trace -> tr2:trace ->
+  b:bytes ->
+  Lemma
+  (requires
+    bytes_well_formed tr1 b /\
+    tr1 <$ tr2
+  )
+  (ensures bytes_well_formed tr2 b)
+  [SMTPat (bytes_well_formed tr1 b);
+   SMTPat (bytes_well_formed tr2 b);
+   SMTPat (tr1 <$ tr2)]
+let rec bytes_well_formed_later tr1 tr2 b =
+  normalize_term_spec bytes_well_formed;
+  introduce forall b_sub. (b_sub << b /\ bytes_well_formed tr1 b_sub) ==> bytes_well_formed tr2 b_sub with (
+    introduce _ ==> _ with _. (
+      bytes_well_formed_later tr1 tr2 b_sub
+    )
+  );
+  match b with
+  | Literal buf -> ()
+  | Rand usg len time -> (
+    assert(event_at tr1 time (get_event_at tr1 time))
+  )
+  | Concat left right -> ()
+  | AeadEnc key nonce msg ad -> ()
+  | Pk sk -> ()
+  | PkEnc pk nonce msg -> ()
+  | Vk sk -> ()
+  | Sign sk nonce msg -> ()
+  | Hash msg -> ()
+  | DhPub sk -> ()
+  | Dh sk pk -> ()
+  | KdfExtract salt ikm -> ()
+  | KdfExpand prk info len -> ()
+  | KemPub sk -> ()
+  | KemEncap pk nonce -> ()
+  | KemSecretShared nonce -> ()
+
+/// Many lemmas with SMT patterns can help proving `bytes_well_formed`.
+/// These lemmas are not expected to be useful in most situations:
+/// - in general we have `bytes_invariant` that implies `bytes_well_formed`
+///   (see theorem `bytes_invariant_implies_well_formed`),
+/// - the only place where we cannot rely on `bytes_invariant`
+///   are in the `pred_later` lemmas inside `crypto_predicates`,
+///   which is only a small amount of the security proof.
+/// Hence the SMT patterns do not trigger by default,
+/// and can be enabled by doing `enable_bytes_well_formed_smtpats tr;`.
+/// See https://github.com/FStarLang/FStar/wiki/Quantifiers-and-patterns
+/// for more information on this technique.
+
+[@@"opaque_to_smt"]
+let bytes_well_formed_smtpats_enabled (tr:trace) = True
+
+val enable_bytes_well_formed_smtpats:
+  tr:trace ->
+  Lemma (bytes_well_formed_smtpats_enabled tr)
+let enable_bytes_well_formed_smtpats tr =
+  normalize_term_spec (bytes_well_formed_smtpats_enabled tr)
+
 /// Customizable functions stating how labels and usages evolve
 /// when using some cryptographic functions.
 
@@ -220,7 +338,7 @@ let default_crypto_usages = {
 val get_usage: {|crypto_usages|} -> b:bytes -> usage
 let rec get_usage #cusages b =
   match b with
-  | Rand usg label len time ->
+  | Rand usg len time ->
     usg
   | Dh sk1 (DhPub sk2) -> (
     match get_usage sk1, get_usage sk2 with
@@ -265,15 +383,21 @@ let rec get_usage #cusages b =
 
 #push-options "--ifuel 2"
 [@@"opaque_to_smt"]
-val get_label: {|crypto_usages|} -> bytes -> label
-let rec get_label #cusages b =
+val get_label: {|crypto_usages|} -> trace -> bytes -> label
+let rec get_label #cusages tr b =
   match b with
   | Literal buf ->
     public
-  | Rand usg label len time ->
-    label
+  | Rand usg len time ->
+    if time < DY.Core.Trace.Type.length tr then (
+      match get_event_at tr time with
+      | RandGen _ lab _ -> lab
+      | _ -> DY.Core.Label.Unknown.unknown_label
+    ) else (
+      DY.Core.Label.Unknown.unknown_label
+    )
   | Concat left right ->
-    meet (get_label left) (get_label right)
+    meet (get_label tr left) (get_label tr right)
   | AeadEnc key nonce msg ad ->
     public
   | Pk sk ->
@@ -283,46 +407,90 @@ let rec get_label #cusages b =
   | Vk sk ->
     public
   | Sign sk nonce msg ->
-    get_label msg
+    get_label tr msg
   | Hash msg ->
-    get_label msg
+    get_label tr msg
   | DhPub sk ->
     public
   | Dh sk1 (DhPub sk2) ->
-    join (get_label sk1) (get_label sk2)
+    join (get_label tr sk1) (get_label tr sk2)
   | Dh sk pk ->
     public
   | KdfExtract salt ikm ->
     let salt_usage = get_usage salt in
     let ikm_usage = get_usage ikm in
     if KdfExtractSaltKey? salt_usage || KdfExtractIkmKey? ikm_usage then
-      kdf_extract_usage.get_label salt_usage ikm_usage (get_label salt) (get_label ikm) salt ikm
+      kdf_extract_usage.get_label salt_usage ikm_usage (get_label tr salt) (get_label tr ikm) salt ikm
     else
-      meet (get_label salt) (get_label ikm)
+      meet (get_label tr salt) (get_label tr ikm)
   | KdfExpand prk info len -> (
     let prk_usage = get_usage prk in
     if KdfExpandKey? prk_usage then
-      kdf_expand_usage.get_label prk_usage (get_label prk) info
+      kdf_expand_usage.get_label prk_usage (get_label tr prk) info
     else
-      get_label prk
+      get_label tr prk
   )
   | KemPub sk ->
     public
   | KemEncap pk nonce ->
     public
   | KemSecretShared nonce ->
-    get_label nonce
+    get_label tr nonce
 #pop-options
 
+val get_label_later:
+  {|crypto_usages|} ->
+  tr1:trace -> tr2:trace ->
+  b:bytes ->
+  Lemma
+  (requires
+    bytes_well_formed tr1 b /\
+    tr1 <$ tr2
+  )
+  (ensures get_label tr1 b == get_label tr2 b)
+  [SMTPat (get_label tr1 b); SMTPat (tr1 <$ tr2)]
+let rec get_label_later #cusgs tr1 tr2 b =
+  normalize_term_spec bytes_well_formed;
+  normalize_term_spec get_label;
+  match b with
+  | Literal buf -> ()
+  | Rand usg len time ->
+    assert(event_at tr1 time (get_event_at tr1 time))
+  | Concat left right ->
+    get_label_later tr1 tr2 left;
+    get_label_later tr1 tr2 right
+  | AeadEnc key nonce msg ad -> ()
+  | Pk sk -> ()
+  | PkEnc pk nonce msg -> ()
+  | Vk sk -> ()
+  | Sign sk nonce msg ->
+    get_label_later tr1 tr2 msg
+  | Hash msg ->
+    get_label_later tr1 tr2 msg
+  | DhPub sk -> ()
+  | Dh sk1 (DhPub sk2) ->
+    get_label_later tr1 tr2 sk1;
+    get_label_later tr1 tr2 sk2
+  | Dh sk pk -> ()
+  | KdfExtract salt ikm ->
+    get_label_later tr1 tr2 salt;
+    get_label_later tr1 tr2 ikm
+  | KdfExpand prk info len ->
+    get_label_later tr1 tr2 prk
+  | KemPub sk -> ()
+  | KemEncap pk nonce -> ()
+  | KemSecretShared nonce ->
+    get_label_later tr1 tr2 nonce
+
 /// Obtain the label of the corresponding decryption key of an encryption key.
 /// Although the encryption key label is public,
 /// this is useful to reason on the corresponding decryption key label.
 
 [@@"opaque_to_smt"]
-val get_sk_label: {|crypto_usages|} -> bytes -> label
-let get_sk_label #cusages pk =
+val get_sk_label: {|crypto_usages|} -> trace -> bytes -> label
+let get_sk_label #cusages tr pk =
   match pk with
-  | Pk sk -> get_label sk
+  | Pk sk -> get_label tr sk
   | _ -> public
 
 /// Same as above, for usage.
@@ -334,15 +502,30 @@ let get_sk_usage #cusages pk =
   | Pk sk -> get_usage sk
   | _ -> NoUsage
 
+val get_sk_label_later:
+  {|crypto_usages|} ->
+  tr1:trace -> tr2:trace ->
+  pk:bytes ->
+  Lemma
+  (requires
+    bytes_well_formed tr1 pk /\
+    tr1 <$ tr2
+  )
+  (ensures get_sk_label tr1 pk == get_sk_label tr2 pk)
+  [SMTPat (get_sk_label tr1 pk); SMTPat (tr1 <$ tr2)]
+let get_sk_label_later #cusgs tr1 tr2 pk =
+  normalize_term_spec bytes_well_formed;
+  normalize_term_spec get_sk_label
+
 /// Obtain the label of the corresponding signature key of a verification key.
 /// Although the verification key label is public,
 /// this is useful to reason on the corresponding signature key label.
 
 [@@"opaque_to_smt"]
-val get_signkey_label: {|crypto_usages|} -> bytes -> label
-let get_signkey_label #cusages pk =
+val get_signkey_label: {|crypto_usages|} -> trace -> bytes -> label
+let get_signkey_label #cusages tr pk =
   match pk with
-  | Vk sk -> get_label sk
+  | Vk sk -> get_label tr sk
   | _ -> public
 
 /// Same as above, for usage.
@@ -354,15 +537,30 @@ let get_signkey_usage #cusages pk =
   | Vk sk -> get_usage sk
   | _ -> NoUsage
 
+val get_signkey_label_later:
+  {|crypto_usages|} ->
+  tr1:trace -> tr2:trace ->
+  pk:bytes ->
+  Lemma
+  (requires
+    bytes_well_formed tr1 pk /\
+    tr1 <$ tr2
+  )
+  (ensures get_signkey_label tr1 pk == get_signkey_label tr2 pk)
+  [SMTPat (get_signkey_label tr1 pk); SMTPat (tr1 <$ tr2)]
+let get_signkey_label_later #cusgs tr1 tr2 pk =
+  normalize_term_spec bytes_well_formed;
+  normalize_term_spec get_signkey_label
+
 /// Obtain the label of the corresponding DH private key of a DH public key.
 /// Although the DH public key label is public,
 /// this is useful to reason on the corresponding DH private key label.
 
 [@@"opaque_to_smt"]
-val get_dh_label: {|crypto_usages|} -> bytes -> label
-let get_dh_label #cusages pk =
+val get_dh_label: {|crypto_usages|} -> trace -> bytes -> label
+let get_dh_label #cusages tr pk =
   match pk with
-  | DhPub sk -> get_label sk
+  | DhPub sk -> get_label tr sk
   | _ -> public
 
 /// Same as above, for usage.
@@ -374,15 +572,30 @@ let get_dh_usage #cusages pk =
   | DhPub sk -> get_usage sk
   | _ -> NoUsage
 
+val get_dh_label_later:
+  {|crypto_usages|} ->
+  tr1:trace -> tr2:trace ->
+  pk:bytes ->
+  Lemma
+  (requires
+    bytes_well_formed tr1 pk /\
+    tr1 <$ tr2
+  )
+  (ensures get_dh_label tr1 pk == get_dh_label tr2 pk)
+  [SMTPat (get_dh_label tr1 pk); SMTPat (tr1 <$ tr2)]
+let get_dh_label_later #cusgs tr1 tr2 pk =
+  normalize_term_spec bytes_well_formed;
+  normalize_term_spec get_dh_label
+
 /// Obtain the label of the corresponding KEM private key of a KEM public key.
 /// Although the KEM public key label is public,
 /// this is useful to reason on the corresponding KEM private key label.
 
 [@@"opaque_to_smt"]
-val get_kem_sk_label: {|crypto_usages|} -> bytes -> label
-let get_kem_sk_label #cusages pk =
+val get_kem_sk_label: {|crypto_usages|} -> trace -> bytes -> label
+let get_kem_sk_label #cusages tr pk =
   match pk with
-  | KemPub sk -> get_label sk
+  | KemPub sk -> get_label tr sk
   | _ -> public
 
 /// Same as above, for usage.
@@ -394,6 +607,20 @@ let get_kem_sk_usage #cusages pk =
   | KemPub sk -> get_usage sk
   | _ -> NoUsage
 
+val get_kem_sk_label_later:
+  {|crypto_usages|} ->
+  tr1:trace -> tr2:trace ->
+  pk:bytes ->
+  Lemma
+  (requires
+    bytes_well_formed tr1 pk /\
+    tr1 <$ tr2
+  )
+  (ensures get_kem_sk_label tr1 pk == get_kem_sk_label tr2 pk)
+  [SMTPat (get_kem_sk_label tr1 pk); SMTPat (tr1 <$ tr2)]
+let get_kem_sk_label_later #cusgs tr1 tr2 pk =
+  normalize_term_spec bytes_well_formed;
+  normalize_term_spec get_kem_sk_label
 
 /// Customizable predicates stating how cryptographic functions may be used
 /// by honest principals.
@@ -405,7 +632,14 @@ type aead_crypto_predicate {|crypto_usages|} = {
     tr1:trace -> tr2:trace ->
     key:bytes{AeadKey? (get_usage key)} -> nonce:bytes -> msg:bytes -> ad:bytes ->
     Lemma
-    (requires pred tr1 key nonce msg ad /\ tr1 <$ tr2)
+    (requires
+      pred tr1 key nonce msg ad /\
+      bytes_well_formed tr1 key /\
+      bytes_well_formed tr1 nonce /\
+      bytes_well_formed tr1 msg /\
+      bytes_well_formed tr1 ad /\
+      tr1 <$ tr2
+    )
     (ensures pred tr2 key nonce msg ad)
   ;
 }
@@ -417,7 +651,12 @@ type pkenc_crypto_predicate {|crypto_usages|} = {
     tr1:trace -> tr2:trace ->
     pk:bytes{PkKey? (get_sk_usage pk)} -> msg:bytes ->
     Lemma
-    (requires pred tr1 pk msg /\ tr1 <$ tr2)
+    (requires
+      pred tr1 pk msg /\
+      bytes_well_formed tr1 pk /\
+      bytes_well_formed tr1 msg /\
+      tr1 <$ tr2
+    )
     (ensures pred tr2 pk msg)
   ;
 }
@@ -429,7 +668,12 @@ type sign_crypto_predicate {|crypto_usages|} = {
     tr1:trace -> tr2:trace ->
     vk:bytes{SigKey? (get_signkey_usage vk)} -> msg:bytes ->
     Lemma
-    (requires pred tr1 vk msg /\ tr1 <$ tr2)
+    (requires
+      pred tr1 vk msg /\
+      bytes_well_formed tr1 vk /\
+      bytes_well_formed tr1 msg /\
+      tr1 <$ tr2
+    )
     (ensures pred tr2 vk msg)
   ;
 }
@@ -503,9 +747,9 @@ let rec bytes_invariant #cinvs tr b =
   match b with
   | Literal buf ->
     True
-  | Rand usage label len time ->
+  | Rand usage len time ->
     // Random bytes correspond to an event
-    event_at tr time (RandGen usage label len)
+    (exists lab. event_at tr time (RandGen usage lab len))
   | Concat left right ->
     bytes_invariant tr left /\
     bytes_invariant tr right
@@ -516,10 +760,10 @@ let rec bytes_invariant #cinvs tr b =
     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 /\
+    (get_label tr 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 /\
+    (get_label tr ad) `can_flow tr` public /\
     (
       (
         // Honest case:
@@ -529,12 +773,12 @@ let rec bytes_invariant #cinvs tr b =
         aead_pred.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)
+        (get_label tr msg) `can_flow tr` (get_label tr key)
       ) \/ (
         // Attacker case:
         // the key and message are both public
-        (get_label key) `can_flow tr` public /\
-        (get_label msg) `can_flow tr` public
+        (get_label tr key) `can_flow tr` public /\
+        (get_label tr msg) `can_flow tr` public
       )
     )
   | Pk sk ->
@@ -552,20 +796,20 @@ let rec bytes_invariant #cinvs tr b =
         pkenc_pred.pred tr pk msg /\
         // - the message is less secret than the decryption key
         //   (this is crucial so that decryption preserve publishability)
-        (get_label msg) `can_flow tr` (get_sk_label pk) /\
+        (get_label tr msg) `can_flow tr` (get_sk_label tr pk) /\
         // - the message is less secret than the nonce
         //   (this is because the standard IND-CCA security assumption
         //   do not give guarantees on the indistinguishability of the message
         //   when the attacker knows the nonce)
-        (get_label msg) `can_flow tr` (get_label nonce) /\
+        (get_label tr msg) `can_flow tr` (get_label tr nonce) /\
         // - the nonce has the correct usage (for the same reason as above)
         PkNonce? (get_usage nonce)
       ) \/ (
         // Attacker case:
         // the attacker knows the nonce, key and message
-        (get_label pk) `can_flow tr` public /\
-        (get_label nonce) `can_flow tr` public /\
-        (get_label msg) `can_flow tr` public
+        (get_label tr pk) `can_flow tr` public /\
+        (get_label tr nonce) `can_flow tr` public /\
+        (get_label tr msg) `can_flow tr` public
       )
     )
   | Vk sk ->
@@ -587,15 +831,15 @@ let rec bytes_invariant #cinvs tr b =
         //   in practice knowing the nonce used to sign a message
         //   can be used to obtain the private key,
         //   hence this restriction)
-        (get_label sk) `can_flow tr` (get_label nonce) /\
+        (get_label tr sk) `can_flow tr` (get_label tr nonce) /\
         // - the nonce has the correct usage (for the same reason as above)
         SigNonce? (get_usage nonce)
       ) \/ (
         // Attacker case:
         // the attacker knows the signature key, nonce and message
-        (get_label sk) `can_flow tr` public /\
-        (get_label nonce) `can_flow tr` public /\
-        (get_label msg) `can_flow tr` public
+        (get_label tr sk) `can_flow tr` public /\
+        (get_label tr nonce) `can_flow tr` public /\
+        (get_label tr msg) `can_flow tr` public
       )
     )
   | Hash msg ->
@@ -614,19 +858,19 @@ let rec bytes_invariant #cinvs tr b =
       ) \/ (
         // Attacker case:
         // the attacker knows one of the secret keys
-        (get_label sk1) `can_flow tr` public \/
-        (get_label sk2) `can_flow tr` public
+        (get_label tr sk1) `can_flow tr` public \/
+        (get_label tr sk2) `can_flow tr` public
       )
     )
   | Dh sk pk ->
     bytes_invariant tr pk /\
     bytes_invariant tr sk /\
-    (get_label pk) `can_flow tr` public /\
+    (get_label tr pk) `can_flow tr` public /\
     (
       (
         DhKey? (get_usage sk)
       ) \/ (
-        (get_label sk) `can_flow tr` public
+        (get_label tr sk) `can_flow tr` public
       )
     )
   | KdfExtract salt ikm ->
@@ -642,8 +886,8 @@ let rec bytes_invariant #cinvs tr b =
       ) \/ (
         // Attacker case:
         // the attacker knows both salt and ikm
-        (get_label salt) `can_flow tr` public /\
-        (get_label ikm) `can_flow tr` public
+        (get_label tr salt) `can_flow tr` public /\
+        (get_label tr ikm) `can_flow tr` public
       )
     )
   | KdfExpand prk info len ->
@@ -657,7 +901,7 @@ let rec bytes_invariant #cinvs tr b =
       ) \/ (
         // Attacker case:
         // the attacker knows both prk and info
-        (get_label prk) `can_flow tr` public
+        (get_label tr prk) `can_flow tr` public
       )
     )
   | KemPub sk ->
@@ -670,7 +914,7 @@ let rec bytes_invariant #cinvs tr b =
         // Honest case:
         // nonce is knowable by the holder of pk
         // (because the nonce roughly corresponds to the shared secret)
-        (get_label nonce) `can_flow tr` (get_kem_sk_label pk) /\ (
+        (get_label tr nonce) `can_flow tr` (get_kem_sk_label tr pk) /\ (
         // nonce and pk agree on the usage of the shared secret
         // (this is because this KEM model does not bind the public key to the shared secret)
           match get_kem_sk_usage pk, get_usage nonce with
@@ -681,16 +925,33 @@ let rec bytes_invariant #cinvs tr b =
       ) \/ (
         // Attacker case:
         // the attacker knows both pk and nonce
-        (get_label pk) `can_flow tr` public /\
-        (get_label nonce) `can_flow tr` public
+        (get_label tr pk) `can_flow tr` public /\
+        (get_label tr nonce) `can_flow tr` public
       )
     )
   | KemSecretShared nonce ->
     bytes_invariant tr nonce
 
+val bytes_invariant_implies_well_formed:
+  {|crypto_invariants|} ->
+  tr:trace -> msg:bytes ->
+  Lemma
+  (requires bytes_invariant tr msg)
+  (ensures bytes_well_formed tr msg)
+  [SMTPat (bytes_well_formed tr msg);
+   SMTPat (bytes_invariant tr msg)]
+let rec bytes_invariant_implies_well_formed #cinvs tr b =
+  normalize_term_spec bytes_invariant;
+  normalize_term_spec bytes_well_formed;
+  introduce forall b_sub. (b_sub << b /\ bytes_invariant tr b_sub) ==> bytes_well_formed tr b_sub with (
+    introduce _ ==> _ with _. (
+      bytes_invariant_implies_well_formed tr b_sub
+    )
+  )
 
 /// The bytes invariant is preserved as the trace grows.
 
+#push-options "--ifuel 2"
 val bytes_invariant_later:
   {|crypto_invariants|} ->
   tr1:trace -> tr2:trace -> msg:bytes ->
@@ -702,7 +963,7 @@ let rec bytes_invariant_later #cinvs tr1 tr2 msg =
   normalize_term_spec bytes_invariant;
   match msg with
   | Literal buf -> ()
-  | Rand usage label len time -> ()
+  | Rand usage len time -> ()
   | Concat left right ->
     bytes_invariant_later tr1 tr2 left;
     bytes_invariant_later tr1 tr2 right
@@ -731,6 +992,7 @@ let rec bytes_invariant_later #cinvs tr1 tr2 msg =
     bytes_invariant_later tr1 tr2 sk;
     bytes_invariant_later tr1 tr2 nonce;
     bytes_invariant_later tr1 tr2 msg;
+    assert(bytes_invariant tr1 (Vk sk)); // to prove well-formedness
     match get_signkey_usage (Vk sk) with
     | SigKey _ _ -> FStar.Classical.move_requires (cinvs.preds.sign_pred.pred_later tr1 tr2 (Vk sk)) msg
     | _ -> ()
@@ -758,6 +1020,7 @@ let rec bytes_invariant_later #cinvs tr1 tr2 msg =
     bytes_invariant_later tr1 tr2 nonce
   | KemSecretShared nonce ->
     bytes_invariant_later tr1 tr2 nonce
+#pop-options
 
 (*** Various predicates ***)
 
@@ -771,7 +1034,7 @@ let rec bytes_invariant_later #cinvs tr1 tr2 msg =
 
 val is_knowable_by: {|crypto_invariants|} -> label -> trace -> bytes -> prop
 let is_knowable_by #cinvs lab tr b =
-  bytes_invariant tr b /\ (get_label b) `can_flow tr` lab
+  bytes_invariant tr b /\ (get_label tr b) `can_flow tr` lab
 
 /// Particular case of the above predicate:
 /// can a given bytestring be published (e.g. on the network)?
@@ -786,13 +1049,13 @@ let is_publishable #cinvs tr b =
 
 val is_secret: {|crypto_invariants|} -> label -> trace -> bytes -> prop
 let is_secret #cinvs lab tr b =
-  bytes_invariant tr b /\ (get_label b) == lab
+  bytes_invariant tr b /\ (get_label tr b) == lab
 
 /// Shorthand predicates for the various type of keys.
 
 val is_verification_key: {|crypto_invariants|} -> usg:usage{SigKey? usg} -> label -> trace -> bytes -> prop
 let is_verification_key #cinvs usg lab tr b =
-  is_publishable tr b /\ (get_signkey_label b) == lab /\
+  is_publishable tr b /\ (get_signkey_label tr b) == lab /\
   get_signkey_usage b == usg
 
 val is_signature_key: {|crypto_invariants|} -> usg:usage{SigKey? usg} -> label -> trace -> bytes -> prop
@@ -802,7 +1065,7 @@ let is_signature_key #cinvs usg lab tr b =
 
 val is_encryption_key: {|crypto_invariants|} -> usg:usage{PkKey? usg} -> label -> trace -> bytes -> prop
 let is_encryption_key #cinvs usg lab tr b =
-  is_publishable tr b /\ (get_sk_label b) == lab /\
+  is_publishable tr b /\ (get_sk_label tr b) == lab /\
   get_sk_usage b == usg
 
 val is_decryption_key: {|crypto_invariants|} -> usg:usage{PkKey? usg} -> label -> trace -> bytes -> prop
@@ -863,7 +1126,6 @@ let bytes_to_literal_to_bytes b =
   normalize_term_spec literal_to_bytes;
   normalize_term_spec bytes_to_literal
 
-
 /// User lemma (length).
 
 val length_literal_to_bytes:
@@ -874,6 +1136,18 @@ let length_literal_to_bytes lit =
   normalize_term_spec literal_to_bytes;
   normalize_term_spec length
 
+/// User lemma (well-formedness)
+
+val bytes_well_formed_literal_to_bytes:
+  tr:trace ->
+  lit:FStar.Seq.seq FStar.UInt8.t ->
+  Lemma (bytes_well_formed tr (literal_to_bytes lit))
+  [SMTPat (bytes_well_formed tr (literal_to_bytes lit));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_literal_to_bytes tr lit =
+  normalize_term_spec bytes_well_formed;
+  normalize_term_spec literal_to_bytes
+
 /// User lemma (bytes invariant).
 /// Coincidentally this is the same as the attacker knowledge lemma above,
 /// but with an SMT pattern.
@@ -991,6 +1265,36 @@ let split_length b i =
   normalize_term_spec split;
   normalize_term_spec length
 
+/// User lemma (concatenation well-formedness)
+
+val bytes_well_formed_concat:
+  tr:trace ->
+  b1:bytes -> b2:bytes ->
+  Lemma
+  (bytes_well_formed tr (concat b1 b2) == (bytes_well_formed tr b1 /\ bytes_well_formed tr b2))
+  [SMTPat (bytes_well_formed tr (concat b1 b2));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_concat tr b1 b2 =
+  normalize_term_spec concat;
+  normalize_term_spec bytes_well_formed
+
+/// User lemma (splitting well-formedness)
+
+val bytes_well_formed_split:
+  tr:trace ->
+  b:bytes -> i:nat ->
+  Lemma (
+    match split b i with
+    | None -> True
+    | Some (b1, b2) -> bytes_well_formed tr b == (bytes_well_formed tr b1 /\ bytes_well_formed tr b2)
+  )
+  [SMTPat (bytes_well_formed tr b);
+   SMTPat (split b i);
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_split tr b i =
+  normalize_term_spec split;
+  normalize_term_spec bytes_well_formed
+
 /// User lemma (concatenation bytes invariant).
 
 val bytes_invariant_concat:
@@ -1025,11 +1329,12 @@ let bytes_invariant_split #cinvs tr b i =
 
 val get_label_concat:
   {|crypto_usages|} ->
+  tr:trace ->
   b1:bytes -> b2:bytes ->
   Lemma
-  (ensures get_label (concat b1 b2) == meet (get_label b1) (get_label b2))
-  [SMTPat (get_label (concat b1 b2))]
-let get_label_concat b1 b2 =
+  (ensures get_label tr (concat b1 b2) == meet (get_label tr b1) (get_label tr b2))
+  [SMTPat (get_label tr (concat b1 b2))]
+let get_label_concat tr b1 b2 =
   normalize_term_spec concat;
   normalize_term_spec get_label
 
@@ -1140,6 +1445,53 @@ let aead_dec_preserves_publishability #cinvs tr key nonce msg ad =
   | Some res -> ()
   | None -> ()
 
+/// User lemma (AEAD encryption well-formedness)
+
+val bytes_well_formed_aead_enc:
+  tr:trace ->
+  key:bytes -> nonce:bytes -> msg:bytes -> ad:bytes ->
+  Lemma (
+    bytes_well_formed tr (aead_enc key nonce msg ad) == (
+      bytes_well_formed tr key /\
+      bytes_well_formed tr nonce /\
+      bytes_well_formed tr msg /\
+      bytes_well_formed tr ad
+    )
+  )
+  [SMTPat (bytes_well_formed tr (aead_enc key nonce msg ad));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_aead_enc tr key nonce msg ad =
+  normalize_term_spec aead_enc;
+  normalize_term_spec bytes_well_formed
+
+/// User lemma (AEAD decryption well-formedness)
+
+val bytes_well_formed_aead_dec:
+  tr:trace ->
+  key:bytes -> nonce:bytes -> msg:bytes -> ad:bytes ->
+  Lemma
+  (
+    match aead_dec key nonce msg ad with
+    | None -> True
+    | Some plaintext -> (
+      bytes_well_formed tr msg == (
+        bytes_well_formed tr key /\
+        bytes_well_formed tr nonce /\
+        bytes_well_formed tr plaintext /\
+        bytes_well_formed tr ad
+      )
+    )
+  )
+  [SMTPat (aead_dec key nonce msg ad);
+   SMTPat (bytes_well_formed tr msg);
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_aead_dec tr key nonce msg ad =
+  normalize_term_spec aead_dec;
+  normalize_term_spec bytes_well_formed;
+  match aead_dec key nonce msg ad with
+  | None -> ()
+  | Some msg -> ()
+
 /// User lemma (AEAD encryption bytes invariant).
 
 val bytes_invariant_aead_enc:
@@ -1151,15 +1503,15 @@ val bytes_invariant_aead_enc:
     bytes_invariant tr nonce /\
     bytes_invariant tr msg /\
     bytes_invariant tr ad /\
-    (get_label nonce) `can_flow tr` public /\
-    (get_label ad) `can_flow tr` public /\
-    (get_label msg) `can_flow tr` (get_label key) /\
+    (get_label tr nonce) `can_flow tr` public /\
+    (get_label tr ad) `can_flow tr` public /\
+    (get_label tr msg) `can_flow tr` (get_label tr key) /\
     (
       (
         AeadKey? (get_usage key) /\
         aead_pred.pred tr key nonce msg ad
       ) \/ (
-        get_label key `can_flow tr` public
+        get_label tr key `can_flow tr` public
       )
     )
   )
@@ -1173,11 +1525,12 @@ let bytes_invariant_aead_enc #cinvs tr key nonce msg ad =
 
 val get_label_aead_enc:
   {|crypto_usages|} ->
+  tr:trace ->
   key:bytes -> nonce:bytes -> msg:bytes -> ad:bytes ->
   Lemma
-  (ensures get_label (aead_enc key nonce msg ad) = public)
-  [SMTPat (get_label (aead_enc key nonce msg ad))]
-let get_label_aead_enc #cusages key nonce msg ad =
+  (ensures get_label tr (aead_enc key nonce msg ad) == public)
+  [SMTPat (get_label tr (aead_enc key nonce msg ad))]
+let get_label_aead_enc #cusages tr key nonce msg ad =
   normalize_term_spec aead_enc;
   normalize_term_spec get_label
 
@@ -1198,7 +1551,7 @@ val bytes_invariant_aead_dec:
     match aead_dec key nonce msg ad with
     | None -> True
     | Some plaintext -> (
-      is_knowable_by (get_label key) tr plaintext /\
+      is_knowable_by (get_label tr key) tr plaintext /\
       (
         (
           AeadKey? (get_usage key) ==>
@@ -1310,6 +1663,63 @@ let pk_dec_preserves_publishability #cinvs tr sk msg =
   normalize_term_spec get_label
 #pop-options
 
+/// User lemma (public encryption key well-formedness)
+
+val bytes_well_formed_pk:
+  tr:trace ->
+  sk:bytes ->
+  Lemma
+  (bytes_well_formed tr (pk sk) == bytes_well_formed tr sk)
+  [SMTPat (bytes_well_formed tr (pk sk));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_pk tr sk =
+  normalize_term_spec pk;
+  normalize_term_spec bytes_well_formed
+
+/// User lemma (public-key encryption well-formedness)
+
+val bytes_well_formed_pk_enc:
+  tr:trace ->
+  pk:bytes -> nonce:bytes -> msg:bytes ->
+  Lemma (
+    bytes_well_formed tr (pk_enc pk nonce msg) == (
+      bytes_well_formed tr pk /\
+      bytes_well_formed tr nonce /\
+      bytes_well_formed tr msg
+    )
+  )
+  [SMTPat (bytes_well_formed tr (pk_enc pk nonce msg));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_pk_enc tr pk nonce msg =
+  normalize_term_spec pk_enc;
+  normalize_term_spec bytes_well_formed
+
+/// User lemma (public-key decryption well-formedness)
+
+val bytes_well_formed_pk_dec:
+  tr:trace ->
+  sk:bytes -> msg:bytes ->
+  Lemma
+  (ensures (
+    match pk_dec sk msg with
+    | None -> True
+    | Some plaintext ->
+      bytes_well_formed tr msg ==> (
+        bytes_well_formed tr sk /\
+        bytes_well_formed tr plaintext
+        // would have equality if we could add `bytes_well_formed tr nonce`
+        // (unfortunately we don't have the nonce)
+      )
+  ))
+  [SMTPat (pk_dec sk msg);
+   SMTPat (bytes_well_formed tr msg);
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_pk_dec tr sk msg =
+  normalize_term_spec pk_dec;
+  normalize_term_spec pk;
+  normalize_term_spec bytes_well_formed
+
+
 /// User lemma (public encryption key bytes invariant).
 
 val bytes_invariant_pk:
@@ -1327,11 +1737,12 @@ let bytes_invariant_pk #cinvs tr sk =
 
 val get_label_pk:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes ->
   Lemma
-  (ensures get_label (pk sk) == public)
-  [SMTPat (get_label (pk sk))]
-let get_label_pk #cusages sk =
+  (ensures get_label tr (pk sk) == public)
+  [SMTPat (get_label tr (pk sk))]
+let get_label_pk #cusages tr sk =
   normalize_term_spec pk;
   normalize_term_spec get_label
 
@@ -1339,11 +1750,12 @@ let get_label_pk #cusages sk =
 
 val get_sk_label_pk:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes ->
   Lemma
-  (ensures get_sk_label (pk sk) == get_label sk)
-  [SMTPat (get_sk_label (pk sk))]
-let get_sk_label_pk #cusages sk =
+  (ensures get_sk_label tr (pk sk) == get_label tr sk)
+  [SMTPat (get_sk_label tr (pk sk))]
+let get_sk_label_pk #cusages tr sk =
   normalize_term_spec pk;
   normalize_term_spec get_sk_label
 
@@ -1369,8 +1781,8 @@ val bytes_invariant_pk_enc:
     bytes_invariant tr pk /\
     bytes_invariant tr nonce /\
     bytes_invariant tr msg /\
-    (get_label msg) `can_flow tr` (get_sk_label pk) /\
-    (get_label msg) `can_flow tr` (get_label nonce) /\
+    (get_label tr msg) `can_flow tr` (get_sk_label tr pk) /\
+    (get_label tr msg) `can_flow tr` (get_label tr nonce) /\
     PkKey? (get_sk_usage pk) /\
     PkNonce? (get_usage nonce) /\
     pkenc_pred.pred tr pk msg
@@ -1385,11 +1797,12 @@ let bytes_invariant_pk_enc #cinvs tr pk nonce msg =
 
 val get_label_pk_enc:
   {|crypto_usages|} ->
+  tr:trace ->
   pk:bytes -> nonce:bytes -> msg:bytes ->
   Lemma
-  (ensures get_label (pk_enc pk nonce msg) == public)
-  [SMTPat (get_label (pk_enc pk nonce msg))]
-let get_label_pk_enc #cusages pk nonce msg =
+  (ensures get_label tr (pk_enc pk nonce msg) == public)
+  [SMTPat (get_label tr (pk_enc pk nonce msg))]
+let get_label_pk_enc #cusages tr pk nonce msg =
   normalize_term_spec pk_enc;
   normalize_term_spec get_label
 
@@ -1408,7 +1821,7 @@ val bytes_invariant_pk_dec:
     match pk_dec sk msg with
     | None -> True
     | Some plaintext ->
-      is_knowable_by (get_label sk) tr plaintext /\
+      is_knowable_by (get_label tr sk) tr plaintext /\
       (
         (
           PkKey? (get_sk_usage (pk sk)) ==>
@@ -1493,6 +1906,37 @@ let sign_preserves_publishability #cinvs tr sk nonce msg =
   normalize_term_spec bytes_invariant;
   normalize_term_spec get_label
 
+/// User lemma (verification key well-formedness)
+
+val bytes_well_formed_vk:
+  tr:trace ->
+  sk:bytes ->
+  Lemma (bytes_well_formed tr (vk sk) == bytes_well_formed tr sk)
+  [SMTPat (bytes_well_formed tr (vk sk));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_vk tr sk =
+  normalize_term_spec vk;
+  normalize_term_spec bytes_well_formed
+
+/// User lemma (signature bytes well-formedness)
+
+val bytes_well_formed_sign:
+  tr:trace ->
+  sk:bytes -> nonce:bytes -> msg:bytes ->
+  Lemma (
+    bytes_well_formed tr (sign sk nonce msg) == (
+      bytes_well_formed tr sk /\
+      bytes_well_formed tr nonce /\
+      bytes_well_formed tr msg
+    )
+  )
+  [SMTPat (bytes_well_formed tr (sign sk nonce msg));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_sign tr sk nonce msg =
+  normalize_term_spec sign;
+  normalize_term_spec vk;
+  normalize_term_spec bytes_well_formed
+
 /// User lemma (verification key bytes invariant).
 
 val bytes_invariant_vk:
@@ -1510,11 +1954,12 @@ let bytes_invariant_vk #cinvs tr sk =
 
 val get_label_vk:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes ->
   Lemma
-  (ensures get_label (vk sk) == public)
-  [SMTPat (get_label (vk sk))]
-let get_label_vk #cusages sk =
+  (ensures get_label tr (vk sk) == public)
+  [SMTPat (get_label tr (vk sk))]
+let get_label_vk #cusages tr sk =
   normalize_term_spec vk;
   normalize_term_spec get_label
 
@@ -1522,11 +1967,12 @@ let get_label_vk #cusages sk =
 
 val get_signkey_label_vk:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes ->
   Lemma
-  (ensures get_signkey_label (vk sk) == get_label sk)
-  [SMTPat (get_signkey_label (vk sk))]
-let get_signkey_label_vk #cusages sk =
+  (ensures get_signkey_label tr (vk sk) == get_label tr sk)
+  [SMTPat (get_signkey_label tr (vk sk))]
+let get_signkey_label_vk #cusages tr sk =
   normalize_term_spec vk;
   normalize_term_spec get_signkey_label
 
@@ -1555,7 +2001,7 @@ val bytes_invariant_sign:
     SigKey? (get_usage sk) /\
     SigNonce? (get_usage nonce) /\
     sign_pred.pred tr (vk sk) msg /\
-    (get_label sk) `can_flow tr` (get_label nonce)
+    (get_label tr sk) `can_flow tr` (get_label tr nonce)
   )
   (ensures bytes_invariant tr (sign sk nonce msg))
   [SMTPat (bytes_invariant tr (sign sk nonce msg))]
@@ -1568,11 +2014,12 @@ let bytes_invariant_sign #cinvs tr sk nonce msg =
 
 val get_label_sign:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes -> nonce:bytes -> msg:bytes ->
   Lemma
-  (ensures get_label (sign sk nonce msg) == get_label msg)
-  [SMTPat (get_label (sign sk nonce msg))]
-let get_label_sign #cusages sk nonce msg =
+  (ensures get_label tr (sign sk nonce msg) == get_label tr msg)
+  [SMTPat (get_label tr (sign sk nonce msg))]
+let get_label_sign #cusages tr sk nonce msg =
   normalize_term_spec sign;
   normalize_term_spec get_label
 
@@ -1593,7 +2040,7 @@ val bytes_invariant_verify:
       SigKey? (get_signkey_usage vk) ==>
       sign_pred.pred tr vk msg
     ) \/ (
-      (get_signkey_label vk) `can_flow tr` public
+      (get_signkey_label tr vk) `can_flow tr` public
     )
   )
   [SMTPat (verify vk msg signature); SMTPat (bytes_invariant tr signature)]
@@ -1624,6 +2071,18 @@ let hash_preserves_publishability #cinvs tr msg =
   normalize_term_spec bytes_invariant;
   normalize_term_spec get_label
 
+/// User lemma (hash bytes well-formedness)
+
+val bytes_well_formed_hash:
+  tr:trace ->
+  msg:bytes ->
+  Lemma (bytes_well_formed tr (hash msg) == bytes_well_formed tr msg)
+  [SMTPat (bytes_well_formed tr (hash msg));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_hash tr msg =
+  normalize_term_spec hash;
+  normalize_term_spec bytes_well_formed
+
 /// User lemma (hash bytes invariant).
 
 val bytes_invariant_hash:
@@ -1641,10 +2100,11 @@ let bytes_invariant_hash #cinvs tr msg =
 
 val get_label_hash:
   {|crypto_usages|} ->
+  tr:trace ->
   msg:bytes ->
-  Lemma (get_label (hash msg) == get_label msg)
-  [SMTPat (get_label (hash msg))]
-let get_label_hash #cusages msg =
+  Lemma (get_label tr (hash msg) == get_label tr msg)
+  [SMTPat (get_label tr (hash msg))]
+let get_label_hash #cusages tr msg =
   normalize_term_spec hash;
   normalize_term_spec get_label
 
@@ -1727,6 +2187,31 @@ let dh_preserves_publishability tr sk pk =
   normalize_term_spec bytes_invariant;
   normalize_term_spec get_label
 
+/// User lemma (dh_pk well-formedness)
+
+val bytes_well_formed_dh_pk:
+  tr:trace ->
+  sk:bytes ->
+  Lemma (bytes_well_formed tr (dh_pk sk) == bytes_well_formed tr sk)
+  [SMTPat (bytes_well_formed tr (dh_pk sk));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_dh_pk tr sk =
+  reveal_opaque (`%dh_pk) (dh_pk);
+  normalize_term_spec bytes_well_formed
+
+/// User lemma (dh well-formedness)
+
+val bytes_well_formed_dh:
+  tr:trace ->
+  sk:bytes -> pk:bytes ->
+  Lemma (bytes_well_formed tr (dh sk pk) <==> (bytes_well_formed tr sk /\ bytes_well_formed tr pk))
+  [SMTPat (bytes_well_formed tr (dh sk pk));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_dh tr sk pk =
+  reveal_opaque (`%dh_pk) (dh_pk);
+  reveal_opaque (`%dh) (dh);
+  normalize_term_spec bytes_well_formed
+
 /// User lemma (dh_pk preserves bytes invariant)
 
 val bytes_invariant_dh_pk:
@@ -1744,11 +2229,12 @@ let bytes_invariant_dh_pk tr sk =
 
 val get_label_dh_pk:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes ->
   Lemma
-  (ensures get_label (dh_pk sk) == public)
-  [SMTPat (get_label (dh_pk sk))]
-let get_label_dh_pk sk =
+  (ensures get_label tr (dh_pk sk) == public)
+  [SMTPat (get_label tr (dh_pk sk))]
+let get_label_dh_pk tr sk =
   reveal_opaque (`%dh_pk) (dh_pk);
   normalize_term_spec get_label
 
@@ -1756,11 +2242,12 @@ let get_label_dh_pk sk =
 
 val get_dh_label_dh_pk:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes ->
   Lemma
-  (get_dh_label (dh_pk sk) == get_label sk)
-  [SMTPat (get_dh_label (dh_pk sk))]
-let get_dh_label_dh_pk sk =
+  (get_dh_label tr (dh_pk sk) == get_label tr sk)
+  [SMTPat (get_dh_label tr (dh_pk sk))]
+let get_dh_label_dh_pk tr sk =
   reveal_opaque (`%dh_pk) (dh_pk);
   reveal_opaque (`%get_dh_label) (get_dh_label)
 
@@ -1799,16 +2286,17 @@ let bytes_invariant_dh tr sk pk =
 #push-options "--z3rlimit 25"
 val get_label_dh:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes -> pk:bytes ->
   Lemma
-  (ensures (get_label (dh sk pk)) `always_equivalent` ((get_label sk) `join` (get_dh_label pk)))
-  [SMTPat (get_label (dh sk pk))]
-let get_label_dh sk pk =
+  (ensures (get_label tr (dh sk pk)) `always_equivalent` ((get_label tr sk) `join` (get_dh_label tr pk)))
+  [SMTPat (get_label tr (dh sk pk))]
+let get_label_dh tr sk pk =
   reveal_opaque (`%dh_pk) (dh_pk);
   reveal_opaque (`%dh) (dh);
   normalize_term_spec get_dh_label;
   normalize_term_spec get_label;
-  join_always_commutes (get_label sk) (get_dh_label pk)
+  join_always_commutes (get_label tr sk) (get_dh_label tr pk)
 #pop-options
 
 /// User lemma (dh bytes usage with known peer)
@@ -1888,7 +2376,7 @@ let kdf_extract_preserves_publishability tr salt ikm =
   let salt_usage = get_usage salt in
   let ikm_usage = get_usage ikm in
   if KdfExtractSaltKey? salt_usage || KdfExtractIkmKey? ikm_usage then
-    kdf_extract_usage.get_label_lemma tr salt_usage ikm_usage (get_label salt) (get_label ikm) salt ikm
+    kdf_extract_usage.get_label_lemma tr salt_usage ikm_usage (get_label tr salt) (get_label tr ikm) salt ikm
   else ()
 
 /// Lemma for attacker knowledge theorem.
@@ -1909,7 +2397,7 @@ let kdf_expand_preserves_publishability tr prk info len =
   normalize_term_spec get_label;
   let prk_usage = get_usage prk in
   if KdfExpandKey? prk_usage then
-    kdf_expand_usage.get_label_lemma tr prk_usage (get_label prk) info
+    kdf_expand_usage.get_label_lemma tr prk_usage (get_label tr prk) info
   else ()
 
 /// Lemma for attacker knowledge theorem.
@@ -1930,6 +2418,40 @@ let kdf_expand_shorter_preserves_publishability tr prk info len1 len2 =
   normalize_term_spec bytes_invariant;
   normalize_term_spec get_label
 
+/// User lemma (kdf_extract well-formedness)
+
+val bytes_well_formed_kdf_extract:
+  tr:trace ->
+  salt:bytes -> ikm:bytes ->
+  Lemma (
+    bytes_well_formed tr (kdf_extract salt ikm) == (
+      bytes_well_formed tr salt /\
+      bytes_well_formed tr ikm
+    )
+  )
+  [SMTPat (bytes_well_formed tr (kdf_extract salt ikm));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_kdf_extract tr salt ikm =
+  reveal_opaque (`%kdf_extract) (kdf_extract);
+  normalize_term_spec bytes_well_formed
+
+/// User lemma (kdf_expand well-formedness)
+
+val bytes_well_formed_kdf_expand:
+  tr:trace ->
+  prk:bytes -> info:bytes -> len:nat{len <> 0} ->
+  Lemma (
+    bytes_well_formed tr (kdf_expand prk info len) == (
+      bytes_well_formed tr prk /\
+      bytes_well_formed tr info
+    )
+  )
+  [SMTPat (bytes_well_formed tr (kdf_expand prk info len));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_kdf_expand tr prk info len =
+  reveal_opaque (`%kdf_expand) (kdf_expand);
+  normalize_term_spec bytes_well_formed
+
 /// User lemma (kdf_extract preserves bytes invariant)
 
 val bytes_invariant_kdf_extract:
@@ -1972,20 +2494,21 @@ let get_usage_kdf_extract salt ikm =
 
 val get_label_kdf_extract:
   {|crypto_usages|} ->
+  tr:trace ->
   salt:bytes -> ikm:bytes ->
   Lemma
   (requires
     (KdfExtractSaltKey? (get_usage salt) \/ KdfExtractIkmKey? (get_usage ikm))
   )
   (ensures
-    get_label (kdf_extract salt ikm) ==
+    get_label tr (kdf_extract salt ikm) ==
     kdf_extract_usage.get_label
       (get_usage salt) (get_usage ikm)
-      (get_label salt) (get_label ikm)
+      (get_label tr salt) (get_label tr ikm)
       salt ikm
   )
-  [SMTPat (get_label (kdf_extract salt ikm))]
-let get_label_kdf_extract salt ikm =
+  [SMTPat (get_label tr (kdf_extract salt ikm))]
+let get_label_kdf_extract tr salt ikm =
   reveal_opaque (`%kdf_extract) (kdf_extract);
   normalize_term_spec get_label
 
@@ -2001,7 +2524,7 @@ val bytes_invariant_kdf_expand:
     bytes_invariant tr info /\
     (
       KdfExpandKey? (get_usage prk) \/
-      get_label prk `can_flow tr` public
+      get_label tr prk `can_flow tr` public
     )
   )
   (ensures bytes_invariant tr (kdf_expand prk info len))
@@ -2029,14 +2552,15 @@ let get_usage_kdf_expand prk info len =
 
 val get_label_kdf_expand:
   {|crypto_usages|} ->
+  tr:trace ->
   prk:bytes -> info:bytes -> len:nat{len <> 0} ->
   Lemma
   (requires KdfExpandKey? (get_usage prk))
   (ensures (
-    get_label (kdf_expand prk info len) == kdf_expand_usage.get_label (get_usage prk) (get_label prk) info
+    get_label tr (kdf_expand prk info len) == kdf_expand_usage.get_label (get_usage prk) (get_label tr prk) info
   ))
-  [SMTPat (get_label (kdf_expand prk info len))]
-let get_label_kdf_expand prk info len =
+  [SMTPat (get_label tr (kdf_expand prk info len))]
+let get_label_kdf_expand tr prk info len =
   reveal_opaque (`%kdf_expand) (kdf_expand);
   normalize_term_spec get_label
 
@@ -2046,14 +2570,14 @@ val get_label_kdf_expand_can_flow:
   {|crypto_usages|} ->
   tr:trace ->
   prk:bytes -> info:bytes -> len:nat{len <> 0} ->
-  Lemma (get_label (kdf_expand prk info len) `can_flow tr` (get_label prk))
-  [SMTPat (can_flow tr (get_label (kdf_expand prk info len)))]
+  Lemma (get_label tr (kdf_expand prk info len) `can_flow tr` (get_label tr prk))
+  [SMTPat (can_flow tr (get_label tr (kdf_expand prk info len)))]
 let get_label_kdf_expand_can_flow tr prk info len =
   reveal_opaque (`%kdf_expand) (kdf_expand);
   normalize_term_spec get_label;
   match get_usage prk with
   | KdfExpandKey _ _ ->
-    kdf_expand_usage.get_label_lemma tr (get_usage prk) (get_label prk) info
+    kdf_expand_usage.get_label_lemma tr (get_usage prk) (get_label tr prk) info
   | _ -> ()
 
 (*** KEM ***)
@@ -2116,6 +2640,113 @@ let kem_pk_preserves_publishability #ci tr sk =
   normalize_term_spec bytes_invariant;
   normalize_term_spec get_label
 
+/// Lemma for attacker knowledge theorem.
+
+val kem_encap_preserves_publishability:
+  {|crypto_invariants|} -> tr:trace ->
+  pk:bytes -> nonce:bytes ->
+  Lemma
+  (requires
+    is_publishable tr pk /\
+    is_publishable tr nonce
+  )
+  (ensures (
+    let (kem_output, ss) = kem_encap pk nonce in
+    is_publishable tr kem_output /\
+    is_publishable tr ss
+  ))
+let kem_encap_preserves_publishability #ci tr pk nonce =
+  normalize_term_spec kem_encap;
+  normalize_term_spec bytes_invariant;
+  normalize_term_spec get_label;
+  assert(is_publishable tr (KemSecretShared nonce))
+
+/// Lemma for attacker knowledge theorem.
+
+val kem_decap_preserves_publishability:
+  {|crypto_invariants|} -> tr:trace ->
+  sk:bytes -> encap:bytes ->
+  Lemma
+  (requires
+    is_publishable tr sk /\
+    is_publishable tr encap
+  )
+  (ensures (
+    match kem_decap sk encap with
+    | Some ss -> is_publishable tr ss
+    | None -> True
+  ))
+let kem_decap_preserves_publishability #ci tr sk encap =
+  normalize_term_spec kem_decap;
+  normalize_term_spec bytes_invariant;
+  normalize_term_spec get_label;
+  normalize_term_spec get_kem_sk_label;
+  match encap with
+  | KemEncap (KemPub sk') nonce ->
+    if sk = sk' then (
+      assert(get_label tr (KemSecretShared nonce) `can_flow tr` public)
+    )
+    else ()
+  | _ -> ()
+
+/// User lemma (kem_pk well-formedness)
+
+val bytes_well_formed_kem_pk:
+  tr:trace ->
+  sk:bytes ->
+  Lemma (bytes_well_formed tr (kem_pk sk) == bytes_well_formed tr sk)
+  [SMTPat (bytes_well_formed tr (kem_pk sk));
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_kem_pk tr sk =
+  normalize_term_spec bytes_well_formed;
+  normalize_term_spec kem_pk
+
+/// User lemma (kem_encap well-formedness)
+
+val bytes_well_formed_kem_encap:
+  tr:trace ->
+  pk:bytes -> nonce:bytes ->
+  Lemma
+  (ensures (
+    let (kem_output, ss) = kem_encap pk nonce in
+    bytes_well_formed tr kem_output == (
+      bytes_well_formed tr pk /\
+      bytes_well_formed tr nonce
+    ) /\
+    bytes_well_formed tr ss == bytes_well_formed tr nonce
+  ))
+  [SMTPat (kem_encap pk nonce);
+   SMTPat (bytes_well_formed tr nonce);
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_kem_encap tr pk nonce =
+  normalize_term_spec kem_encap;
+  normalize_term_spec bytes_well_formed;
+  let (kem_output, ss) = kem_encap pk nonce in
+  ()
+
+/// User lemma (kem_decap well-formedness)
+
+val bytes_well_formed_kem_decap:
+  tr:trace ->
+  sk:bytes -> encap:bytes ->
+  Lemma
+  (ensures (
+    match kem_decap sk encap with
+    | Some ss -> bytes_well_formed tr encap == (bytes_well_formed tr sk /\ bytes_well_formed tr ss)
+    | None -> True
+  ))
+  [SMTPat (kem_decap sk encap);
+   SMTPat (bytes_well_formed tr encap);
+   SMTPat (bytes_well_formed_smtpats_enabled tr)]
+let bytes_well_formed_kem_decap tr sk encap =
+  normalize_term_spec kem_decap;
+  normalize_term_spec bytes_well_formed;
+  match encap with
+  | KemEncap (KemPub sk') nonce ->
+    if sk = sk' then ()
+    else ()
+  | _ -> ()
+
 /// User lemma (kem_pk bytes invariant)
 
 val bytes_invariant_kem_pk:
@@ -2134,13 +2765,14 @@ let bytes_invariant_kem_pk #ci tr sk =
 
 val get_label_kem_pk:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes ->
   Lemma
   (ensures (
-    get_label (kem_pk sk) == public
+    get_label tr (kem_pk sk) == public
   ))
-  [SMTPat (get_label (kem_pk sk))]
-let get_label_kem_pk #cu sk =
+  [SMTPat (get_label tr (kem_pk sk))]
+let get_label_kem_pk #cu tr sk =
   normalize_term_spec get_label;
   normalize_term_spec kem_pk
 
@@ -2162,63 +2794,17 @@ let get_kem_sk_usage_kem_pk #cu sk =
 
 val get_kem_sk_label_kem_pk:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes ->
   Lemma
   (ensures (
-    get_kem_sk_label (kem_pk sk) == get_label sk
+    get_kem_sk_label tr (kem_pk sk) == get_label tr sk
   ))
-  [SMTPat (get_kem_sk_label (kem_pk sk))]
-let get_kem_sk_label_kem_pk #cu sk =
+  [SMTPat (get_kem_sk_label tr (kem_pk sk))]
+let get_kem_sk_label_kem_pk #cu tr sk =
   normalize_term_spec get_kem_sk_label;
   normalize_term_spec kem_pk
 
-/// Lemma for attacker knowledge theorem.
-
-val kem_encap_preserves_publishability:
-  {|crypto_invariants|} -> tr:trace ->
-  pk:bytes -> nonce:bytes ->
-  Lemma
-  (requires
-    is_publishable tr pk /\
-    is_publishable tr nonce
-  )
-  (ensures (
-    let (kem_output, ss) = kem_encap pk nonce in
-    is_publishable tr kem_output /\
-    is_publishable tr ss
-  ))
-let kem_encap_preserves_publishability #ci tr pk nonce =
-  normalize_term_spec kem_encap;
-  normalize_term_spec bytes_invariant;
-  normalize_term_spec get_label;
-  assert(is_publishable tr (KemSecretShared nonce))
-
-/// Lemma for attacker knowledge theorem.
-
-val kem_decap_preserves_publishability:
-  {|crypto_invariants|} -> tr:trace ->
-  sk:bytes -> encap:bytes ->
-  Lemma
-  (requires
-    is_publishable tr sk /\
-    is_publishable tr encap
-  )
-  (ensures (
-    match kem_decap sk encap with
-    | Some ss -> is_publishable tr ss
-    | None -> True
-  ))
-let kem_decap_preserves_publishability #ci tr sk encap =
-  normalize_term_spec kem_decap;
-  normalize_term_spec bytes_invariant;
-  normalize_term_spec get_label;
-  normalize_term_spec get_kem_sk_label;
-  match encap with
-  | KemEncap (KemPub sk') nonce ->
-    if sk = sk' then ()
-    else ()
-  | _ -> ()
-
 /// User lemma (kem_encap properties)
 
 val bytes_invariant_kem_encap:
@@ -2229,8 +2815,8 @@ val bytes_invariant_kem_encap:
     is_publishable tr pk /\
     bytes_invariant tr nonce /\
     KemNonce? (get_usage nonce) /\
-    (get_label nonce) `can_flow tr` (get_kem_sk_label pk) /\ (
-      get_label nonce `can_flow tr` public \/
+    (get_label tr nonce) `can_flow tr` (get_kem_sk_label tr pk) /\ (
+      get_label tr nonce `can_flow tr` public \/
       get_kem_sk_usage pk == KemKey (KemNonce?.usg (get_usage nonce))
     )
   )
@@ -2238,7 +2824,7 @@ val bytes_invariant_kem_encap:
     let (kem_output, ss) = kem_encap pk nonce in
     is_publishable tr kem_output /\
     bytes_invariant tr ss /\
-    get_label ss == get_label nonce /\
+    get_label tr ss == get_label tr nonce /\
     get_usage ss == (KemNonce?.usg (get_usage nonce))
   ))
   [SMTPat (kem_encap pk nonce); SMTPat (bytes_invariant tr nonce)]
@@ -2262,11 +2848,11 @@ val get_usage_kem_decap:
   (requires
     bytes_invariant tr sk /\
     bytes_invariant tr encap /\
-    (KemKey? (get_usage sk) \/ (get_label sk) `can_flow tr` public)
+    (KemKey? (get_usage sk) \/ (get_label tr sk) `can_flow tr` public)
   )
   (ensures (
     match kem_decap sk encap with
-    | Some ss -> get_usage sk == KemKey (get_usage ss) \/ get_label ss `can_flow tr` public
+    | Some ss -> get_usage sk == KemKey (get_usage ss) \/ get_label tr ss `can_flow tr` public
     | None -> True
   ))
   [SMTPat (kem_decap sk encap); SMTPat (bytes_invariant tr encap)]
@@ -2297,7 +2883,7 @@ val bytes_invariant_kem_decap:
   )
   (ensures (
     match kem_decap sk encap with
-    | Some ss -> is_knowable_by (get_label sk) tr ss
+    | Some ss -> is_knowable_by (get_label tr sk) tr ss
     | None -> True
   ))
   [SMTPat (kem_decap sk encap); SMTPat (bytes_invariant tr encap)]
diff --git a/src/core/DY.Core.Label.Type.fst b/src/core/DY.Core.Label.Type.fst
index 754c691..7a88097 100644
--- a/src/core/DY.Core.Label.Type.fst
+++ b/src/core/DY.Core.Label.Type.fst
@@ -41,53 +41,11 @@ type pre_label =
 /// with lower bound (meet) and upper bound (join),
 /// as well as a minima (secret) and maxima (public).
 
+[@@erasable]
+noeq
 type label =
   | Secret: label
   | State: pre_label -> label
   | Meet: label -> label -> label
   | Join: label -> label -> label
   | Public: label
-
-open DY.Core.Internal.Ord
-
-instance integer_encodable_pre_label: integer_encodable pre_label = {
-  encode = (fun x ->
-    match x with
-    | P p -> 0::(encode p)
-    | S p s -> 1::(encode [encode p; encode s.the_id])
-  );
-  encode_inj = (fun x y ->
-    encode_inj_forall (list (list int)) ();
-    encode_inj_forall string ();
-    encode_inj_forall nat ()
-  );
-}
-
-val encode_label: label -> list int
-let rec encode_label l =
-  match l with
-  | Secret -> 0::[]
-  | State s -> 1::(encode [encode s])
-  | Meet l1 l2 -> 2::(encode [encode_label l1; encode_label l2])
-  | Join l1 l2 -> 3::(encode [encode_label l1; encode_label l2])
-  | Public -> 4::[]
-
-val encode_label_inj:
-  l1:label -> l2:label ->
-  Lemma
-  (requires encode_label l1 == encode_label l2)
-  (ensures l1 == l2)
-let rec encode_label_inj l1 l2 =
-  introduce forall l1' l2'. l1' << l1 /\ l2' << l2 /\ encode_label l1' == encode_label l2' ==> l1' == l2' with (
-    introduce _ ==> _ with _. (
-      encode_label_inj l1' l2'
-    )
-  );
-  encode_inj_forall (list (list int)) ();
-  encode_inj_forall pre_label ();
-  allow_inversion label
-
-instance integer_encodable_label: integer_encodable label = {
-  encode = encode_label;
-  encode_inj = encode_label_inj;
-}
diff --git a/src/core/DY.Core.Label.Unknown.fst b/src/core/DY.Core.Label.Unknown.fst
new file mode 100644
index 0000000..60c9b51
--- /dev/null
+++ b/src/core/DY.Core.Label.Unknown.fst
@@ -0,0 +1,3 @@
+module DY.Core.Label.Unknown
+
+let unknown_label = Public
diff --git a/src/core/DY.Core.Label.Unknown.fsti b/src/core/DY.Core.Label.Unknown.fsti
new file mode 100644
index 0000000..c2dcfd1
--- /dev/null
+++ b/src/core/DY.Core.Label.Unknown.fsti
@@ -0,0 +1,15 @@
+module DY.Core.Label.Unknown
+
+open DY.Core.Label.Type
+
+/// In some functions or proofs, we may need a label which can be arbitrary:
+/// its value doesn't matter, we just need a label,
+/// and its value doesn't impact the proofs,
+/// as in `DY.Core.Bytes.get_label` when the `bytes` is ill-formed.
+/// Instead of having to choose an arbitrary label,
+/// we can use the following `unknown_label`
+/// on which we can't reason because it's hidden behind an interface file.
+/// This helps to justify that the proofs don't rely on the actual value of the label.
+
+[@@ must_erase_for_extraction]
+val unknown_label: label
diff --git a/src/core/DY.Core.Trace.Manipulation.fst b/src/core/DY.Core.Trace.Manipulation.fst
index e96199e..dc4857e 100644
--- a/src/core/DY.Core.Trace.Manipulation.fst
+++ b/src/core/DY.Core.Trace.Manipulation.fst
@@ -241,7 +241,7 @@ val mk_rand: usg:usage -> lab:label -> len:nat{len <> 0} -> traceful bytes
 let mk_rand usg lab len =
   let* time = get_time in
   add_event (RandGen usg lab len);*
-  return (Rand usg lab len time)
+  return (Rand usg len time)
 
 /// Generating a random bytestrings always preserve the trace invariant.
 
@@ -289,7 +289,7 @@ val mk_rand_get_label:
   Lemma
   (ensures (
     let (b, tr_out) = mk_rand usg lab len tr in
-    get_label b == lab
+    get_label tr_out b == lab
   ))
   [SMTPat (mk_rand usg lab len tr); SMTPat (trace_invariant tr)]
 let mk_rand_get_label #invs usg lab len tr =
@@ -354,10 +354,13 @@ let rec compute_new_session_id_correct prin tr sess_id state_content =
   match tr with
   | Nil -> ()
   | Snoc tr_init evt -> (
-    if evt = SetState prin sess_id state_content then ()
-    else (
-      compute_new_session_id_correct prin tr_init sess_id state_content
-    )
+    match evt with
+    | SetState prin' sess_id' state_content' ->
+      if prin = prin' && sess_id = sess_id' && state_content = state_content' then ()
+      else (
+        compute_new_session_id_correct prin tr_init sess_id state_content
+      )
+    | _ -> compute_new_session_id_correct prin tr_init sess_id state_content
   )
 
 /// Compute a fresh state identifier for a principal.
diff --git a/src/core/DY.Core.Trace.Type.fst b/src/core/DY.Core.Trace.Type.fst
index 97f51a3..193bf58 100644
--- a/src/core/DY.Core.Trace.Type.fst
+++ b/src/core/DY.Core.Trace.Type.fst
@@ -31,6 +31,7 @@ open DY.Core.Label.Type
 
 /// The type for events in the trace.
 
+noeq
 type trace_event =
   // A message has been sent on the network.
   | MsgSent: bytes -> trace_event
@@ -48,6 +49,7 @@ type trace_event =
 /// the trace is actually a reversed list.
 /// To avoid confusions, we define a custom inductive to swap the arguments of the "cons" constructor.
 
+noeq
 type trace =
   | Nil: trace
   | Snoc: trace -> trace_event -> trace
@@ -301,6 +303,6 @@ let event_triggered_grows tr1 tr2 prin tag content = ()
 val rand_generated_at: trace -> timestamp -> bytes -> prop
 let rand_generated_at tr i b =
   match b with
-  | Rand usg lab len time ->
-    time == i /\ event_at tr i (RandGen usg lab len)
+  | Rand usg len time ->
+    time == i /\ (exists lab. event_at tr i (RandGen usg lab len))
   | _ -> False
diff --git a/src/lib/comparse/DY.Lib.Comparse.Glue.fst b/src/lib/comparse/DY.Lib.Comparse.Glue.fst
index ee03c8d..4552b8d 100644
--- a/src/lib/comparse/DY.Lib.Comparse.Glue.fst
+++ b/src/lib/comparse/DY.Lib.Comparse.Glue.fst
@@ -61,6 +61,19 @@ instance bytes_like_bytes: bytes_like bytes = {
 
 /// Compability of some DY*'s predicates with concat and split.
 
+val bytes_well_formed_is_pre_compatible:
+  tr:trace ->
+  Lemma
+  (bytes_pre_is_compatible (bytes_well_formed tr))
+  [SMTPat (bytes_pre_is_compatible (bytes_well_formed tr))]
+let bytes_well_formed_is_pre_compatible tr =
+  enable_bytes_well_formed_smtpats tr;
+  bytes_pre_is_compatible_intro #bytes (bytes_well_formed tr)
+    ()
+    (fun b1 b2 -> ())
+    (fun b i -> ())
+    (fun sz n -> ())
+
 val bytes_invariant_is_pre_compatible:
   {|crypto_invariants|} -> tr:trace ->
   Lemma
diff --git a/src/lib/crypto/DY.Lib.Crypto.AEAD.Split.fst b/src/lib/crypto/DY.Lib.Crypto.AEAD.Split.fst
index 639a2cf..a6fd623 100644
--- a/src/lib/crypto/DY.Lib.Crypto.AEAD.Split.fst
+++ b/src/lib/crypto/DY.Lib.Crypto.AEAD.Split.fst
@@ -25,6 +25,13 @@ let split_aead_predicate_params {|crypto_usages|}: split_crypto_predicate_parame
     pred (tr, key, (nonce, msg, ad))
   );
 
+  key_and_data_well_formed = (fun tr key (nonce, msg, ad) ->
+    bytes_well_formed tr key /\
+    bytes_well_formed tr nonce /\
+    bytes_well_formed tr msg /\
+    bytes_well_formed tr ad
+  );
+
   apply_mk_global_pred = (fun bare x -> ());
   apply_local_pred_later = (fun lpred tr1 tr2 key (nonce, msg, ad) ->
     lpred.pred_later tr1 tr2 key nonce msg ad
diff --git a/src/lib/crypto/DY.Lib.Crypto.PkEncryption.Split.fst b/src/lib/crypto/DY.Lib.Crypto.PkEncryption.Split.fst
index b455b34..c97d377 100644
--- a/src/lib/crypto/DY.Lib.Crypto.PkEncryption.Split.fst
+++ b/src/lib/crypto/DY.Lib.Crypto.PkEncryption.Split.fst
@@ -25,6 +25,11 @@ let split_pkenc_predicate_params {|crypto_usages|}: split_crypto_predicate_param
     pred (tr, pk, msg)
   );
 
+  key_and_data_well_formed = (fun tr pk msg ->
+    bytes_well_formed tr pk /\
+    bytes_well_formed tr msg
+  );
+
   apply_mk_global_pred = (fun bare x -> ());
   apply_local_pred_later = (fun lpred tr1 tr2 pk msg ->
     lpred.pred_later tr1 tr2 pk msg
diff --git a/src/lib/crypto/DY.Lib.Crypto.Signature.Split.fst b/src/lib/crypto/DY.Lib.Crypto.Signature.Split.fst
index 53c0c1f..e538689 100644
--- a/src/lib/crypto/DY.Lib.Crypto.Signature.Split.fst
+++ b/src/lib/crypto/DY.Lib.Crypto.Signature.Split.fst
@@ -25,6 +25,11 @@ let split_sign_predicate_params {|crypto_usages|}: split_crypto_predicate_parame
     pred (tr, vk, msg)
   );
 
+  key_and_data_well_formed = (fun tr vk msg ->
+    bytes_well_formed tr vk /\
+    bytes_well_formed tr msg
+  );
+
   apply_mk_global_pred = (fun bare x -> ());
   apply_local_pred_later = (fun lpred tr1 tr2 vk msg ->
     lpred.pred_later tr1 tr2 vk msg
diff --git a/src/lib/crypto/DY.Lib.Crypto.SplitPredicate.fst b/src/lib/crypto/DY.Lib.Crypto.SplitPredicate.fst
index 30b2ad7..7221345 100644
--- a/src/lib/crypto/DY.Lib.Crypto.SplitPredicate.fst
+++ b/src/lib/crypto/DY.Lib.Crypto.SplitPredicate.fst
@@ -23,6 +23,8 @@ type split_crypto_predicate_parameters = {
   apply_global_pred: global_pred_t -> (trace & key_t & data_t) -> prop;
   mk_global_pred: ((trace & key_t & data_t) -> prop) -> global_pred_t;
 
+  key_and_data_well_formed: trace -> key_t -> data_t -> prop;
+
   apply_mk_global_pred: bare:((trace & key_t & data_t) -> prop) -> x:(trace & key_t & data_t) -> Lemma
     (apply_global_pred (mk_global_pred bare) x == bare x);
   apply_local_pred_later:
@@ -30,7 +32,10 @@ type split_crypto_predicate_parameters = {
     tr1:trace -> tr2:trace ->
     key:key_t -> data:data_t ->
     Lemma
-    (requires apply_local_pred lpred (tr1, key, data) /\ tr1 <$ tr2)
+    (requires
+      apply_local_pred lpred (tr1, key, data) /\
+      key_and_data_well_formed tr1 key data /\
+      tr1 <$ tr2)
     (ensures apply_local_pred lpred (tr2, key, data))
   ;
 }
@@ -93,7 +98,11 @@ val mk_global_crypto_predicate_later:
   tr1:trace -> tr2:trace ->
   key:params.key_t -> data:params.data_t ->
   Lemma
-  (requires params.apply_global_pred (mk_global_crypto_predicate params tagged_local_preds) (tr1, key, data) /\ tr1 <$ tr2)
+  (requires
+    params.apply_global_pred (mk_global_crypto_predicate params tagged_local_preds) (tr1, key, data) /\
+    params.key_and_data_well_formed tr1 key data /\
+    tr1 <$ tr2
+  )
   (ensures params.apply_global_pred (mk_global_crypto_predicate params tagged_local_preds) (tr2, key, data))
 let mk_global_crypto_predicate_later params tagged_local_preds tr1 tr2 key data =
   let fparams = split_crypto_predicate_parameters_to_split_function_parameters params in
diff --git a/src/lib/hpke/DY.Lib.HPKE.Lemmas.fst b/src/lib/hpke/DY.Lib.HPKE.Lemmas.fst
index 92f5c08..42064a7 100644
--- a/src/lib/hpke/DY.Lib.HPKE.Lemmas.fst
+++ b/src/lib/hpke/DY.Lib.HPKE.Lemmas.fst
@@ -76,9 +76,9 @@ let mk_hpke_sk_usage_inj (usage_tag1, usage_data1) (usage_tag2, usage_data2) =
 
 /// Obtain the label of the corresponding HPKE private key of a HPKE public key.
 
-val get_hpke_sk_label: {|crypto_usages|} -> bytes -> label
-let get_hpke_sk_label #cusages pk =
-  get_kem_sk_label pk
+val get_hpke_sk_label: {|crypto_usages|} -> trace -> bytes -> label
+let get_hpke_sk_label #cusages tr pk =
+  get_kem_sk_label tr pk
 
 /// Obtain the usage of the corresponding HPKE private key of a HPKE public key.
 
@@ -95,7 +95,13 @@ type hpke_crypto_predicate {|crypto_usages|} = {
     tr1:trace -> tr2:trace ->
     usage:(string & bytes) -> msg:bytes -> info:bytes -> ad:bytes ->
     Lemma
-    (requires pred tr1 usage msg info ad /\ tr1 <$ tr2)
+    (requires
+      pred tr1 usage msg info ad /\
+      bytes_well_formed tr1 msg /\
+      bytes_well_formed tr1 info /\
+      bytes_well_formed tr1 ad /\
+      tr1 <$ tr2
+    )
     (ensures pred tr2 usage msg info ad)
   ;
 }
@@ -155,6 +161,7 @@ let hpke_aead_pred #cusgs #hpke = {
     let AeadKey usg data = get_usage key in
     match parse hpke_aead_usage_data data with
     | Some { hpke_usg; info; } ->
+      bytes_well_formed tr info /\
       hpke_pred.pred tr (hpke_usg.usage_tag, hpke_usg.usage_data) msg info ad
     | _ ->
       False
@@ -201,11 +208,12 @@ let bytes_invariant_hpke_pk #ci tr sk = ()
 
 val get_label_hpke_pk:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes ->
   Lemma
-  (ensures get_label (hpke_pk sk) == public)
-  [SMTPat (get_label (hpke_pk sk))]
-let get_label_hpke_pk #cu sk = ()
+  (ensures get_label tr (hpke_pk sk) == public)
+  [SMTPat (get_label tr (hpke_pk sk))]
+let get_label_hpke_pk #cu tr sk = ()
 
 val get_hpke_sk_usage_hpke_pk:
   {|crypto_usages|} ->
@@ -217,11 +225,12 @@ let get_hpke_sk_usage_hpke_pk #cu sk = ()
 
 val get_hpke_sk_label_hpke_pk:
   {|crypto_usages|} ->
+  tr:trace ->
   sk:bytes ->
   Lemma
-  (ensures get_hpke_sk_label (hpke_pk sk) == get_label sk)
-  [SMTPat (get_hpke_sk_label (hpke_pk sk))]
-let get_hpke_sk_label_hpke_pk #cu sk = ()
+  (ensures get_hpke_sk_label tr (hpke_pk sk) == get_label tr sk)
+  [SMTPat (get_hpke_sk_label tr (hpke_pk sk))]
+let get_hpke_sk_label_hpke_pk #cu tr sk = ()
 
 /// Lemma for `hpke_enc`.
 /// It is a bit more complex than `DY.Core.Bytes.bytes_invariant_pk_enc`,
@@ -240,9 +249,9 @@ val bytes_invariant_hpke_enc:
     bytes_invariant tr info /\
     is_publishable tr ad /\
     // the message must flow to the shared secret (derived from the entropy), a requirement of AEAD
-    (get_label msg) `can_flow tr` (get_label entropy) /\
+    (get_label tr msg) `can_flow tr` (get_label tr entropy) /\
     // shared secret (derived from the entropy) must flow to the secret key, a requirement of KEM
-    (get_label entropy) `can_flow tr` (get_hpke_sk_label pkR) /\
+    (get_label tr entropy) `can_flow tr` (get_hpke_sk_label tr pkR) /\
     // the entropy and public key must agree on the usage,
     // or the entropy (hence shared secret) must be publishable:
     // without this precondition, there could be cross-protocol attacks,
@@ -254,7 +263,7 @@ val bytes_invariant_hpke_enc:
         get_hpke_sk_usage pkR == mk_hpke_sk_usage usage /\
         get_usage entropy == mk_hpke_entropy_usage usage
       ) \/
-      get_label entropy `can_flow tr` public
+      get_label tr entropy `can_flow tr` public
     ) /\
     // but even if it is publishable, the entropy must have a correct usage
     (exists usage. get_usage entropy == mk_hpke_entropy_usage usage) /\
@@ -310,7 +319,7 @@ val bytes_invariant_hpke_dec:
     bytes_invariant tr skR /\
     (
       (exists usage. get_usage skR == mk_hpke_sk_usage usage) \/
-      get_label skR `can_flow tr` public
+      get_label tr skR `can_flow tr` public
     ) /\
     bytes_invariant tr enc /\
     bytes_invariant tr ciphertext /\
@@ -322,7 +331,7 @@ val bytes_invariant_hpke_dec:
     match hpke_dec skR (enc, ciphertext) info ad with
     | None -> True
     | Some plaintext ->
-      is_knowable_by (get_label skR) tr plaintext /\
+      is_knowable_by (get_label tr skR) tr plaintext /\
       (
         (
           forall usage. get_hpke_sk_usage (hpke_pk skR) == mk_hpke_sk_usage usage ==>
@@ -341,7 +350,7 @@ let bytes_invariant_hpke_dec #cinvs #hpke tr skR enc ciphertext info ad =
     match hpke_dec skR (enc, ciphertext) info ad with
     | None -> True
     | Some plaintext ->
-      is_knowable_by (get_label skR) tr plaintext /\
+      is_knowable_by (get_label tr skR) tr plaintext /\
       (
         (
           forall usage. get_hpke_sk_usage (hpke_pk skR) == mk_hpke_sk_usage usage ==>
@@ -361,7 +370,7 @@ let bytes_invariant_hpke_dec #cinvs #hpke tr skR enc ciphertext info ad =
 
   eliminate
     (exists usage. get_usage skR == mk_hpke_sk_usage usage) \/
-    get_label skR `can_flow tr` public
+    get_label tr skR `can_flow tr` public
   returns post
   with _. (
     eliminate exists usage. get_usage skR == mk_hpke_sk_usage usage
@@ -379,10 +388,10 @@ let bytes_invariant_hpke_dec #cinvs #hpke tr skR enc ciphertext info ad =
         assert(get_usage shared_secret == KdfExpandKey "DY.Lib.HPKE" (serialize _ {usage_tag; usage_data}) \/ is_publishable tr shared_secret);
         let aead_key = kdf_expand shared_secret key_info_bytes 32 in
         assert(get_usage aead_key == AeadKey "DY.Lib.HPKE" (serialize _ {hpke_usg = {usage_tag; usage_data}; info}) \/ is_publishable tr shared_secret);
-        assert(get_label aead_key == get_label shared_secret \/ is_publishable tr shared_secret);
+        assert(get_label tr aead_key == get_label tr shared_secret \/ is_publishable tr shared_secret);
         let aead_nonce = kdf_expand shared_secret nonce_info_bytes 32 in
         assert(get_usage aead_nonce == NoUsage \/ is_publishable tr shared_secret);
-        assert(get_label aead_nonce == public \/ is_publishable tr shared_secret);
+        assert(get_label tr aead_nonce == public \/ is_publishable tr shared_secret);
         match aead_dec aead_key aead_nonce ciphertext ad with
         | None -> ()
         | Some plaintext -> (
diff --git a/src/lib/hpke/DY.Lib.HPKE.Split.fst b/src/lib/hpke/DY.Lib.HPKE.Split.fst
index 39a302d..6be0cd2 100644
--- a/src/lib/hpke/DY.Lib.HPKE.Split.fst
+++ b/src/lib/hpke/DY.Lib.HPKE.Split.fst
@@ -25,6 +25,12 @@ let split_hpke_predicate_params {|crypto_usages|}: split_crypto_predicate_parame
     pred (tr, usage, (plaintext, info, ad))
   );
 
+  key_and_data_well_formed = (fun tr usage (plaintext, info, ad) ->
+    bytes_well_formed tr plaintext /\
+    bytes_well_formed tr info /\
+    bytes_well_formed tr ad
+  );
+
   apply_mk_global_pred = (fun bare x -> ());
   apply_local_pred_later = (fun lpred tr1 tr2 usage (plaintext, info, ad) ->
     lpred.pred_later tr1 tr2 usage plaintext info ad
diff --git a/src/lib/utils/DY.Lib.Printing.fst b/src/lib/utils/DY.Lib.Printing.fst
index 69d6c9c..77e5d44 100644
--- a/src/lib/utils/DY.Lib.Printing.fst
+++ b/src/lib/utils/DY.Lib.Printing.fst
@@ -15,19 +15,6 @@ open DY.Lib.State.Map
 
 (*** Print Functions for Basic DY* Types ***)
 
-val label_to_string: (l:label) -> string
-let rec label_to_string l =
-  match l with
-  | Secret -> "Secret"
-  | State pre_label -> (
-    match pre_label with
-    | P p -> Printf.sprintf "Principal %s" p
-    | S p s -> Printf.sprintf "Principal %s state %d" p s.the_id
-  ) 
-  | Meet l1 l2 -> Printf.sprintf "Meet [%s; %s]" (label_to_string l1) (label_to_string l2)
-  | Join l1 l2 -> Printf.sprintf "Join [%s; %s]" (label_to_string l1) (label_to_string l2)
-  | Public -> "Public"
-
 val uint_list_to_string: list FStar.UInt8.t -> string
 let rec uint_list_to_string seq =
   match seq with
@@ -44,7 +31,7 @@ let rec bytes_to_string b =
   match b with
   | Literal s -> uint_list_to_string (FStar.Seq.seq_to_list s)
   
-  | Rand usage label len time -> Printf.sprintf "Nonce #%d" time
+  | Rand usage len time -> Printf.sprintf "Nonce #%d" time
   
   | Concat (Literal s) right -> (
       Printf.sprintf "%s%s" 
@@ -226,8 +213,8 @@ let trace_event_to_string printers tr_event i =
       i msg_str
   )
   | RandGen usg lab len -> (
-    Printf.sprintf "{\"TraceID\": %d, \"Type\": \"Nonce\", \"Usage\": %s, \"Label\": \"%s\"}\n" 
-    i (usage_to_string usg) (label_to_string lab)
+    Printf.sprintf "{\"TraceID\": %d, \"Type\": \"Nonce\", \"Usage\": %s}\n" 
+    i (usage_to_string usg)
   )
   | Corrupt prin sess_id -> ""
   | SetState prin sess_id full_content -> (