Implement mlswg/mls-protocol#659

fstar/MLS.NetworkTypes.fst

@@ -420,11 +420,9 @@ type wire_format_nt =
 
 %splice [ps_wire_format_nt] (gen_parser (`wire_format_nt))
 
-noeq type mac_nt (bytes:Type0) {|bytes_like bytes|} = {
-  mac_value: mls_bytes bytes;
-}
-
-%splice [ps_mac_nt] (gen_parser (`mac_nt))
+type mac_nt (bytes:Type0) {|bytes_like bytes|} = mls_bytes bytes
+val ps_mac_nt: #bytes:Type0 -> {|bytes_like bytes|} -> parser_serializer bytes (mac_nt bytes)
+let ps_mac_nt #bytes #bl = ps_mls_bytes
 
 type content_type_nt =
   | CT_application: [@@@ with_num_tag 1 1] unit -> content_type_nt

fstar/MLS.TreeDEM.Message.Framing.fst

@@ -47,8 +47,7 @@ let network_to_message_plaintext #bytes #bl pt =
   auth <-- network_to_message_auth pt.auth;
   let membership_tag: option bytes =
     if NT.S_member? pt.content.sender then (
-      let res: mac_nt bytes = pt.membership_tag in
-      Some res.mac_value
+      Some pt.membership_tag
     ) else None
   in
   return ({
@@ -69,7 +68,7 @@ let message_plaintext_to_network #bytes #bl pt =
     return ({
       content;
       auth;
-      membership_tag = if NT.S_member? content.sender then ({mac_value = Some?.v pt.membership_tag} <: mac_nt bytes) else ();
+      membership_tag = if NT.S_member? content.sender then (Some?.v pt.membership_tag) else ();
     } <: mls_plaintext_nt bytes)
   )
 

fstar/MLS.TreeDEM.Message.Transcript.fst

@@ -29,7 +29,7 @@ let compute_interim_transcript_hash #bytes #cb confirmation_tag confirmed_transc
     internal_failure "compute_interim_transcript_hash: confirmation_tag too long"
   else (
     let serialized_auth = serialize (mls_message_commit_auth_data_nt bytes) ({
-      confirmation_tag = {mac_value = confirmation_tag};
+      confirmation_tag;
     }) in
     hash_hash (concat confirmed_transcript_hash serialized_auth)
   )

fstar/MLS.TreeDEM.Message.Types.fst

@@ -101,16 +101,15 @@ let message_auth_to_network #bytes #bl #content_type msg_auth =
   else (
     return ({
       signature = msg_auth.signature;
-      confirmation_tag = if content_type = CT_commit () then ({mac_value = Some?.v msg_auth.confirmation_tag} <: mac_nt bytes) else ();
+      confirmation_tag = if content_type = CT_commit () then (Some?.v msg_auth.confirmation_tag) else ();
     } <: mls_message_auth_nt bytes content_type)
   )
 
 val network_to_message_auth: #bytes:Type0 -> {|bytes_like bytes|} -> #content_type:content_type_nt -> mls_message_auth_nt bytes content_type -> result (message_auth bytes)
 let network_to_message_auth #bytes #bl #content_type msg_auth =
   let confirmation_tag: option bytes =
     if content_type = CT_commit() then (
-      let mac: mac_nt bytes = msg_auth.confirmation_tag in
-      Some mac.mac_value
+      Some msg_auth.confirmation_tag
     ) else None
   in
   return ({

fstar/MLS.TreeDEM.Welcome.fst

@@ -59,7 +59,7 @@ let network_to_welcome_group_info #bytes #bl gi =
     confirmed_transcript_hash = gi.tbs.confirmed_transcript_hash;
     group_context_extensions = gi.tbs.group_context_extensions;
     other_extensions = gi.tbs.other_extensions;
-    confirmation_tag = gi.tbs.confirmation_tag.mac_value;
+    confirmation_tag = gi.tbs.confirmation_tag;
     signer = gi.tbs.signer;
     signature = gi.signature;
   }
@@ -95,7 +95,7 @@ let welcome_group_info_to_network #bytes #bl gi =
         confirmed_transcript_hash = gi.confirmed_transcript_hash;
         group_context_extensions = gi.group_context_extensions;
         other_extensions = gi.other_extensions;
-        confirmation_tag = {mac_value = gi.confirmation_tag};
+        confirmation_tag = gi.confirmation_tag;
         signer = gi.signer;
       };
       signature = gi.signature;