Merge pull request #1520 from satiscugcat/main

Addition of integer function implementations in Core.Num.fsti, along with generic functions in Rust_primitives.Integer.fsti to support them.

Author: W95Psp

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

@@ -12,6 +12,7 @@ let impl_u64__MIN: u64 = mk_u64 (minint u64_inttype)
 let impl_u128__MAX: u128 = mk_u128 (maxint u128_inttype)
 let impl_u128__MIN: u128 = mk_u128 (minint u128_inttype)
 let impl_usize__MAX: usize = mk_usize (maxint usize_inttype)
+
 let impl_usize__MIN: usize = mk_usize (minint usize_inttype)
 let impl_i8__MAX: i8 = mk_i8 (maxint i8_inttype)
 let impl_i8__MIN: i8 = mk_i8 (minint i8_inttype)
@@ -26,6 +27,65 @@ let impl_i128__MIN: i128 = mk_i128 (minint i128_inttype)
 let impl_isize__MAX: isize = mk_isize (maxint isize_inttype)
 let impl_isize__MIN: isize = mk_isize (minint isize_inttype)
 
+let impl_u8__BITS: u32 = mk_int 8
+let impl_u16__BITS: u32 = mk_int 16
+let impl_u32__BITS: u32 = mk_int 32
+let impl_u64__BITS: u32 = mk_int 64
+let impl_u128__BITS: u32 = mk_int 128
+let impl_i8__BITS: u32 = mk_int 8
+let impl_i16__BITS: u32 = mk_int 16
+let impl_i32__BITS: u32 = mk_int 32
+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__saturating_add: u8 -> u8 -> u8 = add_sat
+let impl_u16__saturating_add: u16 -> u16 ->  u16 = add_sat
+let impl_u32__saturating_add: u32 -> u32 -> u32 = add_sat
+let impl_u64__saturating_add: u64 -> u64 -> u64 = add_sat
+let impl_u128__saturating_add: u128 -> u128 -> u128 = add_sat
+let impl_i8__saturating_add: i8 -> i8 -> i8 = add_sat
+let impl_i16__saturating_add: i16 -> i16 ->  i16 = add_sat
+let impl_i32__saturating_add: i32 -> i32 -> i32 = add_sat
+let impl_i64__saturating_add: i64 -> i64 -> i64 = add_sat
+let impl_i128__saturating_add: i128 -> i128 -> i128 = add_sat
+
+
+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__saturating_sub: u8 -> u8 -> u8 = sub_sat
+let impl_u16__saturating_sub: u16 -> u16 ->  u16 = sub_sat
+let impl_u32__saturating_sub: u32 -> u32 -> u32 = sub_sat
+let impl_u64__saturating_sub: u64 -> u64 -> u64 = sub_sat
+let impl_u128__saturating_sub: u128 -> u128 -> u128 = sub_sat
+let impl_i8__saturating_sub: i8 -> i8 -> i8 = sub_sat
+let impl_i16__saturating_sub: i16 -> i16 ->  i16 = sub_sat
+let impl_i32__saturating_sub: i32 -> i32 -> i32 = sub_sat
+let impl_i64__saturating_sub: i64 -> i64 -> i64 = sub_sat
+let impl_i128__saturating_sub: i128 -> i128 -> i128 = sub_sat
+
 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
@@ -39,32 +99,40 @@ 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_i8__abs (a:i8{minint i8_inttype < v a}) : i8 = abs_int a
+let impl_i16__abs (a:i16{minint i16_inttype < v a}) : i16 = abs_int a
 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_i64__abs (a:i64{minint i64_inttype < v a}) : i64 = abs_int a
+let impl_i128__abs (a:i128{minint i128_inttype < v a}) : i128 = abs_int a
+
 
-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
 val impl_u32__to_le_bytes: u32 -> t_Array u8 (sz 4)
 val impl_u32__to_be_bytes: u32 -> t_Array u8 (sz 4)
 val impl_u32__rotate_right: u32 -> u32 -> u32
-let impl_u32__BITS: u32 = mk_int 32
 
-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
@@ -77,12 +145,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
@@ -98,8 +162,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

@@ -186,6 +186,22 @@ let cast_identity_lemma
 let add_mod (#t:inttype) (a:int_t t) (b:int_t t) =
     mk_int #t ((v a + v b) @%. t)
 
+let add_sat (#t:inttype) (a:int_t t) (b:int_t t) =
+    mk_int #t (if (v a + v b) <= minint t 
+              then minint t 
+              else 
+                if (v a + v b) >= maxint t 
+                then maxint t 
+                else  (v a + v b))
+
+let sub_sat (#t:inttype) (a:int_t t) (b:int_t t) =
+    mk_int #t (if (v a - v b) <= minint t 
+              then minint t 
+              else 
+                if (v a - v b) >= maxint t 
+                then maxint t 
+                else  v a - v b)
+    
 let add (#t:inttype) (a:int_t t)
         (b:int_t t{range (v a + v b) t}) =
     mk_int #t (v a + v b)
@@ -197,6 +213,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)