cleanup: remove dy_bytes alias

fstar/symbolic/MLS.Symbolic.fst

@@ -9,12 +9,9 @@ open MLS.Result
 
 (*** Typeclass instantiation on DY* ***)
 
-val dy_bytes: eqtype
-let dy_bytes = DY.Core.bytes
-
 #push-options "--ifuel 1"
-val dy_bytes_has_crypto: available_ciphersuite -> crypto_bytes dy_bytes
-let dy_bytes_has_crypto acs = {
+val bytes_has_crypto_bytes: available_ciphersuite -> crypto_bytes bytes
+let bytes_has_crypto_bytes acs = {
   base = DY.Lib.bytes_like_bytes;
 
   bytes_hasEq = ();
@@ -82,7 +79,7 @@ let dy_bytes_has_crypto acs = {
   );
 
   string_to_bytes = (fun s ->
-    (ps_whole_ascii_string.serialize s <: dy_bytes)
+    (ps_whole_ascii_string.serialize s <: bytes)
   );
 
   unsafe_split = (fun buf i ->
@@ -96,7 +93,7 @@ let dy_bytes_has_crypto acs = {
 }
 #pop-options
 
-instance crypto_dy_bytes: crypto_bytes dy_bytes = dy_bytes_has_crypto AC_mls_128_dhkemx25519_chacha20poly1305_sha256_ed25519
+instance crypto_bytes_bytes: crypto_bytes bytes = bytes_has_crypto_bytes AC_mls_128_dhkemx25519_chacha20poly1305_sha256_ed25519
 
 type mls_principal = {
   who: principal;

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst

@@ -11,7 +11,7 @@ open MLS.Symbolic
 
 #set-options "--fuel 0 --ifuel 0"
 
-[@@ with_bytes dy_bytes]
+[@@ with_bytes bytes]
 type dy_as_token = {
   time: nat;
 }
@@ -22,7 +22,7 @@ type dy_as_token = {
 /// Instantiation of the abstract "Authentication Service" for DY*.
 /// The token is a a timestamp,
 /// and the AS attests that the signature verification key belonged to that principal at that time.
-val dy_asp: {|crypto_invariants|} -> trace -> as_parameters dy_bytes
+val dy_asp: {|crypto_invariants|} -> trace -> as_parameters bytes
 let dy_asp #ci tr = {
   token_t = dy_as_token;
   credential_ok = (fun (vk, cred) token ->

fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst

@@ -22,32 +22,32 @@ open MLS.TreeSync.Symbolic.API
 instance treesync_crypto_usages: crypto_usages =
   default_crypto_usages
 
-val all_signwithlabel_preds: treekem_types dy_bytes -> list (valid_label & signwithlabel_crypto_pred)
+val all_signwithlabel_preds: treekem_types bytes -> list (valid_label & signwithlabel_crypto_pred)
 let all_signwithlabel_preds tkt = [
   leaf_node_tbs_tag_and_invariant tkt;
 ]
 
-val mls_sign_pred: treekem_types dy_bytes -> sign_crypto_predicate
+val mls_sign_pred: treekem_types bytes -> sign_crypto_predicate
 let mls_sign_pred tkt =
   mk_mls_sign_pred (all_signwithlabel_preds tkt)
 
-val all_sign_preds: treekem_types dy_bytes -> list (string & sign_crypto_predicate)
+val all_sign_preds: treekem_types bytes -> list (string & sign_crypto_predicate)
 let all_sign_preds tkt = [
   ("MLS.LeafSignKey", mls_sign_pred tkt)
 ]
 
-val treesync_crypto_predicates: treekem_types dy_bytes -> crypto_predicates
+val treesync_crypto_predicates: treekem_types bytes -> crypto_predicates
 let treesync_crypto_predicates tkt = {
   default_crypto_predicates with
   sign_pred = mk_sign_predicate (all_sign_preds tkt);
 }
 
-instance treesync_crypto_invariants (tkt:treekem_types dy_bytes): crypto_invariants = {
+instance treesync_crypto_invariants (tkt:treekem_types bytes): crypto_invariants = {
   usages = treesync_crypto_usages;
   preds = treesync_crypto_predicates tkt;
 }
 
-val all_state_predicates: tkt:treekem_types dy_bytes -> list (dtuple2 string local_bytes_state_predicate)
+val all_state_predicates: tkt:treekem_types bytes -> list (dtuple2 string local_bytes_state_predicate)
 let all_state_predicates tkt = [
   as_cache_tag_and_invariant;
   group_manager_tag_and_invariant;
@@ -56,42 +56,42 @@ let all_state_predicates tkt = [
   treesync_signature_key_state_tag_and_invariant
 ]
 
-val treesync_trace_invariants: tkt:treekem_types dy_bytes -> trace_invariants
+val treesync_trace_invariants: tkt:treekem_types bytes -> trace_invariants
 let treesync_trace_invariants tkt = {
   state_pred = mk_state_pred (all_state_predicates tkt);
   event_pred = mk_event_pred [];
 }
 
-instance treesync_protocol_invariants (tkt:treekem_types dy_bytes): protocol_invariants = {
+instance treesync_protocol_invariants (tkt:treekem_types bytes): protocol_invariants = {
   crypto_invs = treesync_crypto_invariants tkt;
   trace_invs = treesync_trace_invariants tkt;
 }
 
 (*** Proofs ***)
 
 #push-options "--ifuel 1 --fuel 1"
-val all_signwithlabel_preds_has_all_signwithlabel_preds: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_signwithlabel_preds; `%for_allP]; iota; zeta] (for_allP (has_signwithlabel_pred (mls_sign_pred tkt)) (all_signwithlabel_preds tkt)))
+val all_signwithlabel_preds_has_all_signwithlabel_preds: tkt:treekem_types bytes -> Lemma (norm [delta_only [`%all_signwithlabel_preds; `%for_allP]; iota; zeta] (for_allP (has_signwithlabel_pred (mls_sign_pred tkt)) (all_signwithlabel_preds tkt)))
 let all_signwithlabel_preds_has_all_signwithlabel_preds tkt =
   assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_signwithlabel_preds tkt)));
   mk_mls_sign_pred_correct (mls_sign_pred tkt) (all_signwithlabel_preds tkt);
   norm_spec [delta_only [`%all_signwithlabel_preds; `%for_allP]; iota; zeta] (for_allP (has_signwithlabel_pred (mls_sign_pred tkt)) (all_signwithlabel_preds tkt))
 #pop-options
 
 #push-options "--ifuel 1 --fuel 1"
-val all_sign_preds_has_all_sign_preds: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP has_sign_predicate (all_sign_preds tkt)))
+val all_sign_preds_has_all_sign_preds: tkt:treekem_types bytes -> Lemma (norm [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP has_sign_predicate (all_sign_preds tkt)))
 let all_sign_preds_has_all_sign_preds tkt =
   assert_norm(List.Tot.no_repeats_p (List.Tot.map fst (all_sign_preds tkt)));
   mk_sign_predicate_correct (all_sign_preds tkt);
   norm_spec [delta_only [`%all_sign_preds; `%for_allP]; iota; zeta] (for_allP has_sign_predicate (all_sign_preds tkt))
 #pop-options
 
-val all_state_predicates_has_all_state_predicates: tkt:treekem_types dy_bytes -> Lemma (norm [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP has_local_bytes_state_predicate (all_state_predicates tkt)))
+val all_state_predicates_has_all_state_predicates: tkt:treekem_types bytes -> Lemma (norm [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP has_local_bytes_state_predicate (all_state_predicates tkt)))
 let all_state_predicates_has_all_state_predicates tkt =
   assert_norm(List.Tot.no_repeats_p (List.Tot.map dfst (all_state_predicates tkt)));
   mk_state_pred_correct (all_state_predicates tkt);
   norm_spec [delta_only [`%all_state_predicates; `%for_allP]; iota; zeta] (for_allP has_local_bytes_state_predicate (all_state_predicates tkt))
 
-val treesync_protocol_invariants_has_has_treesync_invariants: tkt:treekem_types dy_bytes -> Lemma
+val treesync_protocol_invariants_has_has_treesync_invariants: tkt:treekem_types bytes -> Lemma
   (has_treesync_invariants tkt)
   [SMTPat (has_treesync_invariants tkt)]
 let treesync_protocol_invariants_has_has_treesync_invariants tkt =