Add support for math integers

Cargo.toml

@@ -87,4 +87,5 @@ hax-diagnostics = { path = "frontend/diagnostics", version = "=0.1.0-pre.1" }
 hax-lint = { path = "frontend/lint", version = "=0.1.0-pre.1" }
 hax-phase-debug-webapp = { path = "engine/utils/phase-debug-webapp", version = "=0.1.0-pre.1" }
 hax-lib-macros-types = { path = "hax-lib-macros/types", version = "=0.1.0-pre.1" }
+hax-lib-macros = { path = "hax-lib-macros", version = "=0.1.0-pre.1" }
 hax-engine-names = { path = "engine/names", version = "=0.1.0-pre.1" }

engine/backends/fstar/fstar_backend.ml

@@ -253,6 +253,17 @@ struct
       (c Core__cmp__PartialOrd__gt, (2, ">."));
       (`Primitive (LogicalOp And), (2, "&&"));
       (`Primitive (LogicalOp Or), (2, "||"));
+      (c Rust_primitives__hax__int__add, (2, "+"));
+      (c Rust_primitives__hax__int__sub, (2, "-"));
+      (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__ge, (2, ">="));
+      (c Rust_primitives__hax__int__le, (2, "<="));
+      (c Rust_primitives__hax__int__gt, (2, ">"));
+      (c Rust_primitives__hax__int__lt, (2, "<"));
+      (c Rust_primitives__hax__int__ne, (2, "<>"));
+      (c Rust_primitives__hax__int__eq, (2, "="));
     ]
     |> Map.of_alist_exn (module Global_ident)
 
@@ -421,6 +432,24 @@ struct
           Error.assertion_failure e.span
             "pexpr: bad arity for operator application";
         F.term @@ F.AST.Op (F.Ident.id_of_text op, List.map ~f:pexpr args)
+    | App
+        {
+          f = { e = GlobalVar f; _ };
+          args = [ { e = Literal (String s); _ } ];
+          generic_args;
+        }
+      when Global_ident.eq_name Hax_lib__int__Impl_5___unsafe_from_str f ->
+        (match
+           String.chop_prefix ~prefix:"-" s
+           |> Option.value ~default:s
+           |> String.filter ~f:([%matches? '0' .. '9'] >> not)
+         with
+        | "" -> ()
+        | s ->
+            Error.assertion_failure e.span
+            @@ "pexpr: expected a integer, found the following non-digit \
+                chars: '" ^ s ^ "'");
+        F.AST.Const (F.Const.Const_int (s, None)) |> F.term
     | App { f; args; generic_args } ->
         let const_generics =
           List.filter_map
@@ -1475,6 +1504,7 @@ module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.RawOrMutPointer(Features.Rust)
   |> Phases.Transform_hax_lib_inline
+  |> Phases.Specialize
   |> Phases.Drop_sized_trait
   |> Phases.Simplify_question_marks
   |> Phases.And_mut_defsite

engine/lib/diagnostics.ml

@@ -35,6 +35,7 @@ module Phase = struct
     | ResugarForIndexLoops
     | ResugarQuestionMarks
     | SimplifyQuestionMarks
+    | Specialize
     | HoistSideEffects
     | LocalMutation
     | TrivializeAssignLhs

engine/lib/phases/phase_specialize.ml

