Fix dependencies bounded integers

cli/default.nix

@@ -58,7 +58,7 @@
   );
   frontend-docs = craneLib.cargoDoc (commonArgs // {
     preBuildPhases = ["addRustcDocs"];
-    cargoDocExtraArgs = "--document-private-items";
+    cargoDocExtraArgs = "--document-private-items -p hax-bounded-integers";
     addRustcDocs = ''
       mkdir -p target/doc
       cp --no-preserve=mode -rf ${rustc.passthru.availableComponents.rustc-docs}/share/doc/rust/html/rustc/* target/doc/

engine/backends/fstar/fstar_backend.ml

@@ -282,6 +282,7 @@ struct
       (c Rust_primitives__hax__int__mul, (2, "*"));
       (c Rust_primitives__hax__int__div, (2, "/"));
       (c Rust_primitives__hax__int__rem, (2, "%"));
+      (c Rust_primitives__hax__int__neg, (1, "-"));
       (c Rust_primitives__hax__int__ge, (2, ">="));
       (c Rust_primitives__hax__int__le, (2, "<="));
       (c Rust_primitives__hax__int__gt, (2, ">"));
@@ -506,7 +507,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

engine/lib/phases/phase_specialize.ml

@@ -84,6 +84,7 @@ module Make (F : Features.T) =
               Rust_primitives__hax__int__div;
             int_int_any Core__ops__arith__Rem__rem
               Rust_primitives__hax__int__rem;
+            int_any Core__ops__arith__Neg__neg Rust_primitives__hax__int__neg;
             rint_rint_any Core__cmp__PartialOrd__gt
               Rust_primitives__hax__int__gt;
             rint_rint_any Core__cmp__PartialOrd__ge

engine/names/src/lib.rs

@@ -127,6 +127,7 @@ macro_rules! impl_arith {
             fn mul() {}
             fn div() {}
             fn rem() {}
+            fn neg() {}
             fn bit_xor() {}
             fn bit_and() {}
             fn bit_or() {}
@@ -206,6 +207,7 @@ mod hax {
         fn div() {}
         fn mul() {}
         fn rem() {}
+        fn neg() {}
 
         fn le() {}
         fn lt() {}

hax-bounded-integers/src/lib.rs

@@ -1,6 +1,11 @@
 use hax_lib::Refinement;
 pub mod num_traits;
 
+pub mod _macro_utils {
+    pub use duplicate;
+    pub use paste;
+}
+
 #[doc(hidden)]
 #[macro_export]
 macro_rules! derivate_binop_for_bounded {
@@ -21,7 +26,7 @@ macro_rules! derivate_binop_for_bounded {
     (@$t:ident, $bounded_t:ident, $trait:ident, $meth:ident, $get:ident, $out:ty,
      <$(const $cst_name:ident : $cst_ty:ty),*>
     ) => {
-        paste::paste!{
+        $crate::_macro_utils::paste::paste!{
             // BoundedT<A, B> <OP> BoundedT<C, D>
             impl<$(const [< $cst_name _LHS >]: $cst_ty,)* $(const [< $cst_name _RHS >]: $cst_ty,)*>
                 $trait<$bounded_t<$([< $cst_name _RHS >],)*>> for $bounded_t<$([< $cst_name _LHS >],)*>
@@ -75,7 +80,7 @@ macro_rules! derivate_assign_binop_for_bounded {
     (@$t:ident, $bounded_t:ident, $trait:ident, $meth:ident, $get:ident, $out:ty,
      <$(const $cst_name:ident : $cst_ty:ty),*>
     ) => {
-        paste::paste!{
+        $crate::_macro_utils::paste::paste!{
             // BoundedT<A, B> <OP> BoundedT<C, D>
             impl<$(const [< $cst_name _LHS >]: $cst_ty,)* $(const [< $cst_name _RHS >]: $cst_ty,)*>
                 $trait<$bounded_t<$([< $cst_name _RHS >],)*>> for $bounded_t<$([< $cst_name _LHS >],)*>
@@ -115,7 +120,7 @@ macro_rules! derivate_operations_for_bounded {
     ($bounded_t:ident($t: ident $($bytes:expr)?)$(,)?
      <$(const $cst_name:ident : $cst_ty:ty),*>
     ) => {
-          #[duplicate::duplicate_item(
+          #[$crate::_macro_utils::duplicate::duplicate_item(
               INTRO_CONSTANTS USE_CONSTANTS;
               [ $(const $cst_name:$cst_ty),* ] [ $($cst_name),* ];
           )]

hax-lib/src/int/mod.rs

@@ -30,6 +30,14 @@ impl Add for Int {
     }
 }
 
+impl Neg for Int {
+    type Output = Self;
+
+    fn neg(self) -> Self::Output {
+        Self::new(-self.get())
+    }
+}
+
 impl Sub for Int {
     type Output = Self;
 

tests/attributes/Cargo.toml

@@ -5,6 +5,7 @@ edition = "2021"
 
 [dependencies]
 hax-lib = { path = "../../hax-lib" }
+hax-bounded-integers = { path = "../../hax-bounded-integers" }
 serde = { version = "1.0", features = ["derive"] }
 
 [package.metadata.hax-tests]

tests/attributes/src/lib.rs

@@ -290,6 +290,17 @@ mod refinement_types {
     /// Example of a specific constraint on a value
     #[hax_lib::refinement_type(|x| x == 4 || x == 5 || x == 10 || x == 11)]
     pub struct CompressionFactor(u8);
+
+    use hax_lib::int::*;
+    /// Example of a refined int, that derives all common arithmetic operations
+    hax_bounded_integers::refinement_int!(
+        BoundedAbsI16<const B: usize>(i16, 2, |x| B.lift() < int!(32768) && x.lift() >= -B.lift() && x.lift() <= B.lift())
+    );
+
+    #[hax_lib::requires(M.lift() < int!(32768) && M.lift() == N.lift() * int!(2))]
+    fn double_abs_i16<const N: usize, const M: usize>(x: BoundedAbsI16<N>) -> BoundedAbsI16<M> {
+        (x * 2).into_checked()
+    }
 }
 mod nested_refinement_elim {
     use hax_lib::*;