Implement mlswg/mls-protocol#716 (new_member_proposal)

fstar/MLS.NetworkTypes.fst

@@ -400,14 +400,16 @@ noeq type commit_nt (bytes:Type0) {|bytes_like bytes|} = {
 type sender_type_nt =
   | ST_member: [@@@ with_num_tag 1 1] unit -> sender_type_nt
   | ST_external: [@@@ with_num_tag 1 2] unit -> sender_type_nt
-  | ST_new_member: [@@@ with_num_tag 1 3] unit -> sender_type_nt
+  | ST_new_member_proposal: [@@@ with_num_tag 1 3] unit -> sender_type_nt
+  | ST_new_member_commit: [@@@ with_num_tag 1 4] unit -> sender_type_nt
 
 %splice [ps_sender_type_nt] (gen_parser (`sender_type_nt))
 
 noeq type sender_nt (bytes:Type0) {|bytes_like bytes|} =
   | S_member: [@@@ with_tag (ST_member ())] leaf_index:nat_lbytes 4 -> sender_nt bytes
   | S_external: [@@@ with_tag (ST_external ())] sender_index:nat_lbytes 4 -> sender_nt bytes
-  | S_new_member: [@@@ with_tag (ST_new_member ())] unit -> sender_nt bytes
+  | S_new_member_proposal: [@@@ with_tag (ST_new_member_proposal ())] unit -> sender_nt bytes
+  | S_new_member_commit: [@@@ with_tag (ST_new_member_commit ())] unit -> sender_nt bytes
 
 %splice [ps_sender_nt] (gen_parser (`sender_nt))
 
@@ -465,15 +467,17 @@ noeq type mls_message_content_nt (bytes:Type0) {|bytes_like bytes|} = {
 let mls_message_content_tbs_group_context_nt (bytes:Type0) {|bytes_like bytes|} (s:sender_nt bytes) =
   match s with
   | S_member _
-  | S_new_member _ -> group_context_nt bytes
-  | _ -> unit
+  | S_new_member_commit _ -> group_context_nt bytes
+  | S_external _
+  | S_new_member_proposal _ -> unit
 
 val ps_mls_message_content_tbs_group_context_nt: #bytes:Type0 -> {|bytes_like bytes|} -> s:sender_nt bytes -> parser_serializer_unit bytes (mls_message_content_tbs_group_context_nt bytes s)
 let ps_mls_message_content_tbs_group_context_nt #bytes #bl s =
   match s with
   | S_member _
-  | S_new_member _ -> ps_group_context_nt
-  | _ -> ps_unit
+  | S_new_member_commit _ -> ps_group_context_nt
+  | S_external _
+  | S_new_member_proposal _ -> ps_unit
 
 noeq type mls_message_content_tbs_nt (bytes:Type0) {|bytes_like bytes|} = {
   wire_format: wire_format_nt;

fstar/MLS.TreeDEM.Message.Framing.fst

@@ -158,7 +158,7 @@ let compute_message_confirmation_tag #bytes #cb confirmation_key confirmed_trans
 val compute_tbs: #bytes:Type0 -> {|bytes_like bytes|} -> message_content bytes -> option (group_context_nt bytes) -> result (mls_message_content_tbs_nt bytes)
 let compute_tbs #bytes #bl msg group_context =
   content <-- message_content_to_network msg;
-  if not ((NT.S_member? content.sender || NT.S_new_member? content.sender) = Some? group_context) then
+  if not ((NT.S_member? content.sender || NT.S_new_member_commit? content.sender) = Some? group_context) then
     internal_failure "compute_tbs: group_context must be present iff sender is member or new_member"
   else (
     return ({

fstar/MLS.TreeDEM.Message.Types.fst

@@ -11,7 +11,8 @@ module NT = MLS.NetworkTypes
 type sender (bytes:Type0) {|bytes_like bytes|} =
   | S_member: leaf_index:nat -> sender bytes
   | S_external: sender_index:nat -> sender bytes
-  | S_new_member: sender bytes
+  | S_new_member_proposal: sender bytes
+  | S_new_member_commit: sender bytes
 
 noeq type message_content (bytes:Type0) {|bytes_like bytes|} = {
   wire_format: wire_format_nt;
@@ -33,7 +34,8 @@ let network_to_sender #bytes #bl s =
   match s with
   | NT.S_member kp_ref -> return (S_member kp_ref)
   | NT.S_external sender_index -> return (S_external sender_index)
-  | NT.S_new_member () -> return S_new_member
+  | NT.S_new_member_proposal () -> return S_new_member_proposal
+  | NT.S_new_member_commit () -> return S_new_member_commit
   | _ -> error "network_to_sender: invalid sender type"
 
 val sender_to_network: #bytes:Type0 -> {|bytes_like bytes|} -> sender bytes -> result (sender_nt bytes)
@@ -52,7 +54,8 @@ let sender_to_network #bytes #bl s =
       return (NT.S_external sender_index)
     )
   )
-  | S_new_member -> return (NT.S_new_member ())
+  | S_new_member_proposal -> return (NT.S_new_member_proposal ())
+  | S_new_member_commit -> return (NT.S_new_member_commit ())
 
 
 val message_content_to_network: #bytes:Type0 -> {|bytes_like bytes|} -> message_content bytes -> result (mls_message_content_nt bytes)