Skip to content

Commit

Permalink
cleanup: remove lambda in TreeSyncTreeKEMBinder
Browse files Browse the repository at this point in the history
  • Loading branch information
TWal committed Nov 27, 2024
1 parent 4beb781 commit aa1c4a3
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion fstar/glue/code/MLS.TreeSyncTreeKEMBinder.fst
Original file line number Diff line number Diff line change
Expand Up @@ -11,14 +11,17 @@ open MLS.Result

#set-options "--fuel 1 --ifuel 1"

val nat_lbytes_to_nat: #sz:nat -> nat_lbytes sz -> nat
let nat_lbytes_to_nat #sz x = x

val treesync_to_treekem_node:
#bytes:Type0 -> {|crypto_bytes bytes|} ->
parent_node_nt bytes tkt ->
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;
unmerged_leaves = List.Tot.map nat_lbytes_to_nat node.unmerged_leaves;
}

// This does not contain any internal TreeKEM data. To be used then joining a new group.
Expand Down

0 comments on commit aa1c4a3

Please sign in to comment.