Merge pull request #3507 from FStarLang/_taramana_sizet_uint64

Add a cast from size_t to uint64_t
FStarLang · Sep 30, 2024 · 061fcdf · 061fcdf
2 parents c20b10a + 64560b4
commit 061fcdf
Show file tree

Hide file tree

Showing 5 changed files with 24 additions and 1 deletion.
diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml
diff --git a/ocaml/fstar-lib/generated/FStar_SizeT.ml b/ocaml/fstar-lib/generated/FStar_SizeT.ml
diff --git a/src/extraction/FStar.Extraction.Krml.fst b/src/extraction/FStar.Extraction.Krml.fst
@@ -1164,6 +1164,10 @@ and translate_expr' env e: expr =
     when string_of_mlpath p = "FStar.SizeT.sizet_to_uint32" ->
       ECast (translate_expr env arg, TInt UInt32)
 
+  | MLE_App ({ expr = MLE_Name p }, [ arg ])
+    when string_of_mlpath p = "FStar.SizeT.sizet_to_uint64" ->
+      ECast (translate_expr env arg, TInt UInt64)
+
   | MLE_App (head, args) ->
       EApp (translate_expr env head, List.map (translate_expr env) args)
 

diff --git a/ulib/FStar.SizeT.fst b/ulib/FStar.SizeT.fst
@@ -63,6 +63,7 @@ let uint16_to_sizet x = uint_to_t (U16.v x)
 let uint32_to_sizet x = uint_to_t (U32.v x)
 let uint64_to_sizet x = uint_to_t (U64.v x)
 let sizet_to_uint32 x = FStar.Int.Cast.uint64_to_uint32 (Sz?.x x)
+let sizet_to_uint64 x = (Sz?.x x)
 
 let fits_lte x y = ()
 

diff --git a/ulib/FStar.SizeT.fsti b/ulib/FStar.SizeT.fsti
@@ -97,6 +97,10 @@ val sizet_to_uint32 (x:t) : Pure U32.t
   (requires True)
   (ensures fun y -> U32.v y == v x % pow2 32)
 
+val sizet_to_uint64 (x:t) : Pure U64.t
+  (requires True)
+  (ensures fun y -> U64.v y == v x % pow2 64)
+
 val fits_lte (x y: nat) : Lemma
   (requires (x <= y /\ fits y))
   (ensures (fits x))