Merge branch 'revised_api_please_rebase_before_merging' of github.com…

…:inria-prosecco/mls-star into revised_api_please_rebase_before_merging

fstar/api/MLS.API.fst

@@ -42,6 +42,7 @@ type validated_commit bytes #cb = MLS.API.High.validated_commit bytes no_asp
 type credential bytes #cb = MLS.API.High.credential bytes
 type credential_pair bytes #cb = MLS.API.High.credential_pair bytes no_asp
 type signature_keypair bytes #cb = MLS.API.High.signature_keypair bytes
+type proposal bytes #bl = MLS.TreeDEM.NetworkTypes.proposal_nt bytes
 
 let generate_signature_keypair #bytes #cb #entropy_t #entropy_tc =
   MLS.API.High.generate_signature_keypair
@@ -257,3 +258,16 @@ let create_commit #bytes #cb st fparams cparams =
     );
     group_info = serialize _ group_info;
   }, st))
+
+let create_add_proposal #bytes #cb key_package =
+  match Comparse.parse (MLS.Bootstrap.NetworkTypes.key_package_nt bytes MLS.TreeKEM.NetworkTypes.tkt) key_package with
+  | Some key_package -> return (MLS.TreeDEM.NetworkTypes.P_add { key_package })
+  | None -> error "create_add_proposal: malformed key package"
+
+let create_remove_proposal #bytes #cb st removed_cred =
+  let? removed = MLS.API.High.find_credential removed_cred.cred (MLS.Tree.get_leaf_list st.treesync.tree) in
+  let? (): squash(removed < pow2 32) = (
+    if not (removed < pow2 32) then error "create_remove_proposal: removed too big"
+    else return ()
+  ) in
+  return (MLS.TreeDEM.NetworkTypes.P_remove { removed })

fstar/api/MLS.API.fsti

@@ -23,6 +23,7 @@ val validated_commit: bytes:Type0 -> {|crypto_bytes bytes|} -> Type0
 val credential: bytes:Type0 -> {|crypto_bytes bytes|} -> Type0
 val credential_pair: bytes:Type0 -> {|crypto_bytes bytes|} -> Type0
 val signature_keypair: bytes:Type0 -> {|crypto_bytes bytes|} -> Type0
+val proposal: bytes:Type0 -> {|bytes_like bytes|} -> Type0
 
 type framing_params (bytes:Type0) = {
   // Should we encrypt the message?
@@ -40,7 +41,7 @@ type leaf_node_params (bytes:Type0) {|bytes_like bytes|} = {
 noeq
 type commit_params (bytes:Type0) {|bytes_like bytes|} = {
   // Extra proposals to include in the commit
-  proposals: list (MLS.TreeDEM.NetworkTypes.proposal_nt bytes);
+  proposals: list (proposal bytes);
   // Should we inline the ratchet tree in the Welcome messages?
   inline_tree: bool;
   // Should we force the UpdatePath even if we could do an add-only commit?
@@ -285,3 +286,16 @@ val create_commit:
   framing_params bytes ->
   commit_params bytes ->
   prob (result (create_commit_result bytes & mls_group bytes))
+
+(*** Create proposals to inline in a commit ***)
+
+val create_add_proposal:
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  key_package:bytes ->
+  result (proposal bytes)
+
+val create_remove_proposal:
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  mls_group bytes ->
+  removed:credential bytes ->
+  result (proposal bytes)

fstar/api/MLS.fst

@@ -53,11 +53,7 @@ let add state key_package e =
     padding_size = 0;
     authenticated_data = Seq.empty;
   } in
-  let? add_proposal =
-    match Comparse.parse (MLS.Bootstrap.NetworkTypes.key_package_nt bytes MLS.TreeKEM.NetworkTypes.tkt) key_package with
-    | Some key_package -> return (MLS.TreeDEM.NetworkTypes.P_add { key_package })
-    | None -> error "add: malformed key package"
-  in
+  let? add_proposal = MLS.API.create_add_proposal key_package in
   let cparams = {
     // Extra proposals to include in the commit
     proposals = [add_proposal];
@@ -84,21 +80,16 @@ let add state key_package e =
 
 let remove state p e =
   //TODO breaking abstraction here
-  let? removed = MLS.API.High.find_credential (MLS.NetworkTypes.C_basic p) (MLS.Tree.get_leaf_list state.treesync.tree) in
-  let? (): squash (removed < pow2 32) =
-    if not (removed < pow2 32) then
-      internal_failure "remove: removed too big"
-    else
-      return ()
-  in
+  //exploiting the fact that the function do not look for the public key (but maybe it should?)
+  let? remove_proposal = MLS.API.create_remove_proposal state ({ cred = MLS.NetworkTypes.C_basic p; signature_public_key = Comparse.empty #bytes }) in
   let fparams = {
     encrypt = true;
     padding_size = 0;
     authenticated_data = Seq.empty;
   } in
   let cparams = {
     // Extra proposals to include in the commit
-    proposals = [MLS.TreeDEM.NetworkTypes.P_remove {removed}];
+    proposals = [remove_proposal];
     // Should we inline the ratchet tree in the Welcome messages?
     inline_tree = true;
     // Should we force the UpdatePath even if we could do an add-only commit?