@@ -0,0 +1,143 @@
+open! Prelude
+
+module Make (F : Features.T) =
+  Phase_utils.MakeMonomorphicPhase
+    (F)
+    (struct
+      let phase_id = Diagnostics.Phase.Specialize
+
+      module A = Ast.Make (F)
+      module FB = F
+      module B = Ast.Make (F)
+      module U = Ast_utils.Make (F)
+      module Visitors = Ast_visitors.Make (F)
+      open A
+
+      open struct
+        open Concrete_ident_generated
+
+        type pattern = {
+          fn : name;
+          fn_replace : name;
+          args : (expr -> bool) list;
+          ret : ty -> bool;
+        }
+        (** A pattern that helps matching against function applications *)
+
+        type ('a, 'b) predicate = 'a -> 'b option
+        (** Instead of working directly with boolean predicate, we
+        work with `_ -> _ option` so that we can chain them *)
+
+        (** Constructs a predicate out of predicates and names *)
+        let mk (args : ('a, 'b) predicate list) (ret : ('c, 'd) predicate)
+            (fn : name) (fn_replace : name) : pattern =
+          let args = List.map ~f:(fun p x -> p x |> Option.is_some) args in
+          let ret t = ret t |> Option.is_some in
+          { fn; fn_replace; args; ret }
+
+        open struct
+          let etyp (e : expr) : ty = e.typ
+          let tref = function TRef { typ; _ } -> Some typ | _ -> None
+
+          let tapp0 = function
+            | TApp { ident; args = [] } -> Some ident
+            | _ -> None
+
+          let ( >>& ) (f1 : ('a, 'b) predicate) (f2 : ('b, 'c) predicate) :
+              ('a, 'c) predicate =
+           fun x -> Option.bind (f1 x) ~f:f2
+
+          let eq : 'a 'b. eq:('a -> 'b -> bool) -> 'a -> ('b, 'b) predicate =
+           fun ~eq x x' -> if eq x x' then Some x' else None
+
+          let eq_global_ident :
+              name -> (Ast.Global_ident.t, Ast.Global_ident.t) predicate =
+            eq ~eq:Ast.Global_ident.eq_name
+
+          let erase : 'a. ('a, unit) predicate = fun _ -> Some ()
+
+          let is_int : (ty, unit) predicate =
+            tapp0 >>& eq_global_ident Hax_lib__int__Int >>& erase
+
+          let any _ = Some ()
+          let int_any = mk [ etyp >> is_int ] any
+          let int_int_any = mk [ etyp >> is_int; etyp >> is_int ] any
+          let any_int = mk [ any ] is_int
+          let rint_any = mk [ etyp >> (tref >>& is_int) ] any
+
+          let rint_rint_any =
+            mk [ etyp >> (tref >>& is_int); etyp >> (tref >>& is_int) ] any
+
+          let any_rint = mk [ any ] (tref >>& is_int)
+        end
+
+        (** The list of replacements *)
+        let patterns =
+          [
+            int_int_any Core__ops__arith__Add__add
+              Rust_primitives__hax__int__add;
+            int_int_any Core__ops__arith__Sub__sub
+              Rust_primitives__hax__int__sub;
+            int_int_any Core__ops__arith__Mul__mul
+              Rust_primitives__hax__int__mul;
+            int_int_any Core__ops__arith__Div__div
+              Rust_primitives__hax__int__div;
+            int_int_any Core__ops__arith__Rem__rem
+              Rust_primitives__hax__int__rem;
+            rint_rint_any Core__cmp__PartialOrd__gt
+              Rust_primitives__hax__int__gt;
+            rint_rint_any Core__cmp__PartialOrd__ge
+              Rust_primitives__hax__int__ge;
+            rint_rint_any Core__cmp__PartialOrd__lt
+              Rust_primitives__hax__int__lt;
+            rint_rint_any Core__cmp__PartialOrd__le
+              Rust_primitives__hax__int__le;
+            rint_rint_any Core__cmp__PartialEq__ne Rust_primitives__hax__int__ne;
+            rint_rint_any Core__cmp__PartialEq__eq Rust_primitives__hax__int__eq;
+            any_rint Hax_lib__int__Abstraction__lift
+              Rust_primitives__hax__int__from_machine;
+            int_any Hax_lib__int__Concretization__concretize
+              Rust_primitives__hax__int__into_machine;
+          ]
+      end
+
+      module Error = Phase_utils.MakeError (struct
+        let ctx = Diagnostics.Context.Phase phase_id
+      end)
+
+      module Attrs = Attr_payloads.Make (F) (Error)
+
+      let visitor =
+        object (self)
+          inherit [_] Visitors.map as super
+
+          method! visit_expr () e =
+            match e.e with
+            | App { f = { e = GlobalVar f; _ } as f'; args = l; _ } -> (
+                let l = List.map ~f:(self#visit_expr ()) l in
+                let matching =
+                  List.filter patterns ~f:(fun { fn; args; _ } ->
+                      Ast.Global_ident.eq_name fn f
+                      &&
+                      match List.for_all2 args l ~f:apply with
+                      | Ok r -> r
+                      | _ -> false)
+                in
+                match matching with
+                | [ { fn_replace; _ } ] ->
+                    let f = Ast.Global_ident.of_name Value fn_replace in
+                    let f = { f' with e = GlobalVar f } in
+                    {
+                      e with
+                      e = App { f; args = l; impl = None; generic_args = [] };
+                    }
+                | [] -> super#visit_expr () e
+                | _ ->
+                    Error.assertion_failure e.span
+                      "Found multiple matching patterns")
+            | _ -> super#visit_expr () e
+        end
+
+      let ditems (l : A.item list) : B.item list =
+        List.map ~f:(visitor#visit_item ()) l
+    end)

engine/lib/phases/phase_specialize.mli

@@ -0,0 +1,9 @@
+(** This phase specializes certain specific method applications
+(according to their name and the type it is being used on) into plain
+functions.
+
+This is useful espcially for math integers: the methods of the traits
+`Add`, `Sub`, `Mul` etc. are mapped to "primitive" functions in
+backends (e.g. Prims.whatever in FStar). *)
+
+module Make : Phase_utils.UNCONSTRAINTED_MONOMORPHIC_PHASE

engine/lib/utils.ml

@@ -21,6 +21,7 @@ let curry3 f x y z = f (x, y, z)
 let uncurry3 f (x, y, z) = f x y z
 let tup2 a b = (a, b)
 let swap (a, b) = (b, a)
+let apply f x = f x
 let ( let* ) x f = Option.bind ~f x
 let some_if_true = function true -> Some () | _ -> None
 

engine/names/src/lib.rs

@@ -34,6 +34,14 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
     let _ = ..;
     let _ = ..1;
 
+    {
+        use hax_lib::int::*;
+        let a: Int = 3u8.lift();
+        let _ = a.clone().pow2();
+        let _ = Int::_unsafe_from_str("1");
+        let _: u32 = a.concretize();
+    }
+
     fn question_mark_result<A, B: From<A>>(x: A) -> Result<(), B> {
         Err(x)?;
         Ok(())
@@ -148,6 +156,25 @@ mod hax {
     /// to signal that a item was extracted without body.
     fn dropped_body() {}
 
+    mod int {
+        fn add() {}
+        fn sub() {}
+        fn div() {}
+        fn mul() {}
+        fn rem() {}
+
+        fn le() {}
+        fn lt() {}
+        fn ge() {}
+        fn gt() {}
+
+        fn eq() {}
+        fn ne() {}
+
+        fn from_machine() {}
+        fn into_machine() {}
+    }
+
     mod control_flow_monad {
         trait ControlFlowMonad {
             fn lift() {}

hax-lib-macros/src/lib.rs

@@ -541,6 +541,35 @@ 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.
+#[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| !matches!(ch, '0'..='9')) {
+        abort_call_site!(format!("Expected a digit, found {faulty}"));
+    }
+    if negative {
+        lit = format!("-{lit}");
+    }
+    quote! {
+        ::hax_lib::int::Int::_unsafe_from_str(#lit)
+    }
+    .into()
+}
+
 macro_rules! make_quoting_item_proc_macro {
     ($backend:ident, $macro_name:ident, $position:expr, $cfg_name:ident) => {
         #[doc = concat!("This macro inlines verbatim ", stringify!($backend)," code before a Rust item.")]
@@ -595,6 +624,7 @@ macro_rules! make_quoting_item_proc_macro {
         }
     };
 }
+
 macro_rules! make_quoting_proc_macro {
     ($backend:ident($expr_name:ident, $before_name:ident, $after_name:ident, $replace_name:ident, $cfg_name:ident)) => {
         #[doc = concat!("Embed ", stringify!($backend), " expression inside a Rust expression. This macro takes only one argument: some raw ", stringify!($backend), " code as a string literal.")]

hax-lib/Cargo.toml

@@ -12,7 +12,9 @@ description = "Hax-specific helpers for Rust programs"
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-hax-lib-macros = { path = "../hax-lib-macros", optional = true }
+hax-lib-macros = { workspace = true, optional = true }
+num-bigint = { version = "0.4.3", default-features = false }
+num-traits = { version = "0.2.15", default-features = false }
 
 [features]
 default = ["macros"]

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

@@ -0,0 +1,20 @@
+module Hax_lib.Int
+
+open Core
+
+unfold type t_Int = int
+unfold type impl__Int__to_u16
+
+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