Added function implementations for integers in Core.Num

Author: satiscugcat

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

@@ -38,6 +38,29 @@ let impl_i64__BITS: u32 = mk_int 64
 let impl_i128__BITS: u32 = mk_int 128
 
 
+
+let impl_u8__wrapping_add: u8 -> u8 -> u8 = add_mod
+let impl_u16__wrapping_add: u16 -> u16 ->  u16 = add_mod
+let impl_u32__wrapping_add: u32 -> u32 -> u32 = add_mod
+let impl_u64__wrapping_add: u64 -> u64 -> u64 = add_mod
+let impl_u128__wrapping_add: u128 -> u128 -> u128 = add_mod
+let impl_i8__wrapping_add: i8 -> i8 -> i8 = add_mod
+let impl_i16__wrapping_add: i16 -> i16 ->  i16 = add_mod
+let impl_i32__wrapping_add: i32 -> i32 -> i32 = add_mod
+let impl_i64__wrapping_add: i64 -> i64 -> i64 = add_mod
+let impl_i128__wrapping_add: i128 -> i128 -> i128 = add_mod
+
+let impl_u8__wrapping_sub: u8 -> u8 -> u8 = sub_mod
+let impl_u16__wrapping_sub: u16 -> u16 ->  u16 = sub_mod
+let impl_u32__wrapping_sub: u32 -> u32 -> u32 = sub_mod
+let impl_u64__wrapping_sub: u64 -> u64 -> u64 = sub_mod
+let impl_u128__wrapping_sub: u128 -> u128 -> u128 = sub_mod
+let impl_i8__wrapping_sub: i8 -> i8 -> i8 = sub_mod
+let impl_i16__wrapping_sub: i16 -> i16 ->  i16 = sub_mod
+let impl_i32__wrapping_sub: i32 -> i32 -> i32 = sub_mod
+let impl_i64__wrapping_sub: i64 -> i64 -> i64 = sub_mod
+let impl_i128__wrapping_sub: i128 -> i128 -> i128 = sub_mod
+
 let impl_u8__rem_euclid (x: u8) (y: u8 {v y <> 0}): u8 = x %! y
 let impl_u16__rem_euclid (x: u16) (y: u16 {v y <> 0}): u16 = x %! y
 let impl_u32__rem_euclid (x: u32) (y: u32 {v y <> 0}): u32 = x %! y
@@ -51,23 +74,31 @@ let impl_i64__rem_euclid (x: i64) (y: i64 {v y <> 0}): i64 = x %! y
 let impl_i128__rem_euclid (x: i128) (y: i128 {v y <> 0}): i128 = x %! y
 let impl_isize__rem_euclid (x: isize) (y: isize {v y <> 0}): isize = x %! y
 
-let impl_u8__wrapping_add: u8 -> u8 -> u8 = add_mod
-let impl_u8__wrapping_sub: u8 -> u8 -> u8 = sub_mod
-let impl_u16__wrapping_add: u16 -> u16 ->  u16 = add_mod
+
+
+let impl_u8__overflowing_mul: u8 -> u8 -> u8 * bool = mul_overflow
+let impl_u16__overflowing_mul: u16 -> u16 ->  u16 * bool = mul_overflow
+let impl_u32__overflowing_mul: u32 -> u32 -> u32 * bool = mul_overflow
+let impl_u64__overflowing_mul: u64 -> u64 -> u64 * bool = mul_overflow
+let impl_u128__overflowing_mul: u128 -> u128 -> u128 * bool = mul_overflow
+let impl_i8__overflowing_mul: i8 -> i8 -> i8 * bool = mul_overflow
+let impl_i16__overflowing_mul: i16 -> i16 ->  i16 * bool = mul_overflow
+let impl_i32__overflowing_mul: i32 -> i32 -> i32 * bool = mul_overflow
+let impl_i64__overflowing_mul: i64 -> i64 -> i64 * bool = mul_overflow
+let impl_i128__overflowing_mul: i128 -> i128 -> i128 * bool = mul_overflow
+
 val impl_u16__to_be_bytes: u16 -> t_Array u8 (sz 2)
 val impl_u16__from_be_bytes: t_Array u8 (sz 2) -> u16
 
