diff --git a/fstar/api/MLS.API.High.fst b/fstar/api/MLS.API.High.fst
index 450471d..b7afd0f 100644
--- a/fstar/api/MLS.API.High.fst
+++ b/fstar/api/MLS.API.High.fst
@@ -31,11 +31,11 @@ class entropy (bytes:Type0) (t:Type) = {
     (requires x `rel` y /\ y `rel` z)
     (ensures x `rel` z)
   ;
-  extract_entropy_: nat -> x:t -> res:(t & bytes){x `rel` (fst res)}
+  extract_entropy_: nat -> x:t -> res:(bytes & t){x `rel` (snd res)}
 }
 
 let prob (#bytes:Type0) (#entropy_t) {|entropy bytes entropy_t|} (t:Type): Type =
-  x:entropy_t -> res:(entropy_t & t){x `rel` (fst res)}
+  x:entropy_t -> res:(t & entropy_t){x `rel` (snd res)}
 
 val return_prob:
   #bytes:Type0 -> #entropy_t:Type -> {|entropy bytes entropy_t|} ->
@@ -44,17 +44,17 @@ val return_prob:
   prob a
 let return_prob #bytes #entropy_t #entropy_tc #a x e =
   rel_refl e;
-  (e, x)
+  (x, e)
 
 val (let*):
   #bytes:Type0 -> #entropy_t:Type -> {|entropy bytes entropy_t|} ->
   #a:Type -> #b:Type ->
   prob a -> (a -> prob b) -> prob b
 let (let*) #bytes #entropy_t #entropy_tc #a #b x f e0 =
-  let (e1, x_value) = x e0 in
-  let (e2, y_value) = f x_value e1 in
+  let (x_value, e1) = x e0 in
+  let (y_value, e2) = f x_value e1 in
   rel_trans e0 e1 e2;
-  (e2, y_value)
+  (y_value, e2)
 
 #push-options "--ifuel 1"
 val (let*?):
@@ -62,15 +62,15 @@ val (let*?):
   #a:Type -> #b:Type ->
   prob (result a) -> (a -> prob (result b)) -> prob (result b)
 let (let*?) #bytes #entropy_t #entropy_tc #a #b x f e0 =
-  let (e1, x_result) = x e0 in
+  let (x_result, e1) = x e0 in
   match x_result with
   | Success x_value -> (
-    let (e2, y_result) = f x_value e1 in
+    let (y_result, e2) = f x_value e1 in
     rel_trans e0 e1 e2;
-    (e2, y_result)
+    (y_result, e2)
   )
-  | InternalError s -> (e1, InternalError s)
-  | ProtocolError s -> (e1, ProtocolError s)
+  | InternalError s -> (InternalError s, e1)
+  | ProtocolError s -> (ProtocolError s, e1)
 #pop-options
 
 val extract_entropy:  
@@ -277,7 +277,9 @@ type framing_params (bytes:Type0) = {
 }
 
 //TODO
-assume val leaf_node_params (bytes:Type0) {|bytes_like bytes|} (asp:as_parameters bytes): Type0
+type leaf_node_params (bytes:Type0) {|bytes_like bytes|} (asp:as_parameters bytes) = {
+  nothing_yet: unit;
+}
 
 noeq
 type commit_params (bytes:Type0) {|bytes_like bytes|} (asp:as_parameters bytes) = {
@@ -415,6 +417,10 @@ type keystore_value_type (bytes:Type0) {|bytes_like bytes|} = {
   signature_private_key: bytes;
 }
 
+%splice [ps_keystore_value_type] (gen_parser (`keystore_value_type))
+instance parseable_serializeable_keystore_value_type (bytes:Type) {|bytes_like bytes|}: parseable_serializeable bytes (keystore_value_type bytes) =
+  mk_parseable_serializeable ps_keystore_value_type
+
 type create_key_package_result (bytes:Type0) {|bytes_like bytes|} = {
   key_package: key_package_nt bytes tkt;
   // key and value to be added to the store
@@ -897,7 +903,7 @@ val _process_add_proposal_aux:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
   #asp:as_parameters bytes ->
   mls_group bytes asp -> proposal:proposal_and_token bytes asp{P_add? proposal.proposal_token.proposal} ->
-  result (mls_group bytes asp & key_package_nt bytes tkt & nat)
+  result (key_package_nt bytes tkt & nat & mls_group bytes asp)
 let _process_add_proposal_aux #bytes #cb #asp st proposal =
   let P_add {key_package} = proposal.proposal_token.proposal in
   let leaf_node = key_package.tbs.leaf_node in
@@ -911,16 +917,16 @@ let _process_add_proposal_aux #bytes #cb #asp st proposal =
   let? add_pend = MLS.TreeSync.API.prepare_add st.treesync leaf_node in
   let? (treesync, _) = MLS.TreeSync.API.finalize_add add_pend proposal.proposal_token.token in
   let (treekem, add_index) = MLS.TreeKEM.API.add st.treekem ({public_key = key_package.tbs.leaf_node.data.content;}) in
-  return (({ st with treesync; treekem } <: mls_group bytes asp), key_package, add_index)
+  return (key_package, add_index, ({ st with treesync; treekem } <: mls_group bytes asp))
 
 val _process_add_proposal:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
   #asp:as_parameters bytes ->
-  (mls_group bytes asp & list (key_package_nt bytes tkt & nat)) -> proposal:proposal_and_token bytes asp{P_add? proposal.proposal_token.proposal} ->
-  result (mls_group bytes asp & list (key_package_nt bytes tkt & nat))
-let _process_add_proposal #bytes #cb #asp (st, l) proposal =
-  let? (st, key_package, add_index) = _process_add_proposal_aux st proposal in
-  return (st, (key_package, add_index)::l)
+  (list (key_package_nt bytes tkt & nat) & mls_group bytes asp) -> proposal:proposal_and_token bytes asp{P_add? proposal.proposal_token.proposal} ->
+  result (list (key_package_nt bytes tkt & nat) & mls_group bytes asp)
+let _process_add_proposal #bytes #cb #asp (l, st) proposal =
+  let? (key_package, add_index, st) = _process_add_proposal_aux st proposal in
+  return ((key_package, add_index)::l, st)
 
 val _process_update_proposal:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
@@ -1005,14 +1011,14 @@ val _process_proposals:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
   #asp:as_parameters bytes ->
   mls_group bytes asp -> list (proposal_and_token bytes asp) ->
-  result (mls_group bytes asp & list (key_package_nt bytes tkt & nat) & list (proposal_and_token bytes asp))
+  result (list (key_package_nt bytes tkt & nat) & list (proposal_and_token bytes asp) & mls_group bytes asp)
 let _process_proposals #bytes #cb #asp st proposals =
   let sorted_proposals = _sort_proposals proposals in
   let? st = fold_leftM _process_group_context_extensions_proposal st sorted_proposals.group_context_extensions in
   let? st = fold_leftM _process_update_proposal st sorted_proposals.updates in
   let? st = fold_leftM _process_remove_proposal st sorted_proposals.removes in
-  let? (st, adds) = fold_leftM _process_add_proposal (st, []) sorted_proposals.adds in
-  return (st, adds, sorted_proposals.other)
+  let? (adds, st) = fold_leftM _process_add_proposal ([], st) sorted_proposals.adds in
+  return (adds, sorted_proposals.other, st)
 
 val _merge_update_path:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
@@ -1106,7 +1112,7 @@ let merge_commit #bytes #cb #asp st valid_commit =
       // Apply proposals
       let (path_token, proposal_tokens) = valid_commit.tokens in
       let? proposals_and_tokens = _get_all_proposals st commit_msg.content.sender commit.proposals proposal_tokens in
-      let? (st, new_members, other_proposals) = _process_proposals st proposals_and_tokens in
+      let? (new_members, other_proposals, st) = _process_proposals st proposals_and_tokens in
       assume(my_leaf_index == st.my_leaf_index);
 
       let? (new_treesync, pending_treekem, provisional_group_context) = (
@@ -1403,7 +1409,7 @@ val _generate_update_path:
   prob #bytes #entropy_t (result (generate_update_path_result bytes asp st.group_context.group_id st.my_leaf_index))
 let _generate_update_path #bytes #cb #entropy_t #entropy_tc #asp st lnparams proposals_tokens =
   let first_st = st in
-  let*? (st, new_members, other_proposals) = return_prob (_process_proposals st proposals_tokens) in
+  let*? (new_members, other_proposals, st) = return_prob (_process_proposals st proposals_tokens) in
   let st: mls_group bytes asp = st in
   assume(st.my_leaf_index == first_st.my_leaf_index);
   assume(st.group_context.group_id == first_st.group_context.group_id);
diff --git a/fstar/api/MLS.API.fst b/fstar/api/MLS.API.fst
new file mode 100644
index 0000000..486fd39
--- /dev/null
+++ b/fstar/api/MLS.API.fst
@@ -0,0 +1,256 @@
+module MLS.API
+
+open MLS.TreeSync.Invariants.AuthService
+open MLS.NetworkTypes
+open MLS.TreeSync.NetworkTypes
+open MLS.TreeKEM.NetworkTypes
+open MLS.TreeDEM.NetworkTypes
+
+val no_asp:
+  #bytes:Type0 -> {|bytes_like bytes|} ->
+  as_parameters bytes
+let no_asp #bytes #bl = {
+  token_t = unit;
+  credential_ok = (fun _ _ -> True);
+  valid_successor = (fun _ _ -> True);
+}
+
+instance high_entropy (bytes:Type0) (entropy_t:Type) {|entropy bytes entropy_t|}: MLS.API.High.entropy bytes entropy_t = {
+  rel = (fun _ _ -> True);
+  rel_refl = (fun _ -> ());
+  rel_trans = (fun _ _ _ -> ());
+  extract_entropy_ = (fun n e -> extract_entropy n e);
+}
+
+// workaround for FStarLang/FStar#3311
+// to avoid having to `let open MLS.API.High`
+// and then having to reference our types / functions with MLS.API._
+val (let*?):
+  #bytes:Type0 -> #entropy_t:Type -> {|entropy bytes entropy_t|} ->
+  #a:Type -> #b:Type ->
+  MLS.API.High.prob (result a) -> (a -> MLS.API.High.prob (result b)) -> MLS.API.High.prob (result b)
+let (let*?) #bytes #entropy_t #entropy_tc #a #b x f =
+  let open MLS.API.High in
+  let*? x0 = x in
+  f x0
+
+type mls_group bytes #cb = MLS.API.High.mls_group bytes no_asp
+type unvalidated_proposal bytes #cb = MLS.API.High.unvalidated_proposal bytes
+type validated_proposal bytes #cb = MLS.API.High.validated_proposal bytes no_asp
+type unvalidated_commit bytes #cb = MLS.API.High.unvalidated_commit bytes
+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
+
+let generate_signature_keypair #bytes #cb #entropy_t #entropy_tc =
+  MLS.API.High.generate_signature_keypair
+
+let get_signature_public_key #bytes #cb sig_keypair =
+  MLS.API.High.get_signature_public_key sig_keypair
+
+let mk_basic_credential #bytes #cb sig_keypair identity =
+  let? identity = mk_mls_bytes identity "mk_basic_credential" "identity" in
+  let cred = MLS.NetworkTypes.C_basic identity in
+  return (MLS.API.High.mk_credential sig_keypair cred ())
+
+let mk_x509_credential #bytes #cb sig_keypair x509_chain =
+  let? x509_chain = mapM (fun x -> mk_mls_bytes x "mk_x509_credential" "certificate") x509_chain in
+  let? x509_chain = mk_mls_list x509_chain "mk_basic_credential" "x509_chain" in
+  let cred = MLS.NetworkTypes.C_x509 x509_chain in
+  return (MLS.API.High.mk_credential sig_keypair cred ())
+
+let get_public_credential #bytes #cb cred_pair =
+  MLS.API.High.get_public_credential cred_pair
+
+let create_key_package #bytes #cb #entropy #entropy_t cred_pair =
+  let*? res = MLS.API.High.create_key_package cred_pair in
+  MLS.API.High.return_prob (return ({
+    key_package = serialize _ res.key_package;
+    keystore_key = res.keystore_key;
+    keystore_value = serialize _ res.keystore_value;
+  } <: create_key_package_result bytes))
+
+let create_group #bytes #cb #entropy_t #entropy_tc cred_pair =
+  MLS.API.High.create_group cred_pair
+
+let start_join_group_output bytes #cb = MLS.API.High.start_join_group_output bytes
+
+val lift_key_lookup:
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  key_lookup bytes ->
+  MLS.API.High.key_lookup bytes
+let lift_key_lookup #bytes #cb key_lookup b =
+  match key_lookup b with
+  | None -> None
+  | Some k -> parse _ k
+
+let start_join_group #bytes #cb welcome_bytes key_lookup =
+  let? welcome = from_option "start_join_group: malformed welcome" (parse _ welcome_bytes) in
+  MLS.API.High.start_join_group welcome (lift_key_lookup key_lookup)
+
+let continue_join_group_output bytes #cb = MLS.API.High.continue_join_group_output bytes
+
+let continue_join_group #bytes #cb step_before opt_ratchet_tree_bytes =
+  let? opt_ratchet_tree =
+    match opt_ratchet_tree_bytes with
+    | None -> return None
+    | Some ratchet_tree_bytes ->
+      let? ratchet_tree = from_option "continue_join_group: malformed ratchet tree" (parse _ ratchet_tree_bytes) in
+      return (Some ratchet_tree)
+  in
+  MLS.API.High.continue_join_group step_before opt_ratchet_tree
+
+val create_tokens:
+  #bytes:Type0 -> {|bytes_like bytes|} ->
+  leaves:list (option (leaf_node_nt bytes tkt)) ->
+  tokens:list (option ((no_asp #bytes).token_t)){List.Tot.length tokens == List.Tot.length leaves}
+let rec create_tokens #bytes #bl leaves =
+  match leaves with
+  | [] -> []
+  | h::t ->
+    (
+      match h with
+      | Some _ -> Some ()
+      | None -> None
+    )::(create_tokens t)
+
+let finalize_join_group #bytes #cb step_before =
+  MLS.API.High.finalize_join_group step_before (create_tokens (MLS.Tree.get_leaf_list step_before.treesync))
+
+let export_secret #bytes #cb st label context len =
+  MLS.API.High.export_secret st label context len
+
+let epoch_authenticator #bytes #cb st =
+  return (MLS.API.High.epoch_authenticator st)
+
+let epoch #bytes #cb st =
+  return (MLS.API.High.epoch st)
+
+let get_new_credentials #bytes #cb commit =
+  magic()
+
+let get_new_credential #bytes #cb proposal =
+  magic()
+
+let process_message #bytes #cb st msg_bytes =
+  let? msg = from_option "process_message: malformed message" (parse _ msg_bytes) in
+  let? (res, st) = MLS.API.High.process_message st msg in
+  let translated_res_content =
+    match res.content with
+    | MLS.API.High.ApplicationMessage msg -> ApplicationMessage msg
+    | MLS.API.High.Proposal proposal -> Proposal proposal
+    | MLS.API.High.Commit commit -> Commit commit
+  in
+  let translated_res = {
+    group_id = res.group_id;
+    epoch = res.epoch;
+    sender = res.sender;
+    authenticated_data = res.authenticated_data;
+    content = translated_res_content;
+  } in
+  return (translated_res, st)
+
+val mk_proposal_token_for:
+  #bytes:Type0 -> {|bytes_like bytes|} ->
+  proposal:proposal_nt bytes ->
+  MLS.API.High.proposal_token_for no_asp proposal
+let mk_proposal_token_for #bytes #bl proposal = ()
+
+val mk_proposal_tokens_for:
+  #bytes:Type0 -> {|bytes_like bytes|} ->
+  proposals: list (proposal_nt bytes) ->
+  MLS.API.High.list_to_type (List.Tot.map (MLS.API.High.proposal_token_for no_asp) proposals)
+let rec mk_proposal_tokens_for #bytes #bl l =
+  match l with
+  | [] -> ()
+  | h::t ->
+    (mk_proposal_token_for h, mk_proposal_tokens_for t)
+
+val mk_update_path_token:
+  #bytes:Type0 -> {|bytes_like bytes|} ->
+  opt_path:option (update_path_nt bytes) ->
+  MLS.API.High.update_path_token no_asp opt_path
+let mk_update_path_token #bytes #bl opt_path = ()
+
+val mk_commit_tokens_for:
+  #bytes:Type0 -> {|bytes_like bytes|} ->
+  commit:commit_nt bytes ->
+  MLS.API.High.commit_tokens_for no_asp commit
+let mk_commit_tokens_for #bytes #bl commit =
+  (mk_update_path_token commit.path, mk_proposal_tokens_for (MLS.API.High.filter_and_map MLS.API.High._get_proposal commit.proposals))
+
+let i_hereby_declare_that_i_have_checked_the_new_credentials_and_validate_the_commit #bytes #cb commit =
+  {
+    commit;
+    tokens = mk_commit_tokens_for commit.commit_msg.content.content.content;
+  }
+
+let merge_commit #bytes #cb st commit =
+  MLS.API.High.merge_commit st commit
+
+let i_hereby_declare_that_i_have_checked_the_new_credentials_and_validate_the_proposal #bytes #cb proposal = {
+  proposal;
+  token = mk_proposal_token_for proposal.proposal_msg.content.content.content;
+}
+
+let queue_new_proposal #bytes #cb st proposal =
+  MLS.API.High.queue_new_proposal st proposal
+
+val translate_framing_params:
+  #bytes:Type0 -> {|bytes_like bytes|} ->
+  framing_params bytes ->
+  MLS.API.High.framing_params bytes
+let translate_framing_params #bytes #bl fparams =
+  let { encrypt; padding_size; authenticated_data; } = fparams in
+  { encrypt; padding_size; authenticated_data; }
+
+let send_application_message #bytes #cb #entropy_t #entropy_tc st fparams message =
+  let*? (msg, st) = MLS.API.High.send_application_message st (translate_framing_params fparams) message in
+  MLS.API.High.return_prob (return (serialize _ msg, st))
+
+let propose_add_member #bytes #cb #entropy_t #entropy_tc st fparams key_package_bytes =
+  let*? key_package = MLS.API.High.return_prob (from_option "propose_add_member: malformed key package" (parse _ key_package_bytes)) in
+  let*? (msg, st) = MLS.API.High.propose_add_member st (translate_framing_params fparams) key_package in
+  MLS.API.High.return_prob (return (serialize _ msg, st))
+
+let propose_remove_member #bytes #cb #entropy_t #entropy_tc st fparams cred_to_remove =
+  let*? (msg, st) = MLS.API.High.propose_remove_member st (translate_framing_params fparams) cred_to_remove.cred in
+  MLS.API.High.return_prob (return (serialize _ msg, st))
+
+let propose_remove_myself #bytes #cb #entropy_t #entropy_tc st fparams =
+  let*? (msg, st) = MLS.API.High.propose_remove_myself st (translate_framing_params fparams) in
+  MLS.API.High.return_prob (return (serialize _ msg, st))
+
+val translate_leaf_node_params:
+  #bytes:Type0 -> {|bytes_like bytes|} ->
+  leaf_node_params bytes ->
+  MLS.API.High.leaf_node_params bytes no_asp
+let translate_leaf_node_params #bytes #bl lnparams =
+  let { nothing_yet } = lnparams in
+  { nothing_yet }
+
+val translate_commit_params:
+  #bytes:Type0 -> {|bytes_like bytes|} ->
+  commit_params bytes ->
+  MLS.API.High.commit_params bytes no_asp
+let translate_commit_params #bytes #bl cparams =
+  let { proposals; inline_tree; force_update; leaf_node_params; } = cparams in
+  {
+    proposals = List.Tot.map (fun proposal -> { proposal; token = mk_proposal_token_for proposal; } <: MLS.API.High.bare_proposal_and_token bytes no_asp) proposals;
+    inline_tree;
+    force_update;
+    leaf_node_params = translate_leaf_node_params leaf_node_params;
+  }
+
+let create_commit #bytes #cb st fparams cparams =
+  let*? (commit, opt_welcome, group_info, st) = MLS.API.High.create_commit st (translate_framing_params fparams) (translate_commit_params cparams) in
+  MLS.API.High.return_prob (return ({
+    commit = serialize _ commit;
+    welcome = (
+      match opt_welcome with
+      | None -> None
+      | Some welcome -> Some (serialize _ welcome)
+    );
+    group_info = serialize _ group_info;
+  }, st))
diff --git a/fstar/api/MLS.API.fsti b/fstar/api/MLS.API.fsti
index 7bb8f51..3f2a32a 100644
--- a/fstar/api/MLS.API.fsti
+++ b/fstar/api/MLS.API.fsti
@@ -1,88 +1,102 @@
 module MLS.API
 
-/// Basic types that will be completed later
-val uint64: eqtype
-val bytes: eqtype
-val result: Type -> Type
+open Comparse
+
+open MLS.Result
+open MLS.Crypto
 
 /// Entropy typeclass
 
-class entropy (t:Type) = {
-  extract_entropy: t -> nat -> (bytes & t)
+[@@FStar.Tactics.Typeclasses.fundeps [0;1]]
+class entropy (bytes:Type0) (t:Type) = {
+  extract_entropy: nat -> t -> (bytes & t)
 }
 
+type prob (#bytes:Type0) (#entropy_t:Type) {|entropy bytes entropy_t|} (a:Type) = entropy_t -> (a & entropy_t)
+
 /// Types that are abstract
-type mls_group
-type unvalidated_proposal
-type validated_proposal
-type unvalidated_commit
-type validated_commit
-type credential
-type credential_pair
-type signature_keypair
-
-type framing_params = {
+val mls_group: bytes:Type0 -> {|crypto_bytes bytes|} -> Type0
+val unvalidated_proposal: bytes:Type0 -> {|crypto_bytes bytes|} -> Type0
+val validated_proposal: bytes:Type0 -> {|crypto_bytes bytes|} -> Type0
+val unvalidated_commit: bytes:Type0 -> {|crypto_bytes bytes|} -> Type0
+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
+
+type framing_params (bytes:Type0) = {
   // Should we encrypt the message?
   encrypt: bool;
   // How much padding to add
   padding_size: nat;
+  //
+  authenticated_data: bytes;
+}
+
+type leaf_node_params (bytes:Type0) {|bytes_like bytes|} = {
+  nothing_yet: unit;
 }
 
-type commit_params = {
+noeq
+type commit_params (bytes:Type0) {|bytes_like bytes|} = {
   // Extra proposals to include in the commit
-  proposals: unit; //TODO
+  proposals: list (MLS.TreeDEM.NetworkTypes.proposal_nt 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?
   force_update: bool;
   // Options for the generation of the new leaf node
-  leaf_node_options: unit; //TODO
+  leaf_node_params: leaf_node_params bytes;
 }
 
+
 noeq
-type processed_message_content =
-  | ApplicationMessage: bytes -> processed_message_content
-  | Proposal: unvalidated_proposal -> processed_message_content
-  | Commit: unvalidated_commit -> processed_message_content
+type processed_message_content (bytes:Type0) {|crypto_bytes bytes|} =
+  | ApplicationMessage: bytes -> processed_message_content bytes
+  | Proposal: unvalidated_proposal bytes -> processed_message_content bytes
+  | Commit: unvalidated_commit bytes -> processed_message_content bytes
 
 noeq
-type processed_message = {
+type processed_message (bytes:Type0) {|crypto_bytes bytes|} = {
   group_id: bytes;
-  epoch: uint64;
+  epoch: nat_lbytes 8;
   sender: unit; //TODO
   authenticated_data: bytes;
-  content: processed_message_content;
-  credential: credential;
+  content: processed_message_content bytes;
 }
 
 (*** Credentials ***)
 
 val generate_signature_keypair:
-  #entropy_t:Type0 -> {|entropy entropy_t|} ->
-  entropy_t ->
-  entropy_t & result signature_keypair
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  #entropy_t:Type0 -> {|entropy bytes entropy_t|} ->
+  prob (result (signature_keypair bytes))
 
 val get_signature_public_key:
-  signature_keypair ->
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  signature_keypair bytes ->
   bytes
 
 val mk_basic_credential:
-  signature_keypair -> identity:bytes ->
-  result credential_pair
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  signature_keypair bytes -> identity:bytes ->
+  result (credential_pair bytes)
 
 val mk_x509_credential:
-  signature_keypair -> x509_chain:list bytes ->
-  result credential_pair
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  signature_keypair bytes -> x509_chain:list bytes ->
+  result (credential_pair bytes)
 
 val get_public_credential:
-  credential_pair ->
-  credential
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  credential_pair bytes ->
+  credential bytes
 
 // TODO inspect a credential
 
 (*** Create key package ***)
 
-type create_key_package_result = {
+type create_key_package_result (bytes:Type0) {|crypto_bytes bytes|} = {
   key_package: bytes;
   // key and value to be added to the store
   keystore_key: bytes;
@@ -90,56 +104,74 @@ type create_key_package_result = {
 }
 
 val create_key_package:
-  #entropy_t:Type0 -> {|entropy entropy_t|} ->
-  entropy_t ->
-  credential_pair ->
-  entropy_t & (result create_key_package_result)
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  #entropy_t:Type0 -> {|entropy bytes entropy_t|} ->
+  credential_pair bytes ->
+  prob (result (create_key_package_result bytes))
 
 (*** Group creation ***)
 
 val create_group:
-  #entropy_t:Type0 -> {|entropy entropy_t|} ->
-  entropy_t ->
-  credential_pair ->
-  entropy_t & (result mls_group)
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  #entropy_t:Type0 -> {|entropy bytes entropy_t|} ->
+  credential_pair bytes ->
+  prob (result (mls_group bytes))
+
+let key_lookup (bytes:Type0) = bytes -> option bytes
+
+val start_join_group_output: bytes:Type0 -> {|crypto_bytes bytes|} -> Type0
 
-let key_lookup = bytes -> option bytes
-val join_group:
+val start_join_group:
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
   welcome:bytes ->
-  key_lookup ->
-  result mls_group
+  key_lookup bytes ->
+  result (start_join_group_output bytes)
 
-val join_with_external_commit:
-  unit -> //TODO
-  result mls_group
+val continue_join_group_output: bytes:Type0 -> {|crypto_bytes bytes|} -> Type0
+
+val continue_join_group:
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  start_join_group_output bytes -> opt_ratchet_tree:option bytes ->
+  result (continue_join_group_output bytes)
+
+// TODO: I hereby thing for welcome?
+
+val finalize_join_group:
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  step_before:continue_join_group_output bytes ->
+  result (mls_group bytes)
+
+// val join_with_external_commit:
+//   #bytes:Type0 -> {|crypto_bytes bytes|} ->
+//   unit -> //TODO
+//   result (mls_group bytes)
 
 (*** Export data from the group ***)
 
 val export_secret:
-  mls_group ->
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  mls_group bytes ->
   label:string -> context:bytes -> len:nat ->
   result bytes
 
 val epoch_authenticator:
-  mls_group ->
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  mls_group bytes ->
   result bytes
 
 val epoch:
-  mls_group ->
-  result uint64
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  mls_group bytes ->
+  result FStar.UInt64.t
 
 // TODO: get resumption PSK? Or is it useless for the application?
 
-// TODO: not sure how it is useful. Maybe for external commits?
-val group_info:
-  mls_group ->
-  result bytes
-
 (*** Inspect commit ***)
 
 val get_new_credentials:
-  unvalidated_commit ->
-  result (list credential)
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  unvalidated_commit bytes ->
+  result (list (credential bytes))
 
 // TODO:
 // - roster update (added, updated, removed members)
@@ -154,87 +186,97 @@ val get_new_credentials:
 // TODO more getters
 
 val get_new_credential:
-  unvalidated_proposal ->
-  result (option credential)
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  unvalidated_proposal bytes ->
+  result (option (credential bytes))
 
 (*** Process messages ***)
 
 // Returns a new group because some keys are ratcheted forward?
 val process_message:
-  mls_group ->
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  mls_group bytes ->
   bytes ->
-  result (mls_group & processed_message)
+  result (processed_message bytes & mls_group bytes)
 
 val i_hereby_declare_that_i_have_checked_the_new_credentials_and_validate_the_commit:
-  unvalidated_commit ->
-  validated_commit
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  unvalidated_commit bytes ->
+  validated_commit bytes
 
 val merge_commit:
-  mls_group ->
-  validated_commit ->
-  result mls_group
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  mls_group bytes ->
+  validated_commit bytes ->
+  result (mls_group bytes)
 
 val i_hereby_declare_that_i_have_checked_the_new_credentials_and_validate_the_proposal:
-  unvalidated_proposal ->
-  validated_proposal
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  unvalidated_proposal bytes ->
+  validated_proposal bytes
 
 val queue_new_proposal:
-  mls_group ->
-  validated_proposal ->
-  result mls_group
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  mls_group bytes ->
+  validated_proposal bytes ->
+  result (mls_group bytes)
 
 (*** Send messages ***)
 
 // Authenticated data is sent in plaintext!
 val send_application_message:
-  #entropy_t:Type0 -> {|entropy entropy_t|} ->
-  entropy_t ->
-  mls_group ->
-  framing_params ->
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  #entropy_t:Type0 -> {|entropy bytes entropy_t|} ->
+  mls_group bytes ->
+  framing_params bytes ->
   message:bytes ->
-  authenticated_data:bytes ->
-  entropy_t & bytes
+  prob (result (bytes & mls_group bytes))
 
 (*** Send proposals ***)
 
 val propose_add_member:
-  #entropy_t:Type0 -> {|entropy entropy_t|} ->
-  entropy_t ->
-  mls_group ->
-  framing_params ->
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  #entropy_t:Type0 -> {|entropy bytes entropy_t|} ->
+  mls_group bytes ->
+  framing_params bytes ->
   key_package:bytes ->
-  entropy_t & (result bytes)
+  prob (result (bytes & mls_group bytes))
 
 val propose_remove_member:
-  #entropy_t:Type0 -> {|entropy entropy_t|} ->
-  entropy_t ->
-  mls_group ->
-  framing_params ->
-  removed:credential ->
-  entropy_t & (result bytes)
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  #entropy_t:Type0 -> {|entropy bytes entropy_t|} ->
+  mls_group bytes ->
+  framing_params bytes ->
+  removed:credential bytes ->
+  prob (result (bytes & mls_group bytes))
 
 val propose_remove_myself:
-  #entropy_t:Type0 -> {|entropy entropy_t|} ->
-  entropy_t ->
-  mls_group ->
-  framing_params ->
-  entropy_t & (result bytes)
-
-val propose_external_psk:
-  #entropy_t:Type0 -> {|entropy entropy_t|} ->
-  entropy_t ->
-  mls_group ->
-  framing_params ->
-  psk:unit -> // TODO
-  entropy_t & (result bytes)
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  #entropy_t:Type0 -> {|entropy bytes entropy_t|} ->
+  mls_group bytes ->
+  framing_params bytes ->
+  prob (result (bytes & mls_group bytes))
+
+// val propose_external_psk:
+//   #bytes:Type0 -> {|crypto_bytes bytes|} ->
+//   #entropy_t:Type0 -> {|entropy bytes entropy_t|} ->
+//   mls_group bytes ->
+//   framing_params bytes ->
+//   psk:unit -> // TODO
+//   prob (result (bytes & mls_group bytes))
 
 (*** Create commit ***)
 
-val create_commit:
-  #entropy_t:Type0 -> {|entropy entropy_t|} ->
-  entropy_t ->
-  mls_group ->
-  framing_params ->
-  commit_params ->
-  entropy_t & bytes
+type create_commit_result (bytes:Type0) {|crypto_bytes bytes|} = {
+  commit: bytes;
+  welcome: option bytes;
+  group_info: bytes;
+}
 
+val create_commit:
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  #entropy_t:Type0 -> {|entropy bytes entropy_t|} ->
+  mls_group bytes ->
+  framing_params bytes ->
+  commit_params bytes ->
+  prob (result (create_commit_result bytes & mls_group bytes))