feat(proof-libs): generalize shift_right_le

Author: abentkamp

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

@@ -156,31 +156,6 @@ val shift_right_trailing_zeros_nonzero_lemma_usize (a:usize) :
           (ensures (v (shift_right a (impl_usize__trailing_zeros a)) <> 0))
           [SMTPat (shift_right a (impl_usize__trailing_zeros a))]
 
-val shift_right_trailing_zeros_le_lemma_u8 (a:u8) :
-    Lemma (v (shift_right a (impl_u8__trailing_zeros a)) <= v a)
-          [SMTPat (shift_right a (impl_u8__trailing_zeros a))]
-
-val shift_right_trailing_zeros_le_lemma_u16 (a:u16) :
-    Lemma (v (shift_right a (impl_u16__trailing_zeros a)) <= v a)
-          [SMTPat (shift_right a (impl_u16__trailing_zeros a))]
-
-val shift_right_trailing_zeros_le_lemma_u32 (a:u32) :
-    Lemma (v (shift_right a (impl_u32__trailing_zeros a)) <= v a)
-          [SMTPat (shift_right a (impl_u32__trailing_zeros a))]
-
-val shift_right_trailing_zeros_le_lemma_u64 (a:u64) :
-    Lemma (v (shift_right a (impl_u64__trailing_zeros a)) <= v a)
-          [SMTPat (shift_right a (impl_u64__trailing_zeros a))]
-
-val shift_right_trailing_zeros_le_lemma_u128 (a:u128) :
-    Lemma (v (shift_right a (impl_u128__trailing_zeros a)) <= v a)
-          [SMTPat (shift_right a (impl_u128__trailing_zeros a))]
-
-val shift_right_trailing_zeros_le_lemma_usize (a:usize) :
-    Lemma (v (shift_right a (impl_usize__trailing_zeros a)) <= v a)
-          [SMTPat (shift_right a (impl_usize__trailing_zeros a))]
-
-
 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

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

@@ -340,7 +340,13 @@ val shift_right_lemma (#t:inttype) (#t':inttype)
     (a:int_t t) (b:shiftval t t'):
     Lemma (v (shift_right #t #t' a b) == (v a / pow2 (v b)))
           [SMTPat (shift_right #t #t' a b)]
-    
+
+val shift_right_le (#t:inttype) (#t':inttype)
+    (a:int_t t) (b:shiftval t t'):
+    Lemma (requires (unsigned t \/ v a >= 0))
+          (ensures (v (shift_right #t #t' a b) <= v a))
+          [SMTPat (shift_right #t #t' a b)]    
+
 val shift_left (#t:inttype) (#t':inttype)
     (a:int_t t) (b:shiftval t t') : int_t t