Merge pull request #1356 from cryspen/misc-proof-libs

feat(proof-libs): add missing definitions

Author: W95Psp

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

@@ -36,6 +36,7 @@ val impl_u64__to_be_bytes: u64 -> t_Array u8 (sz 8)
 val impl_u64__rotate_right: u64 -> u64 -> u64
 
 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
@@ -51,6 +52,9 @@ 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}
 

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

@@ -15,6 +15,8 @@ val pow2_values: x:nat -> Lemma
    | 32 -> p=4294967296
    | 63 -> p=9223372036854775808
    | 64 -> p=18446744073709551616
+   | 127 -> p=170141183460469231731687303715884105728
+   | 128 -> p=340282366920938463463374607431768211456
    | 2 | 3 | 4 | 5 | 6 | 7
    | 9 | 10 | 11 | 12 | 13 | 14 | 15 
    | 17 | 18 | 19 | 20 | 21 | 22 | 23