expose MLSMessage parsing function

Inria-Prosecco · Jul 3, 2024 · 7ea1b74 · 7ea1b74
1 parent c397e24
commit 7ea1b74
Show file tree

Hide file tree

Showing 5 changed files with 443 additions and 0 deletions.
diff --git a/fstar/api/MLS.API.fst b/fstar/api/MLS.API.fst
@@ -285,3 +285,6 @@ let create_remove_proposal #bytes #cb st removed_cred =
     else return ()
   ) in
   return (MLS.TreeDEM.NetworkTypes.P_remove { removed })
+
+let parse_message #bytes #cb msg_bytes =
+  from_option "parse_message: malformed message" (parse _ msg_bytes)
diff --git a/fstar/api/MLS.API.fsti b/fstar/api/MLS.API.fsti
@@ -299,3 +299,10 @@ val create_remove_proposal:
   mls_group bytes ->
   removed:credential bytes ->
   result (proposal bytes)
+
+(*** Helper function ***)
+
+val parse_message:
+  #bytes:Type0 -> {|crypto_bytes bytes|} ->
+  bytes ->
+  result (MLS.TreeDEM.NetworkTypes.mls_message_nt bytes)