cleanup: treesync_to_treekem can't fail

fstar/api/MLS.fst

@@ -372,7 +372,7 @@ let create e cred private_sign_key group_id =
     //TODO AS check
     return (MLS.TreeSync.API.finalize_create create_pend ())
   ) in
-  let? treekem = treesync_to_treekem treesync_state.tree in
+  let treekem = treesync_to_treekem treesync_state.tree in
   // 10. In principle, the above process could be streamlined by having the
   // creator directly create a tree and choose a random value for first epoch's
   // epoch secret.
@@ -690,7 +690,7 @@ let process_welcome_message w (sign_pk, sign_sk) lookup =
   ) in
   let? leaf_index = find_my_index treesync sign_pk in
   let opt_path_secret_and_inviter_ind: option (bytes & nat) = match secrets.path_secret with | None -> None | Some {path_secret} -> Some (path_secret, group_info.tbs.signer) in
-  let? treekem = treesync_to_treekem treesync in
+  let treekem = treesync_to_treekem treesync in
   assume(leaf_index < pow2 l /\ Some? (leaf_at treekem leaf_index));
   assume(MLS.TreeKEM.Invariants.treekem_invariant treekem);
   let? interim_transcript_hash = MLS.TreeDEM.Message.Transcript.compute_interim_transcript_hash #bytes group_info.tbs.confirmation_tag group_info.tbs.group_context.confirmed_transcript_hash in

fstar/glue/code/MLS.TreeSyncTreeKEMBinder.fst

@@ -11,38 +11,37 @@ open MLS.Result
 
 #set-options "--fuel 1 --ifuel 1"
 
-val treesync_to_treekem_node_package:
+val treesync_to_treekem_node:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
   parent_node_nt bytes tkt ->
-  result (treekem_node bytes)
-let treesync_to_treekem_node_package #bytes #cb np =
-  return ({
-    public_key = np.content;
-    unmerged_leaves = List.Tot.map #(nat_lbytes 4) #nat (fun x -> x) np.unmerged_leaves;
-  })
+  treekem_node bytes
+let treesync_to_treekem_node #bytes #cb node =
+  {
+    public_key = node.content;
+    unmerged_leaves = List.Tot.map #(nat_lbytes 4) #nat (fun x -> x) node.unmerged_leaves;
+  }
 
 // This does not contain any internal TreeKEM data. To be used then joining a new group.
 val treesync_to_treekem:
   #bytes:Type0 -> {|crypto_bytes bytes|} ->
   #l:nat -> #i:tree_index l ->
   treesync bytes tkt l i ->
-  result (treekem bytes l i)
+  treekem bytes l i
 let rec treesync_to_treekem #bytes #cb #l #i t =
   match t with
   | TLeaf None ->
-    return (TLeaf None)
+    TLeaf None
   | TLeaf (Some lp) ->
-    return (TLeaf (Some ({public_key = lp.data.content} <: treekem_leaf bytes)))
-  | TNode onp left right -> begin
-    let? tk_left = treesync_to_treekem left in
-    let? tk_right = treesync_to_treekem right in
+    TLeaf (Some ({public_key = lp.data.content} <: treekem_leaf bytes))
+  | TNode onp left right -> (
+    let tk_left = treesync_to_treekem left in
+    let tk_right = treesync_to_treekem right in
     match onp with
     | None ->
-      return (TNode None tk_left tk_right)
+      TNode None tk_left tk_right
     | Some np ->
-      let? kp = treesync_to_treekem_node_package np in
-      return (TNode (Some kp) tk_left tk_right)
-  end
+      TNode (Some (treesync_to_treekem_node np)) tk_left tk_right
+  )
 
 //This function is used to authenticate data generated by TreeKEM. It allows TreeSync to handle parent hash + signature.
 val treekem_to_treesync:

fstar/test/MLS.Test.FromExt.TreeKEM.fst

@@ -179,7 +179,7 @@ let test_treekem_one t =
     let cb = mk_concrete_crypto_bytes cs in
     let ratchet_tree = extract_option "ratchet_tree" (((ps_prefix_to_ps_whole (ps_ratchet_tree_nt tkt))).parse (hex_string_to_bytes t.ratchet_tree)) in
     let (|l, tsync|) = extract_result (ratchet_tree_to_treesync ratchet_tree) in
-    let tkem = extract_result (treesync_to_treekem tsync) in
+    let tkem = treesync_to_treekem tsync in
     let tree_hash = extract_result (tree_hash tsync) in
     let group_context = gen_group_context (ciphersuite #bytes) (hex_string_to_bytes t.group_id) (UInt64.v t.epoch) tree_hash (hex_string_to_bytes t.confirmed_transcript_hash) in
     let states = List.map (get_leaf_treekem_tree_state tkem) t.leaves_private in