hax-lib: Int improvements and fixes

engine/backends/fstar/fstar_backend.ml

@@ -589,7 +589,7 @@ struct
           args = [ { e = Literal (String s); _ } ];
           generic_args = _;
         }
-      when Global_ident.eq_name Hax_lib__int__Impl_5___unsafe_from_str f ->
+      when Global_ident.eq_name Hax_lib__int__Impl_6___unsafe_from_str f ->
         (match
            String.chop_prefix ~prefix:"-" s
            |> Option.value ~default:s

hax-lib/Cargo.toml

@@ -11,8 +11,8 @@ description = "Hax-specific helpers for Rust programs"
 
 
 [target.'cfg(hax)'.dependencies]
-num-bigint = { version = "0.4.3", default-features = false }
-num-traits = { version = "0.2.15", default-features = false }
+num-bigint = { version = "0.4", default-features = false }
+num-traits = { version = "0.2", default-features = false }
 
 [dependencies]
 hax-lib-macros = { workspace = true, optional = true }

hax-lib/proofs/fstar/extraction/Hax_lib.Int.fst

@@ -4,16 +4,19 @@ open Core
 
 unfold type t_Int = int
 
-unfold let impl__Int__to_u8 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
-unfold let impl__Int__to_u16 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
-unfold let impl__Int__to_u32 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
-unfold let impl__Int__to_u64 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
-unfold let impl__Int__to_u128 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
-unfold let impl__Int__to_usize (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_u8 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_u16 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_u32 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_u64 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_u128 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_usize (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
 
-unfold let impl__Int__to_i8 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
-unfold let impl__Int__to_i16 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
-unfold let impl__Int__to_i32 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
-unfold let impl__Int__to_i64 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
-unfold let impl__Int__to_i128 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
-unfold let impl__Int__to_isize (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_i8 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_i16 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_i32 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_i64 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_i128 (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+unfold let impl_Int__to_isize (#t:inttype) (n:range_t t) : int_t t = mk_int #t n
+
+unfold let impl_Int__pow2 (n: nat) = pow2 n
+unfold let impl_Int__rem_euclid = (%)

hax-lib/src/dummy.rs

@@ -119,6 +119,9 @@ pub mod int {
         pub fn _unsafe_from_str(_s: &str) -> Self {
             Int(0)
         }
+        pub fn rem_euclid(&self, v: Self) -> Self {
+            Self::new(self.0.rem_euclid(v.0))
+        }
     }
 
     pub trait ToInt {

hax-lib/src/int/bigint.rs

@@ -5,7 +5,7 @@
 
 /// Maximal number of bytes stored in our copiable `BigInt`s.
 const BYTES: usize = 1024;
-#[derive(Copy, Clone)]
+#[derive(Debug, Copy, Clone)]
 pub(super) struct BigInt {
     sign: num_bigint::Sign,
     data: [u8; BYTES],
@@ -15,10 +15,12 @@ impl BigInt {
     /// operation panics when the provided [`num_bigint::BigInt`]
     /// has more than [`BYTES`] bytes.
     pub(super) fn new(i: &num_bigint::BigInt) -> Self {
-        let (sign, data) = i.to_bytes_be();
-        let data = data
-            .try_into()
-            .expect("`copiable_bigint::BigInt::new`: too big, please consider increasing `BYTES`");
+        let (sign, bytes) = i.to_bytes_be();
+        if bytes.len() > BYTES {
+            panic!("`copiable_bigint::BigInt::new`: too big, please consider increasing `BYTES`");
+        }
+        let mut data = [0; BYTES];
+        data[BYTES - bytes.len()..].copy_from_slice(&bytes[..]);
         BigInt { sign, data }
     }
 

hax-lib/src/int/mod.rs

@@ -1,3 +1,4 @@
+use core::fmt;
 use core::ops::*;
 use num_traits::cast::ToPrimitive;
 
@@ -12,9 +13,15 @@ pub use hax_lib_macros::int;
 /// Mathematical integers for writting specifications. Mathematical
 /// integers are unbounded and arithmetic operation on them never over
 /// or underflow.
-#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd)]
+#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Debug)]
 pub struct Int(BigInt);
 
+impl fmt::Display for Int {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        write!(f, "{}", self.get())
+    }
+}
+
 impl Int {
     fn new(x: impl Into<num_bigint::BigInt>) -> Self {
         Int(BigInt::new(&x.into()))
@@ -70,6 +77,11 @@ impl Int {
         use core::str::FromStr;
         Self::new(num_bigint::BigInt::from_str(s).unwrap())
     }
+
+    pub fn rem_euclid(&self, v: Self) -> Self {
+        use num_traits::Euclid;
+        Self::new(self.get().rem_euclid(&v.get()))
+    }
 }
 
 #[cfg(feature = "macros")]

proof-libs/fstar/core/Core.Num.fsti

@@ -34,6 +34,11 @@ val impl_u64__from_be_bytes: t_Array u8 (sz 8) -> u64
 val impl_u64__to_le_bytes: u64 -> t_Array u8 (sz 8)
 val impl_u64__to_be_bytes: u64 -> t_Array u8 (sz 8)
 val impl_u64__rotate_right: u64 -> u64 -> u64
+let impl_u64__overflowing_sub (x y: u64): u64 * bool
+  = let sub = v x - v y in
+    let borrow = sub < 0 in
+    let out = if borrow then pow2 64 + sub else sub in
+    (mk_u64 out, borrow)
 
 let impl_u128__wrapping_add: u128 -> u128 -> u128 = add_mod
 let impl_u128__wrapping_sub: u128 -> u128 -> u128 = sub_mod