-let impl_i32__wrapping_add: i32 -> i32 -> i32 = add_mod
-let impl_i32__wrapping_sub: i32 -> i32 -> i32 = sub_mod
+
+
 let impl_i32__abs (a:i32{minint i32_inttype < v a}) : i32 = abs_int a
-val impl_i32__overflowing_mul: i32 -> i32 -> i32 * bool
 
-let impl_i16__wrapping_add: i16 -> i16 -> i16 = add_mod
-let impl_i16__wrapping_sub: i16 -> i16 -> i16 = sub_mod
+
+
 let impl_i16__wrapping_mul: i16 -> i16 -> i16 = mul_mod
-val impl_i16__overflowing_mul: i16 -> i16 -> i16 * bool
 
-let impl_u32__wrapping_add: u32 -> u32 -> u32 = add_mod
+
 val impl_u32__rotate_left: u32 -> u32 -> u32
 val impl_u32__from_le_bytes: t_Array u8 (sz 4) -> u32
 val impl_u32__from_be_bytes: t_Array u8 (sz 4) -> u32
@@ -76,7 +107,6 @@ val impl_u32__to_be_bytes: u32 -> t_Array u8 (sz 4)
 val impl_u32__rotate_right: u32 -> u32 -> u32
 
 
-let impl_u64__wrapping_add: u64 -> u64 -> u64 = add_mod
 val impl_u64__rotate_left: u32 -> u32 -> u32
 val impl_u64__from_le_bytes: t_Array u8 (sz 8) -> u64
 val impl_u64__from_be_bytes: t_Array u8 (sz 8) -> u64
@@ -89,12 +119,8 @@ let impl_u64__overflowing_sub (x y: u64): u64 * bool
     let out = if borrow then pow2 64 + sub else sub in
     (mk_u64 out, borrow)
 
-let impl_i64__wrapping_add: i64 -> i64 -> i64 = add_mod
-let impl_i64__wrapping_sub: i64 -> i64 -> i64 = sub_mod
 let impl_i64__wrapping_mul: i64 -> i64 -> i64 = mul_mod
 
-let impl_u128__wrapping_add: u128 -> u128 -> u128 = add_mod
-let impl_u128__wrapping_sub: u128 -> u128 -> u128 = sub_mod
 val impl_u128__rotate_left: u128 -> u128 -> u128
 val impl_u128__from_le_bytes: t_Array u8 (sz 16) -> u128
 val impl_u128__from_be_bytes: t_Array u8 (sz 16) -> u128
@@ -110,8 +136,6 @@ val impl_u128__pow: u128 -> u32 -> u128
 val impl_i16__pow (base: i16) (exponent: u32): result: i16 {v base == 2 /\ v exponent < 15 ==> (Math.Lemmas.pow2_lt_compat 15 (v exponent); result == mk_i16 (pow2 (v exponent)))}
 val impl_i32__pow (base: i32) (exponent: u32): result: i32 {v base == 2 /\ v exponent <= 16 ==> result == mk_i32 (pow2 (v exponent))}
 
-let impl_i128__wrapping_add: i128 -> i128 -> i128 = add_mod
-let impl_i128__wrapping_sub: i128 -> i128 -> i128 = sub_mod
 
 val impl_u8__count_ones: u8 -> r:u32{v r <= 8}
 val impl_i32__count_ones: i32 -> r:u32{v r <= 32}

hax-lib/proof-libs/fstar/rust_primitives/Rust_primitives.Integers.fsti

@@ -197,6 +197,9 @@ let mul_mod (#t:inttype) (a:int_t t)
             (b:int_t t) =
             mk_int #t (v a * v b @%. t)
 
+let mul_overflow (#t:inttype) (a:int_t t)
+                 (b:int_t t) =
+                 (mk_int #t (v a * v b @%. t), (v a * v b > maxint t || v a * v b < maxint t))
 let mul (#t:inttype) (a:int_t t)
         (b:int_t t{range (v a * v b) t}) =
         mk_int #t (v a * v b)