Merge pull request #1533 from cryspen/fix-1532

feat(hax-lib): `int!`: support hex, octal and binary literals

Author: franziskuskiefer

hax-lib/macros/src/implementation.rs

@@ -803,33 +803,24 @@ pub fn pv_handwritten(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::Toke
     quote! {#attr #item}.into()
 }
 
-/// Create a mathematical integer. This macro expects a integer
-/// literal that consists in an optional minus sign followed by one or
-/// more digits.
+/// Create a mathematical integer. This macro expects a Rust integer
+/// literal without suffix.
+///
+/// ## Examples:
+/// - `int!(0x101010)`
+/// - `int!(42)`
+/// - `int!(0o52)`
+/// - `int!(0h2A)`
 #[proc_macro_error]
 #[proc_macro]
 pub fn int(payload: pm::TokenStream) -> pm::TokenStream {
-    let mut tokens = payload.into_iter().peekable();
-    let negative = matches!(tokens.peek(), Some(pm::TokenTree::Punct(p)) if p.as_char() == '-');
-    if negative {
-        tokens.next();
-    }
-    let [pm::TokenTree::Literal(lit)] = &tokens.collect::<Vec<_>>()[..] else {
-        abort_call_site!("Expected exactly one numeric literal");
-    };
-    let lit = format!("{lit}");
-    // Allow negative numbers
-    let mut lit = lit.strip_prefix("-").unwrap_or(lit.as_str()).to_string();
-    if let Some(faulty) = lit.chars().find(|ch| !ch.is_ascii_digit()) {
-        abort_call_site!(format!("Expected a digit, found {faulty}"));
-    }
-    if negative {
-        lit = format!("-{lit}");
+    let n: LitInt = parse_macro_input!(payload);
+    let suffix = n.suffix();
+    if !suffix.is_empty() {
+        abort_call_site!("The literal suffix `{suffix}` was unexpected.")
     }
-    quote! {
-        ::hax_lib::int::Int::_unsafe_from_str(#lit)
-    }
-    .into()
+    let digits = n.base10_digits();
+    quote! {::hax_lib::int::Int::_unsafe_from_str(#digits)}.into()
 }
 
 macro_rules! make_quoting_item_proc_macro {

test-harness/src/snapshots/toolchain__literals into-coq.snap

@@ -50,6 +50,14 @@ Export hax_lib.
 
 Definition math_integers (x : t_Int) `{andb (f_gt (x) (impl_Int__e_unsafe_from_str (("0"%string : string)))) (f_lt (x) (impl_Int__e_unsafe_from_str (("16"%string : string)))) = true} : t_u8 :=
   let _ : t_Int := f_lift ((3 : t_usize)) in
+  let e_neg_dec := impl_Int__e_unsafe_from_str (("-340282366920938463463374607431768211455000"%string : string)) in
+  let e_pos_dec := impl_Int__e_unsafe_from_str (("340282366920938463463374607431768211455000"%string : string)) in
+  let e_neg_hex := impl_Int__e_unsafe_from_str (("-340282366920938463463374607431768211455000"%string : string)) in
+  let e_pos_hex := impl_Int__e_unsafe_from_str (("340282366920938463463374607431768211455000"%string : string)) in
+  let e_neg_octal := impl_Int__e_unsafe_from_str (("-340282366920938463463374607431768211455000"%string : string)) in
+  let e_pos_octal := impl_Int__e_unsafe_from_str (("340282366920938463463374607431768211455000"%string : string)) in
+  let e_neg_bin := impl_Int__e_unsafe_from_str (("-340282366920938463463374607431768211455000"%string : string)) in
+  let e_pos_bin := impl_Int__e_unsafe_from_str (("340282366920938463463374607431768211455000"%string : string)) in
   let _ := f_gt (impl_Int__e_unsafe_from_str (("-340282366920938463463374607431768211455000"%string : string))) (impl_Int__e_unsafe_from_str (("340282366920938463463374607431768211455000"%string : string))) in
   let _ := f_lt (x) (x) in
   let _ := f_ge (x) (x) in

test-harness/src/snapshots/toolchain__literals into-fstar.snap

@@ -38,6 +38,14 @@ let math_integers (x: Hax_lib.Int.t_Int)
       (requires x > (0 <: Hax_lib.Int.t_Int) && x < (16 <: Hax_lib.Int.t_Int))
       (fun _ -> Prims.l_True) =
   let _:Hax_lib.Int.t_Int = Rust_primitives.Hax.Int.from_machine (mk_usize 3) in
+  let e_neg_dec:Hax_lib.Int.t_Int = (-340282366920938463463374607431768211455000) in
+  let e_pos_dec:Hax_lib.Int.t_Int = 340282366920938463463374607431768211455000 in
+  let e_neg_hex:Hax_lib.Int.t_Int = (-340282366920938463463374607431768211455000) in
+  let e_pos_hex:Hax_lib.Int.t_Int = 340282366920938463463374607431768211455000 in
+  let e_neg_octal:Hax_lib.Int.t_Int = (-340282366920938463463374607431768211455000) in
+  let e_pos_octal:Hax_lib.Int.t_Int = 340282366920938463463374607431768211455000 in
+  let e_neg_bin:Hax_lib.Int.t_Int = (-340282366920938463463374607431768211455000) in
+  let e_pos_bin:Hax_lib.Int.t_Int = 340282366920938463463374607431768211455000 in
   let _:bool =
     ((-340282366920938463463374607431768211455000) <: Hax_lib.Int.t_Int) >
     (340282366920938463463374607431768211455000 <: Hax_lib.Int.t_Int)

tests/literals/src/lib.rs

@@ -4,6 +4,14 @@ use hax_lib::*;
 #[hax_lib::requires(x > int!(0) && x < int!(16))]
 fn math_integers(x: Int) -> u8 {
     let _: Int = 3usize.lift();
+    let _neg_dec = int!(-340282366920938463463374607431768211455000);
+    let _pos_dec = int!(340282366920938463463374607431768211455000);
+    let _neg_hex = int!(-0x3E7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFC18);
+    let _pos_hex = int!(0x3E7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFC18);
+    let _neg_octal = int!(-0o7637777777777777777777777777777777777777776030);
+    let _pos_octal = int!(0o7637777777777777777777777777777777777777776030);
+    let _neg_bin = int!(-0b111110011111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111110000011000);
+    let _pos_bin = int!(0b111110011111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111110000011000);
     let _ = int!(-340282366920938463463374607431768211455000)
         > int!(340282366920938463463374607431768211455000);
     let _ = x < x;