Merge pull request #3751 from mtzguido/int_fits

IntN: add a `fits` for every module
FStarLang · Feb 14, 2025 · 3fe597b · 3fe597b
2 parents f46939e + bbd64d5
commit 3fe597b
Show file tree

Hide file tree

Showing 11 changed files with 22 additions and 0 deletions.
diff --git a/.scripts/FStar.IntN.fstip b/.scripts/FStar.IntN.fstip
@@ -10,6 +10,8 @@ new val t : eqtype
 
 val v (x:t) : Tot (int_t n)
 
+let fits (x:int) : prop = Int.fits x n
+
 val int_to_t: x:int_t n -> Pure t
   (requires True)
   (ensures (fun y -> v y = x))

diff --git a/.scripts/FStar.UIntN.fstip b/.scripts/FStar.UIntN.fstip
@@ -32,6 +32,8 @@ new val t : eqtype
     machine integer *)
 val v (x:t) : Tot (uint_t n)
 
+let fits (x:int) : prop = UInt.fits x n
+
 (** A coercion that injects a bounded mathematical integers into a
     machine integer *)
 val uint_to_t (x:uint_t n) : Pure t

diff --git a/ulib/FStar.Int128.fsti b/ulib/FStar.Int128.fsti
@@ -31,6 +31,8 @@ new val t : eqtype
 
 val v (x:t) : Tot (int_t n)
 
+let fits (x:int) : prop = Int.fits x n
+
 val int_to_t: x:int_t n -> Pure t
   (requires True)
   (ensures (fun y -> v y = x))

diff --git a/ulib/FStar.Int16.fsti b/ulib/FStar.Int16.fsti
@@ -31,6 +31,8 @@ new val t : eqtype
 
 val v (x:t) : Tot (int_t n)
 
+let fits (x:int) : prop = Int.fits x n
+
 val int_to_t: x:int_t n -> Pure t
   (requires True)
   (ensures (fun y -> v y = x))

diff --git a/ulib/FStar.Int32.fsti b/ulib/FStar.Int32.fsti
@@ -31,6 +31,8 @@ new val t : eqtype
 
 val v (x:t) : Tot (int_t n)
 
+let fits (x:int) : prop = Int.fits x n
+
 val int_to_t: x:int_t n -> Pure t
   (requires True)
   (ensures (fun y -> v y = x))

diff --git a/ulib/FStar.Int64.fsti b/ulib/FStar.Int64.fsti
@@ -31,6 +31,8 @@ new val t : eqtype
 
 val v (x:t) : Tot (int_t n)
 
+let fits (x:int) : prop = Int.fits x n
+
 val int_to_t: x:int_t n -> Pure t
   (requires True)
   (ensures (fun y -> v y = x))

diff --git a/ulib/FStar.Int8.fsti b/ulib/FStar.Int8.fsti
@@ -31,6 +31,8 @@ new val t : eqtype
 
 val v (x:t) : Tot (int_t n)
 
+let fits (x:int) : prop = Int.fits x n
+
 val int_to_t: x:int_t n -> Pure t
   (requires True)
   (ensures (fun y -> v y = x))

diff --git a/ulib/FStar.UInt16.fsti b/ulib/FStar.UInt16.fsti
@@ -53,6 +53,8 @@ new val t : eqtype
     machine integer *)
 val v (x:t) : Tot (uint_t n)
 
+let fits (x:int) : prop = UInt.fits x n
+
 (** A coercion that injects a bounded mathematical integers into a
     machine integer *)
 val uint_to_t (x:uint_t n) : Pure t

diff --git a/ulib/FStar.UInt32.fsti b/ulib/FStar.UInt32.fsti
@@ -53,6 +53,8 @@ new val t : eqtype
     machine integer *)
 val v (x:t) : Tot (uint_t n)
 
+let fits (x:int) : prop = UInt.fits x n
+
 (** A coercion that injects a bounded mathematical integers into a
     machine integer *)
 val uint_to_t (x:uint_t n) : Pure t

diff --git a/ulib/FStar.UInt64.fsti b/ulib/FStar.UInt64.fsti
@@ -53,6 +53,8 @@ new val t : eqtype
     machine integer *)
 val v (x:t) : Tot (uint_t n)
 
+let fits (x:int) : prop = UInt.fits x n
+
 (** A coercion that injects a bounded mathematical integers into a
     machine integer *)
 val uint_to_t (x:uint_t n) : Pure t

diff --git a/ulib/FStar.UInt8.fsti b/ulib/FStar.UInt8.fsti
@@ -53,6 +53,8 @@ new val t : eqtype
     machine integer *)
 val v (x:t) : Tot (uint_t n)
 
+let fits (x:int) : prop = UInt.fits x n
+
 (** A coercion that injects a bounded mathematical integers into a
     machine integer *)
 val uint_to_t (x:uint_t n) : Pure t