use UInt64 for epoch

Inria-Prosecco · Jun 28, 2024 · 0a0faab · 0a0faab
1 parent 852cc22
commit 0a0faab
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/fstar/api/MLS.API.High.fst b/fstar/api/MLS.API.High.fst
@@ -304,7 +304,7 @@ type processed_message_content (bytes:Type0) {|bytes_like bytes|} =
 noeq
 type processed_message (bytes:Type0) {|bytes_like bytes|} = {
   group_id: bytes;
-  epoch: nat_lbytes 8;
+  epoch: FStar.UInt64.t;
   sender: unit; //TODO
   authenticated_data: bytes;
   content: processed_message_content bytes;
@@ -844,7 +844,7 @@ let process_message #bytes #cb #asp st msg =
 
   return ({
     group_id = auth_msg.content.group_id;
-    epoch = auth_msg.content.epoch;
+    epoch = FStar.UInt64.uint_to_t auth_msg.content.epoch;
     sender = ();
     authenticated_data = auth_msg.content.authenticated_data;
     content;

diff --git a/fstar/api/MLS.API.fsti b/fstar/api/MLS.API.fsti
@@ -60,7 +60,7 @@ type processed_message_content (bytes:Type0) {|crypto_bytes bytes|} =
 noeq
 type processed_message (bytes:Type0) {|crypto_bytes bytes|} = {
   group_id: bytes;
-  epoch: nat_lbytes 8;
+  epoch: FStar.UInt64.t;
   sender: unit; //TODO
   authenticated_data: bytes;
   content: processed_message_content bytes;